package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
val pp_ident : Format.formatter -> string -> unit
val pp_lident : Format.formatter -> string Location.loced -> unit
type container =
  1. | Collection
  2. | Aggregate
  3. | Partition
  4. | View
val show_container : container -> Ppx_deriving_runtime.string
type currency =
  1. | Tz
  2. | Mtz
  3. | Utz
val show_currency : currency -> Ppx_deriving_runtime.string
type vtyp =
  1. | VTunit
  2. | VTbool
  3. | VTnat
  4. | VTint
  5. | VTrational
  6. | VTdate
  7. | VTduration
  8. | VTstring
  9. | VTaddress
  10. | VTrole
  11. | VTcurrency
  12. | VTkey
  13. | VTkeyhash
  14. | VTsignature
  15. | VTbytes
  16. | VTchainid
type trtyp =
  1. | TRentry
  2. | TRaction
  3. | TRasset
  4. | TRfield
type ptyp =
  1. | Tnamed of int
  2. | Tasset of lident
  3. | Trecord of lident
  4. | Tenum of lident
  5. | Tbuiltin of vtyp
  6. | Tcontainer of ptyp * container
  7. | Tset of ptyp
  8. | Tlist of ptyp
  9. | Tmap of ptyp * ptyp
  10. | Ttuple of ptyp list
  11. | Toption of ptyp
  12. | Toperation
  13. | Tentrysig of ptyp
  14. | Ttrace of trtyp
type type_ = ptyp
val pp_type_ : Ppx_deriving_runtime.Format.formatter -> type_ -> Ppx_deriving_runtime.unit
val show_type_ : type_ -> Ppx_deriving_runtime.string
type logical_operator =
  1. | And
  2. | Or
  3. | Imply
  4. | Equiv
val show_logical_operator : logical_operator -> Ppx_deriving_runtime.string
type comparison_operator =
  1. | Equal
  2. | Nequal
  3. | Gt
  4. | Ge
  5. | Lt
  6. | 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 arithmetic_operator =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | DivRat
  5. | DivEuc
  6. | Modulo
val show_arithmetic_operator : arithmetic_operator -> Ppx_deriving_runtime.string
type unary_arithmetic_operator =
  1. | Uplus
  2. | Uminus
val show_unary_arithmetic_operator : unary_arithmetic_operator -> Ppx_deriving_runtime.string
type operator = [
  1. | `Logical of logical_operator
  2. | `Cmp of comparison_operator
  3. | `Arith of arithmetic_operator
  4. | `Unary of unary_arithmetic_operator
  5. | `Assign of assignment_operator
]
val show_operator : operator -> Ppx_deriving_runtime.string
type const =
  1. | Cstate
  2. | Cnow
  3. | Ctransferred
  4. | Ccaller
  5. | Cfail
  6. | Cbalance
  7. | Csource
  8. | Cselfaddress
  9. | Cconditions
  10. | Centries
  11. | Cnone
  12. | Cany
  13. | Canyentry
  14. | Cresult
  15. | Cchainid
  16. | Coperations
  17. | Cadd
  18. | Caddupdate
  19. | Cceil
  20. | Cclear
  21. | Cconcat
  22. | Ccontains
  23. | Ccount
  24. | Cfloor
  25. | Cget
  26. | Cgetopt
  27. | Cisnone
  28. | Cissome
  29. | Clength
  30. | Cmax
  31. | Cmin
  32. | Cnth
  33. | Cpack
  34. | Cremove
  35. | Cremoveall
  36. | Cremoveif
  37. | Cselect
  38. | Cslice
  39. | Csort
  40. | Csum
  41. | Cunpack
  42. | Cupdate
  43. | Cmkoperation
  44. | Csadd
  45. | Csremove
  46. | Cscontains
  47. | Cslength
  48. | Chead
  49. | Ctail
  50. | Cabs
  51. | Cprepend
  52. | Cmput
  53. | Cmremove
  54. | Cmget
  55. | Cmgetopt
  56. | Cmcontains
  57. | Cmlength
  58. | Cblake2b
  59. | Csha256
  60. | Csha512
  61. | Cchecksignature
  62. | Chashkey
  63. | Cbefore
  64. | Citerated
  65. | Ctoiterate
  66. | Cempty
  67. | Cisempty
  68. | Csingleton
  69. | Csubsetof
  70. | Cunion
  71. | Cinter
  72. | Cdiff
type 'node struct_poly = {
  1. node : 'node;
  2. type_ : ptyp option;
  3. label : Ident.ident option;
  4. loc : Location.t;
}
type 'id qualid_gen = 'id qualid_node struct_poly
and 'id qualid_node =
  1. | Qident of 'id
  2. | Qdot of 'id qualid_gen * 'id
type qualid = lident qualid_gen
val show_qualid : qualid -> Ppx_deriving_runtime.string
type 'id sexpr_gen = 'id sexpr_node struct_poly
and 'id sexpr_node =
  1. | Sref of 'id
  2. | Sor of 'id sexpr_gen * 'id sexpr_gen
  3. | Sany
type sexpr = lident sexpr_gen
type bval_gen = bval_node struct_poly
and bval_node =
  1. | BVint of Core.big_int
  2. | BVnat of Core.big_int
  3. | BVbool of bool
  4. | BVenum of string
  5. | BVrational of Core.big_int * Core.big_int
  6. | BVdate of Core.date
  7. | BVstring of string
  8. | BVcurrency of currency * Core.big_int
  9. | BVaddress of string
  10. | BVduration of Core.duration
  11. | BVbytes of string
  12. | BVunit
val show_bval_gen : bval_gen -> Ppx_deriving_runtime.string
val show_bval_node : bval_node -> Ppx_deriving_runtime.string
type bval = bval_gen
type quantifier =
  1. | Forall
  2. | Exists
val show_quantifier : quantifier -> Ppx_deriving_runtime.string
type 'id pattern_gen = 'id pattern_node struct_poly
and 'id pattern_node =
  1. | Mwild
  2. | Mconst of 'id
type pattern = lident pattern_gen
val show_pattern : pattern -> Ppx_deriving_runtime.string
type 'id call_kind =
  1. | Cid of 'id
  2. | Cconst of const
type var_temporality =
  1. | VTbefore
  2. | VTat of Ident.ident
  3. | VTnone
val show_var_temporality : var_temporality -> Ppx_deriving_runtime.string
type vset =
  1. | Vadded
  2. | Vremoved
  3. | Vunmoved
  4. | Vnone
type 'id term_node =
  1. | Pquantifer of quantifier * 'id * 'id term_gen option * type_ * 'id term_gen
  2. | Pif of 'id term_gen * 'id term_gen * 'id term_gen
  3. | Pmatchwith of 'id term_gen * ('id pattern_gen * 'id term_gen) list
  4. | Pcall of 'id term_gen option * 'id call_kind * 'id term_arg list
  5. | Plogical of logical_operator * 'id term_gen * 'id term_gen
  6. | Pnot of 'id term_gen
  7. | Pmulticomp of 'id term_gen * (comparison_operator * 'id term_gen) list
  8. | Pcomp of comparison_operator * 'id term_gen * 'id term_gen
  9. | Parith of arithmetic_operator * 'id term_gen * 'id term_gen
  10. | Puarith of unary_arithmetic_operator * 'id term_gen
  11. | Precord of 'id term_gen list
  12. | Pletin of 'id * 'id term_gen * ptyp option * 'id term_gen * 'id term_gen option
  13. | Pdeclvar of 'id * ptyp option * 'id term_gen
  14. | Pvar of var_temporality * vset * 'id
  15. | Parray of 'id term_gen list
  16. | Plit of bval
  17. | Pdot of 'id term_gen * 'id
  18. | Pconst of const
  19. | Ptuple of 'id term_gen list
  20. | Ptupleaccess of 'id term_gen * Core.big_int
  21. | Pnone
  22. | Psome of 'id term_gen
  23. | Pcast of ptyp * ptyp * 'id term_gen
  24. | Pself of 'id
  25. | Pentrypoint of ptyp * 'id * 'id term_gen
and 'id term_arg =
  1. | AExpr of 'id term_gen
  2. | AFun of 'id * ptyp * ('id * ptyp * 'id term_gen) list * 'id term_gen
  3. | AEffect of ('id * operator * 'id term_gen) list
  4. | ASorting of bool * 'id
and 'id term_poly = 'id term_node struct_poly
and 'id term_gen = 'id term_poly
type pterm = lident term_gen
type pterm_arg = lident term_arg
val show_pterm_arg : pterm_arg -> Ppx_deriving_runtime.string
type 'id instruction_poly = {
  1. node : 'id instruction_node;
  2. label : string option;
  3. loc : Location.t;
}
and 'id transfer_t =
  1. | TTsimple of 'id term_gen
  2. | TTcontract of 'id term_gen * 'id * type_ * 'id term_gen
  3. | TTentry of 'id term_gen * 'id term_gen
  4. | TTself of 'id * ('id * 'id term_gen) list
and 'id instruction_node =
  1. | Iif of 'id term_gen * 'id instruction_gen * 'id instruction_gen
  2. | Ifor of 'id for_ident * 'id term_gen * 'id instruction_gen
  3. | Iiter of 'id * 'id term_gen * 'id term_gen * 'id instruction_gen
  4. | Iletin of 'id * 'id term_gen * 'id instruction_gen
  5. | Ideclvar of 'id * 'id term_gen
  6. | Iseq of 'id instruction_gen list
  7. | Imatchwith of 'id term_gen * ('id pattern_gen * 'id instruction_gen) list
  8. | Iassign of assignment_operator * ptyp * 'id lvalue_gen * 'id term_gen
  9. | Irequire of bool * 'id term_gen
  10. | Itransfer of 'id term_gen * 'id transfer_t
  11. | Ibreak
  12. | Icall of 'id term_gen option * 'id call_kind * 'id term_arg list
  13. | Ireturn of 'id term_gen
  14. | Ilabel of 'id
  15. | Ifail of 'id term_gen
and 'id for_ident =
  1. | FIsimple of 'id
  2. | FIdouble of 'id * 'id
and 'id instruction_gen = 'id instruction_poly
and instruction = lident instruction_poly
and 'id lvalue_gen = [
  1. | `Var of 'id
  2. | `Field of 'id * 'id term_gen * 'id
]
and lvalue = lident lvalue_gen
val show_instruction : instruction -> Ppx_deriving_runtime.string
val show_lvalue : lvalue -> Ppx_deriving_runtime.string
type 'id decl_gen = {
  1. name : 'id;
  2. typ : ptyp option;
  3. default : 'id term_gen option;
  4. shadow : bool;
  5. loc : Location.t;
}
type 'id label_term = {
  1. label : 'id option;
  2. term : 'id term_gen;
  3. loc : Location.t;
}
type 'id variable = {
  1. decl : 'id decl_gen;
  2. constant : bool;
  3. invs : 'id label_term list;
  4. loc : Location.t;
}
type 'id predicate = {
  1. name : 'id;
  2. args : ('id * type_) list;
  3. body : 'id term_gen;
  4. loc : Location.t;
}
type 'id definition = {
  1. name : 'id;
  2. typ : type_;
  3. var : 'id;
  4. body : 'id term_gen;
  5. loc : Location.t;
}
type 'id invariant = {
  1. label : 'id;
  2. formulas : 'id term_gen list;
}
type 'id postcondition = {
  1. name : 'id;
  2. formula : 'id term_gen;
  3. invariants : 'id invariant list;
  4. uses : 'id list;
}
type 'id assert_ = {
  1. name : 'id;
  2. label : 'id;
  3. formula : 'id term_gen;
  4. invariants : 'id invariant list;
  5. uses : 'id list;
}
val pp_assert_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id assert_ -> Ppx_deriving_runtime.unit
val show_assert_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id assert_ -> Ppx_deriving_runtime.string
type 'id specification = {
  1. predicates : 'id predicate list;
  2. definitions : 'id definition list;
  3. lemmas : 'id label_term list;
  4. theorems : 'id label_term list;
  5. variables : 'id variable list;
  6. invariants : ('id * 'id label_term list) list;
  7. effect : 'id instruction_gen option;
  8. specs : 'id postcondition list;
  9. asserts : 'id assert_ list;
  10. loc : Location.t;
}
type entry_description =
  1. | ADAny
  2. | ADOp of string * lident
val pp_entry_description : Ppx_deriving_runtime.Format.formatter -> entry_description -> Ppx_deriving_runtime.unit
val show_entry_description : entry_description -> Ppx_deriving_runtime.string
type security_role = lident
val show_security_role : security_role -> Ppx_deriving_runtime.string
type security_entry =
  1. | Sany
  2. | Sentry of lident list
val pp_security_entry : Ppx_deriving_runtime.Format.formatter -> security_entry -> Ppx_deriving_runtime.unit
val show_security_entry : security_entry -> Ppx_deriving_runtime.string
type security_node =
  1. | SonlyByRole of entry_description * security_role list
  2. | SonlyInEntry of entry_description * security_entry
  3. | SonlyByRoleInEntry of entry_description * security_role list * security_entry
  4. | SnotByRole of entry_description * security_role list
  5. | SnotInEntry of entry_description * security_entry
  6. | SnotByRoleInEntry of entry_description * security_role list * security_entry
  7. | StransferredBy of entry_description
  8. | StransferredTo of entry_description
  9. | SnoStorageFail of security_entry
val 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 'id function_struct = {
  1. name : 'id;
  2. args : 'id decl_gen list;
  3. body : 'id instruction_gen;
  4. specification : 'id specification option;
  5. return : ptyp;
  6. loc : Location.t;
}
type function_ = lident function_struct
val pp_function_ : Ppx_deriving_runtime.Format.formatter -> function_ -> Ppx_deriving_runtime.unit
val show_function_ : function_ -> Ppx_deriving_runtime.string
type 'id rexpr_gen = 'id rexpr_node struct_poly
and 'id rexpr_node =
  1. | Rany
  2. | Rexpr of 'id term_gen
  3. | Ror of 'id rexpr_gen * 'id rexpr_gen
type rexpr = lident rexpr_gen
type 'id transition = {
  1. from : 'id sexpr_gen;
  2. on : ('id * ptyp * 'id * ptyp) option;
  3. trs : ('id * 'id term_gen option * 'id instruction_gen option) list;
}
type 'id transaction_struct = {
  1. name : 'id;
  2. args : 'id decl_gen list;
  3. calledby : 'id rexpr_gen option;
  4. accept_transfer : bool;
  5. require : 'id label_term list option;
  6. failif : 'id label_term list option;
  7. transition : 'id transition option;
  8. specification : 'id specification option;
  9. functions : 'id function_struct list;
  10. effect : 'id instruction_gen option;
  11. loc : Location.t;
}
type transaction = lident transaction_struct
val show_transaction : transaction -> Ppx_deriving_runtime.string
type 'id enum_item_struct = {
  1. name : 'id;
  2. initial : bool;
  3. invariants : 'id label_term list;
  4. loc : Location.t;
}
type 'id enum_kind =
  1. | EKenum of 'id
  2. | EKstate
type 'id enum_struct = {
  1. kind : 'id enum_kind;
  2. items : 'id enum_item_struct list;
  3. loc : Location.t;
}
type enum = lident enum_struct
type 'id asset_struct = {
  1. name : 'id;
  2. fields : 'id decl_gen list;
  3. keys : 'id list;
  4. sort : 'id list;
  5. big_map : bool;
  6. state : 'id option;
  7. init : 'id term_gen list list;
  8. specs : 'id label_term list;
  9. loc : Location.t;
}
type asset = lident asset_struct
type 'id record_struct = {
  1. name : 'id;
  2. fields : 'id decl_gen list;
  3. loc : Location.t;
}
type record = lident record_struct
type 'id decl_ =
  1. | Dvariable of 'id variable
  2. | Dasset of 'id asset_struct
  3. | Drecord of 'id record_struct
  4. | Denum of 'id enum_struct
val pp_decl_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id decl_ -> Ppx_deriving_runtime.unit
val show_decl_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id decl_ -> Ppx_deriving_runtime.string
type 'id fun_ =
  1. | Ffunction of 'id function_struct
  2. | Ftransaction of 'id transaction_struct
val pp_fun_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id fun_ -> Ppx_deriving_runtime.unit
val show_fun_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id fun_ -> Ppx_deriving_runtime.string
type 'id ast_struct = {
  1. name : 'id;
  2. decls : 'id decl_ list;
  3. funs : 'id fun_ list;
  4. specifications : 'id specification list;
  5. securities : security list;
  6. loc : Location.t;
}
and ast = lident ast_struct
val vtunit : ptyp
val vtbool : ptyp
val vtnat : ptyp
val vtint : ptyp
val vtrational : ptyp
val vtdate : ptyp
val vtduration : ptyp
val vtstring : ptyp
val vtaddress : ptyp
val vtrole : ptyp
val vtcurrency : ptyp
val vtsignature : ptyp
val vtkey : ptyp
val vtkeyhash : ptyp
val vtbytes : ptyp
val vtchainid : ptyp
val mk_sp : ?label:Ident.ident -> ?loc:Location.t -> ?type_:ptyp -> 'a -> 'b struct_poly
val mk_instr : ?label:string -> ?loc:Location.t -> 'a instruction_node -> 'a instruction_poly
val mk_label_term : ?label:'a -> ?loc:Location.t -> 'b term_gen -> 'c label_term
val mk_variable : ?constant:bool -> ?invs:'a label_term list -> ?loc:Location.t -> 'b decl_gen -> 'b variable
val mk_predicate : ?args:('a * type_) list -> ?loc:Location.t -> 'b -> 'c term_gen -> 'd predicate
val mk_definition : ?loc:Location.t -> 'a -> type_ -> 'b -> 'c term_gen -> 'd definition
val mk_invariant : ?formulas:'a term_gen list -> 'b -> 'c invariant
val mk_postcondition : ?invariants:'a invariant list -> ?uses:'b list -> 'c -> 'd term_gen -> 'e postcondition
val mk_assert : ?invariants:'a invariant list -> ?uses:'b list -> 'c -> 'd -> 'e term_gen -> 'f assert_
val mk_specification : ?predicates:'a predicate list -> ?definitions:'b definition list -> ?lemmas:'c label_term list -> ?theorems:'d label_term list -> ?variables:'e variable list -> ?invariants:('f * 'f label_term list) list -> ?effect:'g instruction_gen -> ?specs:'h postcondition list -> ?asserts:'i assert_ list -> ?loc:Location.t -> unit -> 'a specification
val mk_function_struct : ?args:'a decl_gen list -> ?specification:'b specification -> ?loc:Location.t -> 'c -> 'd instruction_gen -> ptyp -> 'e function_struct
val mk_transition : ?on:('a * ptyp * 'a * ptyp) -> ?trs:('b * 'b term_gen option * 'b instruction_gen option) list -> 'c sexpr_gen -> 'c transition
val mk_transaction_struct : ?args:'a decl_gen list -> ?calledby:'b rexpr_gen -> ?accept_transfer:bool -> ?require:'c label_term list -> ?failif:'d label_term list -> ?transition:'e transition -> ?specification:'f specification -> ?functions:'g function_struct list -> ?effect:'h instruction_gen -> ?loc:Location.t -> 'i -> 'j transaction_struct
val mk_enum_item : ?initial:bool -> ?invariants:'id label_term list -> ?loc:Location.t -> 'id0 -> 'id1 enum_item_struct
val mk_enum : ?items:'a enum_item_struct list -> ?loc:Location.t -> 'b enum_kind -> 'b enum_struct
val mk_decl : ?typ:ptyp -> ?default:'a term_gen -> ?shadow:bool -> ?loc:Location.t -> 'b -> 'c decl_gen
val mk_asset : ?fields:'a decl_gen list -> ?keys:'b list -> ?sort:'c list -> ?big_map:bool -> ?state:'d -> ?init:'e term_gen list list -> ?specs:'f label_term list -> ?loc:Location.t -> 'g -> 'h asset_struct
val mk_model : ?decls:'a decl_ list -> ?funs:'b fun_ list -> ?specifications:'c specification list -> ?securities:security list -> ?loc:Location.t -> 'd -> 'e ast_struct
val mk_id : ptyp -> lident -> qualid
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