add counter

src/ligo/ast_simplified.ml

@@ -364,6 +364,7 @@ module Combinators = struct
   let t_int       : type_expression = T_constant ("int", [])
   let t_unit      : type_expression = T_constant ("unit", [])
   let t_option  o : type_expression = T_constant ("option", [o])
+  let t_list  t : type_expression = T_constant ("list", [t])
   let t_tuple lst : type_expression = T_tuple lst
   let t_pair a b = t_tuple [a ; b]
   let t_record m  : type_expression = (T_record m)

src/ligo/ast_typed.ml

@@ -431,6 +431,16 @@ let rec assert_value_eq (a, b: (value*value)) : unit result =
   | E_map _, _ ->
       simple_fail "comparing map with other stuff"
 
+  | E_list lsta, E_list lstb -> (
+      let%bind lst =
+        generic_try (simple_error "list of different lengths")
+          (fun () -> List.combine lsta lstb) in
+      let%bind _all = bind_map_list assert_value_eq lst in
+      ok ()
+    )
+  | E_list _, _ ->
+      simple_fail "comparing list with other stuff"
+
   | _, _ -> simple_fail "comparing not a value"
 
 let merge_annotation (a:type_value option) (b:type_value option) : type_value result =

src/ligo/contracts/counter.ligo

@@ -0,0 +1,2 @@
+function main (const p : int ; const s : int) : (list(operation) * int) is
+  block {skip} with ((nil : operation), p + s)

src/ligo/meta_michelson/contract.ml

@@ -252,6 +252,7 @@ module Types = struct
   let big_map k v = Big_map_t (k, v, None)
 
   let signature = Signature_t None
+  let operation = Operation_t None
 
   let bool = Bool_t None
 

src/ligo/mini_c/PP.ml

@@ -13,6 +13,7 @@ let type_base ppf : type_base -> _ = function
   | Base_nat -> fprintf ppf "nat"
   | Base_string -> fprintf ppf "string"
   | Base_bytes -> fprintf ppf "bytes"
+  | Base_operation -> fprintf ppf "operation"
 
 let rec type_ ppf : type_value -> _ = function
   | T_or(a, b) -> fprintf ppf "(%a) | (%a)" type_ a type_ b

src/ligo/mini_c/compiler.ml

@@ -51,7 +51,8 @@ let rec get_predicate : string -> expression list -> predicate result = fun s ls
   | "GET" -> ok @@ simple_binary @@ prim I_GET
   | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE
   | "INT" -> ok @@ simple_unary @@ prim I_INT
-  | "CONS" -> ok @@ simple_binary @@ seq [prim I_SWAP ; prim I_CONS]
+  | "CONS" -> ok @@ simple_binary @@ prim I_CONS
+  (* | "CONS" -> ok @@ simple_binary @@ seq [prim I_SWAP ; prim I_CONS] *)
   | "MAP_REMOVE" ->
       let%bind v = match lst with
         | [ _ ; (_, m, _) ] ->
@@ -89,7 +90,8 @@ and translate_value (v:value) : michelson result = match v with
       ok @@ seq @@ List.map aux lst'
   | D_list lst ->
       let%bind lst' = bind_map_list translate_value lst in
-      let aux = fun a -> prim ~children:[a] D_Elt in
+      let aux = fun a -> a in
+      (* let aux = fun a -> prim ~children:[a] D_Elt in *)
       ok @@ seq @@ List.map aux lst'
 
 and translate_function ({capture;content}:anon_function) : michelson result =

src/ligo/mini_c/compiler_type.ml

@@ -21,6 +21,7 @@ module Ty = struct
     | Base_int -> return int_k
     | Base_string -> return string_k
     | Base_bytes -> return bytes_k
+    | Base_operation -> fail (not_comparable "operation")
 
   let comparable_type : type_value -> ex_comparable_ty result = fun tv ->
     match tv with
@@ -44,7 +45,7 @@ module Ty = struct
     | Base_nat -> return nat
     | Base_string -> return string
     | Base_bytes -> return bytes
-
+    | Base_operation -> return operation
 
   let rec type_ : type_value -> ex_ty result =
     function
@@ -114,6 +115,7 @@ let base_type : type_base -> O.michelson result =
   | Base_nat -> ok @@ O.prim T_nat
   | Base_string -> ok @@ O.prim T_string
   | Base_bytes -> ok @@ O.prim T_bytes
+  | Base_operation -> ok @@ O.prim T_operation
 
 let rec type_ : type_value -> O.michelson result =
   function

src/ligo/mini_c/types.ml

@@ -7,6 +7,7 @@ type type_base =
   | Base_bool
   | Base_int | Base_nat
   | Base_string | Base_bytes
+  | Base_operation
 
 type type_value =
   | T_pair of (type_value * type_value)

src/ligo/simplify.ml

@@ -236,7 +236,7 @@ and simpl_list_expression (t:Raw.list_expr) : ae result =
       let n' = n.value.inside in
       let%bind t' = simpl_type_expression n'.list_type in
       let e' = E_list [] in
-      ok (annotated_expression e' (Some t'))
+      ok (annotated_expression e' (Some (Combinators.t_list t')))
 
 and simpl_binop (name:string) (t:_ Raw.bin_op) : ae result =
   let%bind a = simpl_expression t.arg1 in

src/ligo/test/integration_tests.ml

@@ -461,19 +461,19 @@ let quote_declarations () : unit result =
     @@ [0 ; 2 ; 42 ; 163 ; -1] in
   ok ()
 
-(* let counter_contract () : unit result =
- *   let%bind program = type_file "./contracts/counter.ligo" in
- *   let aux n =
- *     let open AST_Typed.Combinators in
- *     let input = e_a_pair (e_a_int n) (e_a_int 42) in
- *     let%bind result = easy_run_main_typed program input in
- *     let expected = e_a_pair (e_a_list []) (e_a_int (42 + n)) in
- *     AST_Typed.assert_value_eq (result, expected)
- *   in
- *   let%bind _ = bind_list
- *     @@ List.map aux
- *     @@ [0 ; 2 ; 42 ; 163 ; -1] in
- *   ok () *)
+let counter_contract () : unit result =
+  let%bind program = type_file "./contracts/counter.ligo" in
+  let aux n =
+    let open AST_Typed.Combinators in
+    let input = e_a_pair (e_a_int n) (e_a_int 42) in
+    let%bind result = easy_run_main_typed program input in
+    let expected = e_a_pair (e_a_list [] (t_int ())) (e_a_int (42 + n)) in
+    AST_Typed.assert_value_eq (result, expected)
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 42 ; 163 ; -1] in
+  ok ()
 
 let main = "Integration (End to End)", [
     test "basic" basic ;
@@ -495,5 +495,5 @@ let main = "Integration (End to End)", [
     test "quote declaration" quote_declaration ;
     test "quote declarations" quote_declarations ;
     test "#include directives" include_ ;
-    (* test "counter contract" counter_contract ; *)
+    test "counter contract" counter_contract ;
   ]

src/ligo/transpiler.ml

@@ -18,6 +18,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
   | T_constant ("nat", []) -> ok (T_base Base_nat)
   | T_constant ("string", []) -> ok (T_base Base_string)
   | T_constant ("unit", []) -> ok (T_base Base_unit)
+  | T_constant ("operation", []) -> ok (T_base Base_operation)
   | T_constant ("map", [key;value]) ->
       let%bind kv' = bind_map_pair translate_type (key, value) in
       ok (T_map kv')

src/ligo/typer.ml

@@ -360,10 +360,15 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
           | Some c' ->
               let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
               ok (Some c') in
+        let%bind init = match tv_opt with
+          | None -> ok None
+          | Some ty ->
+              let%bind ty' = Ast_typed.Combinators.get_t_list ty in
+              ok (Some ty') in
         let%bind ty =
-          let%bind opt = bind_fold_list aux None
+          let%bind opt = bind_fold_list aux init
           @@ List.map Ast_typed.get_type_annotation lst' in
-          trace_option (simple_error "empty list expression") opt in
+          trace_option (simple_error "empty list expression without annotation") opt in
         check (t_list ty ())
       in
       ok O.{expression = O.E_list lst' ; type_annotation}