From 6eda849ce962f3fd40836416e6c8d7c9ab7ff8e1 Mon Sep 17 00:00:00 2001 From: Benjamin Canou Date: Mon, 14 Nov 2016 18:09:06 +0100 Subject: [PATCH] Proto: drop imperative constructs and instructions from the language. --- src/proto/bootstrap/docs/json-notations.md | 8 - src/proto/bootstrap/docs/language.md | 82 +------- src/proto/bootstrap/script_interpreter.ml | 105 +++------- src/proto/bootstrap/script_ir_translator.ml | 221 ++++++++++++-------- src/proto/bootstrap/script_typed_ir.ml | 63 +++--- 5 files changed, 208 insertions(+), 271 deletions(-) diff --git a/src/proto/bootstrap/docs/json-notations.md b/src/proto/bootstrap/docs/json-notations.md index 334c60d04..ede2933e9 100644 --- a/src/proto/bootstrap/docs/json-notations.md +++ b/src/proto/bootstrap/docs/json-notations.md @@ -102,8 +102,6 @@ with the following JSON script description. | { "left": [ /* tagged data */, /* type */ ] } | { "right": [ /* type */, /* tagged data */ ] } | { "or": [ /* type */, /* type */, /* untagged data */ ] } - | { "ref": [ /* tagged data */ ] } - | { "ref": [ /* type */, /* untagged data */ ] } | { "some": [ /* tagged data */ ] } | { "some": [ /* type */, /* untagged data */ ] } | { "none": [ /* type */ ] } @@ -135,7 +133,6 @@ with the following JSON script description. | { "pair": [ /* untagged data */, /* untagged data */ ] } | { "left": [ /* untagged data */ ] } | { "right": [ /* untagged data */ ] } - | { "ref": [ /* untagged data */ ] } | { "some": [ /* untagged data */ ] } | "none" | { "list": [ /* untagged data */ ... ] } @@ -161,15 +158,11 @@ with the following JSON script description. | { "if_cons": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } | { "empty_set": [ /* type */ ] } | { "empty_map": [ /* comparable type */, /* type */ ] } - | "iter" | "map" | "reduce" | "mem" | "get" | "update" - | "ref" - | "deref" - | "set" | { "if": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } | { "loop": [ [ /* instruction */ ... ] ] } | { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] } @@ -239,7 +232,6 @@ with the following JSON script description. | "key" | "timestamp" | "signature" - | { "ref": [ /* type */ ] } | { "option": [ /* type */ ] } | { "list": [ /* type */ ] } | { "set": [ /* comparable type */ ] } diff --git a/src/proto/bootstrap/docs/language.md b/src/proto/bootstrap/docs/language.md index 2ff123edc..5b0acf825 100644 --- a/src/proto/bootstrap/docs/language.md +++ b/src/proto/bootstrap/docs/language.md @@ -291,11 +291,8 @@ IV - Data types A union of two types, a value holding either a value a of type 'a or a value b of type 'b, that we write (Left a) or (Right b). - * `ref 'a`: - Classical imperative stores, that we note (Ref const). - * `set 'a`, `map 'a 'b`: - Imperative map and sets, optimized in the db. + Immutable map and sets. V - Operations @@ -559,49 +556,10 @@ constants as is, concatenate them and use them as keys. > CD(\rest)R ; C / S => CDR ; C(\rest)R ; C / S > CR ; C / S => C / S -### Operations on refs - - * `REF`: - Build a ref from its initial contents. - - :: 'a : 'S -> ref 'a : 'S - - > REF ; C / a : S / M => C / l : S / l = (Ref a), M - - * `DEREF`: - Access the contents of a ref. - - :: ref 'a : 'S -> 'a : 'S - - > DEREF ; C / l : S / l = (Ref a), M => C / a : S / l = (Ref a), M - - * `SET` - Update the contents of a ref. - - :: 'a : ref 'a : 'S -> 'S - - > SET ; C / v :: l : S / l = (Ref _), M => C / S / l = (Ref v), M - - * `INCR step`: - Increments a counter. - - :: ref 'a : 'S -> 'S - iff step :: 'a, operator ADD defined on 'a - - > INCR step ; C / l : S / M => DUP ; DEREF ; PUSH step ; ADD ; Set ; C / S / M - - * `DECR step`: - Decrements a counter. - - :: ref 'a : 'S -> 'S - iff step :: 'a, operator SUB defined on 'a - - > DECR step ; C / l : S / M => DUP ; DEREF ; PUSH step ; SUB ; Set ; C / S / M - ### Operations on sets * `EMPTY_SET 'elt`: - Build a new, empty imperative set for elements of a given type. + Build a new, empty set for elements of a given type. :: 'S -> set 'elt : 'S @@ -616,12 +574,7 @@ constants as is, concatenate them and use them as keys. * `UPDATE`: Inserts or removes an element in a set, replacing a previous value. - :: 'elt : bool : set 'elt : 'S -> 'S - - * `ITER`: - Apply an imperative function over all the elements of a set. - - :: lambda 'elt void : set 'elt : 'S -> 'S + :: 'elt : bool : set 'elt : 'S -> set 'elt : 'S * `REDUCE`: Apply a function on a set passing the result of each @@ -632,7 +585,7 @@ constants as is, concatenate them and use them as keys. ### Operations on maps * `EMPTY_MAP 'key 'val`: - Build a new, empty imperative map. + Build a new, empty map. The `'key` type must be comparable (the `COMPARE` primitive must be defined over it). @@ -653,12 +606,7 @@ constants as is, concatenate them and use them as keys. * `UPDATE`: Assign or remove an element in a map. - :: 'key : option 'val : map 'key 'val : 'S -> 'S - - * `ITER`: - Apply an imperative function over all the bindings of a map. - - :: lambda (pair 'key 'val) void : map 'key 'val : 'S -> 'S + :: 'key : option 'val : map 'key 'val : 'S -> map 'key 'val : 'S * `MAP`: Apply a function on a map and return the map of results under @@ -750,11 +698,6 @@ constants as is, concatenate them and use them as keys. > IF_CONS ; C / (Cons a rest) : S => bt ; C / a : rest : S > IF_CONS ; C / Nil : S => bf ; C / S - * `ITER`: - Apply a function on a list from left to right. - - :: lambda 'a void : list 'a : 'S -> 'S - * `MAP`: Apply a function on a list from left to right and return the list of results in the same order. @@ -1191,10 +1134,7 @@ data. For this, the code of the contract is checked to be of the following type lambda (pair (pair tez 'arg) 'global) -> (pair 'ret 'global) where 'global is the type of the original global store given on origination. The contract also takes a parameter and an amount, and -returns a value, hence the complete calling convention above. The -global values can be updated either by rewriting the object, or by -putting mutable values in it and performing side effects on them, -allowing both imperative and functional style. +returns a value, hence the complete calling convention above. ### Empty contract @@ -1564,8 +1504,6 @@ X - Full grammar | Left | Right | Or - | Ref - | Ref | Some | Some | None @@ -1591,7 +1529,6 @@ X - Full grammar | Pair | Left | Right - | Ref | Some | None | List ... @@ -1617,15 +1554,11 @@ X - Full grammar | IF_CONS { ... } { ... } | EMPTY_SET | EMPTY_MAP - | ITER | MAP | REDUCE | MEM | GET | UPDATE - | REF - | DEREF - | SET | IF { ... } { ... } | LOOP { ... } | LAMBDA { ... } @@ -1694,7 +1627,6 @@ X - Full grammar | key | timestamp | signature - | ref | option | list | set @@ -1757,7 +1689,7 @@ The language is implemented in OCaml as follows: well-typed, corresponding GADT expressions. It is mostly a checker, not a full inferer, and thus takes some annotations (basically the inpout and output of the program, of lambdas and of - uninitialized imperative structures). It works by performing a + uninitialized maps and sets). It works by performing a symbolic evaluation of the program, transforming a symbolic stack. It only needs one pass over the whole program. diff --git a/src/proto/bootstrap/script_interpreter.ml b/src/proto/bootstrap/script_interpreter.ml index d7b3ac8af..5e2163527 100644 --- a/src/proto/bootstrap/script_interpreter.ml +++ b/src/proto/bootstrap/script_interpreter.ml @@ -65,16 +65,6 @@ type 'tys stack = | Item : 'ty * 'rest stack -> ('ty * 'rest) stack | Empty : end_of_stack stack -let eq_comparable - : type a. a comparable_ty -> a -> a -> bool - = fun kind x v -> match kind with - | String_key -> Compare.String.(x = v) - | Bool_key -> Compare.Bool.(x = v) - | Tez_key -> Tez.(x = v) - | Key_key -> Ed25519.Public_key_hash.(equal x v) - | Int_key kind -> Script_int.(equal kind x v) - | Timestamp_key -> Timestamp.(x = v) - let rec interp : type p r. int -> Contract.t -> Contract.t -> Tez.t -> @@ -131,11 +121,6 @@ let rec interp step qta ctxt bf rest | If_cons (bt, _), Item (hd :: tl, rest) -> step qta ctxt bt (Item (hd, Item (tl, rest))) - | List_iter, Item (lam, Item (l, rest)) -> - fold_left_s (fun ((), qta, ctxt) arg -> - interp qta orig source amount ctxt lam arg) - ((), qta, ctxt) l >>=? fun ((), qta, ctxt) -> - return (rest, qta, ctxt) | List_map, Item (lam, Item (l, rest)) -> fold_left_s (fun (tail, qta, ctxt) arg -> interp qta orig source amount ctxt lam arg @@ -153,82 +138,60 @@ let rec interp return (Item (res, rest), qta, ctxt) (* sets *) | Empty_set t, rest -> - return (Item ((ref [], t), rest), qta - 1, ctxt) - | Set_iter, Item (lam, Item ((l, _), rest)) -> - fold_left_s (fun ((), qta, ctxt) arg -> - interp qta orig source amount ctxt lam arg) - ((), qta, ctxt) !l >>=? fun ((), qta, ctxt) -> - return (rest, qta, ctxt) - | Set_map t, Item (lam, Item ((l, _), rest)) -> + return (Item (empty_set t, rest), qta - 1, ctxt) + | Set_map t, Item (lam, Item (set, rest)) -> + let items = + List.rev (set_fold (fun e acc -> e :: acc) set []) in fold_left_s - (fun (tail, qta, ctxt) arg -> + (fun (res, qta, ctxt) arg -> interp qta orig source amount ctxt lam arg >>=? fun (ret, qta, ctxt) -> - return (ret :: tail, qta, ctxt)) - ([], qta, ctxt) !l >>=? fun (res, qta, ctxt) -> - return (Item ((ref res, t), rest), qta, ctxt) - | Set_reduce, Item (lam, Item ((l, _), Item (init, rest))) -> + return (set_update ret true res, qta, ctxt)) + (empty_set t, qta, ctxt) items >>=? fun (res, qta, ctxt) -> + return (Item (res, rest), qta, ctxt) + | Set_reduce, Item (lam, Item (set, Item (init, rest))) -> + let items = + List.rev (set_fold (fun e acc -> e :: acc) set []) in fold_left_s (fun (partial, qta, ctxt) arg -> interp qta orig source amount ctxt lam (arg, partial) >>=? fun (partial, qta, ctxt) -> return (partial, qta, ctxt)) - (init, qta, ctxt) !l >>=? fun (res, qta, ctxt) -> + (init, qta, ctxt) items >>=? fun (res, qta, ctxt) -> return (Item (res, rest), qta, ctxt) - | Set_mem, Item (v, Item ((l, kind), rest)) -> - return (Item (List.exists (eq_comparable kind v) !l, rest), qta - 1, ctxt) - | Set_update, Item (v, Item (false, Item ((l, kind), rest))) -> - l := List.filter (fun x -> not (eq_comparable kind x v)) !l ; - return (rest, qta - 1, ctxt) - | Set_update, Item (v, Item (true, Item ((l, kind), rest))) -> - l := v :: List.filter (fun x -> not (eq_comparable kind x v)) !l ; - return (rest, qta - 1, ctxt) + | Set_mem, Item (v, Item (set, rest)) -> + return (Item (set_mem v set, rest), qta - 1, ctxt) + | Set_update, Item (v, Item (presence, Item (set, rest))) -> + return (Item (set_update v presence set, rest), qta - 1, ctxt) (* maps *) | Empty_map (t, _), rest -> - return (Item ((ref [], t), rest), qta - 1, ctxt) - | Map_iter, Item (lam, Item ((l, _), rest)) -> + return (Item (empty_map t, rest), qta - 1, ctxt) + | Map_map, Item (lam, Item (map, rest)) -> + let items = + List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in fold_left_s - (fun ((), qta, ctxt) arg -> interp qta orig source amount ctxt lam arg) - ((), qta, ctxt) !l >>=? fun ((), qta, ctxt) -> - return (rest, qta, ctxt) - | Map_map, Item (lam, Item ((l, t), rest)) -> - fold_left_s - (fun (tail, qta, ctxt) (k, v) -> + (fun (acc, qta, ctxt) (k, v) -> interp qta orig source amount ctxt lam (k, v) >>=? fun (ret, qta, ctxt) -> - return ((k, ret) :: tail, qta, ctxt)) - ([], qta, ctxt) !l >>=? fun (res, qta, ctxt) -> - return (Item ((ref res, t), rest), qta, ctxt) - | Map_reduce, Item (lam, Item ((l, _), Item (init, rest))) -> + return (map_update k (Some ret) acc, qta, ctxt)) + (empty_map (map_key_ty map), qta, ctxt) items >>=? fun (res, qta, ctxt) -> + return (Item (res, rest), qta, ctxt) + | Map_reduce, Item (lam, Item (map, Item (init, rest))) -> + let items = + List.rev (map_fold (fun k v acc -> (k, v) :: acc) map []) in fold_left_s (fun (partial, qta, ctxt) arg -> interp qta orig source amount ctxt lam (arg, partial) >>=? fun (partial, qta, ctxt) -> return (partial, qta, ctxt)) - (init, qta, ctxt) !l >>=? fun (res, qta, ctxt) -> + (init, qta, ctxt) items >>=? fun (res, qta, ctxt) -> return (Item (res, rest), qta, ctxt) - | Map_mem, Item (v, Item ((l, kind), rest)) -> - let res = List.exists (fun (k, _) -> eq_comparable kind k v) !l in - return (Item (res, rest), qta - 1, ctxt) - | Map_get, Item (v, Item ((l, kind), rest)) -> - let res = - try Some (snd (List.find (fun (k, _) -> eq_comparable kind k v) !l)) - with Not_found -> None in - return (Item (res, rest), qta - 1, ctxt) - | Map_update, Item (vk, Item (None, Item ((l, kind), rest))) -> - l := List.filter (fun (k, _) -> not (eq_comparable kind k vk)) !l ; - return (rest, qta - 1, ctxt) - | Map_update, Item (vk, Item (Some v, Item ((l, kind), rest))) -> - l := (vk, v) :: List.filter (fun (k, _) -> not (eq_comparable kind k vk)) !l ; - return (rest, qta - 1, ctxt) - (* reference cells *) - | Ref, Item (v, rest) -> - return (Item (ref v, rest), qta - 1, ctxt) - | Deref, Item ({ contents = v}, rest) -> - return (Item (v, rest), qta - 1, ctxt) - | Set, Item (r, Item (v, rest)) -> - r := v ; - return (rest, qta - 1, ctxt) + | Map_mem, Item (v, Item (map, rest)) -> + return (Item (map_mem v map, rest), qta - 1, ctxt) + | Map_get, Item (v, Item (map, rest)) -> + return (Item (map_get v map, rest), qta - 1, ctxt) + | Map_update, Item (k, Item (v, Item (map, rest))) -> + return (Item (map_update k v map, rest), qta - 1, ctxt) (* timestamp operations *) | Add_seconds_to_timestamp (kind, _pos), Item (n, Item (t, rest)) -> let n = Script_int.to_int64 kind n in diff --git a/src/proto/bootstrap/script_ir_translator.ml b/src/proto/bootstrap/script_ir_translator.ml index 0e76501b4..17753a525 100644 --- a/src/proto/bootstrap/script_ir_translator.ml +++ b/src/proto/bootstrap/script_ir_translator.ml @@ -155,10 +155,6 @@ let rec ty_eq ty_eq tar tbr >>? fun (Eq _) -> (eq ta tb : (ta ty, tb ty) eq tzresult)) |> record_trace (Inconsistent_types (Ty ta, Ty tb)) - | Ref_t tva, Ref_t tvb -> - (ty_eq tva tvb >>? fun (Eq _) -> - (eq ta tb : (ta ty, tb ty) eq tzresult)) |> - record_trace (Inconsistent_types (Ty ta, Ty tb)) | Option_t tva, Option_t tvb -> (ty_eq tva tvb >>? fun (Eq _) -> (eq ta tb : (ta ty, tb ty) eq tzresult)) |> @@ -181,6 +177,108 @@ let rec stack_ty_eq | Empty_t, Empty_t -> eq ta tb | _, _ -> error Inconsistent_stack_lengths +(* ---- Sets and Maps -------------------------------------------------------*) + +let compare_comparable + : type a. a comparable_ty -> a -> a -> int + = fun kind x y -> match kind with + | String_key -> Compare.String.compare x y + | Bool_key -> Compare.Bool.compare x y + | Tez_key -> Tez.compare x y + | Key_key -> Ed25519.Public_key_hash.compare x y + | Int_key kind -> + let res = + Script_int.to_int64 Script_int.Int64 + (Script_int.compare kind x y) in + if Compare.Int64.(res = 0L) then 0 + else if Compare.Int64.(res > 0L) then 1 + else -1 + | Timestamp_key -> Timestamp.compare x y + +let empty_set + : type a. a comparable_ty -> a set + = fun ty -> + let module OPS = Set.Make (struct + type t = a + let compare = compare_comparable ty + end) in + (module struct + type elt = a + module OPS = OPS + let boxed = OPS.empty + end) + +let set_update + : type a. a -> bool -> a set -> a set + = fun v b (module Box) -> + (module struct + type elt = a + module OPS = Box.OPS + let boxed = + if b then + Box.OPS.add v Box.boxed + else + Box.OPS.remove v Box.boxed + end) + +let set_mem + : type elt. elt -> elt set -> bool + = fun v (module Box) -> + Box.OPS.mem v Box.boxed + +let set_fold + : type elt acc. (elt -> acc -> acc) -> elt set -> acc -> acc + = fun f (module Box) -> + Box.OPS.fold f Box.boxed + +let map_key_ty + : type a b. (a, b) map -> a comparable_ty + = fun (module Box) -> Box.key_ty + +let empty_map + : type a b. a comparable_ty -> (a, b) map + = fun ty -> + let module OPS = Map.Make (struct + type t = a + let compare = compare_comparable ty + end) in + (module struct + type key = a + type value = b + let key_ty = ty + module OPS = OPS + let boxed = OPS.empty + end) + +let map_get + : type key value. key -> (key, value) map -> value option + = fun k (module Box) -> + try Some (Box.OPS.find k Box.boxed) with Not_found -> None + +let map_update + : type a b. a -> b option -> (a, b) map -> (a, b) map + = fun k v (module Box) -> + (module struct + type key = a + type value = b + let key_ty = Box.key_ty + module OPS = Box.OPS + let boxed = + match v with + | Some v -> Box.OPS.add k v Box.boxed + | None -> Box.OPS.remove k Box.boxed + end) + +let map_mem + : type key value. key -> (key, value) map -> bool + = fun k (module Box) -> + Box.OPS.mem k Box.boxed + +let map_fold + : type key value acc. (key -> value -> acc -> acc) -> (key, value) map -> acc -> acc + = fun f (module Box) -> + Box.OPS.fold f Box.boxed + (* ---- Type checker resuls -------------------------------------------------*) type 'bef judgement = @@ -276,9 +374,6 @@ let rec parse_ty : Script.expr -> ex_ty tzresult Lwt.t = function parse_ty uta >>=? fun (Ex ta) -> parse_ty utr >>=? fun (Ex tr) -> return @@ Ex (Lambda_t (ta, tr)) - | Prim (_, "ref", [ ut ]) -> - parse_ty ut >>=? fun (Ex t) -> - return @@ Ex (Ref_t t) | Prim (_, "option", [ ut ]) -> parse_ty ut >>=? fun (Ex t) -> return @@ Ex (Option_t t) @@ -433,15 +528,6 @@ let rec parse_tagged_data return @@ Ex (Union_t (tl, tr), v) | Prim (loc, "or", l) -> fail @@ Invalid_arity (loc, Constant, "or", 3, List.length l) - | Prim (_, "ref", [ r ]) -> - parse_tagged_data ctxt r >>=? fun (Ex (tr, r)) -> - return @@ Ex (Ref_t tr, ref r) - | Prim (_, "ref", [ tr; r ]) -> - parse_ty tr >>=? fun (Ex tr) -> - parse_untagged_data ctxt tr r >>=? fun r -> - return @@ Ex (Ref_t tr, ref r) - | Prim (loc, "ref", l) -> - fail @@ Invalid_arity (loc, Constant, "ref", 1, List.length l) | Prim (_, "some", [ r ]) -> parse_tagged_data ctxt r >>=? fun (Ex (tr, r)) -> return @@ Ex (Option_t tr, Some r) @@ -621,14 +707,6 @@ and parse_untagged_data parse_lambda ctxt ta tr script_instr | Lambda_t (_, _), (Prim (loc, _, _) | Int (loc, _) | String (loc, _)) -> fail @@ Invalid_constant (loc, "lambda") - (* References *) - | Ref_t t, Prim (_, "ref", [ v ]) -> - parse_untagged_data ctxt t v >>=? fun v -> - return (ref v) - | Ref_t _, Prim (loc, "ref", l) -> - fail @@ Invalid_arity (loc, Constant, "ref", 1, List.length l) - | Ref_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) -> - fail @@ Invalid_constant (loc, "ref") (* Options *) | Option_t t, Prim (_, "some", [ v ]) -> parse_untagged_data ctxt t v >>=? fun v -> @@ -653,27 +731,25 @@ and parse_untagged_data (* Sets *) | Set_t t, Prim (_, "set", vs) -> fold_left_s - (fun rest v -> + (fun acc v -> parse_untagged_comparable_data ctxt t v >>=? fun v -> - return (v :: rest)) - [] vs >>=? fun v -> - return (ref v, t) + return (set_update v true acc)) + (empty_set t) vs | Set_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) -> fail @@ Invalid_constant (loc, "set") (* Maps *) | Map_t (tk, tv), Prim (_, "map", vs) -> fold_left_s - (fun rest -> function + (fun acc -> function | Prim (_, "item", [ k; v ]) -> parse_untagged_comparable_data ctxt tk k >>=? fun k -> parse_untagged_data ctxt tv v >>=? fun v -> - return ((k, v) :: rest) + return (map_update k (Some v) acc) | Prim (loc, "item", l) -> fail @@ Invalid_arity (loc, Constant, "item", 2, List.length l) | Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _) -> fail @@ Invalid_constant (loc, "item")) - [] vs >>=? fun v -> - return (ref v, tk) + (empty_map tk) vs | Map_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) -> fail @@ Invalid_constant (loc, "map") @@ -786,10 +862,6 @@ and parse_instr parse_instr ?log ?storage_type ctxt bf rest >>=? fun bfr -> let branch ibt ibf = If_cons (ibt, ibf) in merge_branches loc btr bfr { branch } - | Prim (loc, "iter", []), - Item_t (Lambda_t (param, Void_t), Item_t (List_t elt, rest)) -> - check_item_ty elt param loc 2 >>=? fun (Eq _) -> - return (Typed (List_iter, rest)) | Prim (loc, "map", []), Item_t (Lambda_t (param, ret), Item_t (List_t elt, rest)) -> check_item_ty elt param loc 2 >>=? fun (Eq _) -> @@ -806,11 +878,6 @@ and parse_instr rest -> parse_comparable_ty t >>=? fun (Ex t) -> return (Typed (Empty_set t, Item_t (Set_t t, rest))) - | Prim (loc, "iter", []), - Item_t (Lambda_t (param, Void_t), Item_t (Set_t elt, rest)) -> - let elt = ty_of_comparable_ty elt in - check_item_ty elt param loc 2 >>=? fun (Eq _) -> - return (Typed (Set_iter, rest)) | Prim (loc, "map", []), Item_t (Lambda_t (param, ret), Item_t (Set_t elt, rest)) -> let elt = ty_of_comparable_ty elt in @@ -832,21 +899,15 @@ and parse_instr return (Typed (Set_mem, Item_t (Bool_t, rest))) | Prim (loc, "update", []), Item_t (v, Item_t (Bool_t, Item_t (Set_t elt, rest))) -> - let elt = ty_of_comparable_ty elt in - check_item_ty elt v loc 3 >>=? fun (Eq _) -> - return (Typed (Set_update, rest)) + let ty = ty_of_comparable_ty elt in + check_item_ty ty v loc 3 >>=? fun (Eq _) -> + return (Typed (Set_update, Item_t (Set_t elt, rest))) (* maps *) | Prim (_, "empty_map", [ tk ; tv ]), stack -> parse_comparable_ty tk >>=? fun (Ex tk) -> parse_ty tv >>=? fun (Ex tv) -> return (Typed (Empty_map (tk, tv), Item_t (Map_t (tk, tv), stack))) - | Prim (loc, "iter", []), - Item_t (Lambda_t (Pair_t (pk, pv), Void_t), Item_t (Map_t (k, v), rest)) -> - let k = ty_of_comparable_ty k in - check_item_ty pk k loc 2 >>=? fun (Eq _) -> - check_item_ty pv v loc 2 >>=? fun (Eq _) -> - return (Typed (Map_iter, rest)) | Prim (loc, "map", []), Item_t (Lambda_t (Pair_t (pk, pv), ret), Item_t (Map_t (ck, v), rest)) -> let k = ty_of_comparable_ty ck in @@ -877,18 +938,7 @@ and parse_instr let k = ty_of_comparable_ty ck in check_item_ty vk k loc 1 >>=? fun (Eq _) -> check_item_ty vv v loc 2 >>=? fun (Eq _) -> - return (Typed (Map_update, rest)) - (* reference cells *) - | Prim (_, "ref", []), - Item_t (t, rest) -> - return (Typed (Ref, Item_t (Ref_t t, rest))) - | Prim (_, "deref", []), - Item_t (Ref_t t, rest) -> - return (Typed (Deref, Item_t (t, rest))) - | Prim (loc, "set", []), - Item_t (Ref_t t, Item_t (tv, rest)) -> - check_item_ty tv t loc 2 >>=? fun (Eq _) -> - return (Typed (Set, rest)) + return (Typed (Map_update, Item_t (Map_t (ck, v), rest))) (* control *) | Seq (_, []), stack -> @@ -1254,7 +1304,7 @@ and parse_instr (* Primitive parsing errors *) | Prim (loc, ("drop" | "dup" | "swap" | "some" | "pair" | "car" | "cdr" | "cons" - | "mem" | "update" | "iter" | "map" | "reduce" + | "mem" | "update" | "map" | "reduce" | "get" | "ref" | "deref" | "set" | "exec" | "fail" | "nop" | "concat" | "add" | "sub" @@ -1315,7 +1365,7 @@ and parse_instr stack -> fail (Bad_stack (loc, 1, Stack_ty stack)) | Prim (loc, ("swap" | "pair" | "cons" | "set" | "incr" | "decr" - | "map" | "iter" | "get" | "mem" | "exec" + | "map" | "get" | "mem" | "exec" | "check_signature" | "add" | "sub" | "mul" | "div" | "mod" | "and" | "or" | "xor" | "lsl" | "lsr" | "concat" @@ -1414,9 +1464,6 @@ let rec unparse_ty let ta = unparse_ty uta in let tr = unparse_ty utr in Prim (-1, "lambda", [ ta; tr ]) - | Ref_t ut -> - let t = unparse_ty ut in - Prim (-1, "ref", [ t ]) | Option_t ut -> let t = unparse_ty ut in Prim (-1, "option", [ t ]) @@ -1467,9 +1514,6 @@ let rec unparse_untagged_data | Union_t (_, tr), R r -> let r = unparse_untagged_data tr r in Prim (-1, "right", [ r ]) - | Ref_t t, { contents } -> - let contents = unparse_untagged_data t contents in - Prim (-1, "ref", [ contents ]) | Option_t t, Some v -> let v = unparse_untagged_data t v in Prim (-1, "some", [ v ]) @@ -1478,18 +1522,23 @@ let rec unparse_untagged_data | List_t t, items -> let items = List.map (unparse_untagged_data t) items in Prim (-1, "list", items) - | Set_t t, ({ contents = items }, _) -> + | Set_t t, set -> let t = ty_of_comparable_ty t in - let items = List.map (unparse_untagged_data t) items in + let items = + set_fold + (fun item acc -> + unparse_untagged_data t item :: acc ) + set [] in Prim (-1, "set", items) - | Map_t (kt, vt), ({ contents = items }, _) -> + | Map_t (kt, vt), map -> let kt = ty_of_comparable_ty kt in let items = - List.map (fun (k, v) -> + map_fold (fun k v acc -> Prim (-1, "item", [ unparse_untagged_data kt k; - unparse_untagged_data vt v ])) - items in + unparse_untagged_data vt v ]) + :: acc) + map [] in Prim (-1, "map", items) | Lambda_t _, Lam (_, original_code) -> original_code @@ -1536,9 +1585,6 @@ let rec unparse_tagged_data let r = unparse_tagged_data tr r in let tl = unparse_ty tl in Prim (-1, "right", [ tl; r ]) - | Ref_t t, { contents } -> - let contents = unparse_tagged_data t contents in - Prim (-1, "ref", [ contents ]) | Option_t t, Some v -> let v = unparse_tagged_data t v in Prim (-1, "some", [ v ]) @@ -1549,19 +1595,24 @@ let rec unparse_tagged_data let items = List.map (unparse_untagged_data t) items in let t = unparse_ty t in Prim (-1, "list", t :: items) - | Set_t t, ({ contents = items }, _) -> + | Set_t t, set -> let t = ty_of_comparable_ty t in - let items = List.map (unparse_untagged_data t) items in + let items = + set_fold + (fun item acc -> + unparse_untagged_data t item :: acc ) + set [] in let t = unparse_ty t in Prim (-1, "set", t :: items) - | Map_t (kt, vt), ({ contents = items }, _) -> + | Map_t (kt, vt), map -> let kt = ty_of_comparable_ty kt in let items = - List.map (fun (k, v) -> + map_fold (fun k v acc -> Prim (-1, "item", [ unparse_untagged_data kt k; - unparse_untagged_data vt v ])) - items in + unparse_untagged_data vt v ]) + :: acc) + map [] in let kt = unparse_ty kt in let vt = unparse_ty vt in Prim (-1, "map", kt :: vt :: items) diff --git a/src/proto/bootstrap/script_typed_ir.ml b/src/proto/bootstrap/script_typed_ir.ml index 058f04ee9..2617a6d59 100644 --- a/src/proto/bootstrap/script_typed_ir.ml +++ b/src/proto/bootstrap/script_typed_ir.ml @@ -10,6 +10,35 @@ open Tezos_context open Script_int + +(* ---- Auxiliary types -----------------------------------------------------*) + +type 'ty comparable_ty = + | Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty + | String_key : string comparable_ty + | Tez_key : Tez.t comparable_ty + | Bool_key : bool comparable_ty + | Key_key : public_key_hash comparable_ty + | Timestamp_key : Timestamp.t comparable_ty + +module type Boxed_set = sig + type elt + module OPS : Set.S with type elt = elt + val boxed : OPS.t +end + +type 'elt set = (module Boxed_set with type elt = 'elt) + +module type Boxed_map = sig + type key + type value + val key_ty : key comparable_ty + module OPS : Map.S with type key = key + val boxed : value OPS.t +end + +type ('key, 'value) map = (module Boxed_map with type key = 'key and type value = 'value) + type ('arg, 'ret, 'storage) script = { code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ; arg_type : 'arg ty ; @@ -17,8 +46,6 @@ type ('arg, 'ret, 'storage) script = storage : 'storage ; storage_type : 'storage ty } -(* ---- Auxiliary types -----------------------------------------------------*) - and ('a, 'b) pair = 'a * 'b and ('a, 'b) union = L of 'a | R of 'b @@ -31,14 +58,6 @@ and ('arg, 'ret) lambda = and ('arg, 'ret) typed_contract = 'arg ty * 'ret ty * Contract.t -and 'ty comparable_ty = - | Int_key : ('s, 'l) int_kind -> ('s, 'l) int_val comparable_ty - | String_key : string comparable_ty - | Tez_key : Tez.t comparable_ty - | Bool_key : bool comparable_ty - | Key_key : public_key_hash comparable_ty - | Timestamp_key : Timestamp.t comparable_ty - and 'ty ty = | Void_t : unit ty | Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val ty @@ -52,18 +71,11 @@ and 'ty ty = | Union_t : 'a ty * 'b ty -> ('a, 'b) union ty | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty | Option_t : 'v ty -> 'v option ty - | Ref_t : 'v ty -> 'v ref ty | List_t : 'v ty -> 'v list ty | Set_t : 'v comparable_ty -> 'v set ty | Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty | Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract ty -and 'a set = - 'a list ref * 'a comparable_ty (* FIXME: ok, this is bad *) - -and ('a, 'b) map = - ('a * 'b) list ref * 'a comparable_ty (* FIXME: we'll have to do better *) - (* ---- Instructions --------------------------------------------------------*) (* The low-level, typed instructions, as a GADT whose parameters @@ -111,8 +123,6 @@ and ('bef, 'aft) instr = ('rest, ('a list * 'rest)) instr | If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr -> ('a list * 'bef, 'aft) instr - | List_iter : - (('param, unit) lambda * ('param list * 'rest), 'rest) instr | List_map : (('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr | List_reduce : @@ -121,8 +131,6 @@ and ('bef, 'aft) instr = (* sets *) | Empty_set : 'a comparable_ty -> ('rest, 'a set * 'rest) instr - | Set_iter : - (('param, unit) lambda * ('param set * 'rest), 'rest) instr | Set_map : 'ret comparable_ty -> (('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr | Set_reduce : @@ -131,12 +139,10 @@ and ('bef, 'aft) instr = | Set_mem : ('elt * ('elt set * 'rest), bool * 'rest) instr | Set_update : - ('elt * (bool * ('elt set * 'rest)), 'rest) instr + ('elt * (bool * ('elt set * 'rest)), 'elt set * 'rest) instr (* maps *) | Empty_map : 'a comparable_ty * 'v ty -> ('rest, ('a, 'v) map * 'rest) instr - | Map_iter : - (('a * 'v, unit) lambda * (('a, 'v) map * 'rest), 'rest) instr | Map_map : (('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr | Map_reduce : @@ -147,14 +153,7 @@ and ('bef, 'aft) instr = | Map_get : ('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr | Map_update : - ('a * ('v option * (('a, 'v) map * 'rest)), 'rest) instr - (* reference cells *) - | Ref : - ('v * 'rest, 'v ref * 'rest) instr - | Deref : - ('v ref * 'rest, 'v * 'rest) instr - | Set : - ('v ref * ('v * 'rest), 'rest) instr + ('a * ('v option * (('a, 'v) map * 'rest)), ('a, 'v) map * 'rest) instr (* string operations *) | Concat : (string * (string * 'rest), string * 'rest) instr