package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
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. | Tunit
  13. | Tstorage
  14. | Toperation
  15. | Tentrysig of type_
  16. | Tprog of type_
  17. | Tvset of vset * type_
  18. | Ttrace of trtyp
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 =
  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. | Vlocal
  6. | Vparam
  7. | Vfield
  8. | Vstate
  9. | 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 'term container_kind_gen =
  1. | CKcoll
  2. | CKview of 'term
  3. | CKfield of Ident.ident * Ident.ident * 'term
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. | Mnone
  36. | Msome of 'term
  37. | Mtuple of 'term list
  38. | Masset of 'term list
  39. | Massets of 'term list
  40. | Mlitset of 'term list
  41. | Mlitlist of 'term list
  42. | Mlitmap of ('term * 'term) list
  43. | Mlitrecord of (Ident.ident * 'term) list
  44. | Mdot of 'term * 'id
  45. | Mdotassetfield of 'id * 'term * 'id
  46. | Mdotcontract of 'term * 'id
  47. | Maccestuple of 'term * Core.big_int
  48. | Mequal of type_ * 'term * 'term
  49. | Mnequal of type_ * 'term * 'term
  50. | Mgt of 'term * 'term
  51. | Mge of 'term * 'term
  52. | Mlt of 'term * 'term
  53. | Mle of 'term * 'term
  54. | Mmulticomp of 'term * (comparison_operator * 'term) list
  55. | Mand of 'term * 'term
  56. | Mor 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. | Muplus of 'term
  65. | Muminus of 'term
  66. | Maddasset of Ident.ident * 'term
  67. | Maddfield of Ident.ident * Ident.ident * 'term * 'term
  68. | Mremoveasset of Ident.ident * 'term
  69. | Mremovefield of Ident.ident * Ident.ident * 'term * 'term
  70. | Mremoveall of Ident.ident * Ident.ident * 'term
  71. | Mremoveif of Ident.ident * 'term container_kind_gen * (Ident.ident * type_) list * 'term * 'term list
  72. | Mclear of Ident.ident * 'term container_kind_gen
  73. | Mset of Ident.ident * Ident.ident list * 'term * 'term
  74. | Mupdate of Ident.ident * 'term * ('id * assignment_operator * 'term) list
  75. | Maddupdate of Ident.ident * 'term container_kind_gen * 'term * ('id * assignment_operator * 'term) list
  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. | Msetadd of type_ * 'term * 'term
  88. | Msetremove of type_ * 'term * 'term
  89. | Msetcontains of type_ * 'term * 'term
  90. | Msetlength of type_ * 'term
  91. | Mlistprepend of type_ * 'term * 'term
  92. | Mlistcontains of type_ * 'term * 'term
  93. | Mlistlength of type_ * 'term
  94. | Mlistnth of type_ * 'term * 'term
  95. | Mmapput of type_ * type_ * 'term * 'term * 'term
  96. | Mmapremove of type_ * type_ * 'term * 'term
  97. | Mmapget of type_ * type_ * 'term * 'term
  98. | Mmapgetopt of type_ * type_ * 'term * 'term
  99. | Mmapcontains of type_ * type_ * 'term * 'term
  100. | Mmaplength of type_ * type_ * 'term
  101. | Mmin of 'term * 'term
  102. | Mmax of 'term * 'term
  103. | Mabs of 'term
  104. | Mconcat of 'term * 'term
  105. | Mslice of 'term * 'term * 'term
  106. | Mlength of 'term
  107. | Misnone of 'term
  108. | Missome of 'term
  109. | Moptget of 'term
  110. | Mfloor of 'term
  111. | Mceil of 'term
  112. | Mtostring of type_ * 'term
  113. | Mpack of 'term
  114. | Munpack of type_ * 'term
  115. | Mblake2b of 'term
  116. | Msha256 of 'term
  117. | Msha512 of 'term
  118. | Mhashkey of 'term
  119. | Mchecksignature of 'term * 'term * 'term
  120. | Mnow
  121. | Mtransferred
  122. | Mcaller
  123. | Mbalance
  124. | Msource
  125. | Mselfaddress
  126. | Mchainid
  127. | Mvar of 'id * 'term var_kind_gen
  128. | Mrateq of 'term * 'term
  129. | Mratcmp of comparison_operator * 'term * 'term
  130. | Mratarith of rat_arith_op * 'term * 'term
  131. | Mratuminus of 'term
  132. | Mrattez of 'term * 'term
  133. | Mdivtez of 'term * 'term
  134. | Mnattoint of 'term
  135. | Mnattorat of 'term
  136. | Minttorat of 'term
  137. | Mratdur of 'term * 'term
  138. | Mfold of 'id * 'id list * 'term * 'term
  139. | Mbreak
  140. | Mforall of 'id * type_ * 'term option * 'term
  141. | Mexists of 'id * type_ * 'term option * 'term
  142. | Mimply of 'term * 'term
  143. | Mequiv of 'term * 'term
  144. | Msetbefore of 'term
  145. | Msetat of Ident.ident * 'term
  146. | Msetunmoved of 'term
  147. | Msetadded of 'term
  148. | Msetremoved of 'term
  149. | Msetiterated of 'term iter_container_kind_gen
  150. | Msettoiterate of 'term iter_container_kind_gen
  151. | Mempty of Ident.ident
  152. | Msingleton of Ident.ident * 'term
  153. | Msubsetof of Ident.ident * 'term container_kind_gen * 'term
  154. | Misempty of Ident.ident * 'term
  155. | Munion of Ident.ident * 'term * 'term
  156. | Minter of Ident.ident * 'term * 'term
  157. | 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_
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. | DivTez
  7. | 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
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. body : 'id mterm_gen;
  4. 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. | 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 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. variables : 'id variable_gen list;
  6. invariants : ('id * 'id label_term_gen list) list;
  7. effects : 'id mterm_gen list;
  8. postconditions : 'id postcondition_gen list;
  9. 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_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 -> ?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 -> ?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 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_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. | KIargument
  18. | KIlocalvar
  19. | KIlabel
  20. | KIpredicate
  21. | KIdefinition
  22. | KIdefinitionvar
  23. | KIinvariant
  24. | KIpostcondition
  25. | KIpostconditionuse
  26. | KIsecurityad
  27. | KIsecurityrole
  28. | KIsecurityentry
  29. | 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
module Utils : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct