From 2a091edbc0c299c6239476f3f3bdd7a9a02ead1a Mon Sep 17 00:00:00 2001 From: Galfour Date: Mon, 20 May 2019 16:17:26 +0000 Subject: [PATCH 1/3] transpile to mini_c expressions --- src/compiler/compiler_environment.ml | 20 ++- src/compiler/compiler_program.ml | 95 ++++++++---- src/contracts/assign.ligo | 4 + src/contracts/condition-simple.ligo | 8 + src/contracts/declaration-local.ligo | 3 + src/mini_c/PP.ml | 8 +- src/mini_c/combinators.ml | 27 ++-- src/mini_c/types.ml | 4 +- src/test/compiler_tests.ml | 26 +--- src/test/integration_tests.ml | 20 +++ src/test/test_helpers.ml | 2 +- src/transpiler/transpiler.ml | 220 ++++----------------------- 12 files changed, 181 insertions(+), 256 deletions(-) create mode 100644 src/contracts/assign.ligo create mode 100644 src/contracts/condition-simple.ligo create mode 100644 src/contracts/declaration-local.ligo diff --git a/src/compiler/compiler_environment.ml b/src/compiler/compiler_environment.ml index 2ea43b621..05c749095 100644 --- a/src/compiler/compiler_environment.ml +++ b/src/compiler/compiler_environment.ml @@ -135,11 +135,18 @@ let select : environment -> string list -> michelson result = fun e lst -> ok code -let clear : environment -> michelson result = fun e -> select e [] +let select_env : environment -> environment -> michelson result = fun source filter -> + let lst = Environment.get_names filter in + select source lst -let select_env : environment -> environment -> michelson result = fun e e' -> - let lst = Environment.get_names e' in - select e lst +let clear : environment -> (michelson * environment) result = fun e -> + let lst = Environment.get_names e in + let%bind first_name = + trace_option (simple_error "try to clear empty env") @@ + List.nth_opt lst 0 in + let%bind code = select e [ first_name ] in + let e' = Environment.select [ first_name ] e in + ok (code , e') let pack : environment -> michelson result = fun e -> let%bind () = @@ -276,3 +283,8 @@ let add_packed_anon : environment -> type_value -> michelson result = fun e type in ok code + +let pop : environment -> environment result = fun e -> + match e with + | [] -> simple_fail "pop empty env" + | _ :: tl -> ok tl diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 4538bae16..141c7d54c 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -87,6 +87,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m let error_message () = Format.asprintf "\n- expr: %a\n- type: %a\n" PP.expression expr PP.type_ ty in + let i_skip = i_push_unit in let return ?prepend_env ?end_env code = let%bind env' = @@ -123,6 +124,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m trace (error (thunk "compiling expression") error_message) @@ match expr' with + | E_skip -> return @@ i_skip | E_environment_capture c -> let%bind code = Compiler_environment.pack_select env c in return @@ code @@ -130,14 +132,26 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m let%bind (expr' , _) = translate_expression expr env in let%bind clear = Compiler_environment.select env [] in let%bind unpack = Compiler_environment.unpack load_env in - return ~end_env:load_env @@ seq [ + return ~prepend_env:load_env @@ seq [ expr' ; dip clear ; unpack ; + i_skip ; ] | E_environment_select sub_env -> let%bind code = Compiler_environment.select_env env sub_env in - return ~end_env:sub_env code + return ~prepend_env:sub_env @@ seq [ + code ; + i_skip ; + ] + | E_environment_return expr -> ( + let%bind (expr' , env) = translate_expression expr env in + let%bind (code , cleared_env) = Compiler_environment.clear env in + return ~end_env:cleared_env @@ seq [ + expr' ; + code ; + ] + ) | E_literal v -> let%bind v = translate_value v in let%bind t = Compiler_type.type_ ty in @@ -195,11 +209,21 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return code | E_sequence (a , b) -> let%bind (a' , env_a) = translate_expression a env in - let%bind (b' , env_b) = translate_expression b env_a in - return ~prepend_env:env_b @@ seq [ + let%bind env_a' = Compiler_environment.pop env_a in + let%bind (b' , env_b) = translate_expression b env_a' in + return ~end_env:env_b @@ seq [ a' ; + i_drop ; b' ; ] + (* | E_sequence_drop (a , b) -> + * let%bind (a' , env_a) = translate_expression a env in + * let%bind (b' , env_b) = translate_expression b env_a in + * return ~end_env:env_b @@ seq [ + * a' ; + * i_drop ; + * b' ; + * ] *) | E_constant(str, lst) -> let module L = Logger.Stateful() in let%bind lst' = @@ -250,8 +274,9 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return @@ i_none o' | E_if_bool (c, a, b) -> ( let%bind (c' , env') = translate_expression c env in - let%bind (a' , _) = translate_expression a env' in - let%bind (b' , _) = translate_expression b env' in + let%bind popped = Compiler_environment.pop env' in + let%bind (a' , _) = translate_expression a popped in + let%bind (b' , _) = translate_expression b popped in let%bind code = ok (seq [ c' ; i_if a' b' ; @@ -259,16 +284,18 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return code ) | E_if_none (c, n, (ntv , s)) -> ( - let%bind (c' , _env') = translate_expression c env in - let%bind (n' , _) = translate_expression n env in - let s_env = Environment.add ntv env in - let%bind (s' , _) = translate_expression s s_env in - let%bind restrict_s = Compiler_environment.select_env s_env env in + let%bind (c' , env') = translate_expression c env in + let%bind popped = Compiler_environment.pop env' in + let%bind (n' , _) = translate_expression n popped in + let s_env = Environment.add ntv popped in + let%bind (s' , s_env') = translate_expression s s_env in + let%bind popped' = Compiler_environment.pop s_env' in + let%bind restrict_s = Compiler_environment.select_env popped' popped in let%bind code = ok (seq [ c' ; i_if_none n' (seq [ s' ; - restrict_s ; + dip restrict_s ; ]) ; ]) in @@ -298,10 +325,14 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return code ) | E_let_in (v, expr , body) -> ( - let%bind (expr' , _) = translate_expression expr env in - let env' = Environment.add v env in - let%bind (body' , _) = translate_expression body env' in - let%bind restrict = Compiler_environment.select_env env' env in + let%bind (expr' , expr_env) = translate_expression expr env in + let%bind env' = + let%bind popped = Compiler_environment.pop expr_env in + ok @@ Environment.add v popped in + let%bind (body' , body_env) = translate_expression body env' in + let%bind restrict = + let%bind popped = Compiler_environment.pop body_env in + Compiler_environment.select_env popped env in let%bind code = ok (seq [ expr' ; body' ; @@ -312,6 +343,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m ) | E_assignment (name , lrs , expr) -> ( let%bind (expr' , env') = translate_expression expr env in + (* Format.printf "\nass env':%a\n" PP.environment env' ; *) let%bind get_code = Compiler_environment.get env' name in let modify_code = let aux acc step = match step with @@ -333,23 +365,33 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m in error title content in trace error @@ - return ~end_env:env @@ seq [ + return ~prepend_env:env @@ seq [ + i_comment "assign: start # env" ; expr' ; + i_comment "assign: compute rhs # rhs : env" ; get_code ; - i_swap ; modify_code ; + i_comment "assign: get name # name : rhs : env" ; + i_swap ; + i_comment "assign: swap # rhs : name : env" ; + modify_code ; + i_comment "assign: modify code # name+rhs : env" ; set_code ; + i_comment "assign: set new # new_env" ; + i_skip ; ] ) | E_while (expr, block) -> ( let%bind (expr' , env') = translate_expression expr env in - let%bind (block' , env'') = translate_expression block env' in - let%bind restrict_block = Compiler_environment.select_env env'' env' in + let%bind popped = Compiler_environment.pop env' in + let%bind (block' , env'') = translate_expression block popped in + let%bind restrict_block = Compiler_environment.select_env env'' popped in return @@ seq [ expr' ; prim ~children:[seq [ block' ; restrict_block ; expr']] I_LOOP ; + i_skip ; ] ) @@ -528,16 +570,12 @@ and translate_regular_block ((b, env):block) : michelson result = let code = seq (List.rev codes) in ok code -and translate_quote_body ({body;result} as f:anon_function) : michelson result = - let%bind body' = translate_regular_block body in - let%bind (expr , _) = translate_expression result (snd body).post_environment in - let%bind restrict = Compiler_environment.clear (snd body).post_environment in +and translate_quote_body ({result ; binder ; input} as f:anon_function) : michelson result = + let env = Environment.(add (binder , input) empty) in + let%bind (expr , _) = translate_expression result env in let code = seq [ - i_comment "function body" ; - body' ; i_comment "function result" ; expr ; - dip restrict ; ] in let%bind _assert_type = @@ -547,11 +585,10 @@ and translate_quote_body ({body;result} as f:anon_function) : michelson result = let output_stack_ty = Stack.(output_ty @: nil) in let error_message () = Format.asprintf - "\ncode : %a\ninput : %a\noutput : %a\nenv : %a\n" + "\ncode : %a\ninput : %a\noutput : %a\n" Michelson.pp code PP.type_ f.input PP.type_ f.output - PP.environment (snd body).post_environment in let%bind _ = Trace.trace_tzresult_lwt ( diff --git a/src/contracts/assign.ligo b/src/contracts/assign.ligo new file mode 100644 index 000000000..d882d0e40 --- /dev/null +++ b/src/contracts/assign.ligo @@ -0,0 +1,4 @@ +function main (const i : int) : int is + begin + i := i + 1 ; + end with i diff --git a/src/contracts/condition-simple.ligo b/src/contracts/condition-simple.ligo new file mode 100644 index 000000000..708d4c6b5 --- /dev/null +++ b/src/contracts/condition-simple.ligo @@ -0,0 +1,8 @@ +function main (const i : int) : int is + begin + if 1 = 1 then + i := 42 + else + i := 0 + end with i + diff --git a/src/contracts/declaration-local.ligo b/src/contracts/declaration-local.ligo new file mode 100644 index 000000000..94d443b32 --- /dev/null +++ b/src/contracts/declaration-local.ligo @@ -0,0 +1,3 @@ +function main (const i : int) : int is block { + const j : int = 42 ; +} with j diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml index 6209a624a..972707548 100644 --- a/src/mini_c/PP.ml +++ b/src/mini_c/PP.ml @@ -64,6 +64,8 @@ and expression' ppf (e:expression') = match e with | E_environment_capture s -> fprintf ppf "capture(%a)" (list_sep string (const " ; ")) s | E_environment_load (expr , env) -> fprintf ppf "load %a in %a" expression expr environment env | E_environment_select env -> fprintf ppf "select %a" environment env + | E_environment_return expr -> fprintf ppf "return %a" expression expr + | E_skip -> fprintf ppf "skip" | E_variable v -> fprintf ppf "%s" v | E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b | E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst @@ -76,6 +78,7 @@ and expression' ppf (e:expression') = match e with | E_if_left (c, ((name_l, _) , l), ((name_r, _) , r)) -> fprintf ppf "%a ?? %s -> %a : %s -> %a" expression c name_l expression l name_r expression r | E_sequence (a , b) -> fprintf ppf "%a ; %a" expression a expression b + (* | E_sequence_drop (a , b) -> fprintf ppf "%a ;- %a" expression a expression b *) | E_let_in ((name , _) , expr , body) -> fprintf ppf "let %s = %a in %a" name expression expr expression body | E_assignment (r , path , e) -> @@ -91,12 +94,11 @@ and expression_with_type : _ -> expression -> _ = fun ppf e -> expression' e.content type_ e.type_value -and function_ ppf ({binder ; input ; output ; body ; result}:anon_function) = - fprintf ppf "fun (%s:%a) : %a %a return %a" +and function_ ppf ({binder ; input ; output ; result}:anon_function) = + fprintf ppf "fun (%s:%a) : %a return %a" binder type_ input type_ output - block body expression result and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e diff --git a/src/mini_c/combinators.ml b/src/mini_c/combinators.ml index 608b59648..d4528b24e 100644 --- a/src/mini_c/combinators.ml +++ b/src/mini_c/combinators.ml @@ -136,25 +136,34 @@ let t_deep_closure x y z : type_value = T_deep_closure ( x , y , z ) let t_pair x y : type_value = T_pair ( x , y ) let t_union x y : type_value = T_or ( x , y ) -let quote binder input output body result : anon_function = +let quote binder input output result : anon_function = { binder ; input ; output ; - body ; result ; + result ; } -let basic_quote i o b : anon_function result = - let%bind (_, _e) = get_last_statement b in - let r : expression = Expression.make_tpl (E_variable "output", o) in - ok @@ quote "input" i o b r - -let basic_int_quote b : anon_function result = - basic_quote t_int t_int b let e_int expr : expression = Expression.make_tpl (expr, t_int) let e_unit : expression = Expression.make_tpl (E_literal D_unit, t_unit) +let e_skip : expression = Expression.make_tpl (E_skip, t_unit) let e_var_int name : expression = e_int (E_variable name) +let e_let_int v tv expr body : expression = Expression.(make_tpl ( + E_let_in ((v , tv) , expr , body) , + get_type body + )) + +let ez_e_sequence a b : expression = Expression.(make_tpl (E_sequence (make_tpl (a , t_unit) , b) , get_type b)) + +let ez_e_return e : expression = Expression.(make_tpl ((E_environment_return e) , get_type e)) let d_unit : value = D_unit +let basic_quote i o expr : anon_function result = + ok @@ quote "input" i o (ez_e_return expr) + +let basic_int_quote expr : anon_function result = + basic_quote t_int t_int expr + + let environment_wrap pre_environment post_environment = { pre_environment ; post_environment } let id_environment_wrap e = environment_wrap e e diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml index 456770d23..b3f33be6b 100644 --- a/src/mini_c/types.ml +++ b/src/mini_c/types.ml @@ -56,6 +56,8 @@ and expression' = | E_environment_capture of selector | E_environment_select of environment | E_environment_load of (expression * environment) + | E_environment_return of expression + | E_skip | E_constant of string * expression list | E_application of expression * expression | E_variable of var_name @@ -67,6 +69,7 @@ and expression' = | E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression) | E_let_in of ((var_name * type_value) * expression * expression) | E_sequence of (expression * expression) + (* | E_sequence_drop of (expression * expression) *) | E_assignment of (string * [`Left | `Right] list * expression) | E_while of expression * expression @@ -98,7 +101,6 @@ and anon_function = { binder : string ; input : type_value ; output : type_value ; - body : block ; result : expression ; } diff --git a/src/test/compiler_tests.ml b/src/test/compiler_tests.ml index a6db44def..2424d0cd4 100644 --- a/src/test/compiler_tests.ml +++ b/src/test/compiler_tests.ml @@ -11,29 +11,19 @@ let run_entry_int (e:anon_function) (n:int) : int result = | _ -> simple_fail "result is not an int" let identity () : unit result = - let e = basic_int_quote_env in - let s = statement (S_declaration ("output", e_var_int "input")) e in - let%bind b = block [s] in - let%bind f = basic_int_quote b in + let%bind f = basic_int_quote (e_var_int "input") in let%bind result = run_entry_int f 42 in let%bind _ = Assert.assert_equal_int ~msg:__LOC__ 42 result in ok () let multiple_vars () : unit result = - let e = basic_int_quote_env in - (* - Statements can change the environment, and you don't want to pass the new environment manually. - [statements] deals with this and this is why those statements are parametrized over an environment. - Yes. One could do a monad. Feel free when we have the time. - *) - let ss = statements [ - (fun e -> statement (S_declaration ("a", e_var_int "input")) e) ; - (fun e -> statement (S_declaration ("b", e_var_int "input")) e) ; - (fun e -> statement (S_declaration ("c", e_var_int "a")) e) ; - (fun e -> statement (S_declaration ("output", e_var_int "c")) e) ; - ] e in - let%bind b = block ss in - let%bind f = basic_int_quote b in + let expr = + e_let_int "a" t_int (e_var_int "input") @@ + e_let_int "b" t_int (e_var_int "input") @@ + e_let_int "c" t_int (e_var_int "a") @@ + e_let_int "output" t_int (e_var_int "c") @@ + e_var_int "output" in + let%bind f = basic_int_quote expr in let%bind result = run_entry_int f 42 in let%bind _ = Assert.assert_equal_int ~msg:__LOC__ 42 result in ok () diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 5291a0119..5241f83a9 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -15,6 +15,11 @@ let function_ () : unit result = let make_expect = fun n -> n in expect_eq_n_int program "main" make_expect +let assign () : unit result = + let%bind program = type_file "./contracts/assign.ligo" in + let make_expect = fun n -> n + 1 in + expect_eq_n_int program "main" make_expect + let annotation () : unit result = let%bind program = type_file "./contracts/annotation.ligo" in let%bind () = @@ -311,6 +316,12 @@ let condition () : unit result = let make_expected = fun n -> e_a_int (if n = 2 then 42 else 0) in expect_eq_n program "main" make_input make_expected +let condition_simple () : unit result = + let%bind program = type_file "./contracts/condition-simple.ligo" in + let make_input = e_a_int in + let make_expected = fun _ -> e_a_int 42 in + expect_eq_n program "main" make_input make_expected + let loop () : unit result = let%bind program = type_file "./contracts/loop.ligo" in let%bind () = @@ -379,6 +390,12 @@ let declarations () : unit result = let make_expected = fun n -> e_a_int (42 + n) in expect_eq_n program "main" make_input make_expected +let declaration_local () : unit result = + let%bind program = type_file "./contracts/declaration-local.ligo" in + let make_input = e_a_int in + let make_expected = fun _ -> e_a_int 42 in + expect_eq_n program "main" make_input make_expected + let quote_declaration () : unit result = let%bind program = type_file "./contracts/quote-declaration.ligo" in let make_input = e_a_int in @@ -436,11 +453,14 @@ let guess_the_hash_mligo () : unit result = let main = "Integration (End to End)", [ test "function" function_ ; + test "assign" assign ; + test "declaration local" declaration_local ; test "complex function" complex_function ; test "variant" variant ; test "variant matching" variant_matching ; test "tuple" tuple ; test "record" record ; + test "condition simple" condition_simple ; test "condition" condition ; test "shadow" shadow ; test "annotation" annotation ; diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index e24e8ac48..b22d8a034 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -20,7 +20,7 @@ let expect ?options program entry_point input expecter = let content () = Format.asprintf "Entry_point: %s" entry_point in error title content in trace run_error @@ - Ligo.easy_run_typed_simplified ~debug_michelson:false ?options entry_point program input in + Ligo.easy_run_typed_simplified ~debug_michelson:true ?options entry_point program input in expecter result let expect_eq ?options program entry_point input expected = diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index 563ac59be..c21726105 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -119,107 +119,17 @@ let record_access_to_lr : type_value -> type_value AST.type_name_map -> string - bind_fold_list aux (ty , []) lr_path in ok lst -(* let rec translate_block env (b:AST.block) : block result = - * let aux = fun (precs, env) instruction -> - * let%bind lst = translate_instruction env instruction in - * let env' = List.fold_left (fun _ i -> (snd i).post_environment) env lst in (\* Get last environment *\) - * ok (precs @ lst, env') in - * let%bind (instructions, env') = bind_fold_list aux ([], env) b in - * ok (instructions, environment_wrap env env') - * - * and translate_instruction (env:Environment.t) (i:AST.instruction) : statement list result = - * let return ?(env' = env) x : statement list result = ok ([x, environment_wrap env env']) in - * match i with - * | I_declaration {name;annotated_expression} -> - * let%bind expression = translate_annotated_expression annotated_expression in - * let env' = Environment.add (name, (Combinators.Expression.get_type expression)) env in - * return ~env' (S_declaration (name, expression)) - * | I_assignment {name;annotated_expression} -> - * let%bind expression = translate_annotated_expression annotated_expression in - * return (S_assignment (name, expression)) - * | I_patch (r, s, v) -> ( - * let ty = r.type_value in - * let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result = - * fun (prev, acc) cur -> - * let%bind ty' = translate_type prev in - * match cur with - * | Access_tuple ind -> - * let%bind ty_lst = AST.Combinators.get_t_tuple prev in - * let%bind ty'_lst = bind_map_list translate_type ty_lst in - * let%bind path = tuple_access_to_lr ty' ty'_lst ind in - * let path' = List.map snd path in - * ok (List.nth ty_lst ind, acc @ path') - * | Access_record prop -> - * let%bind ty_map = - * let error = - * let title () = "accessing property on not a record" in - * let content () = Format.asprintf "%s on %a in %a" - * prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in - * error title content - * in - * trace error @@ - * AST.Combinators.get_t_record prev in - * let%bind ty'_map = bind_map_smap translate_type ty_map in - * let%bind path = record_access_to_lr ty' ty'_map prop in - * let path' = List.map snd path in - * ok (Map.String.find prop ty_map, acc @ path') - * | Access_map _k -> simple_fail "no patch for map yet" - * in - * let%bind (_, path) = bind_fold_right_list aux (ty, []) s in - * let%bind v' = translate_annotated_expression v in - * return (S_patch (r.type_name, path, v')) - * ) - * | I_matching (expr, m) -> ( - * let%bind expr' = translate_annotated_expression expr in - * let env' = env in - * let return s = - * ok [ (s, environment_wrap env env) ] in - * match m with - * | Match_bool {match_true ; match_false} -> ( - * let%bind true_branch = translate_block env' match_true in - * let%bind false_branch = translate_block env' match_false in - * return @@ S_cond (expr', true_branch, false_branch) - * ) - * | Match_option {match_none ; match_some = ((name, t), sm)} -> ( - * let%bind none_branch = translate_block env' match_none in - * let%bind t' = translate_type t in - * let%bind some_branch = - * let env'' = Environment.add (name, t') env' in - * translate_block env'' sm - * in - * return @@ S_if_none (expr', none_branch, ((name, t'), some_branch)) - * ) - * | _ -> simple_fail "todo : match" - * ) - * | I_loop (expr, body) -> - * let%bind expr' = translate_annotated_expression expr in - * let%bind body' = translate_block env body in - * return (S_while (expr', body')) - * | I_skip -> ok [] - * | I_do ae -> ( - * let%bind ae' = translate_annotated_expression ae in - * return @@ S_do ae' - * ) *) - -let rec translate_block env (b:AST.block) : block result = - let aux = fun (precs, env) instruction -> - let%bind lst = translate_instruction env instruction in - let env' = List.fold_left (fun _ i -> (snd i).post_environment) env lst in (* Get last environment *) - ok (precs @ lst, env') in - let%bind (instructions, env') = bind_fold_list aux ([], env) b in - ok (instructions, environment_wrap env env') - -and translate_block' : expression option -> AST.block -> expression result = fun expr_opt block -> +let rec translate_block : expression option -> AST.block -> expression result = fun expr_opt block -> let aux = fun expr_opt i -> - let%bind expr = translate_instruction' i expr_opt in + let%bind expr = translate_instruction i expr_opt in ok (Some expr) in let%bind expr_opt = bind_fold_right_list aux expr_opt block in let default = e_unit in ok (Option.unopt ~default expr_opt) -and translate_instruction' : AST.instruction -> expression option -> expression result = fun i expr_opt -> +and translate_instruction : AST.instruction -> expression option -> expression result = fun i expr_opt -> let expr = - let default = e_unit in + let default = e_skip in Option.unopt ~default expr_opt in let return ?(tv = expr.type_value) expr' = ok @@ Combinators.Expression.make_tpl (expr' , tv) in let skip = ok expr in @@ -227,6 +137,11 @@ and translate_instruction' : AST.instruction -> expression option -> expression let lhs = Expression.make_tpl (expr' , t_unit) in let rhs = expr in ok @@ Combinators.Expression.make_tpl (E_sequence ( lhs , rhs ) , tv) in + let return_seq_drop ?(tv = expr.type_value) expr' = + let lhs = Expression.make_tpl (expr' , t_unit) in + let rhs = expr in + (* ok @@ Combinators.Expression.make_tpl (E_sequence_drop ( lhs , rhs ) , tv) in *) + ok @@ Combinators.Expression.make_tpl (E_sequence ( lhs , rhs ) , tv) in match i with | I_declaration { name ; annotated_expression } -> let%bind rhs = translate_annotated_expression annotated_expression in @@ -238,15 +153,15 @@ and translate_instruction' : AST.instruction -> expression option -> expression let%bind expr' = translate_annotated_expression matched in match clauses with | Match_bool {match_true ; match_false} -> - let%bind (t , f) = bind_map_pair (translate_block' None) (match_true, match_false) in - return_seq @@ E_if_bool (expr', t, f) + let%bind (t , f) = bind_map_pair (translate_block None) (match_true, match_false) in + return_seq_drop @@ E_if_bool (expr', t, f) | Match_option { match_none; match_some = ((name, tv), s) } -> - let%bind n = translate_block' None match_none in + let%bind n = translate_block None match_none in let%bind (tv' , s') = let%bind tv' = translate_type tv in - let%bind s' = translate_block' None s in + let%bind s' = translate_block None s in ok (tv' , s') in - return_seq @@ E_if_none (expr' , n , ((name , tv') , s')) + return_seq_drop @@ E_if_none (expr' , n , ((name , tv') , s')) | Match_variant (lst , variant) -> ( let%bind tree = tree_of_sum variant in let%bind tree' = match tree with @@ -272,7 +187,7 @@ and translate_instruction' : AST.instruction -> expression option -> expression let%bind ((_ , name) , body) = trace_option (simple_error "not supposed to happen here: missing match clause") @@ List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in - let%bind body' = translate_block' None body in + let%bind body' = translate_block None body in return @@ E_let_in ((name , tv) , top , body') ) | ((`Node (a , b)) , tv) -> @@ -288,7 +203,7 @@ and translate_instruction' : AST.instruction -> expression option -> expression let%bind e = aux (((Expression.make (E_variable "right") b_ty))) b in ok (b_var , e) in - return @@ E_if_left (top , a' , b') + return_seq_drop @@ E_if_left (top , a' , b') in aux expr' tree'' ) @@ -297,7 +212,7 @@ and translate_instruction' : AST.instruction -> expression option -> expression ) | I_loop (condition , body) -> let%bind condition' = translate_annotated_expression condition in - let%bind body' = translate_block' None body in + let%bind body' = translate_block None body in return_seq @@ E_while (condition' , body') | I_do action -> let%bind action' = translate_annotated_expression action in @@ -336,80 +251,6 @@ and translate_instruction' : AST.instruction -> expression option -> expression return_seq (E_assignment (typed_name.type_name, path, expr')) ) -and translate_instruction (env:Environment.t) (i:AST.instruction) : statement list result = - let return ?(env' = env) x : statement list result = ok ([x, environment_wrap env env']) in - match i with - | I_declaration {name;annotated_expression} -> - let%bind expression = translate_annotated_expression annotated_expression in - let env' = Environment.add (name, (Combinators.Expression.get_type expression)) env in - return ~env' (S_declaration (name, expression)) - | I_assignment {name;annotated_expression} -> - let%bind expression = translate_annotated_expression annotated_expression in - return (S_assignment (name, expression)) - | I_patch (r, s, v) -> ( - let ty = r.type_value in - let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result = - fun (prev, acc) cur -> - let%bind ty' = translate_type prev in - match cur with - | Access_tuple ind -> - let%bind ty_lst = AST.Combinators.get_t_tuple prev in - let%bind ty'_lst = bind_map_list translate_type ty_lst in - let%bind path = tuple_access_to_lr ty' ty'_lst ind in - let path' = List.map snd path in - ok (List.nth ty_lst ind, acc @ path') - | Access_record prop -> - let%bind ty_map = - let error = - let title () = "accessing property on not a record" in - let content () = Format.asprintf "%s on %a in %a" - prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in - error title content - in - trace error @@ - AST.Combinators.get_t_record prev in - let%bind ty'_map = bind_map_smap translate_type ty_map in - let%bind path = record_access_to_lr ty' ty'_map prop in - let path' = List.map snd path in - ok (Map.String.find prop ty_map, acc @ path') - | Access_map _k -> simple_fail "no patch for map yet" - in - let%bind (_, path) = bind_fold_right_list aux (ty, []) s in - let%bind v' = translate_annotated_expression v in - return (S_patch (r.type_name, path, v')) - ) - | I_matching (expr, m) -> ( - let%bind expr' = translate_annotated_expression expr in - let env' = env in - let return s = - ok [ (s, environment_wrap env env) ] in - match m with - | Match_bool {match_true ; match_false} -> ( - let%bind true_branch = translate_block env' match_true in - let%bind false_branch = translate_block env' match_false in - return @@ S_cond (expr', true_branch, false_branch) - ) - | Match_option {match_none ; match_some = ((name, t), sm)} -> ( - let%bind none_branch = translate_block env' match_none in - let%bind t' = translate_type t in - let%bind some_branch = - let env'' = Environment.add (name, t') env' in - translate_block env'' sm - in - return @@ S_if_none (expr', none_branch, ((name, t'), some_branch)) - ) - | _ -> simple_fail "todo : match" - ) - | I_loop (expr, body) -> - let%bind expr' = translate_annotated_expression expr in - let%bind body' = translate_block env body in - return (S_while (expr', body')) - | I_skip -> ok [] - | I_do ae -> ( - let%bind ae' = translate_annotated_expression ae in - return @@ S_do ae' - ) - and translate_literal : AST.literal -> value = fun l -> match l with | Literal_bool b -> D_bool b | Literal_int n -> D_int n @@ -701,17 +542,16 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express let init_env = Environment.(add (binder , raw_input) c_env) in let input = Environment.closure_representation init_env in let%bind output = translate_type output_type in - let%bind (statements , body_env) = translate_block init_env body in - let body = - let load_env = Environment.(add ("closure_arg" , input) empty) in - let load_expr = Expression.make_tpl (E_variable "closure_arg" , input) in - let load_st = Mini_c.statement (S_environment_load (load_expr , init_env)) load_env in - let statements' = load_st :: statements in - (statements' , body_env) - in - let%bind result = translate_annotated_expression result in + let%bind result = + let%bind result_expression = translate_annotated_expression result in + let%bind body_expression = translate_block (Some result_expression) body in + let%bind body_wrap_expression = + let load_expr = Expression.make_tpl (E_variable binder , input) in + ok @@ ez_e_return @@ ez_e_sequence (E_environment_load (load_expr , init_env)) body_expression + in + ok body_wrap_expression in let tv = Mini_c.t_function input output in - let f_literal = D_function { binder ; input ; output ; body ; result } in + let f_literal = D_function { binder ; input ; output ; result } in let expr = Expression.make_tpl (E_literal f_literal , tv) in ok (expr , raw_input , output) in let%bind c_expr = @@ -731,16 +571,14 @@ and translate_lambda env l = let%bind result = match (body_fvs, result_fvs) with | [] , [] -> ( - let%bind empty_env = - let%bind input = translate_type input_type in - ok Environment.(add (binder, input) empty) in - let%bind body' = translate_block empty_env body in let%bind result' = translate_annotated_expression result in + let%bind body_expression = translate_block (Some result') body in + let body_wrapped = ez_e_return body_expression in trace (simple_error "translate quote") @@ let%bind input = translate_type input_type in let%bind output = translate_type output_type in let tv = Combinators.t_function input output in - let content = D_function {binder;input;output;body=body';result=result'} in + let content = D_function {binder;input;output;result=body_wrapped} in ok @@ Combinators.Expression.make_tpl (E_literal content, tv) ) | _ -> ( From 46d07c55ead9e7d4771a88421ed9a46eefb05d37 Mon Sep 17 00:00:00 2001 From: Galfour Date: Mon, 20 May 2019 16:26:55 +0000 Subject: [PATCH 2/3] remove statements from mini_c --- src/compiler/compiler_program.ml | 175 ------------------------------- src/mini_c/PP.ml | 18 ---- src/mini_c/combinators.ml | 6 -- src/mini_c/combinators_smart.ml | 46 -------- src/mini_c/types.ml | 18 ---- 5 files changed, 263 deletions(-) diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 141c7d54c..077e8f92f 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -395,181 +395,6 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m ] ) -and translate_statement ((s', w_env) as s:statement) : michelson result = - let error_message () = Format.asprintf "%a" PP.statement s in - let return code = - let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment w_env.pre_environment in - let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment w_env.post_environment in - let error_message () = - let%bind pre_env_michelson = Compiler_type.environment w_env.pre_environment in - let%bind post_env_michelson = Compiler_type.environment w_env.post_environment in - ok @@ Format.asprintf - "statement : %a\ncode : %a\npre type : %a\npost type : %a\n" - PP.statement s - Michelson.pp code - PP_helpers.(list_sep Michelson.pp (const " ; ")) pre_env_michelson - PP_helpers.(list_sep Michelson.pp (const " ; ")) post_env_michelson - in - let%bind _ = - Trace.trace_tzresult_lwt_r (fun () -> let%bind error_message = error_message () in - ok (fun () -> error (thunk "error parsing statement code") - (fun () -> error_message) - ())) @@ - Proto_alpha_utils.Memory_proto_alpha.parse_michelson_fail code - input_stack_ty output_stack_ty - in - ok code - in - - trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with - | S_environment_add _ -> - simple_fail "add not ready yet" - | S_environment_select sub_env -> - let%bind code = Compiler_environment.select_env w_env.pre_environment sub_env in - return code - | S_environment_load (expr , env) -> - let%bind (expr' , _) = translate_expression expr w_env.pre_environment in - let%bind clear = Compiler_environment.select w_env.pre_environment [] in - let%bind unpack = Compiler_environment.unpack env in - return @@ seq [ - expr' ; - dip clear ; - unpack ; - ] - | S_declaration (s, expr) -> - let tv = Combinators.Expression.get_type expr in - let%bind (expr , _) = translate_expression expr w_env.pre_environment in - let%bind add = Compiler_environment.add w_env.pre_environment (s, tv) in - return @@ seq [ - i_comment "declaration" ; - seq [ - i_comment "expr" ; - expr ; - ] ; - seq [ - i_comment "env <- env . expr" ; - add ; - ]; - ] - | S_assignment (s, expr) -> - let%bind (expr , _) = translate_expression expr w_env.pre_environment in - let%bind set = Compiler_environment.set w_env.pre_environment s in - return @@ seq [ - i_comment "assignment" ; - seq [ - i_comment "expr" ; - expr ; - ] ; - seq [ - i_comment "env <- env . expr" ; - set ; - ]; - ] - | S_cond (expr, a, b) -> - let%bind (expr , _) = translate_expression expr w_env.pre_environment in - let%bind a' = translate_regular_block a in - let%bind b' = translate_regular_block b in - return @@ seq [ - expr ; - prim ~children:[seq [a'];seq [b']] I_IF ; - ] - | S_do expr -> ( - match Combinators.Expression.get_content expr with - | E_constant ("FAILWITH" , [ fw ] ) -> ( - let%bind (fw' , _) = translate_expression fw w_env.pre_environment in - return @@ seq [ - fw' ; - i_failwith ; - ] - ) - | _ -> ( - let%bind (expr' , _) = translate_expression expr w_env.pre_environment in - return @@ seq [ - expr' ; - i_drop ; - ] - ) - ) - | S_if_none (expr, none, ((name, tv), some)) -> - let%bind (expr , _) = translate_expression expr w_env.pre_environment in - let%bind none' = translate_regular_block none in - let%bind some' = translate_regular_block some in - let%bind add = - let env' = w_env.pre_environment in - Compiler_environment.add env' (name, tv) in - let%bind restrict_s = Compiler_environment.select_env (snd some).post_environment w_env.pre_environment in - return @@ seq [ - expr ; - prim ~children:[ - seq [none'] ; - seq [add ; some' ; restrict_s] ; - ] I_IF_NONE - ] - | S_while (expr, block) -> - let%bind (expr , _) = translate_expression expr w_env.pre_environment in - let%bind block' = translate_regular_block block in - let%bind restrict_block = - let env_while = (snd block).pre_environment in - Compiler_environment.select_env (snd block).post_environment env_while in - return @@ seq [ - expr ; - prim ~children:[seq [ - block' ; - restrict_block ; - expr]] I_LOOP ; - ] - | S_patch (name, lrs, expr) -> - let%bind (expr' , env') = translate_expression expr w_env.pre_environment in - let%bind get_code = Compiler_environment.get env' name in - let modify_code = - let aux acc step = match step with - | `Left -> seq [dip i_unpair ; acc ; i_pair] - | `Right -> seq [dip i_unpiar ; acc ; i_piar] - in - let init = dip i_drop in - List.fold_right' aux init lrs - in - let%bind set_code = Compiler_environment.set w_env.pre_environment name in - let error = - let title () = "michelson type-checking patch" in - let content () = - let aux ppf = function - | `Left -> Format.fprintf ppf "left" - | `Right -> Format.fprintf ppf "right" in - Format.asprintf "Sub path: %a\n" - PP_helpers.(list_sep aux (const " , ")) lrs - in - error title content in - trace error @@ - return @@ seq [ - expr' ; - get_code ; - i_swap ; modify_code ; - set_code ; - ] - -and translate_regular_block ((b, env):block) : michelson result = - let aux prev statement = - let%bind (lst : michelson list) = prev in - let%bind instruction = translate_statement statement in - ok (instruction :: lst) - in - let%bind codes = - let error_message () = - let%bind schema_michelsons = Compiler_type.environment env.pre_environment in - ok @@ Format.asprintf "\nblock : %a\nschema : %a\n" - PP.block (b, env) - PP_helpers.(list_sep Michelson.pp (const " ; ")) schema_michelsons - in - trace_r (fun () -> - let%bind error_message = error_message () in - ok (fun () -> error (thunk "compiling regular block") - (fun () -> error_message) - ())) @@ - List.fold_left aux (ok []) b in - let code = seq (List.rev codes) in - ok code - and translate_quote_body ({result ; binder ; input} as f:anon_function) : michelson result = let env = Environment.(add (binder , input) empty) in let%bind (expr , _) = translate_expression result env in diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml index 972707548..a7fb12d6c 100644 --- a/src/mini_c/PP.ml +++ b/src/mini_c/PP.ml @@ -105,24 +105,6 @@ and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e -and statement ppf ((s, _) : statement) = match s with - | S_environment_load _ -> fprintf ppf "load env" - | S_environment_select _ -> fprintf ppf "select env" - | S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv - | S_declaration ass -> declaration ppf ass - | S_assignment ass -> assignment ppf ass - | S_do e -> fprintf ppf "do %a" expression e - | S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e - | S_patch (r, path, e) -> - fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e - | S_if_none (expr, none, ((name, _), some)) -> fprintf ppf "if_none (%a) %a %s->%a" expression expr block none name block some - | S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b - -and block ppf ((b, _):block) = - match b with - | [] -> fprintf ppf "{}" - | b -> fprintf ppf "{@; @[%a@]@;}" (pp_print_list ~pp_sep:(tag "@;") statement) b - let tl_statement ppf (ass, _) = assignment ppf ass let program ppf (p:program) = diff --git a/src/mini_c/combinators.ml b/src/mini_c/combinators.ml index d4528b24e..670d63e5f 100644 --- a/src/mini_c/combinators.ml +++ b/src/mini_c/combinators.ml @@ -121,12 +121,6 @@ let get_operation (v:value) = match v with | _ -> simple_fail "not an operation" -let get_last_statement ((b', _):block) : statement result = - let aux lst = match lst with - | [] -> simple_fail "get_last: empty list" - | lst -> ok List.(nth lst (length lst - 1)) in - aux b' - let t_int : type_value = T_base Base_int let t_unit : type_value = T_base Base_unit let t_nat : type_value = T_base Base_nat diff --git a/src/mini_c/combinators_smart.ml b/src/mini_c/combinators_smart.ml index 4e0126f35..6cffd7226 100644 --- a/src/mini_c/combinators_smart.ml +++ b/src/mini_c/combinators_smart.ml @@ -1,52 +1,6 @@ -open Trace open Types open Combinators let basic_int_quote_env : environment = let e = Environment.empty in Environment.add ("input", t_int) e - -let statement s' env : statement = - match s' with - | S_environment_load (_ , env') -> s', environment_wrap env env' - | S_environment_select env' -> s', environment_wrap env env' - | S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env) - | S_cond _ -> s' , id_environment_wrap env - | S_do _ -> s' , id_environment_wrap env - | S_if_none _ -> s' , id_environment_wrap env - | S_while _ -> s' , id_environment_wrap env - | S_patch _ -> s' , id_environment_wrap env - | S_declaration (name , e) -> s', environment_wrap env (Environment.add (name , (Expression.get_type e)) env) - | S_assignment (name , e) -> s', environment_wrap env (Environment.add (name , (Expression.get_type e)) env) - -let block (statements:statement list) : block result = - match statements with - | [] -> simple_fail "no statements in block" - | lst -> - let first = List.hd lst in - let last = List.(nth lst (length lst - 1)) in - ok (lst, environment_wrap (snd first).pre_environment (snd last).post_environment) - -let append_statement' : block -> statement' -> block = fun b s' -> - let b_wrap = snd b in - let s = statement s' b_wrap.post_environment in - let s_wrap = snd s in - let b_wrap' = { b_wrap with post_environment = s_wrap.post_environment } in - let b_content = fst b in - (b_content @ [s], b_wrap') - -let prepend_statement : statement -> block -> block = fun s b -> - let s_wrap = snd s in - let b_wrap = snd b in - let b_wrap' = { b_wrap with pre_environment = s_wrap.pre_environment } in - let b_content = fst b in - (s :: b_content, b_wrap') - -let statements (lst:(environment -> statement) list) e : statement list = - let rec aux lst e = match lst with - | [] -> [] - | hd :: tl -> - let s = hd e in - s :: aux tl (snd s).post_environment - in - aux lst e diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml index b3f33be6b..ca445ee0e 100644 --- a/src/mini_c/types.ml +++ b/src/mini_c/types.ml @@ -81,20 +81,6 @@ and expression = { and assignment = var_name * expression -and statement' = - | S_environment_select of environment - | S_environment_load of (expression * environment) - | S_environment_add of (var_name * type_value) - | S_declaration of assignment (* First assignment *) - | S_assignment of assignment - | S_do of expression - | S_cond of expression * block * block - | S_patch of string * [`Left | `Right] list * expression - | S_if_none of expression * block * ((var_name * type_value) * block) - | S_while of expression * block - -and statement = statement' * environment_wrap - and toplevel_statement = assignment * environment_wrap and anon_function = { @@ -104,8 +90,4 @@ and anon_function = { result : expression ; } -and block' = statement list - -and block = block' * environment_wrap - and program = toplevel_statement list From 9d873c382b90e2c298746a9ab4823661f0b7442b Mon Sep 17 00:00:00 2001 From: Galfour Date: Wed, 22 May 2019 00:46:54 +0000 Subject: [PATCH 3/3] remove statements from everywhere (very atomic commit) --- src/ast_simplified/PP.ml | 22 +-- src/ast_simplified/combinators.ml | 20 ++- src/ast_simplified/types.ml | 24 +--- src/ast_typed/PP.ml | 23 +--- src/ast_typed/combinators.ml | 4 +- src/ast_typed/environment.ml | 8 ++ src/ast_typed/misc.ml | 25 +--- src/ast_typed/misc_smart.ml | 45 +----- src/ast_typed/types.ml | 17 +-- src/compiler/compiler_program.ml | 2 +- src/main/contract.ml | 4 +- src/main/main.ml | 2 +- src/mini_c/PP.ml | 4 +- src/simplify/camligo.ml | 110 +++++++-------- src/simplify/pascaligo.ml | 151 +++++++++++--------- src/test/integration_tests.ml | 1 + src/test/typer_tests.ml | 2 +- src/transpiler/transpiler.ml | 219 ++++++------------------------ src/typer/typer.ml | 217 +++-------------------------- 19 files changed, 245 insertions(+), 655 deletions(-) diff --git a/src/ast_simplified/PP.ml b/src/ast_simplified/PP.ml index 8120fa6cc..d16804d90 100644 --- a/src/ast_simplified/PP.ml +++ b/src/ast_simplified/PP.ml @@ -42,10 +42,10 @@ let rec expression ppf (e:expression) = match e with | E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m | E_list lst -> fprintf ppf "list[%a]" (list_sep_d annotated_expression) lst | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind - | E_lambda {binder;input_type;output_type;result;body} -> - fprintf ppf "lambda (%s:%a) : %a {@; @[%a@]@;} return %a" - binder type_expression input_type type_expression output_type - block body annotated_expression result + | E_lambda {binder;input_type;output_type;result} -> + fprintf ppf "lambda (%s:%a) : %a return %a" + binder (PP_helpers.option type_expression) input_type (PP_helpers.option type_expression) output_type + annotated_expression result | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m | E_failwith ae -> @@ -65,6 +65,7 @@ let rec expression ppf (e:expression) = match e with annotated_expression expr | E_let_in { binder; rhs; result } -> fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result + | E_skip -> fprintf ppf "skip" and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) -> fprintf ppf "%a -> %a" annotated_expression a annotated_expression b @@ -88,8 +89,6 @@ and annotated_expression ppf (ae:annotated_expression) = match ae.type_annotatio and value : _ -> value -> unit = fun x -> annotated_expression x -and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b - and single_record_patch ppf ((p, ae) : string * ae) = fprintf ppf "%s <- %a" p annotated_expression ae @@ -113,17 +112,6 @@ and matching : type a . (formatter -> a -> unit) -> formatter -> a matching -> u | Match_option {match_none ; match_some = (some, match_some)} -> fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none some f match_some -and instruction ppf (i:instruction) = match i with - | I_skip -> fprintf ppf "skip" - | I_do ae -> fprintf ppf "do %a" annotated_expression ae - | I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst - | I_tuple_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_tuple_patch) lst - | I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b - | I_assignment {name;annotated_expression = ae} -> - fprintf ppf "%s := %a" name annotated_expression ae - | I_matching (ae, m) -> - fprintf ppf "match %a with %a" annotated_expression ae (matching block) m - let declaration ppf (d:declaration) = match d with | Declaration_type {type_name ; type_expression = te} -> fprintf ppf "type %s = %a" type_name type_expression te diff --git a/src/ast_simplified/combinators.ml b/src/ast_simplified/combinators.ml index 6744722a6..22863c02b 100644 --- a/src/ast_simplified/combinators.ml +++ b/src/ast_simplified/combinators.ml @@ -9,11 +9,18 @@ let get_type_name : named_type_expression -> string = fun x -> x.type_name let get_type_annotation (x:annotated_expression) = x.type_annotation let get_expression (x:annotated_expression) = x.expression -let i_assignment : _ -> instruction = fun x -> I_assignment x let named_expression name annotated_expression = { name ; annotated_expression } let named_typed_expression name expression ty = { name ; annotated_expression = { expression ; type_annotation = Some ty } } let typed_expression expression ty = { expression ; type_annotation = Some ty } let untyped_expression expression = { expression ; type_annotation = None } +let merge_type_expression ae type_annotation = match ae.type_annotation with + | None -> ok { ae with type_annotation = Some type_annotation } + | Some _ -> simple_fail "merging already typed expression" + +let merge_option_type_expression ae ta_opt = match (ae.type_annotation , ta_opt) with + | _ , None -> ok ae + | None , Some type_annotation -> ok { ae with type_annotation = Some type_annotation } + | _ -> simple_fail "merging already typed expression" let get_untyped_expression : annotated_expression -> expression result = fun ae -> let%bind () = @@ -79,6 +86,10 @@ 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_a_unit : annotated_expression = make_e_a_full (e_unit ()) t_unit let e_a_string s : annotated_expression = make_e_a_full (e_string s) t_string @@ -89,6 +100,7 @@ let e_a_list lst : annotated_expression = make_e_a (e_list lst) let e_a_constructor s a : annotated_expression = make_e_a (e_constructor s a) let e_a_address x = make_e_a_full (e_address x) t_address let e_a_tez x = make_e_a_full (e_tez x) t_tez +let e_a_sequence a b : annotated_expression = make_e_a (e_sequence a b) let e_a_record r = let type_annotation = Option.( @@ -130,17 +142,15 @@ let e_a_typed_list lst t = let e_a_map lst k v = make_e_a ~type_annotation:(t_map k v) (e_map lst) let e_lambda (binder : string) - (input_type : type_expression) - (output_type : type_expression) + (input_type : type_expression option) + (output_type : type_expression option) (result : expression) - (body : block) : expression = E_lambda { binder = (make_name binder) ; input_type = input_type ; output_type = output_type ; result = (make_e_a result) ; - body ; } let e_tuple (lst : ae list) : expression = E_tuple lst diff --git a/src/ast_simplified/types.ml b/src/ast_simplified/types.ml index 75b17a667..9d647cc1c 100644 --- a/src/ast_simplified/types.ml +++ b/src/ast_simplified/types.ml @@ -47,11 +47,10 @@ and type_expression = | T_constant of type_name * te list and lambda = { - binder: name ; - input_type: type_expression; - output_type: type_expression; - result: ae ; - body: block ; + binder : name ; + input_type : type_expression option ; + output_type : type_expression option ; + result : ae ; } and let_in = { @@ -86,6 +85,7 @@ and expression = | E_sequence of (ae * ae) | E_loop of (ae * ae) | E_assign of (name * access_path * ae) + | E_skip and access = | Access_tuple of int @@ -105,18 +105,6 @@ and literal = | Literal_address of string | Literal_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation -and block = instruction list -and b = block - -and instruction = - | I_assignment of named_expression - | I_matching of ae * matching_instr - | I_loop of ae * b - | I_skip - | I_do of ae - | I_record_patch of (name * access_path * (string * ae) list) - | I_tuple_patch of (name * access_path * (int * ae) list) - and 'a matching = | Match_bool of { match_true : 'a ; @@ -133,6 +121,4 @@ and 'a matching = | Match_tuple of name list * 'a | Match_variant of ((constructor_name * name) * 'a) list -and matching_instr = b matching - and matching_expr = annotated_expression matching diff --git a/src/ast_typed/PP.ml b/src/ast_typed/PP.ml index 6292cb650..4c2122fa8 100644 --- a/src/ast_typed/PP.ml +++ b/src/ast_typed/PP.ml @@ -24,10 +24,10 @@ let rec annotated_expression ppf (ae:annotated_expression) : unit = | _ -> fprintf ppf "@[%a@]" expression ae.expression and lambda ppf l = - let {binder;input_type;output_type;result;body} = l in - fprintf ppf "lambda (%s:%a) : %a {@; @[%a@]@;} return %a" + let {binder;input_type;output_type;result} = l in + fprintf ppf "lambda (%s:%a) : %a return %a" binder type_value input_type type_value output_type - block body annotated_expression result + annotated_expression result and expression ppf (e:expression) : unit = match e with @@ -74,8 +74,6 @@ and literal ppf (l:literal) : unit = | Literal_address s -> fprintf ppf "@%s" s | Literal_operation _ -> fprintf ppf "Operation(...bytes)" -and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b - and single_record_patch ppf ((s, ae) : string * ae) = fprintf ppf "%s <- %a" s annotated_expression ae @@ -100,21 +98,6 @@ and pre_access ppf (a:access) = match a with | Access_tuple i -> fprintf ppf ".%d" i | Access_map n -> fprintf ppf ".%a" annotated_expression n -and instruction ppf (i:instruction) = match i with - | I_skip -> fprintf ppf "skip" - | I_do ae -> fprintf ppf "do %a" annotated_expression ae - | I_loop (cond, b) -> fprintf ppf "while (%a) {@; @[%a@]@;}" annotated_expression cond block b - | I_declaration {name;annotated_expression = ae} -> - fprintf ppf "let %s = %a" name annotated_expression ae - | I_assignment {name;annotated_expression = ae} -> - fprintf ppf "%s := %a" name annotated_expression ae - | I_matching (ae, m) -> - fprintf ppf "match %a with %a" annotated_expression ae (matching block) m - | I_patch (s, p, e) -> - fprintf ppf "%s%a := %a" - s.type_name (fun ppf -> List.iter (pre_access ppf)) p - annotated_expression e - let declaration ppf (d:declaration) = match d with | Declaration_constant ({name ; annotated_expression = ae} , _) -> diff --git a/src/ast_typed/combinators.ml b/src/ast_typed/combinators.ml index 430c2ed72..21b6c98be 100644 --- a/src/ast_typed/combinators.ml +++ b/src/ast_typed/combinators.ml @@ -6,7 +6,6 @@ let make_a_e expression type_annotation environment = { expression ; type_annota 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 t_bool ?s () : type_value = make_t (T_constant ("bool", [])) s let t_string ?s () : type_value = make_t (T_constant ("string", [])) s let t_bytes ?s () : type_value = make_t (T_constant ("bytes", [])) s @@ -22,7 +21,6 @@ let t_list t ?s () : type_value = make_t (T_constant ("list", [t])) s let t_contract t ?s () : type_value = make_t (T_constant ("contract", [t])) s let t_pair a b ?s () = t_tuple [a ; b] ?s () - let t_record m ?s () : type_value = make_t (T_record m) s let make_t_ez_record (lst:(string * type_value) list) : type_value = let aux prev (k, v) = SMap.add k v prev in @@ -164,6 +162,7 @@ let e_pair a b : expression = E_tuple [a; b] let e_application a b : expression = E_application (a , b) let e_variable v : expression = E_variable v let e_list lst : expression = E_list lst +let e_let_in binder rhs result = E_let_in { binder ; rhs ; result } let e_a_unit = make_a_e e_unit (t_unit ()) let e_a_int n = make_a_e (e_int n) (t_int ()) @@ -183,6 +182,7 @@ let e_a_variable v ty = make_a_e (e_variable v) ty let ez_e_a_record r = make_a_e (ez_e_record r) (ez_t_record (List.map (fun (x, y) -> x, y.type_annotation) r) ()) let e_a_map lst k v = make_a_e (e_map lst) (t_map k v ()) let e_a_list lst t = make_a_e (e_list lst) (t_list t ()) +let e_a_let_in binder expr body = make_a_e (e_let_in binder expr body) (get_type_annotation body) let get_a_int (t:annotated_expression) = match t.expression with diff --git a/src/ast_typed/environment.ml b/src/ast_typed/environment.ml index 7d254d500..673f8645f 100644 --- a/src/ast_typed/environment.ml +++ b/src/ast_typed/environment.ml @@ -78,3 +78,11 @@ module PP = struct (ne_list_sep small_environment (tag "@;")) e end +open Trace + +let get_trace : string -> t -> element result = fun s env -> + let error = + let title () = "missing var not in env" in + let content () = Format.asprintf "\nvar: %s\nenv: %a\n" s PP.full_environment env in + error title content in + trace_option error @@ get_opt s env diff --git a/src/ast_typed/misc.ml b/src/ast_typed/misc.ml index e34276654..1fec7e428 100644 --- a/src/ast_typed/misc.ml +++ b/src/ast_typed/misc.ml @@ -70,32 +70,11 @@ module Free_variables = struct and lambda : bindings -> lambda -> bindings = fun b l -> let b' = union (singleton l.binder) b in - let (b'', frees) = block' b' l.body in - union (annotated_expression b'' l.result) frees + annotated_expression b' l.result and annotated_expression : bindings -> annotated_expression -> bindings = fun b ae -> expression b ae.expression - and instruction' : bindings -> instruction -> bindings * bindings = fun b i -> - match i with - | I_declaration n -> union (singleton n.name) b , (annotated_expression b n.annotated_expression) - | I_assignment n -> b , (annotated_expression b n.annotated_expression) - | I_skip -> b , empty - | I_do e -> b , annotated_expression b e - | I_loop (a , bl) -> b , union (annotated_expression b a) (block b bl) - | I_patch (_ , _ , a) -> b , annotated_expression b a - | I_matching (a , cs) -> b , union (annotated_expression b a) (matching_block b cs) - - and block' : bindings -> block -> (bindings * bindings) = fun b bl -> - let aux = fun (binds, frees) cur -> - let (binds', frees') = instruction' binds cur in - (binds', union frees frees') in - List.fold_left aux (b , []) bl - - and block : bindings -> block -> bindings = fun b bl -> - let (_ , frees) = block' b bl in - frees - and matching_variant_case : type a . (bindings -> a -> bindings) -> bindings -> ((constructor_name * name) * a) -> bindings = fun f b ((_,n),c) -> f (union (singleton n) b) c @@ -109,8 +88,6 @@ module Free_variables = struct and matching_expression = fun x -> matching annotated_expression x - and matching_block = fun x -> matching block x - end diff --git a/src/ast_typed/misc_smart.ml b/src/ast_typed/misc_smart.ml index b4ac2f93c..2c56ad89c 100644 --- a/src/ast_typed/misc_smart.ml +++ b/src/ast_typed/misc_smart.ml @@ -19,15 +19,10 @@ let program_to_main : program -> string -> lambda result = fun p s -> | _ -> simple_fail "program main isn't a function" in ok (main , input_ty , output_ty) in - let body = - let aux : declaration -> instruction = fun d -> - match d with - | Declaration_constant (d , _) -> I_declaration d in - List.map (Function.compose aux Location.unwrap) p in let env = let aux = fun _ d -> match d with - | Declaration_constant (_ , env) -> env in + | Declaration_constant (_ , (_ , post_env)) -> post_env in List.fold_left aux Environment.full_empty (List.map Location.unwrap p) in let binder = "@contract_input" in let result = @@ -38,7 +33,6 @@ let program_to_main : program -> string -> lambda result = fun p s -> binder ; input_type ; output_type ; - body ; result ; } @@ -103,41 +97,6 @@ module Captured_variables = struct let b' = union (singleton li.binder) b in annotated_expression b' li.result - and instruction' : bindings -> instruction -> (bindings * bindings) result = fun b i -> - match i with - | I_declaration n -> - let bounds = union (singleton n.name) b in - let%bind frees = annotated_expression b n.annotated_expression in - ok (bounds , frees) - | I_assignment n -> - let%bind frees = annotated_expression b n.annotated_expression in - ok (b , frees) - | I_skip -> ok (b , empty) - | I_do e -> - let%bind frees = annotated_expression b e in - ok (b , frees) - | I_loop (a , bl) -> - let%bind ae_frees = annotated_expression b a in - let%bind bl_frees = block b bl in - ok (b , union ae_frees bl_frees) - | I_patch (_ , _ , a) -> - let%bind a' = annotated_expression b a in - ok (b , a') - | I_matching (a , cs) -> - let%bind ae' = annotated_expression b a in - let%bind bl' = matching_block b cs in - ok (b , union ae' bl') - - and block' : bindings -> block -> (bindings * bindings) result = fun b bl -> - let aux = fun (binds, frees) cur -> - let%bind (binds', frees') = instruction' binds cur in - ok (binds', union frees frees') in - bind_fold_list aux (b , []) bl - - and block : bindings -> block -> bindings result = fun b bl -> - let%bind (_ , frees) = block' b bl in - ok frees - and matching_variant_case : type a . (bindings -> a -> bindings result) -> bindings -> ((constructor_name * name) * a) -> bindings result = fun f b ((_,n),c) -> f (union (singleton n) b) c @@ -163,6 +122,4 @@ module Captured_variables = struct and matching_expression = fun x -> matching annotated_expression x - and matching_block = fun x -> matching block x - end diff --git a/src/ast_typed/types.ml b/src/ast_typed/types.ml index 72cd5ef34..9dbd2fc64 100644 --- a/src/ast_typed/types.ml +++ b/src/ast_typed/types.ml @@ -14,7 +14,7 @@ type 'a type_name_map = 'a SMap.t type program = declaration Location.wrap list and declaration = - | Declaration_constant of (named_expression * full_environment) + | Declaration_constant of (named_expression * (full_environment * full_environment)) (* | Macro_declaration of macro_declaration *) and environment_element_definition = @@ -72,7 +72,6 @@ and lambda = { input_type: tv ; output_type: tv ; result: ae ; - body: block ; } and let_in = { @@ -122,18 +121,6 @@ and literal = | Literal_address of string | Literal_operation of Memory_proto_alpha.Alpha_context.packed_internal_operation -and block = instruction list -and b = block - -and instruction = - | I_declaration of named_expression - | I_assignment of named_expression - | I_matching of ae * matching_instr - | I_loop of ae * b - | I_do of ae - | I_skip - | I_patch of named_type_value * access_path * ae - and access = | Access_tuple of int | Access_record of string @@ -157,8 +144,6 @@ and 'a matching = | Match_tuple of (name list * 'a) | Match_variant of (((constructor_name * name) * 'a) list * type_value) -and matching_instr = b matching - and matching_expr = ae matching open Trace diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 077e8f92f..e5b5b6632 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -324,7 +324,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m ]) in return code ) - | E_let_in (v, expr , body) -> ( + | E_let_in (v , expr , body) -> ( let%bind (expr' , expr_env) = translate_expression expr env in let%bind env' = let%bind popped = Compiler_environment.pop expr_env in diff --git a/src/main/contract.ml b/src/main/contract.ml index e41d689f5..0fc8484c4 100644 --- a/src/main/contract.ml +++ b/src/main/contract.ml @@ -110,7 +110,7 @@ let compile_contract_parameter : string -> string -> string -> string result = f let env = let last_declaration = Location.unwrap List.(hd @@ rev program) in match last_declaration with - | Declaration_constant (_ , env) -> env + | Declaration_constant (_ , (_ , post_env)) -> post_env in trace (simple_error "typing expression") @@ Typer.type_annotated_expression env simplified in @@ -158,7 +158,7 @@ let compile_contract_storage : string -> string -> string -> string result = fun let env = let last_declaration = Location.unwrap List.(hd @@ rev program) in match last_declaration with - | Declaration_constant (_ , env) -> env + | Declaration_constant (_ , (_ , post_env)) -> post_env in trace (simple_error "typing expression") @@ Typer.type_annotated_expression env simplified in diff --git a/src/main/main.ml b/src/main/main.ml index 0dce98a61..624c69ed0 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -138,7 +138,7 @@ let easy_run_typed_simplified let env = let last_declaration = Location.unwrap List.(hd @@ rev program) in match last_declaration with - | Declaration_constant (_ , env) -> env + | Declaration_constant (_ , (_ , post_env)) -> post_env in type_expression ~env input in let%bind mini_c_value = transpile_value typed_value in diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml index a7fb12d6c..895b0754a 100644 --- a/src/mini_c/PP.ml +++ b/src/mini_c/PP.ml @@ -80,7 +80,7 @@ and expression' ppf (e:expression') = match e with | E_sequence (a , b) -> fprintf ppf "%a ; %a" expression a expression b (* | E_sequence_drop (a , b) -> fprintf ppf "%a ;- %a" expression a expression b *) | E_let_in ((name , _) , expr , body) -> - fprintf ppf "let %s = %a in %a" name expression expr expression body + fprintf ppf "let %s = %a in ( %a )" name expression expr expression body | E_assignment (r , path , e) -> fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e | E_while (e , b) -> @@ -95,7 +95,7 @@ and expression_with_type : _ -> expression -> _ = fun ppf e -> type_ e.type_value and function_ ppf ({binder ; input ; output ; result}:anon_function) = - fprintf ppf "fun (%s:%a) : %a return %a" + fprintf ppf "fun (%s:%a) : %a (%a)" binder type_ input type_ output diff --git a/src/simplify/camligo.ml b/src/simplify/camligo.ml index 7a99abcb4..11cea6443 100644 --- a/src/simplify/camligo.ml +++ b/src/simplify/camligo.ml @@ -45,6 +45,15 @@ let get_p_variable : I.pattern -> string Location.wrap result = fun p -> | I.P_variable v -> ok v | _ -> simple_fail "not a pattern variable" +let get_p_option_typed_variable : I.pattern -> (string Location.wrap * I.restricted_type_expression Location.wrap option) result = fun p -> + match p with + | I.P_variable v -> ok (v , None) + | I.P_type_annotation (pat , rte) -> ( + let%bind v = get_p_variable @@ unwrap pat in + ok (v , Some rte) + ) + | _ -> simple_fail "not an optionally typed pattern variable" + let get_p_typed_variable : I.pattern -> (string Location.wrap * I.restricted_type_expression Location.wrap) result = fun p -> let%bind (p' , rte) = trace (simple_error "get_p_typed_variable") @@ @@ -171,64 +180,40 @@ let rec of_restricted_type_expression : I.restricted_type_expression -> I.type_e let restricted_type_expression : I.restricted_type_expression -> O.type_expression result = Function.compose type_expression of_restricted_type_expression -type last_instruction_result = (O.block * O.annotated_expression) -type lir = last_instruction_result - let rec expression : I.expression -> O.annotated_expression result = fun e -> - let simple_error str = - let title () = Format.asprintf "No %s in inside expressions" str in - let content () = Format.asprintf "%a" I.pp_expression e in - error title content in match e with - | I.E_sequence _ -> fail @@ simple_error "sequence" - | I.E_let_in _ -> fail @@ simple_error "letin" + | I.E_sequence lst -> ( + let%bind lst' = bind_map_list expression @@ List.map unwrap lst in + match lst' with + | [] -> simple_fail "empty sequence" + | hd :: tl -> ok @@ List.fold_right' (fun prec cur -> untyped_expression @@ e_sequence prec cur) hd tl + ) + | I.E_let_in (pattern , expr , body) -> ( + let%bind (name , rte) = get_p_option_typed_variable @@ unwrap pattern in + let%bind type_expression' = bind_map_option (fun x -> restricted_type_expression @@ unwrap x) rte in + let%bind expr' = expression @@ unwrap expr in + let%bind expr'' = merge_option_type_expression expr' type_expression' in + let%bind body' = expression @@ unwrap body in + ok @@ untyped_expression @@ e_let_in (unwrap name) expr'' body' + ) | I.E_ifthenelse ite -> ifthenelse ite | I.E_ifthen it -> ifthen it | I.E_match m -> match_ m | I.E_record r -> record r - | I.E_fun _ -> fail @@ simple_error "fun" + | I.E_fun (pattern , expr) -> ( + let%bind (name , rte) = get_p_typed_variable @@ unwrap pattern in + let name' = unwrap name in + let%bind type_expression' = restricted_type_expression (unwrap rte) in + let%bind expr' = expression (unwrap expr) in + ok @@ untyped_expression @@ E_lambda { + binder = name' ; + input_type = Some type_expression' ; + output_type = None ; + result = expr' ; + } + ) | I.E_main m -> expression_main m -and expression_last_instruction : I.expression -> lir result = fun e -> - match e with - | I.E_let_in l -> let_in_last_instruction l - | I.E_sequence s -> sequence_last_instruction s - | I.E_fun _|I.E_record _|I.E_ifthenelse _ - | I.E_ifthen _|I.E_match _|I.E_main _ -> ( - let%bind result' = expression e in - ok ([] , result') - ) - -and expression_sequence : I.expression -> O.instruction result = fun e -> - match e with - | _ -> ( - let%bind e' = expression e in - ok @@ O.I_do e' - ) - -and let_in_last_instruction : - I.pattern Location.wrap * I.expression Location.wrap * I.expression Location.wrap -> lir result - = fun l -> - let (pat , expr , body) = l in - let%bind (var , ty) = get_p_typed_variable (unwrap pat) in - let%bind ty' = type_expression @@ of_restricted_type_expression (unwrap ty) in - let%bind expr' = expression (unwrap expr) in - let%bind uexpr' = - trace_strong (simple_error "no annotation on let bodies") @@ - get_untyped_expression expr' in - let%bind (body' , last') = expression_last_instruction (unwrap body) in - let assignment = O.(i_assignment @@ named_typed_expression (unwrap var) uexpr' ty') in - ok (assignment :: body' , last') - -and sequence_last_instruction = fun s -> - let exprs = List.map unwrap s in - let%bind (hds , tl) = - trace_option (simple_error "at least 2 expressions in sequence") @@ - List.rev_uncons_opt exprs in - let%bind instrs' = bind_map_list expression_sequence hds in - let%bind (body' , last') = expression_last_instruction tl in - ok (instrs' @ body' , last') - and ifthenelse : (I.expression Location.wrap * I.expression Location.wrap * I.expression Location.wrap) -> O.annotated_expression result = fun ite -> @@ -444,27 +429,26 @@ let let_entry : _ -> _ result = fun l -> nty in let input = O.Combinators.typed_expression (E_variable input_nty.type_name) input_nty.type_expression in let tpl_declarations = - let aux = fun i (name , type_expression) -> - O.I_assignment { - name ; - annotated_expression = { - expression = O.E_accessor (input , [ Access_tuple i ]) ; - type_annotation = Some type_expression ; - } - } + let aux = fun i (name , type_expression) expr -> + untyped_expression @@ e_let_in name ( + make_e_a_full + (O.E_accessor (input , [ Access_tuple i ])) + type_expression + ) expr in - List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)] + let lst = List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)] in + fun expr -> List.fold_right' (fun prec cur -> cur prec) expr lst in - let%bind (body' , result) = expression_last_instruction (unwrap e) in + let%bind result = expression (unwrap e) in + let result = tpl_declarations result in let input_type' = input_nty.type_expression in let output_type' = O.(t_pair (t_list t_operation , storage_ty)) in let lambda = O.{ binder = input_nty.type_name ; - input_type = input_type'; - output_type = output_type'; + input_type = Some input_type'; + output_type = Some output_type'; result ; - body = tpl_declarations @ body' ; } in let type_annotation = Some (O.T_function (input_type', output_type')) in ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = {expression = O.E_lambda lambda ; type_annotation}} diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index be8526b19..92f66fe41 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -17,6 +17,17 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value let type_constants = Operators.Simplify.type_constants let constants = Operators.Simplify.constants +let return expr = ok @@ fun expr'_opt -> + let expr = untyped_expression expr in + match expr'_opt with + | None -> ok @@ expr + | Some expr' -> ok @@ e_a_sequence expr expr' + +let return_let_in binder rhs = ok @@ fun expr'_opt -> + match expr'_opt with + | None -> simple_fail "missing return" (* Hard to explain. Shouldn't happen in prod. *) + | Some expr' -> ok @@ untyped_expression @@ e_let_in binder rhs expr' + let rec simpl_type_expression (t:Raw.type_expr) : type_expression result = match t with | TPar x -> simpl_type_expression x.value.inside @@ -286,36 +297,33 @@ and simpl_tuple_expression ?te_annot (lst:Raw.expr list) : annotated_expression let%bind lst = bind_list @@ List.map simpl_expression lst in return @@ E_tuple lst -and simpl_local_declaration (t:Raw.local_decl) : (instruction * named_expression) result = +and simpl_local_declaration : Raw.local_decl -> _ result = fun t -> match t with | LocalData d -> simpl_data_declaration d | LocalLam l -> simpl_lambda_declaration l -and simpl_lambda_declaration : Raw.lambda_decl -> (instruction * named_expression) result = - fun l -> +and simpl_lambda_declaration : Raw.lambda_decl -> _ result = fun l -> match l with | FunDecl f -> let%bind e = simpl_fun_declaration (f.value) in - ok (I_assignment e, e) + return_let_in e.name e.annotated_expression | ProcDecl _ -> simple_fail "no local procedure yet" | EntryDecl _ -> simple_fail "no local entry-point yet" -and simpl_data_declaration (t:Raw.data_decl) : (instruction * named_expression) result = - let return x = ok (I_assignment x, x) in +and simpl_data_declaration : Raw.data_decl -> _ result = fun t -> match t with | LocalVar x -> let x = x.value in let name = x.name.value in let%bind t = simpl_type_expression x.var_type in let%bind annotated_expression = simpl_expression ~te_annot:t x.init in - return {name;annotated_expression} + return_let_in name annotated_expression | LocalConst x -> let x = x.value in let name = x.name.value in let%bind t = simpl_type_expression x.const_type in let%bind annotated_expression = simpl_expression ~te_annot:t x.init in - return {name;annotated_expression} - + return_let_in name annotated_expression and simpl_param : Raw.param_decl -> named_type_expression result = fun t -> match t with @@ -341,17 +349,22 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x -> let binder = input.type_name in let input_type = input.type_expression in let%bind local_declarations = - let%bind tmp = bind_list - @@ List.map simpl_local_declaration local_decls in - ok (List.map fst tmp) in + bind_map_list simpl_local_declaration local_decls in let%bind instructions = bind_list @@ List.map simpl_statement @@ npseq_to_list block.value.statements in let%bind result = simpl_expression return in let%bind output_type = simpl_type_expression ret_type in let body = local_declarations @ instructions in - let expression = E_lambda {binder ; input_type = input_type; - output_type = output_type; result ; body } in + let%bind result = + let aux prec cur = cur (Some prec) in + bind_fold_right_list aux result body in + let expression = E_lambda { + binder ; + input_type = Some input_type ; + output_type = Some output_type ; + result + } in let type_annotation = Some (T_function (input_type, output_type)) in ok {name;annotated_expression = {expression;type_annotation}} ) @@ -364,34 +377,34 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x -> { type_name = arguments_name ; type_expression } in let binder = input.type_name in let input_type = input.type_expression in - let tpl_declarations = + let%bind tpl_declarations = let aux = fun i (x:named_type_expression) -> - let ass = I_assignment { - name = x.type_name ; - annotated_expression = { - expression = E_accessor ({ + let expr = E_accessor ({ expression = E_variable arguments_name ; type_annotation = Some input.type_expression ; - } , [ Access_tuple i ] ) ; - type_annotation = Some (x.type_expression) ; - } - } in + } , [ Access_tuple i ]) in + let type_ = x.type_expression in + let ass = return_let_in x.type_name (make_e_a_full expr type_) in ass in - List.mapi aux params in + bind_list @@ List.mapi aux params in let%bind local_declarations = - let%bind typed = bind_map_list simpl_local_declaration local_decls in - ok (List.map fst typed) - in - let%bind output_type = simpl_type_expression ret_type in + bind_map_list simpl_local_declaration local_decls in let%bind instructions = bind_list @@ List.map simpl_statement @@ npseq_to_list block.value.statements in - - let body = tpl_declarations @ local_declarations @ instructions in let%bind result = simpl_expression return in - let expression = E_lambda {binder ; input_type = input_type; - output_type = output_type; result ; body } in + let%bind output_type = simpl_type_expression ret_type in + let body = tpl_declarations @ local_declarations @ instructions in + let%bind result = + let aux prec cur = cur (Some prec) in + bind_fold_right_list aux result body in + let expression = E_lambda { + binder ; + input_type = Some input_type ; + output_type = Some output_type ; + result + } in let type_annotation = Some (T_function (input_type, output_type)) in ok {name = name.value;annotated_expression = {expression;type_annotation}} ) @@ -420,23 +433,25 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap result = fu | LambdaDecl (ProcDecl _) -> simple_fail "no proc declaration yet" | LambdaDecl (EntryDecl _)-> simple_fail "no entry point yet" -and simpl_statement : Raw.statement -> instruction result = fun s -> +and simpl_statement : Raw.statement -> (_ -> annotated_expression result) result = fun s -> match s with | Instr i -> simpl_instruction i - | Data d -> let%bind (i, _) = simpl_data_declaration d in ok i + | Data d -> simpl_data_declaration d -and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> +and simpl_single_instruction : Raw.single_instr -> (_ -> annotated_expression result) result = fun t -> match t with | ProcCall _ -> simple_fail "no proc call" - | Fail e -> + | Fail e -> ( let%bind expr = simpl_expression e.value.fail_expr in - ok @@ I_do (untyped_expression @@ E_failwith expr) - | Skip _ -> ok @@ I_skip + return @@ e_failwith expr + ) + | Skip _ -> return @@ e_skip | Loop (While l) -> let l = l.value in let%bind cond = simpl_expression l.cond in let%bind body = simpl_block l.block.value in - ok @@ I_loop (cond, body) + let%bind body = body None in + return @@ e_loop cond body | Loop (For _) -> simple_fail "no for yet" | Cond c -> @@ -448,7 +463,9 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> let%bind match_false = match c.ifnot with | ClauseInstr i -> simpl_instruction_block i | ClauseBlock b -> simpl_statements @@ fst b.value.inside in - ok @@ I_matching (expr, (Match_bool {match_true; match_false})) + let%bind match_true = match_true None in + let%bind match_false = match_false None in + return @@ E_matching (expr, (Match_bool {match_true; match_false})) | Assign a -> ( let a = a.value in let%bind value_expr = match a.rhs with @@ -458,16 +475,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> match a.lhs with | Path path -> ( let (name , path') = simpl_path path in - match List.rev_uncons_opt path' with - | None -> ( - ok @@ I_assignment {name ; annotated_expression = value_expr} - ) - | Some (hds , last) -> ( - match last with - | Access_record property -> ok @@ I_record_patch (name , hds , [(property , value_expr)]) - | Access_tuple index -> ok @@ I_tuple_patch (name , hds , [(index , value_expr)]) - | _ -> simple_fail "no map assignment in this weird case yet" - ) + return @@ E_assign (name , path' , value_expr) ) | MapPath v -> ( let v' = v.value in @@ -477,21 +485,23 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> let%bind key_expr = simpl_expression v'.index.value.inside in let old_expr = make_e_a @@ E_variable name.value in let expr' = make_e_a @@ E_constant ("MAP_UPDATE", [key_expr ; value_expr ; old_expr]) in - ok @@ I_assignment {name = name.value ; annotated_expression = expr'} + return @@ E_assign (name.value , [] , expr') ) ) - | CaseInstr c -> + | CaseInstr c -> ( let c = c.value in let%bind expr = simpl_expression c.expr in let%bind cases = let aux (x : Raw.instruction Raw.case_clause Raw.reg) = let%bind i = simpl_instruction_block x.value.rhs in + let%bind i = i None in ok (x.value.pattern, i) in bind_list @@ List.map aux @@ npseq_to_list c.cases.value in let%bind m = simpl_cases cases in - ok @@ I_matching (expr, m) + return @@ E_matching (expr, m) + ) | RecordPatch r -> ( let r = r.value in let (name , access_path) = simpl_path r.path in @@ -499,7 +509,20 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> @@ 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.reg) -> x.value) @@ pseq_to_list r.record_inj.value.elements in - ok @@ I_record_patch (name, access_path, inj) + let%bind expr = + let aux = fun (access , v) -> + E_assign (name , access_path @ [ Access_record access ] , v) in + let assigns = List.map aux inj in + match assigns with + | [] -> simple_fail "empty record patch" + | hd :: tl -> ( + let aux acc cur = + e_sequence (untyped_expression acc) (untyped_expression cur) + in + ok @@ List.fold_left aux hd tl + ) + in + return @@ expr ) | MapPatch _ -> simple_fail "no map patch yet" | SetPatch _ -> simple_fail "no set patch yet" @@ -511,7 +534,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> | _ -> simple_fail "no complex map remove yet" in let%bind key' = simpl_expression key in let expr = E_constant ("MAP_REMOVE", [key' ; make_e_a (E_variable map)]) in - ok @@ I_assignment {name = map ; annotated_expression = make_e_a expr} + return @@ E_assign (map , [] , make_e_a expr) | SetRemove _ -> simple_fail "no set remove yet" and simpl_path : Raw.path -> string * Ast_simplified.access_path = fun p -> @@ -606,12 +629,12 @@ and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t - bind_map_list aux lst in ok @@ Match_variant constrs -and simpl_instruction_block : Raw.instruction -> block result = fun t -> +and simpl_instruction_block : Raw.instruction -> (_ -> annotated_expression result) result = fun t -> match t with - | Single s -> let%bind i = simpl_single_instruction s in ok [ i ] + | Single s -> simpl_single_instruction s | Block b -> simpl_block b.value -and simpl_instruction : Raw.instruction -> instruction result = fun t -> +and simpl_instruction : Raw.instruction -> (_ -> annotated_expression result) result = fun t -> let main_error = let title () = "simplifiying instruction" in let content () = Format.asprintf "%a" PP_helpers.(printer Parser.Pascaligo.ParserLog.print_instruction) t in @@ -621,11 +644,17 @@ and simpl_instruction : Raw.instruction -> instruction result = fun t -> | Single s -> simpl_single_instruction s | Block _ -> simple_fail "no block instruction yet" -and simpl_statements : Raw.statements -> block result = fun ss -> +and simpl_statements : Raw.statements -> (_ -> annotated_expression result) result = fun ss -> let lst = npseq_to_list ss in - bind_map_list simpl_statement lst + let%bind fs = bind_map_list simpl_statement lst in + let aux : _ -> (annotated_expression option -> annotated_expression result) -> _ = fun prec cur -> + let%bind res = cur prec in + ok @@ Some res in + ok @@ fun (expr' : _ option) -> + let%bind ret = bind_fold_right_list aux expr' fs in + ok @@ Option.unopt_exn ret -and simpl_block : Raw.block -> block result = fun t -> +and simpl_block : Raw.block -> (_ -> annotated_expression result) result = fun t -> simpl_statements t.statements let simpl_program : Raw.ast -> program result = fun t -> diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 5241f83a9..1dfe4d939 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -388,6 +388,7 @@ let declarations () : unit result = let%bind program = type_file "./contracts/declarations.ligo" in let make_input = e_a_int in let make_expected = fun n -> e_a_int (42 + n) in + expect_eq program "main" (make_input 0) (make_expected 0) >>? fun () -> expect_eq_n program "main" make_input make_expected let declaration_local () : unit result = diff --git a/src/test/typer_tests.ml b/src/test/typer_tests.ml index 415e7ff6c..bf48e50a9 100644 --- a/src/test/typer_tests.ml +++ b/src/test/typer_tests.ml @@ -40,7 +40,7 @@ module TestExpressions = struct let lambda () : unit result = test_expression - I.(e_lambda "x" t_int t_int (e_var "x") []) + I.(e_lambda "x" (Some t_int) (Some t_int) (e_var "x")) O.(t_function (t_int ()) (t_int ()) ()) let tuple () : unit result = diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index c21726105..262b9c722 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -119,139 +119,7 @@ let record_access_to_lr : type_value -> type_value AST.type_name_map -> string - bind_fold_list aux (ty , []) lr_path in ok lst -let rec translate_block : expression option -> AST.block -> expression result = fun expr_opt block -> - let aux = fun expr_opt i -> - let%bind expr = translate_instruction i expr_opt in - ok (Some expr) in - let%bind expr_opt = bind_fold_right_list aux expr_opt block in - let default = e_unit in - ok (Option.unopt ~default expr_opt) - -and translate_instruction : AST.instruction -> expression option -> expression result = fun i expr_opt -> - let expr = - let default = e_skip in - Option.unopt ~default expr_opt in - let return ?(tv = expr.type_value) expr' = ok @@ Combinators.Expression.make_tpl (expr' , tv) in - let skip = ok expr in - let return_seq ?(tv = expr.type_value) expr' = - let lhs = Expression.make_tpl (expr' , t_unit) in - let rhs = expr in - ok @@ Combinators.Expression.make_tpl (E_sequence ( lhs , rhs ) , tv) in - let return_seq_drop ?(tv = expr.type_value) expr' = - let lhs = Expression.make_tpl (expr' , t_unit) in - let rhs = expr in - (* ok @@ Combinators.Expression.make_tpl (E_sequence_drop ( lhs , rhs ) , tv) in *) - ok @@ Combinators.Expression.make_tpl (E_sequence ( lhs , rhs ) , tv) in - match i with - | I_declaration { name ; annotated_expression } -> - let%bind rhs = translate_annotated_expression annotated_expression in - return @@ E_let_in ((name , rhs.type_value) , rhs , expr) - | I_assignment { name ; annotated_expression } -> - let%bind rhs = translate_annotated_expression annotated_expression in - return_seq @@ E_assignment (name , [] , rhs) - | I_matching (matched , clauses) -> ( - let%bind expr' = translate_annotated_expression matched in - match clauses with - | Match_bool {match_true ; match_false} -> - let%bind (t , f) = bind_map_pair (translate_block None) (match_true, match_false) in - return_seq_drop @@ E_if_bool (expr', t, f) - | Match_option { match_none; match_some = ((name, tv), s) } -> - let%bind n = translate_block None match_none in - let%bind (tv' , s') = - let%bind tv' = translate_type tv in - let%bind s' = translate_block None s in - ok (tv' , s') in - return_seq_drop @@ E_if_none (expr' , n , ((name , tv') , s')) - | Match_variant (lst , variant) -> ( - let%bind tree = tree_of_sum variant in - let%bind tree' = match tree with - | Empty -> simple_fail "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' = translate_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 (snd a') (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 (simple_error "not supposed to happen here: missing match clause") @@ - List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in - let%bind body' = translate_block None body in - return @@ E_let_in ((name , tv) , top , body') - ) - | ((`Node (a , b)) , tv) -> - let%bind a' = - let%bind a_ty = get_t_left tv in - let a_var = "left" , a_ty in - let%bind e = aux (((Expression.make (E_variable "left") a_ty))) a in - ok (a_var , e) - in - let%bind b' = - let%bind b_ty = get_t_right tv in - let b_var = "right" , b_ty in - let%bind e = aux (((Expression.make (E_variable "right") b_ty))) b in - ok (b_var , e) - in - return_seq_drop @@ E_if_left (top , a' , b') - in - aux expr' tree'' - ) - | AST.Match_list _ | AST.Match_tuple (_, _) -> - simple_fail "only match bool, option and variants are translated yet" - ) - | I_loop (condition , body) -> - let%bind condition' = translate_annotated_expression condition in - let%bind body' = translate_block None body in - return_seq @@ E_while (condition' , body') - | I_do action -> - let%bind action' = translate_annotated_expression action in - return_seq action'.content - | I_skip -> skip - | I_patch (typed_name , path , rhs) -> ( - let ty = typed_name.type_value in - let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result = - fun (prev, acc) cur -> - let%bind ty' = translate_type prev in - match cur with - | Access_tuple ind -> - let%bind ty_lst = AST.Combinators.get_t_tuple prev in - let%bind ty'_lst = bind_map_list translate_type ty_lst in - let%bind path = tuple_access_to_lr ty' ty'_lst ind in - let path' = List.map snd path in - ok (List.nth ty_lst ind, acc @ path') - | Access_record prop -> - let%bind ty_map = - let error = - let title () = "accessing property on not a record" in - let content () = Format.asprintf "%s on %a in %a" - prop Ast_typed.PP.type_value prev Ast_typed.PP.annotated_expression rhs in - error title content - in - trace error @@ - AST.Combinators.get_t_record prev in - let%bind ty'_map = bind_map_smap translate_type ty_map in - let%bind path = record_access_to_lr ty' ty'_map prop in - let path' = List.map snd path in - ok (Map.String.find prop ty_map, acc @ path') - | Access_map _k -> simple_fail "no patch for map yet" - in - let%bind (_, path) = bind_fold_right_list aux (ty, []) path in - let%bind expr' = translate_annotated_expression rhs in - return_seq (E_assignment (typed_name.type_name, path, expr')) - ) - -and translate_literal : AST.literal -> value = fun l -> match l with +let rec translate_literal : AST.literal -> value = fun l -> match l with | Literal_bool b -> D_bool b | Literal_int n -> D_int n | Literal_nat n -> D_nat n @@ -530,7 +398,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re ) and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.expression result = fun env l -> - let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in + let { binder ; input_type ; output_type ; result } : AST.lambda = l in (* Deep capture. Capture the relevant part of the environment. *) let%bind (fv , c_env , c_tv) = let free_variables = Ast_typed.Free_variables.lambda [] l in @@ -542,14 +410,10 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express let init_env = Environment.(add (binder , raw_input) c_env) in let input = Environment.closure_representation init_env in let%bind output = translate_type output_type in - let%bind result = - let%bind result_expression = translate_annotated_expression result in - let%bind body_expression = translate_block (Some result_expression) body in - let%bind body_wrap_expression = - let load_expr = Expression.make_tpl (E_variable binder , input) in - ok @@ ez_e_return @@ ez_e_sequence (E_environment_load (load_expr , init_env)) body_expression - in - ok body_wrap_expression in + let%bind result = translate_annotated_expression result in + let result = + let load_expr = Expression.make_tpl (E_variable binder , input) in + ez_e_return @@ ez_e_sequence (E_environment_load (load_expr , init_env)) result in let tv = Mini_c.t_function input output in let f_literal = D_function { binder ; input ; output ; result } in let expr = Expression.make_tpl (E_literal f_literal , tv) in @@ -561,24 +425,19 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express ok @@ Expression.make_tpl (expr , tv) and translate_lambda env l = - let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in + let { binder ; input_type ; output_type ; result } : AST.lambda = l in (* Try to translate it in an empty env, if it succeeds, transpiles it as a quote value, else, as a closure expression. *) - let ((_body_bounds , body_fvs) , result_fvs) = AST.Free_variables.( - let bindings = singleton binder in - let ((body_bounds , _) as b) = block' bindings body in - b , annotated_expression body_bounds result - ) in + let fvs = AST.Free_variables.(annotated_expression (singleton binder) result) in let%bind result = - match (body_fvs, result_fvs) with - | [] , [] -> ( + match fvs with + | [] -> ( let%bind result' = translate_annotated_expression result in - let%bind body_expression = translate_block (Some result') body in - let body_wrapped = ez_e_return body_expression in + let result' = ez_e_return result' in trace (simple_error "translate quote") @@ let%bind input = translate_type input_type in let%bind output = translate_type output_type in let tv = Combinators.t_function input output in - let content = D_function {binder;input;output;result=body_wrapped} in + let content = D_function {binder;input;output;result=result'} in ok @@ Combinators.Expression.make_tpl (E_literal content, tv) ) | _ -> ( @@ -619,36 +478,36 @@ let functionalize (e:AST.annotated_expression) : AST.lambda * AST.type_value = input_type = Combinators.t_unit () ; output_type = t ; result = e ; - body = [I_skip] }, Combinators.(t_function (t_unit ()) t ()) let translate_entry (lst:AST.program) (name:string) : anon_function result = - let%bind (lst', l, _) = - let rec aux acc (lst:AST.program) = - match lst with - | [] -> None - | hd :: tl -> ( - let (AST.Declaration_constant (an , _)) = temp_unwrap_loc hd in - match an.name = name with - | true -> ( - match an.annotated_expression.expression with - | E_lambda l -> Some (acc, l, an.annotated_expression.type_annotation) - | _ -> - let (a, b) = functionalize an.annotated_expression in - Some (acc, a, b) - ) - | false -> aux (acc @ [AST.I_declaration an]) tl - ) - in - let%bind (lst', l, tv) = - trace_option (simple_error "no entry-point with given name") - @@ aux [] lst in - ok (lst', l, tv) in - let l' = {l with body = lst' @ l.body} in - let r = - trace (simple_error "translating entry") @@ - translate_main l' in - r + let rec aux acc (lst:AST.program) = + let%bind acc = acc in + match lst with + | [] -> simple_fail "no entry point with given name" + | hd :: tl -> ( + let (AST.Declaration_constant (an , (pre_env , _))) = temp_unwrap_loc hd in + match an.name = name with + | false -> ( + let next = fun expr -> + let cur = e_a_let_in an.name an.annotated_expression expr pre_env in + acc cur in + aux (ok next) tl + ) + | true -> ( + match an.annotated_expression.expression with + | E_lambda l -> + let l' = { l with result = acc l.result } in + translate_main l' + | _ -> + let (l , _) = functionalize an.annotated_expression in + let l' = { l with result = acc l.result } in + translate_main l' + ) + ) + in + let%bind l = aux (ok (fun x -> x)) lst in + ok l open Combinators diff --git a/src/typer/typer.ml b/src/typer/typer.ml index 58220239d..4d59f02cb 100644 --- a/src/typer/typer.ml +++ b/src/typer/typer.ml @@ -73,146 +73,11 @@ and type_declaration env : I.declaration -> (environment * O.declaration option) trace (constant_declaration_error name annotated_expression) @@ type_annotated_expression env annotated_expression in let env' = Environment.add_ez_ae name ae' env in - ok (env', Some (O.Declaration_constant ((make_n_e name ae') , env'))) - -and type_block_full (e:environment) (b:I.block) : (O.block * environment) result = - let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) = - let%bind (e', i') = type_instruction e i in - ok (e', i' @ acc) - in - let%bind (e', lst) = bind_fold_list aux (e, []) b in - ok @@ (List.rev lst, e') - -and type_block (e:environment) (b:I.block) : O.block result = - let%bind (block, _) = type_block_full e b in - ok block - -and type_instruction (e:environment) : I.instruction -> (environment * O.instruction list) result = fun i -> - let return x = ok (e, [x]) in - match i with - | I_skip -> return O.I_skip - | I_do x -> - let%bind expression = type_annotated_expression e x in - let%bind () = - trace_strong (simple_error "do without unit") @@ - Ast_typed.assert_type_value_eq (get_type_annotation expression , t_unit ()) in - return @@ O.I_do expression - | I_loop (cond, body) -> - let%bind cond = type_annotated_expression e cond in - let%bind _ = - O.assert_type_value_eq (cond.type_annotation, t_bool ()) in - let%bind body = type_block e body in - return @@ O.I_loop (cond, body) - | I_assignment {name;annotated_expression} -> ( - match annotated_expression.type_annotation, Environment.get_opt name e with - | None, None -> simple_fail "Initial assignments need type annotation" - | Some _, None -> - let%bind annotated_expression = type_annotated_expression e annotated_expression in - let e' = Environment.add_ez_ae name annotated_expression e in - ok (e', [O.I_declaration (make_n_e name annotated_expression)]) - | None, Some prev -> - let%bind annotated_expression = type_annotated_expression e annotated_expression in - let%bind _ = - O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in - ok (e, [O.I_assignment (make_n_e name annotated_expression)]) - | Some _, Some prev -> - let%bind annotated_expression = type_annotated_expression e annotated_expression in - let%bind _assert = trace (simple_error "Annotation doesn't match environment") - @@ O.assert_type_value_eq (annotated_expression.type_annotation, prev.type_value) in - let e' = Environment.add_ez_ae name annotated_expression e in - ok (e', [O.I_assignment (make_n_e name annotated_expression)]) - ) - | I_matching (ex, m) -> ( - let%bind ex' = type_annotated_expression e ex in - match m with - (* Special case for assert-like failwiths. TODO: CLEAN THIS. *) - | I.Match_bool { match_false = [] ; match_true = [ I_do { expression = E_failwith fw } ] } - | I.Match_bool { match_false = [ I_skip ] ; match_true = [ I_do { expression = E_failwith fw } ] } -> ( - let%bind fw' = type_annotated_expression e fw in - let%bind () = - trace_strong (simple_error "Matching bool on not-a-bool") - @@ assert_t_bool (get_type_annotation ex') in - let assert_ = make_a_e - (E_constant ("ASSERT" , [ex' ; fw'])) - (t_unit ()) - e - in - return (O.I_do assert_) - ) - | _ -> ( - let%bind m' = type_match type_block e ex'.type_annotation m in - return @@ O.I_matching (ex', m') - ) - ) - | I_record_patch (r, path, lst) -> - let aux (s, ae) = - let%bind ae' = type_annotated_expression e ae in - let%bind ty = - trace_option (simple_error "unbound variable in record_patch") @@ - Environment.get_opt r e in - let tv = O.{type_name = r ; type_value = ty.type_value} in - let aux ty access = - match access with - | I.Access_record s -> - let%bind m = O.Combinators.get_t_record ty in - let%bind ty = - trace_option (simple_error "unbound record access in record_patch") @@ - Map.String.find_opt s m in - ok (ty , O.Access_record s) - | I.Access_tuple i -> - let%bind t = O.Combinators.get_t_tuple ty in - let%bind ty = - generic_try (simple_error "unbound tuple access in record_patch") @@ - (fun () -> List.nth t i) in - ok (ty , O.Access_tuple i) - | I.Access_map ind -> - let%bind (k , v) = O.Combinators.get_t_map ty in - let%bind ind' = type_annotated_expression e ind in - let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in - ok (v , O.Access_map ind') - in - let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_record s]) in - ok @@ O.I_patch (tv, path', ae') - in - let%bind lst' = bind_map_list aux lst in - ok (e, lst') - | I_tuple_patch (r, path, lst) -> - let aux (s, ae) = - let%bind ae' = type_annotated_expression e ae in - let%bind ty = - trace_option (simple_error "unbound variable in tuple_patch") @@ - Environment.get_opt r e in - let tv = O.{type_name = r ; type_value = ty.type_value} in - let aux ty access = - match access with - | I.Access_record s -> - let%bind m = O.Combinators.get_t_record ty in - let%bind ty = - trace_option (simple_error "unbound record access in tuple_patch") @@ - Map.String.find_opt s m in - ok (ty , O.Access_record s) - | I.Access_tuple i -> - let%bind t = O.Combinators.get_t_tuple ty in - let%bind ty = - generic_try (simple_error "unbound tuple access in tuple_patch") @@ - (fun () -> List.nth t i) in - ok (ty , O.Access_tuple i) - | I.Access_map ind -> - let%bind (k , v) = O.Combinators.get_t_map ty in - let%bind ind' = type_annotated_expression e ind in - let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in - ok (v , O.Access_map ind') - in - let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_tuple s]) in - ok @@ O.I_patch (tv, path', ae') - in - let%bind lst' = bind_map_list aux lst in - ok (e, lst') - + ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env')))) and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result = fun f e t i -> match i with - | Match_bool {match_true ; match_false} -> + | Match_bool {match_true ; match_false} -> let%bind _ = trace_strong (simple_error "Matching bool on not-a-bool") @@ get_t_bool t in @@ -354,7 +219,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot return (E_variable name) tv'.type_value | E_literal (Literal_bool b) -> return (E_literal (Literal_bool b)) (t_bool ()) - | E_literal Literal_unit -> + | E_literal Literal_unit | E_skip -> return (E_literal (Literal_unit)) (t_unit ()) | E_literal (Literal_string s) -> ( L.log (Format.asprintf "literal_string option type: %a" PP_helpers.(option O.PP.type_value) tv_opt) ; @@ -488,14 +353,20 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot input_type ; output_type ; result ; - body ; } -> ( - let%bind input_type = evaluate_type e input_type in - let%bind output_type = evaluate_type e output_type in + let%bind input_type = + let%bind input_type = + trace_option (simple_error "no input type provided") @@ + input_type in + evaluate_type e input_type in + let%bind output_type = + let%bind output_type = + trace_option (simple_error "no output type provided") @@ + output_type in + evaluate_type e output_type in let e' = Environment.add_ez_binder binder input_type e in - let%bind (body, e'') = type_block_full e' body in - let%bind result = type_annotated_expression e'' result in - return (E_lambda {binder;input_type;output_type;result;body}) (t_function input_type output_type ()) + let%bind result = type_annotated_expression e' result in + return (E_lambda {binder;input_type;output_type;result}) (t_function input_type output_type ()) ) | E_constant (name, lst) -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in @@ -532,7 +403,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot trace_strong (simple_error "Matching not-unit on an assert") @@ assert_t_unit (get_type_annotation mf') in let mt' = make_a_e - (E_failwith fw') + (E_constant ("ASSERT" , [ex' ; fw'])) (t_unit ()) e in @@ -582,9 +453,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot return (O.E_loop (expr' , body')) (t_unit ()) | E_assign (name , path , expr) -> let%bind typed_name = - let%bind ele = - trace_option (simple_error "missing var in env") @@ - Environment.get_opt name e in + let%bind ele = Environment.get_trace name e in ok @@ make_n_t name ele.type_value in let%bind (assign_tv , path') = let aux : ((_ * O.access_path) as 'a) -> I.access -> 'a result = fun (prec_tv , prec_path) cur_path -> @@ -613,7 +482,7 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot return (O.E_assign (typed_name , path' , expr')) (t_unit ()) | E_let_in {binder ; rhs ; result} -> let%bind rhs = type_annotated_expression e rhs in - let e' = Environment.add_ez_binder binder rhs.type_annotation e in + let e' = Environment.add_ez_declaration binder rhs e in let%bind result = type_annotated_expression e' result in return (E_let_in {binder; rhs; result}) result.type_annotation @@ -685,12 +554,11 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex let%bind f' = untype_annotated_expression f in let%bind arg' = untype_annotated_expression arg in return (E_application (f', arg')) - | E_lambda {binder;input_type;output_type;body;result} -> + | E_lambda {binder;input_type;output_type;result} -> let%bind input_type = untype_type_value input_type in let%bind output_type = untype_type_value output_type in let%bind result = untype_annotated_expression result in - let%bind body = untype_block body in - return (E_lambda {binder;input_type = input_type;output_type = output_type;body;result}) + return (E_lambda {binder;input_type = Some input_type;output_type = Some output_type;result}) | E_tuple lst -> let%bind lst' = bind_list @@ List.map untype_annotated_expression lst in @@ -732,51 +600,6 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex let%bind result = untype_annotated_expression result in return (E_let_in {binder;rhs;result}) -and untype_block (b:O.block) : (I.block) result = - bind_list @@ List.map untype_instruction b - -and untype_instruction (i:O.instruction) : (I.instruction) result = - let open I in - match i with - | I_skip -> ok I_skip - | I_do e -> - let%bind e' = untype_annotated_expression e in - ok (I_do e') - | I_loop (e, b) -> - let%bind e' = untype_annotated_expression e in - let%bind b' = untype_block b in - ok @@ I_loop (e', b') - | I_declaration a -> - let%bind annotated_expression = untype_annotated_expression a.annotated_expression in - ok @@ I_assignment {name = a.name ; annotated_expression} - | I_assignment a -> - let%bind annotated_expression = untype_annotated_expression a.annotated_expression in - ok @@ I_assignment {name = a.name ; annotated_expression} - | I_matching (e, m) -> - let%bind e' = untype_annotated_expression e in - let%bind m' = untype_matching untype_block m in - ok @@ I_matching (e', m') - | I_patch (s, p, e) -> - let%bind e' = untype_annotated_expression e in - let%bind (hds, tl) = - trace_option (simple_error "patch without path") @@ - List.rev_uncons_opt p in - let%bind tl_name = match tl with - | Access_record n -> ok n - | Access_tuple _ -> simple_fail "last element of patch is tuple" - | Access_map _ -> simple_fail "last element of patch is map" - in - let%bind hds' = bind_map_list untype_access hds in - ok @@ I_record_patch (s.type_name, hds', [tl_name, e']) - -and untype_access (a:O.access) : I.access result = - match a with - | Access_record n -> ok @@ I.Access_record n - | Access_tuple n -> ok @@ I.Access_tuple n - | Access_map n -> - let%bind n' = untype_annotated_expression n in - ok @@ I.Access_map n' - and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m -> let open I in match m with