diff --git a/src/lib_utils/PP.ml b/src/lib_utils/PP.ml index 442d1e62e..87eb5e87b 100644 --- a/src/lib_utils/PP.ml +++ b/src/lib_utils/PP.ml @@ -14,6 +14,9 @@ let ne_list_sep value separator ppf (hd, tl) = separator ppf () ; pp_print_list ~pp_sep:separator value ppf tl +let prepend s f ppf a = + fprintf ppf "%s%a" s f a + let pair_sep value sep ppf (a, b) = fprintf ppf "%a %s %a" value a sep value b let smap_sep value sep ppf m = let module SMap = X_map.String in diff --git a/src/lib_utils/x_list.ml b/src/lib_utils/x_list.ml index 3caa79f92..e79d2a783 100644 --- a/src/lib_utils/x_list.ml +++ b/src/lib_utils/x_list.ml @@ -11,6 +11,11 @@ let filter_map f = in aux [] +let cons_iter = fun fhd ftl lst -> + match lst with + | [] -> () + | hd :: tl -> fhd hd ; List.iter ftl tl + let range n = let rec aux acc n = if n = 0 diff --git a/src/lib_utils/x_memory_proto_alpha.ml b/src/lib_utils/x_memory_proto_alpha.ml index 3aeba32ac..90ad7803a 100644 --- a/src/lib_utils/x_memory_proto_alpha.ml +++ b/src/lib_utils/x_memory_proto_alpha.ml @@ -66,6 +66,12 @@ let unparse_michelson_data Readable ty value >>=?? fun (michelson, _) -> return michelson +let unparse_michelson_ty + ?(tezos_context = dummy_environment.tezos_context) + ty : Michelson.t tzresult Lwt.t = + Script_ir_translator.unparse_ty tezos_context ty >>=?? fun (michelson, _) -> + return michelson + let interpret ?(tezos_context = dummy_environment.tezos_context) ?(source = (List.nth dummy_environment.identities 0).implicit_contract) diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 255262af1..59f910963 100644 --- a/src/ligo/ast_simplified.ml +++ b/src/ligo/ast_simplified.ml @@ -78,7 +78,8 @@ and access_path = access list and literal = | Literal_unit | Literal_bool of bool - | Literal_number of int + | Literal_int of int + | Literal_nat of int | Literal_string of string | Literal_bytes of bytes @@ -136,7 +137,8 @@ module PP = struct let literal ppf (l:literal) = match l with | Literal_unit -> fprintf ppf "Unit" | Literal_bool b -> fprintf ppf "%b" b - | Literal_number n -> fprintf ppf "%d" n + | Literal_int n -> fprintf ppf "%d" n + | Literal_nat n -> fprintf ppf "%d" n | Literal_string s -> fprintf ppf "%S" s | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b @@ -366,7 +368,8 @@ module Combinators = struct let e_var (s : string) : expression = E_variable s let e_unit () : expression = E_literal (Literal_unit) - let e_number n : expression = E_literal (Literal_number n) + let e_int n : expression = E_literal (Literal_int n) + 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_bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b)) diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index c72cc69b1..08d878946 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -418,6 +418,7 @@ module Combinators = struct let t_string ?s () : type_value = type_value (T_constant ("string", [])) s let t_bytes ?s () : type_value = type_value (T_constant ("bytes", [])) s let t_int ?s () : type_value = type_value (T_constant ("int", [])) s + let t_nat ?s () : type_value = type_value (T_constant ("nat", [])) s let t_unit ?s () : type_value = type_value (T_constant ("unit", [])) s let t_option o ?s () : type_value = type_value (T_constant ("option", [o])) s let t_tuple lst ?s () : type_value = type_value (T_tuple lst) s @@ -472,6 +473,10 @@ module Combinators = struct match t.type_value with | T_constant ("map", [k;v]) -> ok (k, v) | _ -> simple_fail "not a map" + let assert_t_map (t:type_value) : unit result = + match t.type_value with + | T_constant ("map", [_ ; _]) -> ok () + | _ -> simple_fail "not a map" let e_record map : expression = E_record map let ez_e_record (lst : (string * ae) list) : expression = @@ -485,12 +490,16 @@ module Combinators = struct let e_unit : expression = E_literal (Literal_unit) let e_int n : expression = E_literal (Literal_int n) + 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_a_unit = annotated_expression e_unit (t_unit ()) let e_a_int n = annotated_expression (e_int n) (t_int ()) + let e_a_nat n = annotated_expression (e_nat n) (t_nat ()) let e_a_bool b = annotated_expression (e_bool b) (t_bool ()) + let e_a_string s = annotated_expression (e_string s) (t_string ()) let e_a_pair a b = annotated_expression (e_pair a b) (t_pair a.type_annotation b.type_annotation ()) let e_a_some s = annotated_expression (e_some s) (t_option s.type_annotation ()) let e_a_none t = annotated_expression e_none (t_option t ()) diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo index b62cb73db..57677af95 100644 --- a/src/ligo/contracts/heap.ligo +++ b/src/ligo/contracts/heap.ligo @@ -1,9 +1,6 @@ -type heap_element is int * string +type heap_element is int * string ; -type heap is record - heap_content : map(int, heap_element) ; - heap_size : nat ; -end +type heap is map(int, heap_element) ; function is_empty (const h : heap) : bool is - block {skip} with h.heap_size = 0 + block {skip} with size(h) = 0n diff --git a/src/ligo/contracts/map.ligo b/src/ligo/contracts/map.ligo index 2bc9af8a6..1248c6c0c 100644 --- a/src/ligo/contracts/map.ligo +++ b/src/ligo/contracts/map.ligo @@ -1,5 +1,8 @@ type foobar is map(int, int) +function size_ (const m : foobar) : nat is + block {skip} with (size(m)) + function gf (const m : foobar) : int is begin skip end with get_force(23, m) const fb : foobar = map @@ -19,3 +22,4 @@ const bm : foobar = map 120 -> 23 ; 421 -> 23 ; end + diff --git a/src/ligo/dune b/src/ligo/dune index 9bca3a017..9a27a77b1 100644 --- a/src/ligo/dune +++ b/src/ligo/dune @@ -23,7 +23,12 @@ ) (alias - (name runtest) + (name ligo-test) (action (run test/test.exe)) (deps (glob_files contracts/*)) ) + +(alias + (name runtest) + (deps ligo-test) +) diff --git a/src/ligo/ligo_parser/AST.ml b/src/ligo/ligo_parser/AST.ml index 03c0af8d1..2e0659610 100644 --- a/src/ligo/ligo_parser/AST.ml +++ b/src/ligo/ligo_parser/AST.ml @@ -576,6 +576,7 @@ and arith_expr = | Mod of kwd_mod bin_op reg | Neg of minus un_op reg | Int of (Lexer.lexeme * Z.t) reg +| Nat of (Lexer.lexeme * Z.t) reg and string_expr = Cat of cat bin_op reg @@ -729,7 +730,8 @@ and arith_expr_to_region = function | Div {region; _} | Mod {region; _} | Neg {region; _} -| Int {region; _} -> region +| Int {region; _} +| Nat {region; _} -> region and string_expr_to_region = function Cat {region; _} @@ -1307,6 +1309,7 @@ and print_arith_expr = function | Neg {value = {op; arg}; _} -> print_token op "-"; print_expr arg | Int i -> print_int i +| Nat i -> print_int i and print_string_expr = function Cat {value = {arg1; op; arg2}; _} -> diff --git a/src/ligo/ligo_parser/AST.mli b/src/ligo/ligo_parser/AST.mli index 306ceb94d..39a0f08b3 100644 --- a/src/ligo/ligo_parser/AST.mli +++ b/src/ligo/ligo_parser/AST.mli @@ -560,6 +560,7 @@ and arith_expr = | Mod of kwd_mod bin_op reg | Neg of minus un_op reg | Int of (Lexer.lexeme * Z.t) reg +| Nat of (Lexer.lexeme * Z.t) reg and string_expr = Cat of cat bin_op reg diff --git a/src/ligo/ligo_parser/LexToken.mli b/src/ligo/ligo_parser/LexToken.mli index c4934962d..ebf887861 100644 --- a/src/ligo/ligo_parser/LexToken.mli +++ b/src/ligo/ligo_parser/LexToken.mli @@ -31,6 +31,7 @@ type t = String of lexeme Region.reg | Bytes of (lexeme * Hex.t) Region.reg | Int of (lexeme * Z.t) Region.reg +| Nat of (lexeme * Z.t) Region.reg | Ident of lexeme Region.reg | Constr of lexeme Region.reg @@ -141,6 +142,7 @@ type ident_err = Reserved_name val mk_string : lexeme -> Region.t -> token val mk_bytes : lexeme -> Region.t -> token val mk_int : lexeme -> Region.t -> (token, int_err) result +val mk_nat : lexeme -> Region.t -> (token, int_err) result val mk_ident : lexeme -> Region.t -> (token, ident_err) result val mk_constr : lexeme -> Region.t -> token val mk_sym : lexeme -> Region.t -> token diff --git a/src/ligo/ligo_parser/LexToken.mll b/src/ligo/ligo_parser/LexToken.mll index f8bcd91c5..1bc88a695 100644 --- a/src/ligo/ligo_parser/LexToken.mll +++ b/src/ligo/ligo_parser/LexToken.mll @@ -30,6 +30,7 @@ type t = String of lexeme Region.reg | Bytes of (lexeme * Hex.t) Region.reg | Int of (lexeme * Z.t) Region.reg +| Nat of (lexeme * Z.t) Region.reg | Ident of lexeme Region.reg | Constr of lexeme Region.reg @@ -154,6 +155,9 @@ let proj_token = function | Int Region.{region; value = s,n} -> region, sprintf "Int (\"%s\", %s)" s (Z.to_string n) +| Nat Region.{region; value = s,n} -> + region, sprintf "Nat (\"%s\", %s)" s (Z.to_string n) + | Ident Region.{region; value} -> region, sprintf "Ident \"%s\"" value @@ -249,6 +253,7 @@ let to_lexeme = function String s -> s.Region.value | Bytes b -> fst b.Region.value | Int i -> fst i.Region.value +| Nat i -> fst i.Region.value | Ident id | Constr id -> id.Region.value @@ -472,6 +477,15 @@ let mk_int lexeme region = then Error Non_canonical_zero else Ok (Int Region.{region; value = lexeme, z}) +let mk_nat lexeme region = + let z = + Str.(global_replace (regexp "_") "" lexeme) |> + Str.(global_replace (regexp "n") "") |> + Z.of_string in + if Z.equal z Z.zero && lexeme <> "0n" + then Error Non_canonical_zero + else Ok (Nat Region.{region; value = lexeme, z}) + let eof region = EOF region let mk_sym lexeme region = diff --git a/src/ligo/ligo_parser/Lexer.mli b/src/ligo/ligo_parser/Lexer.mli index fa0d3491b..fd03695ca 100644 --- a/src/ligo/ligo_parser/Lexer.mli +++ b/src/ligo/ligo_parser/Lexer.mli @@ -64,6 +64,7 @@ module type TOKEN = val mk_string : lexeme -> Region.t -> token val mk_bytes : lexeme -> Region.t -> token val mk_int : lexeme -> Region.t -> (token, int_err) result + val mk_nat : lexeme -> Region.t -> (token, int_err) result val mk_ident : lexeme -> Region.t -> (token, ident_err) result val mk_constr : lexeme -> Region.t -> token val mk_sym : lexeme -> Region.t -> token diff --git a/src/ligo/ligo_parser/Lexer.mll b/src/ligo/ligo_parser/Lexer.mll index c96bcf7bd..fa31208fd 100644 --- a/src/ligo/ligo_parser/Lexer.mll +++ b/src/ligo/ligo_parser/Lexer.mll @@ -106,6 +106,7 @@ module type TOKEN = val mk_string : lexeme -> Region.t -> token val mk_bytes : lexeme -> Region.t -> token val mk_int : lexeme -> Region.t -> (token, int_err) result + val mk_nat : lexeme -> Region.t -> (token, int_err) result val mk_ident : lexeme -> Region.t -> (token, ident_err) result val mk_constr : lexeme -> Region.t -> token val mk_sym : lexeme -> Region.t -> token @@ -417,6 +418,13 @@ module Make (Token: TOKEN) : (S with module Token = Token) = | Error Token.Non_canonical_zero -> fail region Non_canonical_zero + let mk_nat state buffer = + let region, lexeme, state = sync state buffer in + match Token.mk_nat lexeme region with + Ok token -> token, state + | Error Token.Non_canonical_zero -> + fail region Non_canonical_zero + let mk_ident state buffer = let region, lexeme, state = sync state buffer in match Token.mk_ident lexeme region with @@ -487,6 +495,7 @@ and scan state = parse | ident { mk_ident state lexbuf |> enqueue } | constr { mk_constr state lexbuf |> enqueue } | bytes { (mk_bytes seq) state lexbuf |> enqueue } +| integer 'n' { mk_nat state lexbuf |> enqueue } | integer { mk_int state lexbuf |> enqueue } | symbol { mk_sym state lexbuf |> enqueue } | eof { mk_eof state lexbuf |> enqueue } diff --git a/src/ligo/ligo_parser/ParToken.mly b/src/ligo/ligo_parser/ParToken.mly index dcddbcca7..651e072b8 100644 --- a/src/ligo/ligo_parser/ParToken.mly +++ b/src/ligo/ligo_parser/ParToken.mly @@ -8,6 +8,7 @@ %token String %token <(LexToken.lexeme * Hex.t) Region.reg> Bytes %token <(LexToken.lexeme * Z.t) Region.reg> Int +%token <(LexToken.lexeme * Z.t) Region.reg> Nat %token Ident %token Constr diff --git a/src/ligo/ligo_parser/Parser.mly b/src/ligo/ligo_parser/Parser.mly index 5dd547e6e..93ec6b386 100644 --- a/src/ligo/ligo_parser/Parser.mly +++ b/src/ligo/ligo_parser/Parser.mly @@ -954,6 +954,7 @@ unary_expr: core_expr: Int { EArith (Int $1) } +| Nat { EArith (Nat $1) } | var { EVar $1 } | String { EString (String $1) } | Bytes { EBytes $1 } diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml index 5b5bb7774..71c667dcf 100644 --- a/src/ligo/mini_c.ml +++ b/src/ligo/mini_c.ml @@ -661,6 +661,7 @@ module Translate_program = struct | "SOME" -> ok @@ simple_unary @@ prim I_SOME | "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some] | "GET" -> ok @@ simple_binary @@ prim I_GET + | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist" and translate_value (v:value) : michelson result = match v with @@ -1028,6 +1029,8 @@ module Translate_ir = struct ok @@ D_nat n | (Bool_t _), b -> ok @@ D_bool b + | (String_t _), s -> + ok @@ D_string s | (Unit_t _), () -> ok @@ D_unit | (Option_t _), None -> @@ -1050,7 +1053,21 @@ module Translate_ir = struct bind_map_list aux lst in ok @@ D_map lst' - | _ -> simple_fail "this value can't be transpiled back yet" + | ty, v -> + let%bind error = + let%bind m_data = + trace_tzresult_lwt (simple_error "unparsing unrecognized data") @@ + Tezos_utils.Memory_proto_alpha.unparse_michelson_data ty v in + let%bind m_ty = + trace_tzresult_lwt (simple_error "unparsing unrecognized data") @@ + Tezos_utils.Memory_proto_alpha.unparse_michelson_ty ty in + let error_content = + Format.asprintf "%a : %a" + Michelson.pp m_data + Michelson.pp m_ty in + ok @@ error "this value can't be transpiled back yet" error_content + in + fail error end @@ -1121,6 +1138,10 @@ module Combinators = struct | D_int n -> ok n | _ -> simple_fail "not an int" + let get_nat (v:value) = match v with + | D_nat n -> ok n + | _ -> simple_fail "not a nat" + let get_string (v:value) = match v with | D_string s -> ok s | _ -> simple_fail "not a string" @@ -1178,6 +1199,7 @@ module Combinators = struct aux b' let t_int : type_value = T_base Base_int + let t_nat : type_value = T_base Base_nat let quote binder input output body result : anon_function = let content : anon_function_content = { diff --git a/src/ligo/multifix/dune b/src/ligo/multifix/dune index 5cde1b385..6563a26a9 100644 --- a/src/ligo/multifix/dune +++ b/src/ligo/multifix/dune @@ -51,11 +51,3 @@ ) (modules generator) ) - -;; Tests - -(alias - (name runtest) - (deps generator.exe) - (action (system "./generator.exe parser ; ./generator.exe ast")) -) diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index 4f0c9439f..c11d95f43 100644 --- a/src/ligo/simplify.ml +++ b/src/ligo/simplify.ml @@ -12,6 +12,7 @@ let get_value : 'a Raw.reg -> 'a = fun x -> x.value let type_constants = [ ("unit", 0) ; + ("string", 0) ; ("nat", 0) ; ("int", 0) ; ("bool", 0) ; @@ -76,6 +77,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result let constants = [ ("get_force", 2) ; + ("size", 1) ; ] let rec simpl_expression (t:Raw.expr) : ae result = @@ -152,7 +154,10 @@ let rec simpl_expression (t:Raw.expr) : ae result = simpl_binop "ADD" c.value | EArith (Int n) -> let n = Z.to_int @@ snd @@ n.value in - ok @@ ae @@ E_literal (Literal_number n) + ok @@ ae @@ E_literal (Literal_int n) + | EArith (Nat n) -> + let n = Z.to_int @@ snd @@ n.value in + ok @@ ae @@ E_literal (Literal_nat n) | EArith _ -> simple_fail "arith: not supported yet" | EString (String s) -> ok @@ ae @@ E_literal (Literal_string s.value) diff --git a/src/ligo/test/heap_tests.ml b/src/ligo/test/heap_tests.ml index cff4972e6..7fcceb8e9 100644 --- a/src/ligo/test/heap_tests.ml +++ b/src/ligo/test/heap_tests.ml @@ -1,4 +1,4 @@ -open Ligo_helpers.Trace +open Trace open Ligo open Test_helpers @@ -12,38 +12,49 @@ let get_program = ok program ) -let a_heap content size = - let open AST_Typed.Combinators in - a_record_ez [ - ("content", content) ; - ("size", size) ; - ] let a_heap_ez ?value_type (content:(int * AST_Typed.ae) list) = let open AST_Typed.Combinators in let content = - let aux = fun (x, y) -> a_int x, y in + let aux = fun (x, y) -> e_a_int x, y in List.map aux content in let value_type = match value_type, content with | None, hd :: _ -> (snd hd).type_annotation | Some s, _ -> s | _ -> raise (Failure "no value type and heap empty when building heap") in - a_map content make_t_int value_type + e_a_map content (t_int ()) value_type + +let ez lst = + let open AST_Typed.Combinators in + let value_type = t_pair + (t_int ()) + (t_string ()) + () + in + let lst' = + let aux (i, (j, s)) = + (i, e_a_pair (e_a_int j) (e_a_string s)) in + List.map aux lst in + a_heap_ez ~value_type lst' + +let dummy n = + ez List.( + map (fun n -> (n, (n, string_of_int n))) @@ + range n + ) let is_empty () : unit result = let%bind program = get_program () in let aux n = let open AST_Typed.Combinators in - let input = a_int n in - let%bind result = easy_run_main_typed program input in - let%bind result' = - trace (simple_error "bad result") @@ - get_a_int result in - Assert.assert_equal_int (3 * n + 2) result' + let input = dummy n in + let%bind result = easy_run_typed "is_empty" program input in + let expected = e_a_bool (n = 0) in + AST_Typed.assert_value_eq (expected, result) in let%bind _ = bind_list @@ List.map aux - @@ [0 ; 2 ; 42 ; 163 ; -1] in + @@ [0 ; 2 ; 7 ; 12] in ok () diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index a9a8cfda0..98de49b44 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -193,6 +193,15 @@ let map () : unit result = in bind_map_list aux [0 ; 42 ; 51 ; 421 ; -3] in + let%bind _size = trace (simple_error "size") @@ + let aux n = + let input = ez List.(map (fun x -> (x, x)) @@ range n) in + let%bind result = easy_run_typed "size_" program input in + let expect = AST_Typed.Combinators.(e_a_nat n) in + AST_Typed.assert_value_eq (expect, result) + in + bind_map_list aux [1 ; 10 ; 3] + in let%bind _foobar = trace (simple_error "foobar") @@ let%bind result = easy_evaluate_typed "fb" program in let expect = ez [(23, 0) ; (42, 0)] in diff --git a/src/ligo/test/test.ml b/src/ligo/test/test.ml index 15e0f154e..6d1965d27 100644 --- a/src/ligo/test/test.ml +++ b/src/ligo/test/test.ml @@ -8,6 +8,6 @@ let () = Compiler_tests.main ; Transpiler_tests.main ; Typer_tests.main ; - (* Heap_tests.main ; *) + Heap_tests.main ; ] ; () diff --git a/src/ligo/test/typer_tests.ml b/src/ligo/test/typer_tests.ml index 74814bcef..038adfd8a 100644 --- a/src/ligo/test/typer_tests.ml +++ b/src/ligo/test/typer_tests.ml @@ -8,7 +8,7 @@ module Simplified = Ligo.AST_Simplified let int () : unit result = let open Combinators in - let pre = ae @@ e_number 32 in + let pre = ae @@ e_int 32 in let open Typer in let e = Environment.empty in let%bind post = type_annotated_expression e pre in @@ -33,7 +33,7 @@ module TestExpressions = struct module E = Typer.Environment.Combinators let unit () : unit result = test_expression I.(e_unit ()) O.(t_unit ()) - let int () : unit result = test_expression I.(e_number 32) O.(t_int ()) + let int () : unit result = test_expression I.(e_int 32) O.(t_int ()) let bool () : unit result = test_expression I.(e_bool true) O.(t_bool ()) let string () : unit result = test_expression I.(e_string "s") O.(t_string ()) let bytes () : unit result = test_expression I.(e_bytes "b") O.(t_bytes ()) @@ -45,7 +45,7 @@ module TestExpressions = struct let tuple () : unit result = test_expression - I.(ez_e_tuple [e_number 32; e_string "foo"]) + I.(ez_e_tuple [e_int 32; e_string "foo"]) O.(t_tuple [t_int (); t_string ()] ()) let constructor () : unit result = @@ -53,12 +53,12 @@ module TestExpressions = struct O.[("foo", t_int ()); ("bar", t_string ())] in test_expression ~env:(E.env_sum_type variant_foo_bar) - I.(e_constructor "foo" (ae @@ e_number 32)) + I.(e_constructor "foo" (ae @@ e_int 32)) O.(make_t_ez_sum variant_foo_bar) let record () : unit result = test_expression - I.(ez_e_record [("foo", e_number 32); ("bar", e_string "foo")]) + I.(ez_e_record [("foo", e_int 32); ("bar", e_string "foo")]) O.(make_t_ez_record [("foo", t_int ()); ("bar", t_string ())]) end diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index 692901034..3eee8671e 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -15,6 +15,7 @@ let rec translate_type (t:AST.type_value) : type_value result = match t.type_value with | T_constant ("bool", []) -> ok (T_base Base_bool) | T_constant ("int", []) -> ok (T_base Base_int) + | 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 ("map", [key;value]) -> @@ -405,6 +406,9 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression | T_constant ("int", []) -> let%bind n = get_int v in return (E_literal (Literal_int n)) + | T_constant ("nat", []) -> + let%bind n = get_nat v in + return (E_literal (Literal_nat n)) | T_constant ("string", []) -> let%bind n = get_string v in return (E_literal (Literal_string n)) diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 316cba95b..4bc014b8a 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -271,9 +271,12 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an | E_literal (Literal_bytes s) -> let%bind type_annotation = check (t_bytes ()) in ok O.{expression = E_literal (Literal_bytes s) ; type_annotation } - | E_literal (Literal_number n) -> + | E_literal (Literal_int n) -> let%bind type_annotation = check (t_int ()) in ok O.{expression = E_literal (Literal_int n) ; type_annotation } + | E_literal (Literal_nat n) -> + let%bind type_annotation = check (t_nat ()) in + ok O.{expression = E_literal (Literal_nat n) ; type_annotation } (* Tuple *) | E_tuple lst -> let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in @@ -407,7 +410,8 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt | "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", _ -> simple_fail "EQ only defined over int" + | "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" | "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 ()) @@ -425,6 +429,10 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt let%bind _ = O.assert_type_value_eq (src, i_ty) in ok ("GET_FORCE", dst) | "get_force", _ -> simple_fail "bad number of params to get_force" + | "size", [t] -> + let%bind () = assert_t_map t in + ok ("SIZE", t_nat ()) + | "size", _ -> simple_fail "bad number of params to size" | name, _ -> fail @@ unrecognized_constant name let untype_type_value (t:O.type_value) : (I.type_expression) result = @@ -437,8 +445,8 @@ let untype_literal (l:O.literal) : I.literal result = match l with | Literal_unit -> ok Literal_unit | Literal_bool b -> ok (Literal_bool b) - | Literal_nat n -> ok (Literal_number n) - | Literal_int n -> ok (Literal_number n) + | Literal_nat n -> ok (Literal_nat n) + | Literal_int n -> ok (Literal_int n) | Literal_string s -> ok (Literal_string s) | Literal_bytes b -> ok (Literal_bytes b)