diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 19c85fe29..855f13082 100644 --- a/src/ligo/ast_simplified.ml +++ b/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) diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index f34781fd5..cd736ba51 100644 --- a/src/ligo/ast_typed.ml +++ b/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 = diff --git a/src/ligo/contracts/counter.ligo b/src/ligo/contracts/counter.ligo new file mode 100644 index 000000000..1241242c5 --- /dev/null +++ b/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) diff --git a/src/ligo/meta_michelson/contract.ml b/src/ligo/meta_michelson/contract.ml index 518fc2fb8..b2df55022 100644 --- a/src/ligo/meta_michelson/contract.ml +++ b/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 diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml index 3b0cef09c..6c7f49149 100644 --- a/src/ligo/mini_c/PP.ml +++ b/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 diff --git a/src/ligo/mini_c/compiler.ml b/src/ligo/mini_c/compiler.ml index b9ab70f76..4630b218e 100644 --- a/src/ligo/mini_c/compiler.ml +++ 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 = diff --git a/src/ligo/mini_c/compiler_type.ml b/src/ligo/mini_c/compiler_type.ml index c8bc5597e..e2753f4bc 100644 --- a/src/ligo/mini_c/compiler_type.ml +++ b/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 diff --git a/src/ligo/mini_c/types.ml b/src/ligo/mini_c/types.ml index 6e71a2ffa..03731894b 100644 --- a/src/ligo/mini_c/types.ml +++ b/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) diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index ae6ad0b04..ae988aa49 100644 --- a/src/ligo/simplify.ml +++ b/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 diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index af4dfa3e5..26df37072 100644 --- a/src/ligo/test/integration_tests.ml +++ b/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 ; ] diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index 16a6df154..1b4a5c704 100644 --- a/src/ligo/transpiler.ml +++ b/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') diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 46306876b..074afc7a2 100644 --- a/src/ligo/typer.ml +++ b/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}