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

Michelson: Remove binding annotations

Browse Source 
Use RENAME in code blocks instead.
This commit is contained in:
Alain Mebsout 2018-06-08 12:54:37 +02:00 committed by Benjamin Canou
parent b61df9d816
commit 1748f370fc
8 changed files with 105 additions and 317 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

106
docs/whitedoc/michelson.rst
View File

@ -726,7 +726,7 @@ Bitwise logical operators are also available on unsigned integers.
- ``NOT`` The return type of ``NOT`` is an ``int`` and not a ``nat``.
This is because the sign is also negated. The resulting integer is
computed using two’s complement. For instance, the boolean negation
computed using two's complement. For instance, the boolean negation
of ``0`` is ``-1``. To get a natural back, a possibility is to use
``AND`` with an unsigned mask afterwards.
@ -801,7 +801,7 @@ constants as is, concatenate them and use them as keys.
Operations on pairs
~~~~~~~~~~~~~~~~~~~
- ``PAIR``: Build a pair from the stack’s top two elements.
- ``PAIR``: Build a pair from the stack's top two elements.
::
@ -1282,7 +1282,7 @@ types by mistake. They are also mandatory checked for under/overflows.
::
:: tez : tez : ’S -> int : ’S
:: tez : tez : 'S -> int : 'S
> COMPARE / x : y : S => -1 : S
iff x < y
@ -1473,12 +1473,12 @@ VIII - Macros
-------------
In addition to the operations above, several extensions have been added
to the language’s concrete syntax. If you are interacting with the node
to the language's concrete syntax. If you are interacting with the node
via RPC, bypassing the client, which expands away these macros, you will
need to desugar them yourself.
These macros are designed to be unambiguous and reversible, meaning that
errors are reported in terms of desugared syntax. Below you’ll see
errors are reported in terms of desugared syntax. Below you'll see
these macros defined in terms of other syntactic forms. That is how
these macros are seen by the node.
@ -1840,19 +1840,20 @@ line can also be written, using C-like delimiters (``/* ... */``).
X - Annotations
---------------
The annotation mechanism of Michelson provides ways to better track
data on the stack and to give additional type constraints.
The annotation mechanism of Michelson provides ways to better track data
on the stack and to give additional type constraints. Annotaions are
only here to add constraints, *i.e.* they cannot turn an otherwise
rejected program into an accepted one.
Stack visualization tools like the Michelson’s Emacs mode print
Stack visualization tools like the Michelson's Emacs mode print
annotations associated with each type in the program, as propagated by
the typechecker as well as variable annotations on the types of elements
in the stack. This is useful as a debugging aid.
We distinguish four kinds of annotations:
We distinguish three kinds of annotations:
- type annotations, written ``:type_annot``,
- variable annotations, written ``@var_annot``,
- field or constructors annotations, written ``%field_annot``,
- and binding annotations, written ``$bind_annot``.
- and field or constructors annotations, written ``%field_annot``.
Type Annotations
~~~~~~~~~~~~~~~~
@ -2142,73 +2143,18 @@ the accessed field in the destructed pair must match the one given here.
:: (pair 'a ('b %snd)) : S -> 'b : 'S
Binding Annotations
~~~~~~~~~~~~~~~~~~~
Michelson supports an extra kind of annotations which act as variable
annotations for values bound by instructions inside code blocks.
::
IF_NONE $some_value bt bf
:: option 'a : 'S -> 'b : 'S
iff bt :: [ 'S -> 'b : 'S]
bf :: [ @some_value 'a : 'S -> 'b : 'S]
IF_LEFT $left_value $right_value bt bf
:: or 'a 'b : 'S -> 'c : 'S
iff bt :: [ @left_value 'a : 'S -> 'c : 'S]
bf :: [ @right_value 'b : 'S -> 'c : 'S]
IF_CONS $head $tail bt bf
:: list 'a : 'S -> 'b : 'S
iff bt :: [ @head 'a : @tail list 'a : 'S -> 'b : 'S]
bf :: [ 'S -> 'b : 'S]
MAP $x body
:: (list 'elt) : 'A -> (list 'b) : 'A
iff body :: [ @x 'elt : 'A -> 'b : 'A ]
MAP $x body
:: (set 'elt) : 'A -> (set 'b) : 'A
iff body :: [ @x 'elt : 'A -> 'b : 'A ]
MAP $k $v body
:: (map 'key 'val) : 'A -> (map 'key 'b) : 'A
iff body :: [ (pair ('key %k) ('val %v)) : 'A -> 'b : 'A ]
ITER $x body
:: (set 'elt) : 'A -> 'A
iff body :: [ @x 'elt : 'A -> 'A ]
ITER $x body
:: (list 'elt) : 'A -> 'A
iff body :: [ @x 'elt : 'A -> 'A ]
ITER $k $v body
:: (map 'elt 'val) : 'A -> 'A
iff body :: [ (pair ('elt %k) ('val %v)) : 'A -> 'A ]
LAMBDA $arg 'a 'b code
:: 'A -> (lambda 'a 'b) : 'A
iff code :: [ @arg 'a : [] -> 'b : [] ]
LOOP_LEFT $acc body
:: (or 'a 'b) : 'A -> 'A
iff body :: [ @acc 'a : 'A -> (or 'a 'b) : 'A ]
Syntax
~~~~~~
Primitive applications can receive one or many annotations.
An annotation is a sequence of characters that matches the regular
expression ``[\@\:\%\$][0-9a-zA-Z\.]*``. They come after the primitive
expression ``[\@\:\%\$][_0-9a-zA-Z\.]*``. They come after the primitive
name and before its potential arguments for primitive applications.
::
(prim @annot arg arg ...)
(prim @v :t %x arg1 arg2 ...)
Ordering between different kinds of annotations is not significant, but
@ -2343,10 +2289,16 @@ A similar mechanism is used for context dependent instructions:
NOW :: 'S -> @now timestamp : 'S
If now binding annotation is provided for instruction with code blocks
(that accept one), then the bound items on the stack will be given a
Inside nested code blocks, bound items on the stack will be given a
default variable name annotation depending on the instruction and stack
type.
type (which can be changed). For instance the annotated typing rule for
``ITER`` on lists is:
::
ITER body
:: @l (list 'e) : 'A -> 'A
iff body :: [ @l.elt e' : 'A -> 'A ]
XI - JSON syntax
---------------
@ -2387,8 +2339,8 @@ storage. The type of the global data of the storage is fixed for each
contract at origination time. This is ensured statically by checking on
origination that the code preserves the type of the global data. For
this, the code of the contract is checked to be of type
``lambda (pair ’arg ’global) -> (pair (list operation) ’global)`` where
``’global`` is the type of the original global store given on origination.
``lambda (pair 'arg 'global) -> (pair (list operation) 'global)`` where
``'global`` is the type of the original global store given on origination.
The contract also takes a parameter and returns a list of internal operations,
hence the complete calling convention above. The internal operations are
queued for execution when the contract returns.
@ -2413,7 +2365,7 @@ Reservoir contract
We want to create a contract that stores tez until a timestamp ``T`` or
a maximum amount ``N`` is reached. Whenever ``N`` is reached before
``T``, all tokens are reversed to an account ``B`` (and the contract is
automatically deleted). Any call to the contract’s code performed after
automatically deleted). Any call to the contract's code performed after
``T`` will otherwise transfer the tokens to another account ``A``.
We want to build this contract in a reusable manner, so we do not
@ -2621,7 +2573,7 @@ After the first day, nothing cam happen until ``T``.
During the 24 hours after ``T``, the buyer must pay ``(Q * K)`` to the
contract, minus the amount already sent.
After this day, if the buyer didn’t pay enough then any transaction will
After this day, if the buyer didn't pay enough then any transaction will
send all the tokens to the seller.
Otherwise, the seller must deliver at least ``Q`` tons of dried peas to
@ -2961,7 +2913,7 @@ The language is implemented in OCaml as follows:
- The lower internal representation is written as a GADT whose type
parameters encode exactly the typing rules given in this
specification. In other words, if a program written in this
representation is accepted by OCaml’s typechecker, it is guaranteed
representation is accepted by OCaml's typechecker, it is guaranteed
type-safe. This of course also valid for programs not handwritten but
generated by OCaml code, so we are sure that any manipulated code is
type-safe.
@ -2973,7 +2925,7 @@ The language is implemented in OCaml as follows:
- The interpreter is basically the direct transcription of the
rewriting rules presented above. It takes an instruction, a stack and
transforms it. OCaml’s typechecker ensures that the transformation
transforms it. OCaml's typechecker ensures that the transformation
respects the pre and post stack types declared by the GADT case for
each instruction.

16
src/bin_client/test/contracts/accounts.tz
View File

@ -14,12 +14,12 @@ storage (map :stored_balance key_hash mutez);
code { DUP; CAR;
# Deposit into account
IF_LEFT { DUP; DIIP{ CDR %stored_balance; DUP };
DIP{ SWAP }; GET;
DIP{ SWAP }; GET @opt_prev_balance;
# Create the account
IF_SOME $previous_balance
# Add to an existing account
{ AMOUNT; ADD; SOME; SWAP; UPDATE; NIL operation; PAIR }
{ DIP{ AMOUNT; SOME }; UPDATE; NIL operation; PAIR }}
IF_SOME # Add to an existing account
{ RENAME @previous_balance;
AMOUNT; ADD; SOME; SWAP; UPDATE; NIL operation; PAIR }
{ DIP{ AMOUNT; SOME }; UPDATE; NIL operation; PAIR }}
# Withdrawl
{ DUP; DUP; DUP; DUP;
# Check signature on data
@ -31,10 +31,10 @@ code { DUP; CAR;
DIIP{ CDR %stored_balance; DUP };
CAR %from; HASH_KEY @from_hash; DIP{ SWAP }; GET;
# Account does not exist
IF_NONE $previous_balance
{ FAIL }
IF_NONE { FAIL }
# Account exists
{ DUP; DIIP{ DUP; CDAR %withdraw_amount; DUP };
{ RENAME @previous_balance;
DUP; DIIP{ DUP; CDAR %withdraw_amount; DUP };
# Ensure funds are available
DIP{ CMPLT @not_enough }; SWAP;
IF { FAIL }

6
src/bin_client/test/contracts/map_iter.tz
View File

@ -1,7 +1,7 @@
parameter (map (int :k) (int :e));
storage (pair (int :k) (int :e));
code { CAR; PUSH @acc_e (int :e) 0; PUSH @acc_k (int :k) 0; PAIR; SWAP;
ITER $my_key $my_elt
{ DIP {DUP; CAR; DIP{CDR}}; DUP; # Last instr
DIP{CAR; ADD}; SWAP; DIP{CDR; ADD}; PAIR };
ITER
{ DIP {DUP; CAR; DIP{CDR}}; DUP; # Last instr
DIP{CAR; ADD}; SWAP; DIP{CDR; ADD}; PAIR };
NIL operation; PAIR}

22
src/proto_alpha/lib_client/michelson_v1_macros.ml
View File

@ -572,15 +572,6 @@ let expand_if_right = function
error (Invalid_arity ("IF_RIGHT", List.length args, 2))
| _ -> ok @@ None
let expand_rename = function
| Prim (loc, "RENAME", [], annot) ->
ok @@ Some (Seq (loc, [
Prim (loc, "DUP", [], annot) ;
Prim (loc, "SWAP", [], []) ;
Prim (loc, "DROP", [], []) ;
]))
| _ -> ok @@ None
let expand original =
let rec try_expansions = function
| [] -> ok @@ original
@ -602,7 +593,6 @@ let expand original =
expand_asserts ;
expand_if_some ;
expand_if_right ;
expand_rename ;
]
let expand_rec expr =
@ -1008,15 +998,6 @@ let unexpand_if_right = function
Some (Prim (loc, "IF_RIGHT", [ right ; left ], annot))
| _ -> None
let unexpand_rename = function
| Seq (loc, [
Prim (_, "DUP", [], annot) ;
Prim (_, "SWAP", [], []) ;
Prim (_, "DROP", [], []) ;
]) ->
Some (Prim (loc, "RENAME", [], annot))
| _ -> None
let unexpand original =
let try_unexpansions unexpanders =
match
@ -1039,8 +1020,7 @@ let unexpand original =
unexpand_duuuuup ;
unexpand_compare ;
unexpand_if_some ;
unexpand_if_right ;
unexpand_rename ]
unexpand_if_right ]
let rec unexpand_rec expr =
match unexpand expr with

135
src/proto_alpha/lib_protocol/src/script_ir_annot.ml
View File

@ -18,6 +18,7 @@ let default_balance_annot = Some (`Var_annot "balance")
let default_steps_annot = Some (`Var_annot "steps")
let default_source_annot = Some (`Var_annot "source")
let default_self_annot = Some (`Var_annot "self")
let default_arg_annot = Some (`Var_annot "arg")
let default_param_annot = Some (`Field_annot "parameter")
let default_storage_annot = Some (`Field_annot "storage")
@ -27,13 +28,14 @@ let default_contract_annot = Some (`Field_annot "contract")
let default_addr_annot = Some (`Field_annot "address")
let default_manager_annot = Some (`Field_annot "manager")
let default_arg_annot = Some (`Binding_annot "arg")
let default_elt_annot = Some (`Binding_annot "elt")
let default_key_annot = Some (`Binding_annot "key")
let default_hd_annot = Some (`Binding_annot "hd")
let default_some_annot = Some (`Binding_annot "some")
let default_left_annot = Some (`Binding_annot "left")
let default_right_annot = Some (`Binding_annot "right")
let default_elt_annot = Some (`Field_annot "elt")
let default_key_annot = Some (`Field_annot "key")
let default_hd_annot = Some (`Field_annot "hd")
let default_tl_annot = Some (`Field_annot "tl")
let default_some_annot = Some (`Field_annot "some")
let default_left_annot = Some (`Field_annot "left")
let default_right_annot = Some (`Field_annot "right")
let default_binding_annot = Some (`Field_annot "bnd")
let unparse_type_annot : type_annot option -> string list = function
| None -> []
@ -47,35 +49,11 @@ let unparse_field_annot : field_annot option -> string list = function
| None -> []
| Some `Field_annot a -> [ "%" ^ a ]
let unparse_binding_annot : binding_annot option -> string list = function
| None -> []
| Some `Binding_annot a -> [ "$" ^ a ]
let field_to_var_annot : field_annot option -> var_annot option =
function
| None -> None
| Some (`Field_annot s) -> Some (`Var_annot s)
let field_to_binding_annot : field_annot option -> binding_annot option =
function
| None -> None
| Some (`Field_annot s) -> Some (`Binding_annot s)
let binding_to_var_annot : binding_annot option -> var_annot option =
function
| None -> None
| Some (`Binding_annot s) -> Some (`Var_annot s)
let binding_to_field_annot : binding_annot option -> field_annot option =
function
| None -> None
| Some (`Binding_annot s) -> Some (`Field_annot s)
let var_to_binding_annot : var_annot option -> binding_annot option =
function
| None -> None
| Some (`Var_annot s) -> Some (`Binding_annot s)
let type_to_field_annot : type_annot option -> field_annot option =
function
| None -> None
@ -102,18 +80,6 @@ let gen_access_annot
| Some `Var_annot v, Some `Field_annot f, _ ->
Some (`Var_annot (String.concat "." [v; f]))
let gen_binding_access_annot
: var_annot option -> ?default:binding_annot option -> binding_annot option -> binding_annot option
= fun value_annot ?(default=None) binding_annot ->
match value_annot, binding_annot, default with
| None, None, _ | Some _, None, None | None, Some `Binding_annot "", _ -> None
| None, Some `Binding_annot b, _ ->
Some (`Binding_annot b)
| Some `Var_annot v, (None | Some `Binding_annot ""), Some `Binding_annot b ->
Some (`Binding_annot (String.concat "." [v; b]))
| Some `Var_annot v, Some `Binding_annot b, _ ->
Some (`Binding_annot (String.concat "." [v; b]))
let merge_type_annot
: type_annot option -> type_annot option -> type_annot option tzresult
= fun annot1 annot2 ->
@ -164,7 +130,6 @@ let parse_annots loc l =
| '@' -> ok (`Var_annot (String.sub s 1 @@ String.length s - 1) :: acc)
| ':' -> ok (`Type_annot (String.sub s 1 @@ String.length s - 1) :: acc)
| '%' -> ok (`Field_annot (String.sub s 1 @@ String.length s - 1) :: acc)
| '$' -> ok (`Binding_annot (String.sub s 1 @@ String.length s - 1) :: acc)
| _ -> error (Unexpected_annotation loc)
| exception Invalid_argument _ -> error (Unexpected_annotation loc)
end
@ -249,15 +214,14 @@ let parse_field_annot loc annot =
Lwt.return (parse_field_annot loc annot)
let classify_annot
: annot list -> var_annot list * type_annot list * field_annot list * binding_annot list
: annot list -> var_annot list * type_annot list * field_annot list
= fun l ->
let rv, rt, rf, rb = List.fold_left (fun (rv, rt, rf, rb) -> function
| `Var_annot _ as a -> a :: rv, rt, rf, rb
| `Type_annot _ as a -> rv, a :: rt, rf, rb
| `Field_annot _ as a -> rv, rt, a :: rf, rb
| `Binding_annot _ as a -> rv, rt, rf, a :: rb
) ([], [], [], []) l in
List.rev rv, List.rev rt, List.rev rf, List.rev rb
let rv, rt, rf = List.fold_left (fun (rv, rt, rf) -> function
| `Var_annot _ as a -> a :: rv, rt, rf
| `Type_annot _ as a -> rv, a :: rt, rf
| `Field_annot _ as a -> rv, rt, a :: rf
) ([], [], []) l in
List.rev rv, List.rev rt, List.rev rf
let get_one_annot loc = function
| [] -> Lwt.return (ok None)
@ -275,52 +239,27 @@ let parse_constr_annot
(var_annot option * type_annot option * field_annot option * field_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc bindings >>=? fun () ->
let vars, types, fields = classify_annot annot in
get_one_annot loc vars >>=? fun v ->
get_one_annot loc types >>=? fun t ->
get_two_annot loc fields >>|? fun (f1, f2) ->
(v, t, f1, f2)
let parse_map_annot
: int -> string list ->
(var_annot option * type_annot option * binding_annot option * binding_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc fields >>=? fun () ->
get_one_annot loc vars >>=? fun v ->
get_one_annot loc types >>=? fun t ->
get_two_annot loc bindings >>|? fun (b1, b2) ->
(v, t, b1, b2)
let parse_two_var_annot
: int -> string list -> (var_annot option * var_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc bindings >>=? fun () ->
let vars, types, fields = classify_annot annot in
fail_unexpected_annot loc types >>=? fun () ->
fail_unexpected_annot loc fields >>=? fun () ->
get_two_annot loc vars
let parse_two_binding_annot
: int -> string list -> (binding_annot option * binding_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc vars >>=? fun () ->
fail_unexpected_annot loc types >>=? fun () ->
fail_unexpected_annot loc fields >>=? fun () ->
get_two_annot loc bindings
let parse_var_field_annot
: int -> string list -> (var_annot option * field_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
let vars, types, fields = classify_annot annot in
fail_unexpected_annot loc types >>=? fun () ->
fail_unexpected_annot loc bindings >>=? fun () ->
get_one_annot loc vars >>=? fun v ->
get_one_annot loc fields >>|? fun f ->
(v, f)
@ -329,42 +268,8 @@ let parse_var_type_annot
: int -> string list -> (var_annot option * type_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
let vars, types, fields = classify_annot annot in
fail_unexpected_annot loc fields >>=? fun () ->
fail_unexpected_annot loc bindings >>=? fun () ->
get_one_annot loc vars >>=? fun v ->
get_one_annot loc types >>|? fun t ->
(v, t)
let parse_binding_annot
: int -> string list -> binding_annot option tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc vars >>=? fun () ->
fail_unexpected_annot loc types >>=? fun () ->
fail_unexpected_annot loc fields >>=? fun () ->
get_one_annot loc bindings
let parse_var_binding_annot
: int -> string list -> (var_annot option * binding_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc types >>=? fun () ->
fail_unexpected_annot loc fields >>=? fun () ->
get_one_annot loc vars >>=? fun v ->
get_one_annot loc bindings >>|? fun b ->
(v, b)
let parse_var_type_binding_annot
: int -> string list ->
(var_annot option * type_annot option * binding_annot option) tzresult Lwt.t
= fun loc annot ->
Lwt.return (parse_annots loc annot) >>=? fun annot ->
let vars, types, fields, bindings = classify_annot annot in
fail_unexpected_annot loc fields >>=? fun () ->
get_one_annot loc vars >>=? fun v ->
get_one_annot loc types >>=? fun t ->
get_one_annot loc bindings >>|? fun b ->
(v, t, b)

45
src/proto_alpha/lib_protocol/src/script_ir_annot.mli
View File

@ -18,6 +18,7 @@ val default_balance_annot : var_annot option
val default_steps_annot : var_annot option
val default_source_annot : var_annot option
val default_self_annot : var_annot option
val default_arg_annot : var_annot option
val default_param_annot : field_annot option
val default_storage_annot : field_annot option
@ -27,28 +28,24 @@ val default_contract_annot : field_annot option
val default_addr_annot : field_annot option
val default_manager_annot : field_annot option
val default_arg_annot : binding_annot option
val default_elt_annot : binding_annot option
val default_key_annot : binding_annot option
val default_hd_annot : binding_annot option
val default_some_annot : binding_annot option
val default_left_annot : binding_annot option
val default_right_annot : binding_annot option
val default_elt_annot : field_annot option
val default_key_annot : field_annot option
val default_hd_annot : field_annot option
val default_tl_annot : field_annot option
val default_some_annot : field_annot option
val default_left_annot : field_annot option
val default_right_annot : field_annot option
val default_binding_annot : field_annot option
(** Unparse annotations to their string representation *)
val unparse_type_annot : type_annot option -> string list
val unparse_var_annot : var_annot option -> string list
val unparse_field_annot : field_annot option -> string list
val unparse_binding_annot : binding_annot option -> string list
(** Convertions functions between different annotation kinds *)
val field_to_var_annot : field_annot option -> var_annot option
val field_to_binding_annot : field_annot option -> binding_annot option
val binding_to_var_annot : binding_annot option -> var_annot option
val binding_to_field_annot : binding_annot option -> field_annot option
val var_to_binding_annot : var_annot option -> binding_annot option
val type_to_field_annot : type_annot option -> field_annot option
val var_to_field_annot : var_annot option -> field_annot option
@ -60,12 +57,6 @@ val gen_access_annot :
var_annot option ->
?default:field_annot option -> field_annot option -> var_annot option
(** Generate a binding annotation, of the form $var.some *)
val gen_binding_access_annot :
var_annot option ->
?default:binding_annot option ->
binding_annot option -> binding_annot option
(** Merge type annotations.
@returns an error {!Inconsistent_type_annotations} if they are both present
and different *)
@ -127,29 +118,11 @@ val parse_constr_annot :
int -> string list ->
(var_annot option * type_annot option * field_annot option * field_annot option) tzresult Lwt.t
val parse_map_annot :
int -> string list ->
(var_annot option * type_annot option * binding_annot option * binding_annot option) tzresult Lwt.t
val parse_two_var_annot :
int -> string list -> (var_annot option * var_annot option) tzresult Lwt.t
val parse_two_binding_annot :
int -> string list ->
(binding_annot option * binding_annot option) tzresult Lwt.t
val parse_var_field_annot :
int -> string list -> (var_annot option * field_annot option) tzresult Lwt.t
val parse_var_type_annot :
int -> string list -> (var_annot option * type_annot option) tzresult Lwt.t
val parse_binding_annot :
int -> string list -> binding_annot option tzresult Lwt.t
val parse_var_binding_annot :
int -> string list -> (var_annot option * binding_annot option) tzresult Lwt.t
val parse_var_type_binding_annot :
int -> string list ->
(var_annot option * type_annot option * binding_annot option) tzresult Lwt.t

89
src/proto_alpha/lib_protocol/src/script_ir_translator.ml
View File

@ -1491,11 +1491,8 @@ and parse_instr
(Item_t (Option_t ((t, some_field), _none_field, _), rest, option_annot) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () ->
parse_binding_annot loc annot >>=? fun binding_annot ->
let binding_annot = default_annot binding_annot
~default:(gen_binding_access_annot option_annot (field_to_binding_annot some_field)
~default:default_some_annot) in
let annot = binding_to_var_annot binding_annot in
fail_unexpected_annot loc annot >>=? fun () ->
let annot = gen_access_annot option_annot some_field ~default:default_some_annot in
parse_instr ?type_logger tc_context ctxt bt rest >>=? fun (btr, ctxt) ->
parse_instr ?type_logger tc_context ctxt bf (Item_t (t, rest, annot)) >>=? fun (bfr, ctxt) ->
let branch ibt ibf =
@ -1537,17 +1534,9 @@ and parse_instr
(Item_t (Union_t ((tl, l_field), (tr, r_field), _), rest, union_annot) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () ->
parse_two_binding_annot loc annot >>=? fun (left_bind_annot, right_bind_annot) ->
let left_bind_annot = default_annot left_bind_annot
~default:(gen_binding_access_annot union_annot
(field_to_binding_annot l_field)
~default:default_left_annot) in
let left_annot = binding_to_var_annot left_bind_annot in
let right_bind_annot = default_annot right_bind_annot
~default:(gen_binding_access_annot union_annot
(field_to_binding_annot r_field)
~default:default_right_annot) in
let right_annot = binding_to_var_annot right_bind_annot in
fail_unexpected_annot loc annot >>=? fun () ->
let left_annot = gen_access_annot union_annot l_field ~default:default_left_annot in
let right_annot = gen_access_annot union_annot r_field ~default:default_right_annot in
parse_instr ?type_logger tc_context ctxt bt (Item_t (tl, rest, left_annot)) >>=? fun (btr, ctxt) ->
parse_instr ?type_logger tc_context ctxt bf (Item_t (tr, rest, right_annot)) >>=? fun (bfr, ctxt) ->
let branch ibt ibf =
@ -1566,15 +1555,15 @@ and parse_instr
parse_var_annot loc annot >>=? fun annot ->
typed ctxt loc Cons_list (Item_t (List_t (t, ty_name), rest, annot))
| Prim (loc, I_IF_CONS, [ bt ; bf ], annot),
(Item_t (List_t (t, _), rest, list_annot) as bef) ->
(Item_t (List_t (t, ty_name), rest, list_annot) as bef) ->
check_kind [ Seq_kind ] bt >>=? fun () ->
check_kind [ Seq_kind ] bf >>=? fun () ->
parse_binding_annot loc annot >>=? fun hd_bind_annot ->
let hd_bind_annot = default_annot hd_bind_annot
~default:(gen_binding_access_annot list_annot default_hd_annot) in
let hd_annot = binding_to_var_annot hd_bind_annot in
fail_unexpected_annot loc annot >>=? fun () ->
let hd_annot = gen_access_annot list_annot default_hd_annot in
let tl_annot = gen_access_annot list_annot default_tl_annot in
parse_instr ?type_logger tc_context ctxt bt
(Item_t (t, bef, hd_annot)) >>=? fun (btr, ctxt) ->
(Item_t (t, Item_t (List_t (t, ty_name), rest, tl_annot), hd_annot))
>>=? fun (btr, ctxt) ->
parse_instr ?type_logger tc_context ctxt bf
rest >>=? fun (bfr, ctxt) ->
let branch ibt ibf =
@ -1588,11 +1577,9 @@ and parse_instr
| Prim (loc, I_MAP, [ body ], annot),
(Item_t (List_t (elt, _), starting_rest, list_annot)) ->
check_kind [ Seq_kind ] body >>=? fun () ->
parse_var_type_binding_annot loc annot
>>=? fun (ret_annot, list_ty_name, elt_bind_annot) ->
let elt_bind_annot = default_annot elt_bind_annot
~default:(gen_binding_access_annot list_annot default_elt_annot) in
let elt_annot = binding_to_var_annot elt_bind_annot in
parse_var_type_annot loc annot
>>=? fun (ret_annot, list_ty_name) ->
let elt_annot = gen_access_annot list_annot default_elt_annot in
parse_instr ?type_logger tc_context ctxt
body (Item_t (elt, starting_rest, elt_annot)) >>=? begin fun (judgement, ctxt) ->
match judgement with
@ -1609,10 +1596,8 @@ and parse_instr
| Prim (loc, I_ITER, [ body ], annot),
Item_t (List_t (elt, _), rest, list_annot) ->
check_kind [ Seq_kind ] body >>=? fun () ->
parse_binding_annot loc annot >>=? fun elt_bind_annot ->
let elt_bind_annot = default_annot elt_bind_annot
~default:(gen_binding_access_annot list_annot default_elt_annot) in
let elt_annot = binding_to_var_annot elt_bind_annot in
fail_unexpected_annot loc annot >>=? fun () ->
let elt_annot = gen_access_annot list_annot default_elt_annot in
parse_instr ?type_logger tc_context ctxt
body (Item_t (elt, rest, elt_annot)) >>=? begin fun (judgement, ctxt) ->
match judgement with
@ -1634,10 +1619,8 @@ and parse_instr
| Prim (loc, I_ITER, [ body ], annot),
Item_t (Set_t (comp_elt, _), rest, set_annot) ->
check_kind [ Seq_kind ] body >>=? fun () ->
parse_binding_annot loc annot >>=? fun elt_bind_annot ->
let elt_bind_annot = default_annot elt_bind_annot
~default:(gen_binding_access_annot set_annot default_elt_annot) in
let elt_annot = binding_to_var_annot elt_bind_annot in
fail_unexpected_annot loc annot >>=? fun () ->
let elt_annot = gen_access_annot set_annot default_elt_annot in
let elt = ty_of_comparable_ty comp_elt in
parse_instr ?type_logger tc_context ctxt
body (Item_t (elt, rest, elt_annot)) >>=? begin fun (judgement, ctxt) ->
@ -1675,14 +1658,14 @@ and parse_instr
parse_var_type_annot loc annot >>=? fun (annot, ty_name) ->
typed ctxt loc (Empty_map (tk, tv)) (Item_t (Map_t (tk, tv, ty_name), stack, annot))
| Prim (loc, I_MAP, [ body ], annot),
Item_t (Map_t (ck, elt, _), starting_rest, _map_annot) ->
Item_t (Map_t (ck, elt, _), starting_rest, map_annot) ->
let k = ty_of_comparable_ty ck in
check_kind [ Seq_kind ] body >>=? fun () ->
parse_map_annot loc annot >>=? fun (ret_annot, ty_name, key_bind_annot, elt_bind_annot) ->
let key_field = default_annot key_bind_annot ~default:default_key_annot |> binding_to_field_annot in
let elt_field = default_annot elt_bind_annot ~default:default_elt_annot |> binding_to_field_annot in
parse_var_type_annot loc annot >>=? fun (ret_annot, ty_name) ->
let binding_annot = gen_access_annot map_annot default_binding_annot in
parse_instr ?type_logger tc_context ctxt
body (Item_t (Pair_t ((k, key_field), (elt, elt_field), None), starting_rest, None)) >>=? begin fun (judgement, ctxt) ->
body (Item_t (Pair_t ((k, default_key_annot), (elt, default_elt_annot), None),
starting_rest, binding_annot)) >>=? begin fun (judgement, ctxt) ->
match judgement with
| Typed ({ aft = Item_t (ret, rest, _) ; _ } as ibody) ->
let invalid_map_body = Invalid_map_body (loc, ibody.aft) in
@ -1695,14 +1678,14 @@ and parse_instr
| Failed _ -> fail (Invalid_map_block_fail loc)
end
| Prim (loc, I_ITER, [ body ], annot),
Item_t (Map_t (comp_elt, element_ty, _), rest, _) ->
Item_t (Map_t (comp_elt, element_ty, _), rest, map_annot) ->
check_kind [ Seq_kind ] body >>=? fun () ->
parse_two_binding_annot loc annot >>=? fun (key_bind_annot, elt_bind_annot) ->
let key_field = default_annot key_bind_annot ~default:default_key_annot |> binding_to_field_annot in
let elt_field = default_annot elt_bind_annot ~default:default_elt_annot |> binding_to_field_annot in
fail_unexpected_annot loc annot >>=? fun () ->
let binding_annot = gen_access_annot map_annot default_binding_annot in
let key = ty_of_comparable_ty comp_elt in
parse_instr ?type_logger tc_context ctxt body
(Item_t (Pair_t ((key, key_field), (element_ty, elt_field), None), rest, None))
(Item_t (Pair_t ((key, default_key_annot), (element_ty, default_elt_annot), None),
rest, binding_annot))
>>=? begin fun (judgement, ctxt) -> match judgement with
| Typed ({ aft ; _ } as ibody) ->
let invalid_iter_body = Invalid_iter_body (loc, rest, ibody.aft) in
@ -1828,10 +1811,8 @@ and parse_instr
| Prim (loc, I_LOOP_LEFT, [ body ], annot),
(Item_t (Union_t ((tl, l_field), (tr, _), _), rest, union_annot) as stack) ->
check_kind [ Seq_kind ] body >>=? fun () ->
parse_binding_annot loc annot >>=? fun l_bind_annot ->
let l_bind_annot = default_annot l_bind_annot
~default:(gen_binding_access_annot union_annot (field_to_binding_annot l_field)) in
let l_annot = binding_to_var_annot l_bind_annot in
parse_var_annot loc annot >>=? fun annot ->
let l_annot = gen_access_annot union_annot l_field ~default:default_left_annot in
parse_instr ?type_logger tc_context ctxt body
(Item_t (tl, rest, l_annot)) >>=? begin fun (judgement, ctxt) -> match judgement with
| Typed ibody ->
@ -1839,10 +1820,10 @@ and parse_instr
trace unmatched_branches
(Lwt.return (stack_ty_eq 1 ibody.aft stack) >>=? fun Eq ->
Lwt.return (merge_stacks loc ibody.aft stack) >>=? fun _stack ->
typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, None)))
typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, annot)))
| Failed { descr } ->
let ibody = descr stack in
typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, None))
typed ctxt loc (Loop_left ibody) (Item_t (tr, rest, annot))
end
| Prim (loc, I_LAMBDA, [ arg ; ret ; code ], annot),
stack ->
@ -1851,11 +1832,9 @@ and parse_instr
(Lwt.return (parse_ty ~allow_big_map:false ~allow_operation:true ret))
>>=? fun (Ex_ty ret) ->
check_kind [ Seq_kind ] code >>=? fun () ->
parse_var_binding_annot loc annot >>=? fun (annot, arg_bind_annot) ->
let arg_bind_annot = default_annot arg_bind_annot ~default:default_arg_annot in
let arg_annot = binding_to_var_annot arg_bind_annot in
parse_var_annot loc annot >>=? fun annot ->
parse_returning Lambda ?type_logger ctxt
(arg, arg_annot) ret code >>=? fun (lambda, ctxt) ->
(arg, default_arg_annot) ret code >>=? fun (lambda, ctxt) ->
typed ctxt loc (Lambda lambda) (Item_t (Lambda_t (arg, ret, None), stack, annot))
| Prim (loc, I_EXEC, [], annot),
Item_t (arg, Item_t (Lambda_t (param, ret, _), rest, _), _) ->

3
src/proto_alpha/lib_protocol/src/script_typed_ir.ml
View File

@ -15,9 +15,8 @@ open Script_int
type var_annot = [ `Var_annot of string ]
type type_annot = [ `Type_annot of string ]
type field_annot = [ `Field_annot of string ]
type binding_annot = [ `Binding_annot of string ]
type annot = [ var_annot | type_annot | field_annot | binding_annot ]
type annot = [ var_annot | type_annot | field_annot ]
type 'ty comparable_ty =
| Int_key : type_annot option -> (z num) comparable_ty