🍬 Michelson_v1_primitives.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Inductive prim : Set :=
| K_parameter : prim
| K_storage : prim
| K_code : prim
| K_view : prim
| D_False : prim
| D_Elt : prim
| D_Left : prim
| D_None : prim
| D_Pair : prim
| D_Right : prim
| D_Some : prim
| D_True : prim
| D_Unit : prim
| D_Lambda_rec : prim
| I_PACK : prim
| I_UNPACK : prim
| I_BLAKE2B : prim
| I_SHA256 : prim
| I_SHA512 : prim
| I_ABS : prim
| I_ADD : prim
| I_AMOUNT : prim
| I_AND : prim
| I_BALANCE : prim
| I_CAR : prim
| I_CDR : prim
| I_CHAIN_ID : prim
| I_CHECK_SIGNATURE : prim
| I_COMPARE : prim
| I_CONCAT : prim
| I_CONS : prim
| I_CREATE_ACCOUNT : prim
| I_CREATE_CONTRACT : prim
| I_IMPLICIT_ACCOUNT : prim
| I_DIP : prim
| I_DROP : prim
| I_DUP : prim
| I_VIEW : prim
| I_EDIV : prim
| I_EMPTY_BIG_MAP : prim
| I_EMPTY_MAP : prim
| I_EMPTY_SET : prim
| I_EQ : prim
| I_EXEC : prim
| I_APPLY : prim
| I_FAILWITH : prim
| I_GE : prim
| I_GET : prim
| I_GET_AND_UPDATE : prim
| I_GT : prim
| I_HASH_KEY : prim
| I_IF : prim
| I_IF_CONS : prim
| I_IF_LEFT : prim
| I_IF_NONE : prim
| I_INT : prim
| I_LAMBDA : prim
| I_LAMBDA_REC : prim
| I_LE : prim
| I_LEFT : prim
| I_LEVEL : prim
| I_LOOP : prim
| I_LSL : prim
| I_LSR : prim
| I_LT : prim
| I_MAP : prim
| I_MEM : prim
| I_MUL : prim
| I_NEG : prim
| I_NEQ : prim
| I_NIL : prim
| I_NONE : prim
| I_NOT : prim
| I_NOW : prim
| I_MIN_BLOCK_TIME : prim
| I_OR : prim
| I_PAIR : prim
| I_UNPAIR : prim
| I_PUSH : prim
| I_RIGHT : prim
| I_SIZE : prim
| I_SOME : prim
| I_SOURCE : prim
| I_SENDER : prim
| I_SELF : prim
| I_SELF_ADDRESS : prim
| I_SLICE : prim
| I_STEPS_TO_QUOTA : prim
| I_SUB : prim
| I_SUB_MUTEZ : prim
| I_SWAP : prim
| I_TRANSFER_TOKENS : prim
| I_SET_DELEGATE : prim
| I_UNIT : prim
| I_UPDATE : prim
| I_XOR : prim
| I_ITER : prim
| I_LOOP_LEFT : prim
| I_ADDRESS : prim
| I_CONTRACT : prim
| I_ISNAT : prim
| I_CAST : prim
| I_RENAME : prim
| I_SAPLING_EMPTY_STATE : prim
| I_SAPLING_VERIFY_UPDATE : prim
| I_DIG : prim
| I_DUG : prim
| I_NEVER : prim
| I_VOTING_POWER : prim
| I_TOTAL_VOTING_POWER : prim
| I_KECCAK : prim
| I_SHA3 : prim
| I_PAIRING_CHECK : prim
| I_TICKET : prim
| I_TICKET_DEPRECATED : prim
| I_READ_TICKET : prim
| I_SPLIT_TICKET : prim
| I_JOIN_TICKETS : prim
| I_OPEN_CHEST : prim
| I_EMIT : prim
| T_bool : prim
| T_contract : prim
| T_int : prim
| T_key : prim
| T_key_hash : prim
| T_lambda : prim
| T_list : prim
| T_map : prim
| T_big_map : prim
| T_nat : prim
| T_option : prim
| T_or : prim
| T_pair : prim
| T_set : prim
| T_signature : prim
| T_string : prim
| T_bytes : prim
| T_mutez : prim
| T_timestamp : prim
| T_unit : prim
| T_operation : prim
| T_address : prim
| T_tx_rollup_l2_address : prim
| T_sapling_transaction : prim
| T_sapling_transaction_deprecated : prim
| T_sapling_state : prim
| T_chain_id : prim
| T_never : prim
| T_bls12_381_g1 : prim
| T_bls12_381_g2 : prim
| T_bls12_381_fr : prim
| T_ticket : prim
| T_chest_key : prim
| T_chest : prim
| H_constant : prim.
Inductive namespace : Set :=
| Type_namespace : namespace
| Constant_namespace : namespace
| Instr_namespace : namespace
| Keyword_namespace : namespace
| Constant_hash_namespace : namespace.
Definition namespace_value (function_parameter : prim) : namespace :=
match function_parameter with
| (K_code | K_view | K_parameter | K_storage) ⇒ Keyword_namespace
|
(D_Elt | D_False | D_Left | D_None | D_Pair | D_Right | D_Some | D_True |
D_Unit | D_Lambda_rec) ⇒ Constant_namespace
|
(I_ABS | I_ADD | I_ADDRESS | I_AMOUNT | I_AND | I_APPLY | I_BALANCE |
I_BLAKE2B | I_CAR | I_CAST | I_CDR | I_CHAIN_ID | I_CHECK_SIGNATURE |
I_COMPARE | I_CONCAT | I_CONS | I_CONTRACT | I_CREATE_ACCOUNT |
I_CREATE_CONTRACT | I_DIG | I_DIP | I_DROP | I_DUG | I_DUP | I_VIEW | I_EDIV
| I_EMPTY_BIG_MAP | I_EMPTY_MAP | I_EMPTY_SET | I_EQ | I_EXEC | I_FAILWITH |
I_GE | I_GET | I_GET_AND_UPDATE | I_GT | I_HASH_KEY | I_IF | I_IF_CONS |
I_IF_LEFT | I_IF_NONE | I_IMPLICIT_ACCOUNT | I_INT | I_ISNAT | I_ITER |
I_JOIN_TICKETS | I_KECCAK | I_LAMBDA | I_LAMBDA_REC | I_LE | I_LEFT |
I_LEVEL | I_LOOP | I_LOOP_LEFT | I_LSL | I_LSR | I_LT | I_MAP | I_MEM |
I_MUL | I_NEG | I_NEQ | I_NEVER | I_NIL | I_NONE | I_NOT | I_NOW |
I_MIN_BLOCK_TIME | I_OR | I_PACK | I_PAIR | I_PAIRING_CHECK | I_PUSH |
I_READ_TICKET | I_RENAME | I_RIGHT | I_SAPLING_EMPTY_STATE |
I_SAPLING_VERIFY_UPDATE | I_SELF | I_SELF_ADDRESS | I_SENDER |
I_SET_DELEGATE | I_SHA256 | I_SHA512 | I_SHA3 | I_SIZE | I_SLICE | I_SOME |
I_SOURCE | I_SPLIT_TICKET | I_STEPS_TO_QUOTA | I_SUB | I_SUB_MUTEZ | I_SWAP
| I_TICKET | I_TICKET_DEPRECATED | I_TOTAL_VOTING_POWER | I_TRANSFER_TOKENS
| I_UNIT | I_UNPACK | I_UNPAIR | I_UPDATE | I_VOTING_POWER | I_XOR |
I_OPEN_CHEST | I_EMIT) ⇒ Instr_namespace
|
(T_address | T_tx_rollup_l2_address | T_big_map | T_bool | T_bytes |
T_chain_id | T_contract | T_int | T_key | T_key_hash | T_lambda | T_list |
T_map | T_mutez | T_nat | T_never | T_operation | T_option | T_or | T_pair |
T_sapling_state | T_sapling_transaction | T_sapling_transaction_deprecated |
T_set | T_signature | T_string | T_timestamp | T_unit | T_bls12_381_fr |
T_bls12_381_g1 | T_bls12_381_g2 | T_ticket | T_chest_key | T_chest) ⇒
Type_namespace
| H_constant ⇒ Constant_hash_namespace
end.
#[bypass_check(guard)]
Definition valid_case (name : string) : bool :=
let is_lower (function_parameter : ascii) : bool :=
match function_parameter with
|
("_" % char | "a" % char | "b" % char | "c" % char | "d" % char |
"e" % char | "f" % char | "g" % char | "h" % char | "i" % char |
"j" % char | "k" % char | "l" % char | "m" % char | "n" % char |
"o" % char | "p" % char | "q" % char | "r" % char | "s" % char |
"t" % char | "u" % char | "v" % char | "w" % char | "x" % char |
"y" % char | "z" % char) ⇒ true
| _ ⇒ false
end in
let is_upper (function_parameter : ascii) : bool :=
match function_parameter with
|
("_" % char | "A" % char | "B" % char | "C" % char | "D" % char |
"E" % char | "F" % char | "G" % char | "H" % char | "I" % char |
"J" % char | "K" % char | "L" % char | "M" % char | "N" % char |
"O" % char | "P" % char | "Q" % char | "R" % char | "S" % char |
"T" % char | "U" % char | "V" % char | "W" % char | "X" % char |
"Y" % char | "Z" % char) ⇒ true
| _ ⇒ false
end in
let fix for_all (a_value : int) (b_value : int) (f_value : int → bool)
{struct a_value} : bool :=
(a_value >i b_value) ||
((f_value a_value) && (for_all (a_value +i 1) b_value f_value)) in
let len := String.length name in
(len ≠i 0) &&
((Compare.Char.(Compare.S.op_ltgt) (String.get name 0) "_" % char) &&
(((is_upper (String.get name 0)) &&
(for_all 1 (len -i 1)
(fun (i_value : int) ⇒ is_upper (String.get name i_value)))) ||
(((is_upper (String.get name 0)) &&
(for_all 1 (len -i 1)
(fun (i_value : int) ⇒ is_lower (String.get name i_value)))) ||
((is_lower (String.get name 0)) &&
(for_all 1 (len -i 1)
(fun (i_value : int) ⇒ is_lower (String.get name i_value))))))).
Definition string_of_prim (function_parameter : prim) : string :=
match function_parameter with
| K_parameter ⇒ "parameter"
| K_storage ⇒ "storage"
| K_code ⇒ "code"
| K_view ⇒ "view"
| D_False ⇒ "False"
| D_Elt ⇒ "Elt"
| D_Left ⇒ "Left"
| D_None ⇒ "None"
| D_Pair ⇒ "Pair"
| D_Right ⇒ "Right"
| D_Some ⇒ "Some"
| D_True ⇒ "True"
| D_Unit ⇒ "Unit"
| D_Lambda_rec ⇒ "Lambda_rec"
| I_PACK ⇒ "PACK"
| I_UNPACK ⇒ "UNPACK"
| I_BLAKE2B ⇒ "BLAKE2B"
| I_SHA256 ⇒ "SHA256"
| I_SHA512 ⇒ "SHA512"
| I_ABS ⇒ "ABS"
| I_ADD ⇒ "ADD"
| I_AMOUNT ⇒ "AMOUNT"
| I_AND ⇒ "AND"
| I_BALANCE ⇒ "BALANCE"
| I_CAR ⇒ "CAR"
| I_CDR ⇒ "CDR"
| I_CHAIN_ID ⇒ "CHAIN_ID"
| I_CHECK_SIGNATURE ⇒ "CHECK_SIGNATURE"
| I_COMPARE ⇒ "COMPARE"
| I_CONCAT ⇒ "CONCAT"
| I_CONS ⇒ "CONS"
| I_CREATE_ACCOUNT ⇒ "CREATE_ACCOUNT"
| I_CREATE_CONTRACT ⇒ "CREATE_CONTRACT"
| I_IMPLICIT_ACCOUNT ⇒ "IMPLICIT_ACCOUNT"
| I_DIP ⇒ "DIP"
| I_DROP ⇒ "DROP"
| I_DUP ⇒ "DUP"
| I_EDIV ⇒ "EDIV"
| I_EMPTY_BIG_MAP ⇒ "EMPTY_BIG_MAP"
| I_EMPTY_MAP ⇒ "EMPTY_MAP"
| I_EMPTY_SET ⇒ "EMPTY_SET"
| I_EQ ⇒ "EQ"
| I_EXEC ⇒ "EXEC"
| I_APPLY ⇒ "APPLY"
| I_FAILWITH ⇒ "FAILWITH"
| I_GE ⇒ "GE"
| I_GET ⇒ "GET"
| I_GET_AND_UPDATE ⇒ "GET_AND_UPDATE"
| I_GT ⇒ "GT"
| I_HASH_KEY ⇒ "HASH_KEY"
| I_IF ⇒ "IF"
| I_IF_CONS ⇒ "IF_CONS"
| I_IF_LEFT ⇒ "IF_LEFT"
| I_IF_NONE ⇒ "IF_NONE"
| I_INT ⇒ "INT"
| I_LAMBDA ⇒ "LAMBDA"
| I_LAMBDA_REC ⇒ "LAMBDA_REC"
| I_LE ⇒ "LE"
| I_LEFT ⇒ "LEFT"
| I_LEVEL ⇒ "LEVEL"
| I_LOOP ⇒ "LOOP"
| I_LSL ⇒ "LSL"
| I_LSR ⇒ "LSR"
| I_LT ⇒ "LT"
| I_MAP ⇒ "MAP"
| I_MEM ⇒ "MEM"
| I_MUL ⇒ "MUL"
| I_NEG ⇒ "NEG"
| I_NEQ ⇒ "NEQ"
| I_NIL ⇒ "NIL"
| I_NONE ⇒ "NONE"
| I_NOT ⇒ "NOT"
| I_NOW ⇒ "NOW"
| I_MIN_BLOCK_TIME ⇒ "MIN_BLOCK_TIME"
| I_OR ⇒ "OR"
| I_PAIR ⇒ "PAIR"
| I_PUSH ⇒ "PUSH"
| I_RIGHT ⇒ "RIGHT"
| I_SIZE ⇒ "SIZE"
| I_SOME ⇒ "SOME"
| I_SOURCE ⇒ "SOURCE"
| I_SENDER ⇒ "SENDER"
| I_SELF ⇒ "SELF"
| I_SELF_ADDRESS ⇒ "SELF_ADDRESS"
| I_SLICE ⇒ "SLICE"
| I_STEPS_TO_QUOTA ⇒ "STEPS_TO_QUOTA"
| I_SUB ⇒ "SUB"
| I_SUB_MUTEZ ⇒ "SUB_MUTEZ"
| I_SWAP ⇒ "SWAP"
| I_TRANSFER_TOKENS ⇒ "TRANSFER_TOKENS"
| I_SET_DELEGATE ⇒ "SET_DELEGATE"
| I_UNIT ⇒ "UNIT"
| I_UNPAIR ⇒ "UNPAIR"
| I_UPDATE ⇒ "UPDATE"
| I_XOR ⇒ "XOR"
| I_ITER ⇒ "ITER"
| I_LOOP_LEFT ⇒ "LOOP_LEFT"
| I_ADDRESS ⇒ "ADDRESS"
| I_CONTRACT ⇒ "CONTRACT"
| I_ISNAT ⇒ "ISNAT"
| I_CAST ⇒ "CAST"
| I_RENAME ⇒ "RENAME"
| I_SAPLING_EMPTY_STATE ⇒ "SAPLING_EMPTY_STATE"
| I_SAPLING_VERIFY_UPDATE ⇒ "SAPLING_VERIFY_UPDATE"
| I_DIG ⇒ "DIG"
| I_DUG ⇒ "DUG"
| I_NEVER ⇒ "NEVER"
| I_VOTING_POWER ⇒ "VOTING_POWER"
| I_TOTAL_VOTING_POWER ⇒ "TOTAL_VOTING_POWER"
| I_KECCAK ⇒ "KECCAK"
| I_SHA3 ⇒ "SHA3"
| I_PAIRING_CHECK ⇒ "PAIRING_CHECK"
| I_TICKET ⇒ "TICKET"
| I_TICKET_DEPRECATED ⇒ "TICKET_DEPRECATED"
| I_READ_TICKET ⇒ "READ_TICKET"
| I_SPLIT_TICKET ⇒ "SPLIT_TICKET"
| I_JOIN_TICKETS ⇒ "JOIN_TICKETS"
| I_OPEN_CHEST ⇒ "OPEN_CHEST"
| I_EMIT ⇒ "EMIT"
| I_VIEW ⇒ "VIEW"
| T_bool ⇒ "bool"
| T_contract ⇒ "contract"
| T_int ⇒ "int"
| T_key ⇒ "key"
| T_key_hash ⇒ "key_hash"
| T_lambda ⇒ "lambda"
| T_list ⇒ "list"
| T_map ⇒ "map"
| T_big_map ⇒ "big_map"
| T_nat ⇒ "nat"
| T_option ⇒ "option"
| T_or ⇒ "or"
| T_pair ⇒ "pair"
| T_set ⇒ "set"
| T_signature ⇒ "signature"
| T_string ⇒ "string"
| T_bytes ⇒ "bytes"
| T_mutez ⇒ "mutez"
| T_timestamp ⇒ "timestamp"
| T_unit ⇒ "unit"
| T_operation ⇒ "operation"
| T_address ⇒ "address"
| T_tx_rollup_l2_address ⇒ "tx_rollup_l2_address"
| T_sapling_state ⇒ "sapling_state"
| T_sapling_transaction ⇒ "sapling_transaction"
| T_sapling_transaction_deprecated ⇒ "sapling_transaction_deprecated"
| T_chain_id ⇒ "chain_id"
| T_never ⇒ "never"
| T_bls12_381_g1 ⇒ "bls12_381_g1"
| T_bls12_381_g2 ⇒ "bls12_381_g2"
| T_bls12_381_fr ⇒ "bls12_381_fr"
| T_ticket ⇒ "ticket"
| T_chest_key ⇒ "chest_key"
| T_chest ⇒ "chest"
| H_constant ⇒ "constant"
end.
Definition prim_of_string (function_parameter : string) : M? prim :=
match function_parameter with
| "parameter" ⇒ return? K_parameter
| "storage" ⇒ return? K_storage
| "code" ⇒ return? K_code
| "view" ⇒ return? K_view
| "False" ⇒ return? D_False
| "Elt" ⇒ return? D_Elt
| "Left" ⇒ return? D_Left
| "None" ⇒ return? D_None
| "Pair" ⇒ return? D_Pair
| "Right" ⇒ return? D_Right
| "Some" ⇒ return? D_Some
| "True" ⇒ return? D_True
| "Unit" ⇒ return? D_Unit
| "Lambda_rec" ⇒ return? D_Lambda_rec
| "PACK" ⇒ return? I_PACK
| "UNPACK" ⇒ return? I_UNPACK
| "BLAKE2B" ⇒ return? I_BLAKE2B
| "SHA256" ⇒ return? I_SHA256
| "SHA512" ⇒ return? I_SHA512
| "ABS" ⇒ return? I_ABS
| "ADD" ⇒ return? I_ADD
| "AMOUNT" ⇒ return? I_AMOUNT
| "AND" ⇒ return? I_AND
| "BALANCE" ⇒ return? I_BALANCE
| "CAR" ⇒ return? I_CAR
| "CDR" ⇒ return? I_CDR
| "CHAIN_ID" ⇒ return? I_CHAIN_ID
| "CHECK_SIGNATURE" ⇒ return? I_CHECK_SIGNATURE
| "COMPARE" ⇒ return? I_COMPARE
| "CONCAT" ⇒ return? I_CONCAT
| "CONS" ⇒ return? I_CONS
| "CREATE_ACCOUNT" ⇒ return? I_CREATE_ACCOUNT
| "CREATE_CONTRACT" ⇒ return? I_CREATE_CONTRACT
| "IMPLICIT_ACCOUNT" ⇒ return? I_IMPLICIT_ACCOUNT
| "DIP" ⇒ return? I_DIP
| "DROP" ⇒ return? I_DROP
| "DUP" ⇒ return? I_DUP
| "VIEW" ⇒ return? I_VIEW
| "EDIV" ⇒ return? I_EDIV
| "EMPTY_BIG_MAP" ⇒ return? I_EMPTY_BIG_MAP
| "EMPTY_MAP" ⇒ return? I_EMPTY_MAP
| "EMPTY_SET" ⇒ return? I_EMPTY_SET
| "EQ" ⇒ return? I_EQ
| "EXEC" ⇒ return? I_EXEC
| "APPLY" ⇒ return? I_APPLY
| "FAILWITH" ⇒ return? I_FAILWITH
| "GE" ⇒ return? I_GE
| "GET" ⇒ return? I_GET
| "GET_AND_UPDATE" ⇒ return? I_GET_AND_UPDATE
| "GT" ⇒ return? I_GT
| "HASH_KEY" ⇒ return? I_HASH_KEY
| "IF" ⇒ return? I_IF
| "IF_CONS" ⇒ return? I_IF_CONS
| "IF_LEFT" ⇒ return? I_IF_LEFT
| "IF_NONE" ⇒ return? I_IF_NONE
| "INT" ⇒ return? I_INT
| "KECCAK" ⇒ return? I_KECCAK
| "LAMBDA" ⇒ return? I_LAMBDA
| "LAMBDA_REC" ⇒ return? I_LAMBDA_REC
| "LE" ⇒ return? I_LE
| "LEFT" ⇒ return? I_LEFT
| "LEVEL" ⇒ return? I_LEVEL
| "LOOP" ⇒ return? I_LOOP
| "LSL" ⇒ return? I_LSL
| "LSR" ⇒ return? I_LSR
| "LT" ⇒ return? I_LT
| "MAP" ⇒ return? I_MAP
| "MEM" ⇒ return? I_MEM
| "MUL" ⇒ return? I_MUL
| "NEG" ⇒ return? I_NEG
| "NEQ" ⇒ return? I_NEQ
| "NIL" ⇒ return? I_NIL
| "NONE" ⇒ return? I_NONE
| "NOT" ⇒ return? I_NOT
| "NOW" ⇒ return? I_NOW
| "MIN_BLOCK_TIME" ⇒ return? I_MIN_BLOCK_TIME
| "OR" ⇒ return? I_OR
| "PAIR" ⇒ return? I_PAIR
| "UNPAIR" ⇒ return? I_UNPAIR
| "PAIRING_CHECK" ⇒ return? I_PAIRING_CHECK
| "PUSH" ⇒ return? I_PUSH
| "RIGHT" ⇒ return? I_RIGHT
| "SHA3" ⇒ return? I_SHA3
| "SIZE" ⇒ return? I_SIZE
| "SOME" ⇒ return? I_SOME
| "SOURCE" ⇒ return? I_SOURCE
| "SENDER" ⇒ return? I_SENDER
| "SELF" ⇒ return? I_SELF
| "SELF_ADDRESS" ⇒ return? I_SELF_ADDRESS
| "SLICE" ⇒ return? I_SLICE
| "STEPS_TO_QUOTA" ⇒ return? I_STEPS_TO_QUOTA
| "SUB" ⇒ return? I_SUB
| "SUB_MUTEZ" ⇒ return? I_SUB_MUTEZ
| "SWAP" ⇒ return? I_SWAP
| "TRANSFER_TOKENS" ⇒ return? I_TRANSFER_TOKENS
| "SET_DELEGATE" ⇒ return? I_SET_DELEGATE
| "UNIT" ⇒ return? I_UNIT
| "UPDATE" ⇒ return? I_UPDATE
| "XOR" ⇒ return? I_XOR
| "ITER" ⇒ return? I_ITER
| "LOOP_LEFT" ⇒ return? I_LOOP_LEFT
| "ADDRESS" ⇒ return? I_ADDRESS
| "CONTRACT" ⇒ return? I_CONTRACT
| "ISNAT" ⇒ return? I_ISNAT
| "CAST" ⇒ return? I_CAST
| "RENAME" ⇒ return? I_RENAME
| "SAPLING_EMPTY_STATE" ⇒ return? I_SAPLING_EMPTY_STATE
| "SAPLING_VERIFY_UPDATE" ⇒ return? I_SAPLING_VERIFY_UPDATE
| "DIG" ⇒ return? I_DIG
| "DUG" ⇒ return? I_DUG
| "NEVER" ⇒ return? I_NEVER
| "VOTING_POWER" ⇒ return? I_VOTING_POWER
| "TOTAL_VOTING_POWER" ⇒ return? I_TOTAL_VOTING_POWER
| "TICKET" ⇒ return? I_TICKET
| "TICKET_DEPRECATED" ⇒ return? I_TICKET_DEPRECATED
| "READ_TICKET" ⇒ return? I_READ_TICKET
| "SPLIT_TICKET" ⇒ return? I_SPLIT_TICKET
| "JOIN_TICKETS" ⇒ return? I_JOIN_TICKETS
| "OPEN_CHEST" ⇒ return? I_OPEN_CHEST
| "EMIT" ⇒ return? I_EMIT
| "bool" ⇒ return? T_bool
| "contract" ⇒ return? T_contract
| "int" ⇒ return? T_int
| "key" ⇒ return? T_key
| "key_hash" ⇒ return? T_key_hash
| "lambda" ⇒ return? T_lambda
| "list" ⇒ return? T_list
| "map" ⇒ return? T_map
| "big_map" ⇒ return? T_big_map
| "nat" ⇒ return? T_nat
| "option" ⇒ return? T_option
| "or" ⇒ return? T_or
| "pair" ⇒ return? T_pair
| "set" ⇒ return? T_set
| "signature" ⇒ return? T_signature
| "string" ⇒ return? T_string
| "bytes" ⇒ return? T_bytes
| "mutez" ⇒ return? T_mutez
| "timestamp" ⇒ return? T_timestamp
| "unit" ⇒ return? T_unit
| "operation" ⇒ return? T_operation
| "address" ⇒ return? T_address
| "tx_rollup_l2_address" ⇒ return? T_tx_rollup_l2_address
| "sapling_state" ⇒ return? T_sapling_state
| "sapling_transaction" ⇒ return? T_sapling_transaction
| "sapling_transaction_deprecated" ⇒ return? T_sapling_transaction_deprecated
| "chain_id" ⇒ return? T_chain_id
| "never" ⇒ return? T_never
| "bls12_381_g1" ⇒ return? T_bls12_381_g1
| "bls12_381_g2" ⇒ return? T_bls12_381_g2
| "bls12_381_fr" ⇒ return? T_bls12_381_fr
| "ticket" ⇒ return? T_ticket
| "chest_key" ⇒ return? T_chest_key
| "chest" ⇒ return? T_chest
| "constant" ⇒ return? H_constant
| n_value ⇒
if valid_case n_value then
Error_monad.error_value
(Build_extensible "Unknown_primitive_name" string n_value)
else
Error_monad.error_value (Build_extensible "Invalid_case" string n_value)
end.
#[bypass_check(guard)]
Definition prims_of_strings (expr : Micheline.canonical string)
: M? (Micheline.canonical prim) :=
let fix convert
(function_parameter : Micheline.node Micheline.canonical_location string)
{struct function_parameter}
: M? (Micheline.node Micheline.canonical_location prim) :=
match function_parameter with
| Micheline.Int l_value z_value ⇒ return? (Micheline.Int l_value z_value)
| Micheline.String l_value s_value ⇒
return? (Micheline.String l_value s_value)
| Micheline.Bytes l_value b_value ⇒
return? (Micheline.Bytes l_value b_value)
| Micheline.Prim loc_value prim args annot ⇒
let? prim :=
Error_monad.record_trace
(Build_extensible "Invalid_primitive_name"
(Micheline.canonical string × Micheline.canonical_location)
(expr, loc_value)) (prim_of_string prim) in
let? args := List.map_e convert args in
return? (Micheline.Prim loc_value prim args annot)
| Micheline.Seq loc_value args ⇒
let? args := List.map_e convert args in
return? (Micheline.Seq loc_value args)
end in
let? expr := convert (Micheline.root_value expr) in
return? (Micheline.strip_locations expr).
#[bypass_check(guard)]
Definition strings_of_prims (expr : Micheline.canonical prim)
: Micheline.canonical string :=
let fix convert {A : Set} (function_parameter : Micheline.node A prim)
{struct function_parameter} : Micheline.node A string :=
match function_parameter with
| Micheline.Int l_value z_value ⇒ Micheline.Int l_value z_value
| Micheline.String l_value s_value ⇒ Micheline.String l_value s_value
| Micheline.Bytes l_value b_value ⇒ Micheline.Bytes l_value b_value
| Micheline.Prim loc_value prim args annot ⇒
let prim := string_of_prim prim in
let args := List.map convert args in
Micheline.Prim loc_value prim args annot
| Micheline.Seq loc_value args ⇒
let args := List.map convert args in
Micheline.Seq loc_value args
end in
Micheline.strip_locations (convert (Micheline.root_value expr)).
Definition prim_encoding : Data_encoding.encoding prim :=
Data_encoding.def "michelson.v1.primitives" None None
(Data_encoding.string_enum
[
("parameter", K_parameter);
("storage", K_storage);
("code", K_code);
("False", D_False);
("Elt", D_Elt);
("Left", D_Left);
("None", D_None);
("Pair", D_Pair);
("Right", D_Right);
("Some", D_Some);
("True", D_True);
("Unit", D_Unit);
("PACK", I_PACK);
("UNPACK", I_UNPACK);
("BLAKE2B", I_BLAKE2B);
("SHA256", I_SHA256);
("SHA512", I_SHA512);
("ABS", I_ABS);
("ADD", I_ADD);
("AMOUNT", I_AMOUNT);
("AND", I_AND);
("BALANCE", I_BALANCE);
("CAR", I_CAR);
("CDR", I_CDR);
("CHECK_SIGNATURE", I_CHECK_SIGNATURE);
("COMPARE", I_COMPARE);
("CONCAT", I_CONCAT);
("CONS", I_CONS);
("CREATE_ACCOUNT", I_CREATE_ACCOUNT);
("CREATE_CONTRACT", I_CREATE_CONTRACT);
("IMPLICIT_ACCOUNT", I_IMPLICIT_ACCOUNT);
("DIP", I_DIP);
("DROP", I_DROP);
("DUP", I_DUP);
("EDIV", I_EDIV);
("EMPTY_MAP", I_EMPTY_MAP);
("EMPTY_SET", I_EMPTY_SET);
("EQ", I_EQ);
("EXEC", I_EXEC);
("FAILWITH", I_FAILWITH);
("GE", I_GE);
("GET", I_GET);
("GT", I_GT);
("HASH_KEY", I_HASH_KEY);
("IF", I_IF);
("IF_CONS", I_IF_CONS);
("IF_LEFT", I_IF_LEFT);
("IF_NONE", I_IF_NONE);
("INT", I_INT);
("LAMBDA", I_LAMBDA);
("LE", I_LE);
("LEFT", I_LEFT);
("LOOP", I_LOOP);
("LSL", I_LSL);
("LSR", I_LSR);
("LT", I_LT);
("MAP", I_MAP);
("MEM", I_MEM);
("MUL", I_MUL);
("NEG", I_NEG);
("NEQ", I_NEQ);
("NIL", I_NIL);
("NONE", I_NONE);
("NOT", I_NOT);
("NOW", I_NOW);
("OR", I_OR);
("PAIR", I_PAIR);
("PUSH", I_PUSH);
("RIGHT", I_RIGHT);
("SIZE", I_SIZE);
("SOME", I_SOME);
("SOURCE", I_SOURCE);
("SENDER", I_SENDER);
("SELF", I_SELF);
("STEPS_TO_QUOTA", I_STEPS_TO_QUOTA);
("SUB", I_SUB);
("SWAP", I_SWAP);
("TRANSFER_TOKENS", I_TRANSFER_TOKENS);
("SET_DELEGATE", I_SET_DELEGATE);
("UNIT", I_UNIT);
("UPDATE", I_UPDATE);
("XOR", I_XOR);
("ITER", I_ITER);
("LOOP_LEFT", I_LOOP_LEFT);
("ADDRESS", I_ADDRESS);
("CONTRACT", I_CONTRACT);
("ISNAT", I_ISNAT);
("CAST", I_CAST);
("RENAME", I_RENAME);
("bool", T_bool);
("contract", T_contract);
("int", T_int);
("key", T_key);
("key_hash", T_key_hash);
("lambda", T_lambda);
("list", T_list);
("map", T_map);
("big_map", T_big_map);
("nat", T_nat);
("option", T_option);
("or", T_or);
("pair", T_pair);
("set", T_set);
("signature", T_signature);
("string", T_string);
("bytes", T_bytes);
("mutez", T_mutez);
("timestamp", T_timestamp);
("unit", T_unit);
("operation", T_operation);
("address", T_address);
("SLICE", I_SLICE);
("DIG", I_DIG);
("DUG", I_DUG);
("EMPTY_BIG_MAP", I_EMPTY_BIG_MAP);
("APPLY", I_APPLY);
("chain_id", T_chain_id);
("CHAIN_ID", I_CHAIN_ID);
("LEVEL", I_LEVEL);
("SELF_ADDRESS", I_SELF_ADDRESS);
("never", T_never);
("NEVER", I_NEVER);
("UNPAIR", I_UNPAIR);
("VOTING_POWER", I_VOTING_POWER);
("TOTAL_VOTING_POWER", I_TOTAL_VOTING_POWER);
("KECCAK", I_KECCAK);
("SHA3", I_SHA3);
("PAIRING_CHECK", I_PAIRING_CHECK);
("bls12_381_g1", T_bls12_381_g1);
("bls12_381_g2", T_bls12_381_g2);
("bls12_381_fr", T_bls12_381_fr);
("sapling_state", T_sapling_state);
("sapling_transaction_deprecated", T_sapling_transaction_deprecated);
("SAPLING_EMPTY_STATE", I_SAPLING_EMPTY_STATE);
("SAPLING_VERIFY_UPDATE", I_SAPLING_VERIFY_UPDATE);
("ticket", T_ticket);
("TICKET_DEPRECATED", I_TICKET_DEPRECATED);
("READ_TICKET", I_READ_TICKET);
("SPLIT_TICKET", I_SPLIT_TICKET);
("JOIN_TICKETS", I_JOIN_TICKETS);
("GET_AND_UPDATE", I_GET_AND_UPDATE);
("chest", T_chest);
("chest_key", T_chest_key);
("OPEN_CHEST", I_OPEN_CHEST);
("VIEW", I_VIEW);
("view", K_view);
("constant", H_constant);
("SUB_MUTEZ", I_SUB_MUTEZ);
("tx_rollup_l2_address", T_tx_rollup_l2_address);
("MIN_BLOCK_TIME", I_MIN_BLOCK_TIME);
("sapling_transaction", T_sapling_transaction);
("EMIT", I_EMIT);
("Lambda_rec", D_Lambda_rec);
("LAMBDA_REC", I_LAMBDA_REC);
("TICKET", I_TICKET)
]).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V7.
Inductive prim : Set :=
| K_parameter : prim
| K_storage : prim
| K_code : prim
| K_view : prim
| D_False : prim
| D_Elt : prim
| D_Left : prim
| D_None : prim
| D_Pair : prim
| D_Right : prim
| D_Some : prim
| D_True : prim
| D_Unit : prim
| D_Lambda_rec : prim
| I_PACK : prim
| I_UNPACK : prim
| I_BLAKE2B : prim
| I_SHA256 : prim
| I_SHA512 : prim
| I_ABS : prim
| I_ADD : prim
| I_AMOUNT : prim
| I_AND : prim
| I_BALANCE : prim
| I_CAR : prim
| I_CDR : prim
| I_CHAIN_ID : prim
| I_CHECK_SIGNATURE : prim
| I_COMPARE : prim
| I_CONCAT : prim
| I_CONS : prim
| I_CREATE_ACCOUNT : prim
| I_CREATE_CONTRACT : prim
| I_IMPLICIT_ACCOUNT : prim
| I_DIP : prim
| I_DROP : prim
| I_DUP : prim
| I_VIEW : prim
| I_EDIV : prim
| I_EMPTY_BIG_MAP : prim
| I_EMPTY_MAP : prim
| I_EMPTY_SET : prim
| I_EQ : prim
| I_EXEC : prim
| I_APPLY : prim
| I_FAILWITH : prim
| I_GE : prim
| I_GET : prim
| I_GET_AND_UPDATE : prim
| I_GT : prim
| I_HASH_KEY : prim
| I_IF : prim
| I_IF_CONS : prim
| I_IF_LEFT : prim
| I_IF_NONE : prim
| I_INT : prim
| I_LAMBDA : prim
| I_LAMBDA_REC : prim
| I_LE : prim
| I_LEFT : prim
| I_LEVEL : prim
| I_LOOP : prim
| I_LSL : prim
| I_LSR : prim
| I_LT : prim
| I_MAP : prim
| I_MEM : prim
| I_MUL : prim
| I_NEG : prim
| I_NEQ : prim
| I_NIL : prim
| I_NONE : prim
| I_NOT : prim
| I_NOW : prim
| I_MIN_BLOCK_TIME : prim
| I_OR : prim
| I_PAIR : prim
| I_UNPAIR : prim
| I_PUSH : prim
| I_RIGHT : prim
| I_SIZE : prim
| I_SOME : prim
| I_SOURCE : prim
| I_SENDER : prim
| I_SELF : prim
| I_SELF_ADDRESS : prim
| I_SLICE : prim
| I_STEPS_TO_QUOTA : prim
| I_SUB : prim
| I_SUB_MUTEZ : prim
| I_SWAP : prim
| I_TRANSFER_TOKENS : prim
| I_SET_DELEGATE : prim
| I_UNIT : prim
| I_UPDATE : prim
| I_XOR : prim
| I_ITER : prim
| I_LOOP_LEFT : prim
| I_ADDRESS : prim
| I_CONTRACT : prim
| I_ISNAT : prim
| I_CAST : prim
| I_RENAME : prim
| I_SAPLING_EMPTY_STATE : prim
| I_SAPLING_VERIFY_UPDATE : prim
| I_DIG : prim
| I_DUG : prim
| I_NEVER : prim
| I_VOTING_POWER : prim
| I_TOTAL_VOTING_POWER : prim
| I_KECCAK : prim
| I_SHA3 : prim
| I_PAIRING_CHECK : prim
| I_TICKET : prim
| I_TICKET_DEPRECATED : prim
| I_READ_TICKET : prim
| I_SPLIT_TICKET : prim
| I_JOIN_TICKETS : prim
| I_OPEN_CHEST : prim
| I_EMIT : prim
| T_bool : prim
| T_contract : prim
| T_int : prim
| T_key : prim
| T_key_hash : prim
| T_lambda : prim
| T_list : prim
| T_map : prim
| T_big_map : prim
| T_nat : prim
| T_option : prim
| T_or : prim
| T_pair : prim
| T_set : prim
| T_signature : prim
| T_string : prim
| T_bytes : prim
| T_mutez : prim
| T_timestamp : prim
| T_unit : prim
| T_operation : prim
| T_address : prim
| T_tx_rollup_l2_address : prim
| T_sapling_transaction : prim
| T_sapling_transaction_deprecated : prim
| T_sapling_state : prim
| T_chain_id : prim
| T_never : prim
| T_bls12_381_g1 : prim
| T_bls12_381_g2 : prim
| T_bls12_381_fr : prim
| T_ticket : prim
| T_chest_key : prim
| T_chest : prim
| H_constant : prim.
Inductive namespace : Set :=
| Type_namespace : namespace
| Constant_namespace : namespace
| Instr_namespace : namespace
| Keyword_namespace : namespace
| Constant_hash_namespace : namespace.
Definition namespace_value (function_parameter : prim) : namespace :=
match function_parameter with
| (K_code | K_view | K_parameter | K_storage) ⇒ Keyword_namespace
|
(D_Elt | D_False | D_Left | D_None | D_Pair | D_Right | D_Some | D_True |
D_Unit | D_Lambda_rec) ⇒ Constant_namespace
|
(I_ABS | I_ADD | I_ADDRESS | I_AMOUNT | I_AND | I_APPLY | I_BALANCE |
I_BLAKE2B | I_CAR | I_CAST | I_CDR | I_CHAIN_ID | I_CHECK_SIGNATURE |
I_COMPARE | I_CONCAT | I_CONS | I_CONTRACT | I_CREATE_ACCOUNT |
I_CREATE_CONTRACT | I_DIG | I_DIP | I_DROP | I_DUG | I_DUP | I_VIEW | I_EDIV
| I_EMPTY_BIG_MAP | I_EMPTY_MAP | I_EMPTY_SET | I_EQ | I_EXEC | I_FAILWITH |
I_GE | I_GET | I_GET_AND_UPDATE | I_GT | I_HASH_KEY | I_IF | I_IF_CONS |
I_IF_LEFT | I_IF_NONE | I_IMPLICIT_ACCOUNT | I_INT | I_ISNAT | I_ITER |
I_JOIN_TICKETS | I_KECCAK | I_LAMBDA | I_LAMBDA_REC | I_LE | I_LEFT |
I_LEVEL | I_LOOP | I_LOOP_LEFT | I_LSL | I_LSR | I_LT | I_MAP | I_MEM |
I_MUL | I_NEG | I_NEQ | I_NEVER | I_NIL | I_NONE | I_NOT | I_NOW |
I_MIN_BLOCK_TIME | I_OR | I_PACK | I_PAIR | I_PAIRING_CHECK | I_PUSH |
I_READ_TICKET | I_RENAME | I_RIGHT | I_SAPLING_EMPTY_STATE |
I_SAPLING_VERIFY_UPDATE | I_SELF | I_SELF_ADDRESS | I_SENDER |
I_SET_DELEGATE | I_SHA256 | I_SHA512 | I_SHA3 | I_SIZE | I_SLICE | I_SOME |
I_SOURCE | I_SPLIT_TICKET | I_STEPS_TO_QUOTA | I_SUB | I_SUB_MUTEZ | I_SWAP
| I_TICKET | I_TICKET_DEPRECATED | I_TOTAL_VOTING_POWER | I_TRANSFER_TOKENS
| I_UNIT | I_UNPACK | I_UNPAIR | I_UPDATE | I_VOTING_POWER | I_XOR |
I_OPEN_CHEST | I_EMIT) ⇒ Instr_namespace
|
(T_address | T_tx_rollup_l2_address | T_big_map | T_bool | T_bytes |
T_chain_id | T_contract | T_int | T_key | T_key_hash | T_lambda | T_list |
T_map | T_mutez | T_nat | T_never | T_operation | T_option | T_or | T_pair |
T_sapling_state | T_sapling_transaction | T_sapling_transaction_deprecated |
T_set | T_signature | T_string | T_timestamp | T_unit | T_bls12_381_fr |
T_bls12_381_g1 | T_bls12_381_g2 | T_ticket | T_chest_key | T_chest) ⇒
Type_namespace
| H_constant ⇒ Constant_hash_namespace
end.
#[bypass_check(guard)]
Definition valid_case (name : string) : bool :=
let is_lower (function_parameter : ascii) : bool :=
match function_parameter with
|
("_" % char | "a" % char | "b" % char | "c" % char | "d" % char |
"e" % char | "f" % char | "g" % char | "h" % char | "i" % char |
"j" % char | "k" % char | "l" % char | "m" % char | "n" % char |
"o" % char | "p" % char | "q" % char | "r" % char | "s" % char |
"t" % char | "u" % char | "v" % char | "w" % char | "x" % char |
"y" % char | "z" % char) ⇒ true
| _ ⇒ false
end in
let is_upper (function_parameter : ascii) : bool :=
match function_parameter with
|
("_" % char | "A" % char | "B" % char | "C" % char | "D" % char |
"E" % char | "F" % char | "G" % char | "H" % char | "I" % char |
"J" % char | "K" % char | "L" % char | "M" % char | "N" % char |
"O" % char | "P" % char | "Q" % char | "R" % char | "S" % char |
"T" % char | "U" % char | "V" % char | "W" % char | "X" % char |
"Y" % char | "Z" % char) ⇒ true
| _ ⇒ false
end in
let fix for_all (a_value : int) (b_value : int) (f_value : int → bool)
{struct a_value} : bool :=
(a_value >i b_value) ||
((f_value a_value) && (for_all (a_value +i 1) b_value f_value)) in
let len := String.length name in
(len ≠i 0) &&
((Compare.Char.(Compare.S.op_ltgt) (String.get name 0) "_" % char) &&
(((is_upper (String.get name 0)) &&
(for_all 1 (len -i 1)
(fun (i_value : int) ⇒ is_upper (String.get name i_value)))) ||
(((is_upper (String.get name 0)) &&
(for_all 1 (len -i 1)
(fun (i_value : int) ⇒ is_lower (String.get name i_value)))) ||
((is_lower (String.get name 0)) &&
(for_all 1 (len -i 1)
(fun (i_value : int) ⇒ is_lower (String.get name i_value))))))).
Definition string_of_prim (function_parameter : prim) : string :=
match function_parameter with
| K_parameter ⇒ "parameter"
| K_storage ⇒ "storage"
| K_code ⇒ "code"
| K_view ⇒ "view"
| D_False ⇒ "False"
| D_Elt ⇒ "Elt"
| D_Left ⇒ "Left"
| D_None ⇒ "None"
| D_Pair ⇒ "Pair"
| D_Right ⇒ "Right"
| D_Some ⇒ "Some"
| D_True ⇒ "True"
| D_Unit ⇒ "Unit"
| D_Lambda_rec ⇒ "Lambda_rec"
| I_PACK ⇒ "PACK"
| I_UNPACK ⇒ "UNPACK"
| I_BLAKE2B ⇒ "BLAKE2B"
| I_SHA256 ⇒ "SHA256"
| I_SHA512 ⇒ "SHA512"
| I_ABS ⇒ "ABS"
| I_ADD ⇒ "ADD"
| I_AMOUNT ⇒ "AMOUNT"
| I_AND ⇒ "AND"
| I_BALANCE ⇒ "BALANCE"
| I_CAR ⇒ "CAR"
| I_CDR ⇒ "CDR"
| I_CHAIN_ID ⇒ "CHAIN_ID"
| I_CHECK_SIGNATURE ⇒ "CHECK_SIGNATURE"
| I_COMPARE ⇒ "COMPARE"
| I_CONCAT ⇒ "CONCAT"
| I_CONS ⇒ "CONS"
| I_CREATE_ACCOUNT ⇒ "CREATE_ACCOUNT"
| I_CREATE_CONTRACT ⇒ "CREATE_CONTRACT"
| I_IMPLICIT_ACCOUNT ⇒ "IMPLICIT_ACCOUNT"
| I_DIP ⇒ "DIP"
| I_DROP ⇒ "DROP"
| I_DUP ⇒ "DUP"
| I_EDIV ⇒ "EDIV"
| I_EMPTY_BIG_MAP ⇒ "EMPTY_BIG_MAP"
| I_EMPTY_MAP ⇒ "EMPTY_MAP"
| I_EMPTY_SET ⇒ "EMPTY_SET"
| I_EQ ⇒ "EQ"
| I_EXEC ⇒ "EXEC"
| I_APPLY ⇒ "APPLY"
| I_FAILWITH ⇒ "FAILWITH"
| I_GE ⇒ "GE"
| I_GET ⇒ "GET"
| I_GET_AND_UPDATE ⇒ "GET_AND_UPDATE"
| I_GT ⇒ "GT"
| I_HASH_KEY ⇒ "HASH_KEY"
| I_IF ⇒ "IF"
| I_IF_CONS ⇒ "IF_CONS"
| I_IF_LEFT ⇒ "IF_LEFT"
| I_IF_NONE ⇒ "IF_NONE"
| I_INT ⇒ "INT"
| I_LAMBDA ⇒ "LAMBDA"
| I_LAMBDA_REC ⇒ "LAMBDA_REC"
| I_LE ⇒ "LE"
| I_LEFT ⇒ "LEFT"
| I_LEVEL ⇒ "LEVEL"
| I_LOOP ⇒ "LOOP"
| I_LSL ⇒ "LSL"
| I_LSR ⇒ "LSR"
| I_LT ⇒ "LT"
| I_MAP ⇒ "MAP"
| I_MEM ⇒ "MEM"
| I_MUL ⇒ "MUL"
| I_NEG ⇒ "NEG"
| I_NEQ ⇒ "NEQ"
| I_NIL ⇒ "NIL"
| I_NONE ⇒ "NONE"
| I_NOT ⇒ "NOT"
| I_NOW ⇒ "NOW"
| I_MIN_BLOCK_TIME ⇒ "MIN_BLOCK_TIME"
| I_OR ⇒ "OR"
| I_PAIR ⇒ "PAIR"
| I_PUSH ⇒ "PUSH"
| I_RIGHT ⇒ "RIGHT"
| I_SIZE ⇒ "SIZE"
| I_SOME ⇒ "SOME"
| I_SOURCE ⇒ "SOURCE"
| I_SENDER ⇒ "SENDER"
| I_SELF ⇒ "SELF"
| I_SELF_ADDRESS ⇒ "SELF_ADDRESS"
| I_SLICE ⇒ "SLICE"
| I_STEPS_TO_QUOTA ⇒ "STEPS_TO_QUOTA"
| I_SUB ⇒ "SUB"
| I_SUB_MUTEZ ⇒ "SUB_MUTEZ"
| I_SWAP ⇒ "SWAP"
| I_TRANSFER_TOKENS ⇒ "TRANSFER_TOKENS"
| I_SET_DELEGATE ⇒ "SET_DELEGATE"
| I_UNIT ⇒ "UNIT"
| I_UNPAIR ⇒ "UNPAIR"
| I_UPDATE ⇒ "UPDATE"
| I_XOR ⇒ "XOR"
| I_ITER ⇒ "ITER"
| I_LOOP_LEFT ⇒ "LOOP_LEFT"
| I_ADDRESS ⇒ "ADDRESS"
| I_CONTRACT ⇒ "CONTRACT"
| I_ISNAT ⇒ "ISNAT"
| I_CAST ⇒ "CAST"
| I_RENAME ⇒ "RENAME"
| I_SAPLING_EMPTY_STATE ⇒ "SAPLING_EMPTY_STATE"
| I_SAPLING_VERIFY_UPDATE ⇒ "SAPLING_VERIFY_UPDATE"
| I_DIG ⇒ "DIG"
| I_DUG ⇒ "DUG"
| I_NEVER ⇒ "NEVER"
| I_VOTING_POWER ⇒ "VOTING_POWER"
| I_TOTAL_VOTING_POWER ⇒ "TOTAL_VOTING_POWER"
| I_KECCAK ⇒ "KECCAK"
| I_SHA3 ⇒ "SHA3"
| I_PAIRING_CHECK ⇒ "PAIRING_CHECK"
| I_TICKET ⇒ "TICKET"
| I_TICKET_DEPRECATED ⇒ "TICKET_DEPRECATED"
| I_READ_TICKET ⇒ "READ_TICKET"
| I_SPLIT_TICKET ⇒ "SPLIT_TICKET"
| I_JOIN_TICKETS ⇒ "JOIN_TICKETS"
| I_OPEN_CHEST ⇒ "OPEN_CHEST"
| I_EMIT ⇒ "EMIT"
| I_VIEW ⇒ "VIEW"
| T_bool ⇒ "bool"
| T_contract ⇒ "contract"
| T_int ⇒ "int"
| T_key ⇒ "key"
| T_key_hash ⇒ "key_hash"
| T_lambda ⇒ "lambda"
| T_list ⇒ "list"
| T_map ⇒ "map"
| T_big_map ⇒ "big_map"
| T_nat ⇒ "nat"
| T_option ⇒ "option"
| T_or ⇒ "or"
| T_pair ⇒ "pair"
| T_set ⇒ "set"
| T_signature ⇒ "signature"
| T_string ⇒ "string"
| T_bytes ⇒ "bytes"
| T_mutez ⇒ "mutez"
| T_timestamp ⇒ "timestamp"
| T_unit ⇒ "unit"
| T_operation ⇒ "operation"
| T_address ⇒ "address"
| T_tx_rollup_l2_address ⇒ "tx_rollup_l2_address"
| T_sapling_state ⇒ "sapling_state"
| T_sapling_transaction ⇒ "sapling_transaction"
| T_sapling_transaction_deprecated ⇒ "sapling_transaction_deprecated"
| T_chain_id ⇒ "chain_id"
| T_never ⇒ "never"
| T_bls12_381_g1 ⇒ "bls12_381_g1"
| T_bls12_381_g2 ⇒ "bls12_381_g2"
| T_bls12_381_fr ⇒ "bls12_381_fr"
| T_ticket ⇒ "ticket"
| T_chest_key ⇒ "chest_key"
| T_chest ⇒ "chest"
| H_constant ⇒ "constant"
end.
Definition prim_of_string (function_parameter : string) : M? prim :=
match function_parameter with
| "parameter" ⇒ return? K_parameter
| "storage" ⇒ return? K_storage
| "code" ⇒ return? K_code
| "view" ⇒ return? K_view
| "False" ⇒ return? D_False
| "Elt" ⇒ return? D_Elt
| "Left" ⇒ return? D_Left
| "None" ⇒ return? D_None
| "Pair" ⇒ return? D_Pair
| "Right" ⇒ return? D_Right
| "Some" ⇒ return? D_Some
| "True" ⇒ return? D_True
| "Unit" ⇒ return? D_Unit
| "Lambda_rec" ⇒ return? D_Lambda_rec
| "PACK" ⇒ return? I_PACK
| "UNPACK" ⇒ return? I_UNPACK
| "BLAKE2B" ⇒ return? I_BLAKE2B
| "SHA256" ⇒ return? I_SHA256
| "SHA512" ⇒ return? I_SHA512
| "ABS" ⇒ return? I_ABS
| "ADD" ⇒ return? I_ADD
| "AMOUNT" ⇒ return? I_AMOUNT
| "AND" ⇒ return? I_AND
| "BALANCE" ⇒ return? I_BALANCE
| "CAR" ⇒ return? I_CAR
| "CDR" ⇒ return? I_CDR
| "CHAIN_ID" ⇒ return? I_CHAIN_ID
| "CHECK_SIGNATURE" ⇒ return? I_CHECK_SIGNATURE
| "COMPARE" ⇒ return? I_COMPARE
| "CONCAT" ⇒ return? I_CONCAT
| "CONS" ⇒ return? I_CONS
| "CREATE_ACCOUNT" ⇒ return? I_CREATE_ACCOUNT
| "CREATE_CONTRACT" ⇒ return? I_CREATE_CONTRACT
| "IMPLICIT_ACCOUNT" ⇒ return? I_IMPLICIT_ACCOUNT
| "DIP" ⇒ return? I_DIP
| "DROP" ⇒ return? I_DROP
| "DUP" ⇒ return? I_DUP
| "VIEW" ⇒ return? I_VIEW
| "EDIV" ⇒ return? I_EDIV
| "EMPTY_BIG_MAP" ⇒ return? I_EMPTY_BIG_MAP
| "EMPTY_MAP" ⇒ return? I_EMPTY_MAP
| "EMPTY_SET" ⇒ return? I_EMPTY_SET
| "EQ" ⇒ return? I_EQ
| "EXEC" ⇒ return? I_EXEC
| "APPLY" ⇒ return? I_APPLY
| "FAILWITH" ⇒ return? I_FAILWITH
| "GE" ⇒ return? I_GE
| "GET" ⇒ return? I_GET
| "GET_AND_UPDATE" ⇒ return? I_GET_AND_UPDATE
| "GT" ⇒ return? I_GT
| "HASH_KEY" ⇒ return? I_HASH_KEY
| "IF" ⇒ return? I_IF
| "IF_CONS" ⇒ return? I_IF_CONS
| "IF_LEFT" ⇒ return? I_IF_LEFT
| "IF_NONE" ⇒ return? I_IF_NONE
| "INT" ⇒ return? I_INT
| "KECCAK" ⇒ return? I_KECCAK
| "LAMBDA" ⇒ return? I_LAMBDA
| "LAMBDA_REC" ⇒ return? I_LAMBDA_REC
| "LE" ⇒ return? I_LE
| "LEFT" ⇒ return? I_LEFT
| "LEVEL" ⇒ return? I_LEVEL
| "LOOP" ⇒ return? I_LOOP
| "LSL" ⇒ return? I_LSL
| "LSR" ⇒ return? I_LSR
| "LT" ⇒ return? I_LT
| "MAP" ⇒ return? I_MAP
| "MEM" ⇒ return? I_MEM
| "MUL" ⇒ return? I_MUL
| "NEG" ⇒ return? I_NEG
| "NEQ" ⇒ return? I_NEQ
| "NIL" ⇒ return? I_NIL
| "NONE" ⇒ return? I_NONE
| "NOT" ⇒ return? I_NOT
| "NOW" ⇒ return? I_NOW
| "MIN_BLOCK_TIME" ⇒ return? I_MIN_BLOCK_TIME
| "OR" ⇒ return? I_OR
| "PAIR" ⇒ return? I_PAIR
| "UNPAIR" ⇒ return? I_UNPAIR
| "PAIRING_CHECK" ⇒ return? I_PAIRING_CHECK
| "PUSH" ⇒ return? I_PUSH
| "RIGHT" ⇒ return? I_RIGHT
| "SHA3" ⇒ return? I_SHA3
| "SIZE" ⇒ return? I_SIZE
| "SOME" ⇒ return? I_SOME
| "SOURCE" ⇒ return? I_SOURCE
| "SENDER" ⇒ return? I_SENDER
| "SELF" ⇒ return? I_SELF
| "SELF_ADDRESS" ⇒ return? I_SELF_ADDRESS
| "SLICE" ⇒ return? I_SLICE
| "STEPS_TO_QUOTA" ⇒ return? I_STEPS_TO_QUOTA
| "SUB" ⇒ return? I_SUB
| "SUB_MUTEZ" ⇒ return? I_SUB_MUTEZ
| "SWAP" ⇒ return? I_SWAP
| "TRANSFER_TOKENS" ⇒ return? I_TRANSFER_TOKENS
| "SET_DELEGATE" ⇒ return? I_SET_DELEGATE
| "UNIT" ⇒ return? I_UNIT
| "UPDATE" ⇒ return? I_UPDATE
| "XOR" ⇒ return? I_XOR
| "ITER" ⇒ return? I_ITER
| "LOOP_LEFT" ⇒ return? I_LOOP_LEFT
| "ADDRESS" ⇒ return? I_ADDRESS
| "CONTRACT" ⇒ return? I_CONTRACT
| "ISNAT" ⇒ return? I_ISNAT
| "CAST" ⇒ return? I_CAST
| "RENAME" ⇒ return? I_RENAME
| "SAPLING_EMPTY_STATE" ⇒ return? I_SAPLING_EMPTY_STATE
| "SAPLING_VERIFY_UPDATE" ⇒ return? I_SAPLING_VERIFY_UPDATE
| "DIG" ⇒ return? I_DIG
| "DUG" ⇒ return? I_DUG
| "NEVER" ⇒ return? I_NEVER
| "VOTING_POWER" ⇒ return? I_VOTING_POWER
| "TOTAL_VOTING_POWER" ⇒ return? I_TOTAL_VOTING_POWER
| "TICKET" ⇒ return? I_TICKET
| "TICKET_DEPRECATED" ⇒ return? I_TICKET_DEPRECATED
| "READ_TICKET" ⇒ return? I_READ_TICKET
| "SPLIT_TICKET" ⇒ return? I_SPLIT_TICKET
| "JOIN_TICKETS" ⇒ return? I_JOIN_TICKETS
| "OPEN_CHEST" ⇒ return? I_OPEN_CHEST
| "EMIT" ⇒ return? I_EMIT
| "bool" ⇒ return? T_bool
| "contract" ⇒ return? T_contract
| "int" ⇒ return? T_int
| "key" ⇒ return? T_key
| "key_hash" ⇒ return? T_key_hash
| "lambda" ⇒ return? T_lambda
| "list" ⇒ return? T_list
| "map" ⇒ return? T_map
| "big_map" ⇒ return? T_big_map
| "nat" ⇒ return? T_nat
| "option" ⇒ return? T_option
| "or" ⇒ return? T_or
| "pair" ⇒ return? T_pair
| "set" ⇒ return? T_set
| "signature" ⇒ return? T_signature
| "string" ⇒ return? T_string
| "bytes" ⇒ return? T_bytes
| "mutez" ⇒ return? T_mutez
| "timestamp" ⇒ return? T_timestamp
| "unit" ⇒ return? T_unit
| "operation" ⇒ return? T_operation
| "address" ⇒ return? T_address
| "tx_rollup_l2_address" ⇒ return? T_tx_rollup_l2_address
| "sapling_state" ⇒ return? T_sapling_state
| "sapling_transaction" ⇒ return? T_sapling_transaction
| "sapling_transaction_deprecated" ⇒ return? T_sapling_transaction_deprecated
| "chain_id" ⇒ return? T_chain_id
| "never" ⇒ return? T_never
| "bls12_381_g1" ⇒ return? T_bls12_381_g1
| "bls12_381_g2" ⇒ return? T_bls12_381_g2
| "bls12_381_fr" ⇒ return? T_bls12_381_fr
| "ticket" ⇒ return? T_ticket
| "chest_key" ⇒ return? T_chest_key
| "chest" ⇒ return? T_chest
| "constant" ⇒ return? H_constant
| n_value ⇒
if valid_case n_value then
Error_monad.error_value
(Build_extensible "Unknown_primitive_name" string n_value)
else
Error_monad.error_value (Build_extensible "Invalid_case" string n_value)
end.
#[bypass_check(guard)]
Definition prims_of_strings (expr : Micheline.canonical string)
: M? (Micheline.canonical prim) :=
let fix convert
(function_parameter : Micheline.node Micheline.canonical_location string)
{struct function_parameter}
: M? (Micheline.node Micheline.canonical_location prim) :=
match function_parameter with
| Micheline.Int l_value z_value ⇒ return? (Micheline.Int l_value z_value)
| Micheline.String l_value s_value ⇒
return? (Micheline.String l_value s_value)
| Micheline.Bytes l_value b_value ⇒
return? (Micheline.Bytes l_value b_value)
| Micheline.Prim loc_value prim args annot ⇒
let? prim :=
Error_monad.record_trace
(Build_extensible "Invalid_primitive_name"
(Micheline.canonical string × Micheline.canonical_location)
(expr, loc_value)) (prim_of_string prim) in
let? args := List.map_e convert args in
return? (Micheline.Prim loc_value prim args annot)
| Micheline.Seq loc_value args ⇒
let? args := List.map_e convert args in
return? (Micheline.Seq loc_value args)
end in
let? expr := convert (Micheline.root_value expr) in
return? (Micheline.strip_locations expr).
#[bypass_check(guard)]
Definition strings_of_prims (expr : Micheline.canonical prim)
: Micheline.canonical string :=
let fix convert {A : Set} (function_parameter : Micheline.node A prim)
{struct function_parameter} : Micheline.node A string :=
match function_parameter with
| Micheline.Int l_value z_value ⇒ Micheline.Int l_value z_value
| Micheline.String l_value s_value ⇒ Micheline.String l_value s_value
| Micheline.Bytes l_value b_value ⇒ Micheline.Bytes l_value b_value
| Micheline.Prim loc_value prim args annot ⇒
let prim := string_of_prim prim in
let args := List.map convert args in
Micheline.Prim loc_value prim args annot
| Micheline.Seq loc_value args ⇒
let args := List.map convert args in
Micheline.Seq loc_value args
end in
Micheline.strip_locations (convert (Micheline.root_value expr)).
Definition prim_encoding : Data_encoding.encoding prim :=
Data_encoding.def "michelson.v1.primitives" None None
(Data_encoding.string_enum
[
("parameter", K_parameter);
("storage", K_storage);
("code", K_code);
("False", D_False);
("Elt", D_Elt);
("Left", D_Left);
("None", D_None);
("Pair", D_Pair);
("Right", D_Right);
("Some", D_Some);
("True", D_True);
("Unit", D_Unit);
("PACK", I_PACK);
("UNPACK", I_UNPACK);
("BLAKE2B", I_BLAKE2B);
("SHA256", I_SHA256);
("SHA512", I_SHA512);
("ABS", I_ABS);
("ADD", I_ADD);
("AMOUNT", I_AMOUNT);
("AND", I_AND);
("BALANCE", I_BALANCE);
("CAR", I_CAR);
("CDR", I_CDR);
("CHECK_SIGNATURE", I_CHECK_SIGNATURE);
("COMPARE", I_COMPARE);
("CONCAT", I_CONCAT);
("CONS", I_CONS);
("CREATE_ACCOUNT", I_CREATE_ACCOUNT);
("CREATE_CONTRACT", I_CREATE_CONTRACT);
("IMPLICIT_ACCOUNT", I_IMPLICIT_ACCOUNT);
("DIP", I_DIP);
("DROP", I_DROP);
("DUP", I_DUP);
("EDIV", I_EDIV);
("EMPTY_MAP", I_EMPTY_MAP);
("EMPTY_SET", I_EMPTY_SET);
("EQ", I_EQ);
("EXEC", I_EXEC);
("FAILWITH", I_FAILWITH);
("GE", I_GE);
("GET", I_GET);
("GT", I_GT);
("HASH_KEY", I_HASH_KEY);
("IF", I_IF);
("IF_CONS", I_IF_CONS);
("IF_LEFT", I_IF_LEFT);
("IF_NONE", I_IF_NONE);
("INT", I_INT);
("LAMBDA", I_LAMBDA);
("LE", I_LE);
("LEFT", I_LEFT);
("LOOP", I_LOOP);
("LSL", I_LSL);
("LSR", I_LSR);
("LT", I_LT);
("MAP", I_MAP);
("MEM", I_MEM);
("MUL", I_MUL);
("NEG", I_NEG);
("NEQ", I_NEQ);
("NIL", I_NIL);
("NONE", I_NONE);
("NOT", I_NOT);
("NOW", I_NOW);
("OR", I_OR);
("PAIR", I_PAIR);
("PUSH", I_PUSH);
("RIGHT", I_RIGHT);
("SIZE", I_SIZE);
("SOME", I_SOME);
("SOURCE", I_SOURCE);
("SENDER", I_SENDER);
("SELF", I_SELF);
("STEPS_TO_QUOTA", I_STEPS_TO_QUOTA);
("SUB", I_SUB);
("SWAP", I_SWAP);
("TRANSFER_TOKENS", I_TRANSFER_TOKENS);
("SET_DELEGATE", I_SET_DELEGATE);
("UNIT", I_UNIT);
("UPDATE", I_UPDATE);
("XOR", I_XOR);
("ITER", I_ITER);
("LOOP_LEFT", I_LOOP_LEFT);
("ADDRESS", I_ADDRESS);
("CONTRACT", I_CONTRACT);
("ISNAT", I_ISNAT);
("CAST", I_CAST);
("RENAME", I_RENAME);
("bool", T_bool);
("contract", T_contract);
("int", T_int);
("key", T_key);
("key_hash", T_key_hash);
("lambda", T_lambda);
("list", T_list);
("map", T_map);
("big_map", T_big_map);
("nat", T_nat);
("option", T_option);
("or", T_or);
("pair", T_pair);
("set", T_set);
("signature", T_signature);
("string", T_string);
("bytes", T_bytes);
("mutez", T_mutez);
("timestamp", T_timestamp);
("unit", T_unit);
("operation", T_operation);
("address", T_address);
("SLICE", I_SLICE);
("DIG", I_DIG);
("DUG", I_DUG);
("EMPTY_BIG_MAP", I_EMPTY_BIG_MAP);
("APPLY", I_APPLY);
("chain_id", T_chain_id);
("CHAIN_ID", I_CHAIN_ID);
("LEVEL", I_LEVEL);
("SELF_ADDRESS", I_SELF_ADDRESS);
("never", T_never);
("NEVER", I_NEVER);
("UNPAIR", I_UNPAIR);
("VOTING_POWER", I_VOTING_POWER);
("TOTAL_VOTING_POWER", I_TOTAL_VOTING_POWER);
("KECCAK", I_KECCAK);
("SHA3", I_SHA3);
("PAIRING_CHECK", I_PAIRING_CHECK);
("bls12_381_g1", T_bls12_381_g1);
("bls12_381_g2", T_bls12_381_g2);
("bls12_381_fr", T_bls12_381_fr);
("sapling_state", T_sapling_state);
("sapling_transaction_deprecated", T_sapling_transaction_deprecated);
("SAPLING_EMPTY_STATE", I_SAPLING_EMPTY_STATE);
("SAPLING_VERIFY_UPDATE", I_SAPLING_VERIFY_UPDATE);
("ticket", T_ticket);
("TICKET_DEPRECATED", I_TICKET_DEPRECATED);
("READ_TICKET", I_READ_TICKET);
("SPLIT_TICKET", I_SPLIT_TICKET);
("JOIN_TICKETS", I_JOIN_TICKETS);
("GET_AND_UPDATE", I_GET_AND_UPDATE);
("chest", T_chest);
("chest_key", T_chest_key);
("OPEN_CHEST", I_OPEN_CHEST);
("VIEW", I_VIEW);
("view", K_view);
("constant", H_constant);
("SUB_MUTEZ", I_SUB_MUTEZ);
("tx_rollup_l2_address", T_tx_rollup_l2_address);
("MIN_BLOCK_TIME", I_MIN_BLOCK_TIME);
("sapling_transaction", T_sapling_transaction);
("EMIT", I_EMIT);
("Lambda_rec", D_Lambda_rec);
("LAMBDA_REC", I_LAMBDA_REC);
("TICKET", I_TICKET)
]).
Init function; without side-effects in Coq
Definition init_module : unit :=
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.unknown_primitive_name" "Unknown primitive name"
"In a script or data expression, a primitive was unknown."
(Some
(fun (ppf : Format.formatter) ⇒
fun (n_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Unknown primitive "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Unknown primitive %s.") n_value))
(Data_encoding.obj1
(Data_encoding.req None None "wrong_primitive_name"
Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unknown_primitive_name" then
let got := cast string payload in
Some got
else None
end)
(fun (got : string) ⇒
Build_extensible "Unknown_primitive_name" string got) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.invalid_primitive_name_case" "Invalid primitive name case"
"In a script or data expression, a primitive name is neither uppercase, lowercase or capitalized."
(Some
(fun (ppf : Format.formatter) ⇒
fun (n_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Primitive "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" has invalid case."
CamlinternalFormatBasics.End_of_format)))
"Primitive %s has invalid case.") n_value))
(Data_encoding.obj1
(Data_encoding.req None None "wrong_primitive_name"
Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_case" then
let name := cast string payload in
Some name
else None
end)
(fun (name : string) ⇒ Build_extensible "Invalid_case" string name) in
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.invalid_primitive_name" "Invalid primitive name"
"In a script or data expression, a primitive name is unknown or has a wrong case."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Micheline.canonical string × Micheline.canonical_location) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Invalid primitive."
CamlinternalFormatBasics.End_of_format) "Invalid primitive.")))
(Data_encoding.obj2
(Data_encoding.req None None "expression"
(Micheline.canonical_encoding "generic" Data_encoding.string_value))
(Data_encoding.req None None "location"
Micheline.canonical_location_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_primitive_name" then
let '(expr, loc_value) :=
cast (Micheline.canonical string × Micheline.canonical_location)
payload in
Some (expr, loc_value)
else None
end)
(fun (function_parameter :
Micheline.canonical string × Micheline.canonical_location) ⇒
let '(expr, loc_value) := function_parameter in
Build_extensible "Invalid_primitive_name"
(Micheline.canonical string × Micheline.canonical_location)
(expr, loc_value)).
Definition string_of_namespace (function_parameter : namespace) : string :=
match function_parameter with
| Type_namespace ⇒ "T"
| Constant_namespace ⇒ "D"
| Instr_namespace ⇒ "I"
| Keyword_namespace ⇒ "K"
| Constant_hash_namespace ⇒ "H"
end.
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.unknown_primitive_name" "Unknown primitive name"
"In a script or data expression, a primitive was unknown."
(Some
(fun (ppf : Format.formatter) ⇒
fun (n_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Unknown primitive "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.Char_literal "." % char
CamlinternalFormatBasics.End_of_format)))
"Unknown primitive %s.") n_value))
(Data_encoding.obj1
(Data_encoding.req None None "wrong_primitive_name"
Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Unknown_primitive_name" then
let got := cast string payload in
Some got
else None
end)
(fun (got : string) ⇒
Build_extensible "Unknown_primitive_name" string got) in
let '_ :=
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.invalid_primitive_name_case" "Invalid primitive name case"
"In a script or data expression, a primitive name is neither uppercase, lowercase or capitalized."
(Some
(fun (ppf : Format.formatter) ⇒
fun (n_value : string) ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Primitive "
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
(CamlinternalFormatBasics.String_literal
" has invalid case."
CamlinternalFormatBasics.End_of_format)))
"Primitive %s has invalid case.") n_value))
(Data_encoding.obj1
(Data_encoding.req None None "wrong_primitive_name"
Data_encoding.string_value))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_case" then
let name := cast string payload in
Some name
else None
end)
(fun (name : string) ⇒ Build_extensible "Invalid_case" string name) in
Error_monad.register_error_kind Error_monad.Permanent
"michelson_v1.invalid_primitive_name" "Invalid primitive name"
"In a script or data expression, a primitive name is unknown or has a wrong case."
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter :
Micheline.canonical string × Micheline.canonical_location) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "Invalid primitive."
CamlinternalFormatBasics.End_of_format) "Invalid primitive.")))
(Data_encoding.obj2
(Data_encoding.req None None "expression"
(Micheline.canonical_encoding "generic" Data_encoding.string_value))
(Data_encoding.req None None "location"
Micheline.canonical_location_encoding))
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Invalid_primitive_name" then
let '(expr, loc_value) :=
cast (Micheline.canonical string × Micheline.canonical_location)
payload in
Some (expr, loc_value)
else None
end)
(fun (function_parameter :
Micheline.canonical string × Micheline.canonical_location) ⇒
let '(expr, loc_value) := function_parameter in
Build_extensible "Invalid_primitive_name"
(Micheline.canonical string × Micheline.canonical_location)
(expr, loc_value)).
Definition string_of_namespace (function_parameter : namespace) : string :=
match function_parameter with
| Type_namespace ⇒ "T"
| Constant_namespace ⇒ "D"
| Instr_namespace ⇒ "I"
| Keyword_namespace ⇒ "K"
| Constant_hash_namespace ⇒ "H"
end.