From 68014c6e951d82108a4815dba4cde9a59be24721 Mon Sep 17 00:00:00 2001 From: galfour Date: Thu, 11 Jul 2019 15:20:58 +0200 Subject: [PATCH 1/9] add blog post about update --- .../website/blog/2019-07-11-ligo-update.md | 59 +++++++++++++++++++ 1 file changed, 59 insertions(+) create mode 100644 gitlab-pages/website/blog/2019-07-11-ligo-update.md diff --git a/gitlab-pages/website/blog/2019-07-11-ligo-update.md b/gitlab-pages/website/blog/2019-07-11-ligo-update.md new file mode 100644 index 000000000..1782b7731 --- /dev/null +++ b/gitlab-pages/website/blog/2019-07-11-ligo-update.md @@ -0,0 +1,59 @@ +--- +title: Updates about LIGO and Marigold +author: Gabriel Alfour +--- + +# Updates about LIGO and Marigold + +--- + +It's been a few weeks since our last update. Since then, we've onboarded new collaborators to both LIGO and Marigold, rewritten much of the codebase, and we've begun some exciting new projects. Let's tell you all about it! + +# LIGO + +Now that we've expanded the team, LIGO is progressing faster! Since our last update, we've published some initial tutorials, streamlined the installation process, and added new features to LIGO. + +Our ongoing efforts focus on removing the "warts" of LIGO, i.e. the aspects of LIGO which remain incomplete or unpleasant. Once finished, we will communicate much more extensively about LIGO, how developers can get started, and integrate with popular developer tools. + +We are also working on some longer-term projects which we highlight below. + +## Generic Front End + +LIGO currently supports 2 syntaxes, but that support is clunky and unscaleable to maintain in the long-run. For example, adding a new operator requires us to add it to both syntaxes manually and adding a new syntax remains time-consuming and compounds technical debt. + +As such, we are working on a Generic Front End (GFE), so that it becomes much easier to add syntaxes to LIGO and add new features to all syntaxes at once. The GFE also aims to support seamless translation between the syntaxes, so that one can not only write code in any syntax, but also read code written by other people in the syntax of their choice! + +To attract Ethereum developers, we are also looking at supporting the syntax of [Yul, an intermediary language between Solidity and the EVM](https://solidity.readthedocs.io/en/v0.5.3/yul.html), which would be a big step in supporting contracts written in Solidity! + +## Super Type System + +LIGO currently has a very simple type-system, requiring some extraneous type annotations and forbidding a lot of harmless programs. + +To fix this, we are putting effort into developing a Super Type System (STS). A more comprehensive type system will also help us to natively support Yul and constructs coming from other popular languages. + +Coming at this from the other end, the STS will make it much easier for developers to integrate tools and static analysis into LIGO. + +## Formally Verified Backend + +The most brittle part of our code base is about to become its strongest part. We are currently rewriting the backend of LIGO in Coq, and partially proving its correctness along the way. + +**The significance of this effort can't be stressed enough.** Basically, once we prove the equivalence between a part of LIGO and its Michelson counterpart, we can safely trust it. + +Concretely: +- Running LIGO-in-Browser will become much easier. Instead of having to dry-run it remotely or to rewrite a Michelson interpreter, we'll be able to **directly interpret** the LIGO program. +- It will be possible to prove the properties of Smart-Contracts written in LIGO directly, instead of having to prove the Michelson they produce. +- Fewer tests will ned to be written and testing will instead focus mostly on the developer-facing layers of the compiler (i.e. syntax, typing), rather than on the actual compiling part. + +# Marigold + +We had slowed development on Marigold until LIGO was ready. While we are still knocking out LIGO's remaining warts, we are finally returning our eyes back to Marigold. + +Tangibly speaking, we are locking down some actual implementation details with new collaborators and hope to provide an update in the coming weeks. + +On the more theoretical side, we are also working on a mathematical presentation of Plasma. Although there has been a tremendous amount of innovation and tinkering in the Plasma space, current writings about Plasma are very informal and lack mathematical specification. + +It is thus hard for newcomers (even CS researchers!) to dive into Plasma in a common way. It can also be hard to evaluate new ideas in this space, because each Plasma project brings their own jargon, assumptions, and models of how these systems work. Once this is done, we will strive to make Plasma General even more General. + +# Contact + +If you have any question, feel free to visit [our website](ligolang.org) and to contact us :) From 25566bc3fe98dff5d72a3571a94f95aac5da92db Mon Sep 17 00:00:00 2001 From: galfour Date: Thu, 18 Jul 2019 13:04:13 +0200 Subject: [PATCH 2/9] selection of environment can be done both ways --- src/compiler/compiler_environment.ml | 10 +++++--- src/compiler/compiler_program.ml | 36 +++++++++++++++++++++------- src/compiler/compiler_type.ml | 4 ++++ src/mini_c/PP.ml | 12 +++++----- src/mini_c/environment.ml | 8 +++++-- src/mini_c/types.ml | 2 +- src/transpiler/transpiler.ml | 2 +- 7 files changed, 53 insertions(+), 21 deletions(-) diff --git a/src/compiler/compiler_environment.ml b/src/compiler/compiler_environment.ml index 05c749095..458ac0438 100644 --- a/src/compiler/compiler_environment.ml +++ b/src/compiler/compiler_environment.ml @@ -87,7 +87,7 @@ let add : environment -> (string * type_value) -> michelson result = fun e (_s , ok code -let select : environment -> string list -> michelson result = fun e lst -> +let select ?(rev = false) : environment -> string list -> michelson result = fun e lst -> let module L = Logger.Stateful() in let e_lst = let e_lst = Environment.to_list e in @@ -96,7 +96,11 @@ let select : environment -> string list -> michelson result = fun e lst -> match List.mem s selector with | true -> List.remove_element s selector , true | false -> selector , false in - let e_lst' = List.fold_map_right aux lst e_lst in + let e_lst' = + if rev + then List.fold_map aux lst e_lst + else List.fold_map_right aux lst e_lst + in let e_lst'' = List.combine e_lst e_lst' in e_lst'' in let code = @@ -145,7 +149,7 @@ let clear : environment -> (michelson * environment) result = fun e -> 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 + let e' = Environment.select ~rev:true [ first_name ] e in ok (code , e') let pack : environment -> michelson result = fun e -> diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index ebd20a00a..e5487e3f7 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -106,11 +106,14 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m let return ?prepend_env ?end_env code = let%bind env' = match (prepend_env , end_env) with - | (Some _ , Some _) -> simple_fail ("two args to return at " ^ __LOC__) - | None , None -> ok @@ Environment.add ("_tmp_expression" , ty) env + | (Some _ , Some _) -> + simple_fail ("two args to return at " ^ __LOC__) + | None , None -> + ok @@ Environment.add ("_tmp_expression" , ty) env | Some prepend_env , None -> ok @@ Environment.add ("_tmp_expression" , ty) prepend_env - | None , Some end_env -> ok end_env in + | None , Some end_env -> + ok end_env in let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment env in let%bind output_type = Compiler_type.type_ ty in let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment env' in @@ -152,6 +155,11 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m unpack ; i_skip ; ] + (* return ~end_env:load_env @@ seq [ + * expr' ; + * dip clear ; + * unpack ; + * ] *) | E_environment_select sub_env -> let%bind code = Compiler_environment.select_env env sub_env in return ~prepend_env:sub_env @@ seq [ @@ -161,6 +169,8 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m | E_environment_return expr -> ( let%bind (expr' , env) = translate_expression expr env in let%bind (code , cleared_env) = Compiler_environment.clear env in + Format.printf "pre env %a\n" PP.environment env ; + Format.printf "post clean env %a\n" PP.environment cleared_env ; return ~end_env:cleared_env @@ seq [ expr' ; code ; @@ -221,7 +231,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m | E_variable x -> let%bind code = Compiler_environment.get env x in return code - | E_sequence (a , b) -> + | E_sequence (a , b) -> ( let%bind (a' , env_a) = translate_expression a env in let%bind env_a' = Compiler_environment.pop env_a in let%bind (b' , env_b) = translate_expression b env_a' in @@ -230,6 +240,13 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m i_drop ; 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' ; + * b' ; + * ] *) + ) | E_constant(str, lst) -> let module L = Logger.Stateful() in let%bind lst' = @@ -313,9 +330,9 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m | E_if_left (c, (l_ntv , l), (r_ntv , r)) -> ( let%bind (c' , _env') = translate_expression c env in let l_env = Environment.add l_ntv env in - let%bind (l' , _) = translate_expression l l_env in + let%bind (l' , _l_env') = translate_expression l l_env in let r_env = Environment.add r_ntv env in - let%bind (r' , _) = translate_expression r r_env in + let%bind (r' , _r_env') = translate_expression r r_env in let%bind restrict_l = Compiler_environment.select_env l_env env in let%bind restrict_r = Compiler_environment.select_env r_env env in let%bind code = ok (seq [ @@ -406,7 +423,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m 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%bind (expr , env') = translate_expression result env in let code = seq [ i_comment "function result" ; expr ; @@ -419,10 +436,13 @@ and translate_quote_body ({result ; binder ; input} as f:anon_function) : michel let output_stack_ty = Stack.(output_ty @: nil) in let error_message () = Format.asprintf - "\ncode : %a\ninput : %a\noutput : %a\n" + "\nCode : %a\nMichelson code : %a\ninput : %a\noutput : %a\nstart env : %a\nend env : %a\n" + PP.expression result Michelson.pp code PP.type_ f.input PP.type_ f.output + PP.environment env + PP.environment env' in let%bind _ = Trace.trace_tzresult_lwt ( diff --git a/src/compiler/compiler_type.ml b/src/compiler/compiler_type.ml index 2632f2bd8..5977db461 100644 --- a/src/compiler/compiler_type.ml +++ b/src/compiler/compiler_type.ml @@ -10,12 +10,14 @@ module Contract_types = Meta_michelson.Types module Ty = struct let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) () + let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) () let comparable_type_base : type_base -> ex_comparable_ty result = fun tb -> let open Contract_types in let return x = ok @@ Ex_comparable_ty x in match tb with | Base_unit -> fail (not_comparable "unit") + | Base_void -> fail (not_comparable "void") | Base_bool -> fail (not_comparable "bool") | Base_nat -> return nat_k | Base_tez -> return tez_k @@ -44,6 +46,7 @@ module Ty = struct let return x = ok @@ Ex_ty x in match b with | Base_unit -> return unit + | Base_void -> fail (not_compilable_type "void") | Base_bool -> return bool | Base_int -> return int | Base_nat -> return nat @@ -118,6 +121,7 @@ end let base_type : type_base -> O.michelson result = function | Base_unit -> ok @@ O.prim T_unit + | Base_void -> fail (Ty.not_compilable_type "void") | Base_bool -> ok @@ O.prim T_bool | Base_int -> ok @@ O.prim T_int | Base_nat -> ok @@ O.prim T_nat diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml index af5543689..bf848723b 100644 --- a/src/mini_c/PP.ml +++ b/src/mini_c/PP.ml @@ -10,6 +10,7 @@ let lr = fun ppf -> function `Left -> fprintf ppf "L" | `Right -> fprintf ppf "R let type_base ppf : type_base -> _ = function | Base_unit -> fprintf ppf "unit" + | Base_void -> fprintf ppf "void" | Base_bool -> fprintf ppf "bool" | Base_int -> fprintf ppf "int" | Base_nat -> fprintf ppf "nat" @@ -48,7 +49,7 @@ let rec value ppf : value -> unit = function | D_nat n -> fprintf ppf "+%d" n | D_timestamp n -> fprintf ppf "+%d" n | D_tez n -> fprintf ppf "%dtz" n - | D_unit -> fprintf ppf " " + | D_unit -> fprintf ppf "unit" | D_string s -> fprintf ppf "\"%s\"" s | D_bytes _ -> fprintf ppf "[bytes]" | D_pair (a, b) -> fprintf ppf "(%a), (%a)" value a value b @@ -68,12 +69,12 @@ 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_environment_return expr -> fprintf ppf "return (%a)" expression expr | E_skip -> fprintf ppf "skip" - | E_variable v -> fprintf ppf "%s" v + | E_variable v -> fprintf ppf "V(%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 - | E_literal v -> fprintf ppf "%a" value v + | E_literal v -> fprintf ppf "L(%a)" value v | E_make_empty_map _ -> fprintf ppf "map[]" | E_make_empty_list _ -> fprintf ppf "list[]" | E_make_empty_set _ -> fprintf ppf "set[]" @@ -82,8 +83,7 @@ and expression' ppf (e:expression') = match e with | E_if_none (c, n, ((name, _) , s)) -> fprintf ppf "%a ?? %a : %s -> %a" expression c expression n name expression s | 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_sequence (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) -> diff --git a/src/mini_c/environment.ml b/src/mini_c/environment.ml index 8c1bc796c..36f62a15e 100644 --- a/src/mini_c/environment.ml +++ b/src/mini_c/environment.ml @@ -32,14 +32,18 @@ module Environment (* : ENVIRONMENT *) = struct let get_names : t -> string list = List.map fst let remove : int -> t -> t = List.remove - let select : string list -> t -> t = fun lst env -> + let select ?(rev = false) : string list -> t -> t = fun lst env -> let e_lst = let e_lst = to_list env in let aux selector (s , _) = match List.mem s selector with | true -> List.remove_element s selector , true | false -> selector , false in - let e_lst' = List.fold_map_right aux lst e_lst in + let e_lst' = + if rev + then List.fold_map aux lst e_lst + else List.fold_map_right aux lst e_lst + in let e_lst'' = List.combine e_lst e_lst' in e_lst'' in of_list diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml index 57f117165..77fa0a026 100644 --- a/src/mini_c/types.ml +++ b/src/mini_c/types.ml @@ -1,7 +1,7 @@ type type_name = string type type_base = - | Base_unit + | Base_unit | Base_void | Base_bool | Base_int | Base_nat | Base_tez | Base_timestamp diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index 8dbaf60a8..88e7b5ad9 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -539,7 +539,7 @@ and translate_lambda env l = let%bind output = translate_type output_type in let tv = Combinators.t_function input output in let content = D_function {binder;input;output;result=result'} in - ok @@ Combinators.Expression.make_tpl (E_literal content, tv) + ok @@ Combinators.Expression.make_tpl (E_literal content , tv) ) | _ -> ( translate_lambda_deep env l From 4b6a58907df9854e54f81a1b80ecc84f1f11ef73 Mon Sep 17 00:00:00 2001 From: galfour Date: Thu, 18 Jul 2019 15:19:25 +0200 Subject: [PATCH 3/9] get rid of useless units ; make compiler.ml less brittle --- src/compiler/compiler_environment.ml | 10 +-- src/compiler/compiler_program.ml | 114 +++++++++++++-------------- src/mini_c/environment.ml | 8 +- 3 files changed, 66 insertions(+), 66 deletions(-) diff --git a/src/compiler/compiler_environment.ml b/src/compiler/compiler_environment.ml index 458ac0438..d5734c4e9 100644 --- a/src/compiler/compiler_environment.ml +++ b/src/compiler/compiler_environment.ml @@ -87,17 +87,17 @@ let add : environment -> (string * type_value) -> michelson result = fun e (_s , ok code -let select ?(rev = false) : environment -> string list -> michelson result = fun e lst -> +let select ?(rev = false) ?(keep = true) : environment -> string list -> michelson result = fun e lst -> let module L = Logger.Stateful() in let e_lst = let e_lst = Environment.to_list e in let aux selector (s , _) = L.log @@ Format.asprintf "Selector : %a\n" PP_helpers.(list_sep string (const " , ")) selector ; match List.mem s selector with - | true -> List.remove_element s selector , true - | false -> selector , false in + | true -> List.remove_element s selector , keep + | false -> selector , not keep in let e_lst' = - if rev + if rev = keep then List.fold_map aux lst e_lst else List.fold_map_right aux lst e_lst in @@ -148,7 +148,7 @@ let clear : environment -> (michelson * environment) result = fun e -> 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%bind code = select ~rev:true e [ first_name ] in let e' = Environment.select ~rev:true [ first_name ] e in ok (code , e') diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index e5487e3f7..813def75c 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -96,33 +96,50 @@ and translate_function (content:anon_function) : michelson result = let%bind body = translate_quote_body content in ok @@ seq [ body ] -and translate_expression ?(first=false) (expr:expression) (env:environment) : (michelson * environment) result = +and translate_expression ?push_var_name (expr:expression) (env:environment) : (michelson * environment) result = let (expr' , ty) = Combinators.Expression.(get_content expr , get_type expr) in 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 i_skip = i_push_unit in *) - let return ?prepend_env ?end_env code = + let return ?prepend_env ?end_env ?(unit_opt = false) code = + let code = + if unit_opt && push_var_name <> None + then seq [code ; i_push_unit] + else code + in let%bind env' = - match (prepend_env , end_env) with - | (Some _ , Some _) -> + match (prepend_env , end_env , push_var_name) with + | (Some _ , Some _ , _) -> simple_fail ("two args to return at " ^ __LOC__) - | None , None -> + | None , None , None -> ok @@ Environment.add ("_tmp_expression" , ty) env - | Some prepend_env , None -> + | None , None , Some push_var_name -> + ok @@ Environment.add (push_var_name , ty) env + | Some prepend_env , None , None -> ok @@ Environment.add ("_tmp_expression" , ty) prepend_env - | None , Some end_env -> - ok end_env in + | Some prepend_env , None , Some push_var_name -> + ok @@ Environment.add (push_var_name , ty) prepend_env + | None , Some end_env , None -> + ok end_env + | None , Some end_env , Some push_var_name -> ( + if unit_opt + then ok @@ Environment.add (push_var_name , ty) end_env + else ok end_env + ) + in let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment env in let%bind output_type = Compiler_type.type_ ty in let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment env' in let error_message () = let%bind schema_michelsons = Compiler_type.environment env in ok @@ Format.asprintf - "expression : %a\ncode : %a\nschema type : %a\noutput type : %a" + "expression : %a\ncode : %a\npreenv : %a\npostenv : %a\nschema type : %a\noutput type : %a" PP.expression expr Michelson.pp code + PP.environment env + PP.environment env' PP_helpers.(list_sep Michelson.pp (const ".")) schema_michelsons Michelson.pp output_type in @@ -141,33 +158,27 @@ 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_skip -> return ~end_env:env ~unit_opt:true @@ seq [] | E_environment_capture c -> let%bind code = Compiler_environment.pack_select env c in return @@ code - | E_environment_load (expr , load_env) -> - let%bind (expr' , _) = translate_expression expr env in + | E_environment_load (expr , load_env) -> ( + let%bind (expr' , _) = translate_expression ~push_var_name:"env_to_load" expr env in let%bind clear = Compiler_environment.select env [] in let%bind unpack = Compiler_environment.unpack load_env in - return ~prepend_env:load_env @@ seq [ + return ~end_env:load_env @@ seq [ expr' ; dip clear ; unpack ; - i_skip ; ] - (* return ~end_env:load_env @@ seq [ - * expr' ; - * dip clear ; - * unpack ; - * ] *) + ) | E_environment_select sub_env -> let%bind code = Compiler_environment.select_env env sub_env in - return ~prepend_env:sub_env @@ seq [ + return ~end_env:sub_env @@ seq [ code ; - i_skip ; ] | E_environment_return expr -> ( - let%bind (expr' , env) = translate_expression expr env in + let%bind (expr' , env) = translate_expression ~push_var_name:"return_clause" expr env in let%bind (code , cleared_env) = Compiler_environment.clear env in Format.printf "pre env %a\n" PP.environment env ; Format.printf "post clean env %a\n" PP.environment cleared_env ; @@ -184,8 +195,8 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m match Combinators.Expression.get_type f with | T_function _ -> ( trace (simple_error "Compiling quote application") @@ - let%bind (f , env') = translate_expression ~first f env in - let%bind (arg , _) = translate_expression arg env' in + let%bind (f , env') = translate_expression ~push_var_name:"application_f" f env in + let%bind (arg , _) = translate_expression ~push_var_name:"application_arg" arg env' in return @@ seq [ i_comment "quote application" ; i_comment "get f" ; @@ -197,8 +208,8 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m ) | T_deep_closure (small_env, input_ty , _) -> ( trace (simple_error "Compiling deep closure application") @@ - let%bind (arg' , env') = translate_expression arg env in - let%bind (f' , env'') = translate_expression f env' in + let%bind (arg' , env') = translate_expression ~push_var_name:"closure_arg" arg env in + let%bind (f' , env'') = translate_expression ~push_var_name:"closure_f" f env' in let%bind f_ty = Compiler_type.type_ f.type_value in let%bind append_closure = Compiler_environment.add_packed_anon small_env input_ty in let error = @@ -233,25 +244,17 @@ 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 env_a' = Compiler_environment.pop env_a in - let%bind (b' , env_b) = translate_expression b env_a' in + let%bind (b' , env_b) = translate_expression b env_a in return ~end_env:env_b @@ seq [ a' ; - i_drop ; 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' ; - * b' ; - * ] *) ) | E_constant(str, lst) -> let module L = Logger.Stateful() in let%bind lst' = let aux env expr = - let%bind (code , env') = translate_expression expr env in + let%bind (code , env') = translate_expression ~push_var_name:"constant_argx" expr env in L.log @@ Format.asprintf "\n%a -> %a in %a\n" PP.expression expr Michelson.pp code @@ -299,22 +302,22 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m let%bind o' = Compiler_type.type_ o in return @@ i_none o' | E_if_bool (c, a, b) -> ( - let%bind (c' , env') = translate_expression c env in + let%bind (c' , env') = translate_expression ~push_var_name:"bool_condition" c 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 (a' , env_a') = translate_expression ~push_var_name:"if_true" a popped in + let%bind (b' , _env_b') = translate_expression ~push_var_name:"if_false" b popped in let%bind code = ok (seq [ c' ; i_if a' b' ; ]) in - return code + return ~end_env:env_a' code ) | E_if_none (c, n, (ntv , s)) -> ( - let%bind (c' , env') = translate_expression c env in + let%bind (c' , env') = translate_expression ~push_var_name:"if_none_condition" c env in let%bind popped = Compiler_environment.pop env' in - let%bind (n' , _) = translate_expression n popped in + let%bind (n' , _) = translate_expression ~push_var_name:"if_none" n popped in let s_env = Environment.add ntv popped in - let%bind (s' , s_env') = translate_expression s s_env in + let%bind (s' , s_env') = translate_expression ~push_var_name:"if_some" 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 [ @@ -328,11 +331,11 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return code ) | E_if_left (c, (l_ntv , l), (r_ntv , r)) -> ( - let%bind (c' , _env') = translate_expression c env in + let%bind (c' , _env') = translate_expression ~push_var_name:"if_left_cond" c env in let l_env = Environment.add l_ntv env in - let%bind (l' , _l_env') = translate_expression l l_env in + let%bind (l' , _l_env') = translate_expression ~push_var_name:"if_left" l l_env in let r_env = Environment.add r_ntv env in - let%bind (r' , _r_env') = translate_expression r r_env in + let%bind (r' , _r_env') = translate_expression ~push_var_name:"if_right" r r_env in let%bind restrict_l = Compiler_environment.select_env l_env env in let%bind restrict_r = Compiler_environment.select_env r_env env in let%bind code = ok (seq [ @@ -351,11 +354,11 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return code ) | E_let_in (v , expr , body) -> ( - let%bind (expr' , expr_env) = translate_expression expr env in + let%bind (expr' , expr_env) = translate_expression ~push_var_name:"let_expr" 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 (body' , body_env) = translate_expression ~push_var_name:"let_body" body env' in let%bind restrict = let%bind popped = Compiler_environment.pop body_env in Compiler_environment.select_env popped env in @@ -368,8 +371,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m return code ) | 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 (expr' , env') = translate_expression ~push_var_name:"assignment_expr" expr env in let%bind get_code = Compiler_environment.get env' name in let modify_code = let aux acc step = match step with @@ -391,7 +393,7 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m in error title content in trace error @@ - return ~prepend_env:env @@ seq [ + return ~end_env:env ~unit_opt:true @@ seq [ i_comment "assign: start # env" ; expr' ; i_comment "assign: compute rhs # rhs : env" ; @@ -403,21 +405,19 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m 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 + | E_while (expr , block) -> ( + let%bind (expr' , env') = translate_expression ~push_var_name:"while_expr" expr 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 [ + return ~end_env:env ~unit_opt:true @@ seq [ expr' ; prim ~children:[seq [ block' ; restrict_block ; expr']] I_LOOP ; - i_skip ; ] ) diff --git a/src/mini_c/environment.ml b/src/mini_c/environment.ml index 36f62a15e..1d7463c48 100644 --- a/src/mini_c/environment.ml +++ b/src/mini_c/environment.ml @@ -32,15 +32,15 @@ module Environment (* : ENVIRONMENT *) = struct let get_names : t -> string list = List.map fst let remove : int -> t -> t = List.remove - let select ?(rev = false) : string list -> t -> t = fun lst env -> + let select ?(rev = false) ?(keep = true) : string list -> t -> t = fun lst env -> let e_lst = let e_lst = to_list env in let aux selector (s , _) = match List.mem s selector with - | true -> List.remove_element s selector , true - | false -> selector , false in + | true -> List.remove_element s selector , keep + | false -> selector , not keep in let e_lst' = - if rev + if rev = keep then List.fold_map aux lst e_lst else List.fold_map_right aux lst e_lst in From 7b9d861a34a07bf3885dfef9c500c1cdc42b7dfc Mon Sep 17 00:00:00 2001 From: galfour Date: Fri, 19 Jul 2019 12:13:09 +0200 Subject: [PATCH 4/9] type new operators --- src/ast_typed/combinators.ml | 8 ++ src/compiler/compiler_program.ml | 5 + src/contracts/arithmetic.ligo | 3 + src/operators/helpers.ml | 35 ++++++ src/operators/operators.ml | 206 +++++++++++++++++++++++++------ src/simplify/pascaligo.ml | 11 +- src/test/integration_tests.ml | 1 - 7 files changed, 222 insertions(+), 47 deletions(-) diff --git a/src/ast_typed/combinators.ml b/src/ast_typed/combinators.ml index 1b4a1926c..ec745fabc 100644 --- a/src/ast_typed/combinators.ml +++ b/src/ast_typed/combinators.ml @@ -141,6 +141,11 @@ let get_t_map (t:type_value) : (type_value * type_value) result = | T_constant ("map", [k;v]) -> ok (k, v) | _ -> simple_fail "get: not a map" +let get_t_big_map (t:type_value) : (type_value * type_value) result = + match t.type_value' with + | T_constant ("big_map", [k;v]) -> ok (k, v) + | _ -> simple_fail "get: not a big_map" + let get_t_map_key : type_value -> type_value result = fun t -> let%bind (key , _) = get_t_map t in ok key @@ -154,6 +159,7 @@ let assert_t_map = fun t -> ok () let is_t_map = Function.compose to_bool get_t_map +let is_t_big_map = Function.compose to_bool get_t_big_map let assert_t_tez : type_value -> unit result = get_t_tez let assert_t_key = get_t_key @@ -165,8 +171,10 @@ let assert_t_list t = ok () let is_t_list = Function.compose to_bool get_t_list +let is_t_set = Function.compose to_bool get_t_set let is_t_nat = Function.compose to_bool get_t_nat let is_t_string = Function.compose to_bool get_t_string +let is_t_bytes = Function.compose to_bool get_t_bytes let is_t_int = Function.compose to_bool get_t_int let assert_t_bytes = fun t -> diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 813def75c..f7f0f50a3 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -21,6 +21,11 @@ let get_predicate : string -> type_value -> expression list -> predicate result let%bind m_ty = Compiler_type.type_ ty' in ok @@ simple_unary @@ prim ~children:[m_ty] I_NONE ) + | "NIL" -> ( + let%bind ty' = Mini_c.get_t_list ty in + let%bind m_ty = Compiler_type.type_ ty' in + ok @@ simple_unary @@ prim ~children:[m_ty] I_NIL + ) | "UNPACK" -> ( let%bind ty' = Mini_c.get_t_option ty in let%bind m_ty = Compiler_type.type_ ty' in diff --git a/src/contracts/arithmetic.ligo b/src/contracts/arithmetic.ligo index 25b756b04..efaa0e62b 100644 --- a/src/contracts/arithmetic.ligo +++ b/src/contracts/arithmetic.ligo @@ -15,3 +15,6 @@ function div_op (const n : int) : int is function int_op (const n : nat) : int is block { skip } with int(n) + +function neg_op (const n : int) : int is + begin skip end with -n diff --git a/src/operators/helpers.ml b/src/operators/helpers.ml index 7982ddde0..8fd18a16f 100644 --- a/src/operators/helpers.ml +++ b/src/operators/helpers.ml @@ -70,6 +70,33 @@ module Typer = struct | _ -> fail @@ wrong_param_number s 3 lst let typer_3 name f : typer = (name , typer'_3 name f) + let typer'_4 : name -> (type_value -> type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ -> + match lst with + | [ a ; b ; c ; d ] -> ( + let%bind tv' = f a b c d in + ok (s , tv') + ) + | _ -> fail @@ wrong_param_number s 4 lst + let typer_4 name f : typer = (name , typer'_4 name f) + + let typer'_5 : name -> (type_value -> type_value -> type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ -> + match lst with + | [ a ; b ; c ; d ; e ] -> ( + let%bind tv' = f a b c d e in + ok (s , tv') + ) + | _ -> fail @@ wrong_param_number s 5 lst + let typer_5 name f : typer = (name , typer'_5 name f) + + let typer'_6 : name -> (type_value -> type_value -> type_value -> type_value -> type_value -> type_value -> type_value result) -> typer' = fun s f lst _ -> + match lst with + | [ a ; b ; c ; d ; e ; f_ ] -> ( + let%bind tv' = f a b c d e f_ in + ok (s , tv') + ) + | _ -> fail @@ wrong_param_number s 6 lst + let typer_6 name f : typer = (name , typer'_6 name f) + let constant name cst = typer_0 name (fun _ -> ok cst) open Combinators @@ -77,6 +104,8 @@ module Typer = struct let eq_1 a cst = type_value_eq (a , cst) let eq_2 (a , b) cst = type_value_eq (a , cst) && type_value_eq (b , cst) + let assert_eq_1 a b = Assert.assert_true (eq_1 a b) + let comparator : string -> typer = fun s -> typer_2 s @@ fun a b -> let%bind () = trace_strong (error_uncomparable_types a b) @@ @@ -114,8 +143,14 @@ module Compiler = struct | Unary of michelson | Binary of michelson | Ternary of michelson + | Tetrary of michelson + | Pentary of michelson + | Hexary of michelson let simple_constant c = Constant c let simple_unary c = Unary c let simple_binary c = Binary c let simple_ternary c = Ternary c + let simple_tetrary c = Tetrary c + let simple_pentary c = Pentary c + let simple_hexary c = Hexary c end diff --git a/src/operators/operators.ml b/src/operators/operators.ml index 70fc01986..6a85aaa37 100644 --- a/src/operators/operators.ml +++ b/src/operators/operators.ml @@ -91,7 +91,7 @@ module Simplify = struct module Ligodity = struct let constants = [ ("assert" , "ASSERT") ; - + ("Current.balance", "BALANCE") ; ("balance", "BALANCE") ; ("Current.time", "NOW") ; @@ -132,7 +132,7 @@ module Simplify = struct ("Map.update" , "MAP_UPDATE") ; ("Map.add" , "MAP_ADD") ; ("Map.remove" , "MAP_REMOVE") ; - + ("String.length", "SIZE") ; ("String.size", "SIZE") ; ("String.slice", "SLICE") ; @@ -196,6 +196,8 @@ module Typer = struct then ok @@ t_int () else if (eq_2 (a , b) (t_timestamp ())) then ok @@ t_int () else + if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) + then ok @@ t_timestamp () else if (eq_2 (a , b) (t_tez ())) then ok @@ t_tez () else fail (simple_error "Typing substraction, bad parameters.") @@ -220,7 +222,7 @@ module Typer = struct let%bind () = assert_type_value_eq (dst, v') in ok m - let map_mem : typer = typer_2 "MAP_MEM_TODO" @@ fun k m -> + let map_mem : typer = typer_2 "MAP_MEM" @@ fun k m -> let%bind (src, _dst) = get_t_map m in let%bind () = assert_type_value_eq (src, k) in ok @@ t_bool () @@ -235,46 +237,77 @@ module Typer = struct let%bind () = assert_type_value_eq (src, k) in ok @@ t_option dst () - let map_fold : typer = typer_3 "MAP_FOLD_TODO" @@ fun f m acc -> - let%bind (src, dst) = get_t_map m in - let expected_f_type = t_function (t_tuple [(t_tuple [src ; dst] ()) ; acc] ()) acc () in - let%bind () = assert_type_value_eq (f, expected_f_type) in - ok @@ acc - - let map_map : typer = typer_2 "MAP_MAP_TODO" @@ fun f m -> + let map_iter : typer = typer_2 "MAP_ITER" @@ fun f m -> let%bind (k, v) = get_t_map m in - let%bind (input_type, result_type) = get_t_function f in - let%bind () = assert_type_value_eq (input_type, t_tuple [k ; v] ()) in - ok @@ t_map k result_type () - - let map_map_fold : typer = typer_3 "MAP_MAP_TODO" @@ fun f m acc -> - let%bind (k, v) = get_t_map m in - let%bind (input_type, result_type) = get_t_function f in - let%bind () = assert_type_value_eq (input_type, t_tuple [t_tuple [k ; v] () ; acc] ()) in - let%bind ttuple = get_t_tuple result_type in - match ttuple with - | [result_acc ; result_dst ] -> - ok @@ t_tuple [ t_map k result_dst () ; result_acc ] () - (* TODO: error message *) - | _ -> fail @@ simple_error "function passed to map should take (k * v) * acc as an argument" - - let map_iter : typer = typer_2 "MAP_MAP_TODO" @@ fun f m -> - let%bind (k, v) = get_t_map m in - let%bind () = assert_type_value_eq (f, t_function (t_tuple [k ; v] ()) (t_unit ()) ()) in + let%bind (arg_1 , res) = get_t_function f in + let%bind (arg_2 , res') = get_t_function res in + let%bind () = assert_eq_1 arg_1 k in + let%bind () = assert_eq_1 arg_2 v in + let%bind () = assert_eq_1 res' (t_unit ()) in ok @@ t_unit () + let map_map : typer = typer_2 "MAP_MAP" @@ fun f m -> + let%bind (k, v) = get_t_map m in + let%bind (arg_1 , res) = get_t_function f in + let%bind (arg_2 , res') = get_t_function res in + let%bind () = assert_eq_1 arg_1 k in + let%bind () = assert_eq_1 arg_2 v in + ok @@ res' + + let map_fold : typer = typer_2 "MAP_FOLD" @@ fun f m -> + let%bind (k, v) = get_t_map m in + let%bind (arg_1 , res) = get_t_function f in + let%bind (arg_2 , res') = get_t_function res in + let%bind (arg_3 , res'') = get_t_function res' in + let%bind () = assert_eq_1 arg_1 k in + let%bind () = assert_eq_1 arg_2 v in + let%bind () = assert_eq_1 arg_3 res'' in + ok @@ res' + + let big_map_remove : typer = typer_2 "BIG_MAP_REMOVE" @@ fun k m -> + let%bind (src , _) = get_t_big_map m in + let%bind () = assert_type_value_eq (src , k) in + ok m + + let big_map_add : typer = typer_3 "BIG_MAP_ADD" @@ fun k v m -> + let%bind (src, dst) = get_t_big_map m in + let%bind () = assert_type_value_eq (src, k) in + let%bind () = assert_type_value_eq (dst, v) in + ok m + + let big_map_update : typer = typer_3 "BIG_MAP_UPDATE" @@ fun k v m -> + let%bind (src, dst) = get_t_big_map m in + let%bind () = assert_type_value_eq (src, k) in + let%bind v' = get_t_option v in + let%bind () = assert_type_value_eq (dst, v') in + ok m + + let big_map_mem : typer = typer_2 "BIG_MAP_MEM" @@ fun k m -> + let%bind (src, _dst) = get_t_big_map m in + let%bind () = assert_type_value_eq (src, k) in + ok @@ t_bool () + + let big_map_find : typer = typer_2 "BIG_MAP_FIND" @@ fun k m -> + let%bind (src, dst) = get_t_big_map m in + let%bind () = assert_type_value_eq (src, k) in + ok @@ dst + + let size = typer_1 "SIZE" @@ fun t -> let%bind () = Assert.assert_true @@ - (is_t_map t || is_t_list t || is_t_string t) in + (is_t_map t || is_t_list t || is_t_string t || is_t_bytes t || is_t_set t || is_t_big_map t) in ok @@ t_nat () let slice = typer_3 "SLICE" @@ fun i j s -> - let%bind () = - Assert.assert_true @@ - (is_t_nat i && is_t_nat j && is_t_string s) in - ok @@ t_string () - + let%bind () = assert_eq_1 i (t_nat ()) in + let%bind () = assert_eq_1 j (t_nat ()) in + if eq_1 s (t_string ()) + then ok @@ t_string () + else if eq_1 s (t_bytes ()) + then ok @@ t_bytes () + else simple_fail "bad slice" + let failwith_ = typer_1 "FAILWITH" @@ fun t -> let%bind () = Assert.assert_true @@ @@ -319,7 +352,7 @@ module Typer = struct let%bind () = assert_t_signature s in let%bind () = assert_t_bytes b in ok @@ t_bool () - + let sender = constant "SENDER" @@ t_address () let source = constant "SOURCE" @@ t_address () @@ -328,6 +361,8 @@ module Typer = struct let amount = constant "AMOUNT" @@ t_tez () + let balance = constant "BALANCE" @@ t_tez () + let address = constant "ADDRESS" @@ t_address () let now = constant "NOW" @@ t_timestamp () @@ -338,6 +373,19 @@ module Typer = struct let%bind () = assert_type_value_eq (param , contract_param) in ok @@ t_operation () + let originate = typer_6 "ORIGINATE" @@ fun manager delegate_opt spendable delegatable init_balance code -> + let%bind () = assert_eq_1 manager (t_key_hash ()) in + let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in + let%bind () = assert_eq_1 spendable (t_bool ()) in + let%bind () = assert_eq_1 delegatable (t_bool ()) in + let%bind () = assert_t_tez init_balance in + let%bind (arg , res) = get_t_function code in + let%bind (_param , storage) = get_t_pair arg in + let%bind (storage' , op_lst) = get_t_pair res in + let%bind () = assert_eq_1 storage storage' in + let%bind () = assert_eq_1 op_lst (t_list (t_operation ()) ()) in + ok @@ (t_pair (t_operation ()) (t_address ()) ()) + let get_contract = typer_1_opt "CONTRACT" @@ fun _ tv_opt -> let%bind tv = trace_option (simple_error "get_contract needs a type annotation") tv_opt in @@ -346,15 +394,23 @@ module Typer = struct get_t_contract tv in ok @@ t_contract tv' () + let set_delegate = typer_1 "SET_DELEGATE" @@ fun delegate_opt -> + let%bind () = assert_eq_1 delegate_opt (t_option (t_key_hash ()) ()) in + ok @@ t_operation () + let abs = typer_1 "ABS" @@ fun t -> let%bind () = assert_t_int t in ok @@ t_nat () + let neg = typer_1 "NEG" @@ fun t -> + let%bind () = Assert.assert_true (eq_1 t (t_nat ()) || eq_1 t (t_int ())) in + ok @@ t_int () + let assertion = typer_1 "ASSERT" @@ fun a -> if eq_1 a (t_bool ()) then ok @@ t_unit () else simple_fail "Asserting a non-bool" - + let times = typer_2 "TIMES" @@ fun a b -> if eq_2 (a , b) (t_nat ()) then ok @@ t_nat () else @@ -387,6 +443,8 @@ module Typer = struct then ok @@ t_tez () else if (eq_1 a (t_nat ()) && eq_1 b (t_int ())) || (eq_1 b (t_nat ()) && eq_1 a (t_int ())) then ok @@ t_int () else + if (eq_1 a (t_timestamp ()) && eq_1 b (t_int ())) || (eq_1 b (t_timestamp ()) && eq_1 a (t_int ())) + then ok @@ t_timestamp () else simple_fail "Adding with wrong types. Expected nat, int or tez." let set_mem = typer_2 "SET_MEM" @@ fun elt set -> @@ -407,11 +465,79 @@ module Typer = struct then ok set else simple_fail "Set_remove: elt and set don't match" + let set_iter = typer_2 "SET_ITER" @@ fun set body -> + let%bind (arg , res) = get_t_function body in + let%bind () = Assert.assert_true (eq_1 res (t_unit ())) in + let%bind key = get_t_set set in + if eq_1 key arg + then ok (t_unit ()) + else simple_fail "bad set iter" + + let list_iter = typer_2 "LIST_ITER" @@ fun lst body -> + let%bind (arg , res) = get_t_function body in + let%bind () = Assert.assert_true (eq_1 res (t_unit ())) in + let%bind key = get_t_list lst in + if eq_1 key arg + then ok (t_unit ()) + else simple_fail "bad list iter" + + let list_map = typer_2 "LIST_MAP" @@ fun lst body -> + let%bind (arg , res) = get_t_function body in + let%bind key = get_t_list lst in + if eq_1 key arg + then ok res + else simple_fail "bad list iter" + let not_ = typer_1 "NOT" @@ fun elt -> if eq_1 elt (t_bool ()) then ok @@ t_bool () + else if eq_1 elt (t_nat ()) || eq_1 elt (t_int ()) + then ok @@ t_int () else simple_fail "bad parameter to not" - + + let or_ = typer_2 "OR" @@ fun a b -> + if eq_2 (a , b) (t_bool ()) + then ok @@ t_bool () + else if eq_2 (a , b) (t_nat ()) + then ok @@ t_nat () + else simple_fail "bad or" + + let xor = typer_2 "XOR" @@ fun a b -> + if eq_2 (a , b) (t_bool ()) + then ok @@ t_bool () + else if eq_2 (a , b) (t_nat ()) + then ok @@ t_nat () + else simple_fail "bad xor" + + let and_ = typer_2 "AND" @@ fun a b -> + if eq_2 (a , b) (t_bool ()) + then ok @@ t_bool () + else if eq_2 (a , b) (t_nat ()) || (eq_1 b (t_nat ()) && eq_1 a (t_int ())) + then ok @@ t_nat () + else simple_fail "bad end" + + let lsl_ = typer_2 "LSL" @@ fun a b -> + if eq_2 (a , b) (t_nat ()) + then ok @@ t_nat () + else simple_fail "bad lsl" + + let lsr_ = typer_2 "LSR" @@ fun a b -> + if eq_2 (a , b) (t_nat ()) + then ok @@ t_nat () + else simple_fail "bad lsr" + + let concat = typer_2 "CONCAT" @@ fun a b -> + if eq_2 (a , b) (t_string ()) + then ok @@ t_string () + else if eq_2 (a , b) (t_bytes ()) + then ok @@ t_bytes () + else simple_fail "bad concat" + + let cons = typer_2 "CONS" @@ fun hd tl -> + let%bind elt = get_t_list tl in + let%bind () = assert_eq_1 hd elt in + ok tl + let constant_typers = Map.String.of_list [ add ; times ; @@ -428,20 +554,19 @@ module Typer = struct comparator "GE" ; boolean_operator_2 "OR" ; boolean_operator_2 "AND" ; + boolean_operator_2 "XOR" ; not_ ; map_remove ; map_add ; map_update ; map_mem ; map_find ; - map_map_fold ; map_map ; map_fold ; map_iter ; set_mem ; set_add ; set_remove ; - (* map_size ; (* use size *) *) int ; size ; failwith_ ; @@ -459,6 +584,7 @@ module Typer = struct amount ; transaction ; get_contract ; + neg ; abs ; now ; slice ; @@ -539,5 +665,5 @@ module Compiler = struct ] (* Some complex predicates will need to be added in compiler/compiler_program *) - + end diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index 2f3299cc3..6542473d4 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -468,12 +468,11 @@ let rec simpl_expression (t:Raw.expr) : expr result = return @@ e_literal ~loc (Literal_nat n) ) | EArith (Mtz n) -> ( - let (n , loc) = r_split n in - let n = Z.to_int @@ snd @@ n in - return @@ e_literal ~loc (Literal_tez n) - ) - | EArith _ as e -> - fail @@ unsupported_arith_op e + let (n , loc) = r_split n in + let n = Z.to_int @@ snd @@ n in + return @@ e_literal ~loc (Literal_tez n) + ) + | EArith (Neg e) -> simpl_unop "NEG" e | EString (String s) -> let (s , loc) = r_split s in let s' = diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 55445db99..2f4af5adb 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -127,7 +127,6 @@ let arithmetic () : unit result = ("plus_op", fun n -> (n + 42)) ; ("minus_op", fun n -> (n - 42)) ; ("times_op", fun n -> (n * 42)) ; - (* ("div_op", fun n -> (n / 2)) ; *) ] in let%bind () = expect_eq_n_pos program "int_op" e_nat e_int in let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in From 5c3d801c78e120e4ca1f619d9d9298896cf0d65d Mon Sep 17 00:00:00 2001 From: galfour Date: Fri, 19 Jul 2019 12:42:01 +0200 Subject: [PATCH 5/9] add bitwise arithmetic and string arithmetic tests --- src/compiler/compiler_program.ml | 2 -- src/contracts/bitwise_arithmetic.ligo | 8 ++++++++ src/contracts/string_arithmetic.ligo | 5 +++++ src/operators/operators.ml | 16 +++++++++++---- src/test/integration_tests.ml | 28 +++++++++++++++++++++++++++ src/test/test_helpers.ml | 13 ++++++++++++- 6 files changed, 65 insertions(+), 7 deletions(-) create mode 100644 src/contracts/bitwise_arithmetic.ligo create mode 100644 src/contracts/string_arithmetic.ligo diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index f7f0f50a3..986b675a9 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -185,8 +185,6 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m | E_environment_return expr -> ( let%bind (expr' , env) = translate_expression ~push_var_name:"return_clause" expr env in let%bind (code , cleared_env) = Compiler_environment.clear env in - Format.printf "pre env %a\n" PP.environment env ; - Format.printf "post clean env %a\n" PP.environment cleared_env ; return ~end_env:cleared_env @@ seq [ expr' ; code ; diff --git a/src/contracts/bitwise_arithmetic.ligo b/src/contracts/bitwise_arithmetic.ligo new file mode 100644 index 000000000..0711b5854 --- /dev/null +++ b/src/contracts/bitwise_arithmetic.ligo @@ -0,0 +1,8 @@ +function or_op (const n : nat) : nat is + begin skip end with bitwise_or(n , 4n) + +function and_op (const n : nat) : nat is + begin skip end with bitwise_and(n , 7n) + +function xor_op (const n : nat) : nat is + begin skip end with bitwise_xor(n , 7n) diff --git a/src/contracts/string_arithmetic.ligo b/src/contracts/string_arithmetic.ligo new file mode 100644 index 000000000..c8ceacb01 --- /dev/null +++ b/src/contracts/string_arithmetic.ligo @@ -0,0 +1,5 @@ +function concat_op (const s : string) : string is + begin skip end with string_concat(s , "toto") + +function slice_op (const s : string) : string is + begin skip end with string_slice(1n , 2n , s) diff --git a/src/operators/operators.ml b/src/operators/operators.ml index 6a85aaa37..7f69f392b 100644 --- a/src/operators/operators.ml +++ b/src/operators/operators.ml @@ -69,6 +69,11 @@ module Simplify = struct ("source" , "SOURCE") ; ("sender" , "SENDER") ; ("failwith" , "FAILWITH") ; + ("bitwise_or" , "OR") ; + ("bitwise_and" , "AND") ; + ("bitwise_xor" , "XOR") ; + ("string_concat" , "CONCAT") ; + ("string_slice" , "SLICE") ; ] let type_constants = type_constants @@ -546,15 +551,17 @@ module Typer = struct sub ; none ; some ; + concat ; + slice ; comparator "EQ" ; comparator "NEQ" ; comparator "LT" ; comparator "GT" ; comparator "LE" ; comparator "GE" ; - boolean_operator_2 "OR" ; - boolean_operator_2 "AND" ; - boolean_operator_2 "XOR" ; + or_ ; + and_ ; + xor ; not_ ; map_remove ; map_add ; @@ -655,13 +662,14 @@ module Compiler = struct ("MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ; ("SET_MEM" , simple_binary @@ prim I_MEM) ; ("SET_ADD" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_True)) ; prim I_UPDATE]) ; - ("SLICE" , simple_ternary @@ prim I_SLICE) ; + ("SLICE" , simple_ternary @@ seq [prim I_SLICE ; i_assert_some_msg (i_push_string "SLICE")]) ; ("SHA256" , simple_unary @@ prim I_SHA256) ; ("SHA512" , simple_unary @@ prim I_SHA512) ; ("BLAKE2B" , simple_unary @@ prim I_BLAKE2B) ; ("CHECK_SIGNATURE" , simple_ternary @@ prim I_CHECK_SIGNATURE) ; ("HASH_KEY" , simple_unary @@ prim I_HASH_KEY) ; ("PACK" , simple_unary @@ prim I_PACK) ; + ("CONCAT" , simple_binary @@ prim I_CONCAT) ; ] (* Some complex predicates will need to be added in compiler/compiler_program *) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 2f4af5adb..29235f2a7 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -127,12 +127,38 @@ let arithmetic () : unit result = ("plus_op", fun n -> (n + 42)) ; ("minus_op", fun n -> (n - 42)) ; ("times_op", fun n -> (n * 42)) ; + ("neg_op", fun n -> (-n)) ; ] in let%bind () = expect_eq_n_pos program "int_op" e_nat e_int in let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in let%bind () = expect_eq_n_pos program "div_op" e_int (fun n -> e_int (n / 2)) in ok () +let bitwise_arithmetic () : unit result = + let%bind program = type_file "./contracts/bitwise_arithmetic.ligo" in + let%bind () = expect_eq program "or_op" (e_nat 7) (e_nat 7) in + let%bind () = expect_eq program "or_op" (e_nat 3) (e_nat 7) in + let%bind () = expect_eq program "or_op" (e_nat 2) (e_nat 6) in + let%bind () = expect_eq program "or_op" (e_nat 14) (e_nat 14) in + let%bind () = expect_eq program "or_op" (e_nat 10) (e_nat 14) in + let%bind () = expect_eq program "and_op" (e_nat 7) (e_nat 7) in + let%bind () = expect_eq program "and_op" (e_nat 3) (e_nat 3) in + let%bind () = expect_eq program "and_op" (e_nat 2) (e_nat 2) in + let%bind () = expect_eq program "and_op" (e_nat 14) (e_nat 6) in + let%bind () = expect_eq program "and_op" (e_nat 10) (e_nat 2) in + let%bind () = expect_eq program "xor_op" (e_nat 0) (e_nat 7) in + let%bind () = expect_eq program "xor_op" (e_nat 7) (e_nat 0) in + ok () + +let string_arithmetic () : unit result = + let%bind program = type_file "./contracts/string_arithmetic.ligo" in + let%bind () = expect_eq program "concat_op" (e_string "foo") (e_string "foototo") in + let%bind () = expect_eq program "concat_op" (e_string "") (e_string "toto") in + let%bind () = expect_eq program "slice_op" (e_string "tata") (e_string "at") in + let%bind () = expect_eq program "slice_op" (e_string "foo") (e_string "oo") in + let%bind () = expect_fail program "slice_op" (e_string "ba") in + ok () + let unit_expression () : unit result = let%bind program = type_file "./contracts/unit.ligo" in expect_eq_evaluate program "u" (e_unit ()) @@ -562,6 +588,8 @@ let main = test_suite "Integration (End to End)" [ test "multiple parameters" multiple_parameters ; test "bool" bool_expression ; test "arithmetic" arithmetic ; + test "bitiwse_arithmetic" bitwise_arithmetic ; + test "string_arithmetic" string_arithmetic ; test "unit" unit_expression ; test "string" string_expression ; test "option" option ; diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index f178adcd2..e2f8896ce 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -49,7 +49,7 @@ let test name f = ) let test_suite name lst = Test_suite (name , lst) - + open Ast_simplified.Combinators let expect ?options program entry_point input expecter = @@ -62,6 +62,17 @@ let expect ?options program entry_point input expecter = Ligo.Run.run_simplityped ~debug_michelson:true ?options program entry_point input in expecter result +let expect_fail ?options program entry_point input = + let run_error = + let title () = "expect run" in + let content () = Format.asprintf "Entry_point: %s" entry_point in + error title content + in + trace run_error @@ + Assert.assert_fail + @@ Ligo.Run.run_simplityped ~debug_michelson:true ?options program entry_point input + + let expect_eq ?options program entry_point input expected = let expecter = fun result -> let expect_error = From 33101820ec907f0f7beac9a78af523f3e02f7fd9 Mon Sep 17 00:00:00 2001 From: galfour Date: Fri, 19 Jul 2019 14:35:47 +0200 Subject: [PATCH 6/9] add set tests --- src/compiler/compiler_program.ml | 11 +++++-- src/contracts/set_arithmetic.ligo | 15 +++++++++ src/main/run_mini_c.ml | 8 ++++- src/operators/operators.ml | 14 +++++++- src/simplify/pascaligo.ml | 17 +++++++++- src/test/integration_tests.ml | 32 +++++++++++++++++-- src/test/test_helpers.ml | 8 ++++- src/transpiler/transpiler.ml | 4 +-- vendors/ligo-utils/proto-alpha-utils/trace.ml | 8 +++-- 9 files changed, 104 insertions(+), 13 deletions(-) create mode 100644 src/contracts/set_arithmetic.ligo diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 986b675a9..26f6255bc 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -26,6 +26,11 @@ let get_predicate : string -> type_value -> expression list -> predicate result let%bind m_ty = Compiler_type.type_ ty' in ok @@ simple_unary @@ prim ~children:[m_ty] I_NIL ) + | "SET_EMPTY" -> ( + let%bind ty' = Mini_c.get_t_set ty in + let%bind m_ty = Compiler_type.type_ ty' in + ok @@ simple_constant @@ prim ~children:[m_ty] I_EMPTY_SET + ) | "UNPACK" -> ( let%bind ty' = Mini_c.get_t_option ty in let%bind m_ty = Compiler_type.type_ ty' in @@ -86,14 +91,16 @@ let rec translate_value (v:value) : michelson result = match v with ok @@ prim ~children:[s'] D_Some | D_map lst -> let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in + let sorted = List.sort (fun (x , _) (y , _) -> compare x y) lst' in let aux (a, b) = prim ~children:[a;b] D_Elt in - ok @@ seq @@ List.map aux lst' + ok @@ seq @@ List.map aux sorted | D_list lst -> let%bind lst' = bind_map_list translate_value lst in ok @@ seq lst' | D_set lst -> let%bind lst' = bind_map_list translate_value lst in - ok @@ seq lst' + let sorted = List.sort compare lst' in + ok @@ seq sorted | D_operation _ -> simple_fail "can't compile an operation" diff --git a/src/contracts/set_arithmetic.ligo b/src/contracts/set_arithmetic.ligo new file mode 100644 index 000000000..e4c686310 --- /dev/null +++ b/src/contracts/set_arithmetic.ligo @@ -0,0 +1,15 @@ +const s_e : set(string) = (set_empty : set(string)) + +const s_fb : set(string) = set [ + "foo" ; + "bar" ; +] + +function add_op (const s : set(string)) : set(string) is + begin skip end with set_add("foobar" , s) + +function remove_op (const s : set(string)) : set(string) is + begin skip end with set_remove("foobar" , s) + +function mem_op (const s : set(string)) : bool is + begin skip end with set_mem("foobar" , s) diff --git a/src/main/run_mini_c.ml b/src/main/run_mini_c.ml index 17fc40ba2..24a38b489 100644 --- a/src/main/run_mini_c.ml +++ b/src/main/run_mini_c.ml @@ -32,8 +32,14 @@ let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:v error title content in trace error @@ translate_entry entry in - if debug_michelson then Format.printf "Program: %a\n" Michelson.pp compiled.body ; let%bind input_michelson = translate_value input in + if debug_michelson then ( + Format.printf "Program: %a\n" Michelson.pp compiled.body ; + Format.printf "Expression: %a\n" PP.expression entry.result ; + Format.printf "Input: %a\n" PP.value input ; + Format.printf "Input Type: %a\n" PP.type_ entry.input ; + Format.printf "Compiled Input: %a\n" Michelson.pp input_michelson ; + ) ; let%bind ex_ty_value = run_aux ?options compiled input_michelson in let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in ok result diff --git a/src/operators/operators.ml b/src/operators/operators.ml index 7f69f392b..4fad1501d 100644 --- a/src/operators/operators.ml +++ b/src/operators/operators.ml @@ -74,6 +74,11 @@ module Simplify = struct ("bitwise_xor" , "XOR") ; ("string_concat" , "CONCAT") ; ("string_slice" , "SLICE") ; + ("set_empty" , "SET_EMPTY") ; + ("set_mem" , "SET_MEM") ; + ("set_add" , "SET_ADD") ; + ("set_remove" , "SET_REMOVE") ; + ("set_iter" , "SET_ITER") ; ] let type_constants = type_constants @@ -194,6 +199,11 @@ module Typer = struct | None -> simple_fail "untyped NONE" | Some t -> ok t + let set_empty = typer_0 "SET_EMPTY" @@ fun tv_opt -> + match tv_opt with + | None -> simple_fail "untyped SET_EMPTY" + | Some t -> ok t + let sub = typer_2 "SUB" @@ fun a b -> if (eq_2 (a , b) (t_int ())) then ok @@ t_int () else @@ -571,6 +581,7 @@ module Typer = struct map_map ; map_fold ; map_iter ; + set_empty ; set_mem ; set_add ; set_remove ; @@ -658,10 +669,11 @@ module Compiler = struct ("CALL" , simple_ternary @@ prim I_TRANSFER_TOKENS) ; ("SOURCE" , simple_constant @@ prim I_SOURCE) ; ("SENDER" , simple_constant @@ prim I_SENDER) ; - ("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ; + ("MAP_ADD" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE]) ; ("MAP_UPDATE" , simple_ternary @@ prim I_UPDATE) ; ("SET_MEM" , simple_binary @@ prim I_MEM) ; ("SET_ADD" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_True)) ; prim I_UPDATE]) ; + ("SET_REMOVE" , simple_binary @@ seq [dip (i_push (prim T_bool) (prim D_False)) ; prim I_UPDATE]) ; ("SLICE" , simple_ternary @@ seq [prim I_SLICE ; i_assert_some_msg (i_push_string "SLICE")]) ; ("SHA256" , simple_unary @@ prim I_SHA256) ; ("SHA512" , simple_unary @@ prim I_SHA512) ; diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index 6542473d4..51aacac92 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -484,7 +484,7 @@ let rec simpl_expression (t:Raw.expr) : expr result = fail @@ unsupported_string_catenation e | ELogic l -> simpl_logic_expression l | EList l -> simpl_list_expression l - | ESet _ -> fail @@ unsupported_set_expr t + | ESet s -> simpl_set_expression s | ECase c -> ( let (c , loc) = r_split c in let%bind e = simpl_expression c.expr in @@ -571,6 +571,21 @@ and simpl_list_expression (t:Raw.list_expr) : expression result = return @@ e_list ~loc [] ) +and simpl_set_expression (t:Raw.set_expr) : expression result = + match t with + | SetMem x -> ( + let (x' , loc) = r_split x in + let%bind set' = simpl_expression x'.set in + let%bind element' = simpl_expression x'.element in + ok @@ e_constant ~loc "SET_MEM" [ element' ; set' ] + ) + | SetInj x -> ( + let (x' , loc) = r_split x in + let elements = pseq_to_list x'.elements in + let%bind elements' = bind_map_list simpl_expression elements in + ok @@ e_set ~loc elements' + ) + and simpl_binop (name:string) (t:_ Raw.bin_op Region.reg) : expression result = let return x = ok x in let (t , loc) = r_split t in diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 29235f2a7..bd49a31b9 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -159,6 +159,34 @@ let string_arithmetic () : unit result = let%bind () = expect_fail program "slice_op" (e_string "ba") in ok () +let set_arithmetic () : unit result = + let%bind program = type_file "./contracts/set_arithmetic.ligo" in + let%bind () = + expect_eq program "add_op" + (e_set [e_string "foo" ; e_string "bar"]) + (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) in + let%bind () = + expect_eq program "add_op" + (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) + (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) in + let%bind () = + expect_eq program "remove_op" + (e_set [e_string "foo" ; e_string "bar"]) + (e_set [e_string "foo" ; e_string "bar"]) in + let%bind () = + expect_eq program "remove_op" + (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) + (e_set [e_string "foo" ; e_string "bar"]) in + let%bind () = + expect_eq program "mem_op" + (e_set [e_string "foo" ; e_string "bar" ; e_string "foobar"]) + (e_bool true) in + let%bind () = + expect_eq program "mem_op" + (e_set [e_string "foo" ; e_string "bar"]) + (e_bool false) in + ok () + let unit_expression () : unit result = let%bind program = type_file "./contracts/unit.ligo" in expect_eq_evaluate program "u" (e_unit ()) @@ -368,8 +396,7 @@ let loop () : unit result = let make_expected = fun n -> e_nat (n * (n + 1) / 2) in expect_eq_n_pos_mid program "sum" make_input make_expected in - ok() - + ok () let matching () : unit result = let%bind program = type_file "./contracts/match.ligo" in @@ -590,6 +617,7 @@ let main = test_suite "Integration (End to End)" [ test "arithmetic" arithmetic ; test "bitiwse_arithmetic" bitwise_arithmetic ; test "string_arithmetic" string_arithmetic ; + test "set_arithmetic" set_arithmetic ; test "unit" unit_expression ; test "string" string_expression ; test "option" option ; diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index e2f8896ce..32f45d4a4 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -32,7 +32,13 @@ let rec error_pp out (e : error) = | `Null -> "" | `List lst -> Format.asprintf "@[%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst | _ -> " " ^ (J.to_string infos) ^ "\n" in - Format.fprintf out "%s%s%s.\n%s%s" title error_code message data infos + let children = + let children = e |> member "children" in + match children with + | `Null -> "" + | `List lst -> Format.asprintf "@[%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst + | _ -> " " ^ (J.to_string children) ^ "\n" in + Format.fprintf out "%s%s%s.\n%s%s%s" title error_code message data infos children let test name f = diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index 88e7b5ad9..fcaf67815 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -372,7 +372,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re Mini_c.Combinators.get_t_set tv in let%bind lst' = bind_map_list (translate_annotated_expression) lst in let aux : expression -> expression -> expression result = fun prev cur -> - return @@ E_constant ("CONS", [cur ; prev]) in + return @@ E_constant ("SET_ADD", [cur ; prev]) in let%bind (init : expression) = return @@ E_make_empty_set t in bind_fold_list aux init lst' ) @@ -674,7 +674,7 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression | T_constant ("nat", []) -> ( let%bind n = trace_strong (wrong_mini_c_value "nat" v) @@ - get_nat v in + get_nat v in return (E_literal (Literal_nat n)) ) | T_constant ("timestamp", []) -> ( diff --git a/vendors/ligo-utils/proto-alpha-utils/trace.ml b/vendors/ligo-utils/proto-alpha-utils/trace.ml index 53cffe354..812ce0405 100644 --- a/vendors/ligo-utils/proto-alpha-utils/trace.ml +++ b/vendors/ligo-utils/proto-alpha-utils/trace.ml @@ -26,10 +26,12 @@ let trace_tzresult err = let trace_tzresult_r err_thunk_may_fail = function | Result.Ok x -> ok x - | Error _errs -> - (* let tz_errs = List.map of_tz_error errs in *) + | Error errs -> + let tz_errs = List.map of_tz_error errs in match err_thunk_may_fail () with - | Simple_utils.Trace.Ok (err, annotations) -> ignore annotations; Error (err) + | Simple_utils.Trace.Ok (err, annotations) -> + ignore annotations ; + Error (fun () -> patch_children tz_errs (err ())) | Error errors_while_generating_error -> (* TODO: the complexity could be O(n*n) in the worst case, this should use some catenable lists. *) From 9dd8e63cbfdcfdbfa378514e1e244858f9b5a2ae Mon Sep 17 00:00:00 2001 From: galfour Date: Sat, 20 Jul 2019 13:46:42 +0200 Subject: [PATCH 7/9] add iter for set and lists --- src/compiler/compiler_program.ml | 32 ++++++++- src/contracts/list.ligo | 10 +++ src/contracts/set_arithmetic.ligo | 11 +++ src/mini_c/PP.ml | 2 + src/mini_c/types.ml | 1 + src/operators/operators.ml | 3 + src/simplify/pascaligo.ml | 25 +++++-- src/test/integration_tests.ml | 8 +++ src/transpiler/transpiler.ml | 67 ++++++++++++++++--- vendors/ligo-utils/tezos-utils/x_michelson.ml | 2 + 10 files changed, 145 insertions(+), 16 deletions(-) diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 26f6255bc..6da10d7c5 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -19,7 +19,7 @@ let get_predicate : string -> type_value -> expression list -> predicate result | "NONE" -> ( let%bind ty' = Mini_c.get_t_option ty in let%bind m_ty = Compiler_type.type_ ty' in - ok @@ simple_unary @@ prim ~children:[m_ty] I_NONE + ok @@ simple_constant @@ prim ~children:[m_ty] I_NONE ) | "NIL" -> ( let%bind ty' = Mini_c.get_t_list ty in @@ -380,6 +380,36 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m ]) in return code ) + | E_iterator (name , (v , body) , expr) -> ( + let%bind (expr' , expr_env) = translate_expression ~push_var_name:"iter_expr" expr env in + let%bind popped = Compiler_environment.pop expr_env in + let%bind env' = ok @@ Environment.add v popped in + let%bind (body' , body_env) = translate_expression ~push_var_name:"iter_body" body env' in + match name with + | "ITER" -> ( + let%bind restrict = + Compiler_environment.select_env body_env popped in + let%bind code = ok (seq [ + expr' ; + i_iter (seq [body' ; restrict]) ; + ]) in + return ~end_env:popped code + ) + | "MAP" -> ( + 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' ; + i_map (seq [body' ; restrict]) ; + ]) in + return code + ) + | s -> ( + let error = error (thunk "bad iterator") (thunk s) in + fail error + ) + ) | E_assignment (name , lrs , expr) -> ( let%bind (expr' , env') = translate_expression ~push_var_name:"assignment_expr" expr env in let%bind get_code = Compiler_environment.get env' name in diff --git a/src/contracts/list.ligo b/src/contracts/list.ligo index 60af05003..503d72ffb 100644 --- a/src/contracts/list.ligo +++ b/src/contracts/list.ligo @@ -17,3 +17,13 @@ const bl : foobar = list 120 ; 421 ; end + +function iter_op (const s : list(int)) : int is + var r : int := 0 ; + function aggregate (const i : int) : unit is + begin + r := r + i ; + end with unit + begin + list_iter(s , aggregate) ; + end with r diff --git a/src/contracts/set_arithmetic.ligo b/src/contracts/set_arithmetic.ligo index e4c686310..814120c0c 100644 --- a/src/contracts/set_arithmetic.ligo +++ b/src/contracts/set_arithmetic.ligo @@ -1,3 +1,13 @@ +function iter_op (const s : set(int)) : int is + var r : int := 0 ; + function aggregate (const i : int) : unit is + begin + r := r + i ; + end with unit + begin + set_iter(s , aggregate) ; + end with r + const s_e : set(string) = (set_empty : set(string)) const s_fb : set(string) = set [ @@ -13,3 +23,4 @@ function remove_op (const s : set(string)) : set(string) is function mem_op (const s : set(string)) : bool is begin skip end with set_mem("foobar" , s) + diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml index bf848723b..3d0e3f065 100644 --- a/src/mini_c/PP.ml +++ b/src/mini_c/PP.ml @@ -86,6 +86,8 @@ and expression' ppf (e:expression') = match e with | E_sequence (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_iterator (s , ((name , _) , body) , expr) -> + fprintf ppf "for_%s %s of %a do ( %a )" s 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) -> diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml index 77fa0a026..3e9a69819 100644 --- a/src/mini_c/types.ml +++ b/src/mini_c/types.ml @@ -69,6 +69,7 @@ and expression' = | E_make_empty_list of type_value | E_make_empty_set of type_value | E_make_none of type_value + | E_iterator of (string * ((var_name * type_value) * expression) * expression) | E_if_bool of expression * expression * expression | E_if_none of expression * expression * ((var_name * type_value) * expression) | E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression) diff --git a/src/operators/operators.ml b/src/operators/operators.ml index 4fad1501d..befd3b961 100644 --- a/src/operators/operators.ml +++ b/src/operators/operators.ml @@ -79,6 +79,7 @@ module Simplify = struct ("set_add" , "SET_ADD") ; ("set_remove" , "SET_REMOVE") ; ("set_iter" , "SET_ITER") ; + ("list_iter" , "LIST_ITER") ; ] let type_constants = type_constants @@ -585,6 +586,8 @@ module Typer = struct set_mem ; set_add ; set_remove ; + set_iter ; + list_iter ; int ; size ; failwith_ ; diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml index 51aacac92..59667f39a 100644 --- a/src/simplify/pascaligo.ml +++ b/src/simplify/pascaligo.ml @@ -135,7 +135,7 @@ module Errors = struct let unsupported_for_loops region = let title () = "bounded iterators" in let message () = - Format.asprintf "for loops are not supported yet" in + Format.asprintf "only simple for loops are supported yet" in let data = [ ("loop_loc", fun () -> Format.asprintf "%a" Location.pp_lift @@ region) @@ -744,8 +744,19 @@ and simpl_statement : Raw.statement -> (_ -> expression result) result = and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) result = fun t -> match t with - | ProcCall call -> - fail @@ unsupported_proc_calls call + | ProcCall x -> ( + let ((name, args) , loc) = r_split x in + let (f , f_loc) = r_split name in + let (args , args_loc) = r_split args in + let args' = npseq_to_list args.inside in + match List.assoc_opt f constants with + | None -> + let%bind arg = simpl_tuple_expression ~loc:args_loc args' in + return @@ e_application ~loc (e_variable ~loc:f_loc f) arg + | Some s -> + let%bind lst = bind_map_list simpl_expression args' in + return @@ e_constant ~loc s lst + ) | Fail e -> ( let%bind expr = simpl_expression e.value.fail_expr in return @@ e_failwith expr @@ -760,7 +771,13 @@ and simpl_single_instruction : Raw.single_instr -> (_ -> expression result) resu let%bind body = simpl_block l.block.value in let%bind body = body None in return @@ e_loop cond body - | Loop (For (ForInt {region; _} | ForCollect {region; _})) -> + (* | Loop (For (ForCollect x)) -> ( + * let (x' , loc) = r_split x in + * let%bind expr = simpl_expression x'.expr in + * let%bind body = simpl_block x'.block.value in + * ok _ + * ) *) + | Loop (For (ForInt {region; _} | ForCollect {region ; _})) -> fail @@ unsupported_for_loops region | Cond c -> ( let (c , loc) = r_split c in diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index bd49a31b9..e79ebdd92 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -185,6 +185,10 @@ let set_arithmetic () : unit result = expect_eq program "mem_op" (e_set [e_string "foo" ; e_string "bar"]) (e_bool false) in + let%bind () = + expect_eq program "iter_op" + (e_set [e_int 2 ; e_int 4 ; e_int 7]) + (e_int 13) in ok () let unit_expression () : unit result = @@ -365,6 +369,10 @@ let list () : unit result = let expected = ez [144 ; 51 ; 42 ; 120 ; 421] in expect_eq_evaluate program "bl" expected in + let%bind () = + expect_eq program "iter_op" + (e_list [e_int 2 ; e_int 4 ; e_int 7]) + (e_int 13) in ok () let condition () : unit result = diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index fcaf67815..14b42227a 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -32,12 +32,22 @@ them. please report this to the developers." in let content () = name in error title content + let row_loc l = ("location" , fun () -> Format.asprintf "%a" Location.pp l) + let unsupported_pattern_matching kind location = let title () = "unsupported pattern-matching" in let content () = Format.asprintf "%s patterns aren't supported yet" kind in let data = [ - ("location" , fun () -> Format.asprintf "%a" Location.pp location) ; - ] in + row_loc location ; + ] in + error ~data title content + + let unsupported_iterator location = + let title () = "unsupported iterator" in + let content () = "only lambda are supported as iterators" in + let data = [ + row_loc location ; + ] in error ~data title content let not_functional_main location = @@ -341,15 +351,50 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re let%bind record' = translate_annotated_expression record in let expr = List.fold_left aux record' path in ok expr - | E_constant (name, lst) -> ( - let%bind lst' = bind_map_list (translate_annotated_expression) lst in - match name, lst with - | "NONE", [] -> - let%bind o = - trace_strong (corner_case ~loc:__LOC__ "not an option") @@ - Mini_c.Combinators.get_t_option tv in - return @@ E_make_none o - | _ -> return @@ E_constant (name, lst') + | E_constant (name , lst) -> ( + let (iter , map) = + let iterator name = fun (lst : AST.annotated_expression list) -> match lst with + | [i ; f] -> ( + let%bind f' = match f.expression with + | E_lambda l -> ( + let%bind body' = translate_annotated_expression l.result in + let%bind input' = translate_type l.input_type in + ok ((l.binder , input') , body') + ) + | E_variable v -> ( + let%bind elt = + trace_option (corner_case ~loc:__LOC__ "missing var") @@ + AST.Environment.get_opt v f.environment in + match elt.definition with + | ED_declaration (f , _) -> ( + match f.expression with + | E_lambda l -> ( + let%bind body' = translate_annotated_expression l.result in + let%bind input' = translate_type l.input_type in + ok ((l.binder , input') , body') + ) + | _ -> fail @@ unsupported_iterator f.location + ) + | _ -> fail @@ unsupported_iterator f.location + ) + | _ -> fail @@ unsupported_iterator f.location + in + let%bind i' = translate_annotated_expression i in + return @@ E_iterator (name , f' , i') + ) + | _ -> fail @@ corner_case ~loc:__LOC__ "bad iterator arity" + in + iterator "ITER" , iterator "MAP" in + match (name , lst) with + | ("SET_ITER" , lst) -> iter lst + | ("LIST_ITER" , lst) -> iter lst + | ("MAP_ITER" , lst) -> iter lst + | ("LIST_MAP" , lst) -> map lst + | ("MAP_MAP" , lst) -> map lst + | _ -> ( + let%bind lst' = bind_map_list (translate_annotated_expression) lst in + return @@ E_constant (name , lst') + ) ) | E_lambda l -> let%bind env = diff --git a/vendors/ligo-utils/tezos-utils/x_michelson.ml b/vendors/ligo-utils/tezos-utils/x_michelson.ml index 462a40b63..254b93fab 100644 --- a/vendors/ligo-utils/tezos-utils/x_michelson.ml +++ b/vendors/ligo-utils/tezos-utils/x_michelson.ml @@ -48,6 +48,8 @@ let i_push_string str = i_push t_string (string str) let i_none ty = prim ~children:[ty] I_NONE let i_nil ty = prim ~children:[ty] I_NIL let i_empty_set ty = prim ~children:[ty] I_EMPTY_SET +let i_iter body = prim ~children:[body] I_ITER +let i_map body = prim ~children:[body] I_MAP let i_some = prim I_SOME let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA let i_empty_map src dst = prim ~children:[src;dst] I_EMPTY_MAP From 564a4df1456c826f1dcd3096f12aa08946001b88 Mon Sep 17 00:00:00 2001 From: galfour Date: Sat, 20 Jul 2019 16:18:50 +0200 Subject: [PATCH 8/9] add map to lists ; fix error with lists --- src/ast_simplified/combinators.ml | 2 +- src/compiler/compiler_program.ml | 8 ++++---- src/compiler/uncompiler.ml | 10 +++------- src/contracts/list.ligo | 4 ++++ src/main/run_mini_c.ml | 9 +++++++++ src/main/run_simplified.ml | 9 ++++++--- src/main/run_typed.ml | 10 ++++++++-- src/operators/operators.ml | 7 ++++++- src/test/integration_tests.ml | 16 +++++++++++----- src/test/test_helpers.ml | 2 +- src/transpiler/transpiler.ml | 2 +- 11 files changed, 54 insertions(+), 25 deletions(-) diff --git a/src/ast_simplified/combinators.ml b/src/ast_simplified/combinators.ml index edc8ef449..9fcb96afd 100644 --- a/src/ast_simplified/combinators.ml +++ b/src/ast_simplified/combinators.ml @@ -104,7 +104,7 @@ let e_typed_list ?loc lst t = e_annotation ?loc (e_list lst) (t_list t) let e_typed_map ?loc lst k v = e_annotation ?loc (e_map lst) (t_map k v) - + let e_typed_set ?loc lst k = e_annotation ?loc (e_set lst) (t_set k) let e_lambda ?loc (binder : string) diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml index 6da10d7c5..aa737a071 100644 --- a/src/compiler/compiler_program.ml +++ b/src/compiler/compiler_program.ml @@ -397,13 +397,13 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m ) | "MAP" -> ( let%bind restrict = - let%bind popped = Compiler_environment.pop body_env in - Compiler_environment.select_env popped env in + let%bind popped' = Compiler_environment.pop body_env in + Compiler_environment.select_env popped' popped in let%bind code = ok (seq [ expr' ; - i_map (seq [body' ; restrict]) ; + i_map (seq [body' ; dip restrict]) ; ]) in - return code + return ~prepend_env:popped code ) | s -> ( let error = error (thunk "bad iterator") (thunk s) in diff --git a/src/compiler/uncompiler.ml b/src/compiler/uncompiler.ml index d8855471e..8453c6c5a 100644 --- a/src/compiler/uncompiler.ml +++ b/src/compiler/uncompiler.ml @@ -68,15 +68,11 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result = in ok @@ D_map lst' | (List_t (ty, _)), lst -> - let lst' = - let aux acc cur = cur :: acc in - let lst = List.fold_left aux lst [] in - List.rev lst in - let%bind lst'' = + let%bind lst' = let aux = fun t -> translate_value (Ex_typed_value (ty, t)) in - bind_map_list aux lst' + bind_map_list aux lst in - ok @@ D_list lst'' + ok @@ D_list lst' | (Set_t (ty, _)), (module S) -> ( let lst = S.OPS.elements S.boxed in let lst' = diff --git a/src/contracts/list.ligo b/src/contracts/list.ligo index 503d72ffb..99920b92a 100644 --- a/src/contracts/list.ligo +++ b/src/contracts/list.ligo @@ -27,3 +27,7 @@ function iter_op (const s : list(int)) : int is begin list_iter(s , aggregate) ; end with r + +function map_op (const s : list(int)) : list(int) is + function increment (const i : int) : int is block { skip } with i + 1 + block { skip } with list_map(s , increment) diff --git a/src/main/run_mini_c.ml b/src/main/run_mini_c.ml index 24a38b489..5c8f12e5d 100644 --- a/src/main/run_mini_c.ml +++ b/src/main/run_mini_c.ml @@ -41,5 +41,14 @@ let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:v Format.printf "Compiled Input: %a\n" Michelson.pp input_michelson ; ) ; let%bind ex_ty_value = run_aux ?options compiled input_michelson in + if debug_michelson then ( + let (Ex_typed_value (ty , v)) = ex_ty_value in + ignore @@ + let%bind michelson_value = + trace_tzresult_lwt (simple_error "debugging run_mini_c") @@ + Proto_alpha_utils.Memory_proto_alpha.unparse_michelson_data ty v in + Format.printf "Compiled Output: %a\n" Michelson.pp michelson_value ; + ok () + ) ; let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in ok result diff --git a/src/main/run_simplified.ml b/src/main/run_simplified.ml index 17833d6b3..4faf34aaf 100644 --- a/src/main/run_simplified.ml +++ b/src/main/run_simplified.ml @@ -11,14 +11,17 @@ let run_simplityped match last_declaration with | Declaration_constant (_ , (_ , post_env)) -> post_env in - Typer.type_expression env input in + Typer.type_expression env input in let%bind typed_result = Run_typed.run_typed ?options ~debug_mini_c ~debug_michelson entry program typed_input in let%bind annotated_result = Typer.untype_expression typed_result in ok annotated_result -let evaluate_simplityped ?options (program : Ast_typed.program) (entry : string) +let evaluate_simplityped + ?options + ?(debug_mini_c = false) ?(debug_michelson = false) + (program : Ast_typed.program) (entry : string) : Ast_simplified.expression result = - let%bind typed_result = Run_typed.evaluate_typed ?options entry program in + let%bind typed_result = Run_typed.evaluate_typed ?options ~debug_mini_c ~debug_michelson entry program in let%bind annotated_result = Typer.untype_expression typed_result in ok annotated_result diff --git a/src/main/run_typed.ml b/src/main/run_typed.ml index 4f0ff0f77..788a10406 100644 --- a/src/main/run_typed.ml +++ b/src/main/run_typed.ml @@ -13,12 +13,18 @@ let transpile_value let%bind r = Run_mini_c.run_entry f input in ok r -let evaluate_typed ?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result = +let evaluate_typed + ?(debug_mini_c = false) ?(debug_michelson = false) + ?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result = trace (simple_error "easy evaluate typed") @@ let%bind result = let%bind mini_c_main = Transpiler.translate_entry program entry in - Run_mini_c.run_entry ?options mini_c_main (Mini_c.Combinators.d_unit) in + (if debug_mini_c then + Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main) + ) ; + Run_mini_c.run_entry ?options ~debug_michelson mini_c_main (Mini_c.Combinators.d_unit) + in let%bind typed_result = let%bind typed_main = Ast_typed.get_entry program entry in Transpiler.untranspile result typed_main.type_annotation in diff --git a/src/operators/operators.ml b/src/operators/operators.ml index befd3b961..6a30913f5 100644 --- a/src/operators/operators.ml +++ b/src/operators/operators.ml @@ -80,6 +80,9 @@ module Simplify = struct ("set_remove" , "SET_REMOVE") ; ("set_iter" , "SET_ITER") ; ("list_iter" , "LIST_ITER") ; + ("list_map" , "LIST_MAP") ; + ("map_iter" , "MAP_ITER") ; + ("map_map" , "MAP_MAP") ; ] let type_constants = type_constants @@ -501,7 +504,7 @@ module Typer = struct let%bind (arg , res) = get_t_function body in let%bind key = get_t_list lst in if eq_1 key arg - then ok res + then ok (t_list res ()) else simple_fail "bad list iter" let not_ = typer_1 "NOT" @@ fun elt -> @@ -582,12 +585,14 @@ module Typer = struct map_map ; map_fold ; map_iter ; + map_map ; set_empty ; set_mem ; set_add ; set_remove ; set_iter ; list_iter ; + list_map ; int ; size ; failwith_ ; diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index e79ebdd92..d3f54421e 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -356,15 +356,15 @@ let list () : unit result = let lst' = List.map e_int lst in e_typed_list lst' t_int in + let%bind () = + let expected = ez [23 ; 42] in + expect_eq_evaluate program "fb" expected + in let%bind () = let make_input = fun n -> (ez @@ List.range n) in let make_expected = e_nat in expect_eq_n_strict_pos_small program "size_" make_input make_expected in - let%bind () = - let expected = ez [23 ; 42] in - expect_eq_evaluate program "fb" expected - in let%bind () = let expected = ez [144 ; 51 ; 42 ; 120 ; 421] in expect_eq_evaluate program "bl" expected @@ -372,7 +372,13 @@ let list () : unit result = let%bind () = expect_eq program "iter_op" (e_list [e_int 2 ; e_int 4 ; e_int 7]) - (e_int 13) in + (e_int 13) + in + let%bind () = + expect_eq program "map_op" + (e_list [e_int 2 ; e_int 4 ; e_int 7]) + (e_list [e_int 3 ; e_int 5 ; e_int 8]) + in ok () let condition () : unit result = diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml index 32f45d4a4..60da8f999 100644 --- a/src/test/test_helpers.ml +++ b/src/test/test_helpers.ml @@ -97,7 +97,7 @@ let expect_evaluate program entry_point expecter = let content () = Format.asprintf "Entry_point: %s" entry_point in error title content in trace error @@ - let%bind result = Ligo.Run.evaluate_simplityped program entry_point in + let%bind result = Ligo.Run.evaluate_simplityped ~debug_mini_c:true ~debug_michelson:true program entry_point in expecter result let expect_eq_evaluate program entry_point expected = diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml index 14b42227a..3aed3edb5 100644 --- a/src/transpiler/transpiler.ml +++ b/src/transpiler/transpiler.ml @@ -409,7 +409,7 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re let aux : expression -> expression -> expression result = fun prev cur -> return @@ E_constant ("CONS", [cur ; prev]) in let%bind (init : expression) = return @@ E_make_empty_list t in - bind_fold_list aux init lst' + bind_fold_right_list aux init lst' ) | E_set lst -> ( let%bind t = From d7a16c47c1361377257121e2ac872dadcd4400ef Mon Sep 17 00:00:00 2001 From: galfour Date: Sat, 20 Jul 2019 16:42:34 +0200 Subject: [PATCH 9/9] add iterators for maps --- src/contracts/map.ligo | 11 +++++++++++ src/operators/operators.ml | 20 ++++++++------------ src/test/integration_tests.ml | 10 ++++++++++ 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/contracts/map.ligo b/src/contracts/map.ligo index bcc2a8005..f0576bf54 100644 --- a/src/contracts/map.ligo +++ b/src/contracts/map.ligo @@ -31,3 +31,14 @@ const bm : foobar = map 120 -> 23 ; 421 -> 23 ; end + +function iter_op (const m : foobar) : int is + var r : int := 0 ; + function aggregate (const i : int ; const j : int) : unit is block { r := r + i + j } with unit ; + block { + map_iter(m , aggregate) ; + } with r ; + +function map_op (const m : foobar) : foobar is + function increment (const i : int ; const j : int) : int is block { skip } with j + 1 ; + block { skip } with map_map(m , increment) ; diff --git a/src/operators/operators.ml b/src/operators/operators.ml index 6a30913f5..67c0cdb28 100644 --- a/src/operators/operators.ml +++ b/src/operators/operators.ml @@ -256,22 +256,18 @@ module Typer = struct let%bind () = assert_type_value_eq (src, k) in ok @@ t_option dst () - let map_iter : typer = typer_2 "MAP_ITER" @@ fun f m -> + let map_iter : typer = typer_2 "MAP_ITER" @@ fun m f -> let%bind (k, v) = get_t_map m in - let%bind (arg_1 , res) = get_t_function f in - let%bind (arg_2 , res') = get_t_function res in - let%bind () = assert_eq_1 arg_1 k in - let%bind () = assert_eq_1 arg_2 v in - let%bind () = assert_eq_1 res' (t_unit ()) in + let%bind (arg , res) = get_t_function f in + let%bind () = assert_eq_1 arg (t_pair k v ()) in + let%bind () = assert_eq_1 res (t_unit ()) in ok @@ t_unit () - let map_map : typer = typer_2 "MAP_MAP" @@ fun f m -> + let map_map : typer = typer_2 "MAP_MAP" @@ fun m f -> let%bind (k, v) = get_t_map m in - let%bind (arg_1 , res) = get_t_function f in - let%bind (arg_2 , res') = get_t_function res in - let%bind () = assert_eq_1 arg_1 k in - let%bind () = assert_eq_1 arg_2 v in - ok @@ res' + let%bind (arg , res) = get_t_function f in + let%bind () = assert_eq_1 arg (t_pair k v ()) in + ok @@ t_map k res () let map_fold : typer = typer_2 "MAP_FOLD" @@ fun f m -> let%bind (k, v) = get_t_map m in diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index d3f54421e..0a978b6e5 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -348,6 +348,16 @@ let map () : unit result = let expected = ez [23, 23] in expect_eq program "rm" input expected in + let%bind () = + let input = ez [(1 , 10) ; (2 , 20) ; (3 , 30) ] in + let expected = e_int 66 in + expect_eq program "iter_op" input expected + in + let%bind () = + let input = ez [(1 , 10) ; (2 , 20) ; (3 , 30) ] in + let expected = ez [(1 , 11) ; (2 , 21) ; (3 , 31) ] in + expect_eq program "map_op" input expected + in ok () let list () : unit result =