diff --git a/src/simplify/ligodity.ml b/src/simplify/ligodity.ml index 0c3398758..0e51b6f9f 100644 --- a/src/simplify/ligodity.ml +++ b/src/simplify/ligodity.ml @@ -19,6 +19,8 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value open Operators.Simplify.Ligodity +let r_split = Location.r_split + let rec simpl_type_expression : Raw.type_expr -> type_expression result = function | TPar x -> simpl_type_expression x.value.inside @@ -79,9 +81,10 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result ok @@ T_tuple lst let rec simpl_expression : - ?te_annot:type_expression -> Raw.expr -> expr result = fun ?te_annot t -> - let return x = ok @@ make_option_typed x te_annot in - let simpl_projection = fun (p:Raw.projection) -> + Raw.expr -> expr result = fun t -> + let return x = ok x in + let simpl_projection = fun (p:Raw.projection Region.reg) -> + let (p , loc) = r_split p in let var = let name = p.struct_name.value in e_variable name in @@ -95,107 +98,127 @@ let rec simpl_expression : Access_tuple (Z.to_int (snd index.value)) in List.map aux @@ npseq_to_list path in - return @@ E_accessor (var, path') + return @@ e_accessor ~loc var path' in - let mk_let_in binder rhs result = - E_let_in {binder; rhs; result} in match t with | Raw.ELetIn e -> ( - let Raw.{binding; body; _} = e.value in - let Raw.{variable; lhs_type; let_rhs; _} = binding in - let%bind type_annotation = bind_map_option - (fun (_,type_expr) -> simpl_type_expression type_expr) + let Raw.{binding ; body ; _} = e.value in + let Raw.{variable ; lhs_type ; let_rhs ; _} = binding in + let%bind ty_opt = + bind_map_option + (fun (_ , type_expr) -> simpl_type_expression type_expr) 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 - return @@ mk_let_in (variable.value , None) rhs body + return @@ e_let_in (variable.value , None) rhs' body ) | Raw.EAnnot a -> ( - let (expr , type_expr) = a.value in - match te_annot with - | None -> ( - let%bind te_annot = simpl_type_expression type_expr in - let%bind expr' = simpl_expression ~te_annot expr in - ok expr' - ) - | Some _ -> simple_fail "no double annotation" + let (a , loc) = r_split a in + let (expr , type_expr) = a in + let%bind expr' = simpl_expression expr in + let%bind type_expr' = simpl_type_expression type_expr in + return @@ e_annotation ~loc expr' type_expr' ) | EVar c -> ( let c' = c.value in match List.assoc_opt c' constants with - | None -> return @@ E_variable c.value - | Some s -> return @@ E_constant (s , []) + | None -> return @@ e_variable c.value + | Some s -> return @@ e_constant s [] ) | 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 match e1 with - | EVar f -> - (match List.assoc_opt f.value constants with - | None -> + | EVar f -> ( + let (f , f_loc) = r_split f in + match List.assoc_opt f constants with + | None -> ( let%bind arg = simpl_tuple_expression (nseq_to_list e2) in - return @@ E_application (e_variable f.value, arg) - | Some s -> return @@ E_constant (s , args)) - | e1 -> - let%bind e1' = simpl_expression e1 in - let%bind arg = simpl_tuple_expression (nseq_to_list e2) in - return @@ E_application (e1' , arg) + return @@ e_application ~loc (e_variable ~loc:f_loc f) arg + ) + | Some s -> return @@ e_constant ~loc s args + ) + | e1 -> ( + let%bind e1' = simpl_expression e1 in + let%bind arg = simpl_tuple_expression (nseq_to_list e2) in + return @@ e_application ~loc e1' arg + ) ) - | EPar x -> simpl_expression ?te_annot x.value.inside - | EUnit _ -> return @@ E_literal Literal_unit - | EBytes x -> return @@ E_literal (Literal_bytes (Bytes.of_string @@ fst x.value)) - | ETuple tpl -> simpl_tuple_expression ?te_annot @@ (npseq_to_list tpl.value) - | ERecord r -> + | EPar x -> simpl_expression x.value.inside + | EUnit reg -> ( + let (_ , loc) = r_split 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 -> simpl_tuple_expression @@ (npseq_to_list tpl.value) + | ERecord r -> ( + let (r , loc) = r_split r in 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 (x:Raw.field_assign Raw.reg) -> (x.value.field_name, x.value.field_expr)) - @@ pseq_to_list r.value.elements in - let aux prev (k, v) = SMap.add k v prev in - return @@ E_record (List.fold_left aux SMap.empty fields) - | EProj p' -> ( - let p = p'.value in - simpl_projection p + @@ pseq_to_list r.elements in + let map = SMap.of_list fields in + return @@ e_record ~loc map ) - | EConstr c -> - let (c, args) = c.value in + | EProj p -> simpl_projection p + | EConstr c -> ( + let ((c_name , args) , loc) = r_split c in + let (c_name , _c_loc) = r_split c_name in let args = match args with None -> [] | Some arg -> [arg] 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) -> - simpl_binop ?te_annot "ADD" c.value + simpl_binop "ADD" c | EArith (Sub c) -> - simpl_binop ?te_annot "SUB" c.value + simpl_binop "SUB" c | EArith (Mult c) -> - simpl_binop ?te_annot "TIMES" c.value + simpl_binop "TIMES" c | EArith (Div c) -> - simpl_binop ?te_annot "DIV" c.value + simpl_binop "DIV" c | EArith (Mod c) -> - simpl_binop ?te_annot "MOD" c.value - | EArith (Int n) -> - let n = Z.to_int @@ snd @@ n.value in - return @@ E_literal (Literal_int n) - | EArith (Nat n) -> - let n = Z.to_int @@ snd @@ n.value in - return @@ E_literal (Literal_nat n) - | EArith (Mtz n) -> - let n = Z.to_int @@ snd @@ n.value in - return @@ E_literal (Literal_tez n) + simpl_binop "MOD" c + | EArith (Int n) -> ( + let (n , loc) = r_split n in + let n = Z.to_int @@ snd @@ n in + return @@ e_literal ~loc (Literal_int n) + ) + | EArith (Nat n) -> ( + let (n , loc) = r_split n in + let n = Z.to_int @@ snd @@ n in + 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" - | EString (String s) -> + | EString (String s) -> ( + let (s , loc) = r_split s in let s' = - let s = s.value in + let s = s in String.(sub s 1 ((length s) - 2)) in - return @@ E_literal (Literal_string s') + return @@ e_literal ~loc (Literal_string s') + ) | EString _ -> simple_fail "string: not supported yet" - | ELogic l -> simpl_logic_expression ?te_annot l - | EList l -> simpl_list_expression ?te_annot l - | ECase c -> - let%bind e = simpl_expression c.value.expr in + | ELogic l -> simpl_logic_expression l + | EList l -> simpl_list_expression l + | ECase c -> ( + let (c , loc) = r_split c in + let%bind e = simpl_expression c.expr in let%bind lst = let aux (x : Raw.expr Raw.case_clause) = let%bind expr = simpl_expression x.rhs in @@ -203,96 +226,111 @@ let rec simpl_expression : bind_list @@ List.map aux @@ 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 - return @@ E_matching (e, cases) - | EFun lamb -> + return @@ e_matching ~loc e cases + ) + | EFun lamb -> ( + let (lamb , loc) = r_split lamb in let%bind input_type = bind_map_option (fun (_,type_expr) -> simpl_type_expression type_expr) - lamb.value.p_annot in + lamb.p_annot in let body, body_type = - match lamb.value.body with - EAnnot {value = expr, type_expr} -> expr, Some type_expr + match lamb.body with + | EAnnot {value = expr, type_expr} -> expr, Some type_expr | expr -> expr, None in let%bind output_type = bind_map_option simpl_type_expression body_type in let%bind result = simpl_expression body in - let binder = lamb.value.param.value, input_type in - let lambda = {binder; input_type; output_type; result = result} - in return @@ E_lambda lambda - | ESeq s -> - let items : Raw.expr list = pseq_to_list s.value.elements in - (match items with - [] -> return @@ E_skip - | expr::more -> - let expr' = simpl_expression expr in - let apply (e1: Raw.expr) (e2: expression Trace.result) = - let%bind a = simpl_expression e1 in - let%bind e2' = e2 in - return @@ E_sequence (a, e2') - in List.fold_right apply more expr') - | ECond c -> - let c = c.value in + let binder = lamb.param.value in + return @@ e_lambda ~loc binder input_type output_type result + ) + | ESeq s -> ( + let (s , loc) = r_split s in + let items : Raw.expr list = pseq_to_list s.elements in + match items with + | [] -> return @@ e_skip ~loc () + | expr :: more -> ( + let expr' = simpl_expression expr in + let apply (e1: Raw.expr) (e2: expression Trace.result) = + let%bind a = simpl_expression e1 in + let%bind e2' = e2 in + return @@ e_sequence ~loc a e2' + in List.fold_right apply more expr' + ) + ) + | ECond c -> ( + let (c , loc) = r_split c in let%bind expr = simpl_expression c.test in let%bind match_true = simpl_expression c.ifso in let%bind match_false = simpl_expression c.ifnot in - return @@ E_matching (expr, (Match_bool {match_true; match_false})) -and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result = - let return x = ok @@ make_option_typed x te_annot in - match t with - | BoolExpr (False _) -> - return @@ E_literal (Literal_bool false) - | BoolExpr (True _) -> - return @@ E_literal (Literal_bool true) - | BoolExpr (Or b) -> - simpl_binop ?te_annot "OR" b.value - | BoolExpr (And b) -> - simpl_binop ?te_annot "AND" b.value - | BoolExpr (Not b) -> - simpl_unop ?te_annot "NOT" b.value - | CompExpr (Lt c) -> - simpl_binop ?te_annot "LT" c.value - | CompExpr (Gt c) -> - simpl_binop ?te_annot "GT" c.value - | CompExpr (Leq c) -> - simpl_binop ?te_annot "LE" c.value - | CompExpr (Geq c) -> - simpl_binop ?te_annot "GE" c.value - | CompExpr (Equal c) -> - simpl_binop ?te_annot "EQ" c.value - | CompExpr (Neq c) -> - simpl_binop ?te_annot "NEQ" c.value + let match_bool = Match_bool { match_true ; match_false } in + return @@ e_matching ~loc expr match_bool + ) -and simpl_list_expression ?te_annot (t:Raw.list_expr) : expression result = - let return x = ok @@ make_option_typed x te_annot in +and simpl_logic_expression (t:Raw.logic_expr) : expr result = + let return x = ok @@ x in match t with - | Cons c -> - simpl_binop ?te_annot "CONS" c.value - | List lst -> + | BoolExpr (False reg) -> ( + let loc = Location.lift reg in + return @@ e_literal ~loc (Literal_bool false) + ) + | BoolExpr (True reg) -> ( + let loc = Location.lift reg in + return @@ e_literal ~loc (Literal_bool true) + ) + | BoolExpr (Or b) -> + simpl_binop "OR" b + | BoolExpr (And b) -> + simpl_binop "AND" b + | BoolExpr (Not b) -> + simpl_unop "NOT" b + | CompExpr (Lt c) -> + simpl_binop "LT" c + | CompExpr (Gt c) -> + simpl_binop "GT" c + | CompExpr (Leq c) -> + simpl_binop "LE" c + | CompExpr (Geq c) -> + simpl_binop "GE" c + | CompExpr (Equal c) -> + simpl_binop "EQ" c + | CompExpr (Neq c) -> + simpl_binop "NEQ" c + +and simpl_list_expression (t:Raw.list_expr) : expression result = + let return x = ok @@ x in + match t with + | Cons c -> simpl_binop "CONS" c + | List lst -> ( + let (lst , loc) = r_split lst in let%bind lst' = bind_map_list simpl_expression @@ - pseq_to_list lst.value.elements in - return @@ E_list lst' + pseq_to_list lst.elements in + return @@ e_list ~loc lst' + ) -and simpl_binop ?te_annot (name:string) (t:_ Raw.bin_op) : expression result = - let return x = ok @@ make_option_typed x te_annot in - let%bind a = simpl_expression t.arg1 in - let%bind b = simpl_expression t.arg2 in - return @@ E_constant (name, [a;b]) +and simpl_binop (name:string) (t:_ Raw.bin_op Region.reg) : expression result = + let return x = ok @@ x in + let (args , loc) = r_split t in + let%bind a = simpl_expression args.arg1 in + 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 = - let return x = ok @@ make_option_typed x te_annot in +and simpl_unop (name:string) (t:_ Raw.un_op Region.reg) : expression result = + let return x = ok @@ x in + let (t , loc) = r_split t 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 = - let return x = ok @@ make_option_typed x te_annot in +and simpl_tuple_expression ?loc (lst:Raw.expr list) : expression result = + let return x = ok @@ x in match lst with - | [] -> return @@ E_literal Literal_unit - | [hd] -> simpl_expression ?te_annot hd + | [] -> return @@ e_literal ?loc Literal_unit + | [hd] -> simpl_expression hd | lst -> 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 -> let open! Raw in @@ -309,7 +347,7 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu let%bind type_annotation = bind_map_option (fun (_,type_expr) -> simpl_type_expression type_expr) lhs_type in - let%bind rhs = simpl_expression ?te_annot:type_annotation let_rhs in + let%bind rhs = simpl_expression let_rhs in let name = variable.value in ok @@ loc x @@ (Declaration_constant (name , type_annotation , rhs)) ) diff --git a/src/test/coase_tests.ml b/src/test/coase_tests.ml index 4d15754db..8f3ef0e26 100644 --- a/src/test/coase_tests.ml +++ b/src/test/coase_tests.ml @@ -31,7 +31,7 @@ let card_ez owner = card (e_address owner) let make_cards assoc_lst = 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) = ez_e_record [ @@ -51,7 +51,7 @@ let card_pattern_ez (coeff , qtt) = let make_card_patterns lst = let card_pattern_id_ty = t_nat 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 = ez_e_record [ @@ -208,9 +208,9 @@ let sell () = e_pair sell_action storage in 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 lst = get_e_list ops in + let%bind lst = get_e_list @@ Location.unwrap ops in Assert.assert_list_size lst 1 in let expected_storage = let cards = List.hds @@ cards_ez first_owner n in diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index ccbf6e893..5cfec5068 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -249,7 +249,7 @@ let map () : unit result = let ez lst = let open Ast_simplified.Combinators 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 let%bind () = let make_input = fun n -> ez [(23, n) ; (42, 4)] in