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