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/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_environment.ml b/src/compiler/compiler_environment.ml
index 05c749095..d5734c4e9 100644
--- a/src/compiler/compiler_environment.ml
+++ b/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
-      | false -> selector , false in
-    let e_lst' = List.fold_map_right aux lst e_lst in
+      | true -> List.remove_element s selector , keep
+      | false -> selector , not keep 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 e' = Environment.select [ first_name ] e in
+  let%bind code = select ~rev:true e [ first_name ] 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..aa737a071 100644
--- a/src/compiler/compiler_program.ml
+++ b/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
-      | (Some _ , Some _) -> simple_fail ("two args to return at " ^ __LOC__)
-      | None , None -> ok @@ Environment.add ("_tmp_expression" , ty) env
-      | Some prepend_env , None ->
+      match (prepend_env , end_env , push_var_name) with
+      | (Some _ , Some _ , _) ->
+         simple_fail ("two args to return at " ^ __LOC__)
+      | 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) ->
-      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 ;
       ]
+  )
   | 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 (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" ;
@@ -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 (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 =
@@ -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 (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 [
@@ -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
-      (* 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
@@ -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
+  | 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 ;
       ]
     )
 
 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 (
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/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/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/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/list.ligo b/src/contracts/list.ligo
index 60af05003..99920b92a 100644
--- a/src/contracts/list.ligo
+++ b/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)
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/contracts/set_arithmetic.ligo b/src/contracts/set_arithmetic.ligo
new file mode 100644
index 000000000..814120c0c
--- /dev/null
+++ b/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)
+
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/main/run_mini_c.ml b/src/main/run_mini_c.ml
index 17fc40ba2..5c8f12e5d 100644
--- a/src/main/run_mini_c.ml
+++ b/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
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/mini_c/PP.ml b/src/mini_c/PP.ml
index af5543689..3d0e3f065 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,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_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_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/environment.ml b/src/mini_c/environment.ml
index 8c1bc796c..1d7463c48 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) ?(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
-      let e_lst' = List.fold_map_right aux lst e_lst in
+        | true -> List.remove_element s selector , keep
+        | false -> selector , not keep 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
diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml
index 57f117165..3e9a69819 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
@@ -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/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..67c0cdb28 100644
--- a/src/operators/operators.ml
+++ b/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
@@ -91,7 +105,7 @@ module Simplify = struct
   module Ligodity = struct
     let constants = [
       ("assert" , "ASSERT") ;
-      
+
       ("Current.balance", "BALANCE") ;
       ("balance", "BALANCE") ;
       ("Current.time", "NOW") ;
@@ -132,7 +146,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") ;
@@ -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,46 +256,73 @@ 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 m f ->
     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 , 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 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 () =
-      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 +367,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 +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,15 +409,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 +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" ;
-      boolean_operator_2 "AND" ;
+      or_ ;
+      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 ;
@@ -525,19 +673,21 @@ 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]) ;
-    ("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 *)
-  
+
 end
diff --git a/src/simplify/pascaligo.ml b/src/simplify/pascaligo.ml
index 2f3299cc3..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)
@@ -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' =
@@ -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 ->
-      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
@@ -746,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 55445db99..0a978b6e5 100644
--- a/src/test/integration_tests.ml
+++ b/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 =
@@ -343,8 +420,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
@@ -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 ;
diff --git a/src/test/test_helpers.ml b/src/test/test_helpers.ml
index f178adcd2..60da8f999 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 "@[<v2>%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 "@[<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 =
@@ -49,7 +55,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 +68,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 =
@@ -80,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 8dbaf60a8..3aed3edb5 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 =
@@ -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'
     )
@@ -539,7 +584,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
@@ -674,7 +719,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. *)
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