diff --git a/docs/whitedoc/michelson.rst b/docs/whitedoc/michelson.rst index 91b9df21a..2d7dd3d58 100644 --- a/docs/whitedoc/michelson.rst +++ b/docs/whitedoc/michelson.rst @@ -526,6 +526,8 @@ Stack operations :: 'A -> (lambda 'a 'b) : 'A + > LAMBDA _ _ code / S => code : S + Generic comparison ~~~~~~~~~~~~~~~~~~ @@ -779,12 +781,21 @@ constants as is, concatenate them and use them as keys. :: string : string : 'S -> string : 'S + > CONCAT / s : t : S => (s ^ t) : S + - ``COMPARE``: Lexicographic comparison. :: :: string : string : 'S -> int : 'S + > COMPARE / s : t : S => -1 : S + iff s < t + > COMPARE / s : t : S => 0 : S + iff s = t + > COMPARE / s : t : S => 1 : S + iff s > t + Operations on pairs ~~~~~~~~~~~~~~~~~~~ @@ -831,6 +842,15 @@ Operations on sets :: 'elt : set 'elt : 'S -> bool : 'S + > MEM / x : {} : S => false : S + > MEM / x : { hd ; } : S => r : S + iff COMPARE / x : hd : [] => 1 : [] + where MEM / x : v : { } : S => r : S + > MEM / x : { hd ; } : S => true : S + iff COMPARE / x : hd : [] => 0 : [] + > MEM / x : { hd ; } : S => false : S + iff COMPARE / x : hd : [] => -1 : [] + - ``UPDATE``: Inserts or removes an element in a set, replacing a previous value. @@ -838,6 +858,20 @@ Operations on sets :: 'elt : bool : set 'elt : 'S -> set 'elt : 'S + > UPDATE / x : false : {} : S => {} : S + > UPDATE / x : true : {} : S => { x } : S + > UPDATE / x : v : { hd ; } : S => { hd ; } : S + iff COMPARE / x : hd : [] => 1 : [] + where UPDATE / x : v : { } : S => { } : S + > UPDATE / x : false : { hd ; } : S => { } : S + iff COMPARE / x : hd : [] => 0 : [] + > UPDATE / x : true : { hd ; } : S => { hd ; } : S + iff COMPARE / x : hd : [] => 0 : [] + > UPDATE / x : false : { hd ; } : S => { hd ; } : S + iff COMPARE / x : hd : [] => -1 : [] + > UPDATE / x : true : { hd ; } : S => { x ; hd ; } : S + iff COMPARE / x : hd : [] => -1 : [] + - ``REDUCE``: Apply a function on a set passing the result of each application to the next one and return the last. @@ -845,13 +879,20 @@ Operations on sets :: lambda (pair 'elt * 'b) 'b : set 'elt : 'b : 'S -> 'b : 'S + > REDUCE / f : {} : b : S => b : S + > REDUCE / f : { hd : } : b : S => REDUCE / f : { } : c : S + where f / Pair hd b : [] => c : [] + - ``ITER body``: Apply the body expression to each element of a set. The body sequence has access to the stack. :: :: (set 'elt) : 'A -> 'A - iff body :: [ 'elt : 'A -> 'A ] + iff body :: [ 'elt : 'A -> 'A ] + + > ITER body / {} : S => S + > ITER body / { hd ; } : S => body; ITER body / hd : { } : S - ``SIZE``: Get the cardinality of the set. @@ -859,6 +900,10 @@ Operations on sets :: set 'elt : 'S -> nat : 'S + > SIZE / {} : S => 0 : S + > SIZE / { _ ; } : S => 1 + s : S + where SIZE / { } : S => s : S + Operations on maps ~~~~~~~~~~~~~~~~~~ @@ -871,6 +916,9 @@ Operations on maps :: 'S -> map 'key 'val : 'S + > EMPTY_MAP _ _ / S => {} : S + + - ``GET``: Access an element in a map, returns an optional value to be checked with ``IF_SOME``. @@ -878,18 +926,51 @@ Operations on maps :: 'key : map 'key 'val : 'S -> option 'val : 'S -- ``MEM``: Check for the presence of an element in a map. + > GET / x : {} : S => None : S + > GET / x : { Elt k v ; } : S => opt_y : S + iff COMPARE / x : k : [] => 1 : [] + where GET / x : { } : S => opt_y : S + > GET / x : { Elt k v ; } : S => Some v : S + iff COMPARE / x : k : [] => 0 : [] + > GET / x : { Elt k v ; } : S => None : S + iff COMPARE / x : k : [] => -1 : [] + +- ``MEM``: Check for the presence of a binding for a key in a map. :: :: 'key : map 'key 'val : 'S -> bool : 'S + > MEM / x : {} : S => false : S + > MEM / x : { Elt k v ; } : S => r : S + iff COMPARE / x : k : [] => 1 : [] + where MEM / x : { } : S => r : S + > MEM / x : { Elt k v ; } : S => true : S + iff COMPARE / x : k : [] => 0 : [] + > MEM / x : { Elt k v ; } : S => false : S + iff COMPARE / x : k : [] => -1 : [] + - ``UPDATE``: Assign or remove an element in a map. :: :: 'key : option 'val : map 'key 'val : 'S -> map 'key 'val : 'S + > UPDATE / x : None : {} : S => {} : S + > UPDATE / x : Some y : {} : S => { Elt x y } : S + > UPDATE / x : opt_y : { Elt k v ; } : S => { Elt k v ; } : S + iff COMPARE / x : k : [] => 1 : [] + where UPDATE / x : opt_y : { } : S => { } : S + > UPDATE / x : None : { Elt k v ; } : S => { } : S + iff COMPARE / x : k : [] => 0 : [] + > UPDATE / x : Some y : { Elt k v ; } : S => { Elt k y ; } : S + iff COMPARE / x : k : [] => 0 : [] + > UPDATE / x : None : { Elt k v ; } : S => { Elt k v ; } : S + iff COMPARE / x : k : [] => -1 : [] + > UPDATE / x : Some y : { Elt k v ; } : S => { Elt x y ; Elt k v ; } : S + iff COMPARE / x : k : [] => -1 : [] + + - ``MAP``: Apply a function on a map and return the map of results under the same bindings. @@ -897,6 +978,11 @@ Operations on maps :: lambda (pair 'key 'val) 'b : map 'key 'val : 'S -> map 'key 'b : 'S + > MAP / f : {} : S => {} : S + > MAP / f : { Elt k v ; } : S => { Elt k (f (Pair k v)) ; } : S + where MAP / f : { } : S => { } : S + + - ``MAP body``: Apply the body expression to each element of a map. The body sequence has access to the stack. @@ -905,6 +991,11 @@ Operations on maps :: (map 'key 'val) : 'A -> (map 'key 'b) : 'A iff body :: [ (pair 'key 'val) : 'A -> 'b : 'A ] + > MAP body / {} : S => {} : S + > MAP body / { Elt k v ; } : S => { Elt k (body (Pair k v)) ; } : S + where MAP body / { } : S => { } : S + + - ``REDUCE``: Apply a function on a map passing the result of each application to the next one and return the last. @@ -912,6 +1003,10 @@ Operations on maps :: lambda (pair (pair 'key 'val) 'b) 'b : map 'key 'val : 'b : 'S -> 'b : 'S + > REDUCE / f : {} : b : S => b : S + > REDUCE / f : { Elt k v ; } : b : S => REDUCE / f : { } : c : S + where f / Pair (Pair k v) b : [] => c + - ``ITER body``: Apply the body expression to each element of a map. The body sequence has access to the stack. @@ -920,12 +1015,19 @@ Operations on maps :: (map 'elt 'val) : 'A -> 'A iff body :: [ (pair 'elt 'val) : 'A -> 'A ] + > ITER body / {} : S => S + > ITER body / { Elt k v ; } : S => body ; ITER body / (Pair k v) : { } : S + - ``SIZE``: Get the cardinality of the map. :: :: map 'key 'val : 'S -> nat : 'S + > SIZE / {} : S => 0 : S + > SIZE / { _ ; } : S => 1 + s : S + where SIZE / { } : S => s : S + Operations on optional values ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1034,6 +1136,11 @@ Operations on lists :: lambda 'a 'b : list 'a : 'S -> list 'b : 'S + > MAP / f : { a ; } : S => { f a ; } : S + where MAP / f : { } : S => { } : S + > MAP / f : {} : S => {} : S + + - ``MAP body``: Apply the body expression to each element of the list. The body sequence has access to the stack. @@ -1042,6 +1149,11 @@ Operations on lists :: (list 'elt) : 'A -> (list 'b) : 'A iff body :: [ 'elt : 'A -> 'b : 'A ] + > MAP body / { a ; } : S => { body a ; } : S + where MAP body / { } : S => { } : S + > MAP body / {} : S => {} : S + + - ``REDUCE``: Apply a function on a list from left to right passing the result of each application to the next one and return the last. @@ -1049,19 +1161,32 @@ Operations on lists :: lambda (pair 'a 'b) 'b : list 'a : 'b : 'S -> 'b : 'S + > REDUCE / f : { a : } : b : S => REDUCE / f : { } : c : S + where f / Pair a b : [] => c + > REDUCE / f : {} : b : S => b : S + + - ``SIZE``: Get the number of elements in the list. :: :: list 'elt : 'S -> nat : 'S + > SIZE / { _ ; } : S => 1 + s : S + where SIZE / { } : S => s : S + > SIZE / {} : S => 0 : S + + - ``ITER body``: Apply the body expression to each element of a list. The body sequence has access to the stack. :: :: (list 'elt) : 'A -> 'A - iff body :: [ 'elt : 'A -> 'A ] + iff body :: [ 'elt : 'A -> 'A ] + > ITER body / { a ; } : S => body ; ITER body / a : { } : S + > ITER body / {} : S => S + VI - Domain specific data types ------------------------------- @@ -1120,6 +1245,14 @@ retrieved from script parameters or globals. :: timestamp : timestamp : 'S -> int : 'S + > COMPARE / seconds(t1) : seconds(t2) : S => -1 : S + iff t1 < t2 + > COMPARE / seconds(t1) : seconds(t2) : S => 0 : S + iff t1 = t2 + > COMPARE / seconds(t1) : seconds(t2) : S => 1 : S + iff t1 > t2 + + Operations on Tez ~~~~~~~~~~~~~~~~~ @@ -1167,9 +1300,17 @@ types by mistake. They are also mandatory checked for under/overflows. > EDIV ; C / x : y : S => C / Some (Pair (x / y) (x % y)) : S - ``COMPARE``: +:: :: tez : tez : ’S -> int : ’S + > COMPARE / x : y : S => -1 : S + iff x < y + > COMPARE / x : y : S => 0 : S + iff x = y + > COMPARE / x : y : S => 1 : S + iff x > y + Operations on contracts ~~~~~~~~~~~~~~~~~~~~~~~ @@ -1326,6 +1467,13 @@ Cryptographic primitives :: key_hash : key_hash : 'S -> int : 'S + > COMPARE / x : y : S => -1 : S + iff x < y + > COMPARE / x : y : S => 0 : S + iff x = y + > COMPARE / x : y : S => 1 : S + iff x > y + VIII - Macros -------------