Module Archetype.Model

type lident = Ident.ident Location.loced
val pp_lident : Ppx_deriving_runtime.Format.formatter -> lident -> Ppx_deriving_runtime.unit
val show_lident : lident -> Ppx_deriving_runtime.string
type currency =
| Utz
val pp_currency : Ppx_deriving_runtime.Format.formatter -> currency -> Ppx_deriving_runtime.unit
val show_currency : currency -> Ppx_deriving_runtime.string
type container =
| Collection
| Aggregate
| Partition
| View
val pp_container : Ppx_deriving_runtime.Format.formatter -> container -> Ppx_deriving_runtime.unit
val show_container : container -> Ppx_deriving_runtime.string
type btyp =
| Bunit
| Bbool
| Bint
| Brational
| Bdate
| Bduration
| Btimestamp
| Bstring
| Baddress
| Brole
| Bcurrency
| Bsignature
| Bkey
| Bkeyhash
| Bbytes
| Bnat
| Bchainid
| Bbls12_381_fr
| Bbls12_381_g1
| Bbls12_381_g2
| Bnever
val pp_btyp : Ppx_deriving_runtime.Format.formatter -> btyp -> Ppx_deriving_runtime.unit
val show_btyp : btyp -> Ppx_deriving_runtime.string
type vset =
| VSremoved
| VSadded
| VSstable
| VSbefore
| VSafter
| VSfixed
val pp_vset : Ppx_deriving_runtime.Format.formatter -> vset -> Ppx_deriving_runtime.unit
val show_vset : vset -> Ppx_deriving_runtime.string
type trtyp =
| TRentry
| TRaction
| TRasset
| TRfield
val pp_trtyp : Ppx_deriving_runtime.Format.formatter -> trtyp -> Ppx_deriving_runtime.unit
val show_trtyp : trtyp -> Ppx_deriving_runtime.string
type ntype =
| Tasset of lident
| Tenum of lident
| Tstate
| Tbuiltin of btyp
| Tcontainer of type_ * container
| Tlist of type_
| Toption of type_
| Ttuple of type_ list
| Tset of type_
| Tmap of bool * type_ * type_
| Tor of type_ * type_
| Trecord of lident
| Tlambda of type_ * type_
| Tunit
| Tstorage
| Toperation
| Tcontract of type_
| Tprog of type_
| Tvset of vset * type_
| Ttrace of trtyp
| Tticket of type_
| Tsapling_state of int
| Tsapling_transaction of int
and type_ = ntype * lident option
val pp_ntype : Ppx_deriving_runtime.Format.formatter -> ntype -> Ppx_deriving_runtime.unit
val show_ntype : ntype -> Ppx_deriving_runtime.string
val pp_type_ : Ppx_deriving_runtime.Format.formatter -> type_ -> Ppx_deriving_runtime.unit
val show_type_ : type_ -> Ppx_deriving_runtime.string
type 'id pattern_node =
| Pwild
| Pconst of 'id * lident list
val pp_pattern_node : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id pattern_node -> Ppx_deriving_runtime.unit
val show_pattern_node : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id pattern_node -> Ppx_deriving_runtime.string
type 'id pattern_gen = {
node : 'id pattern_node;
loc : Location.t;
}
val pp_pattern_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id pattern_gen -> Ppx_deriving_runtime.unit
val show_pattern_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id pattern_gen -> Ppx_deriving_runtime.string
type pattern = lident pattern_gen
val pp_pattern : Ppx_deriving_runtime.Format.formatter -> pattern -> Ppx_deriving_runtime.unit
val show_pattern : pattern -> Ppx_deriving_runtime.string
type 'id for_ident_gen =
| FIsimple of 'id
| FIdouble of 'id * 'id
val pp_for_ident_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id for_ident_gen -> Ppx_deriving_runtime.unit
val show_for_ident_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id for_ident_gen -> Ppx_deriving_runtime.string
type for_ident = lident for_ident_gen
val pp_for_ident : Ppx_deriving_runtime.Format.formatter -> for_ident -> Ppx_deriving_runtime.unit
val show_for_ident : for_ident -> Ppx_deriving_runtime.string
type comparison_operator =
| Gt
| Ge
| Lt
| Le
val pp_comparison_operator : Ppx_deriving_runtime.Format.formatter -> comparison_operator -> Ppx_deriving_runtime.unit
val show_comparison_operator : comparison_operator -> Ppx_deriving_runtime.string
type rat_arith_op =
| Rplus
| Rminus
| Rmult
| Rdiv
val pp_rat_arith_op : Ppx_deriving_runtime.Format.formatter -> rat_arith_op -> Ppx_deriving_runtime.unit
val show_rat_arith_op : rat_arith_op -> Ppx_deriving_runtime.string
type assignment_operator =
| ValueAssign
| PlusAssign
| MinusAssign
| MultAssign
| DivAssign
| AndAssign
| OrAssign
val pp_assignment_operator : Ppx_deriving_runtime.Format.formatter -> assignment_operator -> Ppx_deriving_runtime.unit
val show_assignment_operator : assignment_operator -> Ppx_deriving_runtime.string
type sort_kind =
| SKasc
| SKdesc
val pp_sort_kind : Ppx_deriving_runtime.Format.formatter -> sort_kind -> Ppx_deriving_runtime.unit
val show_sort_kind : sort_kind -> Ppx_deriving_runtime.string
type ('id, 'term) assign_kind_gen =
| Avar of 'id
| Avarstore of 'id
| Aasset of 'id * 'id * 'term
| Arecord of 'id * 'id * 'term
| Astate
| Aassetstate of Ident.ident * 'term
| Aoperations
val pp_assign_kind_gen : id term. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> ('id'term) assign_kind_gen -> Ppx_deriving_runtime.unit
val show_assign_kind_gen : id term. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> ('id'term) assign_kind_gen -> Ppx_deriving_runtime.string
type 'term var_kind_gen =
| Vassetstate of 'term
| Vstorevar
| Vstorecol
| Vdefinition
| Vlocal
| Vparam
| Vfield
| Vstate
| Vthe
| Vparameter
val pp_var_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'term var_kind_gen -> Ppx_deriving_runtime.unit
val show_var_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> 'term var_kind_gen -> Ppx_deriving_runtime.string
type temp =
| Tbefore
| Tat of Ident.ident
| Tnone
val pp_temp : Ppx_deriving_runtime.Format.formatter -> temp -> Ppx_deriving_runtime.unit
val show_temp : temp -> Ppx_deriving_runtime.string
type delta =
| Dadded
| Dremoved
| Dunmoved
| Dnone
val pp_delta : Ppx_deriving_runtime.Format.formatter -> delta -> Ppx_deriving_runtime.unit
val show_delta : delta -> Ppx_deriving_runtime.string
type 'term container_kind_gen =
| CKcoll of temp * delta
| CKview of 'term
| CKfield of Ident.ident * Ident.ident * 'term * temp * delta
| CKdef of Ident.ident
val pp_container_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'term container_kind_gen -> Ppx_deriving_runtime.unit
val show_container_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> 'term container_kind_gen -> Ppx_deriving_runtime.string
type 'term iter_container_kind_gen =
| ICKcoll of Ident.ident
| ICKview of 'term
| ICKfield of Ident.ident * Ident.ident * 'term
| ICKset of 'term
| ICKlist of 'term
| ICKmap of 'term
val pp_iter_container_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'term iter_container_kind_gen -> Ppx_deriving_runtime.unit
val show_iter_container_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> 'term iter_container_kind_gen -> Ppx_deriving_runtime.string
type 'term transfer_kind_gen =
| TKsimple of 'term * 'term
| TKcall of 'term * Ident.ident * type_ * 'term * 'term
| TKentry of 'term * 'term * 'term
| TKself of 'term * Ident.ident * (Ident.ident * 'term) list
| TKoperation of 'term
val pp_transfer_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'term transfer_kind_gen -> Ppx_deriving_runtime.unit
val show_transfer_kind_gen : term. (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> 'term transfer_kind_gen -> Ppx_deriving_runtime.string
type ('id, 'term) mterm_node =
| Mletin of 'id list * 'term * type_ option * 'term * 'term option
| Mdeclvar of 'id list * type_ option * 'term
| Mapp of 'id * 'term list
| Massign of assignment_operator * type_ * ('id'term) assign_kind_gen * 'term
| Mif of 'term * 'term * 'term option
| Mmatchwith of 'term * ('id pattern_gen * 'term) list
| Minstrmatchoption of 'term * 'id * 'term * 'term
| Minstrmatchor of 'term * 'id * 'term * 'id * 'term
| Minstrmatchlist of 'term * 'id * 'id * 'term * 'term
| Mfor of 'id for_ident_gen * 'term iter_container_kind_gen * 'term * Ident.ident option
| Miter of 'id * 'term * 'term * 'term * Ident.ident option
| Mwhile of 'term * 'term * Ident.ident option
| Mseq of 'term list
| Mreturn of 'term
| Mlabel of 'id
| Mmark of 'id * 'term
| Mfail of 'id fail_type_gen
| Mtransfer of 'term transfer_kind_gen
| Mentrypoint of type_ * 'id * 'term
| Mself of 'id
| Moperations
| Mmkoperation of 'term * 'term * 'term
| Mint of Core.big_int
| Mnat of Core.big_int
| Mbool of bool
| Mrational of Core.big_int * Core.big_int
| Mstring of string
| Mcurrency of Core.big_int * currency
| Maddress of string
| Mdate of Core.date
| Mduration of Core.duration
| Mtimestamp of Core.big_int
| Mbytes of string
| Munit
| Mexprif of 'term * 'term * 'term
| Mexprmatchwith of 'term * ('id pattern_gen * 'term) list
| Mmatchoption of 'term * 'id * 'term * 'term
| Mmatchor of 'term * 'id * 'term * 'id * 'term
| Mmatchlist of 'term * 'id * 'id * 'term * 'term
| Mfold of 'term * 'id * 'term
| Mmap of 'term * 'id * 'term
| Mexeclambda of 'term * 'term
| Mapplylambda of 'term * 'term
| Mleft of type_ * 'term
| Mright of type_ * 'term
| Mnone
| Msome of 'term
| Mtuple of 'term list
| Masset of 'term list
| Massets of 'term list
| Mlitset of 'term list
| Mlitlist of 'term list
| Mlitmap of bool * ('term * 'term) list
| Mlitrecord of (Ident.ident * 'term) list
| Mlambda of type_ * 'id * type_ * 'term
| Mdot of 'term * 'id
| Mdotassetfield of 'id * 'term * 'id
| Mequal of type_ * 'term * 'term
| Mnequal of type_ * 'term * 'term
| Mgt of 'term * 'term
| Mge of 'term * 'term
| Mlt of 'term * 'term
| Mle of 'term * 'term
| Mmulticomp of 'term * (comparison_operator * 'term) list
| Mand of 'term * 'term
| Mor of 'term * 'term
| Mxor of 'term * 'term
| Mnot of 'term
| Mplus of 'term * 'term
| Mminus of 'term * 'term
| Mmult of 'term * 'term
| Mdivrat of 'term * 'term
| Mdiveuc of 'term * 'term
| Mmodulo of 'term * 'term
| Mdivmod of 'term * 'term
| Muminus of 'term
| MthreeWayCmp of 'term * 'term
| Mshiftleft of 'term * 'term
| Mshiftright of 'term * 'term
| Maddasset of Ident.ident * 'term
| Maddfield of Ident.ident * Ident.ident * 'term * 'term
| Mremoveasset of Ident.ident * 'term
| Mremovefield of Ident.ident * Ident.ident * 'term * 'term
| Mremoveall of Ident.ident * Ident.ident * 'term
| Mremoveif of Ident.ident * 'term container_kind_gen * (Ident.ident * type_) list * 'term * 'term list
| Mclear of Ident.ident * 'term container_kind_gen
| Mset of Ident.ident * Ident.ident list * 'term * 'term
| Mupdate of Ident.ident * 'term * ('id * assignment_operator * 'term) list
| Maddupdate of Ident.ident * 'term container_kind_gen * 'term * ('id * assignment_operator * 'term) list
| Maddforce of Ident.ident * 'term
| Mget of Ident.ident * 'term container_kind_gen * 'term
| Mselect of Ident.ident * 'term container_kind_gen * (Ident.ident * type_) list * 'term * 'term list
| Msort of Ident.ident * 'term container_kind_gen * (Ident.ident * sort_kind) list
| Mcontains of Ident.ident * 'term container_kind_gen * 'term
| Mnth of Ident.ident * 'term container_kind_gen * 'term
| Mcount of Ident.ident * 'term container_kind_gen
| Msum of Ident.ident * 'term container_kind_gen * 'term
| Mhead of Ident.ident * 'term container_kind_gen * 'term
| Mtail of Ident.ident * 'term container_kind_gen * 'term
| Mcast of type_ * type_ * 'term
| Mtupleaccess of 'term * Core.big_int
| Mrecupdate of 'term * (Ident.ident * 'term) list
| Msetadd of type_ * 'term * 'term
| Msetremove of type_ * 'term * 'term
| Msetcontains of type_ * 'term * 'term
| Msetlength of type_ * 'term
| Msetfold of type_ * 'id * 'id * 'term * 'term * 'term
| Mlistprepend of type_ * 'term * 'term
| Mlistlength of type_ * 'term
| Mlistcontains of type_ * 'term * 'term
| Mlistnth of type_ * 'term * 'term
| Mlistreverse of type_ * 'term
| Mlistconcat of type_ * 'term * 'term
| Mlistfold of type_ * 'id * 'id * 'term * 'term * 'term
| Mmapput of type_ * type_ * 'term * 'term * 'term
| Mmapremove of type_ * type_ * 'term * 'term
| Mmapget of type_ * type_ * 'term * 'term
| Mmapgetopt of type_ * type_ * 'term * 'term
| Mmapcontains of type_ * type_ * 'term * 'term
| Mmaplength of type_ * type_ * 'term
| Mmapfold of type_ * 'id * 'id * 'id * 'term * 'term * 'term
| Mmin of 'term * 'term
| Mmax of 'term * 'term
| Mabs of 'term
| Mconcat of 'term * 'term
| Mslice of 'term * 'term * 'term
| Mlength of 'term
| Misnone of 'term
| Missome of 'term
| Moptget of 'term
| Mfloor of 'term
| Mceil of 'term
| Mtostring of type_ * 'term
| Mpack of 'term
| Munpack of type_ * 'term
| Mblake2b of 'term
| Msha256 of 'term
| Msha512 of 'term
| Msha3 of 'term
| Mkeccak of 'term
| Mhashkey of 'term
| Mchecksignature of 'term * 'term * 'term
| Mtotalvotingpower
| Mvotingpower of 'term
| Mcreateticket of 'term * 'term
| Mreadticket of 'term
| Msplitticket of 'term * 'term * 'term
| Mjointickets of 'term * 'term
| Msapling_empty_state of int
| Msapling_verify_update of 'term * 'term
| Mpairing_check of 'term
| Mnow
| Mtransferred
| Mcaller
| Mbalance
| Msource
| Mselfaddress
| Mchainid
| Mmetadata
| Mlevel
| Mvar of 'id * 'term var_kind_gen * temp * delta
| Menumval of 'id * 'term list * Ident.ident
| Mrateq of 'term * 'term
| Mratcmp of comparison_operator * 'term * 'term
| Mratarith of rat_arith_op * 'term * 'term
| Mratuminus of 'term
| Mrattez of 'term * 'term
| Mnattoint of 'term
| Mnattorat of 'term
| Minttorat of 'term
| Mratdur of 'term * 'term
| Mforall of 'id * type_ * 'term option * 'term
| Mexists of 'id * type_ * 'term option * 'term
| Mimply of 'term * 'term
| Mequiv of 'term * 'term
| Msetiterated of 'term iter_container_kind_gen
| Msettoiterate of 'term iter_container_kind_gen
| Mempty of Ident.ident
| Msingleton of Ident.ident * 'term
| Msubsetof of Ident.ident * 'term container_kind_gen * 'term
| Misempty of Ident.ident * 'term
| Munion of Ident.ident * 'term * 'term
| Minter of Ident.ident * 'term * 'term
| Mdiff of Ident.ident * 'term * 'term
and assign_kind = (lidentmterm) assign_kind_gen
and var_kind = mterm var_kind_gen
and container_kind = mterm container_kind_gen
and iter_container_kind = mterm iter_container_kind_gen
and transfer_kind = mterm transfer_kind_gen
and 'id mterm_gen = {
node : ('id'id mterm_gen) mterm_node;
type_ : type_;
loc : Location.t;
}
and mterm = lident mterm_gen
and mterm__node = (lidentmterm) mterm_node
and 'id fail_type_gen =
| Invalid of 'id mterm_gen
| InvalidCaller
| InvalidCondition of Ident.ident option
| NoTransfer
| AssignNat
| InvalidState
and fail_type = lident fail_type_gen
and api_container_kind =
| Coll
| View
| Field of Ident.ident * Ident.ident
and api_asset =
| Get of Ident.ident
| Set of Ident.ident
| Add of Ident.ident
| Remove of Ident.ident
| Clear of Ident.ident * api_container_kind
| Update of Ident.ident * (Ident.ident * assignment_operator * mterm) list
| FieldAdd of Ident.ident * Ident.ident
| FieldRemove of Ident.ident * Ident.ident
| RemoveAll of Ident.ident * Ident.ident
| RemoveIf of Ident.ident * api_container_kind * (Ident.ident * type_) list * mterm
| Contains of Ident.ident * api_container_kind
| Nth of Ident.ident * api_container_kind
| Select of Ident.ident * api_container_kind * (Ident.ident * type_) list * mterm
| Sort of Ident.ident * api_container_kind * (Ident.ident * sort_kind) list
| Count of Ident.ident * api_container_kind
| Sum of Ident.ident * api_container_kind * type_ * mterm
| Head of Ident.ident * api_container_kind
| Tail of Ident.ident * api_container_kind
and api_list =
| Lprepend of type_
| Lcontains of type_
| Llength of type_
| Lnth of type_
| Lreverse of type_
and api_builtin =
| Bmin of type_
| Bmax of type_
| Babs of type_
| Bconcat of type_
| Bslice of type_
| Blength of type_
| Bisnone of type_
| Bissome of type_
| Boptget of type_
| Bfloor
| Bceil
| Btostring of type_
| Bfail of type_
and api_internal =
| RatEq
| RatCmp
| RatArith
| RatUminus
| RatTez
| RatDur
and api_storage_node =
| APIAsset of api_asset
| APIList of api_list
| APIBuiltin of api_builtin
| APIInternal of api_internal
and api_loc =
| OnlyFormula
| OnlyExec
| ExecFormula
and api_storage = {
node_item : api_storage_node;
api_loc : api_loc;
}
and api_verif =
| StorageInvariant of Ident.ident * Ident.ident * mterm
and entry_description =
| ADany
| ADadd of Ident.ident
| ADremove of Ident.ident
| ADupdate of Ident.ident
| ADtransfer of Ident.ident
| ADget of Ident.ident
| ADiterate of Ident.ident
| ADcall of Ident.ident
and security_role = lident
and security_entry =
| Sany
| Sentry of lident list
val pp_mterm_node : id term. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> ('id'term) mterm_node -> Ppx_deriving_runtime.unit
val show_mterm_node : id term. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> (Ppx_deriving_runtime.Format.formatter -> 'term -> Ppx_deriving_runtime.unit) -> ('id'term) mterm_node -> Ppx_deriving_runtime.string
val pp_assign_kind : Ppx_deriving_runtime.Format.formatter -> assign_kind -> Ppx_deriving_runtime.unit
val show_assign_kind : assign_kind -> Ppx_deriving_runtime.string
val pp_var_kind : Ppx_deriving_runtime.Format.formatter -> var_kind -> Ppx_deriving_runtime.unit
val show_var_kind : var_kind -> Ppx_deriving_runtime.string
val pp_container_kind : Ppx_deriving_runtime.Format.formatter -> container_kind -> Ppx_deriving_runtime.unit
val show_container_kind : container_kind -> Ppx_deriving_runtime.string
val pp_iter_container_kind : Ppx_deriving_runtime.Format.formatter -> iter_container_kind -> Ppx_deriving_runtime.unit
val show_iter_container_kind : iter_container_kind -> Ppx_deriving_runtime.string
val pp_transfer_kind : Ppx_deriving_runtime.Format.formatter -> transfer_kind -> Ppx_deriving_runtime.unit
val show_transfer_kind : transfer_kind -> Ppx_deriving_runtime.string
val pp_mterm_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id mterm_gen -> Ppx_deriving_runtime.unit
val show_mterm_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id mterm_gen -> Ppx_deriving_runtime.string
val pp_mterm : Ppx_deriving_runtime.Format.formatter -> mterm -> Ppx_deriving_runtime.unit
val show_mterm : mterm -> Ppx_deriving_runtime.string
val pp_mterm__node : Ppx_deriving_runtime.Format.formatter -> mterm__node -> Ppx_deriving_runtime.unit
val show_mterm__node : mterm__node -> Ppx_deriving_runtime.string
val pp_fail_type_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id fail_type_gen -> Ppx_deriving_runtime.unit
val show_fail_type_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id fail_type_gen -> Ppx_deriving_runtime.string
val pp_fail_type : Ppx_deriving_runtime.Format.formatter -> fail_type -> Ppx_deriving_runtime.unit
val show_fail_type : fail_type -> Ppx_deriving_runtime.string
val pp_api_container_kind : Ppx_deriving_runtime.Format.formatter -> api_container_kind -> Ppx_deriving_runtime.unit
val show_api_container_kind : api_container_kind -> Ppx_deriving_runtime.string
val pp_api_asset : Ppx_deriving_runtime.Format.formatter -> api_asset -> Ppx_deriving_runtime.unit
val show_api_asset : api_asset -> Ppx_deriving_runtime.string
val pp_api_list : Ppx_deriving_runtime.Format.formatter -> api_list -> Ppx_deriving_runtime.unit
val show_api_list : api_list -> Ppx_deriving_runtime.string
val pp_api_builtin : Ppx_deriving_runtime.Format.formatter -> api_builtin -> Ppx_deriving_runtime.unit
val show_api_builtin : api_builtin -> Ppx_deriving_runtime.string
val pp_api_internal : Ppx_deriving_runtime.Format.formatter -> api_internal -> Ppx_deriving_runtime.unit
val show_api_internal : api_internal -> Ppx_deriving_runtime.string
val pp_api_storage_node : Ppx_deriving_runtime.Format.formatter -> api_storage_node -> Ppx_deriving_runtime.unit
val show_api_storage_node : api_storage_node -> Ppx_deriving_runtime.string
val pp_api_loc : Ppx_deriving_runtime.Format.formatter -> api_loc -> Ppx_deriving_runtime.unit
val show_api_loc : api_loc -> Ppx_deriving_runtime.string
val pp_api_storage : Ppx_deriving_runtime.Format.formatter -> api_storage -> Ppx_deriving_runtime.unit
val show_api_storage : api_storage -> Ppx_deriving_runtime.string
val pp_api_verif : Ppx_deriving_runtime.Format.formatter -> api_verif -> Ppx_deriving_runtime.unit
val show_api_verif : api_verif -> Ppx_deriving_runtime.string
val pp_entry_description : Ppx_deriving_runtime.Format.formatter -> entry_description -> Ppx_deriving_runtime.unit
val show_entry_description : entry_description -> Ppx_deriving_runtime.string
val pp_security_role : Ppx_deriving_runtime.Format.formatter -> security_role -> Ppx_deriving_runtime.unit
val show_security_role : security_role -> Ppx_deriving_runtime.string
val pp_security_entry : Ppx_deriving_runtime.Format.formatter -> security_entry -> Ppx_deriving_runtime.unit
val show_security_entry : security_entry -> Ppx_deriving_runtime.string
type 'id label_term_gen = {
label : 'id;
term : 'id mterm_gen;
loc : Location.t;
}
val pp_label_term_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id label_term_gen -> Ppx_deriving_runtime.unit
val show_label_term_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id label_term_gen -> Ppx_deriving_runtime.string
type label_term = lident label_term_gen
val pp_label_term : Ppx_deriving_runtime.Format.formatter -> label_term -> Ppx_deriving_runtime.unit
val show_label_term : label_term -> Ppx_deriving_runtime.string
type model_type =
| MTvar
| MTconst
| MTasset of Ident.ident
| MTstate
| MTenum of Ident.ident
val pp_model_type : Ppx_deriving_runtime.Format.formatter -> model_type -> Ppx_deriving_runtime.unit
val show_model_type : model_type -> Ppx_deriving_runtime.string
type 'id storage_item_gen = {
id : 'id;
model_type : model_type;
typ : type_;
const : bool;
ghost : bool;
default : 'id mterm_gen;
loc : Location.t;
}
val pp_storage_item_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id storage_item_gen -> Ppx_deriving_runtime.unit
val show_storage_item_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id storage_item_gen -> Ppx_deriving_runtime.string
type storage_item = lident storage_item_gen
val pp_storage_item : Ppx_deriving_runtime.Format.formatter -> storage_item -> Ppx_deriving_runtime.unit
val show_storage_item : storage_item -> Ppx_deriving_runtime.string
type 'id storage_gen = 'id storage_item_gen list
val pp_storage_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id storage_gen -> Ppx_deriving_runtime.unit
val show_storage_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id storage_gen -> Ppx_deriving_runtime.string
type storage = lident storage_gen
val pp_storage : Ppx_deriving_runtime.Format.formatter -> storage -> Ppx_deriving_runtime.unit
val show_storage : storage -> Ppx_deriving_runtime.string
type 'id enum_item_gen = {
name : 'id;
args : type_ list;
invariants : 'id label_term_gen list;
}
val pp_enum_item_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id enum_item_gen -> Ppx_deriving_runtime.unit
val show_enum_item_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id enum_item_gen -> Ppx_deriving_runtime.string
type enum_item = lident enum_item_gen
val pp_enum_item : Ppx_deriving_runtime.Format.formatter -> enum_item -> Ppx_deriving_runtime.unit
val show_enum_item : enum_item -> Ppx_deriving_runtime.string
type variable_kind =
| VKconstant
| VKvariable
val pp_variable_kind : Ppx_deriving_runtime.Format.formatter -> variable_kind -> Ppx_deriving_runtime.unit
val show_variable_kind : variable_kind -> Ppx_deriving_runtime.string
type 'id var_gen = {
name : 'id;
type_ : type_;
original_type : type_;
kind : variable_kind;
default : 'id mterm_gen option;
invariants : 'id label_term_gen list;
loc : Location.t;
}
val pp_var_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id var_gen -> Ppx_deriving_runtime.unit
val show_var_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id var_gen -> Ppx_deriving_runtime.string
type var = lident var_gen
type 'id enum_gen = {
name : 'id;
values : 'id enum_item_gen list;
initial : 'id;
}
val pp_enum_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id enum_gen -> Ppx_deriving_runtime.unit
val show_enum_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id enum_gen -> Ppx_deriving_runtime.string
type enum = lident enum_gen
val pp_enum : Ppx_deriving_runtime.Format.formatter -> enum -> Ppx_deriving_runtime.unit
val show_enum : enum -> Ppx_deriving_runtime.string
type 'id asset_item_gen = {
name : 'id;
type_ : type_;
original_type : type_;
default : 'id mterm_gen option;
shadow : bool;
loc : Location.t;
}
val pp_asset_item_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id asset_item_gen -> Ppx_deriving_runtime.unit
val show_asset_item_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id asset_item_gen -> Ppx_deriving_runtime.string
type asset_item = lident asset_item_gen
val pp_asset_item : Ppx_deriving_runtime.Format.formatter -> asset_item -> Ppx_deriving_runtime.unit
val show_asset_item : asset_item -> Ppx_deriving_runtime.string
type 'id asset_gen = {
name : 'id;
values : 'id asset_item_gen list;
keys : Ident.ident list;
sort : 'id list;
big_map : bool;
state : lident option;
invariants : lident label_term_gen list;
init : 'id mterm_gen list;
loc : Location.t;
}
val pp_asset_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id asset_gen -> Ppx_deriving_runtime.unit
val show_asset_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id asset_gen -> Ppx_deriving_runtime.string
type asset = lident asset_gen
val pp_asset : Ppx_deriving_runtime.Format.formatter -> asset -> Ppx_deriving_runtime.unit
val show_asset : asset -> Ppx_deriving_runtime.string
type position =
| Ptuple of Ident.ident list
| Pnode of position list
val pp_position : Ppx_deriving_runtime.Format.formatter -> position -> Ppx_deriving_runtime.unit
val show_position : position -> Ppx_deriving_runtime.string
type 'id record_field_gen = {
name : 'id;
type_ : type_;
loc : Location.t;
}
val pp_record_field_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id record_field_gen -> Ppx_deriving_runtime.unit
val show_record_field_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id record_field_gen -> Ppx_deriving_runtime.string
type record_field = lident record_field_gen
val pp_record_field : Ppx_deriving_runtime.Format.formatter -> record_field -> Ppx_deriving_runtime.unit
val show_record_field : record_field -> Ppx_deriving_runtime.string
type 'id record_gen = {
name : 'id;
fields : 'id record_field_gen list;
pos : position;
loc : Location.t;
}
val pp_record_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id record_gen -> Ppx_deriving_runtime.unit
val show_record_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id record_gen -> Ppx_deriving_runtime.string
type record = lident record_gen
val pp_record : Ppx_deriving_runtime.Format.formatter -> record -> Ppx_deriving_runtime.unit
val show_record : record -> Ppx_deriving_runtime.string
type 'id function_ = {
name : 'id;
}
val pp_function_ : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id function_ -> Ppx_deriving_runtime.unit
val show_function_ : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id function_ -> Ppx_deriving_runtime.string
type 'id entry = {
name : 'id;
}
val pp_entry : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id entry -> Ppx_deriving_runtime.unit
val show_entry : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id entry -> Ppx_deriving_runtime.string
type 'id argument_gen = 'id * type_ * 'id mterm_gen option
val pp_argument_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id argument_gen -> Ppx_deriving_runtime.unit
val show_argument_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id argument_gen -> Ppx_deriving_runtime.string
type argument = lident argument_gen
val pp_argument : Ppx_deriving_runtime.Format.formatter -> argument -> Ppx_deriving_runtime.unit
val show_argument : argument -> Ppx_deriving_runtime.string
type 'id function_struct_gen = {
name : 'id;
args : 'id argument_gen list;
eargs : 'id argument_gen list;
body : 'id mterm_gen;
loc : Location.t;
}
val pp_function_struct_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id function_struct_gen -> Ppx_deriving_runtime.unit
val show_function_struct_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id function_struct_gen -> Ppx_deriving_runtime.string
type function_struct = lident function_struct_gen
val pp_function_struct : Ppx_deriving_runtime.Format.formatter -> function_struct -> Ppx_deriving_runtime.unit
val show_function_struct : function_struct -> Ppx_deriving_runtime.string
type 'id function_node_gen =
| Function of 'id function_struct_gen * type_
| Getter of 'id function_struct_gen * type_
| Entry of 'id function_struct_gen
val pp_function_node_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id function_node_gen -> Ppx_deriving_runtime.unit
val show_function_node_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id function_node_gen -> Ppx_deriving_runtime.string
type function_node = lident function_node_gen
val pp_function_node : Ppx_deriving_runtime.Format.formatter -> function_node -> Ppx_deriving_runtime.unit
val show_function_node : function_node -> Ppx_deriving_runtime.string
type 'id signature_gen = {
name : 'id;
args : 'id argument_gen list;
ret : type_ option;
}
val pp_signature_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id signature_gen -> Ppx_deriving_runtime.unit
val show_signature_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id signature_gen -> Ppx_deriving_runtime.string
type signature = lident signature_gen
val pp_signature : Ppx_deriving_runtime.Format.formatter -> signature -> Ppx_deriving_runtime.unit
val show_signature : signature -> Ppx_deriving_runtime.string
type 'id variable_gen = {
decl : 'id argument_gen;
kind : variable_kind;
loc : Location.t;
}
val pp_variable_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id variable_gen -> Ppx_deriving_runtime.unit
val show_variable_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id variable_gen -> Ppx_deriving_runtime.string
type variable = lident variable_gen
val pp_variable : Ppx_deriving_runtime.Format.formatter -> variable -> Ppx_deriving_runtime.unit
val show_variable : variable -> Ppx_deriving_runtime.string
type 'id predicate_gen = {
name : 'id;
args : ('id * type_) list;
body : 'id mterm_gen;
loc : Location.t;
}
val pp_predicate_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id predicate_gen -> Ppx_deriving_runtime.unit
val show_predicate_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id predicate_gen -> Ppx_deriving_runtime.string
type predicate = lident predicate_gen
val pp_predicate : Ppx_deriving_runtime.Format.formatter -> predicate -> Ppx_deriving_runtime.unit
val show_predicate : predicate -> Ppx_deriving_runtime.string
type 'id definition_gen = {
name : 'id;
typ : type_;
var : 'id;
body : 'id mterm_gen;
loc : Location.t;
}
val pp_definition_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id definition_gen -> Ppx_deriving_runtime.unit
val show_definition_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id definition_gen -> Ppx_deriving_runtime.string
type definition = lident definition_gen
val pp_definition : Ppx_deriving_runtime.Format.formatter -> definition -> Ppx_deriving_runtime.unit
val show_definition : definition -> Ppx_deriving_runtime.string
type 'id invariant_gen = {
label : 'id;
formulas : 'id mterm_gen list;
}
val pp_invariant_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id invariant_gen -> Ppx_deriving_runtime.unit
val show_invariant_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id invariant_gen -> Ppx_deriving_runtime.string
type invariant = lident invariant_gen
val pp_invariant : Ppx_deriving_runtime.Format.formatter -> invariant -> Ppx_deriving_runtime.unit
val show_invariant : invariant -> Ppx_deriving_runtime.string
type 'id fail_gen = {
label : 'id;
arg : 'id;
atype : type_;
formula : 'id mterm_gen;
loc : Location.t;
}
val pp_fail_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id fail_gen -> Ppx_deriving_runtime.unit
val show_fail_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id fail_gen -> Ppx_deriving_runtime.string
type fail = lident fail_gen
val pp_fail : Ppx_deriving_runtime.Format.formatter -> fail -> Ppx_deriving_runtime.unit
val show_fail : fail -> Ppx_deriving_runtime.string
type spec_mode =
| Post
| Assert
val pp_spec_mode : Ppx_deriving_runtime.Format.formatter -> spec_mode -> Ppx_deriving_runtime.unit
val show_spec_mode : spec_mode -> Ppx_deriving_runtime.string
type 'id postcondition_gen = {
name : 'id;
mode : spec_mode;
formula : 'id mterm_gen;
invariants : 'id invariant_gen list;
uses : 'id list;
}
val pp_postcondition_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id postcondition_gen -> Ppx_deriving_runtime.unit
val show_postcondition_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id postcondition_gen -> Ppx_deriving_runtime.string
type postcondition = lident postcondition_gen
val pp_postcondition : Ppx_deriving_runtime.Format.formatter -> postcondition -> Ppx_deriving_runtime.unit
val show_postcondition : postcondition -> Ppx_deriving_runtime.string
type 'id assert_gen = {
name : 'id;
label : 'id;
formula : 'id mterm_gen;
invariants : 'id invariant_gen list;
uses : 'id list;
}
val pp_assert_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id assert_gen -> Ppx_deriving_runtime.unit
val show_assert_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id assert_gen -> Ppx_deriving_runtime.string
type assert_ = lident assert_gen
val pp_assert_ : Ppx_deriving_runtime.Format.formatter -> assert_ -> Ppx_deriving_runtime.unit
val show_assert_ : assert_ -> Ppx_deriving_runtime.string
type 'id specification_gen = {
predicates : 'id predicate_gen list;
definitions : 'id definition_gen list;
lemmas : 'id label_term_gen list;
theorems : 'id label_term_gen list;
fails : 'id fail_gen list;
variables : 'id variable_gen list;
invariants : ('id * 'id label_term_gen list) list;
effects : 'id mterm_gen list;
postconditions : 'id postcondition_gen list;
loc : Location.t;
}
val pp_specification_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id specification_gen -> Ppx_deriving_runtime.unit
val show_specification_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id specification_gen -> Ppx_deriving_runtime.string
type security_node =
| SonlyByRole of entry_description * security_role list
| SonlyInEntry of entry_description * security_entry
| SonlyByRoleInEntry of entry_description * security_role list * security_entry
| SnotByRole of entry_description * security_role list
| SnotInEntry of entry_description * security_entry
| SnotByRoleInEntry of entry_description * security_role list * security_entry
| StransferredBy of entry_description
| StransferredTo of entry_description
| SnoStorageFail of security_entry
val pp_security_node : Ppx_deriving_runtime.Format.formatter -> security_node -> Ppx_deriving_runtime.unit
val show_security_node : security_node -> Ppx_deriving_runtime.string
type security_predicate = {
s_node : security_node;
loc : Location.t;
}
val pp_security_predicate : Ppx_deriving_runtime.Format.formatter -> security_predicate -> Ppx_deriving_runtime.unit
val show_security_predicate : security_predicate -> Ppx_deriving_runtime.string
type security_item = {
label : lident;
predicate : security_predicate;
loc : Location.t;
}
val pp_security_item : Ppx_deriving_runtime.Format.formatter -> security_item -> Ppx_deriving_runtime.unit
val show_security_item : security_item -> Ppx_deriving_runtime.string
type security = {
items : security_item list;
loc : Location.t;
}
val pp_security : Ppx_deriving_runtime.Format.formatter -> security -> Ppx_deriving_runtime.unit
val show_security : security -> Ppx_deriving_runtime.string
type specification = lident specification_gen
val pp_specification : Ppx_deriving_runtime.Format.formatter -> specification -> Ppx_deriving_runtime.unit
val show_specification : specification -> Ppx_deriving_runtime.string
type 'id function__gen = {
node : 'id function_node_gen;
spec : 'id specification_gen option;
}
val pp_function__gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id function__gen -> Ppx_deriving_runtime.unit
val show_function__gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id function__gen -> Ppx_deriving_runtime.string
type function__ = lident function__gen
val pp_function__ : Ppx_deriving_runtime.Format.formatter -> function__ -> Ppx_deriving_runtime.unit
val show_function__ : function__ -> Ppx_deriving_runtime.string
type 'id decl_node_gen =
| Dvar of 'id var_gen
| Denum of 'id enum_gen
| Dasset of 'id asset_gen
| Drecord of 'id record_gen
val pp_decl_node_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id decl_node_gen -> Ppx_deriving_runtime.unit
val show_decl_node_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id decl_node_gen -> Ppx_deriving_runtime.string
type decl_node = lident decl_node_gen
val pp_decl_node : Ppx_deriving_runtime.Format.formatter -> decl_node -> Ppx_deriving_runtime.unit
val show_decl_node : decl_node -> Ppx_deriving_runtime.string
type 'id parameter_gen = {
name : 'id;
typ : type_;
default : 'id mterm_gen option;
value : 'id mterm_gen option;
loc : Location.t;
}
val pp_parameter_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id parameter_gen -> Ppx_deriving_runtime.unit
val show_parameter_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id parameter_gen -> Ppx_deriving_runtime.string
type parameter = lident parameter_gen
val pp_parameter : Ppx_deriving_runtime.Format.formatter -> parameter -> Ppx_deriving_runtime.unit
val show_parameter : parameter -> Ppx_deriving_runtime.string
type 'id model_gen = {
name : lident;
parameters : 'id parameter_gen list;
api_items : api_storage list;
api_verif : api_verif list;
decls : 'id decl_node_gen list;
storage : 'id storage_gen;
functions : 'id function__gen list;
specification : 'id specification_gen;
security : security;
loc : Location.t;
}
val pp_model_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id model_gen -> Ppx_deriving_runtime.unit
val show_model_gen : id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id model_gen -> Ppx_deriving_runtime.string
type property =
| Ppostcondition of postcondition * Ident.ident option
| PstorageInvariant of label_term * Ident.ident
| PsecurityPredicate of security_item
val pp_property : Ppx_deriving_runtime.Format.formatter -> property -> Ppx_deriving_runtime.unit
val show_property : property -> Ppx_deriving_runtime.string
type model = lident model_gen
val pp_model : Ppx_deriving_runtime.Format.formatter -> model -> Ppx_deriving_runtime.unit
val show_model : model -> Ppx_deriving_runtime.string
val mk_pattern : ?⁠loc:Location.t -> 'id pattern_node -> 'id pattern_gen
val mk_mterm : ?⁠loc:Location.t -> ('id'id mterm_gen) mterm_node -> type_ -> 'id mterm_gen
val mk_label_term : ?⁠loc:Location.t -> 'id mterm_gen -> 'id -> 'id label_term_gen
val mk_variable : ?⁠loc:Location.t -> 'a argument_gen -> variable_kind -> 'a variable_gen
val mk_predicate : ?⁠args:('a * type_) list -> ?⁠loc:Location.t -> 'a -> 'a mterm_gen -> 'a predicate_gen
val mk_definition : ?⁠loc:Location.t -> 'a -> type_ -> 'a -> 'a mterm_gen -> 'a definition_gen
val mk_invariant : ?⁠formulas:'a mterm_gen list -> 'a -> 'a invariant_gen
val mk_fail : ?⁠loc:Location.t -> 'a -> 'a -> type_ -> 'a mterm_gen -> 'a fail_gen
val mk_postcondition : ?⁠invariants:'a invariant_gen list -> ?⁠uses:'a list -> 'a -> spec_mode -> 'a mterm_gen -> 'a postcondition_gen
val mk_assert : ?⁠invariants:'a invariant_gen list -> ?⁠uses:'a list -> 'a -> 'a -> 'a mterm_gen -> 'a assert_gen
val mk_specification : ?⁠predicates:'a predicate_gen list -> ?⁠definitions:'a definition_gen list -> ?⁠lemmas:'a label_term_gen list -> ?⁠theorems:'a label_term_gen list -> ?⁠fails:'a fail_gen list -> ?⁠variables:'a variable_gen list -> ?⁠invariants:('a * 'a label_term_gen list) list -> ?⁠effects:'a mterm_gen list -> ?⁠postconditions:'a postcondition_gen list -> ?⁠loc:Location.t -> unit -> 'a specification_gen
val mk_security_predicate : ?⁠loc:Location.t -> security_node -> security_predicate
val mk_security_item : ?⁠loc:Location.t -> lident -> security_predicate -> security_item
val mk_security : ?⁠items:security_item list -> ?⁠loc:Location.t -> unit -> security
val mk_var : ?⁠invariants:'id label_term_gen list -> ?⁠default:'id mterm_gen -> ?⁠loc:Location.t -> 'id -> type_ -> type_ -> variable_kind -> 'id var_gen
val mk_enum : ?⁠values:'id enum_item_gen list -> 'id -> 'id -> 'id enum_gen
val mk_enum_item : ?⁠args:type_ list -> ?⁠invariants:'id label_term_gen list -> 'id -> 'id enum_item_gen
val mk_asset : ?⁠values:'id asset_item_gen list -> ?⁠sort:'id list -> ?⁠big_map:bool -> ?⁠state:lident -> ?⁠keys:Ident.ident list -> ?⁠invariants:lident label_term_gen list -> ?⁠init:'id mterm_gen list -> ?⁠loc:Location.t -> 'id -> 'id asset_gen
val mk_asset_item : ?⁠default:'id mterm_gen -> ?⁠shadow:bool -> ?⁠loc:Location.t -> 'id -> type_ -> type_ -> 'id asset_item_gen
val mk_record : ?⁠fields:'id record_field_gen list -> ?⁠pos:position -> ?⁠loc:Location.t -> 'id -> 'id record_gen
val mk_record_field : ?⁠loc:Location.t -> 'id -> type_ -> 'id record_field_gen
val mk_storage_item : ?⁠const:bool -> ?⁠ghost:bool -> ?⁠loc:Location.t -> 'id -> model_type -> type_ -> 'id mterm_gen -> 'id storage_item_gen
val mk_function_struct : ?⁠args:lident argument_gen list -> ?⁠eargs:lident argument_gen list -> ?⁠loc:Location.t -> lident -> lident mterm_gen -> function_struct
val mk_function : ?⁠spec:'id specification_gen -> 'id function_node_gen -> 'id function__gen
val mk_signature : ?⁠args:'id argument_gen list -> ?⁠ret:type_ -> 'id -> 'id signature_gen
val mk_api_item : api_storage_node -> api_loc -> api_storage
val mk_model : ?⁠parameters:lident parameter_gen list -> ?⁠api_items:api_storage list -> ?⁠api_verif:api_verif list -> ?⁠decls:lident decl_node_gen list -> ?⁠functions:lident function__gen list -> ?⁠storage:lident storage_gen -> ?⁠specification:lident specification_gen -> ?⁠security:security -> ?⁠loc:Location.t -> lident -> model
val mktype : ?⁠annot:lident -> ntype -> type_
val get_ntype : (ntype * 'a) -> ntype
val get_atype : ('a * lident option) -> lident option
val tunit : type_
val tbool : type_
val tnat : type_
val tint : type_
val tstring : type_
val tbytes : type_
val ttez : type_
val tduration : type_
val tkey : type_
val tkeyhash : type_
val tdate : type_
val ttimestamp : type_
val taddress : type_
val trole : type_
val tenum : lident -> type_
val tstate : type_
val tstorage : type_
val trecord : lident -> type_
val toption : type_ -> type_
val tset : type_ -> type_
val tlist : type_ -> type_
val tbmap : bool -> type_ -> type_ -> type_
val tmap : type_ -> type_ -> type_
val tbig_map : type_ -> type_ -> type_
val tor : type_ -> type_ -> type_
val tlambda : type_ -> type_ -> type_
val ttuple : type_ list -> type_
val trat : type_
val toperation : type_
val tsignature : type_
val tcontract : type_ -> type_
val tticket : type_ -> type_
val tsapling_state : int -> type_
val tsapling_transaction : int -> type_
val tchainid : type_
val tbls12_381_fr : type_
val tbls12_381_g1 : type_
val tbls12_381_g2 : type_
val tnever : type_
val tasset : lident -> type_
val tcollection : lident -> type_
val taggregate : lident -> type_
val tpartition : lident -> type_
val tview : lident -> type_
val toperations : type_
val tmetadata : type_
val mk_bool : bool -> 'a mterm_gen
val mk_string : string -> 'a mterm_gen
val mk_bytes : string -> 'a mterm_gen
val mk_bnat : Core.big_int -> 'a mterm_gen
val mk_nat : int -> 'a mterm_gen
val mk_bint : Core.big_int -> 'a mterm_gen
val mk_int : int -> 'a mterm_gen
val mk_address : string -> 'a mterm_gen
val unit : 'a mterm_gen
val mk_date : Core.date -> 'a mterm_gen
val mk_duration : Core.duration -> 'a mterm_gen
val mtrue : 'a mterm_gen
val mfalse : 'a mterm_gen
val mnow : 'a mterm_gen
val mtransferred : 'a mterm_gen
val mcaller : 'a mterm_gen
val mbalance : 'a mterm_gen
val msource : 'a mterm_gen
val mselfaddress : 'a mterm_gen
val mchainid : 'a mterm_gen
val mmetadata : 'a mterm_gen
val mlevel : 'a mterm_gen
val mk_mvar : 'a -> type_ -> 'a mterm_gen
val mk_pvar : 'a -> type_ -> 'a mterm_gen
val mk_svar : 'a -> type_ -> 'a mterm_gen
val mk_parameter : 'a -> type_ -> 'a mterm_gen
val mk_enum_value : ?⁠args:'a mterm_gen list -> 'a -> Ident.ident Location.loced -> 'a mterm_gen
val mk_btez : Core.big_int -> 'a mterm_gen
val mk_tez : int -> 'a mterm_gen
val mk_tuple : mterm list -> lident mterm_gen
val mk_letin : 'a -> 'a mterm_gen -> 'a mterm_gen -> 'a mterm_gen
val mk_tupleaccess : int -> mterm -> lident mterm_gen
val mk_optget : mterm -> lident mterm_gen
val mk_abs : mterm -> lident mterm_gen
val mk_nat_to_int : mterm -> lident mterm_gen
val mk_some : 'a mterm_gen -> 'a mterm_gen
val mk_left : type_ -> 'a mterm_gen -> 'a mterm_gen
val mk_right : type_ -> 'a mterm_gen -> 'a mterm_gen
val mk_none : type_ -> 'a mterm_gen
val mk_brat : Core.big_int -> Core.big_int -> lident mterm_gen
val mk_rat : int -> int -> lident mterm_gen
val mk_metadata : ('a mterm_gen * 'a mterm_gen) list -> 'a mterm_gen
val fail : string -> 'a mterm_gen
val failg : 'a mterm_gen -> 'a mterm_gen
val mnot : 'a mterm_gen -> 'a mterm_gen
val seq : 'a mterm_gen list -> 'a mterm_gen
val skip : 'a mterm_gen
val operations : 'a mterm_gen
val cmp_ident : Ident.ident -> Ident.ident -> bool
val cmp_big_int : Core.big_int -> Core.big_int -> bool
val cmp_int : int -> int -> bool
val cmp_lident : lident -> lident -> bool
val cmp_bool : bool -> bool -> bool
val cmp_assign_op : assignment_operator -> assignment_operator -> bool
val cmp_currency : currency -> currency -> bool
val cmp_container : container -> container -> bool
val cmp_btyp : btyp -> btyp -> bool
val cmp_vset : vset -> vset -> bool
val cmp_trtyp : trtyp -> trtyp -> bool
val cmp_comparison_operator : comparison_operator -> comparison_operator -> bool
val cmp_rat_arith_op : rat_arith_op -> rat_arith_op -> bool
val cmp_entry_description : entry_description -> entry_description -> bool
val cmp_security_role : lident -> lident -> bool
val cmp_security_entry : security_entry -> security_entry -> bool
val cmp_fail_type : ('id mterm_gen -> 'id mterm_gen -> bool) -> 'id fail_type_gen -> 'id fail_type_gen -> bool
val cmp_ntype : ntype -> ntype -> bool
val cmp_type : ?⁠with_annot:bool -> type_ -> type_ -> bool
val cmp_pattern_node : (lident -> lident -> bool) -> lident pattern_node -> lident pattern_node -> bool
val cmp_pattern : lident pattern_gen -> lident pattern_gen -> bool
val cmp_for_ident : ('id -> 'id -> bool) -> 'id for_ident_gen -> 'id for_ident_gen -> bool
val cmp_mterm_node : (mterm -> mterm -> bool) -> (lident -> lident -> bool) -> (lidentmterm) mterm_node -> (lidentmterm) mterm_node -> bool
val cmp_mterm : mterm -> mterm -> bool
val cmp_container_kind : api_container_kind -> api_container_kind -> bool
val cmp_api_item_node : api_storage_node -> api_storage_node -> bool
val cmp_api_loc : api_loc -> api_loc -> bool
val cmp_api_storage : api_storage -> api_storage -> bool
val cmp_api_verif : api_verif -> api_verif -> bool
val map_ptyp : (type_ -> type_) -> ntype -> ntype
val map_type : (type_ -> type_) -> type_ -> type_
val map_for_ident : ('id -> 'id) -> 'id for_ident_gen -> 'id for_ident_gen
val map_assign_kind : (Ident.ident -> Ident.ident) -> ('id -> 'id) -> ('a -> 'b) -> ('id'a) assign_kind_gen -> ('id'b) assign_kind_gen
val map_var_kind : ('a -> 'b) -> 'a var_kind_gen -> 'b var_kind_gen
val map_temp : (Ident.ident -> Ident.ident) -> temp -> temp
val map_delta : delta -> delta
val map_container_kind : (Ident.ident -> Ident.ident) -> ('a -> 'b) -> 'a container_kind_gen -> 'b container_kind_gen
val map_iter_container_kind : (Ident.ident -> Ident.ident) -> ('a -> 'b) -> 'a iter_container_kind_gen -> 'b iter_container_kind_gen
val map_transfer_kind : (Ident.ident -> Ident.ident) -> (type_ -> type_) -> ('a -> 'b) -> 'a transfer_kind_gen -> 'b transfer_kind_gen
val map_term_node_internal : (Ident.ident -> Ident.ident) -> ('id -> 'id) -> (type_ -> type_) -> ('id mterm_gen -> 'id mterm_gen) -> ('id'id mterm_gen) mterm_node -> ('id'id mterm_gen) mterm_node
val map_gen_mterm : ('a -> ('id'id mterm_gen) mterm_node -> ('id'id mterm_gen) mterm_node) -> 'a -> (type_ -> type_) -> 'id mterm_gen -> 'id mterm_gen
val map_mterm : (lident mterm_gen -> lident mterm_gen) -> ?⁠ft:(type_ -> type_) -> mterm -> lident mterm_gen
type ('id, 't) ctx_model_gen = {
formula : bool;
fs : 'id function_struct_gen option;
label : 'id option;
spec_id : 'id option;
invariant_id : 'id option;
custom : 't;
}
type ctx_model = (lident, unit) ctx_model_gen
val mk_ctx_model : ?⁠formula:bool -> ?⁠fs:'id function_struct_gen -> ?⁠label:'id -> ?⁠spec_id:'id -> ?⁠invariant_id:'id -> 't -> ('id't) ctx_model_gen
val map_mterm_model_exec : 't -> ((lident't) ctx_model_gen -> mterm -> mterm) -> model -> model
val map_specification : (lident't) ctx_model_gen -> ((lident't) ctx_model_gen -> mterm -> mterm) -> specification -> specification
val map_mterm_model_formula : 't -> ((lident't) ctx_model_gen -> mterm -> mterm) -> model -> model
val map_mterm_model_gen : 't -> ((lident't) ctx_model_gen -> mterm -> mterm) -> model -> model
val map_mterm_model : ((lident, unit) ctx_model_gen -> mterm -> mterm) -> model -> model
val fold_assign_kind : ('a -> 'b -> 'a) -> 'a -> ('c'b) assign_kind_gen -> 'a
val fold_var_kind : ('a -> 'b -> 'a) -> 'a -> 'b var_kind_gen -> 'a
val fold_container_kind : ('a -> 'b -> 'a) -> 'a -> 'b container_kind_gen -> 'a
val fold_iter_container_kind : ('a -> 'b -> 'a) -> 'a -> 'b iter_container_kind_gen -> 'a
val fold_transfer_kind : ('a -> 'b -> 'a) -> 'a -> 'b transfer_kind_gen -> 'a
val fold_term : ('a -> 'id mterm_gen -> 'a) -> 'a -> 'id mterm_gen -> 'a
val fold_map_term_list : ('a -> 'b -> 'term * 'a) -> 'a -> 'b list -> 'term list * 'a
val fold_map_assign_kind : ('a -> 'b -> 'c * 'a) -> 'a -> ('d'b) assign_kind_gen -> ('d'c) assign_kind_gen * 'a
val fold_map_var_kind : ('a -> 'b -> 'c * 'a) -> 'a -> 'b var_kind_gen -> 'c var_kind_gen * 'a
val fold_map_container_kind : ('a -> 'b -> 'c * 'a) -> 'a -> 'b container_kind_gen -> 'c container_kind_gen * 'a
val fold_map_iter_container_kind : ('a -> 'b -> 'c * 'a) -> 'a -> 'b iter_container_kind_gen -> 'c iter_container_kind_gen * 'a
val fold_map_transfer_kind : ('a -> 'b -> 'c * 'a) -> 'a -> 'b transfer_kind_gen -> 'c transfer_kind_gen * 'a
val fold_map_term : (('id'id mterm_gen) mterm_node -> 'id mterm_gen) -> ('a -> 'id mterm_gen -> 'id mterm_gen * 'a) -> 'a -> 'id mterm_gen -> 'id mterm_gen * 'a
val fold_left : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val fold_label_term : ('id't) ctx_model_gen -> (('id't) ctx_model_gen -> 'a -> 'id mterm_gen -> 'a) -> 'id label_term_gen -> 'a -> 'a
val fold_specification : ('id't) ctx_model_gen -> (('id't) ctx_model_gen -> 'a -> 'id mterm_gen -> 'a) -> 'id specification_gen -> 'a -> 'a
val fold_model : ((lident, unit) ctx_model_gen -> 'a -> lident mterm_gen -> 'a) -> lident model_gen -> 'a -> 'a
type kind_ident =
| KIarchetype
| KIparameter
| KIdeclvarname
| KIassetname
| KIassetfield
| KIassetstate
| KIassetinit
| KIrecordname
| KIrecordfield
| KIparamlambda
| KIenumname
| KIenumvalue
| KIcontractname
| KIcontractentry
| KIstoragefield
| KIentry
| KIfunction
| KIgetter
| KIargument
| KIlocalvar
| KIlabel
| KIpredicate
| KIdefinition
| KIdefinitionvar
| KIinvariant
| KIpostcondition
| KIpostconditionuse
| KIfaillabel
| KIfailarg
| KIsecurityad
| KIsecurityrole
| KIsecurityentry
| KImterm
val map_model : (kind_ident -> Ident.ident -> Ident.ident) -> (type_ -> type_) -> (mterm -> mterm) -> model -> model
val replace_ident_model : (kind_ident -> Ident.ident -> Ident.ident) -> model -> model
val merge_seq : mterm -> mterm -> mterm
val extract_list : mterm -> mterm -> mterm list
type effect =
| Eadded of Ident.ident
| Eremoved of Ident.ident
| Eupdated of Ident.ident
val pp_effect : Ppx_deriving_runtime.Format.formatter -> effect -> Ppx_deriving_runtime.unit
val show_effect : effect -> Ppx_deriving_runtime.string
module Utils : sig ... end