more heaps

src/lib_utils/x_list.ml

@@ -29,7 +29,7 @@ let range n =
     then acc
     else aux ((n-1) :: acc) (n-1)
   in
-  List.rev (aux [] n)
+  aux [] n
 
 let find_map f lst =
   let rec aux = function

src/ligo/ast_simplified.ml

@@ -154,7 +154,7 @@ module PP = struct
     | E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m
     | E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
     | E_lambda {binder;input_type;output_type;result;body} ->
-        fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
+        fprintf ppf "lambda (%s:%a) : %a {@;  @[<v>%a@]@;} return %a"
           binder type_expression input_type type_expression output_type
           block body annotated_expression result
     | E_matching (ae, m) ->
@@ -179,7 +179,7 @@ module PP = struct
     | None -> fprintf ppf "%a" expression ae.expression
     | Some t -> fprintf ppf "(%a) : %a" expression ae.expression type_expression t
 
-  and block ppf (b:block) = (list_sep_d instruction) ppf b
+  and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
 
   and single_record_patch ppf ((p, ae) : string * ae) =
     fprintf ppf "%s <- %a" p annotated_expression ae
@@ -212,7 +212,7 @@ module PP = struct
         fprintf ppf "const %s = %a" name annotated_expression ae
 
   let program ppf (p:program) =
-    fprintf ppf "%a" (list_sep_d declaration) p
+    fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) p
 end
 
 module Rename = struct

src/ligo/ast_typed.ml

@@ -165,8 +165,8 @@ module PP = struct
 
   let rec annotated_expression ppf (ae:annotated_expression) : unit =
     match ae.type_annotation.simplified with
-    | Some _ -> fprintf ppf "%a:%a" expression ae.expression type_value ae.type_annotation
-    | _ -> expression ppf ae.expression
+    | Some _ -> fprintf ppf "@[<v>%a:%a@]" expression ae.expression type_value ae.type_annotation
+    | _ -> fprintf ppf "@[<v>%a@]" expression ae.expression
 
   and expression ppf (e:expression) : unit =
     match e with
@@ -175,15 +175,15 @@ module PP = struct
     | E_constructor (c, lst) -> fprintf ppf "%s(%a)" c annotated_expression lst
     | E_variable a -> fprintf ppf "%s" a
     | E_application (f, arg) -> fprintf ppf "(%a) (%a)" annotated_expression f annotated_expression arg
-    | E_tuple lst -> fprintf ppf "tuple[%a]" (list_sep_d annotated_expression) lst
     | E_lambda {binder;input_type;output_type;result;body} ->
         fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
           binder type_value input_type type_value output_type
           block body annotated_expression result
     | E_tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
     | E_record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
+    | E_tuple lst -> fprintf ppf "tuple[@;  @[<v>%a@]@;]" (list_sep annotated_expression (tag ",@;")) lst
     | E_record m -> fprintf ppf "record[%a]" (smap_sep_d annotated_expression) m
-    | E_map m -> fprintf ppf "map[%a]" (list_sep_d assoc_annotated_expression) m
+    | E_map m -> fprintf ppf "map[@;  @[<v>%a@]@;]" (list_sep assoc_annotated_expression (tag ",@;")) m
     | E_look_up (ds, i) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression i
     | E_matching (ae, m) ->
         fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
@@ -202,7 +202,7 @@ module PP = struct
     | Literal_string s -> fprintf ppf "%s" s
     | Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
 
-  and block ppf (b:block) = (list_sep_d instruction) ppf b
+  and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
 
   and single_record_patch ppf ((s, ae) : string * ae) =
     fprintf ppf "%s <- %a" s annotated_expression ae
@@ -224,7 +224,7 @@ module PP = struct
   and instruction ppf (i:instruction) = match i with
     | I_skip -> fprintf ppf "skip"
     | I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
-    | I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
+    | I_loop (cond, b) -> fprintf ppf "while (%a) {@;  @[<v>%a@]@;}" annotated_expression cond block b
     | I_assignment {name;annotated_expression = ae} ->
         fprintf ppf "%s := %a" name annotated_expression ae
     | I_matching (ae, m) ->
@@ -240,7 +240,7 @@ module PP = struct
         fprintf ppf "const %s = %a" name annotated_expression ae
 
   let program ppf (p:program) =
-    fprintf ppf "%a" (list_sep_d declaration) p
+    fprintf ppf "@[<v>%a@]" (list_sep declaration (tag "@;")) p
 
 end
 
@@ -507,6 +507,14 @@ module Combinators = struct
     | T_constant ("map", [_ ; _]) -> ok ()
     | _ -> simple_fail "not a map"
 
+  let assert_t_int : type_value -> unit result = fun t -> match t.type_value' with
+    | T_constant ("int", []) -> ok ()
+    | _ -> simple_fail "not an int"
+
+  let assert_t_nat : type_value -> unit result = fun t -> match t.type_value' with
+    | T_constant ("nat", []) -> ok ()
+    | _ -> simple_fail "not an nat"
+
   let e_record map : expression = E_record map
   let ez_e_record (lst : (string * ae) list) : expression =
     let aux prev (k, v) = SMap.add k v prev in

src/ligo/contracts/arithmetic.ligo

@@ -0,0 +1,8 @@
+function plus_op (const n : int) : int is
+  begin skip end with n + 42
+
+function times_op (const n : int) : int is
+  begin skip end with n * 42
+
+function int_op (const n : nat) : int is
+  block { skip } with int(n)

src/ligo/contracts/heap.ligo

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

src/ligo/mini_c.ml

@@ -836,6 +836,8 @@ module Translate_program = struct
     match s with
     | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
     | "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD
+    | "TIMES_INT" -> ok @@ simple_binary @@ prim I_MUL
+    | "TIMES_NAT" -> ok @@ simple_binary @@ prim I_MUL
     | "NEG" -> ok @@ simple_unary @@ prim I_NEG
     | "OR" -> ok @@ simple_binary @@ prim I_OR
     | "AND" -> ok @@ simple_binary @@ prim I_AND
@@ -849,6 +851,7 @@ module Translate_program = struct
     | "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
+    | "INT" -> ok @@ simple_unary @@ prim I_INT
     | "MAP_REMOVE" ->
         let%bind v = match lst with
           | [ _ ; (_, m, _) ] ->

src/ligo/simplify.ml

@@ -78,6 +78,7 @@ and simpl_list_type_expression (lst:Raw.type_expr list) : type_expression result
 let constants = [
   ("get_force", 2) ;
   ("size", 1) ;
+  ("int", 1) ;
 ]
 
 let rec simpl_expression (t:Raw.expr) : ae result =
@@ -152,6 +153,8 @@ let rec simpl_expression (t:Raw.expr) : ae result =
       ok @@ annotated_expression (E_constant ("NONE", [])) (Some (Combinators.t_option type_expr'))
   | EArith (Add c) ->
       simpl_binop "ADD" c.value
+  | EArith (Mult c) ->
+      simpl_binop "TIMES" c.value
   | EArith (Int n) ->
       let n = Z.to_int @@ snd @@ n.value in
       ok @@ ae @@ E_literal (Literal_int n)

src/ligo/test/heap_tests.ml

@@ -39,8 +39,9 @@ let ez lst =
 
 let dummy n =
   ez List.(
-    map (fun n -> (n, (n, string_of_int n))) @@
-    range n
+    map (fun n -> (n, (n, string_of_int n)))
+    @@ tl
+    @@ range (n + 1)
   )
 
 let is_empty () : unit result =
@@ -67,7 +68,7 @@ let get_top () : unit result =
     | 0, _ -> ok ()
     | _, result ->
         let%bind result' = result in
-        let expected = e_a_pair (e_a_int 0) (e_a_string "0") in
+        let expected = e_a_pair (e_a_int 1) (e_a_string "1") in
         AST_Typed.assert_value_eq (expected, result')
   in
   let%bind _ = bind_list
@@ -75,7 +76,51 @@ let get_top () : unit result =
     @@ [0 ; 2 ; 7 ; 12] in
   ok ()
 
+let pop_switch () : unit result =
+  let%bind program = get_program () in
+  let aux n =
+    let input = dummy n in
+    match n, easy_run_typed "pop_switch" program input with
+    | 0, Trace.Ok _ -> simple_fail "unexpected success"
+    | 0, _ -> ok ()
+    | _, result ->
+        let%bind result' = result in
+        let expected = ez List.(
+            map (fun i -> if i = 1 then (1, (n, string_of_int n)) else (i, (i, string_of_int i)))
+            @@ tl
+            @@ range (n + 1)
+          ) in
+        AST_Typed.assert_value_eq (expected, result')
+  in
+  let%bind _ = bind_list
+    @@ List.map aux
+    @@ [0 ; 2 ; 7 ; 12] in
+  ok ()
+
+(* let pop () : unit result =
+ *   let%bind program = get_program () in
+ *   let aux n =
+ *     let input = dummy n in
+ *     match n, easy_run_typed "pop" program input with
+ *     | 0, Trace.Ok _ -> simple_fail "unexpected success"
+ *     | 0, _ -> ok ()
+ *     | _, result ->
+ *         let%bind result' = result in
+ *         let expected = ez List.(
+ *             map (fun i -> if i = 1 then (1, (n, string_of_int n)) else (i, (i, string_of_int i)))
+ *             @@ tl
+ *             @@ range (n + 1)
+ *           ) in
+ *         AST_Typed.assert_value_eq (expected, result')
+ *   in
+ *   let%bind _ = bind_list
+ *     @@ List.map aux
+ *     @@ [0 ; 2 ; 7 ; 12] in
+ *   ok () *)
+
 let main = "Heap (End to End)", [
     test "is_empty" is_empty ;
     test "get_top" get_top ;
+    test "pop_switch" pop_switch ;
+    (* test "pop" pop ; *)
   ]

src/ligo/test/integration_tests.ml

@@ -67,6 +67,30 @@ let bool_expression () : unit result =
     ] in
   ok ()
 
+let arithmetic () : unit result =
+  let%bind program = type_file "./contracts/arithmetic.ligo" in
+  let aux (name, f) =
+    let aux n =
+      let open AST_Typed.Combinators in
+      let input = if name = "int_op" then e_a_nat n else e_a_int n in
+      let%bind result = easy_run_typed name program input in
+      AST_Typed.assert_value_eq (f n, result)
+    in
+    let%bind _ = bind_list
+      @@ List.map aux [0 ; 42 ; 128] in
+    ok ()
+  in
+  let%bind _ =
+    let open AST_Typed.Combinators in
+    bind_list
+    @@ List.map aux
+    @@ [
+      ("plus_op", fun n -> e_a_int (n + 42)) ;
+      ("times_op", fun n -> e_a_int (n * 42)) ;
+      (* ("int_op", fun n -> e_a_int n) ; *)
+    ] in
+  ok ()
+
 let unit_expression () : unit result =
   let%bind program = type_file "./contracts/unit.ligo" in
   let open AST_Typed.Combinators in
@@ -405,6 +429,7 @@ let main = "Integration (End to End)", [
     test "function" function_ ;
     test "complex function" complex_function ;
     test "bool" bool_expression ;
+    test "arithmetic" arithmetic ;
     test "unit" unit_expression ;
     test "record" record ;
     test "tuple" tuple ;

src/ligo/typer.ml

@@ -435,6 +435,10 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
   | "ADD", [a ; b] when type_value_eq (a, t_string ()) && type_value_eq (b, t_string ()) -> ok ("CONCAT", t_string ())
   | "ADD", [_ ; _] -> simple_fail "bad types to add"
   | "ADD", _ -> simple_fail "bad number of params to add"
+  | "TIMES", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("TIMES_INT", t_int ())
+  | "TIMES", [a ; b] when type_value_eq (a, t_nat ()) && type_value_eq (b, t_nat ()) -> ok ("TIMES_NAT", t_nat ())
+  | "TIMES", [_ ; _] -> simple_fail "bad types to TIMES"
+  | "TIMES", _ -> simple_fail "bad number of params to TIMES"
   | "EQ", [a ; b] when type_value_eq (a, t_int ()) && type_value_eq (b, t_int ()) -> ok ("EQ", t_bool ())
   | "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"
@@ -473,6 +477,10 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
       let%bind () = assert_t_map t in
       ok ("SIZE", t_nat ())
   | "size", _ -> simple_fail "bad number of params to size"
+  | "int", [t] ->
+      let%bind () = assert_t_nat t in
+      ok ("INT", t_int ())
+  | "int", _ -> simple_fail "bad number of params to int"
   | name, _ -> fail @@ unrecognized_constant name
 
 let untype_type_value (t:O.type_value) : (I.type_expression) result =