package archetype

  1. Overview
  2. Docs
val show_lident : lident -> Ppx_deriving_runtime.string
type currency =
  1. | Tz
  2. | Mtz
  3. | Mutz
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. | 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 * 'term option
  58. | Mdeclvar of 'id list * type_ option * 'term
  59. | Mvarstorevar of 'id
  60. | Mvarstorecol of 'id
  61. | Mvarenumval of 'id
  62. | Mvarlocal of 'id
  63. | Mvarparam of 'id
  64. | Mvarfield of 'id
  65. | Mvarthe
  66. | Mvarstate
  67. | Mnow
  68. | Mtransferred
  69. | Mcaller
  70. | Mbalance
  71. | Mnone
  72. | Msome of 'term
  73. | Marray of 'term list
  74. | Mint of Core.big_int
  75. | Muint of Core.big_int
  76. | Mbool of bool
  77. | Menum of string
  78. | Mrational of Core.big_int * Core.big_int
  79. | Mdate of string
  80. | Mstring of string
  81. | Mcurrency of Core.big_int * currency
  82. | Maddress of string
  83. | Mduration of Core.duration
  84. | Mdotasset of 'term * 'id
  85. | Mdotcontract of 'term * 'id
  86. | Mtuple of 'term list
  87. | Massoc of 'term * 'term
  88. | Mfor of 'id * 'term * 'term * Ident.ident option
  89. | Miter of 'id * 'term * 'term * 'term * Ident.ident option
  90. | Mfold of 'id * 'id list * 'term * 'term
  91. | Mseq of 'term list
  92. | Massign of assignment_operator * 'id * 'term
  93. | Massignfield of assignment_operator * 'term * 'id * 'term
  94. | Massignstate of 'term
  95. | Mtransfer of 'term * bool * 'id qualid_gen option
  96. | Mbreak
  97. | Massert of 'term
  98. | Mreturn of 'term
  99. | Mlabel of 'id
  100. | Mshallow of Ident.ident * 'term
  101. | Munshallow of Ident.ident * 'term
  102. | Mlisttocoll of Ident.ident * 'term
  103. | Mtokeys of Ident.ident * 'term
  104. | Mforall of 'id * type_ * 'term option * 'term
  105. | Mexists of 'id * type_ * 'term option * 'term
  106. | Msetbefore of 'term
  107. | Msetunmoved of 'term
  108. | Msetadded of 'term
  109. | Msetremoved of 'term
  110. | Msetiterated of 'term
  111. | 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
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 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_id =
  1. | SIname of 'id
  2. | SIstate
type 'id storage_item_gen = {
  1. id : 'id storage_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;
  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. | 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. api_verif : api_verif list;
  4. info : info_item list;
  5. decls : 'id decl_node_gen list;
  6. storage : 'id storage_gen;
  7. functions : 'id function__gen list;
  8. specification : 'id specification_gen;
  9. security : security;
}
type property =
  1. | Ppostcondition of postcondition * Ident.ident option
  2. | PstorageInvariant of label_term
  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 : ?label:'id -> ?loc:Location.t -> 'id mterm_gen -> '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_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 -> 'id -> 'id enum_gen
val mk_enum_item : ?invariants:'id label_term_gen list -> 'id -> 'id enum_item_gen
val mk_record : ?values:'id record_item_gen list -> ?key:'id -> 'id -> 'id record_gen
val mk_record_item : ?default:'id mterm_gen -> 'id -> type_ -> 'id record_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 : ?asset:'id -> ?ghost:bool -> ?invariants:lident label_term_gen list -> ?loc:Location.t -> 'id storage_id -> 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 -> ?info:info_item 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