add loop ; fix bug in sub-scope affectation

src/ligo/ast_typed.ml

@@ -351,7 +351,12 @@ let rec assert_value_eq (a, b: (value*value)) : unit result = match (a.expressio
   | E_constant _, E_constant _ ->
       simple_fail "different constants"
   | E_constant _, _ ->
-      simple_fail "comparing constant with other stuff"
+      let error_content =
+        Format.asprintf "%a vs %a"
+          PP.annotated_expression a
+          PP.annotated_expression b
+      in
+      fail @@ error "comparing constant with other stuff" error_content
 
   | E_constructor (ca, a), E_constructor (cb, b) when ca = cb -> (
       let%bind _eq = assert_value_eq (a, b) in
@@ -493,7 +498,7 @@ module Combinators = struct
   let e_nat n : expression = E_literal (Literal_nat n)
   let e_bool b : expression = E_literal (Literal_bool b)
   let e_string s : expression = E_literal (Literal_string s)
-  let e_pair a b : expression = E_constant ("PAIR", [a; b])
+  let e_pair a b : expression = E_tuple [a; b]
 
   let e_a_unit = annotated_expression e_unit (t_unit ())
   let e_a_int n = annotated_expression (e_int n) (t_int ())

src/ligo/contracts/heap-instance.ligo

@@ -0,0 +1,3 @@
+type heap_element is int * string
+
+#include "heap.ligo"

src/ligo/contracts/heap.ligo

@@ -1,6 +1,7 @@
-type heap_element is int * string ;
-
 type heap is map(int, heap_element) ;
 
 function is_empty (const h : heap) : bool is
   block {skip} with size(h) = 0n
+
+function get_top (const h : heap) : heap_element is
+  block {skip} with get_force(0, h)

src/ligo/contracts/loop.ligo

@@ -0,0 +1,19 @@
+function counter (var n : nat) : nat is block {
+  var i : nat := 0n ;
+  while (i < n) block {
+    i := i + 1n ;
+  }
+} with i
+
+function sum (var n : nat) : nat is block {
+  var i : nat := 0n ;
+  var r : nat := 0n ;
+  while (i < n) block {
+    i := i + 1n ;
+    r := r + i ;
+  }
+} with r
+
+function dummy (const n : nat) : nat is block {
+  while (False) block { skip }
+} with n

src/ligo/mini_c.ml

@@ -199,7 +199,7 @@ module PP = struct
     | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b
 
   and block ppf ((b, _):block) =
-    fprintf ppf "@[<v 2>{@,%a@]@,}" (pp_print_list ~pp_sep:pp_print_newline statement) b
+    fprintf ppf "{  @;@[<v 2>%a@]@;}" (pp_print_list ~pp_sep:(PP.tag "@;") statement) b
 
   let tl_statement ppf (ass, _) = assignment ppf ass
 
@@ -556,7 +556,7 @@ module Environment = struct
           | Ok (code, tv) -> ok (seq [i_car ; code], tv)
           | Errors _ ->
             let%bind (code, tv) = aux b str in
-            ok (seq [i_car ; code], tv)
+            ok (seq [i_cdr ; code], tv)
         )
     in
     let%bind (code, tv) = aux s str in
@@ -620,7 +620,7 @@ module Environment = struct
       ok ()
     in
 
-    ok code
+    ok @@ seq [ i_comment "set" ; code ]
 end
 
 module Translate_program = struct
@@ -650,6 +650,7 @@ module Translate_program = struct
 
   let rec get_predicate : string -> predicate result = function
     | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
+    | "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD
     | "NEG" -> ok @@ simple_unary @@ prim I_NEG
     | "OR" -> ok @@ simple_binary @@ prim I_OR
     | "AND" -> ok @@ simple_binary @@ prim I_AND
@@ -657,6 +658,7 @@ module Translate_program = struct
     | "CAR" -> ok @@ simple_unary @@ prim I_CAR
     | "CDR" -> ok @@ simple_unary @@ prim I_CDR
     | "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ]
+    | "LT" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_LT]
     | "UPDATE" -> ok @@ simple_ternary @@ prim I_UPDATE
     | "SOME" -> ok @@ simple_unary @@ prim I_SOME
     | "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some]
@@ -864,6 +866,7 @@ module Translate_program = struct
       in
       ok ()
     in
+
     ok code
 
   and translate_statement ((s', w_env) as s:statement) : michelson result =
@@ -919,10 +922,38 @@ module Translate_program = struct
       let%bind block = translate_regular_block block in
       ok @@ (seq [
         i_push_unit ; expr ; i_car ;
-        dip Environment.to_michelson_extend ;
-        prim ~children:[block ; Environment.to_michelson_restrict ; i_push_unit ; expr ; i_car] I_LOOP ;
+        prim ~children:[seq [
+            Environment.to_michelson_extend ;
+            block ;
+            Environment.to_michelson_restrict ;
+            i_push_unit ; expr ; i_car]] I_LOOP ;
       ])
     in
+
+    let%bind () =
+      let%bind (Ex_ty pre_ty) = Environment.to_ty w_env.pre_environment in
+      let input_stack_ty = Stack.(pre_ty @: nil) in
+      let%bind (Ex_ty post_ty) = Environment.to_ty w_env.post_environment in
+      let output_stack_ty = Stack.(post_ty @: nil) in
+      let%bind error_message =
+        let%bind pre_env_michelson = Environment.to_michelson_type w_env.pre_environment in
+        let%bind post_env_michelson = Environment.to_michelson_type w_env.post_environment in
+        ok @@ Format.asprintf
+          "statement : %a\ncode : %a\npre type : %a\npost type : %a"
+          PP.statement s
+          Michelson.pp code
+          Michelson.pp pre_env_michelson
+          Michelson.pp post_env_michelson
+      in
+      let%bind _ =
+        Trace.trace_tzresult_lwt (error "error parsing statement code" error_message) @@
+        Tezos_utils.Memory_proto_alpha.parse_michelson code
+          input_stack_ty output_stack_ty
+      in
+      ok ()
+    in
+
+
     ok code
 
   and translate_regular_block ((b, env):block) : michelson result =

src/ligo/test/heap_tests.ml

@@ -7,7 +7,7 @@ let get_program =
   fun () -> match !s with
     | Some s -> ok s
     | None -> (
-        let%bind program = type_file "./contracts/heap.ligo" in
+        let%bind program = type_file "./contracts/heap-instance.ligo" in
         s := Some program ;
         ok program
       )
@@ -57,7 +57,25 @@ let is_empty () : unit result =
     @@ [0 ; 2 ; 7 ; 12] in
   ok ()
 
+let get_top () : unit result =
+  let%bind program = get_program () in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = dummy n in
+    match n, easy_run_typed "get_top" program input with
+    | 0, Trace.Ok _ -> simple_fail "unexpected success"
+    | 0, _ -> ok ()
+    | _, result ->
+        let%bind result' = result in
+        let expected = e_a_pair (e_a_int 0) (e_a_string "0") in
+        AST_Typed.assert_value_eq (expected, result')
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 7 ; 12] in
+  ok ()
 
 let main = "Heap (End to End)", [
     test "is_empty" is_empty ;
+    test "get_top" get_top ;
   ]

src/ligo/test/integration_tests.ml

@@ -239,6 +239,50 @@ let condition () : unit result =
     @@ [0 ; 2 ; 42 ; 163 ; -1] in
   ok ()
 
+let loop () : unit result =
+  let%bind program = type_file "./contracts/loop.ligo" in
+  let%bind _dummy = trace (simple_error "dummy") @@
+    let aux n =
+      let open AST_Typed.Combinators in
+      let input = e_a_nat n in
+      let%bind result = easy_run_typed "dummy" program input in
+      let expected = e_a_nat n in
+      AST_Typed.assert_value_eq (expected, result)
+    in
+    let%bind _ = bind_list
+      @@ List.map aux
+      @@ [0 ; 2 ; 42 ; 163] in
+    ok ()
+  in
+  let%bind _counter = trace (simple_error "counter") @@
+    let aux n =
+      let open AST_Typed.Combinators in
+      let input = e_a_nat n in
+      let%bind result = easy_run_typed "counter" program input in
+      let expected = e_a_nat n in
+      AST_Typed.assert_value_eq (expected, result)
+    in
+    let%bind _ = bind_list
+      @@ List.map aux
+      @@ [0 ; 2 ; 42 ; 12] in
+    ok ()
+  in
+  let%bind _sum = trace (simple_error "sum") @@
+    let aux n =
+      let open AST_Typed.Combinators in
+      let input = e_a_nat n in
+      let%bind result = easy_run_typed "sum" program input in
+      let expected = e_a_nat (n * (n + 1) / 2) in
+      AST_Typed.assert_value_eq (expected, result)
+    in
+    let%bind _ = bind_list
+      @@ List.map aux
+      @@ [0 ; 2 ; 42 ; 12] in
+    ok ()
+  in
+  ok()
+
+
 let matching () : unit result =
   let%bind program = type_file "./contracts/match.ligo" in
   let%bind _bool =
@@ -350,6 +394,7 @@ let main = "Integration (End to End)", [
     test "map" map ;
     test "multiple parameters" multiple_parameters ;
     test "condition" condition ;
+    test "loop" loop ;
     test "matching" matching ;
     test "declarations" declarations ;
     test "quote declaration" quote_declaration ;

src/ligo/transpiler.ml

@@ -73,7 +73,10 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
   match i with
   | I_assignment {name;annotated_expression} ->
       let%bind (_, t, _) as expression = translate_annotated_expression env annotated_expression in
-      let env' = Environment.add (name, t) env in
+      let env' =
+        match Environment.has name env with
+        | true -> env
+        | false -> Environment.add (name, t) env in
       return ~env' (Assignment (name, expression))
   | I_matching (expr, m) -> (
       let%bind expr' = translate_annotated_expression env expr in
@@ -96,7 +99,8 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
     )
   | I_loop (expr, body) ->
       let%bind expr' = translate_annotated_expression env expr in
-      let%bind body' = translate_block env body in
+      let env' = Environment.extend env in
+      let%bind body' = translate_block env' body in
       return (While (expr', body'))
   | I_skip -> ok None
   | I_fail _ -> simple_fail "todo : fail"

src/ligo/typer.ml

@@ -406,12 +406,16 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
   let open O in
   match (name, lst) with
   | "ADD", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("ADD_INT", t_int ())
+  | "ADD", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("ADD_NAT", t_nat ())
   | "ADD", [a ; b] when type_value_eq (a, t_string ()) && type_value_eq (b, t_string ()) -> ok ("CONCAT", t_string ())
   | "ADD", [_ ; _] -> simple_fail "bad types to add"
   | "ADD", _ -> simple_fail "bad number of params to add"
   | "EQ", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("EQ", t_bool ())
   | "EQ", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("EQ", t_bool ())
   | "EQ", _ -> simple_fail "EQ only defined over int and nat"
+  | "LT", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("LT", t_bool ())
+  | "LT", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("LT", t_bool ())
+  | "LT", _ -> simple_fail "LT only defined over int and nat"
   | "OR", [a ; b] when type_value_eq (a, t_bool ()) && type_value_eq (b, t_bool ()) -> ok ("OR", t_bool ())
   | "OR", _ -> simple_fail "OR only defined over bool"
   | "AND", [a ; b] when type_value_eq (a, t_bool ()) && type_value_eq (b, t_bool ()) -> ok ("AND", t_bool ())