From de96a0468170220ced2ddf58453a807102284029 Mon Sep 17 00:00:00 2001
From: galfour <gabriel.alfour@gmail.com>
Date: Tue, 20 Aug 2019 22:51:16 +0200
Subject: [PATCH] simplifying compiler

---
 src/compiler/compiler_environment.ml | 153 +-------------
 src/compiler/compiler_program.ml     | 295 +++++++++------------------
 src/main/run_mini_c.ml               |   8 +-
 src/main/run_source.ml               |  20 +-
 src/main/run_typed.ml                |  12 +-
 src/mini_c/PP.ml                     |  10 +-
 src/mini_c/combinators.ml            |  16 +-
 src/mini_c/types.ml                  |   9 +-
 src/test/compiler_tests.ml           |   2 +-
 src/transpiler/transpiler.ml         |  32 +--
 10 files changed, 146 insertions(+), 411 deletions(-)

diff --git a/src/compiler/compiler_environment.ml b/src/compiler/compiler_environment.ml
index d5734c4e9..386412f3f 100644
--- a/src/compiler/compiler_environment.ml
+++ b/src/compiler/compiler_environment.ml
@@ -1,14 +1,12 @@
-open Proto_alpha_utils
 open Trace
 open Mini_c
 open Environment
 open Michelson
-open Memory_proto_alpha.Script_ir_translator
 
 module Stack = Meta_michelson.Stack
 
 let get : environment -> string -> michelson result = fun e s ->
-  let%bind (type_value , position) =
+  let%bind (_ , position) =
     let error =
       let title () = "Environment.get" in
       let content () = Format.asprintf "%s in %a"
@@ -26,22 +24,10 @@ let get : environment -> string -> michelson result = fun e s ->
   in
   let code = aux position in
 
-  let%bind () =
-    let error () = ok @@ simple_error "error producing Env.get" in
-    let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
-    let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
-    let output_stack_ty = Stack.(ty @: input_stack_ty) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
 let set : environment -> string -> michelson result = fun e s ->
-  let%bind (type_value , position) =
+  let%bind (_ , position) =
     generic_try (simple_error "Environment.get") @@
     (fun () -> Environment.get_i s e) in
   let rec aux = fun n ->
@@ -54,37 +40,11 @@ let set : environment -> string -> michelson result = fun e s ->
   in
   let code = aux position in
 
-  let%bind () =
-    let error () = ok @@ simple_error "error producing Env.set" in
-    let%bind (Stack.Ex_stack_ty env_stack_ty) = Compiler_type.Ty.environment e in
-    let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
-    let input_stack_ty = Stack.(ty @: env_stack_ty) in
-    let output_stack_ty = env_stack_ty in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
-let add : environment -> (string * type_value) -> michelson result = fun e (_s , type_value) ->
+let add : environment -> (string * type_value) -> michelson result = fun _ (_s , _) ->
   let code = seq [] in
 
-  let%bind () =
-    let error () = ok @@ simple_error "error producing Env.get" in
-    let%bind (Stack.Ex_stack_ty env_stack_ty) = Compiler_type.Ty.environment e in
-    let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
-    let input_stack_ty = Stack.(ty @: env_stack_ty) in
-    let output_stack_ty = Stack.(ty @: env_stack_ty) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
 let select ?(rev = false) ?(keep = true) : environment -> string list -> michelson result = fun e lst ->
@@ -111,32 +71,6 @@ let select ?(rev = false) ?(keep = true) : environment -> string list -> michels
     in
     List.fold_right' aux (seq []) e_lst in
 
-  let%bind () =
-    let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
-    let e' =
-      Environment.of_list
-      @@ List.map fst
-      @@ List.filter snd
-      @@ e_lst
-    in
-    let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment e' in
-    let error () =
-      let title () = "error producing Env.select" in
-      let content () = Format.asprintf "\nInput : %a\nOutput : %a\nList : {%a}\nCode : %a\nLog : %s\n"
-          PP.environment e
-          PP.environment e'
-          PP_helpers.(list_sep (pair PP.environment_element bool) (const " || ")) e_lst
-          Michelson.pp code
-          (L.get ())
-      in
-      ok @@ (error title content) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
 let select_env : environment -> environment -> michelson result = fun source filter ->
@@ -158,23 +92,6 @@ let pack : environment -> michelson result = fun e ->
     Assert.assert_true (List.length e <> 0) in
   let code = seq @@ List.map (Function.constant i_pair) @@ List.tl e in
 
-  let%bind () =
-    let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
-    let repr = Environment.closure_representation e in
-    let%bind (Ex_ty output_ty) = Compiler_type.Ty.type_ repr in
-    let output_stack_ty = Stack.(output_ty @: nil) in
-    let error () =
-      let title () = "error producing Env.pack" in
-      let content () = Format.asprintf ""
-      in
-      ok @@ (error title content) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
 let unpack : environment -> michelson result = fun e ->
@@ -192,26 +109,6 @@ let unpack : environment -> michelson result = fun e ->
       ] in
   let code = aux l in
 
-  let%bind () =
-    let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment e in
-    let repr = Environment.closure_representation e in
-    let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ repr in
-    let input_stack_ty = Stack.(input_ty @: nil) in
-    let error () =
-      let title () = "error producing Env.unpack" in
-      let content () = Format.asprintf "\nEnvironment:%a\nType Representation:%a\nCode:%a\n"
-          PP.environment e
-          PP.type_ repr
-          Michelson.pp code
-      in
-      ok @@ (error title content) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
 
@@ -239,53 +136,11 @@ let pack_select : environment -> string list -> michelson result = fun e lst ->
     in
     List.fold_right' aux (true , seq []) e_lst in
 
-  let%bind () =
-    let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
-    let e' =
-      Environment.of_list
-      @@ List.map fst
-      @@ List.filter snd
-      @@ e_lst
-    in
-    let%bind (Ex_ty output_ty) = Compiler_type.Ty.environment_representation e' in
-    let output_stack_ty = Stack.(output_ty @: input_stack_ty) in
-    let error () =
-      let title () = "error producing Env.pack_select" in
-      let content () = Format.asprintf "\nInput : %a\nOutput : %a\nList : {%a}\nCode : %a\nLog : %s\n"
-          PP.environment e
-          PP.environment e'
-          PP_helpers.(list_sep (pair PP.environment_element bool) (const " || ")) e_lst
-          Michelson.pp code
-          (L.get ())
-      in
-      ok @@ (error title content) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
-let add_packed_anon : environment -> type_value -> michelson result = fun e type_value ->
+let add_packed_anon : environment -> type_value -> michelson result = fun _ _ ->
   let code = seq [i_pair] in
 
-  let%bind () =
-    let error () = ok @@ simple_error "error producing add packed" in
-    let%bind (Ex_ty input_ty) = Compiler_type.Ty.environment_representation e in
-    let e' = Environment.add ("_add_packed_anon" , type_value) e in
-    let%bind (Ex_ty output_ty) = Compiler_type.Ty.environment_representation e' in
-    let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
-    let input_stack_ty = Stack.(ty @: input_ty @: nil) in
-    let output_stack_ty = Stack.(output_ty @: nil) in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r error @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty in
-    ok ()
-  in
-
   ok code
 
 let pop : environment -> environment result = fun e ->
diff --git a/src/compiler/compiler_program.ml b/src/compiler/compiler_program.ml
index aa737a071..a1d03a1c2 100644
--- a/src/compiler/compiler_program.ml
+++ b/src/compiler/compiler_program.ml
@@ -9,8 +9,6 @@ open Memory_proto_alpha.Script_ir_translator
 
 open Operators.Compiler
 
-open Proto_alpha_utils
-
 let get_predicate : string -> type_value -> expression list -> predicate result = fun s ty lst ->
   match Map.String.find_opt s Operators.Compiler.predicates with
   | Some x -> ok x
@@ -68,7 +66,7 @@ let get_predicate : string -> type_value -> expression list -> predicate result
       | x -> simple_fail ("predicate \"" ^ x ^ "\" doesn't exist")
     )
 
-let rec translate_value (v:value) : michelson result = match v with
+let rec translate_value (v:value) ty : michelson result = match v with
   | D_bool b -> ok @@ prim (if b then D_True else D_False)
   | D_int n -> ok @@ int (Z.of_int n)
   | D_nat n -> ok @@ int (Z.of_int n)
@@ -78,135 +76,78 @@ let rec translate_value (v:value) : michelson result = match v with
   | D_bytes s -> ok @@ bytes (Tezos_stdlib.MBytes.of_bytes s)
   | D_unit -> ok @@ prim D_Unit
   | D_pair (a, b) -> (
-      let%bind a = translate_value a in
-      let%bind b = translate_value b in
+      let%bind (a_ty , b_ty) = get_t_pair ty in
+      let%bind a = translate_value a a_ty in
+      let%bind b = translate_value b b_ty in
       ok @@ prim ~children:[a;b] D_Pair
     )
-  | D_left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left
-  | D_right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right
-  | D_function anon -> translate_function anon
+  | D_left a -> (
+      let%bind (a_ty , _) = get_t_or ty in
+      let%bind a' = translate_value a a_ty in
+      ok @@ prim ~children:[a'] D_Left
+    )
+  | D_right b -> (
+      let%bind (_ , b_ty) = get_t_or ty in
+      let%bind b' = translate_value b b_ty in
+      ok @@ prim ~children:[b'] D_Right
+    )
+  | D_function { binder ; result } -> (
+      match ty with
+      | T_function (in_ty , _) -> (
+          let env = Mini_c.Environment.of_list [ (binder , in_ty) ] in
+          let%bind body = translate_expression result env in
+          ok body
+        )
+      | T_deep_closure _ -> simple_fail "no support for closures yet"
+      | _ -> simple_fail "expected function type"
+    )
   | D_none -> ok @@ prim D_None
   | D_some s ->
-      let%bind s' = translate_value s in
+      let%bind s' = translate_value s ty in
       ok @@ prim ~children:[s'] D_Some
-  | D_map lst ->
-      let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in
+  | D_map lst -> (
+      let%bind (k_ty , v_ty) = get_t_map ty in
+      let%bind lst' =
+        let aux (k , v) = bind_pair (translate_value k k_ty , translate_value v v_ty) in
+        bind_map_list aux lst in
       let sorted = List.sort (fun (x , _) (y , _) -> compare x y) lst' in
       let aux (a, b) = prim ~children:[a;b] D_Elt in
       ok @@ seq @@ List.map aux sorted
-  | D_list lst ->
-      let%bind lst' = bind_map_list translate_value lst in
+    )
+  | D_list lst -> (
+      let%bind e_ty = get_t_list ty in
+      let%bind lst' = bind_map_list (fun x -> translate_value x e_ty) lst in
       ok @@ seq lst'
-  | D_set lst ->
-      let%bind lst' = bind_map_list translate_value lst in
+    )
+  | D_set lst -> (
+      let%bind e_ty = get_t_set ty in
+      let%bind lst' = bind_map_list (fun x -> translate_value x e_ty) lst in
       let sorted = List.sort compare lst' in
       ok @@ seq sorted
+    )
   | D_operation _ ->
       simple_fail "can't compile an operation"
 
-and translate_function (content:anon_function) : michelson result =
-  let%bind body = translate_quote_body content in
-  ok @@ seq [ body ]
-
-and translate_expression ?push_var_name (expr:expression) (env:environment) : (michelson * environment) result =
+and translate_expression (expr:expression) (env:environment) : michelson result =
   let (expr' , ty) = Combinators.Expression.(get_content expr , get_type expr) in
   let error_message () =
     Format.asprintf  "\n- expr: %a\n- type: %a\n" PP.expression expr PP.type_ ty
   in
-  (* let i_skip = i_push_unit in *)
-
-  let return ?prepend_env ?end_env ?(unit_opt = false) code =
-    let code =
-      if unit_opt && push_var_name <> None
-      then seq [code ; i_push_unit]
-      else code
-    in
-    let%bind env' =
-      match (prepend_env , end_env , push_var_name) with
-      | (Some _ , Some _ , _) ->
-         simple_fail ("two args to return at " ^ __LOC__)
-      | None , None , None ->
-         ok @@ Environment.add ("_tmp_expression" , ty) env
-      | None , None , Some push_var_name ->
-         ok @@ Environment.add (push_var_name , ty) env
-      | Some prepend_env , None , None ->
-        ok @@ Environment.add ("_tmp_expression" , ty) prepend_env
-      | Some prepend_env , None , Some push_var_name ->
-        ok @@ Environment.add (push_var_name , ty) prepend_env
-      | None , Some end_env , None ->
-         ok end_env
-      | None , Some end_env , Some push_var_name -> (
-         if unit_opt
-         then ok @@ Environment.add (push_var_name , ty) end_env
-         else ok end_env
-      )
-    in
-    let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment env in
-    let%bind output_type = Compiler_type.type_ ty in
-    let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment env' in
-    let error_message () =
-      let%bind schema_michelsons = Compiler_type.environment env in
-      ok @@ Format.asprintf
-        "expression : %a\ncode : %a\npreenv : %a\npostenv : %a\nschema type : %a\noutput type : %a"
-        PP.expression expr
-        Michelson.pp code
-        PP.environment env
-        PP.environment env'
-        PP_helpers.(list_sep Michelson.pp (const ".")) schema_michelsons
-        Michelson.pp output_type
-    in
-    let%bind _ =
-      Trace.trace_tzresult_lwt_r
-        (fun () ->
-           let%bind error_message = error_message () in
-           ok @@ (fun () -> error (thunk "error parsing expression code")
-                                  (fun () -> error_message)
-                                  ())) @@
-      Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty
-    in
-    ok (code , env')
-  in
+  let return code = ok code in
 
   trace (error (thunk "compiling expression") error_message) @@
   match expr' with
-  | E_skip -> return ~end_env:env ~unit_opt:true @@ seq []
-  | E_environment_capture c ->
-      let%bind code = Compiler_environment.pack_select env c in
-      return @@ code
-  | E_environment_load (expr , load_env) -> (
-      let%bind (expr' , _) = translate_expression ~push_var_name:"env_to_load" expr env in
-      let%bind clear = Compiler_environment.select env [] in
-      let%bind unpack = Compiler_environment.unpack load_env in
-      return ~end_env:load_env @@ seq [
-        expr' ;
-        dip clear ;
-        unpack ;
-      ]
-  )
-  | E_environment_select sub_env ->
-      let%bind code = Compiler_environment.select_env env sub_env in
-      return ~end_env:sub_env @@ seq [
-        code ;
-      ]
-  | E_environment_return expr -> (
-      let%bind (expr' , env) = translate_expression ~push_var_name:"return_clause" expr env in
-      let%bind (code , cleared_env) = Compiler_environment.clear env in
-      return ~end_env:cleared_env @@ seq [
-        expr' ;
-        code ;
-      ]
-    )
+  | E_skip -> return @@ i_push_unit
   | E_literal v ->
-      let%bind v = translate_value v in
+      let%bind v = translate_value v ty in
       let%bind t = Compiler_type.type_ ty in
       return @@ i_push t v
   | E_application(f, arg) -> (
       match Combinators.Expression.get_type f with
       | T_function _ -> (
           trace (simple_error "Compiling quote application") @@
-          let%bind (f , env') = translate_expression ~push_var_name:"application_f" f env in
-          let%bind (arg , _) = translate_expression ~push_var_name:"application_arg" arg env' in
+          let%bind f = translate_expression f env in
+          let%bind arg = translate_expression arg env in
           return @@ seq [
             i_comment "quote application" ;
             i_comment "get f" ;
@@ -218,23 +159,9 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
         )
       | T_deep_closure (small_env, input_ty , _) -> (
           trace (simple_error "Compiling deep closure application") @@
-          let%bind (arg' , env') = translate_expression ~push_var_name:"closure_arg" arg env in
-          let%bind (f' , env'') = translate_expression ~push_var_name:"closure_f" f env' in
-          let%bind f_ty = Compiler_type.type_ f.type_value in
+          let%bind arg' = translate_expression arg env in
+          let%bind f' = translate_expression f env in
           let%bind append_closure = Compiler_environment.add_packed_anon small_env input_ty in
-          let error =
-            let error_title () = "michelson type-checking closure application" in
-            let error_content () =
-              Format.asprintf "\nEnv. %a\nEnv'. %a\nEnv''. %a\nclosure. %a ; %a ; %a\narg. %a\n"
-                PP.environment env
-                PP.environment env'
-                PP.environment env''
-                PP.expression_with_type f Michelson.pp f_ty Michelson.pp f'
-                PP.expression_with_type arg
-            in
-            error error_title error_content
-          in
-          trace error @@
           return @@ seq [
             i_comment "closure application" ;
             i_comment "arg" ;
@@ -253,9 +180,9 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
     let%bind code = Compiler_environment.get env x in
     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 ~end_env:env_b @@ seq [
+    let%bind a' = translate_expression a env in
+    let%bind b' = translate_expression b env in
+    return @@ seq [
       a' ;
       b' ;
     ]
@@ -264,12 +191,12 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       let module L = Logger.Stateful() in
       let%bind lst' =
         let aux env expr =
-          let%bind (code , env') = translate_expression ~push_var_name:"constant_argx" expr env in
+          let%bind code = translate_expression expr env in
           L.log @@ Format.asprintf "\n%a -> %a in %a\n"
             PP.expression expr
             Michelson.pp code
             PP.environment env ;
-          ok (env' , code)
+          ok (env , code)
         in
         bind_fold_map_right_list aux env lst in
       let%bind predicate = get_predicate str ty lst in
@@ -312,24 +239,22 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       let%bind o' = Compiler_type.type_ o in
       return @@ i_none o'
   | E_if_bool (c, a, b) -> (
-      let%bind (c' , env') = translate_expression ~push_var_name:"bool_condition" c env in
-      let%bind popped = Compiler_environment.pop env' in
-      let%bind (a' , env_a') = translate_expression ~push_var_name:"if_true" a popped in
-      let%bind (b' , _env_b') = translate_expression ~push_var_name:"if_false" b popped in
+      let%bind c' = translate_expression c env in
+      let%bind a' = translate_expression a env in
+      let%bind b' = translate_expression b env in
       let%bind code = ok (seq [
           c' ;
           i_if a' b' ;
         ]) in
-      return ~end_env:env_a' code
+      return code
     )
   | E_if_none (c, n, (ntv , s)) -> (
-      let%bind (c' , env') = translate_expression ~push_var_name:"if_none_condition" c env in
-      let%bind popped = Compiler_environment.pop env' in
-      let%bind (n' , _) = translate_expression ~push_var_name:"if_none" n popped in
-      let s_env = Environment.add ntv popped in
-      let%bind (s' , s_env') = translate_expression ~push_var_name:"if_some" s s_env in
-      let%bind popped' = Compiler_environment.pop s_env' in
-      let%bind restrict_s = Compiler_environment.select_env popped' popped in
+      let%bind c' = 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 popped' = Compiler_environment.pop s_env in
+      let%bind restrict_s = Compiler_environment.select_env popped' env in
       let%bind code = ok (seq [
           c' ;
           i_if_none n' (seq [
@@ -341,11 +266,11 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       return code
     )
   | E_if_left (c, (l_ntv , l), (r_ntv , r)) -> (
-      let%bind (c' , _env') = translate_expression ~push_var_name:"if_left_cond" c env in
+      let%bind c' = translate_expression c env in
       let l_env = Environment.add l_ntv env in
-      let%bind (l' , _l_env') = translate_expression ~push_var_name:"if_left" l l_env in
+      let%bind l' = translate_expression l l_env in
       let r_env = Environment.add r_ntv env in
-      let%bind (r' , _r_env') = translate_expression ~push_var_name:"if_right" r r_env in
+      let%bind r' = translate_expression r r_env in
       let%bind restrict_l = Compiler_environment.select_env l_env env in
       let%bind restrict_r = Compiler_environment.select_env r_env env in
       let%bind code = ok (seq [
@@ -364,13 +289,13 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       return code
     )
   | E_let_in (v , expr , body) -> (
-      let%bind (expr' , expr_env) = translate_expression ~push_var_name:"let_expr" expr env in
+      let%bind expr' = translate_expression expr env in
       let%bind env' =
-        let%bind popped = Compiler_environment.pop expr_env in
+        let%bind popped = Compiler_environment.pop env in
         ok @@ Environment.add v popped in
-      let%bind (body' , body_env) = translate_expression ~push_var_name:"let_body" body env' in
+      let%bind body' = translate_expression body env' in
       let%bind restrict =
-        let%bind popped = Compiler_environment.pop body_env in
+        let%bind popped = Compiler_environment.pop env in
         Compiler_environment.select_env popped env in
       let%bind code = ok (seq [
           expr' ;
@@ -381,29 +306,29 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       return code
     )
   | E_iterator (name , (v , body) , expr) -> (
-      let%bind (expr' , expr_env) = translate_expression ~push_var_name:"iter_expr" expr env in
-      let%bind popped = Compiler_environment.pop expr_env in
+      let%bind expr' = translate_expression expr env in
+      let%bind popped = Compiler_environment.pop env in
       let%bind env' = ok @@ Environment.add v popped in
-      let%bind (body' , body_env) = translate_expression ~push_var_name:"iter_body" body env' in
+      let%bind body' = translate_expression body env' in
       match name with
       | "ITER" -> (
           let%bind restrict =
-            Compiler_environment.select_env body_env popped in
+            Compiler_environment.select_env env popped in
           let%bind code = ok (seq [
               expr' ;
               i_iter (seq [body' ; restrict]) ;
             ]) in
-          return ~end_env:popped code
+          return code
         )
       | "MAP" -> (
           let%bind restrict =
-            let%bind popped' = Compiler_environment.pop body_env in
+            let%bind popped' = Compiler_environment.pop env in
             Compiler_environment.select_env popped' popped in
           let%bind code = ok (seq [
               expr' ;
               i_map (seq [body' ; dip restrict]) ;
             ]) in
-          return ~prepend_env:popped code
+          return code
         )
       | s -> (
           let error = error (thunk "bad iterator") (thunk s) in
@@ -411,8 +336,8 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
         )
     )
   | E_assignment (name , lrs , expr) -> (
-      let%bind (expr' , env') = translate_expression ~push_var_name:"assignment_expr" expr env in
-      let%bind get_code = Compiler_environment.get env' name in
+      let%bind expr' = translate_expression expr env 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]
@@ -433,7 +358,7 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
         in
         error title content in
       trace error @@
-      return ~end_env:env ~unit_opt:true @@ seq [
+      return @@ seq [
         i_comment "assign: start # env" ;
         expr' ;
         i_comment "assign: compute rhs # rhs : env" ;
@@ -448,11 +373,11 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       ]
     )
   | E_while (expr , block) -> (
-      let%bind (expr' , env') = translate_expression ~push_var_name:"while_expr" expr env in
-      let%bind popped = Compiler_environment.pop env' in
-      let%bind (block' , env'') = translate_expression block popped in
-      let%bind restrict_block = Compiler_environment.select_env env'' popped in
-      return ~end_env:env ~unit_opt:true @@ seq [
+      let%bind expr' = translate_expression expr env in
+      let%bind popped = Compiler_environment.pop env in
+      let%bind block' = translate_expression block popped in
+      let%bind restrict_block = Compiler_environment.select_env env popped in
+      return @@ seq [
         expr' ;
         prim ~children:[seq [
             block' ;
@@ -461,39 +386,14 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
       ]
     )
 
-and translate_quote_body ({result ; binder ; input} as f:anon_function) : michelson result =
+and translate_quote_body ({result ; binder} : anon_function) input : michelson result =
   let env = Environment.(add (binder , input) empty) in
-  let%bind (expr , env') = translate_expression result env in
+  let%bind expr = translate_expression result env in
   let code = seq [
       i_comment "function result" ;
       expr ;
     ] in
 
-  let%bind _assert_type =
-    let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ f.input in
-    let%bind (Ex_ty output_ty) = Compiler_type.Ty.type_ f.output in
-    let input_stack_ty = Stack.(input_ty @: nil) in
-    let output_stack_ty = Stack.(output_ty @: nil) in
-    let error_message () =
-      Format.asprintf
-        "\nCode : %a\nMichelson code : %a\ninput : %a\noutput : %a\nstart env : %a\nend env : %a\n"
-        PP.expression result
-        Michelson.pp code
-        PP.type_ f.input
-        PP.type_ f.output
-        PP.environment env
-        PP.environment env'
-    in
-    let%bind _ =
-      Trace.trace_tzresult_lwt (
-        error (thunk "error parsing quote code") error_message
-      ) @@
-      Proto_alpha_utils.Memory_proto_alpha.parse_michelson code
-        input_stack_ty output_stack_ty
-    in
-    ok ()
-  in
-
   ok code
 
 type compiled_program = {
@@ -502,12 +402,12 @@ type compiled_program = {
   body : michelson ;
 }
 
-let get_main : program -> string -> anon_function result = fun p entry ->
+let get_main : program -> string -> (anon_function * _) result = fun p entry ->
   let is_main (((name , expr), _):toplevel_statement) =
     match Combinators.Expression.(get_content expr , get_type expr)with
-    | (E_literal (D_function content) , T_function _)
+    | (E_literal (D_function content) , T_function ty)
       when name = entry ->
-        Some content
+        Some (content , ty)
     | _ ->  None
   in
   let%bind main =
@@ -517,18 +417,17 @@ let get_main : program -> string -> anon_function result = fun p entry ->
   ok main
 
 let translate_program (p:program) (entry:string) : compiled_program result =
-  let%bind main = get_main p entry in
-  let {input;output} : anon_function = main in
-  let%bind body = translate_quote_body main in
+  let%bind (main , (input , output)) = get_main p entry in
+  let%bind body = translate_quote_body main input in
   let%bind input = Compiler_type.Ty.type_ input in
   let%bind output = Compiler_type.Ty.type_ output in
   ok ({input;output;body}:compiled_program)
 
-let translate_entry (p:anon_function) : compiled_program result =
-  let {input;output} : anon_function = p in
+let translate_entry (p:anon_function) ty : compiled_program result =
+  let (input , output) = ty in
   let%bind body =
     trace (simple_error "compile entry body") @@
-    translate_quote_body p in
+    translate_quote_body p input in
   let%bind input = Compiler_type.Ty.type_ input in
   let%bind output = Compiler_type.Ty.type_ output in
   ok ({input;output;body}:compiled_program)
@@ -547,11 +446,11 @@ them. please report this to the developers." in
 end
 open Errors
 
-let translate_contract : anon_function -> michelson result = fun f ->
+let translate_contract : anon_function -> _ -> michelson result = fun f ty ->
   let%bind compiled_program =
     trace_strong (corner_case ~loc:__LOC__ "compiling") @@
-    translate_entry f in
-  let%bind (param_ty , storage_ty) = Combinators.get_t_pair f.input in
+    translate_entry f ty in
+  let%bind (param_ty , storage_ty) = Combinators.get_t_pair (fst ty) in
   let%bind param_michelson = Compiler_type.type_ param_ty in
   let%bind storage_michelson = Compiler_type.type_ storage_ty in
   let contract = Michelson.contract param_michelson storage_michelson compiled_program.body in
diff --git a/src/main/run_mini_c.ml b/src/main/run_mini_c.ml
index 5c8f12e5d..725ad67f6 100644
--- a/src/main/run_mini_c.ml
+++ b/src/main/run_mini_c.ml
@@ -22,7 +22,7 @@ let run_aux ?options (program:compiled_program) (input_michelson:Michelson.t) :
     Memory_proto_alpha.interpret ?options descr (Item(input, Empty)) in
   ok (Ex_typed_value (output_ty, output))
 
-let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:value) : value result =
+let run_entry ?(debug_michelson = false) ?options (entry:anon_function) ty (input:value) : value result =
   let%bind compiled =
     let error =
       let title () = "compile entry" in
@@ -31,13 +31,13 @@ let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:v
       in
       error title content in
     trace error @@
-    translate_entry entry in
-  let%bind input_michelson = translate_value input in
+    translate_entry entry ty in
+  let%bind input_michelson = translate_value input (fst ty) in
   if debug_michelson then (
     Format.printf "Program: %a\n" Michelson.pp compiled.body ;
     Format.printf "Expression: %a\n" PP.expression entry.result ;
     Format.printf "Input: %a\n" PP.value input ;
-    Format.printf "Input Type: %a\n" PP.type_ entry.input ;
+    Format.printf "Input Type: %a\n" PP.type_ (fst ty) ;
     Format.printf "Compiled Input: %a\n" Michelson.pp input_michelson ;
   ) ;
   let%bind ex_ty_value = run_aux ?options compiled input_michelson in
diff --git a/src/main/run_source.ml b/src/main/run_source.ml
index a0a18be96..1a5eaa431 100644
--- a/src/main/run_source.ml
+++ b/src/main/run_source.ml
@@ -47,8 +47,8 @@ include struct
 end
 
 let transpile_value
-    (e:Ast_typed.annotated_expression) : Mini_c.value result =
-  let%bind f =
+    (e:Ast_typed.annotated_expression) : (Mini_c.value * _) result =
+  let%bind (f , ty) =
     let open Transpiler in
     let (f , _) = functionalize e in
     let%bind main = translate_main f e.location in
@@ -56,8 +56,8 @@ let transpile_value
   in
 
   let input = Mini_c.Combinators.d_unit in
-  let%bind r = Run_mini_c.run_entry f input in
-  ok r
+  let%bind r = Run_mini_c.run_entry f ty input in
+  ok (r , snd ty)
 
 let parsify_pascaligo = fun source ->
   let%bind raw =
@@ -148,12 +148,12 @@ let compile_contract_file : string -> string -> s_syntax -> string result = fun
   let%bind typed =
     trace (simple_error "typing") @@
     Typer.type_program simplified in
-  let%bind mini_c =
+  let%bind (mini_c , mini_c_ty) =
     trace (simple_error "transpiling") @@
     Transpiler.translate_entry typed entry_point in
   let%bind michelson =
     trace (simple_error "compiling") @@
-    Compiler.translate_contract mini_c in
+    Compiler.translate_contract mini_c mini_c_ty in
   let str =
     Format.asprintf "%a" Michelson.pp_stripped michelson in
   ok str
@@ -184,12 +184,12 @@ let compile_contract_parameter : string -> string -> string -> s_syntax -> strin
     let%bind () =
       trace (simple_error "expression type doesn't match type parameter") @@
       Ast_typed.assert_type_value_eq (parameter_tv , typed.type_annotation) in
-    let%bind mini_c =
+    let%bind (mini_c , mini_c_ty) =
       trace (simple_error "transpiling expression") @@
       transpile_value typed in
     let%bind michelson =
       trace (simple_error "compiling expression") @@
-      Compiler.translate_value mini_c in
+      Compiler.translate_value mini_c mini_c_ty in
     let str =
       Format.asprintf "%a" Michelson.pp_stripped michelson in
     ok str
@@ -223,12 +223,12 @@ let compile_contract_storage : string -> string -> string -> s_syntax -> string
     let%bind () =
       trace (simple_error "expression type doesn't match type storage") @@
       Ast_typed.assert_type_value_eq (storage_tv , typed.type_annotation) in
-    let%bind mini_c =
+    let%bind (mini_c , mini_c_ty) =
       trace (simple_error "transpiling expression") @@
       transpile_value typed in
     let%bind michelson =
       trace (simple_error "compiling expression") @@
-      Compiler.translate_value mini_c in
+      Compiler.translate_value mini_c mini_c_ty in
     let str =
       Format.asprintf "%a" Michelson.pp_stripped michelson in
     ok str
diff --git a/src/main/run_typed.ml b/src/main/run_typed.ml
index 788a10406..fc136c63c 100644
--- a/src/main/run_typed.ml
+++ b/src/main/run_typed.ml
@@ -2,7 +2,7 @@ open Trace
 
 let transpile_value
     (e:Ast_typed.annotated_expression) : Mini_c.value result =
-  let%bind f =
+  let%bind (f , ty) =
     let open Transpiler in
     let (f , _) = functionalize e in
     let%bind main = translate_main f e.location in
@@ -10,7 +10,7 @@ let transpile_value
   in
 
   let input = Mini_c.Combinators.d_unit in
-  let%bind r = Run_mini_c.run_entry f input in
+  let%bind r = Run_mini_c.run_entry f ty input in
   ok r
 
 let evaluate_typed
@@ -18,12 +18,12 @@ let evaluate_typed
     ?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result =
   trace (simple_error "easy evaluate typed") @@
   let%bind result =
-    let%bind mini_c_main =
+    let%bind (mini_c_main , ty) =
       Transpiler.translate_entry program entry in
     (if debug_mini_c then
        Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main)
     ) ;
-    Run_mini_c.run_entry ?options ~debug_michelson mini_c_main (Mini_c.Combinators.d_unit)
+    Run_mini_c.run_entry ?options ~debug_michelson mini_c_main ty (Mini_c.Combinators.d_unit)
   in
   let%bind typed_result =
     let%bind typed_main = Ast_typed.get_entry program entry in
@@ -42,7 +42,7 @@ let run_typed
     Ast_typed.assert_type_value_eq (arg_ty , (Ast_typed.get_type_annotation input))
   in
 
-  let%bind mini_c_main =
+  let%bind (mini_c_main , ty) =
     trace (simple_error "transpile mini_c entry") @@
     Transpiler.translate_entry program entry in
   (if debug_mini_c then
@@ -59,7 +59,7 @@ let run_typed
       in
       error title content in
     trace error @@
-    Run_mini_c.run_entry ~debug_michelson ?options mini_c_main mini_c_value in
+    Run_mini_c.run_entry ~debug_michelson ?options mini_c_main ty mini_c_value in
   let%bind typed_result =
     let%bind main_result_type =
       let%bind typed_main = Ast_typed.get_functional_entry program entry in
diff --git a/src/mini_c/PP.ml b/src/mini_c/PP.ml
index 3d0e3f065..44d8f2719 100644
--- a/src/mini_c/PP.ml
+++ b/src/mini_c/PP.ml
@@ -66,10 +66,6 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
   fprintf ppf "%a -> %a" value a value b
 
 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 "V(%s)" v
   | E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b
@@ -101,11 +97,9 @@ and expression_with_type : _ -> expression -> _  = fun ppf e ->
     expression' e.content
     type_ e.type_value
 
-and function_ ppf ({binder ; input ; output ; result}:anon_function) =
-  fprintf ppf "fun (%s:%a) : %a (%a)"
+and function_ ppf ({binder ; result}:anon_function) =
+  fprintf ppf "fun %s -> (%a)"
     binder
-    type_ input
-    type_ output
     expression result
 
 and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e
diff --git a/src/mini_c/combinators.ml b/src/mini_c/combinators.ml
index 3aa4d5726..f7342987e 100644
--- a/src/mini_c/combinators.ml
+++ b/src/mini_c/combinators.ml
@@ -82,6 +82,10 @@ let get_t_pair (t:type_value) = match t with
   | T_pair (a, b) -> ok (a, b)
   | _ -> simple_fail "not a type pair"
 
+let get_t_or (t:type_value) = match t with
+  | T_or (a, b) -> ok (a, b)
+  | _ -> simple_fail "not a type or"
+
 let get_t_map (t:type_value) = match t with
   | T_map kv -> ok kv
   | _ -> simple_fail "not a type map"
@@ -142,9 +146,9 @@ 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 result : anon_function =
+let quote binder result : anon_function =
   {
-    binder ; input ; output ;
+    binder ;
     result ;
   }
 
@@ -160,15 +164,15 @@ let e_let_int v tv expr body : expression = Expression.(make_tpl (
 
 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 ez_e_return e : expression = 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_quote expr : anon_function result =
+  ok @@ quote "input" (ez_e_return expr)
 
 let basic_int_quote expr : anon_function result =
-  basic_quote t_int t_int expr
+  basic_quote expr
 
 
 let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }
diff --git a/src/mini_c/types.ml b/src/mini_c/types.ml
index 3e9a69819..412a2625c 100644
--- a/src/mini_c/types.ml
+++ b/src/mini_c/types.ml
@@ -11,7 +11,7 @@ type type_base =
 type type_value =
   | T_pair of (type_value * type_value)
   | T_or of type_value * type_value
-  | T_function of type_value * type_value
+  | T_function of (type_value * type_value)
   | T_deep_closure of environment * type_value * type_value
   | T_base of type_base
   | T_map of (type_value * type_value)
@@ -57,10 +57,6 @@ and selector = var_name list
 
 and expression' =
   | E_literal of value
-  | 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
@@ -75,7 +71,6 @@ 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
 
@@ -91,8 +86,6 @@ and toplevel_statement = assignment * environment_wrap
 
 and anon_function = {
   binder : string ;
-  input : type_value ;
-  output : type_value ;
   result : expression ;
 }
 
diff --git a/src/test/compiler_tests.ml b/src/test/compiler_tests.ml
index af26e74d4..0407c281f 100644
--- a/src/test/compiler_tests.ml
+++ b/src/test/compiler_tests.ml
@@ -5,7 +5,7 @@ open Test_helpers
 
 let run_entry_int (e:anon_function) (n:int) : int result =
   let param : value = D_int n in
-  let%bind result = Main.Run_mini_c.run_entry e param in
+  let%bind result = Main.Run_mini_c.run_entry e (t_int , t_int) param in
   match result with
   | D_int n -> ok n
   | _ -> simple_fail "result is not an int"
diff --git a/src/transpiler/transpiler.ml b/src/transpiler/transpiler.ml
index 3aed3edb5..facd0c717 100644
--- a/src/transpiler/transpiler.ml
+++ b/src/transpiler/transpiler.ml
@@ -547,29 +547,19 @@ 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 ; result } : AST.lambda = l in
   (* Deep capture. Capture the relevant part of the environment. *)
-  let%bind (fv , c_env , c_tv) =
+  let%bind c_env =
     let free_variables = Ast_typed.Free_variables.lambda [] l in
     let sub_env = Mini_c.Environment.select free_variables env in
-    let tv = Environment.closure_representation sub_env in
-    ok (free_variables , sub_env , tv) in
+    ok sub_env in
   let%bind (f_expr , input_tv , output_tv) =
     let%bind raw_input = translate_type input_type in
-    let init_env = Environment.(add (binder , raw_input) c_env) in
-    let input = Environment.closure_representation init_env in
     let%bind output = translate_type output_type in
     let%bind result = translate_annotated_expression result in
-    let result =
-      let load_expr = Expression.make_tpl (E_variable binder , input) in
-      ez_e_return @@ ez_e_sequence (E_environment_load (load_expr , init_env)) result in
-    let tv = Mini_c.t_function input output in
-    let f_literal = D_function { binder ; input ; output ; result } in
-    let expr = Expression.make_tpl (E_literal f_literal , tv) in
-    ok (expr , raw_input , output) in
-  let%bind c_expr =
-    ok @@ Expression.make_tpl (E_environment_capture fv , c_tv) in
-  let expr = Expression.pair f_expr c_expr in
+    let f_literal = D_function { binder ; result } in
+    let expr' = E_literal f_literal in
+    ok (expr' , raw_input , output) in
   let tv = Mini_c.t_deep_closure c_env input_tv output_tv in
-  ok @@ Expression.make_tpl (expr , tv)
+  ok @@ Expression.make_tpl (f_expr , tv)
 
 and translate_lambda env l =
   let { binder ; input_type ; output_type ; result } : AST.lambda = l in
@@ -583,7 +573,7 @@ and translate_lambda env l =
         let%bind input = translate_type input_type in
         let%bind output = translate_type output_type in
         let tv = Combinators.t_function input output in
-        let content = D_function {binder;input;output;result=result'} in
+        let content = D_function {binder;result=result'} in
         ok @@ Combinators.Expression.make_tpl (E_literal content , tv)
       )
     | _ -> (
@@ -608,10 +598,10 @@ let translate_program (lst:AST.program) : program result =
   let%bind (statements, _) = List.fold_left aux (ok ([], Environment.empty)) (temp_unwrap_loc_list lst) in
   ok statements
 
-let translate_main (l:AST.lambda) loc : anon_function result =
+let translate_main (l:AST.lambda) loc : (anon_function * _) result =
   let%bind expr = translate_lambda Environment.empty l in
-  match Combinators.Expression.get_content expr with
-  | E_literal (D_function f) -> ok f
+  match expr.content , expr.type_value with
+  | E_literal (D_function f) , T_function ty -> ok (f , ty)
   | _ -> fail @@ not_functional_main loc
 
 (* From an expression [expr], build the expression [fun () -> expr] *)
@@ -625,7 +615,7 @@ let functionalize (e:AST.annotated_expression) : AST.lambda * AST.type_value =
     result = e ;
   }, Combinators.(t_function (t_unit ()) t ())
 
-let translate_entry (lst:AST.program) (name:string) : anon_function result =
+let translate_entry (lst:AST.program) (name:string) : (anon_function * _) result =
   let rec aux acc (lst:AST.program) =
     let%bind acc = acc in
     match lst with