balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Proto: drop imperative constructs and instructions from the language.

Browse Source
This commit is contained in:
Benjamin Canou 2016-11-14 18:09:06 +01:00
parent 8602e5b0a0
commit 6eda849ce9
5 changed files with 208 additions and 271 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/proto/bootstrap/docs/json-notations.md
View File

@ -102,8 +102,6 @@ with the following JSON script description.
| { "left": [ /* tagged data */, /* type */ ] } | { "left": [ /* tagged data */, /* type */ ] }
| { "right": [ /* type */, /* tagged data */ ] } | { "right": [ /* type */, /* tagged data */ ] }
| { "or": [ /* type */, /* type */, /* untagged data */ ] } | { "or": [ /* type */, /* type */, /* untagged data */ ] }
| { "ref": [ /* tagged data */ ] }
| { "ref": [ /* type */, /* untagged data */ ] }
| { "some": [ /* tagged data */ ] } | { "some": [ /* tagged data */ ] }
| { "some": [ /* type */, /* untagged data */ ] } | { "some": [ /* type */, /* untagged data */ ] }
| { "none": [ /* type */ ] } | { "none": [ /* type */ ] }
@ -135,7 +133,6 @@ with the following JSON script description.
| { "pair": [ /* untagged data */, /* untagged data */ ] } | { "pair": [ /* untagged data */, /* untagged data */ ] }
| { "left": [ /* untagged data */ ] } | { "left": [ /* untagged data */ ] }
| { "right": [ /* untagged data */ ] } | { "right": [ /* untagged data */ ] }
| { "ref": [ /* untagged data */ ] }
| { "some": [ /* untagged data */ ] } | { "some": [ /* untagged data */ ] }
| "none" | "none"
| { "list": [ /* untagged data */ ... ] } | { "list": [ /* untagged data */ ... ] }
@ -161,15 +158,11 @@ with the following JSON script description.
| { "if_cons": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } | { "if_cons": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] }
| { "empty_set": [ /* type */ ] } | { "empty_set": [ /* type */ ] }
| { "empty_map": [ /* comparable type */, /* type */ ] } | { "empty_map": [ /* comparable type */, /* type */ ] }
| "iter"
| "map" | "map"
| "reduce" | "reduce"
| "mem" | "mem"
| "get" | "get"
| "update" | "update"
| "ref"
| "deref"
| "set"
| { "if": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] } | { "if": [ [ /* instruction */ ... ], [ /* instruction */ ... ] ] }
| { "loop": [ [ /* instruction */ ... ] ] } | { "loop": [ [ /* instruction */ ... ] ] }
| { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] } | { "lambda": [ /* type */, /* type */, [ /* instruction */ ... ] ] }
@ -239,7 +232,6 @@ with the following JSON script description.
| "key" | "key"
| "timestamp" | "timestamp"
| "signature" | "signature"
| { "ref": [ /* type */ ] }
| { "option": [ /* type */ ] } | { "option": [ /* type */ ] }
| { "list": [ /* type */ ] } | { "list": [ /* type */ ] }
| { "set": [ /* comparable type */ ] } | { "set": [ /* comparable type */ ] }

82
src/proto/bootstrap/docs/language.md
View File

@ -291,11 +291,8 @@ IV - Data types
A union of two types, a value holding either a value a of type 'a 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). 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`: * `set 'a`, `map 'a 'b`:
Imperative map and sets, optimized in the db. Immutable map and sets.
V - Operations 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 > CD(\rest)R ; C / S => CDR ; C(\rest)R ; C / S
> CR ; C / S => 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 ### Operations on sets
* `EMPTY_SET 'elt`: * `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 :: 'S -> set 'elt : 'S
@ -616,12 +574,7 @@ constants as is, concatenate them and use them as keys.
* `UPDATE`: * `UPDATE`:
Inserts or removes an element in a set, replacing a previous value. Inserts or removes an element in a set, replacing a previous value.
:: 'elt : bool : set 'elt : 'S -> 'S :: 'elt : bool : set 'elt : 'S -> set 'elt : 'S
* `ITER`:
Apply an imperative function over all the elements of a set.
:: lambda 'elt void : set 'elt : 'S -> 'S
* `REDUCE`: * `REDUCE`:
Apply a function on a set passing the result of each 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 ### Operations on maps
* `EMPTY_MAP 'key 'val`: * `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 The `'key` type must be comparable (the `COMPARE` primitive must be
defined over it). defined over it).
@ -653,12 +606,7 @@ constants as is, concatenate them and use them as keys.
* `UPDATE`: * `UPDATE`:
Assign or remove an element in a map. Assign or remove an element in a map.
:: 'key : option 'val : map 'key 'val : 'S -> 'S :: 'key : option 'val : map 'key 'val : 'S -> map 'key 'val : 'S
* `ITER`:
Apply an imperative function over all the bindings of a map.
:: lambda (pair 'key 'val) void : map 'key 'val : 'S -> 'S
* `MAP`: * `MAP`:
Apply a function on a map and return the map of results under 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 / (Cons a rest) : S => bt ; C / a : rest : S
> IF_CONS ; C / Nil : S => bf ; C / 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`: * `MAP`:
Apply a function on a list from left to right and Apply a function on a list from left to right and
return the list of results in the same order. 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 following type lambda (pair (pair tez 'arg) 'global) -> (pair 'ret
'global) where 'global is the type of the original global store given 'global) where 'global is the type of the original global store given
on origination. The contract also takes a parameter and an amount, and on origination. The contract also takes a parameter and an amount, and
returns a value, hence the complete calling convention above. The returns a value, hence the complete calling convention above.
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.
### Empty contract ### Empty contract
@ -1564,8 +1504,6 @@ X - Full grammar
| Left <tagged data> <type> | Left <tagged data> <type>
| Right <type> <tagged data> | Right <type> <tagged data>
| Or <type> <type> <untagged data> | Or <type> <type> <untagged data>
| Ref <tagged data>
| Ref <type> <untagged data>
| Some <tagged data> | Some <tagged data>
| Some <type> <untagged data> | Some <type> <untagged data>
| None <type> | None <type>
@ -1591,7 +1529,6 @@ X - Full grammar
| Pair <untagged data> <untagged data> | Pair <untagged data> <untagged data>
| Left <untagged data> | Left <untagged data>
| Right <untagged data> | Right <untagged data>
| Ref <untagged data>
| Some <untagged data> | Some <untagged data>
| None | None
| List <untagged data> ... | List <untagged data> ...
@ -1617,15 +1554,11 @@ X - Full grammar
| IF_CONS { <instruction> ... } { <instruction> ... } | IF_CONS { <instruction> ... } { <instruction> ... }
| EMPTY_SET <type> | EMPTY_SET <type>
| EMPTY_MAP <comparable type> <type> | EMPTY_MAP <comparable type> <type>
| ITER
| MAP | MAP
| REDUCE | REDUCE
| MEM | MEM
| GET | GET
| UPDATE | UPDATE
| REF
| DEREF
| SET
| IF { <instruction> ... } { <instruction> ... } | IF { <instruction> ... } { <instruction> ... }
| LOOP { <instruction> ... } | LOOP { <instruction> ... }
| LAMBDA <type> <type> { <instruction> ... } | LAMBDA <type> <type> { <instruction> ... }
@ -1694,7 +1627,6 @@ X - Full grammar
| key | key
| timestamp | timestamp
| signature | signature
| ref <type>
| option <type> | option <type>
| list <type> | list <type>
| set <comparable type> | set <comparable type>
@ -1757,7 +1689,7 @@ The language is implemented in OCaml as follows:
well-typed, corresponding GADT expressions. It is mostly a well-typed, corresponding GADT expressions. It is mostly a
checker, not a full inferer, and thus takes some annotations checker, not a full inferer, and thus takes some annotations
(basically the inpout and output of the program, of lambdas and of (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 symbolic evaluation of the program, transforming a symbolic
stack. It only needs one pass over the whole program. stack. It only needs one pass over the whole program.

105
src/proto/bootstrap/script_interpreter.ml
View File

@ -65,16 +65,6 @@ type 'tys stack =
| Item : 'ty * 'rest stack -> ('ty * 'rest) stack | Item : 'ty * 'rest stack -> ('ty * 'rest) stack
| Empty : end_of_stack 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 let rec interp
: type p r. : type p r.
int -> Contract.t -> Contract.t -> Tez.t -> int -> Contract.t -> Contract.t -> Tez.t ->
@ -131,11 +121,6 @@ let rec interp
step qta ctxt bf rest step qta ctxt bf rest
| If_cons (bt, _), Item (hd :: tl, rest) -> | If_cons (bt, _), Item (hd :: tl, rest) ->
step qta ctxt bt (Item (hd, Item (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)) -> | List_map, Item (lam, Item (l, rest)) ->
fold_left_s (fun (tail, qta, ctxt) arg -> fold_left_s (fun (tail, qta, ctxt) arg ->
interp qta orig source amount ctxt lam arg interp qta orig source amount ctxt lam arg
@ -153,82 +138,60 @@ let rec interp
return (Item (res, rest), qta, ctxt) return (Item (res, rest), qta, ctxt)
(* sets *) (* sets *)
| Empty_set t, rest -> | Empty_set t, rest ->
return (Item ((ref [], t), rest), qta - 1, ctxt) return (Item (empty_set t, rest), qta - 1, ctxt)
| Set_iter, Item (lam, Item ((l, _), rest)) -> | Set_map t, Item (lam, Item (set, rest)) ->
fold_left_s (fun ((), qta, ctxt) arg -> let items =
interp qta orig source amount ctxt lam arg) List.rev (set_fold (fun e acc -> e :: acc) set []) in
((), qta, ctxt) !l >>=? fun ((), qta, ctxt) ->
return (rest, qta, ctxt)
| Set_map t, Item (lam, Item ((l, _), rest)) ->
fold_left_s fold_left_s
(fun (tail, qta, ctxt) arg -> (fun (res, qta, ctxt) arg ->
interp qta orig source amount ctxt lam arg >>=? interp qta orig source amount ctxt lam arg >>=?
fun (ret, qta, ctxt) -> fun (ret, qta, ctxt) ->
return (ret :: tail, qta, ctxt)) return (set_update ret true res, qta, ctxt))
([], qta, ctxt) !l >>=? fun (res, qta, ctxt) -> (empty_set t, qta, ctxt) items >>=? fun (res, qta, ctxt) ->
return (Item ((ref res, t), rest), qta, ctxt) return (Item (res, rest), qta, ctxt)
| Set_reduce, Item (lam, Item ((l, _), Item (init, rest))) -> | 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 fold_left_s
(fun (partial, qta, ctxt) arg -> (fun (partial, qta, ctxt) arg ->
interp qta orig source amount ctxt lam (arg, partial) interp qta orig source amount ctxt lam (arg, partial)
>>=? fun (partial, qta, ctxt) -> >>=? fun (partial, qta, ctxt) ->
return (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) return (Item (res, rest), qta, ctxt)
| Set_mem, Item (v, Item ((l, kind), rest)) -> | Set_mem, Item (v, Item (set, rest)) ->
return (Item (List.exists (eq_comparable kind v) !l, rest), qta - 1, ctxt) return (Item (set_mem v set, rest), qta - 1, ctxt)
| Set_update, Item (v, Item (false, Item ((l, kind), rest))) -> | Set_update, Item (v, Item (presence, Item (set, rest))) ->
l := List.filter (fun x -> not (eq_comparable kind x v)) !l ; return (Item (set_update v presence set, rest), qta - 1, ctxt)
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)
(* maps *) (* maps *)
| Empty_map (t, _), rest -> | Empty_map (t, _), rest ->
return (Item ((ref [], t), rest), qta - 1, ctxt) return (Item (empty_map t, rest), qta - 1, ctxt)
| Map_iter, Item (lam, Item ((l, _), rest)) -> | 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 fold_left_s
(fun ((), qta, ctxt) arg -> interp qta orig source amount ctxt lam arg) (fun (acc, qta, ctxt) (k, v) ->
((), 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) ->
interp qta orig source amount ctxt lam (k, v) interp qta orig source amount ctxt lam (k, v)
>>=? fun (ret, qta, ctxt) -> >>=? fun (ret, qta, ctxt) ->
return ((k, ret) :: tail, qta, ctxt)) return (map_update k (Some ret) acc, qta, ctxt))
([], qta, ctxt) !l >>=? fun (res, qta, ctxt) -> (empty_map (map_key_ty map), qta, ctxt) items >>=? fun (res, qta, ctxt) ->
return (Item ((ref res, t), rest), qta, ctxt) return (Item (res, rest), qta, ctxt)
| Map_reduce, Item (lam, Item ((l, _), Item (init, rest))) -> | 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 fold_left_s
(fun (partial, qta, ctxt) arg -> (fun (partial, qta, ctxt) arg ->
interp qta orig source amount ctxt lam (arg, partial) interp qta orig source amount ctxt lam (arg, partial)
>>=? fun (partial, qta, ctxt) -> >>=? fun (partial, qta, ctxt) ->
return (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) return (Item (res, rest), qta, ctxt)
| Map_mem, Item (v, Item ((l, kind), rest)) -> | Map_mem, Item (v, Item (map, rest)) ->
let res = List.exists (fun (k, _) -> eq_comparable kind k v) !l in return (Item (map_mem v map, rest), qta - 1, ctxt)
return (Item (res, rest), qta - 1, ctxt) | Map_get, Item (v, Item (map, rest)) ->
| Map_get, Item (v, Item ((l, kind), rest)) -> return (Item (map_get v map, rest), qta - 1, ctxt)
let res = | Map_update, Item (k, Item (v, Item (map, rest))) ->
try Some (snd (List.find (fun (k, _) -> eq_comparable kind k v) !l)) return (Item (map_update k v map, rest), qta - 1, ctxt)
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)
(* timestamp operations *) (* timestamp operations *)
| Add_seconds_to_timestamp (kind, _pos), Item (n, Item (t, rest)) -> | Add_seconds_to_timestamp (kind, _pos), Item (n, Item (t, rest)) ->
let n = Script_int.to_int64 kind n in let n = Script_int.to_int64 kind n in

221
src/proto/bootstrap/script_ir_translator.ml
View File

@ -155,10 +155,6 @@ let rec ty_eq
ty_eq tar tbr >>? fun (Eq _) -> ty_eq tar tbr >>? fun (Eq _) ->
(eq ta tb : (ta ty, tb ty) eq tzresult)) |> (eq ta tb : (ta ty, tb ty) eq tzresult)) |>
record_trace (Inconsistent_types (Ty ta, Ty tb)) 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 -> | Option_t tva, Option_t tvb ->
(ty_eq tva tvb >>? fun (Eq _) -> (ty_eq tva tvb >>? fun (Eq _) ->
(eq ta tb : (ta ty, tb ty) eq tzresult)) |> (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 | Empty_t, Empty_t -> eq ta tb
| _, _ -> error Inconsistent_stack_lengths | _, _ -> 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 checker resuls -------------------------------------------------*)
type 'bef judgement = 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 uta >>=? fun (Ex ta) ->
parse_ty utr >>=? fun (Ex tr) -> parse_ty utr >>=? fun (Ex tr) ->
return @@ Ex (Lambda_t (ta, tr)) return @@ Ex (Lambda_t (ta, tr))
| Prim (_, "ref", [ ut ]) ->
parse_ty ut >>=? fun (Ex t) ->
return @@ Ex (Ref_t t)
| Prim (_, "option", [ ut ]) -> | Prim (_, "option", [ ut ]) ->
parse_ty ut >>=? fun (Ex t) -> parse_ty ut >>=? fun (Ex t) ->
return @@ Ex (Option_t t) return @@ Ex (Option_t t)
@ -433,15 +528,6 @@ let rec parse_tagged_data
return @@ Ex (Union_t (tl, tr), v) return @@ Ex (Union_t (tl, tr), v)
| Prim (loc, "or", l) -> | Prim (loc, "or", l) ->
fail @@ Invalid_arity (loc, Constant, "or", 3, List.length 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 ]) -> | Prim (_, "some", [ r ]) ->
parse_tagged_data ctxt r >>=? fun (Ex (tr, r)) -> parse_tagged_data ctxt r >>=? fun (Ex (tr, r)) ->
return @@ Ex (Option_t tr, Some r) return @@ Ex (Option_t tr, Some r)
@ -621,14 +707,6 @@ and parse_untagged_data
parse_lambda ctxt ta tr script_instr parse_lambda ctxt ta tr script_instr
| Lambda_t (_, _), (Prim (loc, _, _) | Int (loc, _) | String (loc, _)) -> | Lambda_t (_, _), (Prim (loc, _, _) | Int (loc, _) | String (loc, _)) ->
fail @@ Invalid_constant (loc, "lambda") 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 *) (* Options *)
| Option_t t, Prim (_, "some", [ v ]) -> | Option_t t, Prim (_, "some", [ v ]) ->
parse_untagged_data ctxt t v >>=? fun v -> parse_untagged_data ctxt t v >>=? fun v ->
@ -653,27 +731,25 @@ and parse_untagged_data
(* Sets *) (* Sets *)
| Set_t t, Prim (_, "set", vs) -> | Set_t t, Prim (_, "set", vs) ->
fold_left_s fold_left_s
(fun rest v -> (fun acc v ->
parse_untagged_comparable_data ctxt t v >>=? fun v -> parse_untagged_comparable_data ctxt t v >>=? fun v ->
return (v :: rest)) return (set_update v true acc))
[] vs >>=? fun v -> (empty_set t) vs
return (ref v, t)
| Set_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) -> | Set_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
fail @@ Invalid_constant (loc, "set") fail @@ Invalid_constant (loc, "set")
(* Maps *) (* Maps *)
| Map_t (tk, tv), Prim (_, "map", vs) -> | Map_t (tk, tv), Prim (_, "map", vs) ->
fold_left_s fold_left_s
(fun rest -> function (fun acc -> function
| Prim (_, "item", [ k; v ]) -> | Prim (_, "item", [ k; v ]) ->
parse_untagged_comparable_data ctxt tk k >>=? fun k -> parse_untagged_comparable_data ctxt tk k >>=? fun k ->
parse_untagged_data ctxt tv v >>=? fun v -> parse_untagged_data ctxt tv v >>=? fun v ->
return ((k, v) :: rest) return (map_update k (Some v) acc)
| Prim (loc, "item", l) -> | Prim (loc, "item", l) ->
fail @@ Invalid_arity (loc, Constant, "item", 2, List.length l) fail @@ Invalid_arity (loc, Constant, "item", 2, List.length l)
| Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _) -> | Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _) ->
fail @@ Invalid_constant (loc, "item")) fail @@ Invalid_constant (loc, "item"))
[] vs >>=? fun v -> (empty_map tk) vs
return (ref v, tk)
| Map_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) -> | Map_t _, (Prim (loc, _, _) | Int (loc, _) | String (loc, _) | Seq (loc, _)) ->
fail @@ Invalid_constant (loc, "map") fail @@ Invalid_constant (loc, "map")
@ -786,10 +862,6 @@ and parse_instr
parse_instr ?log ?storage_type ctxt bf rest >>=? fun bfr -> parse_instr ?log ?storage_type ctxt bf rest >>=? fun bfr ->
let branch ibt ibf = If_cons (ibt, ibf) in let branch ibt ibf = If_cons (ibt, ibf) in
merge_branches loc btr bfr { branch } 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", []), | Prim (loc, "map", []),
Item_t (Lambda_t (param, ret), Item_t (List_t elt, rest)) -> Item_t (Lambda_t (param, ret), Item_t (List_t elt, rest)) ->
check_item_ty elt param loc 2 >>=? fun (Eq _) -> check_item_ty elt param loc 2 >>=? fun (Eq _) ->
@ -806,11 +878,6 @@ and parse_instr
rest -> rest ->
parse_comparable_ty t >>=? fun (Ex t) -> parse_comparable_ty t >>=? fun (Ex t) ->
return (Typed (Empty_set t, Item_t (Set_t t, rest))) 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", []), | Prim (loc, "map", []),
Item_t (Lambda_t (param, ret), Item_t (Set_t elt, rest)) -> Item_t (Lambda_t (param, ret), Item_t (Set_t elt, rest)) ->
let elt = ty_of_comparable_ty elt in let elt = ty_of_comparable_ty elt in
@ -832,21 +899,15 @@ and parse_instr
return (Typed (Set_mem, Item_t (Bool_t, rest))) return (Typed (Set_mem, Item_t (Bool_t, rest)))
| Prim (loc, "update", []), | Prim (loc, "update", []),
Item_t (v, Item_t (Bool_t, Item_t (Set_t elt, rest))) -> Item_t (v, Item_t (Bool_t, Item_t (Set_t elt, rest))) ->
let elt = ty_of_comparable_ty elt in let ty = ty_of_comparable_ty elt in
check_item_ty elt v loc 3 >>=? fun (Eq _) -> check_item_ty ty v loc 3 >>=? fun (Eq _) ->
return (Typed (Set_update, rest)) return (Typed (Set_update, Item_t (Set_t elt, rest)))
(* maps *) (* maps *)
| Prim (_, "empty_map", [ tk ; tv ]), | Prim (_, "empty_map", [ tk ; tv ]),
stack -> stack ->
parse_comparable_ty tk >>=? fun (Ex tk) -> parse_comparable_ty tk >>=? fun (Ex tk) ->
parse_ty tv >>=? fun (Ex tv) -> parse_ty tv >>=? fun (Ex tv) ->
return (Typed (Empty_map (tk, tv), Item_t (Map_t (tk, tv), stack))) 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", []), | Prim (loc, "map", []),
Item_t (Lambda_t (Pair_t (pk, pv), ret), Item_t (Map_t (ck, v), rest)) -> Item_t (Lambda_t (Pair_t (pk, pv), ret), Item_t (Map_t (ck, v), rest)) ->
let k = ty_of_comparable_ty ck in let k = ty_of_comparable_ty ck in
@ -877,18 +938,7 @@ and parse_instr
let k = ty_of_comparable_ty ck in let k = ty_of_comparable_ty ck in
check_item_ty vk k loc 1 >>=? fun (Eq _) -> check_item_ty vk k loc 1 >>=? fun (Eq _) ->
check_item_ty vv v loc 2 >>=? fun (Eq _) -> check_item_ty vv v loc 2 >>=? fun (Eq _) ->
return (Typed (Map_update, rest)) return (Typed (Map_update, Item_t (Map_t (ck, v), 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))
(* control *) (* control *)
| Seq (_, []), | Seq (_, []),
stack -> stack ->
@ -1254,7 +1304,7 @@ and parse_instr
(* Primitive parsing errors *) (* Primitive parsing errors *)
| Prim (loc, ("drop" | "dup" | "swap" | "some" | Prim (loc, ("drop" | "dup" | "swap" | "some"
| "pair" | "car" | "cdr" | "cons" | "pair" | "car" | "cdr" | "cons"
| "mem" | "update" | "iter" | "map" | "reduce" | "mem" | "update" | "map" | "reduce"
| "get" | "ref" | "deref" | "get" | "ref" | "deref"
| "set" | "exec" | "fail" | "nop" | "set" | "exec" | "fail" | "nop"
| "concat" | "add" | "sub" | "concat" | "add" | "sub"
@ -1315,7 +1365,7 @@ and parse_instr
stack -> stack ->
fail (Bad_stack (loc, 1, Stack_ty stack)) fail (Bad_stack (loc, 1, Stack_ty stack))
| Prim (loc, ("swap" | "pair" | "cons" | "set" | "incr" | "decr" | Prim (loc, ("swap" | "pair" | "cons" | "set" | "incr" | "decr"
| "map" | "iter" | "get" | "mem" | "exec" | "map" | "get" | "mem" | "exec"
| "check_signature" | "add" | "sub" | "mul" | "check_signature" | "add" | "sub" | "mul"
| "div" | "mod" | "and" | "or" | "xor" | "div" | "mod" | "and" | "or" | "xor"
| "lsl" | "lsr" | "concat" | "lsl" | "lsr" | "concat"
@ -1414,9 +1464,6 @@ let rec unparse_ty
let ta = unparse_ty uta in let ta = unparse_ty uta in
let tr = unparse_ty utr in let tr = unparse_ty utr in
Prim (-1, "lambda", [ ta; tr ]) Prim (-1, "lambda", [ ta; tr ])
| Ref_t ut ->
let t = unparse_ty ut in
Prim (-1, "ref", [ t ])
| Option_t ut -> | Option_t ut ->
let t = unparse_ty ut in let t = unparse_ty ut in
Prim (-1, "option", [ t ]) Prim (-1, "option", [ t ])
@ -1467,9 +1514,6 @@ let rec unparse_untagged_data
| Union_t (_, tr), R r -> | Union_t (_, tr), R r ->
let r = unparse_untagged_data tr r in let r = unparse_untagged_data tr r in
Prim (-1, "right", [ r ]) 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 -> | Option_t t, Some v ->
let v = unparse_untagged_data t v in let v = unparse_untagged_data t v in
Prim (-1, "some", [ v ]) Prim (-1, "some", [ v ])
@ -1478,18 +1522,23 @@ let rec unparse_untagged_data
| List_t t, items -> | List_t t, items ->
let items = List.map (unparse_untagged_data t) items in let items = List.map (unparse_untagged_data t) items in
Prim (-1, "list", items) Prim (-1, "list", items)
| Set_t t, ({ contents = items }, _) -> | Set_t t, set ->
let t = ty_of_comparable_ty t in 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) Prim (-1, "set", items)
| Map_t (kt, vt), ({ contents = items }, _) -> | Map_t (kt, vt), map ->
let kt = ty_of_comparable_ty kt in let kt = ty_of_comparable_ty kt in
let items = let items =
List.map (fun (k, v) -> map_fold (fun k v acc ->
Prim (-1, "item", Prim (-1, "item",
[ unparse_untagged_data kt k; [ unparse_untagged_data kt k;
unparse_untagged_data vt v ])) unparse_untagged_data vt v ])
items in :: acc)
map [] in
Prim (-1, "map", items) Prim (-1, "map", items)
| Lambda_t _, Lam (_, original_code) -> | Lambda_t _, Lam (_, original_code) ->
original_code original_code
@ -1536,9 +1585,6 @@ let rec unparse_tagged_data
let r = unparse_tagged_data tr r in let r = unparse_tagged_data tr r in
let tl = unparse_ty tl in let tl = unparse_ty tl in
Prim (-1, "right", [ tl; r ]) 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 -> | Option_t t, Some v ->
let v = unparse_tagged_data t v in let v = unparse_tagged_data t v in
Prim (-1, "some", [ v ]) Prim (-1, "some", [ v ])
@ -1549,19 +1595,24 @@ let rec unparse_tagged_data
let items = List.map (unparse_untagged_data t) items in let items = List.map (unparse_untagged_data t) items in
let t = unparse_ty t in let t = unparse_ty t in
Prim (-1, "list", t :: items) Prim (-1, "list", t :: items)
| Set_t t, ({ contents = items }, _) -> | Set_t t, set ->
let t = ty_of_comparable_ty t in 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 let t = unparse_ty t in
Prim (-1, "set", t :: items) 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 kt = ty_of_comparable_ty kt in
let items = let items =
List.map (fun (k, v) -> map_fold (fun k v acc ->
Prim (-1, "item", Prim (-1, "item",
[ unparse_untagged_data kt k; [ unparse_untagged_data kt k;
unparse_untagged_data vt v ])) unparse_untagged_data vt v ])
items in :: acc)
map [] in
let kt = unparse_ty kt in let kt = unparse_ty kt in
let vt = unparse_ty vt in let vt = unparse_ty vt in
Prim (-1, "map", kt :: vt :: items) Prim (-1, "map", kt :: vt :: items)

63
src/proto/bootstrap/script_typed_ir.ml
View File

@ -10,6 +10,35 @@
open Tezos_context open Tezos_context
open Script_int 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 = type ('arg, 'ret, 'storage) script =
{ code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ; { code : (((Tez.t, 'arg) pair, 'storage) pair, ('ret, 'storage) pair) lambda ;
arg_type : 'arg ty ; arg_type : 'arg ty ;
@ -17,8 +46,6 @@ type ('arg, 'ret, 'storage) script =
storage : 'storage ; storage : 'storage ;
storage_type : 'storage ty } storage_type : 'storage ty }
(* ---- Auxiliary types -----------------------------------------------------*)
and ('a, 'b) pair = 'a * 'b and ('a, 'b) pair = 'a * 'b
and ('a, 'b) union = L of 'a | R of 'b and ('a, 'b) union = L of 'a | R of 'b
@ -31,14 +58,6 @@ and ('arg, 'ret) lambda =
and ('arg, 'ret) typed_contract = and ('arg, 'ret) typed_contract =
'arg ty * 'ret ty * Contract.t '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 = and 'ty ty =
| Void_t : unit ty | Void_t : unit ty
| Int_t : ('s, 'l) int_kind -> ('s, 'l) int_val 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 | Union_t : 'a ty * 'b ty -> ('a, 'b) union ty
| Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty | Lambda_t : 'arg ty * 'ret ty -> ('arg, 'ret) lambda ty
| Option_t : 'v ty -> 'v option ty | Option_t : 'v ty -> 'v option ty
| Ref_t : 'v ty -> 'v ref ty
| List_t : 'v ty -> 'v list ty | List_t : 'v ty -> 'v list ty
| Set_t : 'v comparable_ty -> 'v set ty | Set_t : 'v comparable_ty -> 'v set ty
| Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty | Map_t : 'k comparable_ty * 'v ty -> ('k, 'v) map ty
| Contract_t : 'arg ty * 'ret ty -> ('arg, 'ret) typed_contract 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 --------------------------------------------------------*) (* ---- Instructions --------------------------------------------------------*)
(* The low-level, typed instructions, as a GADT whose parameters (* The low-level, typed instructions, as a GADT whose parameters
@ -111,8 +123,6 @@ and ('bef, 'aft) instr =
('rest, ('a list * 'rest)) instr ('rest, ('a list * 'rest)) instr
| If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr -> | If_cons : ('a * ('a list * 'bef), 'aft) instr * ('bef, 'aft) instr ->
('a list * 'bef, 'aft) instr ('a list * 'bef, 'aft) instr
| List_iter :
(('param, unit) lambda * ('param list * 'rest), 'rest) instr
| List_map : | List_map :
(('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr (('param, 'ret) lambda * ('param list * 'rest), 'ret list * 'rest) instr
| List_reduce : | List_reduce :
@ -121,8 +131,6 @@ and ('bef, 'aft) instr =
(* sets *) (* sets *)
| Empty_set : 'a comparable_ty -> | Empty_set : 'a comparable_ty ->
('rest, 'a set * 'rest) instr ('rest, 'a set * 'rest) instr
| Set_iter :
(('param, unit) lambda * ('param set * 'rest), 'rest) instr
| Set_map : 'ret comparable_ty -> | Set_map : 'ret comparable_ty ->
(('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr (('param, 'ret) lambda * ('param set * 'rest), 'ret set * 'rest) instr
| Set_reduce : | Set_reduce :
@ -131,12 +139,10 @@ and ('bef, 'aft) instr =
| Set_mem : | Set_mem :
('elt * ('elt set * 'rest), bool * 'rest) instr ('elt * ('elt set * 'rest), bool * 'rest) instr
| Set_update : | Set_update :
('elt * (bool * ('elt set * 'rest)), 'rest) instr ('elt * (bool * ('elt set * 'rest)), 'elt set * 'rest) instr
(* maps *) (* maps *)
| Empty_map : 'a comparable_ty * 'v ty -> | Empty_map : 'a comparable_ty * 'v ty ->
('rest, ('a, 'v) map * 'rest) instr ('rest, ('a, 'v) map * 'rest) instr
| Map_iter :
(('a * 'v, unit) lambda * (('a, 'v) map * 'rest), 'rest) instr
| Map_map : | Map_map :
(('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr (('a * 'v, 'r) lambda * (('a, 'v) map * 'rest), ('a, 'r) map * 'rest) instr
| Map_reduce : | Map_reduce :
@ -147,14 +153,7 @@ and ('bef, 'aft) instr =
| Map_get : | Map_get :
('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr ('a * (('a, 'v) map * 'rest), 'v option * 'rest) instr
| Map_update : | Map_update :
('a * ('v option * (('a, 'v) map * 'rest)), 'rest) instr ('a * ('v option * (('a, 'v) map * 'rest)), ('a, 'v) map * '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
(* string operations *) (* string operations *)
| Concat : | Concat :
(string * (string * 'rest), string * 'rest) instr (string * (string * 'rest), string * 'rest) instr