Merge branch 'ast/tail_recursion' into 'dev'

Adding tail recursion in Ligo

See merge request ligolang/ligo!491

gitlab-pages/docs/language-basics/functions.md

@@ -299,3 +299,43 @@ gitlab-pages/docs/language-basics/src/functions/incr_map.religo incr_map
 
 </Syntax>
 
+## Recursive function
+
+LIGO functions are not recursive by default, the user need to indicate that the function is recursive.
+
+At the moment, recursive function are limited to one (possibly tupled) parameter and recursion is
+limited to tail recursion (i.e the recursive call should be the last expression of the function)
+
+<Syntax syntax="pascaligo">
+In PascaLigo recursive functions are defined using the `recursive` keyword
+
+```pascaligo group=d
+recursive function sum (const n : int; const acc: int) : int is
+  if n<1 then acc else sum(n-1,acc+n)
+
+recursive function fibo (const n: int; const n_1: int; const n_0 :int) : int is
+  if n<2 then n_1 else fibo(n-1,n_1+n_0,n_1)
+```
+</Syntax>
+<Syntax syntax="cameligo">
+In CameLigo recursive functions are defined using the `rec` keyword
+
+```cameligo group=d
+let rec sum ((n,acc):int * int) : int =
+    if (n < 1) then acc else sum (n-1, acc+n)
+ 
+let rec fibo ((n,n_1,n_0):int*int*int) : int = 
+    if (n < 2) then n_1 else fibo (n-1, n_1 + n_0, n_1)
+```
+</Syntax>
+<Syntax syntax="reasonligo">
+In ReasonLigo recursive functions are defined using the `rec` keyword
+
+```reasonligo group=d
+let rec sum = ((n, acc) : (int,int)): int =>
+    if (n < 1) {acc;} else {sum ((n-1,acc+n));};
+
+let rec fibo = ((n, n_1, n_0) : (int,int,int)): int =>
+    if (n < 2) {n_1;} else {fibo ((n-1,n_1+n_0,n_1));};
+```
+</Syntax>

gitlab-pages/docs/language-basics/loops.md

@@ -57,45 +57,21 @@ constant, therefore it makes no sense in CameLIGO to feature loops,
 which we understand as syntactic constructs where the state of a
 stopping condition is mutated, as with "while" loops in PascaLIGO.
 
-Instead, CameLIGO implements a *folded operation* by means of a
+Instead, CameLIGO loops are written by means of a tail recursive function
-predefined function named `Loop.fold_while`. It takes an initial value
-of a certain type, called an *accumulator*, and repeatedly calls a
-given function, called *folded function*, that takes that
-accumulator and returns the next value of the accumulator, until a
-condition is met and the fold stops with the final value of the
-accumulator. The iterated function needs to have a special type: if
-the type of the accumulator is `t`, then it must have the type `bool *
-t` (not simply `t`). It is the boolean value that denotes whether the
-stopping condition has been reached.
 
 Here is how to compute the greatest common divisors of two natural
 numbers by means of Euclid's algorithm:
 
 ```cameligo group=a
-let iter (x,y : nat * nat) : bool * (nat * nat) =
+let rec iter (x,y : nat * nat) : nat =
-  if y = 0n then false, (x,y) else true, (y, x mod y)
+  if y = 0n then x else iter (y, x mod y)
 
 let gcd (x,y : nat * nat) : nat =
   let x,y = if x < y then y,x else x,y in
-  let x,y = Loop.fold_while iter (x,y)
+  iter (x,y)
-  in x
 ```
 
-To ease the writing and reading of the iterated functions (here,
+> Note that `fold_while`, `stop` and `continue` (now `Loop.resume`) are
-`iter`), two predefined functions are provided: `Loop.resume` and
-`Loop.stop`:
-
-```cameligo group=a
-let iter (x,y : nat * nat) : bool * (nat * nat) =
-  if y = 0n then Loop.stop (x,y) else Loop.resume (y, x mod y)
-
-let gcd (x,y : nat * nat) : nat =
-  let x,y = if x < y then y,x else x,y in
-  let x,y = Loop.fold_while iter (x,y)
-  in x
-```
-
-> Note that `stop` and `continue` (now `Loop.resume`) are
 > *deprecated*.
 
 You can call the function `gcd` defined above using the LIGO compiler
@@ -114,47 +90,22 @@ constant, therefore it makes no sense in ReasonLIGO to feature loops,
 which we understand as syntactic constructs where the state of a
 stopping condition is mutated, as with "while" loops in PascaLIGO.
 
-Instead, ReasonLIGO features a *fold operation* as a predefined
+Instead, ReasonLIGO loops are written by means of tail recursive functions
-function named `Loop.fold_while`. It takes an initial value of a
-certain type, called an *accumulator*, and repeatedly calls a given
-function, called *iterated function*, that takes that accumulator and
-returns the next value of the accumulator, until a condition is met
-and the fold stops with the final value of the accumulator. The
-iterated function needs to have a special type: if the type of the
-accumulator is `t`, then it must have the type `bool * t` (not simply
-`t`). It is the boolean value that denotes whether the stopping
-condition has been reached.
 
 Here is how to compute the greatest common divisors of two natural
 numbers by means of Euclid's algorithm:
 
 ```reasonligo group=a
-let iter = ((x,y) : (nat, nat)) : (bool, (nat, nat)) =>
+let rec iter = ((x,y) : (nat, nat)) : nat =>
-  if (y == 0n) { (false, (x,y)); } else { (true, (y, x mod y)); };
+  if (y == 0n) { x; } else { iter ((y, x mod y)); };
 
 let gcd = ((x,y) : (nat, nat)) : nat => {
   let (x,y) = if (x < y) { (y,x); } else { (x,y); };
-  let (x,y) = Loop.fold_while (iter, (x,y));
+  iter ((x,y))
-  x
 };
 ```
 
-To ease the writing and reading of the iterated functions (here,
+> Note that `fold_while`, `stop` and `continue` (now `Loop.resume`) are
-`iter`), two predefined functions are provided: `Loop.resume` and
-`Loop.stop`:
-
-```reasonligo group=b
-let iter = ((x,y) : (nat, nat)) : (bool, (nat, nat)) =>
-  if (y == 0n) { Loop.stop ((x,y)); } else { Loop.resume ((y, x mod y)); };
-
-let gcd = ((x,y) : (nat, nat)) : nat => {
-  let (x,y) = if (x < y) { (y,x); } else { (x,y); };
-  let (x,y) = Loop.fold_while (iter, (x,y));
-  x
-};
-```
-
-> Note that `stop` and `continue` (now `Loop.resume`) are
 > *deprecated*.
 
 </Syntax>

src/bin/expect_tests/contract_tests.ml

@@ -1174,7 +1174,7 @@ let%expect_test _ =
 let%expect_test _ =
   run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ;
   [%expect {|
-ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P : ( nat * string ):Some(( nat * string ))) : None return let rhs#809 = #P in let p = rhs#809.0 in let s = rhs#809.1 in ( list[] : (TO_list(operation)) , store ) , NONE() : (TO_option(key_hash)) , 300000000mutez , \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
+ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return let rhs#812 = #P in let p = rhs#812.0 in let s = rhs#812.1 in ( list[] : (TO_list(operation)) , store ) , NONE() : (TO_option(key_hash)) , 300000000mutez , \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"}
 
 
  If you're not sure how to fix this error, you can
@@ -1187,7 +1187,7 @@ ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8,
 
   run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ;
   [%expect {|
-ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P : ( nat * int ):Some(( nat * int ))) : None return let rhs#812 = #P in let p = rhs#812.0 in let s = rhs#812.1 in ( list[] : (TO_list(operation)) , a ) , NONE() : (TO_option(key_hash)) , 300000000mutez , 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
+ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return let rhs#815 = #P in let p = rhs#815.0 in let s = rhs#815.1 in ( list[] : (TO_list(operation)) , a ) , NONE() : (TO_option(key_hash)) , 300000000mutez , 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"}
 
 
  If you're not sure how to fix this error, you can
@@ -1344,4 +1344,4 @@ let%expect_test _ =
     * Visit our documentation: https://ligolang.org/docs/intro/what-and-why/
     * Ask a question on our Discord: https://discord.gg/9rhYaEt
     * Open a gitlab issue: https://gitlab.com/ligolang/ligo/issues/new
-    * Check the changelog by running 'ligo changelog' |}]
+    * Check the changelog by running 'ligo changelog' |}]

src/bin/expect_tests/ligo_interpreter_tests.ml

@@ -53,4 +53,7 @@ let%expect_test _ =
     val s = { ; 1 : int ; 2 : int ; 3 : int}
     val set_add = {  ; 0 = ({ ; 1 : int ; 2 : int ; 3 : int}) ; 1 = ({ ; 1 : int ; 2 : int ; 3 : int ; 4 : int}) ; 2 = ({ ; 1 : int}) }
     val set_iter_fail = "set_iter_fail" : failure
-    val set_mem = {  ; 0 = (true) ; 1 = (false) ; 2 = (false) } |}] ;
+    val set_mem = {  ; 0 = (true) ; 1 = (false) ; 2 = (false) }
+    val recursion_let_rec_in = 55 : int
+    val sum_rec = <rec fun>
+    val top_level_recursion = 55 : int |}] ;

src/bin/expect_tests/typer_error_tests.ml

@@ -32,6 +32,19 @@ let%expect_test _ =
     ligo: in file "", line 0, characters 0-0. different kinds:  {"a":"( (TO_list(operation)) * sum[Add -> int , Sub -> int] )","b":"sum[Add -> int , Sub -> int]"}
 
 
+     If you're not sure how to fix this error, you can
+     do one of the following:
+
+    * Visit our documentation: https://ligolang.org/docs/intro/what-and-why/
+    * Ask a question on our Discord: https://discord.gg/9rhYaEt
+    * Open a gitlab issue: https://gitlab.com/ligolang/ligo/issues/new
+    * Check the changelog by running 'ligo changelog' |}];
+
+  run_ligo_bad [ "compile-contract" ; "../../test/contracts/negative/error_no_tail_recursive_function.mligo"; "f"];
+  [%expect {|
+    ligo: in file "error_no_tail_recursive_function.mligo", line 2, characters 14-21. Recursion must be achieved through tail-calls only:  {"function":"unvalid","location":"in file \"error_no_tail_recursive_function.mligo\", line 2, characters 14-21"}
+
+
      If you're not sure how to fix this error, you can
      do one of the following:
 

src/main/compile/dune

@@ -9,10 +9,10 @@
     interpreter
     ast_simplified
     self_ast_simplified
-    self_ast_typed
     typer_new
     typer
     ast_typed
+    self_ast_typed
     transpiler
     mini_c
     self_mini_c

src/main/compile/of_simplified.ml

@@ -7,10 +7,11 @@ type form =
 let compile (cform: form) (program : Ast_simplified.program) : (Ast_typed.program * Typer.Solver.state) result =
   let%bind (prog_typed , state) = Typer.type_program program in
   let () = Typer.Solver.discard_state state in
-  let%bind prog_typed' = match cform with
+  let%bind applied = Self_ast_typed.all_program prog_typed in
-    | Contract entrypoint -> Self_ast_typed.all_contract entrypoint prog_typed
+  let%bind applied' = match cform with
-    | Env -> ok prog_typed in
+    | Contract entrypoint -> Self_ast_typed.all_contract entrypoint applied
-  ok @@ (prog_typed', state)
+    | Env -> ok applied in
+  ok @@ (applied', state)
 
 let compile_expression ?(env = Ast_typed.Environment.full_empty) ~(state : Typer.Solver.state) (ae : Ast_simplified.expression)
     : (Ast_typed.expression * Typer.Solver.state) result =

src/passes/1-parser/cameligo/AST.ml

@@ -30,6 +30,7 @@ type kwd_else  = Region.t
 type kwd_end   = Region.t
 type kwd_false = Region.t
 type kwd_fun   = Region.t
+type kwd_rec   = Region.t
 type kwd_if    = Region.t
 type kwd_in    = Region.t
 type kwd_let   = Region.t
@@ -134,7 +135,7 @@ and ast = t
 and attributes = attribute list
 
 and declaration =
-  Let      of (kwd_let * let_binding * attributes) reg
+  Let      of (kwd_let * kwd_rec option * let_binding * attributes) reg
 | TypeDecl of type_decl reg
 
 (* Non-recursive values *)
@@ -362,6 +363,7 @@ and 'a case_clause = {
 
 and let_in = {
   kwd_let    : kwd_let;
+  kwd_rec    : kwd_rec option;
   binding    : let_binding;
   kwd_in     : kwd_in;
   body       : expr;

src/passes/1-parser/cameligo/LexToken.mli

@@ -95,6 +95,7 @@ type t =
 | End   of Region.t
 | False of Region.t
 | Fun   of Region.t
+| Rec   of Region.t
 | If    of Region.t
 | In    of Region.t
 | Let   of Region.t

src/passes/1-parser/cameligo/LexToken.mll

@@ -79,6 +79,7 @@ type t =
 | End   of Region.t
 | False of Region.t
 | Fun   of Region.t
+| Rec   of Region.t
 | If    of Region.t
 | In    of Region.t
 | Let   of Region.t
@@ -154,6 +155,7 @@ let proj_token = function
 | End region -> region, "End"
 | False region -> region, "False"
 | Fun region -> region, "Fun"
+| Rec region -> region, "Rec"
 | If region -> region, "If"
 | In region -> region, "In"
 | Let region -> region, "Let"
@@ -213,6 +215,7 @@ let to_lexeme = function
 | End _   -> "end"
 | False _ -> "false"
 | Fun _   -> "fun"
+| Rec _   -> "rec"
 | If _    -> "if"
 | In _    -> "in"
 | Let _   -> "let"
@@ -250,6 +253,7 @@ let keywords = [
   (fun reg -> End   reg);
   (fun reg -> False reg);
   (fun reg -> Fun   reg);
+  (fun reg -> Rec   reg);
   (fun reg -> If    reg);
   (fun reg -> In    reg);
   (fun reg -> Let   reg);
@@ -291,7 +295,6 @@ let reserved =
     |> add "object"
     |> add "open"
     |> add "private"
-    |> add "rec"
     |> add "sig"
     |> add "struct"
     |> add "to"
@@ -499,6 +502,7 @@ let is_kwd = function
   | End _
   | False _
   | Fun _
+  | Rec _
   | If _
   | In _
   | Let _

src/passes/1-parser/cameligo/ParToken.mly

@@ -59,6 +59,7 @@
 %token <Region.t> End   "end"
 %token <Region.t> False "false"
 %token <Region.t> Fun   "fun"
+%token <Region.t> Rec   "rec"
 %token <Region.t> If    "if"
 %token <Region.t> In    "in"
 %token <Region.t> Let   "let"

src/passes/1-parser/cameligo/Parser.mly

@@ -203,14 +203,15 @@ field_decl:
     and value  = {field_name=$1; colon=$2; field_type=$3}
     in {region; value} }
 
-(* Top-level non-recursive definitions *)
+(* Top-level definitions *)
 
 let_declaration:
-  "let" let_binding seq(Attr) {
+  "let" ioption("rec") let_binding seq(Attr) {
     let kwd_let    = $1 in
-    let attributes = $3 in
+    let kwd_rec    = $2 in
-    let binding    = $2 in
+    let attributes = $4 in
-    let value      = kwd_let, binding, attributes in
+    let binding    = $3 in
+    let value      = kwd_let, kwd_rec, binding, attributes in
     let stop       = expr_to_region binding.let_rhs in
     let region     = cover $1 stop
     in {region; value} }
@@ -453,15 +454,16 @@ case_clause(right_expr):
     {pattern=$1; arrow=$2; rhs=$3} }
 
 let_expr(right_expr):
-  "let" let_binding seq(Attr) "in" right_expr  {
+  "let" ioption("rec") let_binding seq(Attr) "in" right_expr  {
     let kwd_let    = $1
-    and binding    = $2
+    and kwd_rec    = $2
-    and attributes = $3
+    and binding    = $3
-    and kwd_in     = $4
+    and attributes = $4
-    and body       = $5 in
+    and kwd_in     = $5
+    and body       = $6 in
     let stop       = expr_to_region body in
     let region     = cover kwd_let stop
-    and value      = {kwd_let; binding; kwd_in; body; attributes}
+    and value      = {kwd_let; kwd_rec; binding; kwd_in; body; attributes}
     in ELetIn {region; value} }
 
 fun_expr(right_expr):

src/passes/1-parser/cameligo/ParserLog.ml

@@ -136,8 +136,9 @@ and print_attributes state attributes =
    ) attributes
 
 and print_statement state = function
-  Let {value=kwd_let, let_binding, attributes; _} ->
+  Let {value=kwd_let, kwd_rec, let_binding, attributes; _} ->
     print_token       state kwd_let "let";
+    print_token_opt   state kwd_rec "rec";
     print_let_binding state let_binding;
     print_attributes  state attributes
 | TypeDecl {value={kwd_type; name; eq; type_expr}; _} ->
@@ -544,8 +545,9 @@ and print_case_clause state {value; _} =
   print_expr    state rhs
 
 and print_let_in state {value; _} =
-  let {kwd_let; binding; kwd_in; body; attributes} = value in
+  let {kwd_let; kwd_rec; binding; kwd_in; body; attributes} = value in
   print_token       state kwd_let "let";
+  print_token_opt   state kwd_rec "rec";
   print_let_binding state binding;
   print_attributes  state attributes;
   print_token       state kwd_in "in";
@@ -616,9 +618,14 @@ let rec pp_ast state {decl; _} =
   List.iteri (List.length decls |> apply) decls
 
 and pp_declaration state = function
-  Let {value = (_, let_binding, attr); region} ->
+  Let {value = (_, kwd_rec, let_binding, attr); region} ->
     pp_loc_node    state "Let" region;
+    (match kwd_rec with
+    | None -> ()
+    | Some (_) -> pp_node (state#pad 0 0) "rec"
+    );
     pp_let_binding state let_binding attr;
+
 | TypeDecl {value; region} ->
     pp_loc_node  state "TypeDecl" region;
     pp_type_decl state value
@@ -854,14 +861,21 @@ and pp_fun_expr state node =
   in ()
 
 and pp_let_in state node =
-  let {binding; body; attributes; _} = node in
+  let {binding; body; attributes; kwd_rec; _} = node in
   let {binders; lhs_type; let_rhs; _} = binding in
   let fields = if lhs_type = None then 3 else 4 in
+  let fields = if kwd_rec = None then fields else fields+1 in
   let fields = if attributes = [] then fields else fields+1 in
+  let arity = 
+    match kwd_rec with
+      None -> 0
+    | Some (_) ->
+      let state = state#pad fields 0 in
+      pp_node state "rec"; 0 in
   let arity =
     let state = state#pad fields 0 in
     pp_node state "<binders>";
-    pp_binders state binders; 0 in
+    pp_binders state binders; arity in
   let arity =
     match lhs_type with
       None -> arity

src/passes/1-parser/pascaligo/AST.ml

@@ -37,6 +37,7 @@ type kwd_end        = Region.t
 type kwd_for        = Region.t
 type kwd_from       = Region.t
 type kwd_function   = Region.t
+type kwd_recursive  = Region.t
 type kwd_if         = Region.t
 type kwd_in         = Region.t
 type kwd_is         = Region.t
@@ -201,6 +202,7 @@ and type_tuple = (type_expr, comma) nsepseq par reg
 (* Function and procedure declarations *)
 
 and fun_expr = {
+  kwd_recursive: kwd_recursive option;
   kwd_function : kwd_function;
   param        : parameters;
   colon        : colon;
@@ -210,6 +212,7 @@ and fun_expr = {
 }
 
 and fun_decl = {
+  kwd_recursive: kwd_recursive option;
   kwd_function : kwd_function;
   fun_name     : variable;
   param        : parameters;

src/passes/1-parser/pascaligo/LexToken.mli

@@ -89,6 +89,7 @@ type t =
 | For        of Region.t  (* "for"        *)
 | From       of Region.t  (* "from"       *)
 | Function   of Region.t  (* "function"   *)
+| Recursive  of Region.t  (* "recursive"  *)
 | If         of Region.t  (* "if"         *)
 | In         of Region.t  (* "in"         *)
 | Is         of Region.t  (* "is"         *)

src/passes/1-parser/pascaligo/LexToken.mll

@@ -87,6 +87,7 @@ type t =
 | For        of Region.t  (* "for"        *)
 | From       of Region.t  (* "from"       *)
 | Function   of Region.t  (* "function"   *)
+| Recursive  of Region.t  (* "recursive"  *)
 | If         of Region.t  (* "if"         *)
 | In         of Region.t  (* "in"         *)
 | Is         of Region.t  (* "is"         *)
@@ -199,6 +200,7 @@ let proj_token = function
 | For        region -> region, "For"
 | From       region -> region, "From"
 | Function   region -> region, "Function"
+| Recursive  region -> region, "Recursive"
 | If         region -> region, "If"
 | In         region -> region, "In"
 | Is         region -> region, "Is"
@@ -289,6 +291,7 @@ let to_lexeme = function
 | For        _ -> "for"
 | From       _ -> "from"
 | Function   _ -> "function"
+| Recursive  _ -> "recursive"
 | If         _ -> "if"
 | In         _ -> "in"
 | Is         _ -> "is"
@@ -361,6 +364,7 @@ let keywords = [
   (fun reg -> Or         reg);
   (fun reg -> Patch      reg);
   (fun reg -> Record     reg);
+  (fun reg -> Recursive  reg);
   (fun reg -> Remove     reg);
   (fun reg -> Set        reg);
   (fun reg -> Skip       reg);

src/passes/1-parser/pascaligo/ParToken.mly

@@ -57,6 +57,7 @@
 %token <Region.t> False       "False"
 %token <Region.t> For         "for"
 %token <Region.t> Function    "function"
+%token <Region.t> Recursive   "recursive"
 %token <Region.t> From        "from"
 %token <Region.t> If          "if"
 %token <Region.t> In          "in"

src/passes/1-parser/pascaligo/Parser.mly

@@ -237,49 +237,52 @@ field_decl:
 
 
 fun_expr:
-  "function" parameters ":" type_expr "is" expr {
+  | ioption ("recursive") "function" parameters ":" type_expr "is" expr {
-    let stop   = expr_to_region $6 in
+    let stop   = expr_to_region $7 in
-    let region = cover $1 stop
+    let region = cover $2 stop
-    and value  = {kwd_function = $1;
+    and value  = {kwd_recursive= $1;
-                  param        = $2;
+                  kwd_function = $2;
-                  colon        = $3;
+                  param        = $3;
-                  ret_type     = $4;
+                  colon        = $4;
-                  kwd_is       = $5;
+                  ret_type     = $5;
-                  return       = $6}
+                  kwd_is       = $6;
+                  return       = $7}
     in {region; value} }
 
 (* Function declarations *)
 
 open_fun_decl:
-  "function" fun_name parameters ":" type_expr "is"
+  ioption ("recursive") "function" fun_name parameters ":" type_expr "is"
   block "with" expr {
-    Scoping.check_reserved_name $2;
+    Scoping.check_reserved_name $3;
-    let stop   = expr_to_region $9 in
+    let stop   = expr_to_region $10 in
-    let region = cover $1 stop
+    let region = cover $2 stop
-    and value  = {kwd_function = $1;
+    and value  = {kwd_recursive= $1;
-                  fun_name     = $2;
+                  kwd_function = $2;
-                  param        = $3;
+                  fun_name     = $3;
-                  colon        = $4;
+                  param        = $4;
-                  ret_type     = $5;
+                  colon        = $5;
-                  kwd_is       = $6;
+                  ret_type     = $6;
-                  block_with   = Some ($7, $8);
+                  kwd_is       = $7;
-                  return       = $9;
+                  block_with   = Some ($8, $9);
+                  return       = $10;
                   terminator   = None;
                   attributes   = None}
     in {region; value}
   }
-| "function" fun_name parameters ":" type_expr "is" expr {
+| ioption ("recursive") "function" fun_name parameters ":" type_expr "is" expr {
-    Scoping.check_reserved_name $2;
+    Scoping.check_reserved_name $3;
-    let stop   = expr_to_region $7 in
+    let stop   = expr_to_region $8 in
-    let region = cover $1 stop
+    let region = cover $2 stop
-    and value  = {kwd_function = $1;
+    and value  = {kwd_recursive= $1;
-                  fun_name     = $2;
+                  kwd_function = $2;
-                  param        = $3;
+                  fun_name     = $3;
-                  colon        = $4;
+                  param        = $4;
-                  ret_type     = $5;
+                  colon        = $5;
-                  kwd_is       = $6;
+                  ret_type     = $6;
+                  kwd_is       = $7;
                   block_with   = None;
-                  return       = $7;
+                  return       = $8;
                   terminator   = None;
                   attributes   = None}
     in {region; value} }

src/passes/1-parser/pascaligo/ParserLog.ml

@@ -218,8 +218,9 @@ and print_fun_decl state {value; _} =
   print_terminator state terminator;
 
 and print_fun_expr state {value; _} =
-  let {kwd_function; param; colon;
+  let {kwd_recursive; kwd_function; param; colon;
        ret_type; kwd_is; return} : fun_expr = value in
+  print_token_opt   state kwd_recursive "recursive";
   print_token       state kwd_function "function";
   print_parameters  state param;
   print_token       state colon ":";
@@ -608,8 +609,8 @@ and print_field_path_assign state {value; _} =
   print_nsepseq state "field_path" print_var field_path;
   print_token state equal "=";
   print_expr  state field_expr
-  
+
-and print_update_expr state {value; _} = 
+and print_update_expr state {value; _} =
   let {record; kwd_with; updates} = value in
   print_path state record;
   print_token state kwd_with "with";
@@ -858,20 +859,26 @@ and pp_declaration state = function
 and pp_attr_decl state = pp_ne_injection pp_string state
 
 and pp_fun_decl state decl =
-  let arity = 5 in
+  let arity, start =
+    match decl.kwd_recursive with
+      None -> 5,0
+    | Some _ ->
+       let state = state#pad 6 0 in
+       let () = pp_node state "recursive"
+       in 6,1 in
   let () =
-    let state = state#pad arity 0 in
+    let state = state#pad arity start in
     pp_ident state decl.fun_name in
   let () =
-    let state = state#pad arity 1 in
+    let state = state#pad arity (start + 1) in
     pp_node state "<parameters>";
     pp_parameters state decl.param in
   let () =
-    let state = state#pad arity 2 in
+    let state = state#pad arity (start + 2) in
     pp_node state "<return type>";
     pp_type_expr (state#pad 1 0) decl.ret_type in
   let () =
-    let state = state#pad arity 3 in
+    let state = state#pad arity (start + 3) in
     pp_node state "<body>";
     let statements =
       match decl.block_with with
@@ -879,7 +886,7 @@ and pp_fun_decl state decl =
       | None -> Instr (Skip Region.ghost), [] in
     pp_statements state statements in
   let () =
-    let state = state#pad arity 4 in
+    let state = state#pad arity (start + 4) in
     pp_node state "<return>";
     pp_expr (state#pad 1 0) decl.return
   in ()

src/passes/1-parser/reasonligo/LexToken.mli

@@ -95,6 +95,7 @@ type t =
 | False of Region.t
 | If of Region.t
 | Let of Region.t
+| Rec of Region.t
 | Switch of Region.t
 | Mod of Region.t
 | Or of Region.t

src/passes/1-parser/reasonligo/LexToken.mll

@@ -80,6 +80,7 @@ type t =
 | False of Region.t
 | If of Region.t
 | Let of Region.t
+| Rec of Region.t
 | Switch of Region.t
 | Mod of Region.t
 | Or of Region.t
@@ -146,6 +147,7 @@ let proj_token = function
 | False region -> region, "False"
 | If region -> region, "If"
 | Let region -> region, "Let"
+| Rec region -> region, "Rec"
 | Switch region -> region, "Switch"
 | Mod region -> region, "Mod"
 | NOT region -> region, "!"
@@ -197,6 +199,7 @@ let to_lexeme = function
 | False _ -> "false"
 | If _ -> "if"
 | Let _ -> "let"
+| Rec _ -> "rec"
 | Mod _ -> "mod"
 | NOT _ -> "!"
 | Or _ -> "or"
@@ -232,6 +235,7 @@ let keywords = [
   (fun reg -> False  reg);
   (fun reg -> If     reg);
   (fun reg -> Let    reg);
+  (fun reg -> Rec    reg);
   (fun reg -> Switch reg);
   (fun reg -> Mod    reg);
   (fun reg -> Or     reg);
@@ -273,7 +277,6 @@ let reserved =
     |> add "of"
     |> add "open"
     |> add "private"
-    |> add "rec"
     |> add "sig"
     |> add "struct"
     |> add "then"
@@ -478,6 +481,7 @@ let is_kwd = function
 | False _
 | If _
 | Let _
+| Rec _
 | Switch _
 | Mod _
 | Or _

src/passes/1-parser/reasonligo/ParToken.mly

@@ -59,6 +59,7 @@
 %token <Region.t> False  "false"
 %token <Region.t> If     "if"
 %token <Region.t> Let    "let"
+%token <Region.t> Rec    "rec"
 %token <Region.t> Switch "switch"
 %token <Region.t> Mod    "mod"
 %token <Region.t> Or     "or"

src/passes/1-parser/reasonligo/Parser.mly

@@ -261,14 +261,15 @@ field_decl:
     and value  = {field_name=$1; colon=$2; field_type=$3}
     in {region; value} }
 
-(* Top-level non-recursive definitions *)
+(* Top-level definitions *)
 
 let_declaration:
-  seq(Attr) "let" let_binding {
+  seq(Attr) "let" ioption("rec") let_binding {
     let attributes = $1 in
     let kwd_let    = $2 in
-    let binding    = $3 in
+    let kwd_rec    = $3 in
-    let value      = kwd_let, binding, attributes in
+    let binding    = $4 in
+    let value      = kwd_let, kwd_rec, binding, attributes in
     let stop       = expr_to_region binding.let_rhs in
     let region     = cover $2 stop
     in {region; value} }
@@ -650,15 +651,16 @@ case_clause(right_expr):
     in {region; value} }
 
 let_expr(right_expr):
-  seq(Attr) "let" let_binding ";" right_expr {
+  seq(Attr) "let" ioption("rec") let_binding ";" right_expr {
     let attributes = $1 in
     let kwd_let = $2 in
-    let binding = $3 in
+    let kwd_rec = $3 in
-    let kwd_in  = $4 in
+    let binding = $4 in
-    let body    = $5 in
+    let kwd_in  = $5 in
-    let stop    = expr_to_region $5 in
+    let body    = $6 in
+    let stop    = expr_to_region $6 in
     let region  = cover $2 stop
-    and value   = {kwd_let; binding; kwd_in; body; attributes}
+    and value   = {kwd_let; kwd_rec; binding; kwd_in; body; attributes}
     in ELetIn {region; value} }
 
 disj_expr_level:

src/passes/2-simplify/cameligo.ml

@@ -70,6 +70,17 @@ module Errors = struct
        fun () -> Format.asprintf "%a" Location.pp_lift @@ param_loc)]
     in error ~data title message
 
+  let untyped_recursive_function var =
+    let title () = "" in
+    let message () =
+      Format.asprintf "\nUntyped recursive functions \
+                       are not supported yet.\n" in
+    let param_loc = var.Region.region in
+    let data = [
+      ("location",
+       fun () -> Format.asprintf "%a" Location.pp_lift @@ param_loc)]
+    in error ~data title message
+
   let unsupported_tuple_pattern p =
     let title () = "" in
     let message () =
@@ -334,7 +345,7 @@ let rec simpl_expression :
   trace (simplifying_expr t) @@
   match t with
     Raw.ELetIn e ->
-      let Raw.{binding; body; attributes; _} = e.value in
+      let Raw.{kwd_rec; binding; body; attributes; _} = e.value in
       let inline = List.exists (fun (a: Raw.attribute) -> a.value = "inline") attributes in
       let Raw.{binders; lhs_type; let_rhs; _} = binding in
       begin match binders with
@@ -382,10 +393,50 @@ let rec simpl_expression :
           (chain_let_in tl body)
         | [] -> body (* Precluded by corner case assertion above *)
       in
-      if List.length prep_vars = 1
+      let%bind ty_opt = match ty_opt with 
-      then ok (chain_let_in prep_vars body)
+      | None -> (match let_rhs with 
-      (* Bind the right hand side so we only evaluate it once *)
+        | EFun {value={binders;lhs_type}} -> 
-      else ok (e_let_in (rhs_b, ty_opt) false inline rhs' (chain_let_in prep_vars body))
+          let f_args = nseq_to_list (binders) in
+          let%bind lhs_type' = bind_map_option (fun x -> simpl_type_expression (snd x)) lhs_type in
+          let%bind ty = bind_map_list typed_pattern_to_typed_vars f_args in
+          let aux acc ty = Option.map (t_function (snd ty)) acc in
+          ok @@ (List.fold_right' aux lhs_type' ty)
+        | _ -> ok None
+        )
+      | Some t -> ok @@ Some t
+      in
+      let%bind ret_expr = if List.length prep_vars = 1
+        then ok (chain_let_in prep_vars body)
+        (* Bind the right hand side so we only evaluate it once *)
+        else ok (e_let_in (rhs_b, ty_opt) false inline rhs' (chain_let_in prep_vars body))
+      in
+      let%bind ret_expr = match kwd_rec with 
+        | None -> ok @@ ret_expr
+        | Some _ -> 
+          match ret_expr.expression_content with 
+            | E_let_in li -> (
+              let%bind lambda = 
+                let rec aux rhs = match rhs.expression_content with
+                  | E_lambda l -> ok @@ l
+                  | E_ascription a -> aux a.anno_expr
+                  | _ -> fail @@ corner_case "recursive only supported for lambda"
+                in
+                aux rhs'
+              in
+              let fun_name = fst @@ List.hd prep_vars in
+              let%bind fun_type = match ty_opt with 
+                | Some t -> ok @@ t
+                | None -> match rhs'.expression_content with 
+                      | E_ascription a -> ok a.type_annotation
+                      | _ -> fail @@ untyped_recursive_function e
+              in
+              let expression_content = E_recursive {fun_name;fun_type;lambda} in
+              let expression_content = E_let_in {li with rhs = {li.rhs with  expression_content}} in
+              ok @@ {ret_expr with expression_content}
+          )
+          | _ -> fail @@ corner_case "impossible"
+      in
+      ok ret_expr
 
       (* let f p1 ps... = rhs in body *)
       | (f, p1 :: ps) ->
@@ -630,6 +681,7 @@ and simpl_fun lamb' : expr result =
             in
             let let_in: Raw.let_in =
               {kwd_let= Region.ghost;
+               kwd_rec= None;
                binding= let_in_binding;
                kwd_in= Region.ghost;
                body= lamb.body;
@@ -658,7 +710,8 @@ and simpl_fun lamb' : expr result =
       e_lambda ~loc (binder) (Some input_type) output_type (layer_arguments tl)
     | [] -> body
   in
-  return @@ layer_arguments params'
+  let ret_lamb = layer_arguments params' in
+  return @@ ret_lamb
 
 
 and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
@@ -738,12 +791,11 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap list result
       let%bind type_expression = simpl_type_expression type_expr in
       ok @@ [loc x @@ Declaration_type (Var.of_name name.value , type_expression)]
   | Let x -> (
-      let (_, let_binding, attributes), _ = r_split x in
+      let (_, recursive, let_binding, attributes), _ = r_split x in
       let inline = List.exists (fun (a: Raw.attribute) -> a.value = "inline") attributes in
       let binding = let_binding in
       let {binders; lhs_type; let_rhs} = binding in
-      let%bind (hd, _) =
+      let (hd, _) = binders in
-        let (hd, tl) = binders in ok (hd, tl) in
         match hd with
         | PTuple pt ->
           let process_variable (var_pair: pattern * Raw.expr) :
@@ -795,11 +847,11 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap list result
           in ok @@ decls
         | PPar {region = _ ; value = { lpar = _ ; inside = pt; rpar = _; } } ->
           (* Extract parenthetical multi-bind *)
-          let (wild, _, attributes) = fst @@ r_split x in
+          let (wild, recursive, _, attributes) = fst @@ r_split x in
           simpl_declaration
             (Let {
                 region = x.region;
-                value = (wild, {binders = (pt, []);
+                value = (wild, recursive, {binders = (pt, []);
                                 lhs_type = lhs_type;
                                 eq = Region.ghost ;
                                 let_rhs = let_rhs}, attributes)}
@@ -840,6 +892,18 @@ and simpl_declaration : Raw.declaration -> declaration Location.wrap list result
         )
       | Some t -> ok @@ Some t
       in
+      let binder = Var.of_name var.value in
+      let%bind rhs' = match recursive with 
+        None -> ok @@ rhs' 
+        | Some _ -> match rhs'.expression_content with 
+          E_lambda lambda ->
+            (match lhs_type with 
+              None -> fail @@ untyped_recursive_function var 
+              | Some (lhs_type) -> 
+              let expression_content = E_recursive {fun_name=binder;fun_type=lhs_type;lambda} in
+              ok @@ {rhs' with expression_content})
+          | _ -> ok @@ rhs'
+      in
       ok @@ [loc x @@ (Declaration_constant (Var.of_name var.value , lhs_type , inline, rhs'))]
     )
 

src/passes/2-simplify/pascaligo.ml

@@ -659,7 +659,7 @@ and simpl_fun_decl :
       ((expression_variable * type_expression option) * expression) result =
   fun ~loc x ->
   let open! Raw in
-  let {fun_name; param; ret_type; block_with;
+  let {kwd_recursive;fun_name; param; ret_type; block_with;
        return; attributes} : fun_decl = x in
   let inline =
     match attributes with
@@ -683,11 +683,17 @@ and simpl_fun_decl :
        let%bind result =
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
-       let expression : expression = e_lambda ~loc (Var.of_name binder) (Some input_type)
+      let binder = Var.of_name binder in
-           (Some output_type) result in
+      let fun_name = Var.of_name fun_name.value in
-       let type_annotation =
+      let fun_type = t_function input_type output_type in
-         Some (make_t @@ T_arrow {type1=input_type;type2=output_type}) in
+      let expression : expression = 
-       ok ((Var.of_name fun_name.value, type_annotation), expression)
+        e_lambda ~loc binder (Some input_type)(Some output_type) result in
+      let%bind expression = match kwd_recursive with
+        None -> ok @@ expression |
+        Some _ -> ok @@ e_recursive ~loc fun_name fun_type 
+        @@ {binder;input_type=Some input_type; output_type= Some output_type; result}
+      in
+       ok ((fun_name, Some fun_type), expression)
      )
    | lst -> (
        let lst = npseq_to_list lst in
@@ -713,10 +719,16 @@ and simpl_fun_decl :
        let%bind result =
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
-       let expression =
+      let fun_name = Var.of_name fun_name.value in
-         e_lambda ~loc binder (Some (input_type)) (Some output_type) result in
+      let fun_type = t_function input_type output_type in
-       let type_annotation = Some (make_t @@ T_arrow {type1=input_type; type2=output_type}) in
+      let expression : expression = 
-       ok ((Var.of_name fun_name.value, type_annotation), expression)
+        e_lambda ~loc binder (Some input_type)(Some output_type) result in
+      let%bind expression = match kwd_recursive with
+        None -> ok @@ expression |
+        Some _ -> ok @@ e_recursive ~loc fun_name fun_type 
+        @@ {binder;input_type=Some input_type; output_type= Some output_type; result}
+      in
+       ok ((fun_name, Some fun_type), expression)
      )
   )
 
@@ -724,24 +736,28 @@ and simpl_fun_expression :
   loc:_ -> Raw.fun_expr -> (type_expression option * expression) result =
   fun ~loc x ->
   let open! Raw in
-  let {param;ret_type;return;_} : fun_expr = x in
+  let {kwd_recursive;param;ret_type;return} : fun_expr = x in
   let statements = [] in
   (match param.value.inside with
-     a, [] -> (
+    a, [] -> (
-       let%bind input = simpl_param a in
+        let%bind input = simpl_param a in
-       let (binder , input_type) = input in
+        let (binder , input_type) = input in
-       let%bind instructions = simpl_statement_list statements in
+        let%bind instructions = simpl_statement_list statements in
-       let%bind result = simpl_expression return in
+        let%bind result = simpl_expression return in
-       let%bind output_type = simpl_type_expression ret_type in
+        let%bind output_type = simpl_type_expression ret_type in
-       let body = instructions in
+        let body = instructions in
-       let%bind result =
+        let%bind result =
-         let aux prec cur = cur (Some prec) in
+          let aux prec cur = cur (Some prec) in
-         bind_fold_right_list aux result body in
+          bind_fold_right_list aux result body in
-       let expression : expression = e_lambda ~loc (Var.of_name binder) (Some input_type)
+        let binder = Var.of_name binder in
-           (Some output_type) result in
+        let fun_type = t_function input_type output_type in
-       let type_annotation = Some (make_t @@ T_arrow {type1=input_type;type2=output_type}) in
+        let expression = match kwd_recursive with
-       ok (type_annotation , expression)
+          | None -> e_lambda ~loc binder (Some input_type)(Some output_type) result
-     )
+          | Some _ -> e_recursive ~loc binder fun_type 
+          @@ {binder;input_type=Some input_type; output_type= Some output_type; result}
+        in
+        ok (Some fun_type , expression)
+      )
    | lst -> (
        let lst = npseq_to_list lst in
        (* TODO wrong, should be fresh? *)
@@ -765,10 +781,13 @@ and simpl_fun_expression :
        let%bind result =
          let aux prec cur = cur (Some prec) in
          bind_fold_right_list aux result body in
-       let expression =
+      let fun_type = t_function input_type output_type in
-         e_lambda ~loc binder (Some (input_type)) (Some output_type) result in
+      let expression = match kwd_recursive with
-       let type_annotation = Some (make_t @@ T_arrow {type1=input_type;type2=output_type}) in
+        | None -> e_lambda ~loc binder (Some input_type)(Some output_type) result
-       ok (type_annotation , expression)
+        | Some _ -> e_recursive ~loc binder fun_type 
+        @@ {binder;input_type=Some input_type; output_type= Some output_type; result}
+      in
+      ok (Some fun_type , expression)
      )
   )
 
@@ -1202,8 +1221,8 @@ and simpl_while_loop : Raw.while_loop -> (_ -> expression result) result = fun w
   in
   let init_rec = e_tuple [store_mutable_variable @@ captured_name_list] in
   let restore = fun expr -> List.fold_right aux captured_name_list expr in
-  let continue_expr = e_constant C_CONTINUE [for_body] in
+  let continue_expr = e_constant C_FOLD_CONTINUE [for_body] in
-  let stop_expr = e_constant C_STOP [e_variable binder] in
+  let stop_expr = e_constant C_FOLD_STOP [e_variable binder] in
   let aux_func = 
     e_lambda binder None None @@ 
     restore @@
@@ -1229,11 +1248,12 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi ->
   let%bind bound = simpl_expression fi.bound in
   let cond = e_annotation (e_constant C_LE [var ; bound]) t_bool in
   let step = e_int 1 in
+  let continue_expr = e_constant C_FOLD_CONTINUE [(e_variable binder)] in
   let ctrl = 
-    e_let_in (it,Some t_int) false false (e_constant C_ADD [ var ; step ]) 
+    e_let_in (it,Some t_int) false false (e_constant C_ADD [ var ; step ]) @@
-    (e_let_in (binder, None) false false (e_update (e_variable binder) "1" var)
+    e_let_in (binder, None) false false (e_update (e_variable binder) "1" var)@@
-    (e_variable binder))
+    continue_expr
-    in
+  in
   (* Modify the body loop*)
   let%bind for_body = simpl_block fi.block.value in
   let%bind for_body = for_body @@ Some ctrl in
@@ -1247,11 +1267,10 @@ and simpl_for_int : Raw.for_int -> (_ -> expression result) result = fun fi ->
   let restore = fun expr -> List.fold_right aux captured_name_list expr in
 
   (*Prep the lambda for the fold*)
-  let continue_expr = e_constant C_CONTINUE [restore(for_body)] in
+  let stop_expr = e_constant C_FOLD_STOP [e_variable binder] in
-  let stop_expr = e_constant C_STOP [e_variable binder] in
   let aux_func = e_lambda binder None None @@ 
                  e_let_in (it,Some t_int) false false (e_accessor (e_variable binder) "1") @@
-                 e_cond cond continue_expr (stop_expr) in
+                 e_cond cond (restore for_body) (stop_expr) in
 
   (* Make the fold_while en precharge the vakye *)
   let loop = e_constant C_FOLD_WHILE [aux_func; e_variable env_rec] in

src/passes/3-self_ast_simplified/helpers.ml

@@ -56,6 +56,9 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
       let%bind res = self res let_result in
       ok res
     )
+  | E_recursive { lambda={result=e;_}; _} ->
+      let%bind res = self init' e in
+      ok res
 
 and fold_cases : 'a folder -> 'a -> matching_expr -> 'a result = fun f init m ->
   match m with
@@ -156,6 +159,10 @@ let rec map_expression : exp_mapper -> expression -> expression result = fun f e
       let%bind result = self result in
       return @@ E_lambda { binder ; input_type ; output_type ; result }
     )
+  | E_recursive { fun_name; fun_type; lambda} ->
+      let%bind result = self lambda.result in
+      let lambda = {lambda with result} in
+      return @@ E_recursive { fun_name; fun_type; lambda}
   | E_constant c -> (
       let%bind args = bind_map_list self c.arguments in
       return @@ E_constant {c with arguments=args}
@@ -295,6 +302,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
       let%bind (res,result) = self init' result in
       ok ( res, return @@ E_lambda { binder ; input_type ; output_type ; result })
     )
+  | E_recursive { fun_name; fun_type; lambda} ->
+      let%bind (res, result) = self init' lambda.result in
+      let lambda = {lambda with result} in
+      ok ( res, return @@ E_recursive { fun_name; fun_type; lambda})
   | E_constant c -> (
       let%bind (res,args) = bind_fold_map_list self init' c.arguments in
       ok (res, return @@ E_constant {c with arguments=args})

src/passes/4-typer-new/solver.ml

@@ -291,6 +291,14 @@ module Wrap = struct
         C_equation (result' , P_variable whole_expr)
       ] @ rhs_tv_opt', whole_expr
 
+  let recursive : T.type_expression -> (constraints * T.type_variable) =
+    fun fun_type ->
+      let fun_type = type_expression_to_type_value fun_type in
+      let whole_expr = Core.fresh_type_variable () in
+      O.[
+        C_equation (fun_type, P_variable whole_expr)
+        ], whole_expr
+
   let assign : T.type_expression -> T.type_expression -> (constraints * T.type_variable) =
     fun v e ->
       let v' = type_expression_to_type_value v in

src/passes/4-typer-new/typer.ml

@@ -797,26 +797,16 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
   (* | _ -> ( … ) *)
 
 
-  | E_lambda {
+  | E_lambda lambda -> 
-      binder ;
+    let%bind (lambda,state',wrapped) = type_lambda e state lambda in
-      input_type ;
+    return_wrapped (E_lambda lambda) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
-      output_type ;
-      result ;
-    } -> (
-      let%bind input_type' = bind_map_option (evaluate_type e) input_type in
-      let%bind output_type' = bind_map_option (evaluate_type e) output_type in
-
-      let fresh : O.type_expression = t_variable (Wrap.fresh_binder ()) () in
-      let binder = fst binder in 
-      let e' = Environment.add_ez_binder (binder) fresh e in
-
-      let%bind (result , state') = type_expression e' state result in
-      let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
-      let wrapped = Wrap.lambda fresh input_type' output_type' in
-      return_wrapped
-        (E_lambda {binder = binder; result}) (* TODO: is the type of the entire lambda enough to access the input_type=fresh; ? *)
         state' wrapped
-    )
+  | E_recursive {fun_name;fun_type;lambda} ->
+    let%bind fun_type = evaluate_type e fun_type in
+    let e = Environment.add_ez_binder fun_name fun_type e in
+    let%bind (lambda,state,_) = type_lambda e state lambda in
+    let wrapped = Wrap.recursive fun_type in
+    return_wrapped (E_recursive {fun_name;fun_type;lambda}) state wrapped
 
   | E_constant {cons_name=name; arguments=lst} ->
     let () = ignore (name , lst) in
@@ -838,7 +828,22 @@ and type_expression : environment -> Solver.state -> ?tv_opt:O.type_expression -
         type_constant name tv_lst tv_opt ae.location in
       return (E_constant (name' , lst')) tv
     *)
+and type_lambda e state {
+      binder ;
+      input_type ;
+      output_type ;
+      result ;
+    } =
+      let%bind input_type' = bind_map_option (evaluate_type e) input_type in
+      let%bind output_type' = bind_map_option (evaluate_type e) output_type in
 
+      let fresh : O.type_expression = t_variable (Solver.Wrap.fresh_binder ()) () in
+      let e' = Environment.add_ez_binder (binder) fresh e in
+
+      let%bind (result , state') = type_expression e' state result in
+      let () = Printf.printf "this does not make use of the typed body, this code sounds buggy." in
+      let wrapped = Solver.Wrap.lambda fresh input_type' output_type' in
+      ok (({binder;result}:O.lambda),state',wrapped)
 (* Advanced *)
 
 and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
@@ -1040,12 +1045,10 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
       let%bind f' = untype_expression expr1 in
       let%bind arg' = untype_expression expr2 in
       return (e_application f' arg')
-  | E_lambda {binder; result} -> (
+  | E_lambda lambda ->
-      let%bind io = get_t_function e.type_expression in
+      let%bind lambda = untype_lambda e.type_expression lambda in
-      let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
+      let {binder;input_type;output_type;result} = lambda in
-      let%bind result = untype_expression result in
+      return (e_lambda (binder) (input_type) (output_type) result)
-      return (e_lambda (binder) (Some input_type) (Some output_type) result)
-    )
   | E_constructor {constructor; element} ->
       let%bind p' = untype_expression element in
       let Constructor n = constructor in
@@ -1092,6 +1095,16 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
     let%bind rhs = untype_expression rhs in
     let%bind result = untype_expression let_result in
     return (e_let_in (let_binder , (Some tv)) false inline rhs result)
+  | E_recursive {fun_name; fun_type; lambda} ->
+      let%bind lambda = untype_lambda fun_type lambda in
+      let%bind fun_type = untype_type_expression fun_type in
+      return @@ e_recursive fun_name fun_type lambda
+
+and untype_lambda ty {binder; result} : I.lambda result =
+      let%bind io = get_t_function ty in
+      let%bind (input_type , output_type) = bind_map_pair untype_type_value io in
+      let%bind result = untype_expression result in
+      ok ({binder;input_type = Some input_type; output_type = Some output_type; result}: I.lambda)
 
 (*
   Tranform a Ast_typed matching into an ast_simplified matching

src/passes/4-typer-old/typer.ml

@@ -613,45 +613,12 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
         ok (t_big_map key_type value_type ())
       in
       return (E_big_map lst') tv
-  | E_lambda {
+  | E_lambda lambda -> 
-      binder ;
+   let%bind (lambda, lambda_type) = type_lambda e lambda in
-      input_type ;
+   return (E_lambda lambda ) lambda_type
-      output_type ;
-      result ;
-    } -> (
-      let%bind input_type =
-        let%bind input_type =
-          (* Hack to take care of let_in introduced by `simplify/cameligo.ml` in ECase's hack *)
-          let default_action e () = fail @@ (needs_annotation e "the returned value") in
-          match input_type with
-          | Some ty -> ok ty
-          | None -> (
-              match result.expression_content with
-              | I.E_let_in li -> (
-                  match li.rhs.expression_content with
-                  | I.E_variable name when name = (fst binder) -> (
-                      match snd li.let_binder with
-                      | Some ty -> ok ty
-                      | None -> default_action li.rhs ()
-                    )
-                  | _ -> default_action li.rhs ()
-                )
-              | _ -> default_action result ()
-            )
-        in
-        evaluate_type e input_type in
-      let%bind output_type =
-        bind_map_option (evaluate_type e) output_type
-      in
-      let binder = fst binder in
-      let e' = Environment.add_ez_binder binder input_type e in
-      let%bind body = type_expression' ?tv_opt:output_type e' result in
-      let output_type = body.type_expression in
-      return (E_lambda {binder; result=body}) (t_function input_type output_type ())
-    )
   | E_constant {cons_name=( C_LIST_FOLD | C_MAP_FOLD | C_SET_FOLD) as opname ;
                 arguments=[
-                    ( { expression_content = (I.E_lambda { binder = (lname, None) ;
+                    ( { expression_content = (I.E_lambda { binder = lname ;
                                                    input_type = None ; 
                                                    output_type = None ; 
                                                    result }) ;
@@ -683,7 +650,7 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       return (E_constant {cons_name=opname';arguments=lst'}) tv
   | E_constant {cons_name=C_FOLD_WHILE as opname;
                 arguments = [
-                    ( { expression_content = (I.E_lambda { binder = (lname, None) ;
+                    ( { expression_content = (I.E_lambda { binder = lname ;
                                                    input_type = None ; 
                                                    output_type = None ; 
                                                    result }) ;
@@ -773,6 +740,11 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
     let e' = Environment.add_ez_declaration (let_binder) rhs e in
     let%bind let_result = type_expression' e' let_result in
     return (E_let_in {let_binder; rhs; let_result; inline}) let_result.type_expression
+  | E_recursive {fun_name; fun_type; lambda} ->
+    let%bind fun_type = evaluate_type e fun_type in
+    let e' = Environment.add_ez_binder fun_name fun_type e in
+    let%bind (lambda,_) = type_lambda e' lambda in
+    return (E_recursive {fun_name;fun_type;lambda}) fun_type
   | E_ascription {anno_expr; type_annotation} ->
     let%bind tv = evaluate_type e type_annotation in
     let%bind expr' = type_expression' ~tv_opt:tv e anno_expr in
@@ -788,6 +760,42 @@ and type_expression' : environment -> ?tv_opt:O.type_expression -> I.expression
       | Some tv' -> O.assert_type_expression_eq (tv' , type_annotation) in
     ok {expr' with type_expression=type_annotation}
 
+and type_lambda e {
+      binder ;
+      input_type ;
+      output_type ;
+      result ;
+    } = 
+      let%bind input_type =
+        let%bind input_type =
+          (* Hack to take care of let_in introduced by `simplify/cameligo.ml` in ECase's hack *)
+          let default_action e () = fail @@ (needs_annotation e "the returned value") in
+          match input_type with
+          | Some ty -> ok ty
+          | None -> (
+              match result.expression_content with
+              | I.E_let_in li -> (
+                  match li.rhs.expression_content with
+                  | I.E_variable name when name = (binder) -> (
+                      match snd li.let_binder with
+                      | Some ty -> ok ty
+                      | None -> default_action li.rhs ()
+                    )
+                  | _ -> default_action li.rhs ()
+                )
+              | _ -> default_action result ()
+            )
+        in
+        evaluate_type e input_type in
+      let%bind output_type =
+        bind_map_option (evaluate_type e) output_type
+      in
+      let e' = Environment.add_ez_binder binder input_type e in
+      let%bind body = type_expression' ?tv_opt:output_type e' result in
+      let output_type = body.type_expression in
+      ok (({binder; result=body}:O.lambda),(t_function input_type output_type ()))
+
+
 
 and type_constant (name:I.constant') (lst:O.type_expression list) (tv_opt:O.type_expression option) : (O.constant' * O.type_expression) result =
   let%bind typer = Operators.Typer.constant_typers name in
@@ -820,9 +828,11 @@ let untype_literal (l:O.literal) : I.literal result =
   | Literal_operation s -> ok (Literal_operation s)
 
 let rec untype_expression (e:O.expression) : (I.expression) result =
+  untype_expression_content e.type_expression e.expression_content
+  and untype_expression_content ty (ec:O.expression_content) : (I.expression) result =
   let open I in
   let return e = ok e in
-  match e.expression_content with
+  match ec with
   | E_literal l ->
       let%bind l = untype_literal l in
       return (e_literal l)
@@ -836,7 +846,7 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
       let%bind arg' = untype_expression expr2 in
       return (e_application f' arg')
   | E_lambda {binder ; result} -> (
-      let%bind io = get_t_function e.type_expression in
+      let%bind io = get_t_function ty in
       let%bind (input_type , output_type) = bind_map_pair untype_type_expression io in
       let%bind result = untype_expression result in
       return (e_lambda (binder) (Some input_type) (Some output_type) result)
@@ -883,7 +893,12 @@ let rec untype_expression (e:O.expression) : (I.expression) result =
       let%bind tv = untype_type_expression rhs.type_expression in
       let%bind rhs = untype_expression rhs in
       let%bind result = untype_expression let_result in
-      return (I.e_let_in (let_binder , (Some tv)) false inline rhs result)
+      return (e_let_in (let_binder , (Some tv)) false inline rhs result)
+  | E_recursive {fun_name;fun_type; lambda} ->
+      let%bind fun_type = untype_type_expression fun_type in
+      let%bind unty_expr= untype_expression_content ty @@ E_lambda lambda in
+      let lambda = match unty_expr.expression_content with I.E_lambda l -> l | _ -> failwith "impossible case" in
+      return @@ e_recursive fun_name fun_type lambda
 
 and untype_matching : (O.expression -> I.expression result) -> O.matching_expr -> I.matching_expr result = fun f m ->
   let open I in

src/passes/5-self_ast_typed/helpers.ml

@@ -25,6 +25,7 @@ let rec fold_expression : 'a folder -> 'a -> expression -> 'a result = fun f ini
       ok res
     )
   | E_lambda { binder = _ ; result = e }
+  | E_recursive {lambda= {result=e}}
   | E_constructor {element=e} -> (
       let%bind res = self init' e in
       ok res
@@ -148,6 +149,10 @@ let rec map_expression : mapper -> expression -> expression result = fun f e ->
       let%bind result = self result in
       return @@ E_lambda { binder ; result }
     )
+  | E_recursive { fun_name; fun_type; lambda = {binder;result}} -> (
+      let%bind result = self result in
+      return @@ E_recursive { fun_name; fun_type; lambda = {binder;result}}
+    )
   | E_constant c -> (
       let%bind args = bind_map_list self c.arguments in
       return @@ E_constant {c with arguments=args}
@@ -172,9 +177,9 @@ and map_cases : mapper -> matching_expr -> matching_expr result = fun f m ->
       let%bind some = map_expression f some in
       ok @@ Match_option { match_none ; match_some = (name , some, te) }
     )
-  | Match_tuple ((names , e), _) -> (
+  | Match_tuple ((names , e), te) -> (
       let%bind e' = map_expression f e in
-      ok @@ Match_tuple ((names , e'), [])
+      ok @@ Match_tuple ((names , e'), te)
     )
   | Match_variant (lst, te) -> (
       let aux ((a , b) , e) =
@@ -188,9 +193,9 @@ and map_cases : mapper -> matching_expr -> matching_expr result = fun f m ->
 and map_program : mapper -> program -> program result = fun m p ->
   let aux = fun (x : declaration) ->
     match x with
-    | Declaration_constant (v , e , i, env) -> (
+    | Declaration_constant (n , e , i, env) -> (
         let%bind e' = map_expression m e in
-        ok (Declaration_constant (v , e' , i, env))
+        ok (Declaration_constant (n , e' , i, env))
       )
   in
   bind_map_list (bind_map_location aux) p
@@ -260,6 +265,10 @@ let rec fold_map_expression : 'a fold_mapper -> 'a -> expression -> ('a * expres
       let%bind (res,result) = self init' result in
       ok ( res, return @@ E_lambda { binder ; result })
     )
+  | E_recursive { fun_name; fun_type; lambda={binder;result}} -> (
+      let%bind (res,result) = self init' result in
+      ok (res, return @@ E_recursive {fun_name; fun_type; lambda={binder;result}})
+    )
   | E_constant c -> (
       let%bind (res,args) = bind_fold_map_list self init' c.arguments in
       ok (res, return @@ E_constant {c with arguments=args})
@@ -283,9 +292,9 @@ and fold_map_cases : 'a fold_mapper -> 'a -> matching_expr -> ('a * matching_exp
       let%bind (init, some) = fold_map_expression f init some in
       ok @@ (init, Match_option { match_none ; match_some = (name , some, te) })
     )
-  | Match_tuple ((names , e), _) -> (
+  | Match_tuple ((names , e), te) -> (
       let%bind (init, e') = fold_map_expression f init e in
-      ok @@ (init, Match_tuple ((names , e'), []))
+      ok @@ (init, Match_tuple ((names , e'), te))
     )
   | Match_variant (lst, te) -> (
       let aux init ((a , b) , e) =

src/passes/5-self_ast_typed/self_ast_typed.ml

@@ -1,6 +1,8 @@
 open Trace
 
-let all_passes = []
+let all_passes = [
+  Tail_recursion.peephole_expression
+]
 
 let contract_passes = [
   Contract_passes.self_typing ;
@@ -22,3 +24,12 @@ let all_contract main_name prg =
     } in
   let all_p = List.map (fun pass -> Helpers.fold_map_program pass data) contract_passes in
   bind_chain_ignore_acc all_p prg
+let all = [
+  Tail_recursion.peephole_expression
+]
+
+let map_expression = Helpers.map_expression
+
+let fold_expression = Helpers.fold_expression
+
+let fold_map_expression = Helpers.fold_map_expression

src/passes/5-self_ast_typed/tail_recursion.ml

@@ -0,0 +1,108 @@
+open Ast_typed
+open Trace
+
+module Errors = struct
+  let recursive_call_is_only_allowed_as_the_last_operation name loc () =
+    let title = (thunk ("Recursion must be achieved through tail-calls only")) in
+    let message () = "" in
+    let data = [
+      ("function" , fun () -> Format.asprintf "%a" PP.expression_variable name);
+      ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
+    ] in
+    error ~data title message ()
+end
+open Errors
+
+let rec check_recursive_call : expression_variable -> bool -> expression -> unit result = fun n final_path e ->
+  match e.expression_content with
+  | E_literal _   -> ok ()
+  | E_constant c  ->
+    let%bind _ = bind_map_list (check_recursive_call n false) c.arguments in
+    ok ()
+  | E_variable v  -> (
+    let%bind _ = trace_strong (recursive_call_is_only_allowed_as_the_last_operation n e.location) @@
+    Assert.assert_true (final_path || n <> v) in
+    ok ()
+    )
+  | E_application {expr1;expr2} ->
+    let%bind _ = check_recursive_call n final_path expr1 in
+    let%bind _ = check_recursive_call n false expr2 in
+    ok ()
+  | E_lambda {result;_} ->
+    let%bind _ = check_recursive_call n final_path result in
+    ok ()
+  | E_recursive { fun_name; lambda} ->
+    let%bind _ = check_recursive_call fun_name true lambda.result in
+    ok ()
+  | E_let_in {rhs;let_result;_} ->
+    let%bind _ = check_recursive_call n false rhs in
+    let%bind _ = check_recursive_call n final_path let_result in
+    ok ()
+  | E_constructor {element;_} ->
+    let%bind _ = check_recursive_call n false element in
+    ok ()
+  | E_matching {matchee;cases} ->
+    let%bind _ = check_recursive_call n false matchee in
+    let%bind _ = check_recursive_call_in_matching n final_path cases in
+    ok ()
+  | E_record elm -> 
+    let es = LMap.to_list elm in
+    let%bind _ = bind_map_list (check_recursive_call n false) es in
+    ok ()
+  | E_record_accessor {expr;_} ->
+    let%bind _ = check_recursive_call n false expr in
+    ok ()
+  | E_record_update {record;update;_} ->
+    let%bind _ = check_recursive_call n false record in
+    let%bind _ = check_recursive_call n false update in
+    ok ()
+  | E_map eel | E_big_map eel->
+    let aux (e1,e2) = 
+      let%bind _ = check_recursive_call n false e1 in
+      let%bind _ = check_recursive_call n false e2 in
+      ok ()
+    in
+    let%bind _ = bind_map_list aux eel in
+    ok ()
+  | E_list el | E_set el ->
+    let%bind _ = bind_map_list (check_recursive_call n false) el in
+    ok ()
+  | E_look_up (e1,e2) ->
+    let%bind _ = check_recursive_call n false e1 in
+    let%bind _ = check_recursive_call n false e2 in
+    ok ()
+
+and check_recursive_call_in_matching = fun n final_path c ->
+  match c with
+  | Match_bool {match_true;match_false} ->
+    let%bind _ = check_recursive_call n final_path match_true in
+    let%bind _ = check_recursive_call n final_path match_false in
+    ok ()
+  | Match_list {match_nil;match_cons=(_,_,e,_)} ->
+    let%bind _ = check_recursive_call n final_path match_nil in
+    let%bind _ = check_recursive_call n final_path e in
+    ok ()
+  | Match_option {match_none; match_some=(_,e,_)} ->
+    let%bind _ = check_recursive_call n final_path match_none in
+    let%bind _ = check_recursive_call n final_path e in
+    ok ()
+  | Match_tuple ((_,e),_) ->
+    let%bind _ = check_recursive_call n final_path e in
+    ok ()
+  | Match_variant (l,_) ->
+    let aux (_,e) =
+      let%bind _ = check_recursive_call n final_path e in
+      ok ()
+    in
+    let%bind _ = bind_map_list aux l in
+    ok ()
+    
+
+let peephole_expression : expression -> expression result = fun e ->
+  let return expression_content = ok { e with expression_content } in
+  match e.expression_content with
+  | E_recursive {fun_name; lambda} as e-> (
+    let%bind _ = check_recursive_call fun_name true lambda.result in
+    return e
+    )
+  | e -> return e

src/passes/6-interpreter/interpreter.ml

@@ -80,8 +80,8 @@ let rec apply_operator : Ast_typed.constant' -> value list -> value result =
     | ( C_IS_NAT , [ V_Ct (C_int a')    ] ) ->
       if a' > 0 then return_some @@ V_Ct (C_nat a')
       else return_none ()
-    | ( C_CONTINUE  , [ v ] ) -> ok @@ v_pair (v_bool true  , v)
+    | ( C_FOLD_CONTINUE  , [ v ] ) -> ok @@ v_pair (v_bool true  , v)
-    | ( C_STOP      , [ v ] ) -> ok @@ v_pair (v_bool false , v)
+    | ( C_FOLD_STOP      , [ v ] ) -> ok @@ v_pair (v_bool false , v)
     | ( C_ASSERTION , [ v ] ) ->
       let%bind pass = is_true v in
       if pass then return_ct @@ C_unit
@@ -272,18 +272,23 @@ and eval : Ast_typed.expression -> env -> value result
     match term.expression_content with
     | E_application ({expr1 = f; expr2 = args}) -> (
       let%bind f' = eval f env in
+      let%bind args' = eval args env in
       match f' with
       | V_Func_val (arg_names, body, f_env) ->
-        let%bind args' = eval args env in
         let f_env' = Env.extend f_env (arg_names, args') in
         eval body f_env'
+      | V_Func_rec (fun_name, arg_names, body, f_env) ->
+        let f_env' = Env.extend f_env (arg_names, args') in
+        let f_env'' = Env.extend f_env' (fun_name, f') in
+        eval body f_env''
       | _ -> simple_fail "trying to apply on something that is not a function"
     )
-    | E_lambda { binder; result;} ->
+    | E_lambda {binder; result;} ->
       ok @@ V_Func_val (binder,result,env)
-    | E_let_in { let_binder; rhs; let_result; _} ->
+    | E_let_in {let_binder ; rhs; let_result} -> (
       let%bind rhs' = eval rhs env in
       eval let_result (Env.extend env (let_binder,rhs'))
+    )
     | E_map kvlist | E_big_map kvlist ->
       let%bind kvlist' = bind_map_list
         (fun kv -> bind_map_pair (fun (el:Ast_typed.expression) -> eval el env) kv)
@@ -371,6 +376,8 @@ and eval : Ast_typed.expression -> env -> value result
       | _ -> simple_fail "not yet supported case"
         (* ((ctor,name),body) *)
     )
+    | E_recursive {fun_name; fun_type=_; lambda} ->
+      ok @@ V_Func_rec (fun_name, lambda.binder, lambda.result, env)
     | E_look_up _ ->
       let serr = Format.asprintf "Unsupported construct :\n %a\n" Ast_typed.PP.expression term in
       simple_fail serr

src/passes/6-transpiler/transpiler.ml

@@ -101,6 +101,15 @@ them. please report this to the developers." in
       ("value" , fun () -> Format.asprintf "%a" Mini_c.PP.value value) ;
     ] in
     error ~data title content
+  
+  let unsupported_recursive_function expression_variable =
+    let title () = "unsupported recursive function yet" in
+    let content () = "only fuction with one variable are supported" in
+    let data = [
+      ("value" , fun () -> Format.asprintf "%a" AST.PP.expression_variable expression_variable) ;
+    ] in
+    error ~data title content
+
 
 end
 open Errors
@@ -379,6 +388,8 @@ and transpile_annotated_expression (ae:AST.expression) : expression result =
   | E_lambda l ->
     let%bind io = AST.get_t_function ae.type_expression in
     transpile_lambda l io
+  | E_recursive r ->
+    transpile_recursive r
   | E_list lst -> (
       let%bind t =
         trace_strong (corner_case ~loc:__LOC__ "not a list") @@
@@ -518,6 +529,125 @@ and transpile_lambda l (input_type , output_type) =
   let closure = E_closure { binder; body = result'} in
   ok @@ Combinators.Expression.make_tpl (closure , tv)
 
+and transpile_recursive {fun_name; fun_type; lambda} =
+  let rec map_lambda : AST.expression_variable -> type_value -> AST.expression -> (expression * expression_variable list) result = fun fun_name loop_type e ->
+    match e.expression_content with 
+      E_lambda {binder;result} -> 
+        let%bind (body,l) = map_lambda fun_name loop_type result in
+        ok @@ (Expression.make (E_closure {binder;body}) loop_type, binder::l)
+      | _  -> 
+        let%bind res = replace_callback fun_name loop_type false e in
+        ok @@ (res, [])
+
+  and replace_callback : AST.expression_variable -> type_value -> bool -> AST.expression -> expression result = fun fun_name loop_type shadowed e ->
+    match e.expression_content with
+      E_let_in li -> 
+        let shadowed = shadowed || Var.equal li.let_binder fun_name in 
+        let%bind let_result = replace_callback fun_name loop_type shadowed li.let_result in
+        let%bind rhs = transpile_annotated_expression li.rhs in
+        let%bind ty  = transpile_type e.type_expression in
+        ok @@ e_let_in li.let_binder ty li.inline rhs let_result |
+      E_matching m -> 
+        let%bind ty = transpile_type e.type_expression in
+        matching fun_name loop_type shadowed m ty |
+      E_application {expr1;expr2} -> (
+        match expr1.expression_content,shadowed with
+        E_variable name, false when Var.equal fun_name name -> 
+          let%bind expr = transpile_annotated_expression expr2 in
+          ok @@ Expression.make (E_constant {cons_name=C_LOOP_CONTINUE;arguments=[expr]}) loop_type |
+        _ -> 
+          let%bind expr = transpile_annotated_expression e in
+          ok @@ Expression.make (E_constant {cons_name=C_LOOP_STOP;arguments=[expr]}) loop_type
+      ) |
+      _ -> 
+        let%bind expr = transpile_annotated_expression e in
+        ok @@ Expression.make (E_constant {cons_name=C_LOOP_STOP;arguments=[expr]}) loop_type
+  and matching : AST.expression_variable -> type_value -> bool -> AST.matching -> type_value -> expression result = fun fun_name loop_type shadowed m ty ->
+    let return ret = ok @@ Expression.make ret @@ ty in
+    let%bind expr = transpile_annotated_expression m.matchee in
+    match m.cases with
+      Match_bool {match_true; match_false} -> 
+          let%bind (t , f) = bind_map_pair (replace_callback fun_name loop_type shadowed) (match_true, match_false) in
+          return @@ E_if_bool (expr, t, f)
+      | Match_option { match_none; match_some = (name, s, tv) } ->
+          let%bind n = replace_callback fun_name loop_type shadowed match_none in
+          let%bind (tv' , s') =
+            let%bind tv' = transpile_type tv in
+            let%bind s' = replace_callback fun_name loop_type shadowed s in
+            ok (tv' , s')
+          in
+          return @@ E_if_none (expr , n , ((name , tv') , s'))
+      | Match_list {
+          match_nil ;
+          match_cons = ((hd_name) , (tl_name), match_cons, ty) ;
+        } -> (
+          let%bind nil = replace_callback fun_name loop_type shadowed match_nil in
+          let%bind cons =
+            let%bind ty' = transpile_type ty in
+            let%bind match_cons' = replace_callback fun_name loop_type shadowed match_cons in
+            ok (((hd_name , ty') , (tl_name , ty')) , match_cons')
+          in
+          return @@ E_if_cons (expr , nil , cons)
+        )
+      | Match_variant (lst , variant) -> (
+          let%bind tree =
+            trace_strong (corner_case ~loc:__LOC__ "getting lr tree") @@
+            tree_of_sum variant in
+          let%bind tree' = match tree with
+            | Empty -> fail (corner_case ~loc:__LOC__ "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' = transpile_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 (None, snd a') (None, 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 (corner_case ~loc:__LOC__ "missing match clause") @@
+                  List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in
+                let%bind body' = replace_callback fun_name loop_type shadowed body in
+                return @@ E_let_in ((name , tv) , false , top , body')
+              )
+            | ((`Node (a , b)) , tv) ->
+                let%bind a' =
+                  let%bind a_ty = get_t_left tv in
+                  let left_var = Var.fresh ~name:"left" () in
+                  let%bind e = aux (((Expression.make (E_variable left_var) a_ty))) a in
+                  ok ((left_var , a_ty) , e)
+                in
+                let%bind b' =
+                  let%bind b_ty = get_t_right tv in
+                  let right_var = Var.fresh ~name:"right" () in
+                  let%bind e = aux (((Expression.make (E_variable right_var) b_ty))) b in
+                  ok ((right_var , b_ty) , e)
+                in
+                return @@ E_if_left (top , a' , b')
+          in
+          trace_strong (corner_case ~loc:__LOC__ "building constructor") @@
+          aux expr tree''
+       )
+      | AST.Match_tuple _ -> failwith "match_tuple not supported"
+  in
+  let%bind fun_type = transpile_type fun_type in
+  let%bind (input_type,output_type) = get_t_function fun_type in
+  let loop_type = t_union (None, input_type) (None, output_type) in
+  let%bind (body,binder) = map_lambda fun_name loop_type lambda.result in
+  let binder = lambda.binder::binder in
+  let%bind binder = match binder with hd::[] -> ok @@ hd | _ -> fail @@ unsupported_recursive_function fun_name in
+  let expr = Expression.make_tpl (E_variable binder, input_type) in
+  let body = Expression.make (E_iterator (C_LOOP_LEFT, ((lambda.binder, loop_type),body), expr)) output_type in
+  ok @@ Expression.make (E_closure {binder;body}) fun_type
+
 let transpile_declaration env (d:AST.declaration) : toplevel_statement result =
   match d with
   | Declaration_constant (name,expression, inline, _) ->

src/passes/8-compiler/compiler_program.ml

@@ -50,13 +50,22 @@ let rec get_operator : constant' -> type_value -> expression list -> predicate r
           let%bind ty' = Mini_c.get_t_option ty in
           let%bind m_ty = Compiler_type.type_ ty' in
           ok @@ simple_constant @@ prim ~children:[m_ty] I_NONE
-
         )
       | C_NIL -> (
           let%bind ty' = Mini_c.get_t_list ty in
           let%bind m_ty = Compiler_type.type_ ty' in
           ok @@ simple_unary @@ prim ~children:[m_ty] I_NIL
         )
+      | C_LOOP_CONTINUE -> (
+          let%bind (_,ty) = get_t_or ty in
+          let%bind m_ty = Compiler_type.type_ ty in
+          ok @@ simple_unary @@ prim ~children:[m_ty] I_LEFT
+      )
+      | C_LOOP_STOP -> (
+          let%bind (ty, _) = get_t_or ty in
+          let%bind m_ty = Compiler_type.type_ ty in
+          ok @@ simple_unary @@ prim ~children:[m_ty] I_RIGHT
+      )
       | C_SET_EMPTY -> (
           let%bind ty' = Mini_c.get_t_set ty in
           let%bind m_ty = Compiler_type.type_ ty' in
@@ -397,6 +406,16 @@ and translate_expression (expr:expression) (env:environment) : michelson result
             ]) in
           return code
         )
+      | C_LOOP_LEFT -> (
+          let%bind (_, ty) = get_t_or (snd v) in
+          let%bind m_ty = Compiler_type.type_ ty in
+          let%bind code = ok (seq [
+              expr' ;
+              prim ~children:[m_ty] I_LEFT;
+              i_loop_left body';
+            ]) in
+          return code
+        )
       | s -> (
           let iter = Format.asprintf "iter %a" PP.constant s in
           let error = error (thunk "bad iterator") (thunk iter) in

src/passes/operators/operators.ml

@@ -349,11 +349,11 @@ module Simplify = struct
 
     (* Loop module *)
 
-    | "Loop.fold_while" -> ok C_FOLD_WHILE
+    | "Loop.fold_while" -> ok C_FOLD_WHILE    (* Deprecated *)
-    | "Loop.resume"     -> ok C_CONTINUE
+    | "Loop.resume"     -> ok C_FOLD_CONTINUE
-    | "continue"        -> ok C_CONTINUE (* Deprecated *)
+    | "continue"        -> ok C_FOLD_CONTINUE (* Deprecated *)
-    | "Loop.stop"       -> ok C_STOP
+    | "Loop.stop"       -> ok C_FOLD_STOP
-    | "stop"            -> ok C_STOP     (* Deprecated *)
+    | "stop"            -> ok C_FOLD_STOP     (* Deprecated *)
 
     (* Others *)
 
@@ -515,8 +515,8 @@ module Typer = struct
       | C_FAILWITH            -> ok @@ t_failwith ;
       (* LOOPS *)
       | C_FOLD_WHILE          -> ok @@ t_fold_while ;
-      | C_CONTINUE            -> ok @@ t_continuation ;
+      | C_FOLD_CONTINUE       -> ok @@ t_continuation ;
-      | C_STOP                -> ok @@ t_continuation ;
+      | C_FOLD_STOP           -> ok @@ t_continuation ;
       (* MATH *)
       | C_NEG                 -> ok @@ t_neg ;
       | C_ABS                 -> ok @@ t_abs ;
@@ -1115,8 +1115,8 @@ module Typer = struct
     | C_FAILWITH            -> ok @@ failwith_ ;
     (* LOOPS *)
     | C_FOLD_WHILE          -> ok @@ fold_while ;
-    | C_CONTINUE            -> ok @@ continue ;
+    | C_FOLD_CONTINUE       -> ok @@ continue ;
-    | C_STOP                -> ok @@ stop ;
+    | C_FOLD_STOP           -> ok @@ stop ;
      (* MATH *)
     | C_NEG                 -> ok @@ neg ;
     | C_ABS                 -> ok @@ abs ;
@@ -1248,8 +1248,8 @@ module Compiler = struct
     | C_MAP_ADD         -> ok @@ simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE]
     | C_MAP_UPDATE      -> ok @@ simple_ternary @@ prim I_UPDATE
     | C_FOLD_WHILE      -> ok @@ simple_binary @@ seq [i_swap ; (i_push (prim T_bool) (prim D_True));prim ~children:[seq [dip i_dup; i_exec; i_unpair]] I_LOOP ;i_swap ; i_drop]
-    | C_CONTINUE        -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_True)); i_pair]
+    | C_FOLD_CONTINUE   -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_True)); i_pair]
-    | C_STOP            -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_False)); i_pair]
+    | C_FOLD_STOP       -> ok @@ simple_unary @@ seq [(i_push (prim T_bool) (prim D_False)); i_pair]
     | C_SIZE            -> ok @@ simple_unary @@ prim I_SIZE
     | C_FAILWITH        -> ok @@ simple_unary @@ prim I_FAILWITH
     | C_ASSERT_INFERRED -> ok @@ simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])

src/stages/ast_simplified/PP.ml

@@ -11,7 +11,9 @@ let expression_variable ppf (ev : expression_variable) : unit =
 
 
 let rec expression ppf (e : expression) =
-  match e.expression_content with
+  expression_content ppf e.expression_content
+and expression_content ppf (ec : expression_content) =
+  match ec with
   | E_literal l ->
       literal ppf l
   | E_variable n ->
@@ -40,16 +42,23 @@ let rec expression ppf (e : expression) =
   | E_look_up (ds, ind) ->
       fprintf ppf "(%a)[%a]" expression ds expression ind
   | E_lambda {binder; input_type; output_type; result} ->
-      fprintf ppf "lambda (%a:%a) : %a return %a" option_type_name binder
+      fprintf ppf "lambda (%a:%a) : %a return %a" 
+        expression_variable binder
         (PP_helpers.option type_expression)
         input_type
         (PP_helpers.option type_expression)
         output_type expression result
   | E_matching {matchee; cases; _} ->
-      fprintf ppf "match %a with %a" expression matchee (matching expression)
+      fprintf ppf "match %a with %a"
+        expression matchee (matching expression)
         cases
   | E_let_in { let_binder ; mut; rhs ; let_result; inline } ->    
-    fprintf ppf "let %a%a = %a%a in %a" option_mut mut option_type_name let_binder expression rhs option_inline inline expression let_result
+      fprintf ppf "let %a%a = %a%a in %a" option_mut mut option_type_name let_binder expression rhs option_inline inline expression let_result
+  | E_recursive { fun_name; fun_type; lambda} ->
+      fprintf ppf "rec (%a:%a => %a )" 
+        expression_variable fun_name 
+        type_expression fun_type
+        expression_content (E_lambda lambda)
   | E_skip ->
       fprintf ppf "skip"
   | E_ascription {anno_expr; type_annotation} ->

src/stages/ast_simplified/combinators.ml

@@ -178,11 +178,12 @@ let e_lambda ?loc (binder : expression_variable)
     (result : expression)
   : expression =
   location_wrap ?loc @@ E_lambda {
-    binder = (binder , input_type) ;
+    binder = binder;
     input_type = input_type ;
     output_type = output_type ;
     result ;
   }
+let e_recursive ?loc fun_name fun_type lambda = location_wrap ?loc @@ E_recursive {fun_name; fun_type; lambda}
 
 
 let e_assign_with_let ?loc var access_path expr = 

src/stages/ast_simplified/combinators.mli

@@ -106,6 +106,7 @@ val e_typed_big_map : ?loc:Location.t -> ( expression * expression ) list  -> ty
 val e_typed_set : ?loc:Location.t -> expression list -> type_expression -> expression
 
 val e_lambda : ?loc:Location.t -> expression_variable -> type_expression option -> type_expression option -> expression -> expression
+val e_recursive : ?loc:Location.t -> expression_variable -> type_expression -> lambda -> expression
 val e_record : ?loc:Location.t -> expr Map.String.t -> expression
 val e_update : ?loc:Location.t -> expression -> string -> expression -> expression
 val e_assign_with_let : ?loc:Location.t -> string -> string list -> expression -> ((expression_variable*type_expression option)*bool*expression*bool)

src/stages/ast_simplified/misc.ml

@@ -182,7 +182,7 @@ let rec assert_value_eq (a, b: (expression * expression )) : unit result =
   | (_a' , E_ascription b) -> assert_value_eq (a , b.anno_expr)
   | (E_variable _, _) | (E_lambda _, _)
   | (E_application _, _) | (E_let_in _, _)
-  | (E_record_accessor _, _)
+  | (E_recursive _,_) | (E_record_accessor _, _)
   | (E_look_up _, _) | (E_matching _, _)
   | (E_skip, _) -> simple_fail "comparing not a value"
 

src/stages/ast_simplified/types.ml

@@ -35,6 +35,7 @@ and expression_content =
   | E_application of application
   | E_lambda of lambda
   | E_let_in of let_in
+  | E_recursive of recursive
   | E_skip
   (* Variant *)
   | E_constructor of constructor (* For user defined constructors *)
@@ -60,7 +61,7 @@ and constant =
 and application = {expr1: expression; expr2: expression}
 
 and lambda =
-  { binder: expression_variable * type_expression option
+  { binder: expression_variable 
   ; input_type: type_expression option
   ; output_type: type_expression option
   ; result: expression }
@@ -72,6 +73,12 @@ and let_in =
   ; let_result: expression
   ; inline: bool }
 
+and recursive = {
+  fun_name :  expression_variable;
+  fun_type : type_expression;
+  lambda : lambda;
+}
+
 and constructor = {constructor: constructor'; element: expression}
 
 and accessor = {expr: expression; label: label}

src/stages/ast_typed/PP.ml

@@ -11,7 +11,10 @@ let expression_variable ppf (ev : expression_variable) : unit =
 
 
 let rec expression ppf (e : expression) =
-  match e.expression_content with
+  expression_content ppf e.expression_content
+
+and expression_content ppf (ec: expression_content) =
+  match ec with
   | E_literal l ->
       literal ppf l
   | E_variable n ->
@@ -47,6 +50,11 @@ let rec expression ppf (e : expression) =
   | E_let_in {let_binder; rhs; let_result; inline} ->
       fprintf ppf "let %a = %a%a in %a" expression_variable let_binder expression
         rhs option_inline inline expression let_result
+  | E_recursive { fun_name;fun_type; lambda} ->
+      fprintf ppf "rec (%a:%a => %a )" 
+        expression_variable fun_name 
+        type_expression fun_type
+        expression_content (E_lambda lambda)
 
 and assoc_expression ppf : expr * expr -> unit =
  fun (a, b) -> fprintf ppf "%a -> %a" expression a expression b

src/stages/ast_typed/combinators.ml

@@ -168,6 +168,17 @@ let get_t_function (t:type_expression) : (type_expression * type_expression) res
   | T_arrow {type1;type2} -> ok (type1,type2)
   | _ -> simple_fail "not a function"
 
+let get_t_function_full (t:type_expression) : (type_expression * type_expression) result =
+  let%bind _ = get_t_function t in
+  let rec aux n t = match t.type_content with 
+    | T_arrow {type1;type2} -> 
+      let (l, o) = aux (n+1) type2 in
+      ((Label (string_of_int n),type1)::l,o)
+    | _ -> ([],t)
+  in
+  let (input,output) = aux 0 t in
+  ok @@ (t_record (LMap.of_list input) (),output) 
+
 let get_t_sum (t:type_expression) : type_expression constructor_map result = match t.type_content with
   | T_sum m -> ok m
   | _ -> fail @@ Errors.not_a_x_type "sum" t ()

src/stages/ast_typed/combinators.mli

@@ -62,6 +62,7 @@ val get_t_key_hash : type_expression -> unit result
 val get_t_tuple : type_expression -> type_expression list result
 val get_t_pair : type_expression -> ( type_expression * type_expression ) result
 val get_t_function : type_expression -> ( type_expression * type_expression ) result
+val get_t_function_full : type_expression -> ( type_expression * type_expression ) result
 val get_t_sum : type_expression -> type_expression constructor_map result
 val get_t_record : type_expression -> type_expression label_map result
 val get_t_map : type_expression -> ( type_expression * type_expression ) result

src/stages/ast_typed/misc.ml

@@ -221,6 +221,9 @@ module Free_variables = struct
       union
         (expression b' let_result)
         (self rhs)
+    | E_recursive {fun_name;lambda;_} ->
+      let b' = union (singleton fun_name) b in
+      expression_content b' @@ E_lambda lambda
 
   and lambda : bindings -> lambda -> bindings = fun b l ->
     let b' = union (singleton l.binder) b in
@@ -529,7 +532,7 @@ let rec assert_value_eq (a, b: (expression*expression)) : unit result =
   | E_set _, _ ->
       fail @@ different_values_because_different_types "set vs. non-set" a b
   | (E_literal _, _) | (E_variable _, _) | (E_application _, _)
-  | (E_lambda _, _) | (E_let_in _, _)
+  | (E_lambda _, _) | (E_let_in _, _) | (E_recursive _, _)
   | (E_record_accessor _, _) | (E_record_update _,_)
   | (E_look_up _, _) | (E_matching _, _)
   -> fail @@ error_uncomparable_values "can't compare sequences nor loops" a b

src/stages/ast_typed/misc_smart.ml

@@ -45,9 +45,11 @@ module Captured_variables = struct
   let empty : bindings = []
   let of_list : expression_variable list -> bindings = fun x -> x
 
-  let rec expression : bindings -> expression -> bindings result = fun b ae ->
+  let rec expression : bindings -> expression -> bindings result = fun b e ->
+    expression_content b e.environment e.expression_content
+  and expression_content : bindings -> full_environment -> expression_content -> bindings result = fun b env ec ->
     let self = expression b in
-    match ae.expression_content with
+    match ec with
     | E_lambda l -> ok @@ Free_variables.lambda empty l
     | E_literal _ -> ok empty
     | E_constant {arguments;_} ->
@@ -56,7 +58,7 @@ module Captured_variables = struct
     | E_variable name -> (
         let%bind env_element =
           trace_option (simple_error "missing var in env") @@
-          Environment.get_opt name ae.environment in
+          Environment.get_opt name env in
         match env_element.definition with
         | ED_binder -> ok empty
         | ED_declaration {expr=_ ; free_variables=_} -> simple_fail "todo"
@@ -92,6 +94,9 @@ module Captured_variables = struct
     | E_let_in li ->
       let b' = union (singleton li.let_binder) b in
       expression b' li.let_result
+    | E_recursive r -> 
+      let b' = union (singleton r.fun_name) b in
+      expression_content b' env @@ E_lambda r.lambda
 
   and matching_variant_case : type a . (bindings -> a -> bindings result) -> bindings -> ((constructor' * expression_variable) * a) -> bindings result  = fun f b ((_,n),c) ->
     f (union (singleton n) b) c

src/stages/ast_typed/types.ml

@@ -41,6 +41,7 @@ and expression_content =
   | E_application of application
   | E_lambda of lambda
   | E_let_in of let_in
+  | E_recursive of recursive
   (* Variant *)
   | E_constructor of constructor (* For user defined constructors *)
   | E_matching of matching
@@ -76,6 +77,12 @@ and let_in = {
     inline : inline ;
   }
 
+and recursive = {
+  fun_name : expression_variable;
+  fun_type : type_expression;
+  lambda : lambda;
+}
+
 and constructor = {
     constructor: constructor';
     element: expression ;

src/stages/common/PP.ml

@@ -56,8 +56,11 @@ let constant ppf : constant' -> unit = function
   | C_ITER                  -> fprintf ppf "ITER"
   | C_FOLD                  -> fprintf ppf "FOLD"
   | C_FOLD_WHILE            -> fprintf ppf "FOLD_WHILE"
-  | C_CONTINUE              -> fprintf ppf "CONTINUE"
+  | C_FOLD_CONTINUE         -> fprintf ppf "CONTINUE"
-  | C_STOP                  -> fprintf ppf "STOP"
+  | C_FOLD_STOP             -> fprintf ppf "STOP"
+  | C_LOOP_LEFT             -> fprintf ppf "LOOP_LEFT"
+  | C_LOOP_CONTINUE         -> fprintf ppf "LOOP_CONTINUE"
+  | C_LOOP_STOP             -> fprintf ppf "LOOP_STOP"
   (* MATH *)
   | C_NEG                   -> fprintf ppf "NEG"
   | C_ABS                   -> fprintf ppf "ABS"

src/stages/common/types.ml

@@ -197,8 +197,11 @@ and constant' =
   (* Loops *)
   | C_ITER
   | C_FOLD_WHILE
-  | C_CONTINUE
+  | C_FOLD_CONTINUE
-  | C_STOP
+  | C_FOLD_STOP
+  | C_LOOP_LEFT
+  | C_LOOP_CONTINUE
+  | C_LOOP_STOP
   | C_FOLD
   (* MATH *)
   | C_NEG

src/stages/ligo_interpreter/PP.ml

@@ -19,6 +19,7 @@ let rec pp_value : value -> string = function
       recmap "" in
     Format.asprintf "{ %s }" content
   | V_Func_val _ -> Format.asprintf "<fun>"
+  | V_Func_rec _ -> Format.asprintf "<rec fun>"
   | V_Construct (name,v) -> Format.asprintf "%s(%s)" name (pp_value v)
   | V_List vl ->
     Format.asprintf "[%s]" @@
@@ -36,4 +37,4 @@ let pp_env : env -> unit = fun env ->
     Format.printf "\t%s -> %s\n" (Var.to_name var) (pp_value v))
   env in
   let () = Format.printf "\n}\n" in
-  ()
+  ()

src/stages/ligo_interpreter/types.ml

@@ -31,6 +31,7 @@ and constant_val =
 
 and value =
   | V_Func_val of (expression_variable * Ast_typed.expression * env)
+  | V_Func_rec of (expression_variable * expression_variable * Ast_typed.expression * env)
   | V_Ct of constant_val
   | V_List of value list
   | V_Record of value label_map

src/stages/mini_c/PP.ml

@@ -149,8 +149,11 @@ and constant ppf : constant' -> unit = function
   (* Loops *)
   | C_FOLD                  -> fprintf ppf "FOLD"
   | C_FOLD_WHILE            -> fprintf ppf "FOLD_WHILE"
-  | C_CONTINUE              -> fprintf ppf "CONTINUE"
+  | C_FOLD_CONTINUE         -> fprintf ppf "CONTINUE"
-  | C_STOP                  -> fprintf ppf "STOP"
+  | C_FOLD_STOP             -> fprintf ppf "STOP"
+  | C_LOOP_LEFT             -> fprintf ppf "LOOP_LEFT"
+  | C_LOOP_CONTINUE         -> fprintf ppf "LOOP_CONTINUE"
+  | C_LOOP_STOP             -> fprintf ppf "LOOP_STOP"
   | C_ITER                  -> fprintf ppf "ITER"
   (* MATH *)
   | C_NEG                   -> fprintf ppf "NEG"

src/stages/typesystem/misc.ml

@@ -164,6 +164,12 @@ module Substitution = struct
         let%bind rhs = s_expression ~substs rhs in
         let%bind let_result = s_expression ~substs let_result in
         ok @@ T.E_let_in { let_binder; rhs; let_result; inline }
+      | T.E_recursive { fun_name; fun_type; lambda} ->
+        let%bind fun_name = s_variable ~substs fun_name in
+        let%bind fun_type = s_type_expression ~substs fun_type in
+        let%bind sec = s_expression_content ~substs (T.E_lambda lambda) in
+        let lambda = match sec with E_lambda l -> l | _ -> failwith "impossible case" in
+        ok @@ T.E_recursive { fun_name; fun_type; lambda}
       | T.E_constructor  {constructor;element} ->
         let%bind constructor = s_constructor ~substs constructor in
         let%bind element = s_expression ~substs element in

src/stages/typesystem/shorthands.ml

@@ -48,6 +48,7 @@ let (=>) tc ty = (tc , ty)
 let (-->) arg ret = P_constant (C_arrow  , [arg; ret])
 let option t  = P_constant (C_option  , [t])
 let pair a b  = P_constant (C_record , [a; b])
+let sum  a b  = P_constant (C_variant, [a; b])
 let map  k v  = P_constant (C_map   , [k; v])
 let unit      = P_constant (C_unit    , [])
 let list   t  = P_constant (C_list    , [t])

src/test/contracts/interpret_test.mligo

@@ -232,3 +232,15 @@ let set_mem =
   Set.mem 1 s,
   Set.mem 4 s,
   Set.mem 1 (Set.empty : int set)
+
+let recursion_let_rec_in =
+  let rec sum : int*int -> int = fun ((n,res):int*int) ->
+    let i = 1 in
+    if (n<1) then res else sum (n-i,res+n)
+  in
+  sum (10,0)
+
+let rec sum_rec ((n,acc):int * int) : int =
+    if (n < 1) then acc else sum_rec (n-1, acc+n)
+
+let top_level_recursion = sum_rec (10,0)

src/test/contracts/loop.mligo

@@ -1,10 +1,9 @@
 (* Test functional iterators in CameLIGO *)
 
-let aux_simple (i : int) : bool * int =
+let rec aux_simple (i : int) : int =
-  if i < 100 then Loop.resume (i + 1) else Loop.stop i
+  if i < 100 then aux_simple (i + 1) else i
 
-let counter_simple (n : int) : int =
+let counter_simple (n : int) : int = aux_simple n
-  Loop.fold_while aux_simple n
 
 type sum_aggregator = {
   counter : int;
@@ -13,25 +12,23 @@ type sum_aggregator = {
 
 let counter (n : int) : int =
   let initial : sum_aggregator = {counter=0; sum=0} in
-  let aggregate = fun (prev : sum_aggregator) ->
+  let rec aggregate : sum_aggregator -> int = fun (prev: sum_aggregator) ->
     if prev.counter <= n then
-      Loop.resume {counter = prev.counter + 1;
+      aggregate {counter = prev.counter + 1;
                    sum = prev.counter + prev.sum}
     else
-      Loop.stop {counter = prev.counter; sum = prev.sum} in
+      prev.sum 
-  let out : sum_aggregator =
+  in
-    Loop.fold_while aggregate initial
+  aggregate initial
-  in out.sum
 
-let aux_nest (prev : sum_aggregator) : bool * sum_aggregator =
+let rec aux_nest (prev : sum_aggregator) : int =
   if prev.counter < 100 then
-    let sum : int =
+    let sum = prev.sum + (aux_simple prev.counter) in
-      prev.sum + Loop.fold_while aux_simple prev.counter
+    aux_nest {counter = prev.counter + 1; sum = sum}
-    in Loop.resume {counter = prev.counter + 1; sum = sum}
   else
-    Loop.stop {counter = prev.counter; sum = prev.sum}
+    prev.sum
 
 let counter_nest (n : int) : int =
   let initial : sum_aggregator = {counter=0; sum=0} in
-  let out : sum_aggregator = Loop.fold_while aux_nest initial
+  let out = aux_nest initial
-  in out.sum
+  in out

src/test/contracts/loop.religo

@@ -1,9 +1,9 @@
 /* Test loops in ReasonLIGO */
 
-let aux_simple = (i : int) : (bool, int) =>
+let rec aux_simple = (i : int) : int =>
-  if (i < 100) { Loop.resume (i + 1); } else { Loop.stop (i); };
+  if (i < 100) { aux_simple (i + 1); } else { i; };
 
-let counter_simple = (n : int) : int => Loop.fold_while (aux_simple, n);
+let counter_simple = (n : int) : int => aux_simple (n);
 
 type sum_aggregator = {
   counter : int,
@@ -12,30 +12,28 @@ type sum_aggregator = {
 
 let counter = (n : int) : int => {
   let initial : sum_aggregator = {counter: 0, sum: 0};
-  let aggregate = (prev : sum_aggregator) =>
+  let rec aggregate = (prev : sum_aggregator):int =>
     if (prev.counter <= n) {
-      Loop.resume ({counter : prev.counter + 1,
+      aggregate ({counter : prev.counter + 1,
                     sum : prev.counter + prev.sum});
     } else {
-      Loop.stop ({counter: prev.counter, sum: prev.sum});
+      prev.sum;
     };
-  let out : sum_aggregator =
+  aggregate (initial);
-    Loop.fold_while (aggregate, initial);
-  out.sum;
 };
 
-let aux_nest = (prev : sum_aggregator) : (bool, sum_aggregator) =>
+let rec aux_nest = (prev : sum_aggregator) : sum_aggregator =>
   if (prev.counter < 100) {
     let sum : int =
-      prev.sum + Loop.fold_while (aux_simple, prev.counter);
+      prev.sum + aux_simple (prev.counter);
-    Loop.resume ({counter: prev.counter + 1,
+    aux_nest ({counter: prev.counter + 1,
                   sum: sum});
   } else {
-    Loop.stop ({counter: prev.counter, sum: prev.sum});
+    ({counter: prev.counter, sum: prev.sum});
   };
 
 let counter_nest = (n : int) : int => {
   let initial : sum_aggregator = {counter: 0, sum: 0};
-  let out : sum_aggregator = Loop.fold_while (aux_nest, initial);
+  let out : sum_aggregator = aux_nest (initial);
   out.sum;
 };

src/test/contracts/negative/error_no_tail_recursive_function.mligo

@@ -0,0 +1,3 @@
+let rec unvalid (n:int):int =
+    let res = unvalid (n) in
+    res + 1

src/test/contracts/recursion.ligo

@@ -0,0 +1,7 @@
+// Test while loops in PascaLIGO
+
+recursive function sum (const n : int; const acc: int) : int is
+  if n<1 then acc else sum(n-1,acc+n)
+
+recursive function fibo (const n: int; const n_1: int; const n_0 :int) : int is
+  if n<2 then n_1 else fibo(n-1,n_1+n_0,n_1)

src/test/contracts/recursion.mligo

@@ -0,0 +1,7 @@
+// Test while loops in PascaLIGO
+
+let rec sum ((n,acc):int * int) : int =
+    if (n < 1) then acc else sum (n-1, acc+n)
+ 
+let rec fibo ((n,n_1,n_0):int*int*int) : int = 
+    if (n < 2) then n_1 else fibo (n-1, n_1 + n_0, n_1)

src/test/contracts/recursion.religo

@@ -0,0 +1,7 @@
+// Test while loops in PascaLIGO
+
+let rec sum = ((n, acc) : (int,int)): int =>
+    if (n < 1) {acc;} else {sum ((n-1,acc+n));};
+
+let rec fibo = ((n, n_1, n_0) : (int,int,int)): int =>
+    if (n < 2) {n_1;} else {fibo ((n-1,n_1+n_0,n_1));};

src/test/integration_tests.ml

@@ -1493,6 +1493,46 @@ let assert_religo () : unit result =
   let%bind _ = expect_eq program "main" (make_input true) make_expected in
   ok ()
 
+let recursion_ligo () : unit result =
+  let%bind program = type_file "./contracts/recursion.ligo" in
+  let%bind _ =
+    let make_input = e_pair (e_int 10) (e_int 0) in
+    let make_expected = e_int 55 in
+    expect_eq program "sum" make_input make_expected 
+  in
+  let%bind _ =
+    let make_input = e_tuple [(e_int 10); (e_int 1); (e_int 1)] in
+    let make_expected = e_int 89 in
+    expect_eq program "fibo" make_input make_expected
+  in ok ()
+  
+
+let recursion_mligo () : unit result =
+  let%bind program = mtype_file "./contracts/recursion.mligo" in
+  let%bind _ =
+    let make_input = e_pair (e_int 10) (e_int 0) in
+    let make_expected = e_int 55 in
+    expect_eq program "sum" make_input make_expected 
+  in
+  let%bind _ =
+    let make_input = e_tuple [(e_int 10); (e_int 1); (e_int 1)] in
+    let make_expected = e_int 89 in
+    expect_eq program "fibo" make_input make_expected
+  in ok ()
+
+let recursion_religo () : unit result =
+  let%bind program = retype_file "./contracts/recursion.religo" in
+  let%bind _ =
+    let make_input = e_pair (e_int 10) (e_int 0) in
+    let make_expected = e_int 55 in
+    expect_eq program "sum" make_input make_expected 
+  in
+  let%bind _ =
+    let make_input = e_tuple [(e_int 10); (e_int 1); (e_int 1)] in
+    let make_expected = e_int 89 in
+    expect_eq program "fibo" make_input make_expected
+  in ok ()
+
 let guess_string_mligo () : unit result =
   let%bind program = type_file "./contracts/guess_string.mligo" in
   let make_input = fun n -> e_pair (e_int n) (e_int 42) in
@@ -2407,6 +2447,9 @@ let main = test_suite "Integration (End to End)" [
     test "failwith ligo" failwith_ligo ;
     test "failwith mligo" failwith_mligo ;
     test "assert mligo" assert_mligo ;
+    test "recursion (ligo)" recursion_ligo ;
+    test "recursion (mligo)" recursion_mligo ;
+    test "recursion (religo)" recursion_religo ;
     (* test "guess string mligo" guess_string_mligo ; WIP? *)
     test "lambda mligo" lambda_mligo ;
     test "lambda religo" lambda_religo ;

test.mligo

@@ -0,0 +1,8 @@
+let rec fibo2 ((n,n_1,n_0):int*int*int) : int =
+  let fibo2 : int -> int = fun (k : int) -> k in
+  if (n < 2) then n_1 else fibo2 3
+
+let main (p,s : unit * int) : operation list * int =
+  let x : int = fibo2 (5, 1, 1) in
+  (([] : operation list), x)
+

vendors/ligo-utils/tezos-utils/x_michelson.ml

@@ -78,6 +78,8 @@ let i_dug n : michelson = prim ~children:[Int (0 , Z.of_int n)] I_DUG
 let i_unpair = seq [i_dup ; i_car ; dip i_cdr]
 let i_unpiar = seq [i_dup ; i_cdr ; dip i_car]
 
+let i_loop_left body = prim ~children:[seq[body; dip i_drop]] I_LOOP_LEFT
+
 let rec strip_annots : michelson -> michelson = function
   | Seq(l, s) -> Seq(l, List.map strip_annots s)
   | Prim (l, p, lst, _) -> Prim (l, p, List.map strip_annots lst, [])