package archetype

  1. Overview
  2. Docs

Module Archetype.AstSource

Sourceval pp_ident : Format.formatter -> string -> unit
Sourceval pp_lident : Format.formatter -> string Location.loced -> unit
Sourcetype container =
  1. | Collection
  2. | Aggregate
  3. | Partition
  4. | View
Sourcetype currency =
  1. | Tz
  2. | Mtz
  3. | Utz
Sourcetype 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
Sourcetype trtyp =
  1. | TRentry
  2. | TRaction
  3. | TRasset
  4. | TRfield
Sourcetype 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
Sourcetype type_ = ptyp
Sourceval pp_type_ : Ppx_deriving_runtime.Format.formatter -> type_ -> Ppx_deriving_runtime.unit
Sourceval show_type_ : type_ -> Ppx_deriving_runtime.string
Sourcetype logical_operator =
  1. | And
  2. | Or
  3. | Imply
  4. | Equiv
Sourcetype comparison_operator =
  1. | Equal
  2. | Nequal
  3. | Gt
  4. | Ge
  5. | Lt
  6. | Le
Sourceval show_comparison_operator : comparison_operator -> Ppx_deriving_runtime.string
Sourcetype assignment_operator =
  1. | ValueAssign
  2. | PlusAssign
  3. | MinusAssign
  4. | MultAssign
  5. | DivAssign
  6. | AndAssign
  7. | OrAssign
Sourceval show_assignment_operator : assignment_operator -> Ppx_deriving_runtime.string
Sourcetype arithmetic_operator =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | DivRat
  5. | DivEuc
  6. | Modulo
Sourceval show_arithmetic_operator : arithmetic_operator -> Ppx_deriving_runtime.string
Sourcetype unary_arithmetic_operator =
  1. | Uplus
  2. | Uminus
Sourceval show_unary_arithmetic_operator : unary_arithmetic_operator -> Ppx_deriving_runtime.string
Sourcetype 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
]
Sourcetype 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. | Ctostring
  45. | Csadd
  46. | Csremove
  47. | Cscontains
  48. | Cslength
  49. | Chead
  50. | Ctail
  51. | Cabs
  52. | Cprepend
  53. | Cmput
  54. | Cmremove
  55. | Cmget
  56. | Cmgetopt
  57. | Cmcontains
  58. | Cmlength
  59. | Cblake2b
  60. | Csha256
  61. | Csha512
  62. | Cchecksignature
  63. | Chashkey
  64. | Cbefore
  65. | Citerated
  66. | Ctoiterate
  67. | Cempty
  68. | Cisempty
  69. | Csingleton
  70. | Csubsetof
  71. | Cunion
  72. | Cinter
  73. | Cdiff
Sourcetype 'node struct_poly = {
  1. node : 'node;
  2. type_ : ptyp option;
  3. label : Ident.ident option;
  4. loc : Location.t;
}
Sourcetype 'id qualid_gen = 'id qualid_node struct_poly
Sourceand 'id qualid_node =
  1. | Qident of 'id
  2. | Qdot of 'id qualid_gen * 'id
Sourcetype qualid = lident qualid_gen
Sourcetype 'id sexpr_gen = 'id sexpr_node struct_poly
Sourceand 'id sexpr_node =
  1. | Sref of 'id
  2. | Sor of 'id sexpr_gen * 'id sexpr_gen
  3. | Sany
Sourcetype sexpr = lident sexpr_gen
Sourceand 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
Sourcetype bval = bval_gen
Sourcetype quantifier =
  1. | Forall
  2. | Exists
Sourcetype 'id pattern_gen = 'id pattern_node struct_poly
Sourceand 'id pattern_node =
  1. | Mwild
  2. | Mconst of 'id
Sourcetype pattern = lident pattern_gen
Sourcetype 'id call_kind =
  1. | Cid of 'id
  2. | Cconst of const
Sourcetype var_temporality =
  1. | VTbefore
  2. | VTat of Ident.ident
  3. | VTnone
Sourcetype vset =
  1. | Vadded
  2. | Vremoved
  3. | Vunmoved
  4. | Vnone
Sourcetype '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
Sourceand '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
Sourceand 'id term_poly = 'id term_node struct_poly
Sourceand 'id term_gen = 'id term_poly
Sourcetype pterm = lident term_gen
Sourcetype pterm_arg = lident term_arg
Sourcetype 'id instruction_poly = {
  1. node : 'id instruction_node;
  2. label : string option;
  3. loc : Location.t;
}
Sourceand '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
Sourceand '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 * '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
Sourceand 'id for_ident =
  1. | FIsimple of 'id
  2. | FIdouble of 'id * 'id
Sourceand 'id instruction_gen = 'id instruction_poly
Sourceand instruction = lident instruction_poly
Sourceand 'id lvalue_gen = [
  1. | `Var of 'id
  2. | `Field of 'id * 'id term_gen * 'id
]
Sourcetype 'id decl_gen = {
  1. name : 'id;
  2. typ : ptyp option;
  3. default : 'id term_gen option;
  4. shadow : bool;
  5. loc : Location.t;
}
Sourcetype 'id label_term = {
  1. label : 'id option;
  2. term : 'id term_gen;
  3. error : 'id term_gen option;
  4. loc : Location.t;
}
Sourcetype 'id variable = {
  1. decl : 'id decl_gen;
  2. constant : bool;
  3. invs : 'id label_term list;
  4. loc : Location.t;
}
Sourcetype 'id predicate = {
  1. name : 'id;
  2. args : ('id * type_) list;
  3. body : 'id term_gen;
  4. loc : Location.t;
}
Sourcetype 'id definition = {
  1. name : 'id;
  2. typ : type_;
  3. var : 'id;
  4. body : 'id term_gen;
  5. loc : Location.t;
}
Sourcetype 'id invariant = {
  1. label : 'id;
  2. formulas : 'id term_gen list;
}
Sourcetype 'id postcondition = {
  1. name : 'id;
  2. formula : 'id term_gen;
  3. invariants : 'id invariant list;
  4. uses : 'id list;
}
Sourcetype 'id assert_ = {
  1. name : 'id;
  2. label : 'id;
  3. formula : 'id term_gen;
  4. invariants : 'id invariant list;
  5. uses : 'id list;
}
Sourceval pp_assert_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id assert_ -> Ppx_deriving_runtime.unit
Sourceval show_assert_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id assert_ -> Ppx_deriving_runtime.string
Sourcetype '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;
}
Sourcetype entry_description =
  1. | ADAny
  2. | ADOp of string * lident
Sourceval pp_entry_description : Ppx_deriving_runtime.Format.formatter -> entry_description -> Ppx_deriving_runtime.unit
Sourceval show_entry_description : entry_description -> Ppx_deriving_runtime.string
Sourcetype security_role = lident
Sourcetype security_entry =
  1. | Sany
  2. | Sentry of lident list
Sourceval pp_security_entry : Ppx_deriving_runtime.Format.formatter -> security_entry -> Ppx_deriving_runtime.unit
Sourceval show_security_entry : security_entry -> Ppx_deriving_runtime.string
Sourcetype 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
Sourcetype security_predicate = {
  1. s_node : security_node;
  2. loc : Location.t;
}
Sourceval show_security_predicate : security_predicate -> Ppx_deriving_runtime.string
Sourcetype security_item = {
  1. label : lident;
  2. predicate : security_predicate;
  3. loc : Location.t;
}
Sourcetype security = {
  1. items : security_item list;
  2. loc : Location.t;
}
Sourcetype '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;
}
Sourcetype function_ = lident function_struct
Sourceval pp_function_ : Ppx_deriving_runtime.Format.formatter -> function_ -> Ppx_deriving_runtime.unit
Sourceval show_function_ : function_ -> Ppx_deriving_runtime.string
Sourcetype 'id rexpr_gen = 'id rexpr_node struct_poly
Sourceand 'id rexpr_node =
  1. | Rany
  2. | Rexpr of 'id term_gen
  3. | Ror of 'id rexpr_gen * 'id rexpr_gen
Sourcetype rexpr = lident rexpr_gen
Sourcetype '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;
}
Sourcetype '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;
}
Sourcetype transaction = lident transaction_struct
Sourcetype 'id enum_item_struct = {
  1. name : 'id;
  2. initial : bool;
  3. invariants : 'id label_term list;
  4. loc : Location.t;
}
Sourcetype 'id enum_kind =
  1. | EKenum of 'id
  2. | EKstate
Sourcetype 'id enum_struct = {
  1. kind : 'id enum_kind;
  2. items : 'id enum_item_struct list;
  3. loc : Location.t;
}
Sourcetype '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;
}
Sourcetype 'id record_struct = {
  1. name : 'id;
  2. fields : 'id decl_gen list;
  3. loc : Location.t;
}
Sourcetype '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
Sourceval pp_decl_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id decl_ -> Ppx_deriving_runtime.unit
Sourceval show_decl_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id decl_ -> Ppx_deriving_runtime.string
Sourcetype 'id fun_ =
  1. | Ffunction of 'id function_struct
  2. | Ftransaction of 'id transaction_struct
Sourceval pp_fun_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id fun_ -> Ppx_deriving_runtime.unit
Sourceval show_fun_ : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id fun_ -> Ppx_deriving_runtime.string
Sourcetype '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;
}
Sourceval vtunit : ptyp
Sourceval vtbool : ptyp
Sourceval vtnat : ptyp
Sourceval vtint : ptyp
Sourceval vtrational : ptyp
Sourceval vtdate : ptyp
Sourceval vtduration : ptyp
Sourceval vtstring : ptyp
Sourceval vtaddress : ptyp
Sourceval vtrole : ptyp
Sourceval vtcurrency : ptyp
Sourceval vtsignature : ptyp
Sourceval vtkey : ptyp
Sourceval vtkeyhash : ptyp
Sourceval vtbytes : ptyp
Sourceval vtchainid : ptyp
Sourceval mk_sp : ?label:Ident.ident -> ?loc:Location.t -> ?type_:ptyp -> 'a -> 'a struct_poly
Sourceval mk_instr : ?label:string -> ?loc:Location.t -> 'a instruction_node -> 'a instruction_poly
Sourceval mk_label_term : ?label:'a -> ?error:'a term_gen -> ?loc:Location.t -> 'a term_gen -> 'a label_term
Sourceval mk_variable : ?constant:bool -> ?invs:'a label_term list -> ?loc:Location.t -> 'a decl_gen -> 'a variable
Sourceval mk_predicate : ?args:('a * type_) list -> ?loc:Location.t -> 'a -> 'a term_gen -> 'a predicate
Sourceval mk_definition : ?loc:Location.t -> 'a -> type_ -> 'a -> 'a term_gen -> 'a definition
Sourceval mk_invariant : ?formulas:'a term_gen list -> 'a -> 'a invariant
Sourceval mk_postcondition : ?invariants:'a invariant list -> ?uses:'a list -> 'a -> 'a term_gen -> 'a postcondition
Sourceval mk_assert : ?invariants:'a invariant list -> ?uses:'a list -> 'a -> 'a -> 'a term_gen -> 'a assert_
Sourceval mk_specification : ?predicates:'a predicate list -> ?definitions:'a definition list -> ?lemmas:'a label_term list -> ?theorems:'a label_term list -> ?variables:'a variable list -> ?invariants:('a * 'a label_term list) list -> ?effect:'a instruction_gen -> ?specs:'a postcondition list -> ?asserts:'a assert_ list -> ?loc:Location.t -> unit -> 'a specification
Sourceval mk_function_struct : ?args:'a decl_gen list -> ?specification:'a specification -> ?loc:Location.t -> 'a -> 'a instruction_gen -> ptyp -> 'a function_struct
Sourceval mk_transition : ?on:('a * ptyp * 'a * ptyp) -> ?trs:('a * 'a term_gen option * 'a instruction_gen option) list -> 'a sexpr_gen -> 'a transition
Sourceval mk_transaction_struct : ?args:'a decl_gen list -> ?calledby:'a rexpr_gen -> ?accept_transfer:bool -> ?require:'a label_term list -> ?failif:'a label_term list -> ?transition:'a transition -> ?specification:'a specification -> ?functions:'a function_struct list -> ?effect:'a instruction_gen -> ?loc:Location.t -> 'a -> 'a transaction_struct
Sourceval mk_enum_item : ?initial:bool -> ?invariants:'id label_term list -> ?loc:Location.t -> 'id -> 'id enum_item_struct
Sourceval mk_enum : ?items:'a enum_item_struct list -> ?loc:Location.t -> 'a enum_kind -> 'a enum_struct
Sourceval mk_decl : ?typ:ptyp -> ?default:'a term_gen -> ?shadow:bool -> ?loc:Location.t -> 'a -> 'a decl_gen
Sourceval mk_asset : ?fields:'a decl_gen list -> ?keys:'a list -> ?sort:'a list -> ?big_map:bool -> ?state:'a -> ?init:'a term_gen list list -> ?specs:'a label_term list -> ?loc:Location.t -> 'a -> 'a asset_struct
Sourceval mk_model : ?decls:'a decl_ list -> ?funs:'a fun_ list -> ?specifications:'a specification list -> ?securities:security list -> ?loc:Location.t -> 'a -> 'a ast_struct
Sourceval mk_id : ptyp -> lident -> qualid
Sourcemodule Utils : sig ... end