From e7c71ae4cc4612631ab11e857a2c96c9e7772bc1 Mon Sep 17 00:00:00 2001 From: Pierre-Emmanuel Wulfman Date: Fri, 6 Mar 2020 23:44:28 +0100 Subject: [PATCH] passing test for Cameligo --- src/passes/2-simplify/cameligo.ml | 28 ++++- src/passes/2-simplify/pascaligo.ml | 8 +- src/passes/6-interpreter/interpreter.ml | 4 +- src/passes/6-transpiler/transpiler.ml | 114 +++++++++++++++++- src/passes/8-compiler/compiler_program.ml | 24 +++- src/passes/operators/operators.ml | 33 +++-- src/stages/common/PP.ml | 7 +- src/stages/common/types.ml | 7 +- src/stages/mini_c/PP.ml | 7 +- src/stages/typesystem/shorthands.ml | 1 + src/test/contracts/recursion.mligo | 4 +- src/test/integration_tests.ml | 2 +- test.mligo | 10 ++ vendors/ligo-utils/tezos-utils/x_michelson.ml | 2 + 14 files changed, 220 insertions(+), 31 deletions(-) create mode 100644 test.mligo diff --git a/src/passes/2-simplify/cameligo.ml b/src/passes/2-simplify/cameligo.ml index 03a3f77b5..2f7e7e32e 100644 --- a/src/passes/2-simplify/cameligo.ml +++ b/src/passes/2-simplify/cameligo.ml @@ -70,6 +70,17 @@ module Errors = struct fun () -> Format.asprintf "%a" Location.pp_lift @@ param_loc)] in error ~data title message + let untyped_recursive_function var = + let title () = "" in + let message () = + Format.asprintf "\nUntyped recursive function \ + are not supported yet.\n" in + let param_loc = var.Region.region in + let data = [ + ("location", + fun () -> Format.asprintf "%a" Location.pp_lift @@ param_loc)] + in error ~data title message + let unsupported_tuple_pattern p = let title () = "" in let message () = @@ -739,12 +750,11 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap list result let%bind type_expression = simpl_type_expression type_expr in ok @@ [loc x @@ Declaration_type (Var.of_name name.value , type_expression)] | Let x -> ( - let (_, _rec, let_binding, attributes), _ = r_split x in + let (_, recursive, let_binding, attributes), _ = r_split x in let inline = List.exists (fun (a: Raw.attribute) -> a.value = "inline") attributes in let binding = let_binding in let {binders; lhs_type; let_rhs} = binding in - let%bind (hd, _) = - let (hd, tl) = binders in ok (hd, tl) in + let (hd, _) = binders in match hd with | PTuple pt -> let process_variable (var_pair: pattern * Raw.expr) : @@ -841,6 +851,18 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap list result ) | Some t -> ok @@ Some t in + let binder = Var.of_name var.value in + let%bind rhs' = match recursive with + None -> ok @@ rhs' + | Some _ -> match rhs'.expression_content with + E_lambda lambda -> + (match lhs_type with + None -> fail @@ untyped_recursive_function var + | Some (lhs_type) -> + let expression_content = E_recursive {fun_name=binder;fun_type=lhs_type;lambda} in + ok @@ {rhs' with expression_content}) + | _ -> ok @@ rhs' + in ok @@ [loc x @@ (Declaration_constant (Var.of_name var.value , lhs_type , inline, rhs'))] ) diff --git a/src/passes/2-simplify/pascaligo.ml b/src/passes/2-simplify/pascaligo.ml index 370e36e93..d62fc5125 100644 --- a/src/passes/2-simplify/pascaligo.ml +++ b/src/passes/2-simplify/pascaligo.ml @@ -1202,8 +1202,8 @@ and simpl_while_loop : Raw.while_loop -> (_ -> expression result) result = fun w in let init_rec = e_tuple [store_mutable_variable @@ captured_name_list] in let restore = fun expr -> List.fold_right aux captured_name_list expr in - let continue_expr = e_constant C_CONTINUE [for_body] in - let stop_expr = e_constant C_STOP [e_variable binder] in + let continue_expr = e_constant C_FOLD_CONTINUE [for_body] in + let stop_expr = e_constant C_FOLD_STOP [e_variable binder] in let aux_func = e_lambda binder None None @@ restore @@ @@ -1247,8 +1247,8 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi -> let restore = fun expr -> List.fold_right aux captured_name_list expr in (*Prep the lambda for the fold*) - let continue_expr = e_constant C_CONTINUE [restore(for_body)] in - let stop_expr = e_constant C_STOP [e_variable binder] in + let continue_expr = e_constant C_FOLD_CONTINUE [restore(for_body)] in + let stop_expr = e_constant C_FOLD_STOP [e_variable binder] in let aux_func = e_lambda binder None None @@ e_let_in (it,Some t_int) false false (e_accessor (e_variable binder) "1") @@ e_cond cond continue_expr (stop_expr) in diff --git a/src/passes/6-interpreter/interpreter.ml b/src/passes/6-interpreter/interpreter.ml index 3ef211f83..b93d0cf60 100644 --- a/src/passes/6-interpreter/interpreter.ml +++ b/src/passes/6-interpreter/interpreter.ml @@ -80,8 +80,8 @@ let rec apply_operator : Ast_typed.constant' -> value list -> value result = | ( C_IS_NAT , [ V_Ct (C_int a') ] ) -> if a' > 0 then return_some @@ V_Ct (C_nat a') else return_none () - | ( C_CONTINUE , [ v ] ) -> ok @@ v_pair (v_bool true , v) - | ( C_STOP , [ v ] ) -> ok @@ v_pair (v_bool false , v) + | ( C_FOLD_CONTINUE , [ v ] ) -> ok @@ v_pair (v_bool true , v) + | ( C_FOLD_STOP , [ v ] ) -> ok @@ v_pair (v_bool false , v) | ( C_ASSERTION , [ v ] ) -> let%bind pass = is_true v in if pass then return_ct @@ C_unit diff --git a/src/passes/6-transpiler/transpiler.ml b/src/passes/6-transpiler/transpiler.ml index d3dd96b10..8b39e6c4a 100644 --- a/src/passes/6-transpiler/transpiler.ml +++ b/src/passes/6-transpiler/transpiler.ml @@ -521,8 +521,118 @@ and transpile_lambda l (input_type , output_type) = ok @@ Combinators.Expression.make_tpl (closure , tv) and transpile_recursive {fun_name; fun_type; lambda} = - let closure = E_closure { binder=fun_name; body} in - ok @@ Combinators.Expression.make closure fun_type + let rec map_lambda : AST.expression_variable -> type_value -> AST.expression -> expression result = fun fun_name loop_type e -> + match e.expression_content with + E_lambda {binder;result} -> + let%bind body = map_lambda fun_name loop_type result in + ok @@ Expression.make (E_closure {binder;body}) loop_type| + _ -> replace_callback fun_name loop_type e + + and replace_callback : AST.expression_variable -> type_value -> AST.expression -> expression result = fun fun_name loop_type e -> + match e.expression_content with + E_let_in li -> + let%bind let_result = replace_callback fun_name loop_type li.let_result in + let%bind rhs = transpile_annotated_expression li.rhs in + let%bind ty = transpile_type e.type_expression in + ok @@ e_let_in li.let_binder ty li.inline rhs let_result | + E_matching m -> + let%bind ty = transpile_type e.type_expression in + matching fun_name loop_type m ty | + E_application {expr1;expr2} -> ( + match expr1.expression_content with + E_variable name when Var.equal fun_name name -> + let%bind expr = transpile_annotated_expression expr2 in + ok @@ Expression.make (E_constant {cons_name=C_LOOP_CONTINUE;arguments=[expr]}) loop_type | + _ -> + let%bind expr = transpile_annotated_expression e in + ok @@ Expression.make (E_constant {cons_name=C_LOOP_STOP;arguments=[expr]}) loop_type + ) | + _ -> + let%bind expr = transpile_annotated_expression e in + ok @@ Expression.make (E_constant {cons_name=C_LOOP_STOP;arguments=[expr]}) loop_type + and matching : AST.expression_variable -> type_value -> AST.matching -> type_value -> expression result = fun fun_name loop_type m ty -> + let return ret = ok @@ Expression.make ret @@ ty in + let%bind expr = transpile_annotated_expression m.matchee in + match m.cases with + Match_bool {match_true; match_false} -> + let%bind (t , f) = bind_map_pair (replace_callback fun_name loop_type) (match_true, match_false) in + return @@ E_if_bool (expr, t, f) + | Match_option { match_none; match_some = (name, s, tv) } -> + let%bind n = replace_callback fun_name loop_type match_none in + let%bind (tv' , s') = + let%bind tv' = transpile_type tv in + let%bind s' = replace_callback fun_name loop_type s in + ok (tv' , s') + in + return @@ E_if_none (expr , n , ((name , tv') , s')) + | Match_list { + match_nil ; + match_cons = ((hd_name) , (tl_name), match_cons, ty) ; + } -> ( + let%bind nil = replace_callback fun_name loop_type match_nil in + let%bind cons = + let%bind ty' = transpile_type ty in + let%bind match_cons' = replace_callback fun_name loop_type match_cons in + ok (((hd_name , ty') , (tl_name , ty')) , match_cons') + in + return @@ E_if_cons (expr , nil , cons) + ) + | Match_variant (lst , variant) -> ( + let%bind tree = + trace_strong (corner_case ~loc:__LOC__ "getting lr tree") @@ + tree_of_sum variant in + let%bind tree' = match tree with + | Empty -> fail (corner_case ~loc:__LOC__ "match empty variant") + | Full x -> ok x in + let%bind tree'' = + let rec aux t = + match (t : _ Append_tree.t') with + | Leaf (name , tv) -> + let%bind tv' = transpile_type tv in + ok (`Leaf name , tv') + | Node {a ; b} -> + let%bind a' = aux a in + let%bind b' = aux b in + let tv' = Mini_c.t_union (None, snd a') (None, snd b') in + ok (`Node (a' , b') , tv') + in aux tree' + in + let rec aux top t = + match t with + | ((`Leaf constructor_name) , tv) -> ( + let%bind ((_ , name) , body) = + trace_option (corner_case ~loc:__LOC__ "missing match clause") @@ + List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in + let%bind body' = replace_callback fun_name loop_type body in + return @@ E_let_in ((name , tv) , false , top , body') + ) + | ((`Node (a , b)) , tv) -> + let%bind a' = + let%bind a_ty = get_t_left tv in + let left_var = Var.fresh ~name:"left" () in + let%bind e = aux (((Expression.make (E_variable left_var) a_ty))) a in + ok ((left_var , a_ty) , e) + in + let%bind b' = + let%bind b_ty = get_t_right tv in + let right_var = Var.fresh ~name:"right" () in + let%bind e = aux (((Expression.make (E_variable right_var) b_ty))) b in + ok ((right_var , b_ty) , e) + in + return @@ E_if_left (top , a' , b') + in + trace_strong (corner_case ~loc:__LOC__ "building constructor") @@ + aux expr tree'' + ) + | AST.Match_tuple _ -> failwith "match_tuple not supported" + in + let%bind fun_type = transpile_type fun_type in + let%bind (input_type,output_type) = get_t_function fun_type in + let loop_type = t_union (None, input_type) (None, output_type) in + let%bind body = map_lambda fun_name loop_type lambda.result in + let expr = Expression.make_tpl (E_variable fun_name, input_type) in + let body = Expression.make (E_iterator (C_LOOP_LEFT, ((lambda.binder, loop_type),body), expr)) output_type in + ok @@ Expression.make (E_closure {binder=fun_name;body}) fun_type let transpile_declaration env (d:AST.declaration) : toplevel_statement result = match d with diff --git a/src/passes/8-compiler/compiler_program.ml b/src/passes/8-compiler/compiler_program.ml index 491b1b91a..6d24bd06b 100644 --- a/src/passes/8-compiler/compiler_program.ml +++ b/src/passes/8-compiler/compiler_program.ml @@ -50,13 +50,23 @@ let rec get_operator : constant' -> type_value -> expression list -> predicate r let%bind ty' = Mini_c.get_t_option ty in let%bind m_ty = Compiler_type.type_ ty' in ok @@ simple_constant @@ prim ~children:[m_ty] I_NONE - ) | C_NIL -> ( let%bind ty' = Mini_c.get_t_list ty in let%bind m_ty = Compiler_type.type_ ty' in ok @@ simple_unary @@ prim ~children:[m_ty] I_NIL ) + | C_LOOP_CONTINUE -> ( + let%bind (_,ty) = get_t_or ty in + let%bind m_ty = Compiler_type.type_ ty in + let m_ty' = t_pair t_unit m_ty in + ok @@ simple_unary @@ prim ~children:[m_ty'] I_LEFT + ) + | C_LOOP_STOP -> ( + let%bind (ty, _) = get_t_or ty in + let%bind m_ty = Compiler_type.type_ ty in + ok @@ simple_unary @@ seq [ i_push_unit; i_pair; prim ~children:[m_ty] I_RIGHT] + ) | C_SET_EMPTY -> ( let%bind ty' = Mini_c.get_t_set ty in let%bind m_ty = Compiler_type.type_ ty' in @@ -397,6 +407,18 @@ and translate_expression (expr:expression) (env:environment) : michelson result ]) in return code ) + | C_LOOP_LEFT -> ( + let%bind (_, ty) = get_t_or (snd v) in + let%bind m_ty = Compiler_type.type_ ty in + let m_ty' = t_pair t_unit m_ty in + let%bind code = ok (seq [ + expr' ; + prim ~children:[m_ty'] I_LEFT; + i_loop_left body'; + prim I_CDR + ]) in + return code + ) | s -> ( let iter = Format.asprintf "iter %a" PP.constant s in let error = error (thunk "bad iterator") (thunk iter) in diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml index f01b5aa44..9815ec83f 100644 --- a/src/passes/operators/operators.ml +++ b/src/passes/operators/operators.ml @@ -350,10 +350,11 @@ module Simplify = struct (* Loop module *) | "Loop.fold_while" -> ok C_FOLD_WHILE - | "Loop.resume" -> ok C_CONTINUE - | "continue" -> ok C_CONTINUE (* Deprecated *) - | "Loop.stop" -> ok C_STOP - | "stop" -> ok C_STOP (* Deprecated *) + | "Loop.loop_left" -> ok C_LOOP_LEFT + | "Loop.resume" -> ok C_FOLD_CONTINUE + | "continue" -> ok C_FOLD_CONTINUE (* Deprecated *) + | "Loop.stop" -> ok C_FOLD_STOP + | "stop" -> ok C_FOLD_STOP (* Deprecated *) (* Others *) @@ -484,6 +485,7 @@ module Typer = struct let t_continuation = forall "a" @@ fun a -> tuple2 bool a --> pair bool a let t_fold_while = forall "a" @@ fun a -> tuple2 (a --> pair bool a) a --> a + let t_loop_left = forall2 "a" "b" @@ fun a b -> tuple2 (a --> sum a b) a --> b let t_neg = tuple1 int --> int let t_and = tuple2 bool bool --> bool let t_or = tuple2 bool bool --> bool @@ -515,8 +517,9 @@ module Typer = struct | C_FAILWITH -> ok @@ t_failwith ; (* LOOPS *) | C_FOLD_WHILE -> ok @@ t_fold_while ; - | C_CONTINUE -> ok @@ t_continuation ; - | C_STOP -> ok @@ t_continuation ; + | C_LOOP_LEFT -> ok @@ t_loop_left; + | C_FOLD_CONTINUE -> ok @@ t_continuation ; + | C_FOLD_STOP -> ok @@ t_continuation ; (* MATH *) | C_NEG -> ok @@ t_neg ; | C_ABS -> ok @@ t_abs ; @@ -1018,6 +1021,15 @@ module Typer = struct let%bind () = assert_eq_1 (t_pair (t_bool ()) init ()) result in ok init + let loop_left = typer_2 "LOOP_LEFT" @@ fun _body _init -> + failwith ("should not be used before mini-c") + (* + let%bind (arg, result) = get_t_function body in + let%bind () = assert_eq_1 arg init in + let%bind () = assert_eq_1 arg result in (* Right now, only able to compile when both types are equals *) + ok result + *) + (* Continue and Stop are just syntactic sugar for building a pair (bool * a') *) let continue = typer_1 "CONTINUE" @@ fun arg -> ok @@ t_pair (t_bool ()) arg () @@ -1115,8 +1127,9 @@ module Typer = struct | C_FAILWITH -> ok @@ failwith_ ; (* LOOPS *) | C_FOLD_WHILE -> ok @@ fold_while ; - | C_CONTINUE -> ok @@ continue ; - | C_STOP -> ok @@ stop ; + | C_LOOP_LEFT -> ok @@ loop_left; + | C_FOLD_CONTINUE -> ok @@ continue ; + | C_FOLD_STOP -> ok @@ stop ; (* MATH *) | C_NEG -> ok @@ neg ; | C_ABS -> ok @@ abs ; @@ -1248,8 +1261,8 @@ module Compiler = struct | C_MAP_ADD -> ok @@ simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE] | C_MAP_UPDATE -> ok @@ simple_ternary @@ prim I_UPDATE | C_FOLD_WHILE -> ok @@ simple_binary @@ seq [i_swap ; (i_push (prim T_bool) (prim D_True));prim ~children:[seq [dip i_dup; i_exec; i_unpair]] I_LOOP ;i_swap ; i_drop] - | C_CONTINUE -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_True)); i_pair] - | C_STOP -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_False)); i_pair] + | C_FOLD_CONTINUE -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_True)); i_pair] + | C_FOLD_STOP -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_False)); i_pair] | C_SIZE -> ok @@ simple_unary @@ prim I_SIZE | C_FAILWITH -> ok @@ simple_unary @@ prim I_FAILWITH | C_ASSERT_INFERRED -> ok @@ simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit]) diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml index ee232f044..c3557f3d5 100644 --- a/src/stages/common/PP.ml +++ b/src/stages/common/PP.ml @@ -56,8 +56,11 @@ let constant ppf : constant' -> unit = function | C_ITER -> fprintf ppf "ITER" | C_FOLD -> fprintf ppf "FOLD" | C_FOLD_WHILE -> fprintf ppf "FOLD_WHILE" - | C_CONTINUE -> fprintf ppf "CONTINUE" - | C_STOP -> fprintf ppf "STOP" + | C_FOLD_CONTINUE -> fprintf ppf "CONTINUE" + | C_FOLD_STOP -> fprintf ppf "STOP" + | C_LOOP_LEFT -> fprintf ppf "LOOP_LEFT" + | C_LOOP_CONTINUE -> fprintf ppf "LOOP_CONTINUE" + | C_LOOP_STOP -> fprintf ppf "LOOP_STOP" (* MATH *) | C_NEG -> fprintf ppf "NEG" | C_ABS -> fprintf ppf "ABS" diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml index 1eacb7f7c..20964d3b6 100644 --- a/src/stages/common/types.ml +++ b/src/stages/common/types.ml @@ -197,8 +197,11 @@ and constant' = (* Loops *) | C_ITER | C_FOLD_WHILE - | C_CONTINUE - | C_STOP + | C_FOLD_CONTINUE + | C_FOLD_STOP + | C_LOOP_LEFT + | C_LOOP_CONTINUE + | C_LOOP_STOP | C_FOLD (* MATH *) | C_NEG diff --git a/src/stages/mini_c/PP.ml b/src/stages/mini_c/PP.ml index 7626081cc..dfbbfdd64 100644 --- a/src/stages/mini_c/PP.ml +++ b/src/stages/mini_c/PP.ml @@ -149,8 +149,11 @@ and constant ppf : constant' -> unit = function (* Loops *) | C_FOLD -> fprintf ppf "FOLD" | C_FOLD_WHILE -> fprintf ppf "FOLD_WHILE" - | C_CONTINUE -> fprintf ppf "CONTINUE" - | C_STOP -> fprintf ppf "STOP" + | C_FOLD_CONTINUE -> fprintf ppf "CONTINUE" + | C_FOLD_STOP -> fprintf ppf "STOP" + | C_LOOP_LEFT -> fprintf ppf "LOOP_LEFT" + | C_LOOP_CONTINUE -> fprintf ppf "LOOP_CONTINUE" + | C_LOOP_STOP -> fprintf ppf "LOOP_STOP" | C_ITER -> fprintf ppf "ITER" (* MATH *) | C_NEG -> fprintf ppf "NEG" diff --git a/src/stages/typesystem/shorthands.ml b/src/stages/typesystem/shorthands.ml index 81a341b32..844be70a3 100644 --- a/src/stages/typesystem/shorthands.ml +++ b/src/stages/typesystem/shorthands.ml @@ -48,6 +48,7 @@ let (=>) tc ty = (tc , ty) let (-->) arg ret = P_constant (C_arrow , [arg; ret]) let option t = P_constant (C_option , [t]) let pair a b = P_constant (C_record , [a; b]) +let sum a b = P_constant (C_variant, [a; b]) let map k v = P_constant (C_map , [k; v]) let unit = P_constant (C_unit , []) let list t = P_constant (C_list , [t]) diff --git a/src/test/contracts/recursion.mligo b/src/test/contracts/recursion.mligo index 2b8eb4e1b..13e86518b 100644 --- a/src/test/contracts/recursion.mligo +++ b/src/test/contracts/recursion.mligo @@ -1,5 +1,5 @@ // Test while loops in PascaLIGO -let rec fibo (n : int) (acc: int) : int = +let rec fibo ((n,acc):int * int) : int = if (n < 1) then acc - else fibo (n-1) (acc+n) + else fibo (n-1, acc+n) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 77159d479..66b9bdf05 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -2429,7 +2429,7 @@ let main = test_suite "Integration (End to End)" [ test "failwith mligo" failwith_mligo ; test "assert mligo" assert_mligo ; (* test "recursion (ligo)" recursion_ligo ; *) - (* test "recursion (mligo)" recursion_mligo ; *) + test "recursion (mligo)" recursion_mligo ; test "recursion (religo)" recursion_religo ; (* test "guess string mligo" guess_string_mligo ; WIP? *) test "lambda mligo" lambda_mligo ; diff --git a/test.mligo b/test.mligo new file mode 100644 index 000000000..6ee619aaa --- /dev/null +++ b/test.mligo @@ -0,0 +1,10 @@ +type parameter = int * int + +let rec fibo ((n,acc):int * int) : int = + if (n < 1) then acc + else fibo (n-1, acc+n) + +let main ((p,s):parameter*int) = + let s = fibo (p) in + ([] : operation list),s + diff --git a/vendors/ligo-utils/tezos-utils/x_michelson.ml b/vendors/ligo-utils/tezos-utils/x_michelson.ml index c6af850a3..6bb075cf2 100644 --- a/vendors/ligo-utils/tezos-utils/x_michelson.ml +++ b/vendors/ligo-utils/tezos-utils/x_michelson.ml @@ -78,6 +78,8 @@ let i_dug n : michelson = prim ~children:[Int (0 , Z.of_int n)] I_DUG let i_unpair = seq [i_dup ; i_car ; dip i_cdr] let i_unpiar = seq [i_dup ; i_cdr ; dip i_car] +let i_loop_left body = prim ~children:[seq[body; dip i_drop]] I_LOOP_LEFT + let rec strip_annots : michelson -> michelson = function | Seq(l, s) -> Seq(l, List.map strip_annots s) | Prim (l, p, lst, _) -> Prim (l, p, List.map strip_annots lst, [])