From 6bca49fb8b96bc6ded642dafce740d559916443d Mon Sep 17 00:00:00 2001 From: Galfour Date: Wed, 10 Apr 2019 12:09:32 +0000 Subject: [PATCH] more heaps --- src/lib_utils/x_list.ml | 2 +- src/ligo/ast_simplified.ml | 6 ++-- src/ligo/ast_typed.ml | 22 +++++++++---- src/ligo/contracts/arithmetic.ligo | 8 +++++ src/ligo/contracts/heap.ligo | 19 +++++++++-- src/ligo/mini_c.ml | 3 ++ src/ligo/simplify.ml | 3 ++ src/ligo/test/heap_tests.ml | 51 ++++++++++++++++++++++++++++-- src/ligo/test/integration_tests.ml | 25 +++++++++++++++ src/ligo/typer.ml | 8 +++++ 10 files changed, 130 insertions(+), 17 deletions(-) create mode 100644 src/ligo/contracts/arithmetic.ligo diff --git a/src/lib_utils/x_list.ml b/src/lib_utils/x_list.ml index e269b4f01..d07a3592f 100644 --- a/src/lib_utils/x_list.ml +++ b/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 diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 428d74295..461097d6d 100644 --- a/src/ligo/ast_simplified.ml +++ b/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 {@; @[%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 "@[%a@]" (list_sep declaration (tag "@;")) p end module Rename = struct diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index a65cdbf11..129e6d4c5 100644 --- a/src/ligo/ast_typed.ml +++ b/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 "@[%a:%a@]" expression ae.expression type_value ae.type_annotation + | _ -> fprintf ppf "@[%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[@; @[%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[@; @[%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) {@; @[%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 "@[%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 diff --git a/src/ligo/contracts/arithmetic.ligo b/src/ligo/contracts/arithmetic.ligo new file mode 100644 index 000000000..e229115cb --- /dev/null +++ b/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) diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo index 36ff64629..82896d751 100644 --- a/src/ligo/contracts/heap.ligo +++ b/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 ; diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml index 87885d462..874ac6c79 100644 --- a/src/ligo/mini_c.ml +++ b/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, _) ] -> diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index e0bd62ac4..c3fed89f9 100644 --- a/src/ligo/simplify.ml +++ b/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) diff --git a/src/ligo/test/heap_tests.ml b/src/ligo/test/heap_tests.ml index 53a5a9989..9a8612bbe 100644 --- a/src/ligo/test/heap_tests.ml +++ b/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 ; *) ] diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index d39d67742..dd84c32d7 100644 --- a/src/ligo/test/integration_tests.ml +++ b/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 ; diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index af30fa8e9..9321ba89b 100644 --- a/src/ligo/typer.ml +++ b/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 =