Merge branch 'dev' into feature/better-error-messages

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 :)

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 ->

src/compiler/compiler_environment.ml

@@ -87,16 +87,20 @@ 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) ?(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
+      | true -> List.remove_element s selector , keep
-      | false -> selector , false in
+      | false -> selector , not keep in
-    let e_lst' = List.fold_map_right aux lst e_lst in
+    let e_lst' =
+      if rev = keep
+      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 =
@@ -144,8 +148,8 @@ 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 [ first_name ] e in
+  let e' = Environment.select ~rev:true [ first_name ] e in
   ok (code , e')
 
 let pack : environment -> michelson result = fun e ->

src/compiler/compiler_program.ml

@@ -19,7 +19,17 @@ 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
+          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
@@ -81,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"
 
@@ -96,30 +108,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
+      match (prepend_env , end_env , push_var_name) with
-      | (Some _ , Some _) -> simple_fail ("two args to return at " ^ __LOC__)
+      | (Some _ , Some _ , _) ->
-      | None , None -> ok @@ Environment.add ("_tmp_expression" , ty) env
+         simple_fail ("two args to return at " ^ __LOC__)
-      | Some prepend_env , None ->
+      | None , None , None ->
+         ok @@ Environment.add ("_tmp_expression" , ty) env
+      | 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
@@ -138,28 +170,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) ->
+  | E_environment_load (expr , load_env) -> (
-      let%bind (expr' , _) = translate_expression expr env in
+      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 ;
       ]
+  )
   | 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
       return ~end_env:cleared_env @@ seq [
         expr' ;
@@ -174,8 +205,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 (f , env') = translate_expression ~push_var_name:"application_f" f env in
-          let%bind (arg , _) = translate_expression arg 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" ;
@@ -187,8 +218,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 (arg' , env') = translate_expression ~push_var_name:"closure_arg" arg env in
-          let%bind (f' , env'') = translate_expression f 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 =
@@ -221,20 +252,19 @@ 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
-    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' =
         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
@@ -282,22 +312,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 (a' , env_a') = translate_expression ~push_var_name:"if_true" a popped in
-      let%bind (b' , _) = translate_expression b 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 [
@@ -311,11 +341,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' , _) = 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' , _) = 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 [
@@ -334,11 +364,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
@@ -350,9 +380,38 @@ and translate_expression ?(first=false) (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' popped in
+          let%bind code = ok (seq [
+              expr' ;
+              i_map (seq [body' ; dip restrict]) ;
+            ]) in
+          return ~prepend_env:popped code
+        )
+      | s -> (
+          let error = error (thunk "bad iterator") (thunk s) in
+          fail error
+        )
+    )
   | E_assignment (name , lrs , expr) -> (
-      let%bind (expr' , env') = translate_expression expr env in
+      let%bind (expr' , env') = translate_expression ~push_var_name:"assignment_expr" 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
@@ -374,7 +433,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" ;
@@ -386,27 +445,25 @@ 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
+      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 ;
       ]
     )
 
 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 +476,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 (

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

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%bind lst' =
-        let aux acc cur = cur :: acc in
-        let lst = List.fold_left aux lst [] in
-        List.rev lst in
-      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' =

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

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)

src/contracts/list.ligo

@@ -17,3 +17,17 @@ 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
+
+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)

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) ;

src/contracts/set_arithmetic.ligo

@@ -0,0 +1,26 @@
+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 [
+      "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)
+

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)

src/main/run_mini_c.ml

@@ -32,8 +32,23 @@ 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
+  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

src/main/run_simplified.ml

@@ -17,8 +17,11 @@ let run_simplityped
   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

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

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,10 +83,11 @@ 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 (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_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) ->

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) ?(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
+        | true -> List.remove_element s selector , keep
-        | false -> selector , false in
+        | false -> selector , not keep in
-      let e_lst' = List.fold_map_right aux lst e_lst in
+      let e_lst' =
+        if rev = keep
+        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

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
@@ -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)

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

src/operators/operators.ml

@@ -69,6 +69,20 @@ module Simplify = struct
       ("source" , "SOURCE") ;
       ("sender" , "SENDER") ;
       ("failwith" , "FAILWITH") ;
+      ("bitwise_or" , "OR") ;
+      ("bitwise_and" , "AND") ;
+      ("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") ;
+      ("list_iter" , "LIST_ITER") ;
+      ("list_map" , "LIST_MAP") ;
+      ("map_iter" , "MAP_ITER") ;
+      ("map_map" , "MAP_MAP") ;
     ]
 
     let type_constants = type_constants
@@ -189,6 +203,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
@@ -196,6 +215,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 +241,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,45 +256,72 @@ 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 map_iter : typer = typer_2 "MAP_ITER" @@ fun m f ->
-    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%bind (k, v) = get_t_map m in
-    let%bind (input_type, result_type) = get_t_function f in
+    let%bind (arg , res) = get_t_function f in
-    let%bind () = assert_type_value_eq (input_type, t_tuple [k ; v] ()) in
+    let%bind () = assert_eq_1 arg (t_pair k v ()) in
-    ok @@ t_map k result_type ()
+    let%bind () = assert_eq_1 res (t_unit ()) in
-
-  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
     ok @@ t_unit ()
 
+  let map_map : typer = typer_2 "MAP_MAP" @@ fun m f ->
+    let%bind (k, v) = get_t_map m in
+    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
+    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 () =
+    let%bind () = assert_eq_1 i (t_nat ()) in
-      Assert.assert_true @@
+    let%bind () = assert_eq_1 j (t_nat ()) in
-      (is_t_nat i && is_t_nat j && is_t_string s) in
+    if eq_1 s (t_string ())
-    ok @@ 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 () =
@@ -328,6 +376,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 +388,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,10 +409,18 @@ 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 ()
@@ -387,6 +458,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 +480,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 (t_list 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 ;
@@ -420,28 +561,34 @@ module Typer = struct
       sub ;
       none ;
       some ;
+      concat ;
+      slice ;
       comparator "EQ" ;
       comparator "NEQ" ;
       comparator "LT" ;
       comparator "GT" ;
       comparator "LE" ;
       comparator "GE" ;
-      boolean_operator_2 "OR" ;
+      or_ ;
-      boolean_operator_2 "AND" ;
+      and_ ;
+      xor ;
       not_ ;
       map_remove ;
       map_add ;
       map_update ;
       map_mem ;
       map_find ;
-      map_map_fold ;
       map_map ;
       map_fold ;
       map_iter ;
+      map_map ;
+      set_empty ;
       set_mem ;
       set_add ;
       set_remove ;
-      (* map_size ; (* use size *) *)
+      set_iter ;
+      list_iter ;
+      list_map ;
       int ;
       size ;
       failwith_ ;
@@ -459,6 +606,7 @@ module Typer = struct
       amount ;
       transaction ;
       get_contract ;
+      neg ;
       abs ;
       now ;
       slice ;
@@ -529,13 +677,15 @@ 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) ;
+    ("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) ;
     ("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 *)

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)
@@ -472,8 +472,7 @@ let rec simpl_expression (t:Raw.expr) : expr result =
     let n = Z.to_int @@ snd @@ n in
     return @@ e_literal ~loc (Literal_tez n)
   )
-  | EArith _ as e ->
+  | EArith (Neg e) -> simpl_unop "NEG" e
-       fail @@ unsupported_arith_op e
   | EString (String s) ->
     let (s , loc) = r_split s in
       let s' =
@@ -485,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
@@ -572,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
@@ -730,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 ->
+  | ProcCall x -> (
-      fail @@ unsupported_proc_calls call
+      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
@@ -746,6 +771,12 @@ 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 (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 -> (

src/test/integration_tests.ml

@@ -127,13 +127,70 @@ 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)) ; *)
+      ("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 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
+  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 =
   let%bind program = type_file "./contracts/unit.ligo" in
   expect_eq_evaluate program "u" (e_unit ())
@@ -291,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 =
@@ -299,19 +366,29 @@ 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
   in
+  let%bind () =
+    expect_eq program "iter_op"
+      (e_list [e_int 2 ; e_int 4 ; e_int 7])
+      (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 =
@@ -345,7 +422,6 @@ let loop () : unit result =
   in
   ok ()
 
-
 let matching () : unit result =
   let%bind program = type_file "./contracts/match.ligo" in
   let%bind () =
@@ -563,6 +639,9 @@ 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 "set_arithmetic" set_arithmetic ;
     test "unit" unit_expression ;
     test "string" string_expression ;
     test "option" option ;

src/test/test_helpers.ml

@@ -21,6 +21,41 @@ let wrap_test_raw f =
   | Error err ->
     Format.printf "%a\n%!" Ligo.Display.error_pp (err ())
 
+(* let rec error_pp out (e : error) =
+ *     let open JSON_string_utils in
+ *   let message =
+ *     let opt = e |> member "message" |> string in
+ *     let msg = Option.unopt ~default:"" opt in
+ *     if msg = ""
+ *     then ""
+ *     else ": " ^ msg in
+ *   let error_code =
+ *     let error_code = e |> member "error_code" in
+ *     match error_code with
+ *     | `Null -> ""
+ *     | _ -> " (" ^ (J.to_string error_code) ^ ")" in
+ *   let title =
+ *     let opt = e |> member "title" |> string in
+ *     Option.unopt ~default:"" opt in
+ *   let data =
+ *     let data = e |> member "data" in
+ *     match data with
+ *     | `Null -> ""
+ *     | _ -> " " ^ (J.to_string data) ^ "\n" in
+ *   let infos =
+ *     let infos = e |> member "infos" in
+ *     match infos with
+ *     | `Null -> ""
+ *     | `List lst -> Format.asprintf "@[<v2>%a@]" PP_helpers.(list_sep error_pp (tag "@,")) lst
+ *     | _ -> " " ^ (J.to_string infos) ^ "\n" in
+ *   let children =
+ *     let children = e |> member "children" in
+ *     match children with
+ *     | `Null -> ""
+ *     | `List lst -> Format.asprintf "@[<v2>%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 =
   Test (
     Alcotest.test_case name `Quick @@ fun () ->
@@ -41,6 +76,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 =
@@ -59,7 +105,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 =

src/transpiler/transpiler.ml

@@ -32,11 +32,21 @@ 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) ;
+        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
 
@@ -342,14 +352,49 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
       let expr = List.fold_left aux record' path in
       ok expr
   | 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
-      match name, lst with
+          return @@ E_constant (name , lst')
-      | "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_lambda l ->
     let%bind env =
@@ -364,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 =
@@ -372,7 +417,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'
     )

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 ->
+  | Error errs ->
-      (* let tz_errs = List.map of_tz_error errs in *)
+      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. *)

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