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
  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. | Tstate
  4. | Tcontract of lident
  5. | Tbuiltin of btyp
  6. | Tcontainer of type_ * container
  7. | Toption of type_
  8. | Ttuple of type_ list
  9. | Tassoc of btyp * type_
  10. | Tunit
  11. | Tstorage
  12. | Toperation
  13. | Tentry
  14. | Tprog of type_
  15. | Tvset of vset * type_
  16. | 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. | Mgetbefore of Ident.ident * 'term
  8. | Mgetat of Ident.ident * Ident.ident * 'term
  9. | Mset of Ident.ident * Ident.ident list * 'term * 'term
  10. | Maddasset of Ident.ident * 'term
  11. | Maddfield of Ident.ident * Ident.ident * 'term * 'term
  12. | Maddlocal of 'term * 'term
  13. | Mremoveasset of Ident.ident * 'term
  14. | Mremovefield of Ident.ident * Ident.ident * 'term * 'term
  15. | Mremovelocal of 'term * 'term
  16. | Mremoveif of Ident.ident * 'term * 'term
  17. | Mclearasset of Ident.ident
  18. | Mclearfield of Ident.ident * Ident.ident * 'term
  19. | Mclearlocal of 'term
  20. | Mreverseasset of Ident.ident
  21. | Mreversefield of Ident.ident * Ident.ident * 'term
  22. | Mreverselocal of 'term
  23. | Mselect of Ident.ident * 'term * 'term
  24. | Msort of Ident.ident * 'term * Ident.ident * sort_kind
  25. | Mcontains of Ident.ident * 'term * 'term
  26. | Mmem of Ident.ident * 'term * 'term
  27. | Msubsetof of Ident.ident * 'term * 'term
  28. | Mnth of Ident.ident * 'term * 'term
  29. | Mcount of Ident.ident * 'term
  30. | Msum of Ident.ident * 'id * 'term
  31. | Mmin of Ident.ident * 'id * 'term
  32. | Mmax of Ident.ident * 'id * 'term
  33. | Mmathmax of 'term * 'term
  34. | Mmathmin of 'term * 'term
  35. | Mhead of Ident.ident * 'term * 'term
  36. | Mtail of Ident.ident * 'term * 'term
  37. | Mfail of 'id fail_type_gen
  38. | Mand of 'term * 'term
  39. | Mor of 'term * 'term
  40. | Mimply of 'term * 'term
  41. | Mequiv of 'term * 'term
  42. | Misempty of Ident.ident * 'term
  43. | Mnot of 'term
  44. | Mmulticomp of 'term * (comparison_operator * 'term) list
  45. | Mequal of 'term * 'term
  46. | Mnequal of 'term * 'term
  47. | Mgt of 'term * 'term
  48. | Mge of 'term * 'term
  49. | Mlt of 'term * 'term
  50. | Mle of 'term * '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. | Masset of 'term list
  59. | Mletin of 'id list * 'term * type_ option * 'term * 'term option
  60. | Mdeclvar of 'id list * type_ option * 'term
  61. | Mvarstorevar of 'id
  62. | Mvarstorecol of 'id
  63. | Mvarenumval of 'id
  64. | Mvarlocal of 'id
  65. | Mvarparam of 'id
  66. | Mvarfield of 'id
  67. | Mvarthe
  68. | Mvarstate
  69. | Mnow
  70. | Mtransferred
  71. | Mcaller
  72. | Mbalance
  73. | Mnone
  74. | Msome of 'term
  75. | Marray of 'term list
  76. | Mint of Core.big_int
  77. | Muint of Core.big_int
  78. | Mbool of bool
  79. | Menum of string
  80. | Mrational of Core.big_int * Core.big_int
  81. | Mdate of Core.date
  82. | Mstring of string
  83. | Mcurrency of Core.big_int * currency
  84. | Maddress of string
  85. | Mduration of Core.duration
  86. | Mdotasset of 'term * 'id
  87. | Mdotcontract of 'term * 'id
  88. | Mtuple of 'term list
  89. | Massoc of 'term * 'term
  90. | Mfor of 'id * 'term * 'term * Ident.ident option
  91. | Miter of 'id * 'term * 'term * 'term * Ident.ident option
  92. | Mfold of 'id * 'id list * 'term * 'term
  93. | Mseq of 'term list
  94. | Massign of assignment_operator * 'id * 'term
  95. | Massignvarstore of assignment_operator * 'id * 'term
  96. | Massignfield of assignment_operator * 'term * 'id * 'term
  97. | Massignstate of 'term
  98. | Mtransfer of 'term * 'term
  99. | Mbreak
  100. | Massert of 'term
  101. | Mreturn of 'term
  102. | Mlabel of 'id
  103. | Mshallow of Ident.ident * 'term
  104. | Munshallow of Ident.ident * 'term
  105. | Mlisttocoll of Ident.ident * 'term
  106. | Mtokeys of Ident.ident * 'term
  107. | Mcoltokeys of Ident.ident
  108. | Mforall of 'id * type_ * 'term option * 'term
  109. | Mexists of 'id * type_ * 'term option * 'term
  110. | Msetbefore of 'term
  111. | Msetat of Ident.ident * 'term
  112. | Msetunmoved of 'term
  113. | Msetadded of 'term
  114. | Msetremoved of 'term
  115. | Msetiterated of 'term
  116. | Msettoiterate of '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 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
  12. | ColToKeys 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 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_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_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. ghost : bool;
  5. default : 'id mterm_gen;
  6. 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. invariants : lident label_term_gen list;
}
type asset = lident asset_gen
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;
  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_item 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;
}
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 -> ?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: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 : ?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 : ?only_formula:bool -> api_item_node -> api_item
val mk_model : ?api_items:api_item 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 -> 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) -> '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_item_node -> api_item_node -> bool
val cmp_api_verif : api_verif -> api_verif -> bool
val map_term_node : ('id mterm_gen -> 'id mterm_gen) -> ('a, 'id mterm_gen) mterm_node -> ('a, '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
val map_mterm : ('a mterm_gen -> 'a mterm_gen) -> 'a mterm_gen -> 'a 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_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
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