added maps

This commit is contained in:
Galfour 2019-03-29 15:47:56 +00:00
parent c3c4473a0b
commit f5d9fa8266
11 changed files with 324 additions and 12 deletions

View File

@ -63,6 +63,8 @@ and expression =
(* Record *)
| Record of ae_map
| Accessor of ae * access_path
(* Data Structures *)
| Map of (ae * ae) list
and access =
| Tuple_access of int
@ -137,11 +139,15 @@ module PP = struct
| Tuple lst -> fprintf ppf "tuple[%a]" (list_sep annotated_expression) lst
| Accessor (ae, p) -> fprintf ppf "%a.%a" annotated_expression ae access_path p
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
| Lambda {binder;input_type;output_type;result;body} ->
fprintf ppf "lambda (%s:%a) : %a {%a} return %a"
binder type_expression input_type type_expression output_type
block body annotated_expression result
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and access ppf (a:access) =
match a with
| Tuple_access n -> fprintf ppf "%d" n
@ -300,6 +306,10 @@ module Rename = struct
let%bind sm' = bind_smap
@@ SMap.map (rename_annotated_expression r) sm in
ok (Record sm')
| Map m ->
let%bind m' = bind_map_list
(fun (x, y) -> bind_map_pair (rename_annotated_expression r) (x, y)) m in
ok (Map m')
end
end

View File

@ -64,8 +64,10 @@ and expression =
(* Record *)
| Record of ae_map
| Record_accessor of ae * string
(* Data Structures *)
| Map of (ae * ae) list
and value = annotated_expression (* BAD *)
and value = annotated_expression (* todo (for refactoring) *)
and literal =
| Unit
@ -105,6 +107,7 @@ open! Ligo_helpers.Trace
let type_value type_value simplified = { type_value ; simplified }
let annotated_expression expression type_annotation = { expression ; type_annotation }
let get_type_annotation x = x.type_annotation
let get_entry (p:program) (entry : string) : annotated_expression result =
let aux (d:declaration) =
@ -159,6 +162,10 @@ module PP = struct
| Tuple_accessor (ae, i) -> fprintf ppf "%a.%d" annotated_expression ae i
| Record_accessor (ae, s) -> fprintf ppf "%a.%s" annotated_expression ae s
| Record m -> fprintf ppf "record[%a]" (smap_sep annotated_expression) m
| Map m -> fprintf ppf "map[%a]" (list_sep assoc_annotated_expression) m
and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" annotated_expression a annotated_expression b
and literal ppf (l:literal) : unit =
match l with
@ -415,6 +422,9 @@ module Combinators = struct
let m = SMap.of_list lst in
make_t_record m
let t_map key value s = type_value (Type_constant ("map", [key ; value])) s
let make_t_map key value = t_map key value None
let t_sum m s : type_value = type_value (Type_sum m) s
let make_t_sum m = t_sum m None
let make_t_ez_sum (lst:(string * type_value) list) : type_value =
@ -452,12 +462,13 @@ module Combinators = struct
| _ -> simple_fail "not a record"
let record map : expression = Record map
let record_ez (lst : (string * ae) list) : expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
record map
let map lst : expression = Map lst
let unit : expression = Literal (Unit)
let int n : expression = Literal (Int n)
let bool b : expression = Literal (Bool b)
@ -469,6 +480,7 @@ module Combinators = struct
let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
let a_record r = annotated_expression (record r) (make_t_record (SMap.map (fun x -> x.type_annotation) r))
let a_record_ez r = annotated_expression (record_ez r) (make_t_record_ez (List.map (fun (x, y) -> x, y.type_annotation) r))
let a_map lst k v = annotated_expression (map lst) (make_t_map k v)
let get_a_int (t:annotated_expression) =
match t.expression with

View File

@ -1,4 +1,8 @@
type heap is record
heap_content : map(int, heap_element) ;
heap_size : nat ;
end
function is_empty (const h : heap) : bool is
block {skip} with h.heap_size = 0

View File

@ -114,6 +114,10 @@ let bind_and (a, b) =
b >>? fun b ->
ok (a, b)
let bind_pair = bind_and
let bind_map_pair f (a, b) =
bind_pair (f a, f b)
module AE = Tezos_utils.Memory_proto_alpha.Alpha_environment
module TP = Tezos_base__TzPervasives

View File

@ -247,6 +247,7 @@ module Types = struct
let nat = Nat_t None
let int = Int_t None
let nat_k = Nat_key None
let int_k = Int_key None
let big_map k v = Big_map_t (k, v, None)

View File

@ -15,7 +15,7 @@ type type_name = string
type type_base =
| Unit
| Bool
| Int | Nat | Float
| Int | Nat
| String | Bytes
type type_value = [
@ -25,6 +25,7 @@ type type_value = [
| `Deep_closure of environment_small * type_value * type_value
| `Shallow_closure of environment * type_value * type_value
| `Base of type_base
| `Map of type_value * type_value
]
and environment_element = string * type_value
@ -114,7 +115,6 @@ module PP = struct
| Unit -> fprintf ppf "unit"
| Bool -> fprintf ppf "bool"
| Int -> fprintf ppf "int"
| Float -> fprintf ppf "float"
| Nat -> fprintf ppf "nat"
| String -> fprintf ppf "string"
| Bytes -> fprintf ppf "bytes"
@ -124,6 +124,7 @@ module PP = struct
| `Pair(a, b) -> fprintf ppf "(%a) & (%a)" type_ a type_ b
| `Base b -> type_base ppf b
| `Function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b
| `Map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v
| `Shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b
| `Deep_closure(c, arg, ret) ->
fprintf ppf "[%a](%a)->(%a)"
@ -232,12 +233,40 @@ module Translate_type = struct
module Ty = struct
let base_type : type_base -> ex_ty result =
function
| Unit -> ok @@ Ex_ty Types.unit
| Bool -> ok @@ Ex_ty Types.bool
| Int -> ok @@ Ex_ty Types.int
| _ -> simple_fail "all based types not supported yet"
let not_comparable name = error "not a comparable type" name
let comparable_type_base : type_base -> ex_comparable_ty result = fun tb ->
let open Types in
let return x = ok @@ Ex_comparable_ty x in
match tb with
| Unit -> fail (not_comparable "unit")
| Bool -> fail (not_comparable "bool")
| Nat -> return nat_k
| Int -> return int_k
| String -> return string_k
| Bytes -> return bytes_k
let comparable_type : type_value -> ex_comparable_ty result = fun tv ->
match tv with
| `Base b -> comparable_type_base b
| `Deep_closure _ -> fail (not_comparable "deep closure")
| `Shallow_closure _ -> fail (not_comparable "shallow closure")
| `Function _ -> fail (not_comparable "function closure")
| `Or _ -> fail (not_comparable "or closure")
| `Pair _ -> fail (not_comparable "pair closure")
| `Map _ -> fail (not_comparable "map closure")
let base_type : type_base -> ex_ty result = fun b ->
let open Types in
let return x = ok @@ Ex_ty x in
match b with
| Unit -> return unit
| Bool -> return bool
| Int -> return int
| Nat -> return nat
| String -> return string
| Bytes -> return bytes
let rec type_ : type_value -> ex_ty result =
function
@ -266,6 +295,10 @@ module Translate_type = struct
let%bind (Ex_ty arg) = type_ arg in
let%bind (Ex_ty ret) = type_ ret in
ok @@ Ex_ty Types.(pair capture @@ lambda (pair capture arg) ret)
| `Map (k, v) ->
let%bind (Ex_comparable_ty k') = comparable_type k in
let%bind (Ex_ty v') = type_ v in
ok @@ Ex_ty Types.(map k' v')
and environment_small' = let open Append_tree in function
@ -294,7 +327,9 @@ module Translate_type = struct
| Unit -> ok @@ prim T_unit
| Bool -> ok @@ prim T_bool
| Int -> ok @@ prim T_int
| _ -> simple_fail "all based types not supported yet"
| Nat -> ok @@ prim T_nat
| String -> ok @@ prim T_string
| Bytes -> ok @@ prim T_bytes
let rec type_ : type_value -> michelson result =
function
@ -309,6 +344,9 @@ module Translate_type = struct
type_ t' >>? fun t' ->
ok @@ prim ~children:[t;t'] T_or
)
| `Map kv ->
let%bind (k', v') = bind_map_pair type_ kv in
ok @@ prim ~children:[k';v'] T_map
| `Function (arg, ret) ->
let%bind arg = type_ arg in
let%bind ret = type_ ret in
@ -1037,6 +1075,10 @@ module Combinators = struct
| `Pair (a, b) -> ok (a, b)
| _ -> simple_fail "not a type pair"
let get_t_map (t:type_value) = match t with
| `Map kv -> ok kv
| _ -> simple_fail "not a type map"
let get_left (v:value) = match v with
| `Left b -> ok b
| _ -> simple_fail "not a left"

199
src/ligo/test/heap_tests.ml Normal file
View File

@ -0,0 +1,199 @@
open Ligo_helpers.Trace
open Ligo
open Test_helpers
let get_program =
let s = ref None in
fun () -> match !s with
| Some s -> ok s
| None -> (
let%bind program = type_file "./contracts/heap.ligo" in
s := Some 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
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
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'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let bool_expression () : unit result =
let%bind program = type_file "./contracts/boolean_operators.ligo" in
let aux (name, f) =
let aux b =
let open AST_Typed.Combinators in
let input = a_bool b in
let%bind result = easy_run_typed name program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_bool result in
Assert.assert_equal_bool (f b) result'
in
let%bind _ = bind_list
@@ List.map aux [true;false] in
ok ()
in
let%bind _ = bind_list
@@ List.map aux
@@ [
("or_true", fun b -> b || true) ;
("or_false", fun b -> b || false) ;
("and_true", fun b -> b && true) ;
("and_false", fun b -> b && false) ;
] in
ok ()
let unit_expression () : unit result =
let%bind program = type_file "./contracts/unit.ligo" in
let open AST_Typed.Combinators in
let%bind result = easy_evaluate_typed "u" program in
let%bind () =
trace (simple_error "result isn't unit") @@
get_a_unit result in
ok ()
let record_ez_int names n =
let open AST_Typed.Combinators in
a_record_ez @@ List.map (fun x -> x, a_int n) names
let multiple_parameters () : unit result =
let%bind program = type_file "./contracts/multiple-parameters.ligo" in
let inputs = [0 ; 2 ; 42 ; 163 ; -1] in
let aux (name, input_f, output_f) =
let aux n =
let input = input_f n in
let%bind result = easy_run_typed name program input in
let%bind result' = AST_Typed.Combinators.get_a_int result in
let expected = output_f n in
let%bind _ = Assert.assert_equal_int expected result' in
ok ()
in
let%bind _ = bind_list @@ List.map aux inputs in
ok ()
in
let%bind _ = bind_list @@ List.map aux [
("ab", record_ez_int ["a";"b"], fun n -> 2 * n) ;
("abcd", record_ez_int ["a";"b";"c";"d"], fun n -> 4 * n + 2) ;
("abcde", record_ez_int ["a";"b";"c";"d";"e"], fun n -> 2 * n + 3) ;
] in
ok ()
let record () : unit result =
let%bind program = type_file "./contracts/record.ligo" in
let%bind _foobar =
let%bind result = easy_evaluate_typed "fb" program in
let expect = record_ez_int ["foo";"bar"] 0 in
AST_Typed.assert_value_eq (expect, result)
in
let%bind _projection =
let aux n =
let input = record_ez_int ["foo";"bar"] n in
let%bind result = easy_run_typed "projection" program input in
let expect = AST_Typed.Combinators.a_int (2 * n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_list @@ List.map aux [0 ; -42 ; 144]
in
let%bind _big =
let%bind result = easy_evaluate_typed "br" program in
let expect = record_ez_int ["a";"b";"c";"d";"e"] 23 in
AST_Typed.assert_value_eq (expect, result)
in
ok ()
let condition () : unit result =
let%bind program = type_file "./contracts/condition.ligo" 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 (if n = 2 then 42 else 0) result'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let declarations () : unit result =
let%bind program = type_file "./contracts/declarations.ligo" 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 (42 + n) result'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let quote_declaration () : unit result =
let%bind program = type_file "./contracts/quote-declaration.ligo" 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 result' (42 + 2 * n)
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let quote_declarations () : unit result =
let%bind program = type_file "./contracts/quote-declarations.ligo" 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 result' (74 + 2 * n)
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let main = "Heap (End to End)", [
test "is_empty" is_empty ;
]

View File

@ -189,7 +189,6 @@ let quote_declarations () : unit result =
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let main = "Integration (End to End)", [
test "basic" basic ;
test "function" function_ ;

View File

@ -7,5 +7,6 @@ let () =
Compiler_tests.main ;
Transpiler_tests.main ;
Typer_tests.main ;
Heap_tests.main ;
] ;
()

View File

@ -84,6 +84,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_expression) : expression result =
let%bind tv = translate_type ae.type_annotation in
let return (expr, tv) = ok (expr, tv, env) in
match ae.expression with
| Literal (Bool b) -> ok (Literal (`Bool b), tv, env)
| Literal (Int n) -> ok (Literal (`Int n), tv, env)
@ -198,6 +199,15 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in
ok (Predicate (name, lst'), tv, env)
| Lambda l -> translate_lambda env l tv
| Map m ->
let aux : expression result -> (AST.ae * AST.ae) -> expression result = fun prev kv ->
let%bind prev' = prev in
let%bind (k', v') = bind_map_pair (translate_annotated_expression env) kv in
return (Predicate ("UPDATE", [k' ; v' ; prev']), tv)
in
let init = return (Predicate ("EMPTY", []), tv) in
List.fold_left aux init m
and translate_lambda_shallow env l tv =
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in

View File

@ -317,6 +317,33 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
let%bind m' = bind_fold_smap aux (ok SMap.empty) m in
let%bind type_annotation = check @@ make_t_record (SMap.map get_annotation m') in
ok O.{expression = O.Record m' ; type_annotation }
(* Data-structure *)
| Map lst ->
let%bind lst' = bind_map_list (bind_map_pair (type_annotated_expression e)) lst in
let%bind type_annotation =
let aux opt c =
match opt with
| None -> ok (Some c)
| Some c' ->
let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
ok (Some c') in
let%bind key_type =
let%bind opt =
bind_fold_list aux None
@@ List.map Ast_typed.get_type_annotation
@@ List.map fst lst' in
trace_option (simple_error "empty map expression") opt
in
let%bind value_type =
let%bind opt =
bind_fold_list aux None
@@ List.map Ast_typed.get_type_annotation
@@ List.map snd lst' in
trace_option (simple_error "empty map expression") opt
in
check (make_t_map key_type value_type)
in
ok O.{expression = O.Map lst' ; type_annotation}
| Lambda {
binder ;
input_type ;
@ -420,6 +447,9 @@ let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_ex
| Record_accessor (r, s) ->
let%bind r' = untype_annotated_expression r in
return (Accessor (r', [Record_access s]))
| Map m ->
let%bind m' = bind_map_list (bind_map_pair untype_annotated_expression) m in
return (Map m')
and untype_block (b:O.block) : (I.block) result =
bind_list @@ List.map untype_instruction b