package archetype

  1. Overview
  2. Docs
val pp_lident : Ppx_deriving_runtime.Format.formatter -> lident -> Ppx_deriving_runtime.unit
val show_lident : lident -> Ppx_deriving_runtime.string
type currency =
  1. | Tz
  2. | Mtz
  3. | Utz
val pp_currency : Ppx_deriving_runtime.Format.formatter -> currency -> Ppx_deriving_runtime.unit
val show_currency : currency -> Ppx_deriving_runtime.string
type container =
  1. | Collection
  2. | Aggregate
  3. | Partition
  4. | View
val pp_container : Ppx_deriving_runtime.Format.formatter -> container -> Ppx_deriving_runtime.unit
val show_container : container -> Ppx_deriving_runtime.string
type btyp =
  1. | Bunit
  2. | Bbool
  3. | Bint
  4. | Brational
  5. | Bdate
  6. | Bduration
  7. | Btimestamp
  8. | Bstring
  9. | Baddress
  10. | Brole
  11. | Bcurrency
  12. | Bsignature
  13. | Bkey
  14. | Bkeyhash
  15. | Bbytes
  16. | Bnat
  17. | Bchainid
val pp_btyp : Ppx_deriving_runtime.Format.formatter -> btyp -> Ppx_deriving_runtime.unit
type vset =
  1. | VSremoved
  2. | VSadded
  3. | VSstable
  4. | VSbefore
  5. | VSafter
  6. | VSfixed
val pp_vset : Ppx_deriving_runtime.Format.formatter -> vset -> Ppx_deriving_runtime.unit
type trtyp =
  1. | TRentry
  2. | TRaction
  3. | TRasset
  4. | TRfield
val pp_trtyp : Ppx_deriving_runtime.Format.formatter -> trtyp -> Ppx_deriving_runtime.unit
type type_ =
  1. | Tasset of lident
  2. | Tenum of lident
  3. | Tstate
  4. | Tbuiltin of btyp
  5. | Tcontainer of type_ * container
  6. | Tlist of type_
  7. | Toption of type_
  8. | Ttuple of type_ list
  9. | Tset of type_
  10. | Tmap of bool * type_ * type_
  11. | Trecord of lident
  12. | Tlambda of type_ * type_
  13. | Tunit
  14. | Tstorage
  15. | Toperation
  16. | Tcontract of type_
  17. | Tprog of type_
  18. | Tvset of vset * type_
  19. | Ttrace of trtyp
val pp_type_ : Ppx_deriving_runtime.Format.formatter -> type_ -> Ppx_deriving_runtime.unit
type 'id pattern_node =
  1. | Pwild
  2. | Pconst of 'id
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 = {
  1. node : 'id pattern_node;
  2. 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 =
  1. | FIsimple of 'id
  2. | 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 =
  1. | Gt
  2. | Ge
  3. | Lt
  4. | 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 =
  1. | Rplus
  2. | Rminus
  3. | Rmult
  4. | 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 =
  1. | ValueAssign
  2. | PlusAssign
  3. | MinusAssign
  4. | MultAssign
  5. | DivAssign
  6. | AndAssign
  7. | 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 =
  1. | SKasc
  2. | 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 =
  1. | Avar of 'id
  2. | Avarstore of 'id
  3. | Aasset of 'id * 'id * 'term
  4. | Arecord of 'id * 'id * 'term
  5. | Astate
  6. | Aassetstate of Ident.ident * 'term
  7. | 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 =
  1. | Vassetstate of 'term
  2. | Vstorevar
  3. | Vstorecol
  4. | Venumval
  5. | Vdefinition
  6. | Vlocal
  7. | Vparam
  8. | Vfield
  9. | Vstate
  10. | Vthe
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 =
  1. | Tbefore
  2. | Tat of Ident.ident
  3. | Tnone
val pp_temp : Ppx_deriving_runtime.Format.formatter -> temp -> Ppx_deriving_runtime.unit
type delta =
  1. | Dadded
  2. | Dremoved
  3. | Dunmoved
  4. | Dnone
val pp_delta : Ppx_deriving_runtime.Format.formatter -> delta -> Ppx_deriving_runtime.unit
type 'term container_kind_gen =
  1. | CKcoll of temp * delta
  2. | CKview of 'term
  3. | CKfield of Ident.ident * Ident.ident * 'term * temp * delta
  4. | 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 =
  1. | ICKcoll of Ident.ident
  2. | ICKview of 'term
  3. | ICKfield of Ident.ident * Ident.ident * 'term
  4. | ICKset of 'term
  5. | ICKlist of 'term
  6. | 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 =
  1. | TKsimple of 'term
  2. | TKcall of Ident.ident * type_ * 'term * 'term
  3. | TKentry of 'term * 'term
  4. | TKself of Ident.ident * (Ident.ident * 'term) list
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 =
  1. | Mletin of 'id list * 'term * type_ option * 'term * 'term option
  2. | Mdeclvar of 'id list * type_ option * 'term
  3. | Mapp of 'id * 'term list
  4. | Massign of assignment_operator * type_ * ('id, 'term) assign_kind_gen * 'term
  5. | Mif of 'term * 'term * 'term option
  6. | Mmatchwith of 'term * ('id pattern_gen * 'term) list
  7. | Mfor of 'id for_ident_gen * 'term iter_container_kind_gen * 'term * Ident.ident option
  8. | Miter of 'id * 'term * 'term * 'term * Ident.ident option
  9. | Mwhile of 'term * 'term * Ident.ident option
  10. | Mseq of 'term list
  11. | Mreturn of 'term
  12. | Mlabel of 'id
  13. | Mmark of 'id * 'term
  14. | Mfail of 'id fail_type_gen
  15. | Mtransfer of 'term * 'term transfer_kind_gen
  16. | Mentrypoint of type_ * 'id * 'term
  17. | Mself of 'id
  18. | Moperations
  19. | Mmkoperation of 'term * 'term * 'term
  20. | Mint of Core.big_int
  21. | Mnat of Core.big_int
  22. | Mbool of bool
  23. | Menum of string
  24. | Mrational of Core.big_int * Core.big_int
  25. | Mstring of string
  26. | Mcurrency of Core.big_int * currency
  27. | Maddress of string
  28. | Mdate of Core.date
  29. | Mduration of Core.duration
  30. | Mtimestamp of Core.big_int
  31. | Mbytes of string
  32. | Munit
  33. | Mexprif of 'term * 'term * 'term
  34. | Mexprmatchwith of 'term * ('id pattern_gen * 'term) list
  35. | Mmatchsome of 'term * 'term * Ident.ident * 'term
  36. | Mnone
  37. | Msome of 'term
  38. | Mtuple of 'term list
  39. | Masset of 'term list
  40. | Massets of 'term list
  41. | Mlitset of 'term list
  42. | Mlitlist of 'term list
  43. | Mlitmap of ('term * 'term) list
  44. | Mlitrecord of (Ident.ident * 'term) list
  45. | Mdot of 'term * 'id
  46. | Mdotassetfield of 'id * 'term * 'id
  47. | Mequal of type_ * 'term * 'term
  48. | Mnequal of type_ * 'term * 'term
  49. | Mgt of 'term * 'term
  50. | Mge of 'term * 'term
  51. | Mlt of 'term * 'term
  52. | Mle of 'term * 'term
  53. | Mmulticomp of 'term * (comparison_operator * 'term) list
  54. | Mand of 'term * 'term
  55. | Mor of 'term * 'term
  56. | Mxor of 'term * 'term
  57. | Mnot of 'term
  58. | Mplus of 'term * 'term
  59. | Mminus of 'term * 'term
  60. | Mmult of 'term * 'term
  61. | Mdivrat of 'term * 'term
  62. | Mdiveuc of 'term * 'term
  63. | Mmodulo of 'term * 'term
  64. | Muminus of 'term
  65. | Maddasset of Ident.ident * 'term
  66. | Maddfield of Ident.ident * Ident.ident * 'term * 'term
  67. | Mremoveasset of Ident.ident * 'term
  68. | Mremovefield of Ident.ident * Ident.ident * 'term * 'term
  69. | Mremoveall of Ident.ident * Ident.ident * 'term
  70. | Mremoveif of Ident.ident * 'term container_kind_gen * (Ident.ident * type_) list * 'term * 'term list
  71. | Mclear of Ident.ident * 'term container_kind_gen
  72. | Mset of Ident.ident * Ident.ident list * 'term * 'term
  73. | Mupdate of Ident.ident * 'term * ('id * assignment_operator * 'term) list
  74. | Maddupdate of Ident.ident * 'term container_kind_gen * 'term * ('id * assignment_operator * 'term) list
  75. | Maddforce of Ident.ident * 'term
  76. | Mget of Ident.ident * 'term container_kind_gen * 'term
  77. | Mselect of Ident.ident * 'term container_kind_gen * (Ident.ident * type_) list * 'term * 'term list
  78. | Msort of Ident.ident * 'term container_kind_gen * (Ident.ident * sort_kind) list
  79. | Mcontains of Ident.ident * 'term container_kind_gen * 'term
  80. | Mnth of Ident.ident * 'term container_kind_gen * 'term
  81. | Mcount of Ident.ident * 'term container_kind_gen
  82. | Msum of Ident.ident * 'term container_kind_gen * 'term
  83. | Mhead of Ident.ident * 'term container_kind_gen * 'term
  84. | Mtail of Ident.ident * 'term container_kind_gen * 'term
  85. | Mcast of type_ * type_ * 'term
  86. | Mtupleaccess of 'term * Core.big_int
  87. | Mrecupdate of 'term * (Ident.ident * 'term) list
  88. | Msetadd of type_ * 'term * 'term
  89. | Msetremove of type_ * 'term * 'term
  90. | Msetcontains of type_ * 'term * 'term
  91. | Msetlength of type_ * 'term
  92. | Msetfold of type_ * 'id * 'id * 'term * 'term * 'term
  93. | Mlistprepend of type_ * 'term * 'term
  94. | Mlistheadtail of type_ * 'term
  95. | Mlistlength of type_ * 'term
  96. | Mlistcontains of type_ * 'term * 'term
  97. | Mlistnth of type_ * 'term * 'term
  98. | Mlistreverse of type_ * 'term
  99. | Mlistfold of type_ * 'id * 'id * 'term * 'term * 'term
  100. | Mmapput of type_ * type_ * 'term * 'term * 'term
  101. | Mmapremove of type_ * type_ * 'term * 'term
  102. | Mmapget of type_ * type_ * 'term * 'term
  103. | Mmapgetopt of type_ * type_ * 'term * 'term
  104. | Mmapcontains of type_ * type_ * 'term * 'term
  105. | Mmaplength of type_ * type_ * 'term
  106. | Mmapfold of type_ * 'id * 'id * 'id * 'term * 'term * 'term
  107. | Mmin of 'term * 'term
  108. | Mmax of 'term * 'term
  109. | Mabs of 'term
  110. | Mconcat of 'term * 'term
  111. | Mslice of 'term * 'term * 'term
  112. | Mlength of 'term
  113. | Misnone of 'term
  114. | Missome of 'term
  115. | Moptget of 'term
  116. | Mfloor of 'term
  117. | Mceil of 'term
  118. | Mtostring of type_ * 'term
  119. | Mpack of 'term
  120. | Munpack of type_ * 'term
  121. | Mblake2b of 'term
  122. | Msha256 of 'term
  123. | Msha512 of 'term
  124. | Mhashkey of 'term
  125. | Mchecksignature of 'term * 'term * 'term
  126. | Mnow
  127. | Mtransferred
  128. | Mcaller
  129. | Mbalance
  130. | Msource
  131. | Mselfaddress
  132. | Mchainid
  133. | Mmetadata
  134. | Mvar of 'id * 'term var_kind_gen * temp * delta
  135. | Mrateq of 'term * 'term
  136. | Mratcmp of comparison_operator * 'term * 'term
  137. | Mratarith of rat_arith_op * 'term * 'term
  138. | Mratuminus of 'term
  139. | Mrattez of 'term * 'term
  140. | Mnattoint of 'term
  141. | Mnattorat of 'term
  142. | Minttorat of 'term
  143. | Mratdur of 'term * 'term
  144. | Mforall of 'id * type_ * 'term option * 'term
  145. | Mexists of 'id * type_ * 'term option * 'term
  146. | Mimply of 'term * 'term
  147. | Mequiv of 'term * 'term
  148. | Msetiterated of 'term iter_container_kind_gen
  149. | Msettoiterate of 'term iter_container_kind_gen
  150. | Mempty of Ident.ident
  151. | Msingleton of Ident.ident * 'term
  152. | Msubsetof of Ident.ident * 'term container_kind_gen * 'term
  153. | Misempty of Ident.ident * 'term
  154. | Munion of Ident.ident * 'term * 'term
  155. | Minter of Ident.ident * 'term * 'term
  156. | Mdiff of Ident.ident * 'term * 'term
and assign_kind = (lident, mterm) 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 = {
  1. node : ('id, 'id mterm_gen) mterm_node;
  2. type_ : type_;
  3. loc : Location.t;
}
and mterm = lident mterm_gen
and mterm__node = (lident, mterm) mterm_node
and 'id fail_type_gen =
  1. | Invalid of 'id mterm_gen
  2. | InvalidCaller
  3. | InvalidCondition of Ident.ident option
  4. | NoTransfer
  5. | AssignNat
  6. | InvalidState
and fail_type = lident fail_type_gen
and api_container_kind =
  1. | Coll
  2. | View
  3. | Field of Ident.ident * Ident.ident
and api_list =
  1. | Lprepend of type_
  2. | Lcontains of type_
  3. | Llength of type_
  4. | Lnth of type_
  5. | Lreverse of type_
and api_builtin =
  1. | Bmin of type_
  2. | Bmax of type_
  3. | Babs of type_
  4. | Bconcat of type_
  5. | Bslice of type_
  6. | Blength of type_
  7. | Bisnone of type_
  8. | Bissome of type_
  9. | Boptget of type_
  10. | Bfloor
  11. | Bceil
  12. | Btostring of type_
  13. | Bfail of type_
and api_internal =
  1. | RatEq
  2. | RatCmp
  3. | RatArith
  4. | RatUminus
  5. | RatTez
  6. | RatDur
and api_storage_node =
  1. | APIAsset of api_asset
  2. | APIList of api_list
  3. | APIBuiltin of api_builtin
  4. | APIInternal of api_internal
and api_loc =
  1. | OnlyFormula
  2. | OnlyExec
  3. | ExecFormula
and api_storage = {
  1. node_item : api_storage_node;
  2. api_loc : api_loc;
}
and api_verif =
  1. | StorageInvariant of Ident.ident * Ident.ident * mterm
and entry_description =
  1. | ADany
  2. | ADadd of Ident.ident
  3. | ADremove of Ident.ident
  4. | ADupdate of Ident.ident
  5. | ADtransfer of Ident.ident
  6. | ADget of Ident.ident
  7. | ADiterate of Ident.ident
  8. | ADcall of Ident.ident
and security_role = lident
and security_entry =
  1. | Sany
  2. | 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 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 = {
  1. label : 'id;
  2. term : 'id mterm_gen;
  3. 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 =
  1. | MTvar
  2. | MTconst
  3. | MTasset of Ident.ident
  4. | MTstate
  5. | 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 = {
  1. id : 'id;
  2. model_type : model_type;
  3. typ : type_;
  4. const : bool;
  5. ghost : bool;
  6. default : 'id mterm_gen;
  7. 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 = {
  1. name : 'id;
  2. 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 'id var_gen = {
  1. name : 'id;
  2. type_ : type_;
  3. original_type : type_;
  4. constant : bool;
  5. default : 'id mterm_gen option;
  6. invariants : 'id label_term_gen list;
  7. 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 = {
  1. name : 'id;
  2. values : 'id enum_item_gen list;
  3. 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
type 'id asset_item_gen = {
  1. name : 'id;
  2. type_ : type_;
  3. original_type : type_;
  4. default : 'id mterm_gen option;
  5. shadow : bool;
  6. 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 = {
  1. name : 'id;
  2. values : 'id asset_item_gen list;
  3. keys : Ident.ident list;
  4. sort : 'id list;
  5. big_map : bool;
  6. state : lident option;
  7. invariants : lident label_term_gen list;
  8. init : 'id mterm_gen list;
  9. 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
type 'id record_field_gen = {
  1. name : 'id;
  2. type_ : type_;
  3. 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 = {
  1. name : 'id;
  2. fields : 'id record_field_gen list;
  3. 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_ = {
  1. 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 = {
  1. 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 = {
  1. name : 'id;
  2. args : 'id argument_gen list;
  3. eargs : 'id argument_gen list;
  4. body : 'id mterm_gen;
  5. 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 =
  1. | Function of 'id function_struct_gen * type_
  2. | Getter of 'id function_struct_gen * type_
  3. | 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 = {
  1. name : 'id;
  2. args : 'id argument_gen list;
  3. 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 = {
  1. decl : 'id argument_gen;
  2. constant : bool;
  3. 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 = {
  1. name : 'id;
  2. args : ('id * type_) list;
  3. body : 'id mterm_gen;
  4. 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 = {
  1. name : 'id;
  2. typ : type_;
  3. var : 'id;
  4. body : 'id mterm_gen;
  5. 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 = {
  1. label : 'id;
  2. 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 = {
  1. label : 'id;
  2. arg : 'id;
  3. atype : type_;
  4. formula : 'id mterm_gen;
  5. 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
type spec_mode =
  1. | Post
  2. | 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 = {
  1. name : 'id;
  2. mode : spec_mode;
  3. formula : 'id mterm_gen;
  4. invariants : 'id invariant_gen list;
  5. 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 = {
  1. name : 'id;
  2. label : 'id;
  3. formula : 'id mterm_gen;
  4. invariants : 'id invariant_gen list;
  5. 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 = {
  1. predicates : 'id predicate_gen list;
  2. definitions : 'id definition_gen list;
  3. lemmas : 'id label_term_gen list;
  4. theorems : 'id label_term_gen list;
  5. fails : 'id fail_gen list;
  6. variables : 'id variable_gen list;
  7. invariants : ('id * 'id label_term_gen list) list;
  8. effects : 'id mterm_gen list;
  9. postconditions : 'id postcondition_gen list;
  10. 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 =
  1. | SonlyByRole of entry_description * security_role list
  2. | SonlyInEntry of entry_description * security_entry
  3. | SonlyByRoleInEntry of entry_description * security_role list * security_entry
  4. | SnotByRole of entry_description * security_role list
  5. | SnotInEntry of entry_description * security_entry
  6. | SnotByRoleInEntry of entry_description * security_role list * security_entry
  7. | StransferredBy of entry_description
  8. | StransferredTo of entry_description
  9. | 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 = {
  1. s_node : security_node;
  2. 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 = {
  1. label : lident;
  2. predicate : security_predicate;
  3. 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 = {
  1. items : security_item list;
  2. 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 = {
  1. node : 'id function_node_gen;
  2. 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 =
  1. | Dvar of 'id var_gen
  2. | Denum of 'id enum_gen
  3. | Dasset of 'id asset_gen
  4. | 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 model_gen = {
  1. name : lident;
  2. api_items : api_storage list;
  3. api_verif : api_verif list;
  4. decls : 'id decl_node_gen list;
  5. storage : 'id storage_gen;
  6. functions : 'id function__gen list;
  7. specification : 'id specification_gen;
  8. security : security;
  9. 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 =
  1. | Ppostcondition of postcondition * Ident.ident option
  2. | PstorageInvariant of label_term * Ident.ident
  3. | 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 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 : ?constant:bool -> ?loc:Location.t -> 'a argument_gen -> '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 : ?constant:bool -> ?invariants:'id label_term_gen list -> ?default:'id mterm_gen -> ?loc:Location.t -> 'id -> type_ -> type_ -> 'id var_gen
val mk_enum : ?values:'id enum_item_gen list -> 'id -> 'id -> 'id enum_gen
val mk_enum_item : ?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 -> ?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 : ?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 tunit : type_
val tbool : type_
val tnat : type_
val tint : type_
val tstring : type_
val tbytes : type_
val ttez : type_
val tkey : type_
val tkeyhash : type_
val ttimestamp : type_
val taddress : type_
val toption : type_ -> type_
val tset : type_ -> type_
val tlist : type_ -> type_
val tmap : type_ -> type_ -> type_
val tbig_map : 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 tchainid : 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 unit : 'a mterm_gen
val mtrue : 'a mterm_gen
val mfalse : '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_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_none : type_ -> '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 cmp_ident : Ident.ident -> Ident.ident -> 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_type : type_ -> type_ -> bool
val cmp_pattern_node : ('id -> 'id -> bool) -> 'id pattern_node -> 'id 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) -> (lident, mterm) mterm_node -> (lident, mterm) 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_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 = {
  1. formula : bool;
  2. fs : 'id function_struct_gen option;
  3. label : 'id option;
  4. spec_id : 'id option;
  5. invariant_id : 'id option;
  6. 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 =
  1. | KIarchetype
  2. | KIdeclvarname
  3. | KIassetname
  4. | KIassetfield
  5. | KIassetstate
  6. | KIassetinit
  7. | KIrecordname
  8. | KIrecordfield
  9. | KIparamlambda
  10. | KIenumname
  11. | KIenumvalue
  12. | KIcontractname
  13. | KIcontractentry
  14. | KIstoragefield
  15. | KIentry
  16. | KIfunction
  17. | KIgetter
  18. | KIargument
  19. | KIlocalvar
  20. | KIlabel
  21. | KIpredicate
  22. | KIdefinition
  23. | KIdefinitionvar
  24. | KIinvariant
  25. | KIpostcondition
  26. | KIpostconditionuse
  27. | KIfaillabel
  28. | KIfailarg
  29. | KIsecurityad
  30. | KIsecurityrole
  31. | KIsecurityentry
  32. | 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 =
  1. | Eadded of Ident.ident
  2. | Eremoved of Ident.ident
  3. | 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
OCaml

Innovation. Community. Security.