fix ligodity; add it to the bin; add source locations; merge
This commit is contained in:
commit
6febd855c4
@ -30,7 +30,7 @@ let literal ppf (l:literal) = match l with
|
|||||||
| Literal_address s -> fprintf ppf "@%S" s
|
| Literal_address s -> fprintf ppf "@%S" s
|
||||||
| Literal_operation _ -> fprintf ppf "Operation(...bytes)"
|
| Literal_operation _ -> fprintf ppf "Operation(...bytes)"
|
||||||
|
|
||||||
let rec expression ppf (e:expression) = match e with
|
let rec expression ppf (e:expression) = match Location.unwrap e with
|
||||||
| E_literal l -> literal ppf l
|
| E_literal l -> literal ppf l
|
||||||
| E_variable name -> fprintf ppf "%s" name
|
| E_variable name -> fprintf ppf "%s" name
|
||||||
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg
|
| E_application (f, arg) -> fprintf ppf "(%a)@(%a)" expression f expression arg
|
||||||
|
@ -35,76 +35,79 @@ let t_map key value = (T_constant ("map", [key ; value]))
|
|||||||
|
|
||||||
let make_name (s : string) : name = s
|
let make_name (s : string) : name = s
|
||||||
|
|
||||||
let e_var (s : string) : expression = E_variable s
|
let e_var ?loc (s : string) : expression = Location.wrap ?loc @@ E_variable s
|
||||||
|
let e_literal ?loc l : expression = Location.wrap ?loc @@ E_literal l
|
||||||
|
let e_unit ?loc () : expression = Location.wrap ?loc @@ E_literal (Literal_unit)
|
||||||
|
let e_int ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_int n)
|
||||||
|
let e_nat ?loc n : expression = Location.wrap ?loc @@ E_literal (Literal_nat n)
|
||||||
|
let e_bool ?loc b : expression = Location.wrap ?loc @@ E_literal (Literal_bool b)
|
||||||
|
let e_string ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_string s)
|
||||||
|
let e_address ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_address s)
|
||||||
|
let e_tez ?loc s : expression = Location.wrap ?loc @@ E_literal (Literal_tez s)
|
||||||
|
let e_bytes ?loc b : expression = Location.wrap ?loc @@ E_literal (Literal_bytes (Bytes.of_string b))
|
||||||
|
let e_record ?loc map : expression = Location.wrap ?loc @@ E_record map
|
||||||
|
let e_tuple ?loc lst : expression = Location.wrap ?loc @@ E_tuple lst
|
||||||
|
let e_some ?loc s : expression = Location.wrap ?loc @@ E_constant ("SOME", [s])
|
||||||
|
let e_none ?loc () : expression = Location.wrap ?loc @@ E_constant ("NONE", [])
|
||||||
|
let e_map_update ?loc k v old : expression = Location.wrap ?loc @@ E_constant ("MAP_UPDATE" , [k ; v ; old])
|
||||||
|
let e_map ?loc lst : expression = Location.wrap ?loc @@ E_map lst
|
||||||
|
let e_list ?loc lst : expression = Location.wrap ?loc @@ E_list lst
|
||||||
|
let e_pair ?loc a b : expression = Location.wrap ?loc @@ E_tuple [a; b]
|
||||||
|
let e_constructor ?loc s a : expression = Location.wrap ?loc @@ E_constructor (s , a)
|
||||||
|
let e_matching ?loc a b : expression = Location.wrap ?loc @@ E_matching (a , b)
|
||||||
|
let e_matching_bool ?loc a b c : expression = e_matching ?loc a (Match_bool {match_true = b ; match_false = c})
|
||||||
|
let e_accessor ?loc a b = Location.wrap ?loc @@ E_accessor (a , b)
|
||||||
|
let e_accessor_props ?loc a b = e_accessor ?loc a (List.map (fun x -> Access_record x) b)
|
||||||
|
let e_variable ?loc v = Location.wrap ?loc @@ E_variable v
|
||||||
|
let e_failwith ?loc v = Location.wrap ?loc @@ E_failwith v
|
||||||
|
let e_skip ?loc () = Location.wrap ?loc @@ E_skip
|
||||||
|
let e_loop ?loc cond body = Location.wrap ?loc @@ E_loop (cond , body)
|
||||||
|
let e_sequence ?loc a b = Location.wrap ?loc @@ E_sequence (a , b)
|
||||||
|
let e_let_in ?loc binder rhs result = Location.wrap ?loc @@ E_let_in { binder ; rhs ; result }
|
||||||
|
let e_annotation ?loc expr ty = Location.wrap ?loc @@ E_annotation (expr , ty)
|
||||||
|
let e_application ?loc a b = Location.wrap ?loc @@ E_application (a , b)
|
||||||
|
let e_binop ?loc name a b = Location.wrap ?loc @@ E_constant (name , [a ; b])
|
||||||
|
let e_constant ?loc name lst = Location.wrap ?loc @@ E_constant (name , lst)
|
||||||
|
let e_look_up ?loc x y = Location.wrap ?loc @@ E_look_up (x , y)
|
||||||
|
let e_assign ?loc a b c = Location.wrap ?loc @@ E_assign (a , b , c)
|
||||||
|
|
||||||
let e_unit () : expression = E_literal (Literal_unit)
|
let make_option_typed ?loc e t_opt =
|
||||||
let e_int n : expression = E_literal (Literal_int n)
|
|
||||||
let e_nat n : expression = E_literal (Literal_nat n)
|
|
||||||
let e_bool b : expression = E_literal (Literal_bool b)
|
|
||||||
let e_string s : expression = E_literal (Literal_string s)
|
|
||||||
let e_address s : expression = E_literal (Literal_address s)
|
|
||||||
let e_tez s : expression = E_literal (Literal_tez s)
|
|
||||||
let e_bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b))
|
|
||||||
let e_record map : expression = E_record map
|
|
||||||
let e_tuple lst : expression = E_tuple lst
|
|
||||||
let e_some s : expression = E_constant ("SOME", [s])
|
|
||||||
let e_none : expression = E_constant ("NONE", [])
|
|
||||||
let e_map_update k v old : expression = E_constant ("MAP_UPDATE" , [k ; v ; old])
|
|
||||||
let e_map lst : expression = E_map lst
|
|
||||||
let e_list lst : expression = E_list lst
|
|
||||||
let e_pair a b : expression = E_tuple [a; b]
|
|
||||||
let e_constructor s a : expression = E_constructor (s , a)
|
|
||||||
let e_match a b : expression = E_matching (a , b)
|
|
||||||
let e_match_bool a b c : expression = e_match a (Match_bool {match_true = b ; match_false = c})
|
|
||||||
let e_accessor a b = E_accessor (a , b)
|
|
||||||
let e_accessor_props a b = e_accessor a (List.map (fun x -> Access_record x) b)
|
|
||||||
let e_variable v = E_variable v
|
|
||||||
let e_failwith v = E_failwith v
|
|
||||||
let e_skip = E_skip
|
|
||||||
let e_loop cond body = E_loop (cond , body)
|
|
||||||
let e_sequence a b = E_sequence (a , b)
|
|
||||||
let e_let_in binder rhs result = E_let_in { binder ; rhs ; result }
|
|
||||||
let e_annotation expr ty = E_annotation (expr , ty)
|
|
||||||
let e_application a b = E_application (a , b)
|
|
||||||
|
|
||||||
let e_binop name a b = E_constant (name , [a ; b])
|
|
||||||
|
|
||||||
let make_option_typed e t_opt =
|
|
||||||
match t_opt with
|
match t_opt with
|
||||||
| None -> e
|
| None -> e
|
||||||
| Some t -> e_annotation e t
|
| Some t -> e_annotation ?loc e t
|
||||||
|
|
||||||
|
|
||||||
let ez_e_record lst =
|
let ez_e_record ?loc lst =
|
||||||
let aux prev (k, v) = SMap.add k v prev in
|
let aux prev (k, v) = SMap.add k v prev in
|
||||||
let map = List.fold_left aux SMap.empty lst in
|
let map = List.fold_left aux SMap.empty lst in
|
||||||
e_record map
|
e_record ?loc map
|
||||||
|
|
||||||
let e_typed_none t_opt =
|
let e_typed_none ?loc t_opt =
|
||||||
let type_annotation = t_option t_opt in
|
let type_annotation = t_option t_opt in
|
||||||
e_annotation e_none type_annotation
|
e_annotation ?loc (e_none ?loc ()) type_annotation
|
||||||
|
|
||||||
let e_typed_list lst t =
|
let e_typed_list ?loc lst t =
|
||||||
e_annotation (e_list lst) (t_list t)
|
e_annotation ?loc (e_list lst) (t_list t)
|
||||||
|
|
||||||
let e_map lst k v = e_annotation (e_map lst) (t_map k v)
|
let e_typed_map ?loc lst k v = e_annotation ?loc (e_map lst) (t_map k v)
|
||||||
|
|
||||||
let e_lambda (binder : string)
|
let e_lambda ?loc (binder : string)
|
||||||
(input_type : type_expression option)
|
(input_type : type_expression option)
|
||||||
(output_type : type_expression option)
|
(output_type : type_expression option)
|
||||||
(result : expression)
|
(result : expression)
|
||||||
: expression =
|
: expression =
|
||||||
E_lambda {
|
Location.wrap ?loc @@ E_lambda {
|
||||||
binder = (make_name binder , input_type) ;
|
binder = (make_name binder , input_type) ;
|
||||||
input_type = input_type ;
|
input_type = input_type ;
|
||||||
output_type = output_type ;
|
output_type = output_type ;
|
||||||
result ;
|
result ;
|
||||||
}
|
}
|
||||||
|
|
||||||
let e_record (lst : (string * expr) list) : expression =
|
let e_record ?loc map = Location.wrap ?loc @@ E_record map
|
||||||
let aux prev (k, v) = SMap.add k v prev in
|
|
||||||
let map = List.fold_left aux SMap.empty lst in
|
let e_ez_record ?loc (lst : (string * expr) list) : expression =
|
||||||
E_record map
|
let map = SMap.of_list lst in
|
||||||
|
e_record ?loc map
|
||||||
|
|
||||||
let get_e_accessor = fun t ->
|
let get_e_accessor = fun t ->
|
||||||
match t with
|
match t with
|
||||||
@ -130,3 +133,10 @@ let get_e_list = fun t ->
|
|||||||
match t with
|
match t with
|
||||||
| E_list lst -> ok lst
|
| E_list lst -> ok lst
|
||||||
| _ -> simple_fail "not a pair"
|
| _ -> simple_fail "not a pair"
|
||||||
|
|
||||||
|
let get_e_failwith = fun e ->
|
||||||
|
match Location.unwrap e with
|
||||||
|
| E_failwith fw -> ok fw
|
||||||
|
| _ -> simple_fail "not a failwith"
|
||||||
|
|
||||||
|
let is_e_failwith e = to_bool @@ get_e_failwith e
|
||||||
|
@ -35,7 +35,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
|
|||||||
Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
|
Format.asprintf "\n@[<v>- %a@;- %a]" PP.expression a PP.expression b
|
||||||
in
|
in
|
||||||
trace (fun () -> error (thunk "not equal") error_content ()) @@
|
trace (fun () -> error (thunk "not equal") error_content ()) @@
|
||||||
match (a , b) with
|
match (Location.unwrap a , Location.unwrap b) with
|
||||||
| E_literal a , E_literal b ->
|
| E_literal a , E_literal b ->
|
||||||
assert_literal_eq (a, b)
|
assert_literal_eq (a, b)
|
||||||
| E_literal _ , _ ->
|
| E_literal _ , _ ->
|
||||||
@ -113,8 +113,8 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
|
|||||||
)
|
)
|
||||||
| E_list _, _ ->
|
| E_list _, _ ->
|
||||||
simple_fail "comparing list with other stuff"
|
simple_fail "comparing list with other stuff"
|
||||||
| (E_annotation (a , _) , b) -> assert_value_eq (a , b)
|
| (E_annotation (a , _) , _b') -> assert_value_eq (a , b)
|
||||||
| (a , E_annotation (b , _)) -> assert_value_eq (a , b)
|
| (_a' , E_annotation (b , _)) -> assert_value_eq (a , b)
|
||||||
| (E_variable _, _) | (E_lambda _, _)
|
| (E_variable _, _) | (E_lambda _, _)
|
||||||
| (E_application _, _) | (E_let_in _, _)
|
| (E_application _, _) | (E_let_in _, _)
|
||||||
| (E_accessor _, _)
|
| (E_accessor _, _)
|
||||||
|
@ -42,7 +42,7 @@ and let_in = {
|
|||||||
result : expr ;
|
result : expr ;
|
||||||
}
|
}
|
||||||
|
|
||||||
and expression =
|
and expression' =
|
||||||
(* Base *)
|
(* Base *)
|
||||||
| E_literal of literal
|
| E_literal of literal
|
||||||
| E_constant of (name * expr list) (* For language constants, like (Cons hd tl) or (plus i j) *)
|
| E_constant of (name * expr list) (* For language constants, like (Cons hd tl) or (plus i j) *)
|
||||||
@ -72,6 +72,8 @@ and expression =
|
|||||||
(* Annotate *)
|
(* Annotate *)
|
||||||
| E_annotation of expr * type_expression
|
| E_annotation of expr * type_expression
|
||||||
|
|
||||||
|
and expression = expression' Location.wrap
|
||||||
|
|
||||||
and access =
|
and access =
|
||||||
| Access_tuple of int
|
| Access_tuple of int
|
||||||
| Access_record of string
|
| Access_record of string
|
||||||
|
@ -2,7 +2,13 @@ open Trace
|
|||||||
open Types
|
open Types
|
||||||
|
|
||||||
let make_t type_value' simplified = { type_value' ; simplified }
|
let make_t type_value' simplified = { type_value' ; simplified }
|
||||||
let make_a_e expression type_annotation environment = { expression ; type_annotation ; dummy_field = () ; environment }
|
let make_a_e ?(location = Location.generated) expression type_annotation environment = {
|
||||||
|
expression ;
|
||||||
|
type_annotation ;
|
||||||
|
dummy_field = () ;
|
||||||
|
environment ;
|
||||||
|
location ;
|
||||||
|
}
|
||||||
let make_n_e name a_e = { name ; annotated_expression = a_e }
|
let make_n_e name a_e = { name ; annotated_expression = a_e }
|
||||||
let make_n_t type_name type_value = { type_name ; type_value }
|
let make_n_t type_name type_value = { type_name ; type_value }
|
||||||
|
|
||||||
|
@ -37,6 +37,7 @@ and annotated_expression = {
|
|||||||
expression : expression ;
|
expression : expression ;
|
||||||
type_annotation : tv ;
|
type_annotation : tv ;
|
||||||
environment : full_environment ;
|
environment : full_environment ;
|
||||||
|
location : Location.t ;
|
||||||
dummy_field : unit ;
|
dummy_field : unit ;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,4 +1,4 @@
|
|||||||
type storage = int
|
type storage = int
|
||||||
|
|
||||||
let%entry main (p:int) storage =
|
let%entry main (p:int) storage =
|
||||||
((list [] : operation list) , p + storage)
|
(([] : operation list) , p + storage)
|
||||||
|
@ -327,7 +327,7 @@ and let_in = {
|
|||||||
|
|
||||||
and fun_expr = {
|
and fun_expr = {
|
||||||
kwd_fun : kwd_fun;
|
kwd_fun : kwd_fun;
|
||||||
param : variable;
|
params : pattern list;
|
||||||
p_annot : (colon * type_expr) option;
|
p_annot : (colon * type_expr) option;
|
||||||
arrow : arrow;
|
arrow : arrow;
|
||||||
body : expr
|
body : expr
|
||||||
@ -737,10 +737,10 @@ and print_let_in (bind: let_in) =
|
|||||||
print_expr body
|
print_expr body
|
||||||
|
|
||||||
and print_fun_expr {value; _} =
|
and print_fun_expr {value; _} =
|
||||||
let {kwd_fun; param; p_annot; arrow; body} = value in
|
let {kwd_fun; params; p_annot; arrow; body} = value in
|
||||||
print_token kwd_fun "fun";
|
print_token kwd_fun "fun";
|
||||||
(match p_annot with
|
(match p_annot with
|
||||||
None -> print_var param
|
None -> List.iter print_pattern params
|
||||||
| Some (colon, type_expr) ->
|
| Some (colon, type_expr) ->
|
||||||
print_token colon ":";
|
print_token colon ":";
|
||||||
print_type_expr type_expr);
|
print_type_expr type_expr);
|
||||||
|
@ -336,7 +336,7 @@ and let_in = {
|
|||||||
|
|
||||||
and fun_expr = {
|
and fun_expr = {
|
||||||
kwd_fun : kwd_fun;
|
kwd_fun : kwd_fun;
|
||||||
param : variable;
|
params : pattern list;
|
||||||
p_annot : (colon * type_expr) option;
|
p_annot : (colon * type_expr) option;
|
||||||
arrow : arrow;
|
arrow : arrow;
|
||||||
body : expr
|
body : expr
|
||||||
|
@ -7,10 +7,10 @@ open AST
|
|||||||
|
|
||||||
module VMap = Utils.String.Map
|
module VMap = Utils.String.Map
|
||||||
|
|
||||||
let ghost_of value = Region.{region=ghost; value}
|
(*let ghost_of value = Region.{region=ghost; value}*)
|
||||||
let ghost = Region.ghost
|
let ghost = Region.ghost
|
||||||
|
|
||||||
let fail_syn_unif type1 type2 : 'a =
|
(* let fail_syn_unif type1 type2 : 'a =
|
||||||
let reg = AST.region_of_type_expr type1 in
|
let reg = AST.region_of_type_expr type1 in
|
||||||
let reg = reg#compact ~file:false `Byte in
|
let reg = reg#compact ~file:false `Byte in
|
||||||
let value =
|
let value =
|
||||||
@ -25,6 +25,7 @@ let mk_component rank =
|
|||||||
let par = {lpar=ghost; inside = ghost_of num; rpar=ghost}
|
let par = {lpar=ghost; inside = ghost_of num; rpar=ghost}
|
||||||
in Component (ghost_of par)
|
in Component (ghost_of par)
|
||||||
|
|
||||||
|
|
||||||
let rec mk_field_path (rank, tail) =
|
let rec mk_field_path (rank, tail) =
|
||||||
let head = mk_component rank in
|
let head = mk_component rank in
|
||||||
match tail with
|
match tail with
|
||||||
@ -35,12 +36,7 @@ let mk_projection fresh (path : int Utils.nseq) = {
|
|||||||
struct_name = fresh;
|
struct_name = fresh;
|
||||||
selector = ghost;
|
selector = ghost;
|
||||||
field_path = Utils.nsepseq_rev (mk_field_path path)
|
field_path = Utils.nsepseq_rev (mk_field_path path)
|
||||||
}
|
} *)
|
||||||
|
|
||||||
let rec sub_rec fresh path (map, rank) pattern =
|
|
||||||
let path' = Utils.nseq_cons rank path in
|
|
||||||
let map' = split fresh map path' pattern
|
|
||||||
in map', rank+1
|
|
||||||
|
|
||||||
|
|
||||||
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
|
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
|
||||||
@ -198,7 +194,7 @@ declarations:
|
|||||||
declaration:
|
declaration:
|
||||||
reg(kwd(LetEntry) entry_binding {$1,$2}) { LetEntry $1, [] }
|
reg(kwd(LetEntry) entry_binding {$1,$2}) { LetEntry $1, [] }
|
||||||
| reg(type_decl) { TypeDecl $1, [] }
|
| reg(type_decl) { TypeDecl $1, [] }
|
||||||
| let_declaration { $1 }
|
| let_declaration { $1, [] }
|
||||||
|
|
||||||
(* Type declarations *)
|
(* Type declarations *)
|
||||||
|
|
||||||
@ -284,36 +280,32 @@ field_decl:
|
|||||||
entry_binding:
|
entry_binding:
|
||||||
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
let let_rhs = $5 in
|
let let_rhs = $5 in
|
||||||
{bindings = ($1 , $2); lhs_type=$3; eq=$4; let_rhs}
|
let pattern = PVar $1 in
|
||||||
|
let (hd , tl) = $2 in
|
||||||
|
{bindings = pattern :: hd :: tl; lhs_type=$3; eq=$4; let_rhs}
|
||||||
}
|
}
|
||||||
| ident type_annotation? eq fun_expr(expr) {
|
| ident type_annotation? eq fun_expr(expr) {
|
||||||
{bindings = ($1 , []); lhs_type=$2; eq=$3; let_rhs=$4} }
|
let pattern = PVar $1 in
|
||||||
|
{bindings = [pattern]; lhs_type=$2; eq=$3; let_rhs=$4} }
|
||||||
|
|
||||||
(* Top-level non-recursive definitions *)
|
(* Top-level non-recursive definitions *)
|
||||||
|
|
||||||
let_declaration:
|
let_declaration:
|
||||||
reg(kwd(Let) let_binding {$1,$2}) {
|
reg(kwd(Let) let_binding {$1,$2}) {
|
||||||
let kwd_let, (binding, map) = $1.value in
|
let kwd_let, binding = $1.value in
|
||||||
let let0 = Let {$1 with value = kwd_let, binding}
|
Let {$1 with value = kwd_let, binding}
|
||||||
in
|
|
||||||
mk_let_bindings map (let0,[])
|
|
||||||
}
|
}
|
||||||
|
|
||||||
let_binding:
|
let_binding:
|
||||||
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
let let_rhs = $5 in
|
let let_rhs = $5 in
|
||||||
let map = VMap.empty in
|
let ident_pattern = PVar $1 in
|
||||||
{bindings= ($1 , $2); lhs_type=$3; eq=$4; let_rhs}, map
|
let (hd , tl) = $2 in
|
||||||
|
{bindings= (ident_pattern :: hd :: tl); lhs_type=$3; eq=$4; let_rhs}
|
||||||
}
|
}
|
||||||
| irrefutable type_annotation? eq expr {
|
| irrefutable type_annotation? eq expr {
|
||||||
let variable, type_opt, map = split_pattern $1 in
|
let pattern = $1 in
|
||||||
match type_opt, $2 with
|
{bindings = [pattern]; lhs_type=$2; eq=$3; let_rhs=$4}
|
||||||
Some type1, Some (_,type2) when type1 <> type2 ->
|
|
||||||
fail_syn_unif type1 type2
|
|
||||||
| Some type1, None ->
|
|
||||||
let lhs_type = Some (ghost, type1) in
|
|
||||||
{variable; lhs_type; eq=$3; let_rhs=$4}, map
|
|
||||||
| _ -> {variable; lhs_type=$2; eq=$3; let_rhs=$4}, map
|
|
||||||
}
|
}
|
||||||
|
|
||||||
type_annotation:
|
type_annotation:
|
||||||
@ -459,13 +451,23 @@ case_clause(right_expr):
|
|||||||
|
|
||||||
let_expr(right_expr):
|
let_expr(right_expr):
|
||||||
reg(kwd(Let) let_binding kwd(In) right_expr {$1,$2,$3,$4}) {
|
reg(kwd(Let) let_binding kwd(In) right_expr {$1,$2,$3,$4}) {
|
||||||
let kwd_let, (binding, map), kwd_in, body = $1.value in
|
let kwd_let, binding , kwd_in, body = $1.value in
|
||||||
let body = mk_let_in_bindings map body in
|
|
||||||
let let_in = {kwd_let; binding; kwd_in; body}
|
let let_in = {kwd_let; binding; kwd_in; body}
|
||||||
in ELetIn {region=$1.region; value=let_in} }
|
in ELetIn {region=$1.region; value=let_in} }
|
||||||
|
|
||||||
fun_expr(right_expr):
|
fun_expr(right_expr):
|
||||||
kwd(Fun) nseq(irrefutable) arrow right_expr { norm_fun_expr $2 $4 }
|
reg(kwd(Fun) nseq(irrefutable) arrow right_expr {$1,$2,$3,$4}) {
|
||||||
|
let kwd_fun, bindings, arrow, body = $1.value in
|
||||||
|
let (hd , tl) = bindings in
|
||||||
|
let f = {
|
||||||
|
kwd_fun ;
|
||||||
|
params = hd :: tl ;
|
||||||
|
p_annot = None ;
|
||||||
|
arrow ;
|
||||||
|
body ;
|
||||||
|
} in
|
||||||
|
EFun { region=$1.region; value=f }
|
||||||
|
}
|
||||||
|
|
||||||
disj_expr_level:
|
disj_expr_level:
|
||||||
reg(disj_expr) { ELogic (BoolExpr (Or $1)) }
|
reg(disj_expr) { ELogic (BoolExpr (Or $1)) }
|
||||||
|
@ -206,7 +206,7 @@ and ifthenelse
|
|||||||
let%bind cond' = bind_map_location expression cond in
|
let%bind cond' = bind_map_location expression cond in
|
||||||
let%bind branch_true' = bind_map_location expression branch_true in
|
let%bind branch_true' = bind_map_location expression branch_true in
|
||||||
let%bind branch_false' = bind_map_location expression branch_false in
|
let%bind branch_false' = bind_map_location expression branch_false in
|
||||||
ok @@ O.(e_match_bool (unwrap cond') (unwrap branch_true') (unwrap branch_false'))
|
ok @@ O.(e_matching_bool (unwrap cond') (unwrap branch_true') (unwrap branch_false'))
|
||||||
|
|
||||||
and ifthen
|
and ifthen
|
||||||
: (I.expression Location.wrap * I.expression Location.wrap) -> O.expression result
|
: (I.expression Location.wrap * I.expression Location.wrap) -> O.expression result
|
||||||
@ -214,7 +214,7 @@ and ifthen
|
|||||||
let (cond , branch_true) = it in
|
let (cond , branch_true) = it in
|
||||||
let%bind cond' = bind_map_location expression cond in
|
let%bind cond' = bind_map_location expression cond in
|
||||||
let%bind branch_true' = bind_map_location expression branch_true in
|
let%bind branch_true' = bind_map_location expression branch_true in
|
||||||
ok @@ O.(e_match_bool (unwrap cond') (unwrap branch_true') (e_unit ()))
|
ok @@ O.(e_matching_bool (unwrap cond') (unwrap branch_true') (e_unit ()))
|
||||||
|
|
||||||
and match_
|
and match_
|
||||||
: I.expression Location.wrap * I.e_match_clause Location.wrap list -> O.expression result
|
: I.expression Location.wrap * I.e_match_clause Location.wrap list -> O.expression result
|
||||||
@ -231,7 +231,7 @@ and match_
|
|||||||
ok (x' , y') in
|
ok (x' , y') in
|
||||||
bind_map_list aux clauses in
|
bind_map_list aux clauses in
|
||||||
let%bind matching = match_clauses clauses' in
|
let%bind matching = match_clauses clauses' in
|
||||||
ok O.(e_match expr' matching)
|
ok O.(e_matching expr' matching)
|
||||||
|
|
||||||
and record
|
and record
|
||||||
= fun r ->
|
= fun r ->
|
||||||
@ -244,7 +244,7 @@ and record
|
|||||||
in
|
in
|
||||||
let%bind r' = bind_map_list (bind_map_location aux) r in
|
let%bind r' = bind_map_list (bind_map_location aux) r in
|
||||||
let lst = List.map ((fun (x, y) -> unwrap x, unwrap y) >| unwrap) r' in
|
let lst = List.map ((fun (x, y) -> unwrap x, unwrap y) >| unwrap) r' in
|
||||||
ok @@ O.(e_record lst)
|
ok @@ O.(e_ez_record lst)
|
||||||
|
|
||||||
and expression_main : I.expression_main Location.wrap -> O.expression result = fun em ->
|
and expression_main : I.expression_main Location.wrap -> O.expression result = fun em ->
|
||||||
let return x = ok @@ x in
|
let return x = ok @@ x in
|
||||||
@ -334,13 +334,13 @@ and expression_main : I.expression_main Location.wrap -> O.expression result = f
|
|||||||
and identifier_application : (string Location.wrap) list * string Location.wrap -> O.expression option -> _ result = fun (lst , v) param_opt ->
|
and identifier_application : (string Location.wrap) list * string Location.wrap -> O.expression option -> _ result = fun (lst , v) param_opt ->
|
||||||
let constant_name = String.concat "." ((List.map unwrap lst) @ [unwrap v]) in
|
let constant_name = String.concat "." ((List.map unwrap lst) @ [unwrap v]) in
|
||||||
match List.assoc_opt constant_name constants , param_opt with
|
match List.assoc_opt constant_name constants , param_opt with
|
||||||
| Some s , None -> ok O.(E_constant (s , []))
|
| Some s , None -> ok O.(e_constant s [])
|
||||||
| Some s , Some param -> (
|
| Some s , Some param -> (
|
||||||
let params =
|
let params =
|
||||||
match param with
|
match Location.unwrap param with
|
||||||
| E_tuple lst -> lst
|
| E_tuple lst -> lst
|
||||||
| _ -> [ param ] in
|
| _ -> [ param ] in
|
||||||
ok O.(E_constant (s , params))
|
ok O.(e_constant s params)
|
||||||
)
|
)
|
||||||
| None , param_opt -> (
|
| None , param_opt -> (
|
||||||
let%bind () =
|
let%bind () =
|
||||||
|
@ -19,6 +19,35 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value
|
|||||||
|
|
||||||
open Operators.Simplify.Ligodity
|
open Operators.Simplify.Ligodity
|
||||||
|
|
||||||
|
let r_split = Location.r_split
|
||||||
|
|
||||||
|
let rec pattern_to_var : Raw.pattern -> _ = fun p ->
|
||||||
|
match p with
|
||||||
|
| Raw.PPar p -> pattern_to_var p.value.inside
|
||||||
|
| Raw.PVar v -> ok v
|
||||||
|
| _ -> simple_fail "not a var"
|
||||||
|
|
||||||
|
let rec pattern_to_typed_var : Raw.pattern -> _ = fun p ->
|
||||||
|
match p with
|
||||||
|
| Raw.PPar p -> pattern_to_typed_var p.value.inside
|
||||||
|
| Raw.PTyped tp -> (
|
||||||
|
let tp = tp.value in
|
||||||
|
let%bind v = pattern_to_var tp.pattern in
|
||||||
|
ok (v , Some tp.type_expr)
|
||||||
|
)
|
||||||
|
| Raw.PVar v -> ok (v , None)
|
||||||
|
| _ -> simple_fail "not a var"
|
||||||
|
|
||||||
|
let rec expr_to_typed_expr : Raw.expr -> _ = fun e ->
|
||||||
|
match e with
|
||||||
|
| EPar e -> expr_to_typed_expr e.value.inside
|
||||||
|
| EAnnot a -> ok (fst a.value , Some (snd a.value))
|
||||||
|
| _ -> ok (e , None)
|
||||||
|
|
||||||
|
let patterns_to_var : Raw.pattern list -> _ = fun ps ->
|
||||||
|
let%bind () = Assert.assert_list_size ps 1 in
|
||||||
|
pattern_to_var @@ List.hd ps
|
||||||
|
|
||||||
let rec simpl_type_expression : Raw.type_expr -> type_expression result =
|
let rec simpl_type_expression : Raw.type_expr -> type_expression result =
|
||||||
function
|
function
|
||||||
| TPar x -> simpl_type_expression x.value.inside
|
| TPar x -> simpl_type_expression x.value.inside
|
||||||
@ -79,9 +108,10 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
|
|||||||
ok @@ T_tuple lst
|
ok @@ T_tuple lst
|
||||||
|
|
||||||
let rec simpl_expression :
|
let rec simpl_expression :
|
||||||
?te_annot:type_expression -> Raw.expr -> expr result = fun ?te_annot t ->
|
Raw.expr -> expr result = fun t ->
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok x in
|
||||||
let simpl_projection = fun (p:Raw.projection) ->
|
let simpl_projection = fun (p:Raw.projection Region.reg) ->
|
||||||
|
let (p , loc) = r_split p in
|
||||||
let var =
|
let var =
|
||||||
let name = p.struct_name.value in
|
let name = p.struct_name.value in
|
||||||
e_variable name in
|
e_variable name in
|
||||||
@ -95,10 +125,8 @@ let rec simpl_expression :
|
|||||||
Access_tuple (Z.to_int (snd index.value))
|
Access_tuple (Z.to_int (snd index.value))
|
||||||
in
|
in
|
||||||
List.map aux @@ npseq_to_list path in
|
List.map aux @@ npseq_to_list path in
|
||||||
return @@ E_accessor (var, path')
|
return @@ e_accessor ~loc var path'
|
||||||
in
|
in
|
||||||
let mk_let_in binder rhs result =
|
|
||||||
E_let_in {binder; rhs; result} in
|
|
||||||
|
|
||||||
trace (
|
trace (
|
||||||
let title () = "simplifying expression" in
|
let title () = "simplifying expression" in
|
||||||
@ -111,99 +139,122 @@ let rec simpl_expression :
|
|||||||
match t with
|
match t with
|
||||||
| Raw.ELetIn e -> (
|
| Raw.ELetIn e -> (
|
||||||
let Raw.{binding ; body ; _} = e.value in
|
let Raw.{binding ; body ; _} = e.value in
|
||||||
let Raw.{variable; lhs_type; let_rhs; _} = binding in
|
let Raw.{bindings ; lhs_type ; let_rhs ; _} = binding in
|
||||||
let%bind type_annotation = bind_map_option
|
let%bind variable = patterns_to_var bindings in
|
||||||
|
let%bind ty_opt =
|
||||||
|
bind_map_option
|
||||||
(fun (_ , type_expr) -> simpl_type_expression type_expr)
|
(fun (_ , type_expr) -> simpl_type_expression type_expr)
|
||||||
lhs_type in
|
lhs_type in
|
||||||
let%bind rhs = simpl_expression ?te_annot:type_annotation let_rhs in
|
let%bind rhs = simpl_expression let_rhs in
|
||||||
|
let rhs' =
|
||||||
|
match ty_opt with
|
||||||
|
| None -> rhs
|
||||||
|
| Some ty -> e_annotation rhs ty in
|
||||||
let%bind body = simpl_expression body in
|
let%bind body = simpl_expression body in
|
||||||
return @@ mk_let_in (variable.value , None) rhs body
|
return @@ e_let_in (variable.value , None) rhs' body
|
||||||
)
|
)
|
||||||
| Raw.EAnnot a -> (
|
| Raw.EAnnot a -> (
|
||||||
let (expr , type_expr) = a.value in
|
let (a , loc) = r_split a in
|
||||||
match te_annot with
|
let (expr , type_expr) = a in
|
||||||
| None -> (
|
let%bind expr' = simpl_expression expr in
|
||||||
let%bind te_annot = simpl_type_expression type_expr in
|
let%bind type_expr' = simpl_type_expression type_expr in
|
||||||
let%bind expr' = simpl_expression ~te_annot expr in
|
return @@ e_annotation ~loc expr' type_expr'
|
||||||
ok expr'
|
|
||||||
)
|
|
||||||
| Some _ -> simple_fail "no double annotation"
|
|
||||||
)
|
)
|
||||||
| EVar c -> (
|
| EVar c -> (
|
||||||
let c' = c.value in
|
let c' = c.value in
|
||||||
match List.assoc_opt c' constants with
|
match List.assoc_opt c' constants with
|
||||||
| None -> return @@ E_variable c.value
|
| None -> return @@ e_variable c.value
|
||||||
| Some s -> return @@ E_constant (s , [])
|
| Some s -> return @@ e_constant s []
|
||||||
)
|
)
|
||||||
| ECall x -> (
|
| ECall x -> (
|
||||||
let (e1, e2) = x.value in
|
let ((e1 , e2) , loc) = r_split x in
|
||||||
let%bind args = bind_map_list simpl_expression (nseq_to_list e2) in
|
let%bind args = bind_map_list simpl_expression (nseq_to_list e2) in
|
||||||
match e1 with
|
match e1 with
|
||||||
| EVar f ->
|
| EVar f -> (
|
||||||
(match List.assoc_opt f.value constants with
|
let (f , f_loc) = r_split f in
|
||||||
| None ->
|
match List.assoc_opt f constants with
|
||||||
|
| None -> (
|
||||||
let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
|
let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
|
||||||
return @@ E_application (e_variable f.value, arg)
|
return @@ e_application ~loc (e_variable ~loc:f_loc f) arg
|
||||||
| Some s -> return @@ E_constant (s , args))
|
)
|
||||||
| e1 ->
|
| Some s -> return @@ e_constant ~loc s args
|
||||||
|
)
|
||||||
|
| e1 -> (
|
||||||
let%bind e1' = simpl_expression e1 in
|
let%bind e1' = simpl_expression e1 in
|
||||||
let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
|
let%bind arg = simpl_tuple_expression (nseq_to_list e2) in
|
||||||
return @@ E_application (e1' , arg)
|
return @@ e_application ~loc e1' arg
|
||||||
)
|
)
|
||||||
| EPar x -> simpl_expression ?te_annot x.value.inside
|
)
|
||||||
| EUnit _ -> return @@ E_literal Literal_unit
|
| EPar x -> simpl_expression x.value.inside
|
||||||
| EBytes x -> return @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value))
|
| EUnit reg -> (
|
||||||
| ETuple tpl -> simpl_tuple_expression ?te_annot @@ (npseq_to_list tpl.value)
|
let (_ , loc) = r_split reg in
|
||||||
| ERecord r ->
|
return @@ e_literal ~loc Literal_unit
|
||||||
|
)
|
||||||
|
| EBytes x -> (
|
||||||
|
let (x , loc) = r_split x in
|
||||||
|
return @@ e_literal ~loc (Literal_bytes (Bytes.of_string @@ fst x))
|
||||||
|
)
|
||||||
|
| ETuple tpl -> simpl_tuple_expression @@ (npseq_to_list tpl.value)
|
||||||
|
| ERecord r -> (
|
||||||
|
let (r , loc) = r_split r in
|
||||||
let%bind fields = bind_list
|
let%bind fields = bind_list
|
||||||
@@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
|
@@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
|
||||||
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
|
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
|
||||||
@@ pseq_to_list r.value.elements in
|
@@ pseq_to_list r.elements in
|
||||||
let aux prev (k, v) = SMap.add k v prev in
|
let map = SMap.of_list fields in
|
||||||
return @@ E_record (List.fold_left aux SMap.empty fields)
|
return @@ e_record ~loc map
|
||||||
| EProj p' -> (
|
|
||||||
let p = p'.value in
|
|
||||||
simpl_projection p
|
|
||||||
)
|
)
|
||||||
| EConstr c ->
|
| EProj p -> simpl_projection p
|
||||||
let (c, args) = c.value in
|
| EConstr c -> (
|
||||||
|
let ((c_name , args) , loc) = r_split c in
|
||||||
|
let (c_name , _c_loc) = r_split c_name in
|
||||||
let args =
|
let args =
|
||||||
match args with
|
match args with
|
||||||
None -> []
|
None -> []
|
||||||
| Some arg -> [arg] in
|
| Some arg -> [arg] in
|
||||||
let%bind arg = simpl_tuple_expression @@ args in
|
let%bind arg = simpl_tuple_expression @@ args in
|
||||||
return @@ E_constructor (c.value, arg)
|
return @@ e_constructor ~loc c_name arg
|
||||||
|
)
|
||||||
| EArith (Add c) ->
|
| EArith (Add c) ->
|
||||||
simpl_binop ?te_annot "ADD" c.value
|
simpl_binop "ADD" c
|
||||||
| EArith (Sub c) ->
|
| EArith (Sub c) ->
|
||||||
simpl_binop ?te_annot "SUB" c.value
|
simpl_binop "SUB" c
|
||||||
| EArith (Mult c) ->
|
| EArith (Mult c) ->
|
||||||
simpl_binop ?te_annot "TIMES" c.value
|
simpl_binop "TIMES" c
|
||||||
| EArith (Div c) ->
|
| EArith (Div c) ->
|
||||||
simpl_binop ?te_annot "DIV" c.value
|
simpl_binop "DIV" c
|
||||||
| EArith (Mod c) ->
|
| EArith (Mod c) ->
|
||||||
simpl_binop ?te_annot "MOD" c.value
|
simpl_binop "MOD" c
|
||||||
| EArith (Int n) ->
|
| EArith (Int n) -> (
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
let (n , loc) = r_split n in
|
||||||
return @@ E_literal (Literal_int n)
|
let n = Z.to_int @@ snd @@ n in
|
||||||
| EArith (Nat n) ->
|
return @@ e_literal ~loc (Literal_int n)
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
)
|
||||||
return @@ E_literal (Literal_nat n)
|
| EArith (Nat n) -> (
|
||||||
| EArith (Mtz n) ->
|
let (n , loc) = r_split n in
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
let n = Z.to_int @@ snd @@ n in
|
||||||
return @@ E_literal (Literal_tez n)
|
return @@ e_literal ~loc (Literal_nat n)
|
||||||
|
)
|
||||||
|
| EArith (Mtz n) -> (
|
||||||
|
let (n , loc) = r_split n in
|
||||||
|
let n = Z.to_int @@ snd @@ n in
|
||||||
|
return @@ e_literal ~loc (Literal_tez n)
|
||||||
|
)
|
||||||
| EArith _ -> simple_fail "arith: not supported yet"
|
| EArith _ -> simple_fail "arith: not supported yet"
|
||||||
| EString (String s) ->
|
| EString (String s) -> (
|
||||||
|
let (s , loc) = r_split s in
|
||||||
let s' =
|
let s' =
|
||||||
let s = s.value in
|
let s = s in
|
||||||
String.(sub s 1 ((length s) - 2))
|
String.(sub s 1 ((length s) - 2))
|
||||||
in
|
in
|
||||||
return @@ E_literal (Literal_string s')
|
return @@ e_literal ~loc (Literal_string s')
|
||||||
|
)
|
||||||
| EString _ -> simple_fail "string: not supported yet"
|
| EString _ -> simple_fail "string: not supported yet"
|
||||||
| ELogic l -> simpl_logic_expression ?te_annot l
|
| ELogic l -> simpl_logic_expression l
|
||||||
| EList l -> simpl_list_expression ?te_annot l
|
| EList l -> simpl_list_expression l
|
||||||
| ECase c -> (
|
| ECase c -> (
|
||||||
let%bind e = simpl_expression c.value.expr in
|
let (c , loc) = r_split c in
|
||||||
|
let%bind e = simpl_expression c.expr in
|
||||||
let%bind lst =
|
let%bind lst =
|
||||||
let aux (x : Raw.expr Raw.case_clause) =
|
let aux (x : Raw.expr Raw.case_clause) =
|
||||||
let%bind expr = simpl_expression x.rhs in
|
let%bind expr = simpl_expression x.rhs in
|
||||||
@ -211,10 +262,10 @@ let rec simpl_expression :
|
|||||||
bind_list
|
bind_list
|
||||||
@@ List.map aux
|
@@ List.map aux
|
||||||
@@ List.map get_value
|
@@ List.map get_value
|
||||||
@@ npseq_to_list c.value.cases.value in
|
@@ npseq_to_list c.cases.value in
|
||||||
let default_action () =
|
let default_action () =
|
||||||
let%bind cases = simpl_cases lst in
|
let%bind cases = simpl_cases lst in
|
||||||
return @@ E_matching (e , cases) in
|
return @@ e_matching ~loc e cases in
|
||||||
(* Hack to take care of patterns introduced by `parser/ligodity/Parser.mly` in "norm_fun_expr" *)
|
(* Hack to take care of patterns introduced by `parser/ligodity/Parser.mly` in "norm_fun_expr" *)
|
||||||
match lst with
|
match lst with
|
||||||
| [ (pattern , rhs) ] -> (
|
| [ (pattern , rhs) ] -> (
|
||||||
@ -238,125 +289,127 @@ let rec simpl_expression :
|
|||||||
| _ -> default_action ()
|
| _ -> default_action ()
|
||||||
)
|
)
|
||||||
| EFun lamb -> simpl_fun lamb
|
| EFun lamb -> simpl_fun lamb
|
||||||
| ESeq s ->
|
| ESeq s -> (
|
||||||
let items : Raw.expr list = pseq_to_list s.value.elements in
|
let (s , loc) = r_split s in
|
||||||
|
let items : Raw.expr list = pseq_to_list s.elements in
|
||||||
(match items with
|
(match items with
|
||||||
[] -> return @@ E_skip
|
[] -> return @@ e_skip ~loc ()
|
||||||
| expr::more ->
|
| expr::more ->
|
||||||
let expr' = simpl_expression expr in
|
let expr' = simpl_expression expr in
|
||||||
let apply (e1: Raw.expr) (e2: expression Trace.result) =
|
let apply (e1: Raw.expr) (e2: expression Trace.result) =
|
||||||
let%bind a = simpl_expression e1 in
|
let%bind a = simpl_expression e1 in
|
||||||
let%bind e2' = e2 in
|
let%bind e2' = e2 in
|
||||||
return @@ E_sequence (a, e2')
|
return @@ e_sequence a e2'
|
||||||
in List.fold_right apply more expr')
|
in List.fold_right apply more expr')
|
||||||
| ECond c ->
|
)
|
||||||
let c = c.value in
|
| ECond c -> (
|
||||||
|
let (c , loc) = r_split c in
|
||||||
let%bind expr = simpl_expression c.test in
|
let%bind expr = simpl_expression c.test in
|
||||||
let%bind match_true = simpl_expression c.ifso in
|
let%bind match_true = simpl_expression c.ifso in
|
||||||
let%bind match_false = simpl_expression c.ifnot in
|
let%bind match_false = simpl_expression c.ifnot in
|
||||||
return @@ E_matching (expr, (Match_bool {match_true; match_false}))
|
return @@ e_matching ~loc expr (Match_bool {match_true; match_false})
|
||||||
|
|
||||||
and simpl_fun lamb : expr result =
|
|
||||||
let return x = ok x in
|
|
||||||
let rec aux args body =
|
|
||||||
match body with
|
|
||||||
| Raw.EFun l -> (
|
|
||||||
let l' = l.value in
|
|
||||||
let annot = Option.map snd l'.p_annot in
|
|
||||||
aux (args @ [(l'.param.value , annot)]) l'.body
|
|
||||||
)
|
)
|
||||||
| _ -> (args , body) in
|
|
||||||
let (args , body) = aux [] (Raw.EFun lamb) in
|
and simpl_fun lamb' : expr result =
|
||||||
|
let return x = ok x in
|
||||||
|
let (lamb , loc) = r_split lamb' in
|
||||||
let%bind args' =
|
let%bind args' =
|
||||||
let aux = fun (name , ty_opt) ->
|
let args = lamb.params in
|
||||||
let%bind ty =
|
let%bind p_args = bind_map_list pattern_to_typed_var args in
|
||||||
match ty_opt with
|
let aux ((var : Raw.variable) , ty_opt) =
|
||||||
| Some ty -> simpl_type_expression ty
|
match var.value , ty_opt with
|
||||||
| None when name = "storage" -> ok (T_variable "storage")
|
| "storage" , None ->
|
||||||
| None -> simple_fail "missing type annotation on input"
|
ok (var , T_variable "storage")
|
||||||
|
| _ , None ->
|
||||||
|
simple_fail "untyped function parameter"
|
||||||
|
| _ , Some ty -> (
|
||||||
|
let%bind ty' = simpl_type_expression ty in
|
||||||
|
ok (var , ty')
|
||||||
|
)
|
||||||
in
|
in
|
||||||
ok (name , ty)
|
bind_map_list aux p_args
|
||||||
in
|
|
||||||
bind_map_list aux args
|
|
||||||
in
|
in
|
||||||
let arguments_name = "arguments" in
|
let arguments_name = "arguments" in
|
||||||
let (binder , input_type) =
|
let (binder , input_type) =
|
||||||
let type_expression = T_tuple (List.map snd args') in
|
let type_expression = T_tuple (List.map snd args') in
|
||||||
(arguments_name , type_expression) in
|
(arguments_name , type_expression) in
|
||||||
let body, body_type =
|
let%bind (body , body_type) = expr_to_typed_expr lamb.body in
|
||||||
match body with
|
|
||||||
| EAnnot {value = expr, type_expr} -> expr, Some type_expr
|
|
||||||
| expr -> expr, None in
|
|
||||||
let%bind output_type =
|
let%bind output_type =
|
||||||
bind_map_option simpl_type_expression body_type in
|
bind_map_option simpl_type_expression body_type in
|
||||||
let%bind result = simpl_expression body in
|
let%bind result = simpl_expression body in
|
||||||
let wrapped_result =
|
let wrapped_result =
|
||||||
let aux = fun i (name , ty) wrapped ->
|
let aux = fun i ((name : Raw.variable) , ty) wrapped ->
|
||||||
let accessor = E_accessor (E_variable arguments_name , [ Access_tuple i ]) in
|
let accessor = e_accessor (e_variable arguments_name) [ Access_tuple i ] in
|
||||||
e_let_in (name , Some ty) accessor wrapped
|
e_let_in (name.value , Some ty) accessor wrapped
|
||||||
in
|
in
|
||||||
let wraps = List.mapi aux args' in
|
let wraps = List.mapi aux args' in
|
||||||
List.fold_right' (fun x f -> f x) result wraps in
|
List.fold_right' (fun x f -> f x) result wraps in
|
||||||
let lambda = {binder = (binder , Some input_type); input_type = (Some input_type); output_type; result = wrapped_result}
|
return @@ e_lambda ~loc binder (Some input_type) output_type wrapped_result
|
||||||
in return @@ E_lambda lambda
|
|
||||||
|
|
||||||
|
|
||||||
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
|
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok @@ make_option_typed x te_annot in
|
||||||
match t with
|
match t with
|
||||||
| BoolExpr (False _) ->
|
| BoolExpr (False reg) -> (
|
||||||
return @@ E_literal (Literal_bool false)
|
let loc = Location.lift reg in
|
||||||
| BoolExpr (True _) ->
|
return @@ e_literal ~loc (Literal_bool false)
|
||||||
return @@ E_literal (Literal_bool true)
|
)
|
||||||
|
| BoolExpr (True reg) -> (
|
||||||
|
let loc = Location.lift reg in
|
||||||
|
return @@ e_literal ~loc (Literal_bool true)
|
||||||
|
)
|
||||||
| BoolExpr (Or b) ->
|
| BoolExpr (Or b) ->
|
||||||
simpl_binop ?te_annot "OR" b.value
|
simpl_binop "OR" b
|
||||||
| BoolExpr (And b) ->
|
| BoolExpr (And b) ->
|
||||||
simpl_binop ?te_annot "AND" b.value
|
simpl_binop "AND" b
|
||||||
| BoolExpr (Not b) ->
|
| BoolExpr (Not b) ->
|
||||||
simpl_unop ?te_annot "NOT" b.value
|
simpl_unop "NOT" b
|
||||||
| CompExpr (Lt c) ->
|
| CompExpr (Lt c) ->
|
||||||
simpl_binop ?te_annot "LT" c.value
|
simpl_binop "LT" c
|
||||||
| CompExpr (Gt c) ->
|
| CompExpr (Gt c) ->
|
||||||
simpl_binop ?te_annot "GT" c.value
|
simpl_binop "GT" c
|
||||||
| CompExpr (Leq c) ->
|
| CompExpr (Leq c) ->
|
||||||
simpl_binop ?te_annot "LE" c.value
|
simpl_binop "LE" c
|
||||||
| CompExpr (Geq c) ->
|
| CompExpr (Geq c) ->
|
||||||
simpl_binop ?te_annot "GE" c.value
|
simpl_binop "GE" c
|
||||||
| CompExpr (Equal c) ->
|
| CompExpr (Equal c) ->
|
||||||
simpl_binop ?te_annot "EQ" c.value
|
simpl_binop "EQ" c
|
||||||
| CompExpr (Neq c) ->
|
| CompExpr (Neq c) ->
|
||||||
simpl_binop ?te_annot "NEQ" c.value
|
simpl_binop "NEQ" c
|
||||||
|
|
||||||
and simpl_list_expression ?te_annot (t:Raw.list_expr) : expression result =
|
and simpl_list_expression (t:Raw.list_expr) : expression result =
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok @@ x in
|
||||||
match t with
|
match t with
|
||||||
| Cons c ->
|
| Cons c -> simpl_binop "CONS" c
|
||||||
simpl_binop ?te_annot "CONS" c.value
|
| List lst -> (
|
||||||
| List lst ->
|
let (lst , loc) = r_split lst in
|
||||||
let%bind lst' =
|
let%bind lst' =
|
||||||
bind_map_list simpl_expression @@
|
bind_map_list simpl_expression @@
|
||||||
pseq_to_list lst.value.elements in
|
pseq_to_list lst.elements in
|
||||||
return @@ E_list lst'
|
return @@ e_list ~loc lst'
|
||||||
|
)
|
||||||
|
|
||||||
and simpl_binop ?te_annot (name:string) (t:_ Raw.bin_op) : expression result =
|
and simpl_binop (name:string) (t:_ Raw.bin_op Region.reg) : expression result =
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok @@ x in
|
||||||
let%bind a = simpl_expression t.arg1 in
|
let (args , loc) = r_split t in
|
||||||
let%bind b = simpl_expression t.arg2 in
|
let%bind a = simpl_expression args.arg1 in
|
||||||
return @@ E_constant (name, [a;b])
|
let%bind b = simpl_expression args.arg2 in
|
||||||
|
return @@ e_constant ~loc name [ a ; b ]
|
||||||
|
|
||||||
and simpl_unop ?te_annot (name:string) (t:_ Raw.un_op) : expression result =
|
and simpl_unop (name:string) (t:_ Raw.un_op Region.reg) : expression result =
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok @@ x in
|
||||||
|
let (t , loc) = r_split t in
|
||||||
let%bind a = simpl_expression t.arg in
|
let%bind a = simpl_expression t.arg in
|
||||||
return @@ E_constant (name, [a])
|
return @@ e_constant ~loc name [ a ]
|
||||||
|
|
||||||
and simpl_tuple_expression ?te_annot (lst:Raw.expr list) : expression result =
|
and simpl_tuple_expression ?loc (lst:Raw.expr list) : expression result =
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok @@ x in
|
||||||
match lst with
|
match lst with
|
||||||
| [] -> return @@ E_literal Literal_unit
|
| [] -> return @@ e_literal ?loc Literal_unit
|
||||||
| [hd] -> simpl_expression ?te_annot hd
|
| [hd] -> simpl_expression hd
|
||||||
| lst ->
|
| lst ->
|
||||||
let%bind lst = bind_list @@ List.map simpl_expression lst in
|
let%bind lst = bind_list @@ List.map simpl_expression lst in
|
||||||
return @@ E_tuple lst
|
return @@ e_tuple ?loc lst
|
||||||
|
|
||||||
and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
|
and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
|
||||||
let open! Raw in
|
let open! Raw in
|
||||||
@ -369,13 +422,34 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
|
|||||||
| LetEntry x (* -> simple_fail "no entry point yet" *)
|
| LetEntry x (* -> simple_fail "no entry point yet" *)
|
||||||
| Let x -> (
|
| Let x -> (
|
||||||
let _ , binding = x.value in
|
let _ , binding = x.value in
|
||||||
let {variable ; lhs_type ; let_rhs} = binding in
|
let {bindings ; lhs_type ; let_rhs} = binding in
|
||||||
let%bind type_annotation = bind_map_option
|
let%bind (var , args) =
|
||||||
(fun (_,type_expr) -> simpl_type_expression type_expr)
|
let%bind (hd , tl) = match bindings with
|
||||||
lhs_type in
|
| [] -> simple_fail "let without bindgings"
|
||||||
let%bind rhs = simpl_expression ?te_annot:type_annotation let_rhs in
|
| hd :: tl -> ok (hd , tl)
|
||||||
let name = variable.value in
|
in
|
||||||
ok @@ loc x @@ (Declaration_constant (name , type_annotation , rhs))
|
let%bind var = pattern_to_var hd in
|
||||||
|
ok (var , tl)
|
||||||
|
in
|
||||||
|
match args with
|
||||||
|
| [] -> (
|
||||||
|
let%bind lhs_type' = bind_map_option
|
||||||
|
(fun (_ , te) -> simpl_type_expression te) lhs_type in
|
||||||
|
let%bind rhs' = simpl_expression let_rhs in
|
||||||
|
ok @@ loc x @@ (Declaration_constant (var.value , lhs_type' , rhs'))
|
||||||
|
)
|
||||||
|
| _ -> (
|
||||||
|
let fun_ = {
|
||||||
|
kwd_fun = Region.ghost ;
|
||||||
|
params = args ;
|
||||||
|
p_annot = lhs_type ;
|
||||||
|
arrow = Region.ghost ;
|
||||||
|
body = let_rhs ;
|
||||||
|
} in
|
||||||
|
let rhs = Raw.EFun {region=Region.ghost ; value=fun_} in
|
||||||
|
let%bind rhs' = simpl_expression rhs in
|
||||||
|
ok @@ loc x @@ (Declaration_constant (var.value , None , rhs'))
|
||||||
|
)
|
||||||
)
|
)
|
||||||
|
|
||||||
and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
|
and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->
|
||||||
|
@ -16,16 +16,18 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value
|
|||||||
|
|
||||||
open Operators.Simplify.Pascaligo
|
open Operators.Simplify.Pascaligo
|
||||||
|
|
||||||
|
let r_split = Location.r_split
|
||||||
|
|
||||||
let return expr = ok @@ fun expr'_opt ->
|
let return expr = ok @@ fun expr'_opt ->
|
||||||
let expr = expr in
|
let expr = expr in
|
||||||
match expr'_opt with
|
match expr'_opt with
|
||||||
| None -> ok @@ expr
|
| None -> ok @@ expr
|
||||||
| Some expr' -> ok @@ e_sequence expr expr'
|
| Some expr' -> ok @@ e_sequence expr expr'
|
||||||
|
|
||||||
let return_let_in binder rhs = ok @@ fun expr'_opt ->
|
let return_let_in ?loc binder rhs = ok @@ fun expr'_opt ->
|
||||||
match expr'_opt with
|
match expr'_opt with
|
||||||
| None -> simple_fail "missing return" (* Hard to explain. Shouldn't happen in prod. *)
|
| None -> simple_fail "missing return" (* Hard to explain. Shouldn't happen in prod. *)
|
||||||
| Some expr' -> ok @@ e_let_in binder rhs expr'
|
| Some expr' -> ok @@ e_let_in ?loc binder rhs expr'
|
||||||
|
|
||||||
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
|
let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
|
||||||
match t with
|
match t with
|
||||||
@ -88,11 +90,12 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
|
|||||||
|
|
||||||
let rec simpl_expression (t:Raw.expr) : expr result =
|
let rec simpl_expression (t:Raw.expr) : expr result =
|
||||||
let return x = ok x in
|
let return x = ok x in
|
||||||
let simpl_projection = fun (p:Raw.projection) ->
|
let simpl_projection = fun (p : Raw.projection Region.reg) ->
|
||||||
|
let (p' , loc) = r_split p in
|
||||||
let var =
|
let var =
|
||||||
let name = p.struct_name.value in
|
let name = p'.struct_name.value in
|
||||||
e_variable name in
|
e_variable name in
|
||||||
let path = p.field_path in
|
let path = p'.field_path in
|
||||||
let path' =
|
let path' =
|
||||||
let aux (s:Raw.selection) =
|
let aux (s:Raw.selection) =
|
||||||
match s with
|
match s with
|
||||||
@ -100,97 +103,112 @@ let rec simpl_expression (t:Raw.expr) : expr result =
|
|||||||
| Component index -> Access_tuple (Z.to_int (snd index.value))
|
| Component index -> Access_tuple (Z.to_int (snd index.value))
|
||||||
in
|
in
|
||||||
List.map aux @@ npseq_to_list path in
|
List.map aux @@ npseq_to_list path in
|
||||||
return @@ E_accessor (var, path')
|
return @@ e_accessor ~loc var path'
|
||||||
in
|
in
|
||||||
match t with
|
match t with
|
||||||
| EAnnot a -> (
|
| EAnnot a -> (
|
||||||
let (expr , type_expr) = a.value in
|
let ((expr , type_expr) , loc) = r_split a in
|
||||||
let%bind expr' = simpl_expression expr in
|
let%bind expr' = simpl_expression expr in
|
||||||
let%bind type_expr' = simpl_type_expression type_expr in
|
let%bind type_expr' = simpl_type_expression type_expr in
|
||||||
return @@ e_annotation expr' type_expr'
|
return @@ e_annotation ~loc expr' type_expr'
|
||||||
)
|
)
|
||||||
| EVar c -> (
|
| EVar c -> (
|
||||||
let c' = c.value in
|
let (c' , loc) = r_split c in
|
||||||
match List.assoc_opt c' constants with
|
match List.assoc_opt c' constants with
|
||||||
| None -> return @@ E_variable c.value
|
| None -> return @@ e_variable ~loc c.value
|
||||||
| Some s -> return @@ E_constant (s , [])
|
| Some s -> return @@ e_constant ~loc s []
|
||||||
)
|
)
|
||||||
| ECall x -> (
|
| ECall x -> (
|
||||||
let (name, args) = x.value in
|
let ((name, args) , loc) = r_split x in
|
||||||
let f = name.value in
|
let (f , f_loc) = r_split name in
|
||||||
let args' = npseq_to_list args.value.inside in
|
let (args , args_loc) = r_split args in
|
||||||
|
let args' = npseq_to_list args.inside in
|
||||||
match List.assoc_opt f constants with
|
match List.assoc_opt f constants with
|
||||||
| None ->
|
| None ->
|
||||||
let%bind arg = simpl_tuple_expression args' in
|
let%bind arg = simpl_tuple_expression ~loc:args_loc args' in
|
||||||
return @@ E_application (e_variable f, arg)
|
return @@ e_application ~loc (e_variable ~loc:f_loc f) arg
|
||||||
| Some s ->
|
| Some s ->
|
||||||
let%bind lst = bind_map_list simpl_expression args' in
|
let%bind lst = bind_map_list simpl_expression args' in
|
||||||
return @@ E_constant (s , lst)
|
return @@ e_constant ~loc s lst
|
||||||
)
|
)
|
||||||
| EPar x -> simpl_expression x.value.inside
|
| EPar x -> simpl_expression x.value.inside
|
||||||
| EUnit _ -> return @@ E_literal Literal_unit
|
| EUnit reg ->
|
||||||
| EBytes x -> return @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value))
|
let loc = Location.lift reg in
|
||||||
|
return @@ e_literal ~loc Literal_unit
|
||||||
|
| EBytes x ->
|
||||||
|
let (x' , loc) = r_split x in
|
||||||
|
return @@ e_literal ~loc (Literal_bytes (Bytes.of_string @@ fst x'))
|
||||||
| ETuple tpl ->
|
| ETuple tpl ->
|
||||||
let (Raw.TupleInj tpl') = tpl in
|
let (Raw.TupleInj tpl') = tpl in
|
||||||
simpl_tuple_expression
|
let (tpl' , loc) = r_split tpl' in
|
||||||
@@ npseq_to_list tpl'.value.inside
|
simpl_tuple_expression ~loc @@ npseq_to_list tpl'.inside
|
||||||
| ERecord r ->
|
| ERecord r ->
|
||||||
let%bind fields = bind_list
|
let%bind fields = bind_list
|
||||||
@@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
|
@@ List.map (fun ((k : _ Raw.reg), v) -> let%bind v = simpl_expression v in ok (k.value, v))
|
||||||
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
|
@@ List.map (fun (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr))
|
||||||
@@ pseq_to_list r.value.elements in
|
@@ pseq_to_list r.value.elements in
|
||||||
let aux prev (k, v) = SMap.add k v prev in
|
let aux prev (k, v) = SMap.add k v prev in
|
||||||
return @@ E_record (List.fold_left aux SMap.empty fields)
|
return @@ e_record (List.fold_left aux SMap.empty fields)
|
||||||
| EProj p' -> (
|
| EProj p -> simpl_projection p
|
||||||
let p = p'.value in
|
| EConstr (ConstrApp c) -> (
|
||||||
simpl_projection p
|
let ((c, args) , loc) = r_split c in
|
||||||
|
let (args , args_loc) = r_split args in
|
||||||
|
let%bind arg =
|
||||||
|
simpl_tuple_expression ~loc:args_loc
|
||||||
|
@@ npseq_to_list args.inside in
|
||||||
|
return @@ e_constructor ~loc c.value arg
|
||||||
)
|
)
|
||||||
| EConstr (ConstrApp c) ->
|
|
||||||
let (c, args) = c.value in
|
|
||||||
let%bind arg =
|
|
||||||
simpl_tuple_expression
|
|
||||||
@@ npseq_to_list args.value.inside in
|
|
||||||
return @@ E_constructor (c.value, arg)
|
|
||||||
| EConstr (SomeApp a) ->
|
| EConstr (SomeApp a) ->
|
||||||
let (_, args) = a.value in
|
let ((_, args) , loc) = r_split a in
|
||||||
|
let (args , args_loc) = r_split args in
|
||||||
let%bind arg =
|
let%bind arg =
|
||||||
simpl_tuple_expression
|
simpl_tuple_expression ~loc:args_loc
|
||||||
@@ npseq_to_list args.value.inside in
|
@@ npseq_to_list args.inside in
|
||||||
return @@ E_constant ("SOME", [arg])
|
return @@ e_constant ~loc "SOME" [arg]
|
||||||
| EConstr (NoneExpr _) ->
|
| EConstr (NoneExpr reg) -> (
|
||||||
return @@ E_constant ("NONE" , [])
|
let loc = Location.lift reg in
|
||||||
|
return @@ e_none ~loc ()
|
||||||
|
)
|
||||||
| EArith (Add c) ->
|
| EArith (Add c) ->
|
||||||
simpl_binop "ADD" c.value
|
simpl_binop "ADD" c
|
||||||
| EArith (Sub c) ->
|
| EArith (Sub c) ->
|
||||||
simpl_binop "SUB" c.value
|
simpl_binop "SUB" c
|
||||||
| EArith (Mult c) ->
|
| EArith (Mult c) ->
|
||||||
simpl_binop "TIMES" c.value
|
simpl_binop "TIMES" c
|
||||||
| EArith (Div c) ->
|
| EArith (Div c) ->
|
||||||
simpl_binop "DIV" c.value
|
simpl_binop "DIV" c
|
||||||
| EArith (Mod c) ->
|
| EArith (Mod c) ->
|
||||||
simpl_binop "MOD" c.value
|
simpl_binop "MOD" c
|
||||||
| EArith (Int n) ->
|
| EArith (Int n) -> (
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
let (n , loc) = r_split n in
|
||||||
return @@ E_literal (Literal_int n)
|
let n = Z.to_int @@ snd n in
|
||||||
| EArith (Nat n) ->
|
return @@ e_literal ~loc (Literal_int n)
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
)
|
||||||
return @@ E_literal (Literal_nat n)
|
| EArith (Nat n) -> (
|
||||||
| EArith (Mtz n) ->
|
let (n , loc) = r_split n in
|
||||||
let n = Z.to_int @@ snd @@ n.value in
|
let n = Z.to_int @@ snd @@ n in
|
||||||
return @@ E_literal (Literal_tez n)
|
return @@ e_literal ~loc (Literal_nat n)
|
||||||
|
)
|
||||||
|
| EArith (Mtz n) -> (
|
||||||
|
let (n , loc) = r_split n in
|
||||||
|
let n = Z.to_int @@ snd @@ n in
|
||||||
|
return @@ e_literal ~loc (Literal_tez n)
|
||||||
|
)
|
||||||
| EArith _ -> simple_fail "arith: not supported yet"
|
| EArith _ -> simple_fail "arith: not supported yet"
|
||||||
| EString (String s) ->
|
| EString (String s) ->
|
||||||
|
let (s , loc) = r_split s in
|
||||||
let s' =
|
let s' =
|
||||||
let s = s.value in
|
(* S contains quotes *)
|
||||||
String.(sub s 1 ((length s) - 2))
|
String.(sub s 1 ((length s) - 2))
|
||||||
in
|
in
|
||||||
return @@ E_literal (Literal_string s')
|
return @@ e_literal ~loc (Literal_string s')
|
||||||
| EString _ -> simple_fail "string: not supported yet"
|
| EString _ -> simple_fail "string: not supported yet"
|
||||||
| ELogic l -> simpl_logic_expression l
|
| ELogic l -> simpl_logic_expression l
|
||||||
| EList l -> simpl_list_expression l
|
| EList l -> simpl_list_expression l
|
||||||
| ESet _ -> simple_fail "set: not supported yet"
|
| ESet _ -> simple_fail "set: not supported yet"
|
||||||
| ECase c ->
|
| ECase c -> (
|
||||||
let%bind e = simpl_expression c.value.expr in
|
let (c , loc) = r_split c in
|
||||||
|
let%bind e = simpl_expression c.expr in
|
||||||
let%bind lst =
|
let%bind lst =
|
||||||
let aux (x : Raw.expr Raw.case_clause) =
|
let aux (x : Raw.expr Raw.case_clause) =
|
||||||
let%bind expr = simpl_expression x.rhs in
|
let%bind expr = simpl_expression x.rhs in
|
||||||
@ -198,84 +216,103 @@ let rec simpl_expression (t:Raw.expr) : expr result =
|
|||||||
bind_list
|
bind_list
|
||||||
@@ List.map aux
|
@@ List.map aux
|
||||||
@@ List.map get_value
|
@@ List.map get_value
|
||||||
@@ npseq_to_list c.value.cases.value in
|
@@ npseq_to_list c.cases.value in
|
||||||
let%bind cases = simpl_cases lst in
|
let%bind cases = simpl_cases lst in
|
||||||
return @@ E_matching (e, cases)
|
return @@ e_matching ~loc e cases
|
||||||
| EMap (MapInj mi) ->
|
)
|
||||||
|
| EMap (MapInj mi) -> (
|
||||||
|
let (mi , loc) = r_split mi in
|
||||||
let%bind lst =
|
let%bind lst =
|
||||||
let lst = List.map get_value @@ pseq_to_list mi.value.elements in
|
let lst = List.map get_value @@ pseq_to_list mi.elements in
|
||||||
let aux : Raw.binding -> (expression * expression) result = fun b ->
|
let aux : Raw.binding -> (expression * expression) result = fun b ->
|
||||||
let%bind src = simpl_expression b.source in
|
let%bind src = simpl_expression b.source in
|
||||||
let%bind dst = simpl_expression b.image in
|
let%bind dst = simpl_expression b.image in
|
||||||
ok (src, dst) in
|
ok (src, dst) in
|
||||||
bind_map_list aux lst in
|
bind_map_list aux lst in
|
||||||
return (E_map lst)
|
return @@ e_map ~loc lst
|
||||||
| EMap (MapLookUp lu) ->
|
)
|
||||||
let%bind path = match lu.value.path with
|
| EMap (MapLookUp lu) -> (
|
||||||
| Name v -> return (E_variable v.value)
|
let (lu , loc) = r_split lu in
|
||||||
| Path p -> simpl_projection p.value
|
let%bind path = match lu.path with
|
||||||
|
| Name v -> (
|
||||||
|
let (v , loc) = r_split v in
|
||||||
|
return @@ e_variable ~loc v
|
||||||
|
)
|
||||||
|
| Path p -> simpl_projection p
|
||||||
in
|
in
|
||||||
let%bind index = simpl_expression lu.value.index.value.inside in
|
let%bind index = simpl_expression lu.index.value.inside in
|
||||||
return (E_look_up (path, index))
|
return @@ e_look_up ~loc path index
|
||||||
|
)
|
||||||
|
|
||||||
and simpl_logic_expression (t:Raw.logic_expr) : expression result =
|
and simpl_logic_expression (t:Raw.logic_expr) : expression result =
|
||||||
let return x = ok x in
|
let return x = ok x in
|
||||||
match t with
|
match t with
|
||||||
| BoolExpr (False _) ->
|
| BoolExpr (False reg) -> (
|
||||||
return @@ E_literal (Literal_bool false)
|
let loc = Location.lift reg in
|
||||||
| BoolExpr (True _) ->
|
return @@ e_literal ~loc (Literal_bool false)
|
||||||
return @@ E_literal (Literal_bool true)
|
)
|
||||||
|
| BoolExpr (True reg) -> (
|
||||||
|
let loc = Location.lift reg in
|
||||||
|
return @@ e_literal ~loc (Literal_bool true)
|
||||||
|
)
|
||||||
| BoolExpr (Or b) ->
|
| BoolExpr (Or b) ->
|
||||||
simpl_binop "OR" b.value
|
simpl_binop "OR" b
|
||||||
| BoolExpr (And b) ->
|
| BoolExpr (And b) ->
|
||||||
simpl_binop "AND" b.value
|
simpl_binop "AND" b
|
||||||
| BoolExpr (Not b) ->
|
| BoolExpr (Not b) ->
|
||||||
simpl_unop "NOT" b.value
|
simpl_unop "NOT" b
|
||||||
| CompExpr (Lt c) ->
|
| CompExpr (Lt c) ->
|
||||||
simpl_binop "LT" c.value
|
simpl_binop "LT" c
|
||||||
| CompExpr (Gt c) ->
|
| CompExpr (Gt c) ->
|
||||||
simpl_binop "GT" c.value
|
simpl_binop "GT" c
|
||||||
| CompExpr (Leq c) ->
|
| CompExpr (Leq c) ->
|
||||||
simpl_binop "LE" c.value
|
simpl_binop "LE" c
|
||||||
| CompExpr (Geq c) ->
|
| CompExpr (Geq c) ->
|
||||||
simpl_binop "GE" c.value
|
simpl_binop "GE" c
|
||||||
| CompExpr (Equal c) ->
|
| CompExpr (Equal c) ->
|
||||||
simpl_binop "EQ" c.value
|
simpl_binop "EQ" c
|
||||||
| CompExpr (Neq c) ->
|
| CompExpr (Neq c) ->
|
||||||
simpl_binop "NEQ" c.value
|
simpl_binop "NEQ" c
|
||||||
|
|
||||||
and simpl_list_expression (t:Raw.list_expr) : expression result =
|
and simpl_list_expression (t:Raw.list_expr) : expression result =
|
||||||
let return x = ok x in
|
let return x = ok x in
|
||||||
match t with
|
match t with
|
||||||
| Cons c ->
|
| Cons c ->
|
||||||
simpl_binop "CONS" c.value
|
simpl_binop "CONS" c
|
||||||
| List lst ->
|
| List lst -> (
|
||||||
|
let (lst , loc) = r_split lst in
|
||||||
let%bind lst' =
|
let%bind lst' =
|
||||||
bind_map_list simpl_expression @@
|
bind_map_list simpl_expression @@
|
||||||
pseq_to_list lst.value.elements in
|
pseq_to_list lst.elements in
|
||||||
return @@ E_list lst'
|
return @@ e_list ~loc lst'
|
||||||
| Nil _ ->
|
)
|
||||||
return @@ E_list []
|
| Nil reg -> (
|
||||||
|
let loc = Location.lift reg in
|
||||||
|
return @@ e_list ~loc []
|
||||||
|
)
|
||||||
|
|
||||||
and simpl_binop (name:string) (t:_ Raw.bin_op) : expression result =
|
and simpl_binop (name:string) (t:_ Raw.bin_op Region.reg) : expression result =
|
||||||
let return x = ok x in
|
let return x = ok x in
|
||||||
|
let (t , loc) = r_split t in
|
||||||
let%bind a = simpl_expression t.arg1 in
|
let%bind a = simpl_expression t.arg1 in
|
||||||
let%bind b = simpl_expression t.arg2 in
|
let%bind b = simpl_expression t.arg2 in
|
||||||
return @@ E_constant (name, [a;b])
|
return @@ e_constant ~loc name [ a ; b ]
|
||||||
|
|
||||||
and simpl_unop (name:string) (t:_ Raw.un_op) : expression result =
|
and simpl_unop (name:string) (t:_ Raw.un_op Region.reg) : expression result =
|
||||||
let return x = ok x in
|
let return x = ok x in
|
||||||
|
let (t , loc) = r_split t in
|
||||||
let%bind a = simpl_expression t.arg in
|
let%bind a = simpl_expression t.arg in
|
||||||
return @@ E_constant (name, [a])
|
return @@ e_constant ~loc name [ a ]
|
||||||
|
|
||||||
and simpl_tuple_expression (lst:Raw.expr list) : expression result =
|
and simpl_tuple_expression ?loc (lst:Raw.expr list) : expression result =
|
||||||
let return x = ok x in
|
let return x = ok x in
|
||||||
match lst with
|
match lst with
|
||||||
| [] -> return @@ E_literal Literal_unit
|
| [] -> return @@ e_literal Literal_unit
|
||||||
| [hd] -> simpl_expression hd
|
| [hd] -> simpl_expression hd
|
||||||
| lst ->
|
| lst -> (
|
||||||
let%bind lst = bind_list @@ List.map simpl_expression lst in
|
let%bind lst = bind_list @@ List.map simpl_expression lst in
|
||||||
return @@ E_tuple lst
|
return @@ e_tuple ?loc lst
|
||||||
|
)
|
||||||
|
|
||||||
and simpl_local_declaration : Raw.local_decl -> _ result = fun t ->
|
and simpl_local_declaration : Raw.local_decl -> _ result = fun t ->
|
||||||
match t with
|
match t with
|
||||||
@ -284,26 +321,28 @@ and simpl_local_declaration : Raw.local_decl -> _ result = fun t ->
|
|||||||
|
|
||||||
and simpl_lambda_declaration : Raw.lambda_decl -> _ result = fun l ->
|
and simpl_lambda_declaration : Raw.lambda_decl -> _ result = fun l ->
|
||||||
match l with
|
match l with
|
||||||
| FunDecl f ->
|
| FunDecl f -> (
|
||||||
let%bind (name , e) = simpl_fun_declaration (f.value) in
|
let (f , loc) = r_split f in
|
||||||
return_let_in name e
|
let%bind (name , e) = simpl_fun_declaration ~loc f in
|
||||||
|
return_let_in ~loc name e
|
||||||
|
)
|
||||||
| ProcDecl _ -> simple_fail "no local procedure yet"
|
| ProcDecl _ -> simple_fail "no local procedure yet"
|
||||||
| EntryDecl _ -> simple_fail "no local entry-point yet"
|
| EntryDecl _ -> simple_fail "no local entry-point yet"
|
||||||
|
|
||||||
and simpl_data_declaration : Raw.data_decl -> _ result = fun t ->
|
and simpl_data_declaration : Raw.data_decl -> _ result = fun t ->
|
||||||
match t with
|
match t with
|
||||||
| LocalVar x ->
|
| LocalVar x ->
|
||||||
let x = x.value in
|
let (x , loc) = r_split x in
|
||||||
let name = x.name.value in
|
let name = x.name.value in
|
||||||
let%bind t = simpl_type_expression x.var_type in
|
let%bind t = simpl_type_expression x.var_type in
|
||||||
let%bind expression = simpl_expression x.init in
|
let%bind expression = simpl_expression x.init in
|
||||||
return_let_in (name , Some t) expression
|
return_let_in ~loc (name , Some t) expression
|
||||||
| LocalConst x ->
|
| LocalConst x ->
|
||||||
let x = x.value in
|
let (x , loc) = r_split x in
|
||||||
let name = x.name.value in
|
let name = x.name.value in
|
||||||
let%bind t = simpl_type_expression x.const_type in
|
let%bind t = simpl_type_expression x.const_type in
|
||||||
let%bind expression = simpl_expression x.init in
|
let%bind expression = simpl_expression x.init in
|
||||||
return_let_in (name , Some t) expression
|
return_let_in ~loc (name , Some t) expression
|
||||||
|
|
||||||
and simpl_param : Raw.param_decl -> (type_name * type_expression) result = fun t ->
|
and simpl_param : Raw.param_decl -> (type_name * type_expression) result = fun t ->
|
||||||
match t with
|
match t with
|
||||||
@ -318,7 +357,7 @@ and simpl_param : Raw.param_decl -> (type_name * type_expression) result = fun t
|
|||||||
let%bind type_expression = simpl_type_expression c.param_type in
|
let%bind type_expression = simpl_type_expression c.param_type in
|
||||||
ok (type_name , type_expression)
|
ok (type_name , type_expression)
|
||||||
|
|
||||||
and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * expression) result = fun x ->
|
and simpl_fun_declaration : loc:_ -> Raw.fun_decl -> ((name * type_expression option) * expression) result = fun ~loc x ->
|
||||||
let open! Raw in
|
let open! Raw in
|
||||||
let {name;param;ret_type;local_decls;block;return} : fun_decl = x in
|
let {name;param;ret_type;local_decls;block;return} : fun_decl = x in
|
||||||
(match npseq_to_list param.value.inside with
|
(match npseq_to_list param.value.inside with
|
||||||
@ -338,12 +377,8 @@ and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * e
|
|||||||
let%bind result =
|
let%bind result =
|
||||||
let aux prec cur = cur (Some prec) in
|
let aux prec cur = cur (Some prec) in
|
||||||
bind_fold_right_list aux result body in
|
bind_fold_right_list aux result body in
|
||||||
let expression = E_lambda {
|
let expression : expression = e_lambda ~loc binder (Some input_type)
|
||||||
binder = (binder , Some input_type) ;
|
(Some output_type) result in
|
||||||
input_type = Some input_type ;
|
|
||||||
output_type = Some output_type ;
|
|
||||||
result
|
|
||||||
} in
|
|
||||||
let type_annotation = Some (T_function (input_type, output_type)) in
|
let type_annotation = Some (T_function (input_type, output_type)) in
|
||||||
ok ((name , type_annotation) , expression)
|
ok ((name , type_annotation) , expression)
|
||||||
)
|
)
|
||||||
@ -355,7 +390,7 @@ and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * e
|
|||||||
(arguments_name , type_expression) in
|
(arguments_name , type_expression) in
|
||||||
let%bind tpl_declarations =
|
let%bind tpl_declarations =
|
||||||
let aux = fun i x ->
|
let aux = fun i x ->
|
||||||
let expr = E_accessor (E_variable arguments_name , [ Access_tuple i ]) in
|
let expr = e_accessor (e_variable arguments_name) [ Access_tuple i ] in
|
||||||
let type_ = Some (snd x) in
|
let type_ = Some (snd x) in
|
||||||
let ass = return_let_in (fst x , type_) expr in
|
let ass = return_let_in (fst x , type_) expr in
|
||||||
ass
|
ass
|
||||||
@ -372,24 +407,20 @@ and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * e
|
|||||||
let%bind result =
|
let%bind result =
|
||||||
let aux prec cur = cur (Some prec) in
|
let aux prec cur = cur (Some prec) in
|
||||||
bind_fold_right_list aux result body in
|
bind_fold_right_list aux result body in
|
||||||
let expression = E_lambda {
|
let expression = e_lambda ~loc binder (Some input_type) (Some output_type) result in
|
||||||
binder = (binder , Some input_type) ;
|
|
||||||
input_type = Some input_type ;
|
|
||||||
output_type = Some output_type ;
|
|
||||||
result
|
|
||||||
} in
|
|
||||||
let type_annotation = Some (T_function (input_type, output_type)) in
|
let type_annotation = Some (T_function (input_type, output_type)) in
|
||||||
ok ((name.value , type_annotation) , expression)
|
ok ((name.value , type_annotation) , expression)
|
||||||
)
|
)
|
||||||
)
|
)
|
||||||
and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
|
and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fun t ->
|
||||||
let open! Raw in
|
let open! Raw in
|
||||||
let loc : 'a . 'a Raw.reg -> _ -> _ = fun x v -> Location.wrap ~loc:(File x.region) v in
|
|
||||||
match t with
|
match t with
|
||||||
| TypeDecl x ->
|
| TypeDecl x -> (
|
||||||
let {name;type_expr} : Raw.type_decl = x.value in
|
let (x , loc) = r_split x in
|
||||||
|
let {name;type_expr} : Raw.type_decl = x in
|
||||||
let%bind type_expression = simpl_type_expression type_expr in
|
let%bind type_expression = simpl_type_expression type_expr in
|
||||||
ok @@ loc x @@ Declaration_type (name.value , type_expression)
|
ok @@ Location.wrap ~loc (Declaration_type (name.value , type_expression))
|
||||||
|
)
|
||||||
| ConstDecl x ->
|
| ConstDecl x ->
|
||||||
let simpl_const_decl = fun {name;const_type;init} ->
|
let simpl_const_decl = fun {name;const_type;init} ->
|
||||||
let%bind expression = simpl_expression init in
|
let%bind expression = simpl_expression init in
|
||||||
@ -398,11 +429,11 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu
|
|||||||
ok @@ Declaration_constant (name.value , type_annotation , expression)
|
ok @@ Declaration_constant (name.value , type_annotation , expression)
|
||||||
in
|
in
|
||||||
bind_map_location simpl_const_decl (Location.lift_region x)
|
bind_map_location simpl_const_decl (Location.lift_region x)
|
||||||
| LambdaDecl (FunDecl x) ->
|
| LambdaDecl (FunDecl x) -> (
|
||||||
let aux f x =
|
let (x , loc) = r_split x in
|
||||||
let%bind ((name , ty_opt) , expr) = f x in
|
let%bind ((name , ty_opt) , expr) = simpl_fun_declaration ~loc x in
|
||||||
ok @@ Declaration_constant (name , ty_opt , expr) in
|
ok @@ Location.wrap ~loc (Declaration_constant (name , ty_opt , expr))
|
||||||
bind_map_location (aux simpl_fun_declaration) (Location.lift_region x)
|
)
|
||||||
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
|
| LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet"
|
||||||
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
|
| LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet"
|
||||||
|
|
||||||
@ -418,7 +449,10 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
let%bind expr = simpl_expression e.value.fail_expr in
|
let%bind expr = simpl_expression e.value.fail_expr in
|
||||||
return @@ e_failwith expr
|
return @@ e_failwith expr
|
||||||
)
|
)
|
||||||
| Skip _ -> return @@ e_skip
|
| Skip reg -> (
|
||||||
|
let loc = Location.lift reg in
|
||||||
|
return @@ e_skip ~loc ()
|
||||||
|
)
|
||||||
| Loop (While l) ->
|
| Loop (While l) ->
|
||||||
let l = l.value in
|
let l = l.value in
|
||||||
let%bind cond = simpl_expression l.cond in
|
let%bind cond = simpl_expression l.cond in
|
||||||
@ -427,8 +461,8 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
return @@ e_loop cond body
|
return @@ e_loop cond body
|
||||||
| Loop (For _) ->
|
| Loop (For _) ->
|
||||||
simple_fail "no for yet"
|
simple_fail "no for yet"
|
||||||
| Cond c ->
|
| Cond c -> (
|
||||||
let c = c.value in
|
let (c , loc) = r_split c in
|
||||||
let%bind expr = simpl_expression c.test in
|
let%bind expr = simpl_expression c.test in
|
||||||
let%bind match_true = match c.ifso with
|
let%bind match_true = match c.ifso with
|
||||||
| ClauseInstr i -> simpl_instruction_block i
|
| ClauseInstr i -> simpl_instruction_block i
|
||||||
@ -438,9 +472,10 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
|
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in
|
||||||
let%bind match_true = match_true None in
|
let%bind match_true = match_true None in
|
||||||
let%bind match_false = match_false None in
|
let%bind match_false = match_false None in
|
||||||
return @@ E_matching (expr, (Match_bool {match_true; match_false}))
|
return @@ e_matching expr ~loc (Match_bool {match_true; match_false})
|
||||||
|
)
|
||||||
| Assign a -> (
|
| Assign a -> (
|
||||||
let a = a.value in
|
let (a , loc) = r_split a in
|
||||||
let%bind value_expr = match a.rhs with
|
let%bind value_expr = match a.rhs with
|
||||||
| Expr e -> simpl_expression e
|
| Expr e -> simpl_expression e
|
||||||
| NoneExpr _ -> simple_fail "no none assignments yet"
|
| NoneExpr _ -> simple_fail "no none assignments yet"
|
||||||
@ -448,7 +483,7 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
match a.lhs with
|
match a.lhs with
|
||||||
| Path path -> (
|
| Path path -> (
|
||||||
let (name , path') = simpl_path path in
|
let (name , path') = simpl_path path in
|
||||||
return @@ E_assign (name , path' , value_expr)
|
return @@ e_assign ~loc name path' value_expr
|
||||||
)
|
)
|
||||||
| MapPath v -> (
|
| MapPath v -> (
|
||||||
let v' = v.value in
|
let v' = v.value in
|
||||||
@ -458,11 +493,11 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
let%bind key_expr = simpl_expression v'.index.value.inside in
|
let%bind key_expr = simpl_expression v'.index.value.inside in
|
||||||
let old_expr = e_variable name.value in
|
let old_expr = e_variable name.value in
|
||||||
let expr' = e_map_update key_expr value_expr old_expr in
|
let expr' = e_map_update key_expr value_expr old_expr in
|
||||||
return @@ E_assign (name.value , [] , expr')
|
return @@ e_assign ~loc name.value [] expr'
|
||||||
)
|
)
|
||||||
)
|
)
|
||||||
| CaseInstr c -> (
|
| CaseInstr c -> (
|
||||||
let c = c.value in
|
let (c , loc) = r_split c in
|
||||||
let%bind expr = simpl_expression c.expr in
|
let%bind expr = simpl_expression c.expr in
|
||||||
let%bind cases =
|
let%bind cases =
|
||||||
let aux (x : Raw.instruction Raw.case_clause Raw.reg) =
|
let aux (x : Raw.instruction Raw.case_clause Raw.reg) =
|
||||||
@ -473,25 +508,25 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
@@ List.map aux
|
@@ List.map aux
|
||||||
@@ npseq_to_list c.cases.value in
|
@@ npseq_to_list c.cases.value in
|
||||||
let%bind m = simpl_cases cases in
|
let%bind m = simpl_cases cases in
|
||||||
return @@ E_matching (expr, m)
|
return @@ e_matching ~loc expr m
|
||||||
)
|
)
|
||||||
| RecordPatch r -> (
|
| RecordPatch r -> (
|
||||||
let r = r.value in
|
let r = r.value in
|
||||||
let (name , access_path) = simpl_path r.path in
|
let (name , access_path) = simpl_path r.path in
|
||||||
let%bind inj = bind_list
|
let%bind inj = bind_list
|
||||||
@@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
|
@@ List.map (fun (x:Raw.field_assign Region.reg) ->
|
||||||
@@ List.map (fun (x:_ Raw.reg) -> x.value)
|
let (x , loc) = r_split x in
|
||||||
|
let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e , loc)
|
||||||
|
)
|
||||||
@@ pseq_to_list r.record_inj.value.elements in
|
@@ pseq_to_list r.record_inj.value.elements in
|
||||||
let%bind expr =
|
let%bind expr =
|
||||||
let aux = fun (access , v) ->
|
let aux = fun (access , v , loc) ->
|
||||||
E_assign (name , access_path @ [ Access_record access ] , v) in
|
e_assign ~loc name (access_path @ [ Access_record access ]) v in
|
||||||
let assigns = List.map aux inj in
|
let assigns = List.map aux inj in
|
||||||
match assigns with
|
match assigns with
|
||||||
| [] -> simple_fail "empty record patch"
|
| [] -> simple_fail "empty record patch"
|
||||||
| hd :: tl -> (
|
| hd :: tl -> (
|
||||||
let aux acc cur =
|
let aux acc cur = e_sequence (acc) (cur) in
|
||||||
e_sequence (acc) (cur)
|
|
||||||
in
|
|
||||||
ok @@ List.fold_left aux hd tl
|
ok @@ List.fold_left aux hd tl
|
||||||
)
|
)
|
||||||
in
|
in
|
||||||
@ -499,15 +534,16 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu
|
|||||||
)
|
)
|
||||||
| MapPatch _ -> simple_fail "no map patch yet"
|
| MapPatch _ -> simple_fail "no map patch yet"
|
||||||
| SetPatch _ -> simple_fail "no set patch yet"
|
| SetPatch _ -> simple_fail "no set patch yet"
|
||||||
| MapRemove r ->
|
| MapRemove r -> (
|
||||||
let v = r.value in
|
let (v , loc) = r_split r in
|
||||||
let key = v.key in
|
let key = v.key in
|
||||||
let%bind map = match v.map with
|
let%bind map = match v.map with
|
||||||
| Name v -> ok v.value
|
| Name v -> ok v.value
|
||||||
| _ -> simple_fail "no complex map remove yet" in
|
| _ -> simple_fail "no complex map remove yet" in
|
||||||
let%bind key' = simpl_expression key in
|
let%bind key' = simpl_expression key in
|
||||||
let expr = E_constant ("MAP_REMOVE", [key' ; e_variable map]) in
|
let expr = e_constant ~loc "MAP_REMOVE" [key' ; e_variable map] in
|
||||||
return @@ E_assign (map , [] , expr)
|
return @@ e_assign ~loc map [] expr
|
||||||
|
)
|
||||||
| SetRemove _ -> simple_fail "no set remove yet"
|
| SetRemove _ -> simple_fail "no set remove yet"
|
||||||
|
|
||||||
and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p ->
|
and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p ->
|
||||||
|
@ -33,7 +33,7 @@ let card_ez owner = card (e_address owner)
|
|||||||
|
|
||||||
let make_cards assoc_lst =
|
let make_cards assoc_lst =
|
||||||
let card_id_ty = t_nat in
|
let card_id_ty = t_nat in
|
||||||
e_map assoc_lst card_id_ty card_ty
|
e_typed_map assoc_lst card_id_ty card_ty
|
||||||
|
|
||||||
let card_pattern (coeff , qtt) =
|
let card_pattern (coeff , qtt) =
|
||||||
ez_e_record [
|
ez_e_record [
|
||||||
@ -53,7 +53,7 @@ let card_pattern_ez (coeff , qtt) =
|
|||||||
let make_card_patterns lst =
|
let make_card_patterns lst =
|
||||||
let card_pattern_id_ty = t_nat in
|
let card_pattern_id_ty = t_nat in
|
||||||
let assoc_lst = List.mapi (fun i x -> (e_nat i , x)) lst in
|
let assoc_lst = List.mapi (fun i x -> (e_nat i , x)) lst in
|
||||||
e_map assoc_lst card_pattern_id_ty card_pattern_ty
|
e_typed_map assoc_lst card_pattern_id_ty card_pattern_ty
|
||||||
|
|
||||||
let storage cards_patterns cards next_id =
|
let storage cards_patterns cards next_id =
|
||||||
ez_e_record [
|
ez_e_record [
|
||||||
@ -210,9 +210,9 @@ let sell () =
|
|||||||
e_pair sell_action storage
|
e_pair sell_action storage
|
||||||
in
|
in
|
||||||
let make_expecter : int -> expression -> unit result = fun n result ->
|
let make_expecter : int -> expression -> unit result = fun n result ->
|
||||||
let%bind (ops , storage) = get_e_pair result in
|
let%bind (ops , storage) = get_e_pair @@ Location.unwrap result in
|
||||||
let%bind () =
|
let%bind () =
|
||||||
let%bind lst = get_e_list ops in
|
let%bind lst = get_e_list @@ Location.unwrap ops in
|
||||||
Assert.assert_list_size lst 1 in
|
Assert.assert_list_size lst 1 in
|
||||||
let expected_storage =
|
let expected_storage =
|
||||||
let cards = List.hds @@ cards_ez first_owner n in
|
let cards = List.hds @@ cards_ez first_owner n in
|
||||||
|
@ -253,7 +253,7 @@ let map () : unit result =
|
|||||||
let ez lst =
|
let ez lst =
|
||||||
let open Ast_simplified.Combinators in
|
let open Ast_simplified.Combinators in
|
||||||
let lst' = List.map (fun (x, y) -> e_int x, e_int y) lst in
|
let lst' = List.map (fun (x, y) -> e_int x, e_int y) lst in
|
||||||
e_map lst' t_int t_int
|
e_typed_map lst' t_int t_int
|
||||||
in
|
in
|
||||||
let%bind () =
|
let%bind () =
|
||||||
let make_input = fun n -> ez [(23, n) ; (42, 4)] in
|
let make_input = fun n -> ez [(23, n) ; (42, 4)] in
|
||||||
|
@ -29,7 +29,7 @@ module Errors = struct
|
|||||||
let wrong_arity (n:string) (expected:int) (actual:int) () =
|
let wrong_arity (n:string) (expected:int) (actual:int) () =
|
||||||
let title () = "wrong arity" in
|
let title () = "wrong arity" in
|
||||||
let full () =
|
let full () =
|
||||||
Format.asprintf "Wrong number of args passed to [%s]. Expected was %d, received was %d."
|
Format.asprintf "Wrong number of args passed to [%s]. Expected was %d, received was %d"
|
||||||
n expected actual
|
n expected actual
|
||||||
in
|
in
|
||||||
error title full ()
|
error title full ()
|
||||||
@ -204,13 +204,20 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
|||||||
match tv_opt with
|
match tv_opt with
|
||||||
| None -> ok ()
|
| None -> ok ()
|
||||||
| Some tv' -> O.assert_type_value_eq (tv' , tv) in
|
| Some tv' -> O.assert_type_value_eq (tv' , tv) in
|
||||||
ok @@ make_a_e expr tv e in
|
let location = Location.get_location ae in
|
||||||
|
ok @@ make_a_e ~location expr tv e in
|
||||||
let main_error =
|
let main_error =
|
||||||
let title () = "typing expression" in
|
let title () = "typing expression" in
|
||||||
let content () = Format.asprintf "Expression: %a\nLog: %s\n" I.PP.expression ae (L.get()) in
|
let content () =
|
||||||
|
match L.get () with
|
||||||
|
| "" ->
|
||||||
|
Format.asprintf "Expression: %a\n" I.PP.expression ae
|
||||||
|
| l ->
|
||||||
|
Format.asprintf "Expression: %a\nLog: %s\n" I.PP.expression ae l
|
||||||
|
in
|
||||||
error title content in
|
error title content in
|
||||||
trace main_error @@
|
trace main_error @@
|
||||||
match ae with
|
match Location.unwrap ae with
|
||||||
(* Basic *)
|
(* Basic *)
|
||||||
| E_failwith _ -> simple_fail "can't type failwith in isolation"
|
| E_failwith _ -> simple_fail "can't type failwith in isolation"
|
||||||
| E_variable name ->
|
| E_variable name ->
|
||||||
@ -362,9 +369,9 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
|||||||
match input_type with
|
match input_type with
|
||||||
| Some ty -> ok ty
|
| Some ty -> ok ty
|
||||||
| None -> (
|
| None -> (
|
||||||
match result with
|
match Location.unwrap result with
|
||||||
| I.E_let_in li -> (
|
| I.E_let_in li -> (
|
||||||
match li.rhs with
|
match Location.unwrap li.rhs with
|
||||||
| I.E_variable name when name = (fst binder) -> (
|
| I.E_variable name when name = (fst binder) -> (
|
||||||
match snd li.binder with
|
match snd li.binder with
|
||||||
| Some ty -> ok ty
|
| Some ty -> ok ty
|
||||||
@ -409,7 +416,8 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
|
|||||||
let%bind ex' = type_expression e ex in
|
let%bind ex' = type_expression e ex in
|
||||||
match m with
|
match m with
|
||||||
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
|
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
|
||||||
| I.Match_bool { match_false ; match_true = E_failwith fw } -> (
|
| I.Match_bool { match_false ; match_true } when I.is_e_failwith match_true -> (
|
||||||
|
let%bind fw = I.get_e_failwith match_true in
|
||||||
let%bind fw' = type_expression e fw in
|
let%bind fw' = type_expression e fw in
|
||||||
let%bind mf' = type_expression e match_false in
|
let%bind mf' = type_expression e match_false in
|
||||||
let%bind () =
|
let%bind () =
|
||||||
@ -541,55 +549,54 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
|
|||||||
match e.expression with
|
match e.expression with
|
||||||
| E_literal l ->
|
| E_literal l ->
|
||||||
let%bind l = untype_literal l in
|
let%bind l = untype_literal l in
|
||||||
return (E_literal l)
|
return (e_literal l)
|
||||||
| E_constant (n, lst) ->
|
| E_constant (n, lst) ->
|
||||||
let%bind lst' = bind_list
|
let%bind lst' = bind_map_list untype_expression lst in
|
||||||
@@ List.map untype_expression lst in
|
return (e_constant n lst')
|
||||||
return (E_constant (n, lst'))
|
|
||||||
| E_variable n ->
|
| E_variable n ->
|
||||||
return (E_variable n)
|
return (e_variable n)
|
||||||
| E_application (f, arg) ->
|
| E_application (f, arg) ->
|
||||||
let%bind f' = untype_expression f in
|
let%bind f' = untype_expression f in
|
||||||
let%bind arg' = untype_expression arg in
|
let%bind arg' = untype_expression arg in
|
||||||
return (E_application (f', arg'))
|
return (e_application f' arg')
|
||||||
| E_lambda {binder;input_type;output_type;result} ->
|
| E_lambda {binder;input_type;output_type;result} ->
|
||||||
let%bind input_type = untype_type_value input_type in
|
let%bind input_type = untype_type_value input_type in
|
||||||
let%bind output_type = untype_type_value output_type in
|
let%bind output_type = untype_type_value output_type in
|
||||||
let%bind result = untype_expression result in
|
let%bind result = untype_expression result in
|
||||||
return (E_lambda {binder = (binder , Some input_type);input_type = Some input_type;output_type = Some output_type;result})
|
return (e_lambda binder (Some input_type) (Some output_type) result)
|
||||||
| E_tuple lst ->
|
| E_tuple lst ->
|
||||||
let%bind lst' = bind_list
|
let%bind lst' = bind_list
|
||||||
@@ List.map untype_expression lst in
|
@@ List.map untype_expression lst in
|
||||||
return (E_tuple lst')
|
return (e_tuple lst')
|
||||||
| E_tuple_accessor (tpl, ind) ->
|
| E_tuple_accessor (tpl, ind) ->
|
||||||
let%bind tpl' = untype_expression tpl in
|
let%bind tpl' = untype_expression tpl in
|
||||||
return (E_accessor (tpl', [Access_tuple ind]))
|
return (e_accessor tpl' [Access_tuple ind])
|
||||||
| E_constructor (n, p) ->
|
| E_constructor (n, p) ->
|
||||||
let%bind p' = untype_expression p in
|
let%bind p' = untype_expression p in
|
||||||
return (E_constructor (n, p'))
|
return (e_constructor n p')
|
||||||
| E_record r ->
|
| E_record r ->
|
||||||
let%bind r' = bind_smap
|
let%bind r' = bind_smap
|
||||||
@@ SMap.map untype_expression r in
|
@@ SMap.map untype_expression r in
|
||||||
return (E_record r')
|
return (e_record r')
|
||||||
| E_record_accessor (r, s) ->
|
| E_record_accessor (r, s) ->
|
||||||
let%bind r' = untype_expression r in
|
let%bind r' = untype_expression r in
|
||||||
return (E_accessor (r', [Access_record s]))
|
return (e_accessor r' [Access_record s])
|
||||||
| E_map m ->
|
| E_map m ->
|
||||||
let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
|
let%bind m' = bind_map_list (bind_map_pair untype_expression) m in
|
||||||
return (E_map m')
|
return (e_map m')
|
||||||
| E_list lst ->
|
| E_list lst ->
|
||||||
let%bind lst' = bind_map_list untype_expression lst in
|
let%bind lst' = bind_map_list untype_expression lst in
|
||||||
return (E_list lst')
|
return (e_list lst')
|
||||||
| E_look_up dsi ->
|
| E_look_up dsi ->
|
||||||
let%bind dsi' = bind_map_pair untype_expression dsi in
|
let%bind (a , b) = bind_map_pair untype_expression dsi in
|
||||||
return (E_look_up dsi')
|
return (e_look_up a b)
|
||||||
| E_matching (ae, m) ->
|
| E_matching (ae, m) ->
|
||||||
let%bind ae' = untype_expression ae in
|
let%bind ae' = untype_expression ae in
|
||||||
let%bind m' = untype_matching untype_expression m in
|
let%bind m' = untype_matching untype_expression m in
|
||||||
return (E_matching (ae', m'))
|
return (e_matching ae' m')
|
||||||
| E_failwith ae ->
|
| E_failwith ae ->
|
||||||
let%bind ae' = untype_expression ae in
|
let%bind ae' = untype_expression ae in
|
||||||
return (E_failwith ae')
|
return (e_failwith ae')
|
||||||
| E_sequence _
|
| E_sequence _
|
||||||
| E_loop _
|
| E_loop _
|
||||||
| E_assign _ -> simple_fail "not possible to untranspile statements yet"
|
| E_assign _ -> simple_fail "not possible to untranspile statements yet"
|
||||||
@ -597,7 +604,7 @@ let rec untype_expression (e:O.annotated_expression) : (I.expression) result =
|
|||||||
let%bind tv = untype_type_value rhs.type_annotation in
|
let%bind tv = untype_type_value rhs.type_annotation in
|
||||||
let%bind rhs = untype_expression rhs in
|
let%bind rhs = untype_expression rhs in
|
||||||
let%bind result = untype_expression result in
|
let%bind result = untype_expression result in
|
||||||
return (E_let_in {binder = (binder , Some tv);rhs;result})
|
return (e_let_in (binder , (Some tv)) rhs result)
|
||||||
|
|
||||||
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
|
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
|
||||||
let open I in
|
let open I in
|
||||||
|
8
vendors/ligo-utils/simple-utils/location.ml
vendored
8
vendors/ligo-utils/simple-utils/location.ml
vendored
@ -22,16 +22,22 @@ let make (start_pos:Lexing.position) (end_pos:Lexing.position) : t =
|
|||||||
|
|
||||||
let virtual_location s = Virtual s
|
let virtual_location s = Virtual s
|
||||||
let dummy = virtual_location "dummy"
|
let dummy = virtual_location "dummy"
|
||||||
|
let generated = virtual_location "generated"
|
||||||
|
|
||||||
type 'a wrap = {
|
type 'a wrap = {
|
||||||
wrap_content : 'a ;
|
wrap_content : 'a ;
|
||||||
location : t ;
|
location : t ;
|
||||||
}
|
}
|
||||||
|
|
||||||
let wrap ~loc wrap_content = { wrap_content ; location = loc }
|
let wrap ?(loc = generated) wrap_content = { wrap_content ; location = loc }
|
||||||
|
let get_location x = x.location
|
||||||
let unwrap { wrap_content ; _ } = wrap_content
|
let unwrap { wrap_content ; _ } = wrap_content
|
||||||
let map f x = { x with wrap_content = f x.wrap_content }
|
let map f x = { x with wrap_content = f x.wrap_content }
|
||||||
let pp_wrap f ppf { wrap_content ; _ } = Format.fprintf ppf "%a" f wrap_content
|
let pp_wrap f ppf { wrap_content ; _ } = Format.fprintf ppf "%a" f wrap_content
|
||||||
|
|
||||||
let lift_region : 'a Region.reg -> 'a wrap = fun x ->
|
let lift_region : 'a Region.reg -> 'a wrap = fun x ->
|
||||||
wrap ~loc:(File x.region) x.value
|
wrap ~loc:(File x.region) x.value
|
||||||
|
let lift : Region.region -> t = fun x -> File x
|
||||||
|
|
||||||
|
let r_extract : 'a Region.reg -> t = fun x -> File x.region
|
||||||
|
let r_split : 'a Region.reg -> ('a * t) = fun x -> x.value , File x.region
|
||||||
|
13
vendors/ligo-utils/simple-utils/trace.ml
vendored
13
vendors/ligo-utils/simple-utils/trace.ml
vendored
@ -134,7 +134,7 @@ let mk_error
|
|||||||
let message' = X_option.map (fun x -> ("message" , `String (x ()))) message in
|
let message' = X_option.map (fun x -> ("message" , `String (x ()))) message in
|
||||||
`Assoc (X_option.collapse_list [ error_code' ; title' ; message' ; data' ])
|
`Assoc (X_option.collapse_list [ error_code' ; title' ; message' ; data' ])
|
||||||
|
|
||||||
let error title message () = mk_error ~title:(title) ~message:(message) ()
|
let error ?data ?error_code title message () = mk_error ?data ?error_code ~title:(title) ~message:(message) ()
|
||||||
|
|
||||||
(**
|
(**
|
||||||
Helpers that ideally shouldn't be used in production.
|
Helpers that ideally shouldn't be used in production.
|
||||||
@ -470,13 +470,17 @@ let json_of_error = J.to_string
|
|||||||
|
|
||||||
let error_pp out (e : error) =
|
let error_pp out (e : error) =
|
||||||
let open JSON_string_utils in
|
let open JSON_string_utils in
|
||||||
let message = e |> member "message" |> J.to_string in
|
let message =
|
||||||
|
let opt = e |> member "message" |> string in
|
||||||
|
X_option.unopt ~default:"" opt in
|
||||||
let error_code =
|
let error_code =
|
||||||
let error_code = e |> member "error_code" in
|
let error_code = e |> member "error_code" in
|
||||||
match error_code with
|
match error_code with
|
||||||
| `Null -> ""
|
| `Null -> ""
|
||||||
| _ -> " (" ^ (J.to_string error_code) ^ ")" in
|
| _ -> " (" ^ (J.to_string error_code) ^ ")" in
|
||||||
let title = e |> member "title" |> J.to_string in
|
let title =
|
||||||
|
let opt = e |> member "title" |> string in
|
||||||
|
X_option.unopt ~default:"" opt in
|
||||||
let data =
|
let data =
|
||||||
let data = e |> member "data" in
|
let data = e |> member "data" in
|
||||||
match data with
|
match data with
|
||||||
@ -484,9 +488,6 @@ let error_pp out (e : error) =
|
|||||||
| _ -> J.to_string data in
|
| _ -> J.to_string data in
|
||||||
Format.fprintf out "%s (%s): %s. %s" title error_code message data
|
Format.fprintf out "%s (%s): %s. %s" title error_code message data
|
||||||
|
|
||||||
(* let error_pp out (e : error) =
|
|
||||||
* Format.fprintf out "%s" @@ json_of_error e *)
|
|
||||||
|
|
||||||
|
|
||||||
let error_pp_short out (e : error) =
|
let error_pp_short out (e : error) =
|
||||||
let open JSON_string_utils in
|
let open JSON_string_utils in
|
||||||
|
Loading…
Reference in New Issue
Block a user