non-atomic commit: refactor ; add Nat to lexer and parser ; improve multifix ; start heap tests

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

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

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)

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))

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 ())

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

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
+

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)
+)

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}; _} ->

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

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

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 =

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

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 }

src/ligo/ligo_parser/ParToken.mly

@@ -8,6 +8,7 @@
 %token           <LexToken.lexeme Region.reg> 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           <LexToken.lexeme Region.reg> Ident
 %token           <LexToken.lexeme Region.reg> Constr
 

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                    }

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 = {

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"))
-)

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)

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 ()
 
 

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

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 ;
   ] ;
   ()

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

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))

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)