revert let_in as lambda and add let_in

src/ast_simplified/PP.ml

@@ -44,12 +44,14 @@ let rec expression ppf (e:expression) = match e with
   | 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_annotation input_type type_annotation output_type
+        binder type_expression input_type type_expression output_type
         block body annotated_expression result
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
   | E_failwith ae ->
       fprintf ppf "failwith %a" annotated_expression ae
+  | E_let_in { binder; rhs; result } ->
+      fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result
 
 and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
   fprintf ppf "%a -> %a" annotated_expression a annotated_expression b

src/ast_simplified/combinators.ml

@@ -137,8 +137,8 @@ let e_lambda (binder : string)
   : expression =
   E_lambda {
     binder = (make_name binder) ;
-    input_type = Some input_type ;
-    output_type = Some output_type ;
+    input_type = input_type ;
+    output_type = output_type ;
     result = (make_e_a result) ;
     body ;
   }

src/ast_simplified/types.ml

@@ -1,3 +1,4 @@
+[@@@warning "-30"]
 module Map = Simple_utils.Map
 module Location = Simple_utils.Location
 
@@ -47,12 +48,18 @@ and type_expression =
 
 and lambda = {
   binder: name ;
-  input_type: type_expression option;
-  output_type: type_expression option;
+  input_type: type_expression;
+  output_type: type_expression;
   result: ae ;
   body: block ;
 }
 
+and let_in = {
+  binder : name;
+  rhs    : ae;
+  result : ae;
+}
+
 and expression =
   (* Base *)
   | E_literal of literal
@@ -60,6 +67,7 @@ and expression =
   | E_variable of name
   | E_lambda of lambda
   | E_application of (ae * ae)
+  | E_let_in of let_in
   (* E_Tuple *)
   | E_tuple of ae list
   (* Sum *)

src/ast_typed/PP.ml

@@ -47,6 +47,8 @@ and expression ppf (e:expression) : unit =
   | E_matching (ae, m) ->
       fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
   | E_failwith ae -> fprintf ppf "failwith %a" annotated_expression ae
+  | E_let_in { binder; rhs; result } ->
+      fprintf ppf "let %s = %a in %a" binder annotated_expression rhs annotated_expression result
 
 and value ppf v = annotated_expression ppf v
 

src/ast_typed/misc.ml

@@ -59,6 +59,12 @@ module Free_variables = struct
     | E_look_up (a , b) -> unions @@ List.map self [ a ; b ]
     | E_matching (a , cs) -> union (self a) (matching_expression b cs)
     | E_failwith a -> self a
+    | E_let_in { binder; rhs; result } ->
+      let b' = union (singleton binder) b in
+      union
+        (annotated_expression b' result)
+        (annotated_expression b' rhs) (* TODO: what about frees ??? *)
+
 
   and lambda : bindings -> lambda -> bindings = fun b l ->
     let b' = union (singleton l.binder) b in

src/ast_typed/misc_smart.ml

@@ -94,6 +94,7 @@ module Captured_variables = struct
       let%bind cs' = matching_expression b cs in
       ok @@ union a' cs'
     | E_failwith a -> self a
+    | E_let_in { binder; rhs; result } -> ignore (binder, rhs, result); (failwith "TODO")
 
   and instruction' : bindings -> instruction -> (bindings * bindings) result = fun b i ->
     match i with

src/ast_typed/types.ml

@@ -75,6 +75,12 @@ and lambda = {
   body: block ;
 }
 
+and let_in = {
+  binder: name;
+  rhs: ae;
+  result: ae;
+}
+
 and expression =
   (* Base *)
   | E_literal of literal
@@ -82,6 +88,7 @@ and expression =
   | E_variable of name
   | E_application of (ae * ae)
   | E_lambda of lambda
+  | E_let_in of let_in
   (* Tuple *)
   | E_tuple of ae list
   | E_tuple_accessor of (ae * int) (* Access n'th tuple's element *)

src/simplify/camligo.ml

@@ -461,8 +461,8 @@ let let_entry : _ -> _ result = fun l ->
   let lambda =
     O.{
       binder = input_nty.type_name ;
-      input_type = Some input_type';
-      output_type = Some output_type';
+      input_type = input_type';
+      output_type = output_type';
       result ;
       body = tpl_declarations @ body' ;
     } in

src/simplify/pascaligo.ml

@@ -350,8 +350,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
        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 = Some input_type;
-                                  output_type = Some output_type; result ; body } in
+       let expression = E_lambda {binder ; input_type = input_type;
+                                  output_type = output_type; result ; body } in
        let type_annotation = Some (T_function (input_type, output_type)) in
        ok {name;annotated_expression = {expression;type_annotation}}
      )
@@ -390,8 +390,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
 
        let body = tpl_declarations @ local_declarations @ instructions in
        let%bind result = simpl_expression return in
-       let expression = E_lambda {binder ; input_type = Some input_type;
-                                  output_type = Some output_type; result ; body } in
+       let expression = E_lambda {binder ; input_type = input_type;
+                                  output_type = output_type; result ; body } in
        let type_annotation = Some (T_function (input_type, output_type)) in
        ok {name = name.value;annotated_expression = {expression;type_annotation}}
      )

src/transpiler/transpiler.ml

@@ -247,12 +247,10 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
   let f = translate_annotated_expression in
   match ae.expression with
     (* Optimise immediate application as a let-in *)
-  | E_application ({expression = E_lambda {binder; input_type; output_type=_; body=[]; result}; _},
-                   rhs) ->
-    let%bind ty' = translate_type input_type in
+  | E_let_in {binder; rhs; result} ->
     let%bind rhs' = translate_annotated_expression rhs in
     let%bind result' = translate_annotated_expression result in
-    return (E_let_in ((binder, ty'), rhs', result'))
+    return (E_let_in ((binder, rhs'.type_value), rhs', result'))
   | E_failwith ae -> (
       let%bind ae' = translate_annotated_expression ae in
       return @@ E_constant ("FAILWITH" , [ae'])

src/typer/typer.ml

@@ -490,16 +490,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
       result ;
       body ;
     } -> (
-      let%bind input_type =
-        let%bind input_type =
-          trace_option (simple_error "missing annotation on input type")
-            input_type in
-        evaluate_type e input_type in
-      let%bind output_type =
-        let%bind output_type =
-          trace_option (simple_error "missing annotation of output type")
-            output_type in
-        evaluate_type e output_type in
+      let%bind input_type = evaluate_type e input_type in
+      let%bind output_type = 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
@@ -571,6 +563,11 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
           return (O.E_matching (ex', m')) tv
         )
     )
+  | 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%bind result = type_annotated_expression e' result in
+    return (E_let_in {binder; rhs; result}) result.type_annotation
 
 and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value option) : (string * O.type_value) result =
   (* Constant poorman's polymorphism *)
@@ -645,7 +642,7 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
       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 = Some input_type;output_type = Some output_type;body;result})
+      return (E_lambda {binder;input_type = input_type;output_type = output_type;body;result})
   | E_tuple lst ->
       let%bind lst' = bind_list
         @@ List.map untype_annotated_expression lst in
@@ -679,6 +676,10 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
   | E_failwith ae ->
       let%bind ae' = untype_annotated_expression ae in
       return (E_failwith ae')
+  | E_let_in {binder;rhs;result} ->
+      let%bind rhs = untype_annotated_expression rhs in
+      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