package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
val show_lident : lident -> Ppx_deriving_runtime.string
type currency =
  1. | Tz
  2. | Mtz
  3. | Utz
val show_currency : currency -> Ppx_deriving_runtime.string
type container =
  1. | Collection
  2. | Partition
val show_container : container -> Ppx_deriving_runtime.string
type btyp =
  1. | Bbool
  2. | Bint
  3. | Brational
  4. | Bdate
  5. | Bduration
  6. | Btimestamp
  7. | Bstring
  8. | Baddress
  9. | Brole
  10. | Bcurrency
  11. | Bkey
  12. | Bbytes
  13. | Bnat
type vset =
  1. | VSremoved
  2. | VSadded
  3. | VSstable
  4. | VSbefore
  5. | VSafter
  6. | VSfixed
type trtyp =
  1. | TRentry
  2. | TRaction
  3. | TRasset
  4. | TRfield
type type_ =
  1. | Tasset of lident
  2. | Tenum of lident
  3. | Tstate
  4. | Tcontract of lident
  5. | Tbuiltin of btyp
  6. | Tcontainer of type_ * container
  7. | Tlist of type_
  8. | Toption of type_
  9. | Ttuple of type_ list
  10. | Tassoc of btyp * type_
  11. | Tunit
  12. | Tstorage
  13. | Toperation
  14. | Tentry
  15. | Tprog of type_
  16. | Tvset of vset * type_
  17. | 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
type 'id pattern_gen = {
  1. node : 'id pattern_node;
  2. loc : Location.t;
}
type pattern = lident pattern_gen
val show_pattern : pattern -> Ppx_deriving_runtime.string
type comparison_operator =
  1. | Gt
  2. | Ge
  3. | Lt
  4. | Le
val show_comparison_operator : comparison_operator -> Ppx_deriving_runtime.string
type rat_arith_op =
  1. | Rplus
  2. | Rminus
  3. | Rmult
  4. | Rdiv
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 show_assignment_operator : assignment_operator -> Ppx_deriving_runtime.string
type ('id, 'qualid) qualid_node =
  1. | Qident of 'id
  2. | Qdot of 'qualid * 'id
type 'id qualid_gen = {
  1. node : ('id, 'id qualid_gen) qualid_node;
  2. type_ : type_;
  3. loc : Location.t;
}
type qualid = lident qualid_gen
val show_qualid : qualid -> Ppx_deriving_runtime.string
type sort_kind =
  1. | SKasc
  2. | SKdesc
val show_sort_kind : sort_kind -> 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
  5. | Massignvarstore of assignment_operator * type_ * 'id * 'term
  6. | Massignfield of assignment_operator * type_ * 'term * 'id * 'term
  7. | Massignstate of 'term
  8. | Massignassetstate of Ident.ident * 'term * 'term
  9. | Mif of 'term * 'term * 'term option
  10. | Mmatchwith of 'term * ('id pattern_gen * 'term) list
  11. | Mfor of 'id * 'term * 'term * Ident.ident option
  12. | Miter of 'id * 'term * 'term * 'term * Ident.ident option
  13. | Mseq of 'term list
  14. | Mreturn of 'term
  15. | Mlabel of 'id
  16. | Mfail of 'id fail_type_gen
  17. | Mtransfer of 'term * 'term
  18. | Mentrycall of 'term * 'term * Ident.ident * 'id * ('id * 'term) list
  19. | Mint of Core.big_int
  20. | Muint of Core.big_int
  21. | Mbool of bool
  22. | Menum of string
  23. | Mrational of Core.big_int * Core.big_int
  24. | Mstring of string
  25. | Mcurrency of Core.big_int * currency
  26. | Maddress of string
  27. | Mdate of Core.date
  28. | Mduration of Core.duration
  29. | Mtimestamp of Core.big_int
  30. | Mbytes of string
  31. | Mexprif of 'term * 'term * 'term
  32. | Mexprmatchwith of 'term * ('id pattern_gen * 'term) list
  33. | Mnone
  34. | Msome of 'term
  35. | Marray of 'term list
  36. | Mtuple of 'term list
  37. | Masset of 'term list
  38. | Massoc of 'term * 'term
  39. | Mdotasset of 'term * 'id
  40. | Mdotcontract of 'term * 'id
  41. | Mequal of 'term * 'term
  42. | Mnequal of 'term * 'term
  43. | Mgt of 'term * 'term
  44. | Mge of 'term * 'term
  45. | Mlt of 'term * 'term
  46. | Mle of 'term * 'term
  47. | Mmulticomp of 'term * (comparison_operator * 'term) list
  48. | Mand of 'term * 'term
  49. | Mor of 'term * 'term
  50. | Mnot of 'term
  51. | Mplus of 'term * 'term
  52. | Mminus of 'term * 'term
  53. | Mmult of 'term * 'term
  54. | Mdiv of 'term * 'term
  55. | Mmodulo of 'term * 'term
  56. | Muplus of 'term
  57. | Muminus of 'term
  58. | Maddasset of Ident.ident * 'term
  59. | Maddfield of Ident.ident * Ident.ident * 'term * 'term
  60. | Mremoveasset of Ident.ident * 'term
  61. | Mremovefield of Ident.ident * Ident.ident * 'term * 'term
  62. | Mclearasset of Ident.ident
  63. | Mclearfield of Ident.ident * Ident.ident * 'term
  64. | Mset of Ident.ident * Ident.ident list * 'term * 'term
  65. | Mupdate of Ident.ident * 'term * ('id * assignment_operator * 'term) list
  66. | Mremoveif of Ident.ident * 'term * 'term
  67. | Maddupdate of Ident.ident * 'term * ('id * assignment_operator * 'term) list
  68. | Mget of Ident.ident * 'term
  69. | Mselect of Ident.ident * 'term * 'term
  70. | Msort of Ident.ident * 'term * (Ident.ident * sort_kind) list
  71. | Mcontains of Ident.ident * 'term * 'term
  72. | Mnth of Ident.ident * 'term * 'term
  73. | Mcount of Ident.ident * 'term
  74. | Msum of Ident.ident * 'term * 'term
  75. | Mhead of Ident.ident * 'term * 'term
  76. | Mtail of Ident.ident * 'term * 'term
  77. | Mcast of type_ * type_ * 'term
  78. | Mgetfrommap of Ident.ident * 'term * 'term
  79. | Mlistprepend of type_ * 'term * 'term
  80. | Mlistcontains of type_ * 'term * 'term
  81. | Mlistcount of type_ * 'term
  82. | Mlistnth of type_ * 'term * 'term
  83. | Mmin of 'term * 'term
  84. | Mmax of 'term * 'term
  85. | Mabs of 'term
  86. | Mstrconcat of 'term * 'term
  87. | Mvarstate
  88. | Mnow
  89. | Mtransferred
  90. | Mcaller
  91. | Mbalance
  92. | Msource
  93. | Mvarassetstate of Ident.ident * 'term
  94. | Mvarstorevar of 'id
  95. | Mvarstorecol of 'id
  96. | Mvarenumval of 'id
  97. | Mvarlocal of 'id
  98. | Mvarparam of 'id
  99. | Mvarfield of 'id
  100. | Mvarthe
  101. | Mdivrat of 'term * 'term
  102. | Mrateq of 'term * 'term
  103. | Mratcmp of comparison_operator * 'term * 'term
  104. | Mratarith of rat_arith_op * 'term * 'term
  105. | Mratuminus of 'term
  106. | Mrattez of 'term * 'term
  107. | Minttorat of 'term
  108. | Mfold of 'id * 'id list * 'term * 'term
  109. | Mbreak
  110. | Mshallow of Ident.ident * 'term
  111. | Munshallow of Ident.ident * 'term
  112. | Mlisttocoll of Ident.ident * 'term
  113. | Maddshallow of Ident.ident * 'term list
  114. | Mtokeys of Ident.ident * 'term
  115. | Mcoltokeys of Ident.ident
  116. | Mforall of 'id * type_ * 'term option * 'term
  117. | Mexists of 'id * type_ * 'term option * 'term
  118. | Mimply of 'term * 'term
  119. | Mequiv of 'term * 'term
  120. | Msetbefore of 'term
  121. | Msetat of Ident.ident * 'term
  122. | Msetunmoved of 'term
  123. | Msetadded of 'term
  124. | Msetremoved of 'term
  125. | Msetiterated of 'term
  126. | Msettoiterate of 'term
  127. | Mapifget of Ident.ident * 'term * 'term
  128. | Mapifsubsetof of Ident.ident * 'term * 'term
  129. | Mapifisempty of Ident.ident * 'term
  130. | Mapifselect of Ident.ident * 'term * 'term
  131. | Mapifsort of Ident.ident * 'term * (Ident.ident * sort_kind) list
  132. | Mapifcontains of Ident.ident * 'term * 'term
  133. | Mapifnth of Ident.ident * 'term * 'term
  134. | Mapifcount of Ident.ident * 'term
  135. | Mapifsum of Ident.ident * 'term * 'term
  136. | Mapifhead of Ident.ident * 'term * 'term
  137. | Mapiftail of Ident.ident * 'term * 'term
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. | InvalidState
and fail_type = lident fail_type_gen
and api_asset =
  1. | Get of Ident.ident
  2. | Set of Ident.ident
  3. | Add of Ident.ident
  4. | Remove of Ident.ident
  5. | Clear of Ident.ident
  6. | UpdateAdd of Ident.ident * Ident.ident
  7. | UpdateRemove of Ident.ident * Ident.ident
  8. | UpdateClear of Ident.ident * Ident.ident
  9. | ToKeys of Ident.ident
  10. | ColToKeys of Ident.ident
  11. | Select of Ident.ident * mterm
  12. | Sort of Ident.ident * (Ident.ident * sort_kind) list
  13. | Contains of Ident.ident
  14. | Nth of Ident.ident
  15. | Count of Ident.ident
  16. | Sum of Ident.ident * type_ * mterm
  17. | Min of Ident.ident * Ident.ident
  18. | Max of Ident.ident * Ident.ident
  19. | Shallow of Ident.ident
  20. | Unshallow of Ident.ident
  21. | Listtocoll of Ident.ident
  22. | Head of Ident.ident
  23. | Tail of Ident.ident
and api_list =
  1. | Lprepend of type_
  2. | Lcontains of type_
  3. | Lcount of type_
  4. | Lnth of type_
and api_builtin =
  1. | MinBuiltin of type_
  2. | MaxBuiltin of type_
  3. | AbsBuiltin of type_
and api_internal =
  1. | RatEq
  2. | RatCmp
  3. | RatArith
  4. | RatUminus
  5. | RatTez
  6. | StrConcat
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 action_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_action =
  1. | Sany
  2. | Sentry of lident list
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 show_fail_type : fail_type -> Ppx_deriving_runtime.string
val show_api_asset : api_asset -> Ppx_deriving_runtime.string
val show_api_list : api_list -> Ppx_deriving_runtime.string
val show_api_builtin : api_builtin -> Ppx_deriving_runtime.string
val show_api_internal : api_internal -> Ppx_deriving_runtime.string
val show_api_storage_node : api_storage_node -> Ppx_deriving_runtime.string
val show_api_loc : api_loc -> Ppx_deriving_runtime.string
val show_api_storage : api_storage -> Ppx_deriving_runtime.string
val show_api_verif : api_verif -> Ppx_deriving_runtime.string
val show_action_description : action_description -> Ppx_deriving_runtime.string
val show_security_role : security_role -> Ppx_deriving_runtime.string
val show_security_action : security_action -> Ppx_deriving_runtime.string
type 'id label_term_gen = {
  1. label : 'id;
  2. term : 'id mterm_gen;
  3. loc : Location.t;
}
type label_term = lident label_term_gen
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 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;
}
type storage_item = lident storage_item_gen
type 'id storage_gen = 'id storage_item_gen list
type storage = lident storage_gen
val show_storage : storage -> Ppx_deriving_runtime.string
type 'id enum_item_gen = {
  1. name : 'id;
  2. invariants : 'id label_term_gen list;
}
type enum_item = lident enum_item_gen
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;
}
type var = lident var_gen
type 'id enum_gen = {
  1. name : 'id;
  2. values : 'id enum_item_gen list;
  3. initial : 'id;
}
type enum = lident enum_gen
type 'id asset_item_gen = {
  1. name : 'id;
  2. type_ : type_;
  3. original_type : type_;
  4. default : 'id mterm_gen option;
  5. shadow : bool;
}
type asset_item = lident asset_item_gen
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. key : Ident.ident;
  4. sort : Ident.ident list;
  5. state : lident option;
  6. invariants : lident label_term_gen list;
}
type asset = lident asset_gen
type 'id contract_signature_gen = {
  1. name : 'id;
  2. args : (lident * type_) list;
  3. loc : Location.t;
}
type contract_signature = lident contract_signature_gen
val show_contract_signature : contract_signature -> Ppx_deriving_runtime.string
type 'id contract_gen = {
  1. name : 'id;
  2. signatures : 'id contract_signature_gen list;
  3. init : 'id mterm_gen option;
  4. loc : Location.t;
}
type contract = lident contract_gen
val show_contract : contract -> 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
type argument = lident argument_gen
val show_argument : argument -> Ppx_deriving_runtime.string
type source =
  1. | Exo
  2. | Endo
val show_source : source -> Ppx_deriving_runtime.string
type 'id function_struct_gen = {
  1. name : 'id;
  2. args : 'id argument_gen list;
  3. body : 'id mterm_gen;
  4. src : source;
  5. loc : Location.t;
}
type function_struct = lident function_struct_gen
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
type function_node = lident function_node_gen
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;
}
type signature = lident signature_gen
val show_signature : signature -> Ppx_deriving_runtime.string
type 'id variable_gen = {
  1. decl : 'id argument_gen;
  2. constant : bool;
  3. from : 'id qualid_gen option;
  4. to_ : 'id qualid_gen option;
  5. loc : Location.t;
}
type variable = lident variable_gen
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;
}
type predicate = lident predicate_gen
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;
}
type definition = lident definition_gen
val show_definition : definition -> Ppx_deriving_runtime.string
type 'id invariant_gen = {
  1. label : 'id;
  2. formulas : 'id mterm_gen list;
}
type invariant = lident invariant_gen
val show_invariant : invariant -> Ppx_deriving_runtime.string
type spec_mode =
  1. | Post
  2. | Assert
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;
}
type postcondition = lident postcondition_gen
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;
}
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;
}
type security_node =
  1. | SonlyByRole of action_description * security_role list
  2. | SonlyInAction of action_description * security_action
  3. | SonlyByRoleInAction of action_description * security_role list * security_action
  4. | SnotByRole of action_description * security_role list
  5. | SnotInAction of action_description * security_action
  6. | SnotByRoleInAction of action_description * security_role list * security_action
  7. | StransferredBy of action_description
  8. | StransferredTo of action_description
  9. | SnoStorageFail of security_action
val show_security_node : security_node -> Ppx_deriving_runtime.string
type security_predicate = {
  1. s_node : security_node;
  2. loc : Location.t;
}
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 show_security_item : security_item -> Ppx_deriving_runtime.string
type security = {
  1. items : security_item list;
  2. loc : Location.t;
}
val show_security : security -> Ppx_deriving_runtime.string
type specification = lident specification_gen
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. | Dcontract of 'id contract_gen
type decl_node = lident decl_node_gen
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;
}
type property =
  1. | Ppostcondition of postcondition * Ident.ident option
  2. | PstorageInvariant of label_term * Ident.ident
  3. | PsecurityPredicate of security_item
val show_property : property -> Ppx_deriving_runtime.string
type model = lident model_gen
val mk_qualid : ?loc:Location.t -> ('id, 'id qualid_gen) qualid_node -> type_ -> 'id qualid_gen
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 -> ?from:'a qualid_gen -> ?to_:'a qualid_gen -> ?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:Ident.ident list -> ?state:lident -> ?invariants:lident label_term_gen list -> 'id -> Ident.ident -> 'id asset_gen
val mk_asset_item : ?default:'id mterm_gen -> ?shadow:bool -> 'id -> type_ -> type_ -> 'id asset_item_gen
val mk_contract_signature : ?args:(lident * type_) list -> ?loc:Location.t -> 'id -> 'id contract_signature_gen
val mk_contract : ?signatures:'id contract_signature_gen list -> ?init:'id mterm_gen -> ?loc:Location.t -> 'id -> 'id contract_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 -> ?src:source -> 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_action_description : action_description -> action_description -> bool
val cmp_security_role : lident -> lident -> bool
val cmp_security_action : security_action -> security_action -> 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_qualid_node : ('q -> 'q -> bool) -> ('id -> 'id -> bool) -> ('id, 'q) qualid_node -> ('id, 'q) qualid_node -> bool
val cmp_qualid : lident qualid_gen -> lident qualid_gen -> bool
val cmp_mterm_node : (lident mterm_gen -> lident mterm_gen -> bool) -> (lident -> lident -> bool) -> (lident, lident mterm_gen) mterm_node -> (lident, lident mterm_gen) mterm_node -> bool
val cmp_mterm : mterm -> mterm -> bool
val cmp_api_item_node : api_storage_node -> api_storage_node -> bool
val cmp_api_verif : api_verif -> api_verif -> bool
val map_type : (type_ -> type_) -> type_ -> type_
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 -> 'id mterm_gen -> 'id 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_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_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_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. | KIenumname
  7. | KIenumvalue
  8. | KIcontractname
  9. | KIcontractentry
  10. | KIstoragefield
  11. | KIaction
  12. | KIfunction
  13. | KIargument
  14. | KIlocalvar
  15. | KIlabel
  16. | KIpredicate
  17. | KIdefinition
  18. | KIdefinitionvar
  19. | KIinvariant
  20. | KIpostcondition
  21. | KIpostconditionuse
  22. | KIsecurityad
  23. | KIsecurityrole
  24. | KIsecurityaction
  25. | KImterm
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