refactor little ; add error message

src/lib_utils/x_tezos_micheline.ml

@@ -38,8 +38,10 @@ module Michelson = struct
   let i_push ty code = prim ~children:[ty;code] I_PUSH
   let i_push_unit = i_push t_unit d_unit
   let i_none ty = prim ~children:[ty] I_NONE
+  let i_nil ty = prim ~children:[ty] I_NIL
   let i_some = prim I_SOME
   let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA
+  let i_empty_map src dst = prim ~children:[src;dst] I_EMPTY_MAP
   let i_drop = prim I_DROP
   let i_exec = prim I_EXEC
 

src/ligo/compiler/compiler_program.ml

@@ -26,6 +26,11 @@ let get_predicate : string -> expression list -> predicate result = fun s lst ->
       | x -> simple_fail ("predicate \"" ^ x ^ "\" doesn't exist")
     )
 
+let virtual_push = fun first m ->
+  match first with
+  | true -> m
+  | false -> seq [m ; i_pair]
+
 let rec translate_value (v:value) : michelson result = match v with
   | D_bool b -> ok @@ prim (if b then D_True else D_False)
   | D_int n -> ok @@ int (Z.of_int n)
@@ -51,9 +56,7 @@ let rec 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 -> a in
+      ok @@ seq lst'
-      (* 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 =
   let {capture_type } = content in
@@ -74,9 +77,11 @@ and translate_function ({capture;content}:anon_function) : michelson result =
       ok @@ d_pair capture_m body
   | _ -> simple_fail "compiling closure without capture"
 
-and translate_expression (expr:expression) : michelson result =
+and translate_expression ?(first=false) (expr:expression) : michelson result =
   let (expr' , ty , env) = Combinators.Expression.(get_content expr , get_type expr , get_environment expr) in
   let error_message () = Format.asprintf  "%a" PP.expression expr in
+  let virtual_push_first = virtual_push first in
+  let virtual_push = virtual_push false in
 
   let return code =
     let%bind (Ex_ty schema_ty) = Compiler_environment.to_ty env in
@@ -115,17 +120,14 @@ and translate_expression (expr:expression) : michelson result =
     | E_literal v ->
         let%bind v = translate_value v in
         let%bind t = Compiler_type.type_ ty in
-        return @@ seq [
+        return @@ virtual_push_first @@ i_push t v
-          prim ~children:[t;v] I_PUSH ;
-          prim I_PAIR ;
-        ]
     | E_application(f, arg) -> (
         match Combinators.Expression.get_type f with
         | T_function _ -> (
             trace (simple_error "Compiling quote application") @@
-            let%bind f = translate_expression f in
+            let%bind f = translate_expression ~first f in
             let%bind arg = translate_expression arg in
-            return @@ seq [
+            return @@ virtual_push @@ seq [
               i_comment "quote application" ;
               i_comment "get f" ;
               f ;
@@ -133,7 +135,6 @@ and translate_expression (expr:expression) : michelson result =
               arg ;
               i_unpair ; dip i_unpair ;
               prim I_EXEC ;
-              i_pair ;
             ]
           )
         | T_deep_closure (_small_env, _, _) -> (
@@ -141,7 +142,7 @@ and translate_expression (expr:expression) : michelson result =
           )
         | T_shallow_closure (_, _, _) -> (
             trace (simple_error "Compiling shallow closure application") @@
-            let%bind f' = translate_expression f in
+            let%bind f' = translate_expression ~first f in
             let%bind arg' = translate_expression arg in
             let error =
               let error_title () = "michelson type-checking closure application" in
@@ -154,50 +155,62 @@ and translate_expression (expr:expression) : michelson result =
               error error_title error_content
             in
             trace error @@
-            return @@ seq [
+            return @@ virtual_push @@ seq [
               i_comment "(* unit :: env *)" ;
-              i_comment "compute closure" ;
-              f' ;
-              i_comment "(* (closure * unit) :: env *)" ;
               i_comment "compute arg" ;
-              arg' ;
+              arg' ; i_unpair ;
-              i_comment "(* (arg * closure * unit) :: env *)" ;
+              i_comment "(* (arg * unit) :: env *)" ;
-              i_comment "separate stuff" ;
+              i_comment "compute closure" ;
-              i_unpair ; dip i_unpair ; dip i_unpair ;
+              dip @@ seq [f' ; i_unpair ; i_unpair] ;
               i_comment "(* arg :: capture :: f :: unit :: env *)" ;
               i_pair ;
               i_exec ; (* output :: stack :: env *)
-              i_pair ; (* stack :: env *)
             ]
+            (* return @@ virtual_push @@ seq [
+             *   i_comment "(\* unit :: env *\)" ;
+             *   i_comment "compute closure" ;
+             *   f' ;
+             *   i_comment "(\* (closure * unit) :: env *\)" ;
+             *   i_comment "compute arg" ;
+             *   arg' ;
+             *   i_comment "(\* (arg * closure * unit) :: env *\)" ;
+             *   i_comment "separate stuff" ;
+             *   i_unpair ; dip i_unpair ; dip i_unpair ;
+             *   i_comment "(\* arg :: capture :: f :: unit :: env *\)" ;
+             *   i_pair ;
+             *   i_exec ; (\* output :: stack :: env *\)
+             * ] *)
           )
         | _ -> simple_fail "E_applicationing something not appliable"
       )
     | E_variable x ->
         let%bind (get, _) = Compiler_environment.to_michelson_get env x in
-        return @@ seq [
+        return @@ virtual_push_first @@ seq [
-          dip (seq [prim I_DUP ; get]) ;
+          dip (seq [i_dup ; get]) ;
-          i_piar ;
+          i_swap ;
         ]
     | E_constant(str, lst) ->
-        let%bind lst' = bind_list @@ List.map translate_expression lst in
+        let%bind lst' =
+          let aux i e =
+            let first = first && i = 0 in
+            translate_expression ~first e in
+          bind_list @@ List.mapi aux lst in
         let%bind predicate = get_predicate str lst in
         let%bind code = match (predicate, List.length lst) with
-          | Constant c, 0 -> ok (seq @@ lst' @ [
+          | Constant c, 0 -> ok @@ virtual_push_first @@ seq @@ lst' @ [
-              c ; i_pair ;
+              c ;
-            ])
+            ]
-          | Unary f, 1 -> ok (seq @@ lst' @ [
+          | Unary f, 1 -> ok @@ virtual_push @@ seq @@ lst' @ [
               i_unpair ;
               f ;
-              i_pair ;
+            ]
-            ])
+          | Binary f, 2 -> ok @@ virtual_push @@ seq @@ lst' @ [
-          | Binary f, 2 -> ok (seq @@ lst' @ [
               i_unpair ;
               dip i_unpair ;
               i_swap ;
               f ;
-              i_pair ;
+            ]
-            ])
+          | Ternary f, 3 -> ok @@ virtual_push @@ seq @@ lst' @ [
-          | Ternary f, 3 -> ok (seq @@ lst' @ [
               i_unpair ;
               dip i_unpair ;
               dip (dip i_unpair) ;
@@ -205,59 +218,28 @@ and translate_expression (expr:expression) : michelson result =
               dip i_swap ;
               i_swap ;
               f ;
-              i_pair ;
+            ]
-            ])
           | _ -> simple_fail "bad arity"
         in
         return code
     | E_empty_map sd ->
         let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in
-        let code = seq [
+        return @@ virtual_push_first @@ i_empty_map src dst
-            prim ~children:[src;dst] I_EMPTY_MAP ;
-            i_pair ;
-          ] in
-        return code
     | E_empty_list t ->
         let%bind t' = Compiler_type.type_ t in
-        let code = seq [
+        return @@ virtual_push_first @@ i_nil t'
-            prim ~children:[t'] I_NIL ;
-            i_pair ;
-          ] in
-        return code
     | E_make_none o ->
         let%bind o' = Compiler_type.type_ o in
-        let code = seq [
+        return @@ virtual_push_first @@ i_none o'
-            prim ~children:[o'] I_NONE ;
-            i_pair ;
-          ] in
-        return code
     | E_function anon -> (
         match anon.capture_type with
         | No_capture ->
             let%bind body = translate_quote_body anon in
             let%bind input_type = Compiler_type.type_ anon.input in
             let%bind output_type = Compiler_type.type_ anon.output in
-            let code = seq [
+            let code = virtual_push_first @@ i_lambda input_type output_type body in
-                i_lambda input_type output_type body ;
-                i_pair ;
-              ] in
             return code
         | Deep_capture _small_env -> simple_fail "no deep capture expression yet"
-            (* (\* Capture the variable bounds, assemble them. On call, append the input. *\)
-             * let senv_type = Compiler_environment.Small.to_mini_c_type small_env in
-             * let%bind body = translate_closure_body anon senv_type in
-             * let%bind capture = Environment.Small.to_mini_c_capture env small_env in
-             * let%bind capture = translate_expression capture in
-             * let%bind input_type = Compiler_type.type_ anon.input in
-             * let%bind output_type = Compiler_type.type_ anon.output in
-             * let code = seq [
-             *     capture ;
-             *     i_unpair ;
-             *     i_lambda input_type output_type body ;
-             *     i_piar ;
-             *     i_pair ;
-             *   ] in
-             * return code *)
         | Shallow_capture env ->
             (* Capture the whole environment. *)
             let env_type = Compiler_environment.to_mini_c_type env in
@@ -266,7 +248,7 @@ and translate_expression (expr:expression) : michelson result =
               let input_type = Combinators.t_pair anon.input env_type in
               Compiler_type.type_ input_type in
             let%bind output_type = Compiler_type.type_ anon.output in
-            let code = seq [ (* stack :: env *)
+            let code = virtual_push_first @@ seq [ (* stack :: env *)
                 i_comment "env on top" ;
                 dip i_dup ; i_swap ; (* env :: stack :: env *)
                 i_comment "lambda" ;
@@ -274,7 +256,6 @@ and translate_expression (expr:expression) : michelson result =
                 i_comment "pair env + lambda" ;
                 i_piar ; (* (env * lambda) :: stack :: env *)
                 i_comment "new stack" ;
-                i_pair ; (* new_stack :: env *)
               ] in
             let error =
               let error_title () = "michelson type-checking trace" in

src/ligo/contracts/heap.ligo

@@ -1,18 +1,18 @@
-type heap is map(int, heap_element) ;
+type heap is map(nat, 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(1, h)
+  block {skip} with get_force(1n, h)
 
 function pop_switch (const h : heap) : heap is
   block {
    const result : heap_element = get_top (h) ;
    const s : nat = size(h) ;
-   const last : heap_element = get_force(int(s), h) ;
+   const last : heap_element = get_force(s, h) ;
-   remove 1 from map h ;
+   remove 1n from map h ;
-   h[1] := last ;
+   h[1n] := last ;
   } with h ;
 
 

src/ligo/test/heap_tests.ml

@@ -12,17 +12,16 @@ let get_program =
         ok program
       )
 
-
 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) -> e_a_int x, y in
+    let aux = fun (x, y) -> e_a_nat 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
-  e_a_map content (t_int ()) value_type
+  e_a_map content (t_nat ()) value_type
 
 let ez lst =
   let open AST_Typed.Combinators in

src/ligo/typer.ml

@@ -466,12 +466,21 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
     let l = List.length lst in
     trace_strong (wrong_arity name arity l) @@
     Assert.assert_true (arity = l) in
-  let aux = fun (predicate, typer') ->
+
-    match predicate lst with
+  let error =
-    | true -> typer' lst tv_opt
+    let title () = "typing: unrecognized constant" in
-    | false -> dummy_fail
+    let content () = name in
+    error title content in
+  let rec aux = fun ts ->
+    match ts with
+    | [] -> fail error
+    | (predicate, typer') :: tl -> (
+        match predicate lst with
+        | false -> aux tl
+        | true -> typer' lst tv_opt
+      )
   in
-  bind_find_map_list (simple_error "typing: unrecognized constant") aux typer
+  aux typer
 
 let untype_type_value (t:O.type_value) : (I.type_expression) result =
   match t.simplified with