package archetype

  1. Overview
  2. Docs
val show_lident : lident -> Ppx_deriving_runtime.string
type currency =
  1. | Tz
  2. | Mtz
val show_currency : currency -> Ppx_deriving_runtime.string
type container =
  1. | Collection
  2. | Partition
  3. | List
val show_container : container -> Ppx_deriving_runtime.string
type btyp =
  1. | Bbool
  2. | Bint
  3. | Brational
  4. | Bdate
  5. | Bduration
  6. | Bstring
  7. | Baddress
  8. | Brole
  9. | Bcurrency
  10. | Bkey
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. | Tcontract of lident
  4. | Tbuiltin of btyp
  5. | Tcontainer of type_ * container
  6. | Toption of type_
  7. | Ttuple of type_ list
  8. | Tassoc of btyp * type_
  9. | Tunit
  10. | Tstorage
  11. | Toperation
  12. | Tentry
  13. | Tprog of type_
  14. | Tvset of vset * type_
  15. | 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 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. | Mif of 'term * 'term * 'term option
  2. | Mmatchwith of 'term * ('id pattern_gen * 'term) list
  3. | Mapp of 'id * 'term list
  4. | Maddshallow of Ident.ident * 'term list
  5. | Mexternal of 'id * 'id * 'term * 'term list
  6. | Mget of Ident.ident * 'term
  7. | Mset of Ident.ident * Ident.ident list * 'term * 'term
  8. | Maddasset of Ident.ident * 'term
  9. | Maddfield of Ident.ident * Ident.ident * 'term * 'term
  10. | Maddlocal of 'term * 'term
  11. | Mremoveasset of Ident.ident * 'term
  12. | Mremovefield of Ident.ident * Ident.ident * 'term * 'term
  13. | Mremovelocal of 'term * 'term
  14. | Mremoveif of Ident.ident * 'term * 'term
  15. | Mclearasset of Ident.ident
  16. | Mclearfield of Ident.ident * Ident.ident * 'term
  17. | Mclearlocal of 'term
  18. | Mreverseasset of Ident.ident
  19. | Mreversefield of Ident.ident * Ident.ident * 'term
  20. | Mreverselocal of 'term
  21. | Mselect of Ident.ident * 'term * 'term
  22. | Msort of Ident.ident * 'term * Ident.ident * sort_kind
  23. | Mcontains of Ident.ident * 'term * 'term
  24. | Mmem of Ident.ident * 'term * 'term
  25. | Msubsetof of Ident.ident * 'term * 'term
  26. | Mnth of Ident.ident * 'term * 'term
  27. | Mcount of Ident.ident * 'term
  28. | Msum of Ident.ident * 'id * 'term
  29. | Mmin of Ident.ident * 'id * 'term
  30. | Mmax of Ident.ident * 'id * 'term
  31. | Mmathmax of 'term * 'term
  32. | Mmathmin of 'term * 'term
  33. | Mhead of Ident.ident * 'term * 'term
  34. | Mtail of Ident.ident * 'term * 'term
  35. | Mfail of 'id fail_type_gen
  36. | Mand of 'term * 'term
  37. | Mor of 'term * 'term
  38. | Mimply of 'term * 'term
  39. | Mequiv of 'term * 'term
  40. | Misempty of Ident.ident * 'term
  41. | Mnot of 'term
  42. | Mmulticomp of 'term * (comparison_operator * 'term) list
  43. | Mequal of 'term * 'term
  44. | Mnequal of 'term * 'term
  45. | Mgt of 'term * 'term
  46. | Mge of 'term * 'term
  47. | Mlt of 'term * 'term
  48. | Mle of 'term * 'term
  49. | Mplus of 'term * 'term
  50. | Mminus of 'term * 'term
  51. | Mmult of 'term * 'term
  52. | Mdiv of 'term * 'term
  53. | Mmodulo of 'term * 'term
  54. | Muplus of 'term
  55. | Muminus of 'term
  56. | Mrecord of 'term list
  57. | Mletin of 'id list * 'term * type_ option * 'term
  58. | Mvarstorevar of 'id
  59. | Mvarstorecol of 'id
  60. | Mvarenumval of 'id
  61. | Mvarlocal of 'id
  62. | Mvarparam of 'id
  63. | Mvarfield of 'id
  64. | Mvarthe
  65. | Mstate
  66. | Mnow
  67. | Mtransferred
  68. | Mcaller
  69. | Mbalance
  70. | Mnone
  71. | Msome of 'term
  72. | Marray of 'term list
  73. | Mint of Core.big_int
  74. | Muint of Core.big_int
  75. | Mbool of bool
  76. | Menum of string
  77. | Mrational of Core.big_int * Core.big_int
  78. | Mdate of string
  79. | Mstring of string
  80. | Mcurrency of Core.big_int * currency
  81. | Maddress of string
  82. | Mduration of Core.duration
  83. | Mdotasset of 'term * 'id
  84. | Mdotcontract of 'term * 'id
  85. | Mtuple of 'term list
  86. | Massoc of 'term * 'term
  87. | Mfor of 'id * 'term * 'term * Ident.ident option
  88. | Miter of 'id * 'term * 'term * 'term * Ident.ident option
  89. | Mfold of 'id * 'id list * 'term * 'term
  90. | Mseq of 'term list
  91. | Massign of assignment_operator * 'id * 'term
  92. | Massignfield of assignment_operator * 'id * 'id * 'term
  93. | Mtransfer of 'term * bool * 'id qualid_gen option
  94. | Mbreak
  95. | Massert of 'term
  96. | Mreturn of 'term
  97. | Mlabel of 'id
  98. | Mshallow of Ident.ident * 'term
  99. | Munshallow of Ident.ident * 'term
  100. | Mlisttocoll of Ident.ident * 'term
  101. | Mtokeys of Ident.ident * 'term
  102. | Mforall of 'id * type_ * 'term option * 'term
  103. | Mexists of 'id * type_ * 'term option * 'term
  104. | Msetbefore of 'term
  105. | Msetunmoved of 'term
  106. | Msetadded of 'term
  107. | Msetremoved of 'term
  108. | Msetiterated of 'term
  109. | Msettoiterate of 'term
and 'id mterm_gen = {
  1. node : ('id, 'id mterm_gen) mterm_node;
  2. type_ : type_;
  3. subvars : Ident.ident list;
  4. 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 storage_const =
  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. | Reverse of Ident.ident
  7. | UpdateAdd of Ident.ident * Ident.ident
  8. | UpdateRemove of Ident.ident * Ident.ident
  9. | UpdateClear of Ident.ident * Ident.ident
  10. | UpdateReverse of Ident.ident * Ident.ident
  11. | ToKeys of Ident.ident
and container_const =
  1. | AddItem of type_
  2. | RemoveItem of type_
  3. | ClearItem of type_
  4. | ReverseItem of type_
and function_const =
  1. | Select of Ident.ident * mterm
  2. | Sort of Ident.ident * Ident.ident
  3. | Contains of Ident.ident
  4. | Nth of Ident.ident
  5. | Count of Ident.ident
  6. | Sum of Ident.ident * Ident.ident
  7. | Min of Ident.ident * Ident.ident
  8. | Max of Ident.ident * Ident.ident
  9. | Shallow of Ident.ident
  10. | Unshallow of Ident.ident
  11. | Listtocoll of Ident.ident
  12. | Head of Ident.ident
  13. | Tail of Ident.ident
and builtin_const =
  1. | MinBuiltin of type_
  2. | MaxBuiltin of type_
and api_item_node =
  1. | APIStorage of storage_const
  2. | APIContainer of container_const
  3. | APIFunction of function_const
  4. | APIBuiltin of builtin_const
and api_item = {
  1. node_item : api_item_node;
  2. only_formula : bool;
}
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_storage_const : storage_const -> Ppx_deriving_runtime.string
val show_container_const : container_const -> Ppx_deriving_runtime.string
val show_function_const : function_const -> Ppx_deriving_runtime.string
val show_builtin_const : builtin_const -> Ppx_deriving_runtime.string
val show_api_item_node : api_item_node -> Ppx_deriving_runtime.string
val show_api_item : api_item -> 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 info_var = {
  1. name : Ident.ident;
  2. type_ : type_;
  3. constant : bool;
  4. init : mterm option;
}
val show_info_var : info_var -> Ppx_deriving_runtime.string
type info_enum = {
  1. name : Ident.ident;
  2. values : Ident.ident list;
}
val show_info_enum : info_enum -> Ppx_deriving_runtime.string
type info_asset = {
  1. name : Ident.ident;
  2. key : Ident.ident;
  3. sort : Ident.ident list;
  4. values : (Ident.ident * type_ * mterm option) list;
}
val show_info_asset : info_asset -> Ppx_deriving_runtime.string
type info_contract = {
  1. name : Ident.ident;
  2. signatures : (Ident.ident * type_ list) list;
}
val show_info_contract : info_contract -> Ppx_deriving_runtime.string
type info_item =
  1. | Ivar of info_var
  2. | Ienum of info_enum
  3. | Iasset of info_asset
  4. | Icontract of info_contract
val show_info_item : info_item -> Ppx_deriving_runtime.string
type 'id label_term_gen = {
  1. label : 'id option;
  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 'id storage_item_gen = {
  1. name : 'id;
  2. asset : 'id option;
  3. typ : type_;
  4. ghost : bool;
  5. default : 'id mterm_gen;
  6. invariants : lident label_term_gen list;
  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 enum_gen = {
  1. name : 'id;
  2. values : 'id enum_item_gen list;
}
type enum = lident enum_gen
type 'id record_item_gen = {
  1. name : 'id;
  2. type_ : type_;
  3. default : 'id mterm_gen option;
}
type record_item = lident record_item_gen
val show_record_item : record_item -> Ppx_deriving_runtime.string
type 'id record_gen = {
  1. name : 'id;
  2. key : 'id option;
  3. values : 'id record_item_gen list;
}
type record = lident record_gen
val show_record : record -> Ppx_deriving_runtime.string
type 'id contract_signature_gen = {
  1. name : 'id;
  2. args : 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;
}
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;
}
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. | Denum of 'id enum_gen
  2. | Drecord of 'id record_gen
  3. | 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_item list;
  3. info : info_item 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;
}
type model = lident model_gen
val mk_qualid : ?loc:Location.t -> ('id, 'id qualid_gen) qualid_node -> type_ -> 'id0 qualid_gen
val mk_pattern : ?loc:Location.t -> 'id pattern_node -> 'id0 pattern_gen
val mk_mterm : ?subvars:Ident.ident list -> ?loc:Location.t -> ('id, 'id mterm_gen) mterm_node -> type_ -> 'id0 mterm_gen
val mk_label_term : ?label:'id -> ?loc:Location.t -> 'id0 mterm_gen -> 'id1 label_term_gen
val mk_variable : ?constant:bool -> ?from:'a qualid_gen -> ?to_:'b qualid_gen -> ?loc:Location.t -> 'c argument_gen -> 'c variable_gen
val mk_predicate : ?args:('a * type_) list -> ?loc:Location.t -> 'b -> 'c mterm_gen -> 'd predicate_gen
val mk_definition : ?loc:Location.t -> 'a -> type_ -> 'b -> 'c mterm_gen -> 'd definition_gen
val mk_invariant : ?formulas:'a mterm_gen list -> 'b -> 'c invariant_gen
val mk_postcondition : ?invariants:'a invariant_gen list -> 'b -> spec_mode -> 'c mterm_gen -> 'd postcondition_gen
val mk_assert : ?invariants:'a invariant_gen list -> 'b -> 'c -> 'd mterm_gen -> 'e assert_gen
val mk_specification : ?predicates:'a predicate_gen list -> ?definitions:'b definition_gen list -> ?lemmas:'c label_term_gen list -> ?theorems:'d label_term_gen list -> ?variables:'e variable_gen list -> ?invariants:('f * 'f label_term_gen list) list -> ?effects:'g mterm_gen list -> ?postconditions:'h postcondition_gen list -> ?asserts:'i 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_info_var : ?constant:bool -> ?init:mterm -> Ident.ident -> type_ -> info_var
val mk_info_enum : ?values:Ident.ident list -> Ident.ident -> info_enum
val mk_info_asset : ?values:(Ident.ident * type_ * mterm option) list -> ?sort:Ident.ident list -> Ident.ident -> Ident.ident -> info_asset
val mk_info_contract : ?signatures:(Ident.ident * type_ list) list -> Ident.ident -> info_contract
val mk_enum : ?values:'id enum_item_gen list -> 'id0 -> 'id1 enum_gen
val mk_enum_item : ?invariants:'id label_term_gen list -> 'id0 -> 'id1 enum_item_gen
val mk_record : ?values:'id record_item_gen list -> ?key:'id0 -> 'id1 -> 'id2 record_gen
val mk_record_item : ?default:'id mterm_gen -> 'id0 -> type_ -> 'id1 record_item_gen
val mk_contract_signature : ?args:type_ list -> ?loc:Location.t -> 'id -> 'id0 contract_signature_gen
val mk_contract : ?signatures:'id contract_signature_gen list -> ?init:'id0 mterm_gen -> ?loc:Location.t -> 'id1 -> 'id2 contract_gen
val mk_storage_item : ?asset:'id -> ?ghost:bool -> ?invariants:lident label_term_gen list -> ?loc:Location.t -> 'id0 -> type_ -> 'id1 mterm_gen -> 'id2 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 -> 'id0 function_node_gen -> 'id1 function__gen
val mk_signature : ?args:'id argument_gen list -> ?ret:type_ -> 'id0 -> 'id1 signature_gen
val mk_api_item : ?only_formula:bool -> api_item_node -> api_item
val mk_model : ?api_items:api_item list -> ?info:info_item list -> ?decls:lident decl_node_gen list -> ?functions:lident function__gen list -> ?storage:'a list -> ?specification:lident specification_gen -> ?security:security -> lident storage_gen -> 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_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) -> 'id0 fail_type_gen -> 'id1 fail_type_gen -> bool
val cmp_type : type_ -> type_ -> bool
val cmp_pattern_node : ('id -> 'id -> bool) -> 'id0 pattern_node -> 'id1 pattern_node -> bool
val cmp_pattern : lident pattern_gen -> lident pattern_gen -> bool
val cmp_qualid_node : ('q -> 'q -> bool) -> ('id -> 'id -> bool) -> ('id0, 'q0) qualid_node -> ('id1, 'q1) 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_item_node -> api_item_node -> bool
val map_term_node : ('id mterm_gen -> 'id mterm_gen) -> ('a, 'id mterm_gen) mterm_node -> ('b, 'id mterm_gen) mterm_node
val map_gen_mterm : ('a -> ('id, 'id mterm_gen) mterm_node -> ('id0, 'id0 mterm_gen) mterm_node) -> 'b -> 'id1 mterm_gen -> 'id2 mterm_gen
val map_mterm : ('a mterm_gen -> 'a mterm_gen) -> 'b mterm_gen -> 'b 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:'id0 -> ?spec_id:'id1 -> ?invariant_id:'id2 -> 't -> ('id3, 't0) ctx_model_gen
val map_mterm_model_exec : 't -> ((lident, 't0) ctx_model_gen -> mterm -> mterm) -> model -> model
val map_mterm_model_formula : 't -> ((lident, 't0) ctx_model_gen -> mterm -> mterm) -> model -> model
val map_mterm_model_gen : 't -> ((lident, 't0) 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) -> 'a0 -> 'id0 mterm_gen -> 'a1
val fold_map_term_list : ('a -> 'b -> 'term * 'a0) -> 'a1 -> 'c list -> 'term0 list * 'a2
val fold_map_term : (('id, 'id mterm_gen) mterm_node -> 'id mterm_gen) -> ('a -> 'id0 mterm_gen -> 'id0 mterm_gen * 'a) -> 'a0 -> 'id1 mterm_gen -> 'id2 mterm_gen * 'a1
val fold_left : ('a -> 'b -> 'c) -> 'd list -> 'e -> 'f
val fold_specification : ('id, 't) ctx_model_gen -> (('id0, 't0) ctx_model_gen -> 'a -> 'id0 mterm_gen -> 'a) -> 'id1 specification_gen -> 'a0 -> 'a1
val fold_model : ((lident, unit) ctx_model_gen -> 'a -> lident mterm_gen -> 'a) -> lident model_gen -> 'a0 -> 'a1
val merge_seq : mterm -> mterm -> mterm
val extract_list : mterm -> mterm -> mterm list
module Utils : sig ... end