package archetype

  1. Overview
  2. Docs
val pp_ident : Stdlib.Format.formatter -> string -> unit
val pp_lident : Stdlib.Format.formatter -> string Location.loced -> unit
type container =
  1. | Collection
  2. | Subset
  3. | Partition
val pp_container : Ppx_deriving_runtime.Format.formatter -> container -> Ppx_deriving_runtime.unit
val show_container : container -> Ppx_deriving_runtime.string
type currency =
  1. | Tz
  2. | Mtz
val pp_currency : Ppx_deriving_runtime.Format.formatter -> currency -> Ppx_deriving_runtime.unit
val show_currency : currency -> Ppx_deriving_runtime.string
type vtyp =
  1. | VTbool
  2. | VTint
  3. | VTrational
  4. | VTdate
  5. | VTduration
  6. | VTstring
  7. | VTaddress
  8. | VTrole
  9. | VTcurrency
  10. | VTkey
val pp_vtyp : Ppx_deriving_runtime.Format.formatter -> vtyp -> Ppx_deriving_runtime.unit
type trtyp =
  1. | TRentry
  2. | TRaction
  3. | TRasset
  4. | TRfield
val pp_trtyp : Ppx_deriving_runtime.Format.formatter -> trtyp -> Ppx_deriving_runtime.unit
type ptyp =
  1. | Tasset of lident
  2. | Tenum of lident
  3. | Tcontract of lident
  4. | Tbuiltin of vtyp
  5. | Tcontainer of ptyp * container
  6. | Ttuple of ptyp list
  7. | Toption of ptyp
  8. | Tentry
  9. | Ttrace of trtyp
val pp_ptyp : Ppx_deriving_runtime.Format.formatter -> ptyp -> Ppx_deriving_runtime.unit
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 pp_logical_operator : Ppx_deriving_runtime.Format.formatter -> logical_operator -> Ppx_deriving_runtime.unit
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 pp_comparison_operator : Ppx_deriving_runtime.Format.formatter -> comparison_operator -> Ppx_deriving_runtime.unit
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 pp_assignment_operator : Ppx_deriving_runtime.Format.formatter -> assignment_operator -> Ppx_deriving_runtime.unit
val show_assignment_operator : assignment_operator -> Ppx_deriving_runtime.string
type arithmetic_operator =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | Div
  5. | Modulo
val pp_arithmetic_operator : Ppx_deriving_runtime.Format.formatter -> arithmetic_operator -> Ppx_deriving_runtime.unit
val show_arithmetic_operator : arithmetic_operator -> Ppx_deriving_runtime.string
type unary_arithmetic_operator =
  1. | Uplus
  2. | Uminus
val pp_unary_arithmetic_operator : Ppx_deriving_runtime.Format.formatter -> unary_arithmetic_operator -> Ppx_deriving_runtime.unit
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 pp_operator : Ppx_deriving_runtime.Format.formatter -> operator -> Ppx_deriving_runtime.unit
val show_operator : operator -> Ppx_deriving_runtime.string
type const =
  1. | Cstate
  2. | Cnow
  3. | Ctransferred
  4. | Ccaller
  5. | Cfail
  6. | Cbalance
  7. | Cconditions
  8. | Cactions
  9. | Cnone
  10. | Cany
  11. | Canyaction
  12. | Cisempty
  13. | Cget
  14. | Cadd
  15. | Caddnofail
  16. | Cremove
  17. | Cremovenofail
  18. | Cremoveif
  19. | Cupdate
  20. | Cupdatenofail
  21. | Cclear
  22. | Ccontains
  23. | Cnth
  24. | Creverse
  25. | Cselect
  26. | Csort
  27. | Ccount
  28. | Csum
  29. | Cmax
  30. | Cmin
  31. | Csubsetof
  32. | Chead
  33. | Ctail
  34. | Cbefore
  35. | Cunmoved
  36. | Cadded
  37. | Cremoved
  38. | Citerated
  39. | Ctoiterate
val pp_const : Ppx_deriving_runtime.Format.formatter -> const -> Ppx_deriving_runtime.unit
type 'node struct_poly = {
  1. node : 'node;
  2. type_ : ptyp option;
  3. label : Ident.ident option;
  4. loc : Location.t;
}
val pp_struct_poly : 'node. (Ppx_deriving_runtime.Format.formatter -> 'node -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'node struct_poly -> Ppx_deriving_runtime.unit
val show_struct_poly : 'node. (Ppx_deriving_runtime.Format.formatter -> 'node -> Ppx_deriving_runtime.unit) -> 'node struct_poly -> Ppx_deriving_runtime.string
type 'id qualid_gen = 'id qualid_node struct_poly
and 'id qualid_node =
  1. | Qident of 'id
  2. | Qdot of 'id qualid_gen * 'id
val pp_qualid_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id qualid_gen -> Ppx_deriving_runtime.unit
val show_qualid_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id qualid_gen -> Ppx_deriving_runtime.string
val pp_qualid_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id qualid_node -> Ppx_deriving_runtime.unit
val show_qualid_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id qualid_node -> Ppx_deriving_runtime.string
type qualid = lident qualid_gen
val pp_qualid : Ppx_deriving_runtime.Format.formatter -> qualid -> Ppx_deriving_runtime.unit
val show_qualid : qualid -> Ppx_deriving_runtime.string
type 'id rexpr_gen = 'id rexpr_node struct_poly
and 'id rexpr_node =
  1. | Rany
  2. | Rqualid of 'id qualid_gen
  3. | Ror of 'id rexpr_gen * 'id rexpr_gen
  4. | Raddress of 'id
val pp_rexpr_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id rexpr_gen -> Ppx_deriving_runtime.unit
val show_rexpr_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id rexpr_gen -> Ppx_deriving_runtime.string
val pp_rexpr_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id rexpr_node -> Ppx_deriving_runtime.unit
val show_rexpr_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id rexpr_node -> Ppx_deriving_runtime.string
type rexpr = lident rexpr_gen
val pp_rexpr : Ppx_deriving_runtime.Format.formatter -> rexpr -> Ppx_deriving_runtime.unit
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
val pp_sexpr_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id sexpr_gen -> Ppx_deriving_runtime.unit
val show_sexpr_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id sexpr_gen -> Ppx_deriving_runtime.string
val pp_sexpr_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id sexpr_node -> Ppx_deriving_runtime.unit
val show_sexpr_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id sexpr_node -> Ppx_deriving_runtime.string
type sexpr = lident sexpr_gen
val pp_sexpr : Ppx_deriving_runtime.Format.formatter -> sexpr -> Ppx_deriving_runtime.unit
type bval_gen = bval_node struct_poly
and bval_node =
  1. | BVint of Core.big_int
  2. | BVuint of Core.big_int
  3. | BVbool of bool
  4. | BVenum of string
  5. | BVrational of Core.big_int * Core.big_int
  6. | BVdate of string
  7. | BVstring of string
  8. | BVcurrency of currency * Core.big_int
  9. | BVaddress of string
  10. | BVduration of Core.duration
val pp_bval_gen : Ppx_deriving_runtime.Format.formatter -> bval_gen -> Ppx_deriving_runtime.unit
val show_bval_gen : bval_gen -> Ppx_deriving_runtime.string
val pp_bval_node : Ppx_deriving_runtime.Format.formatter -> bval_node -> Ppx_deriving_runtime.unit
val show_bval_node : bval_node -> Ppx_deriving_runtime.string
type bval = bval_gen
val pp_bval : Ppx_deriving_runtime.Format.formatter -> bval -> Ppx_deriving_runtime.unit
type 'id signature = {
  1. name : 'id;
  2. args : ptyp list;
  3. loc : Location.t;
}
val pp_signature : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id signature -> Ppx_deriving_runtime.unit
val show_signature : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id signature -> Ppx_deriving_runtime.string
type quantifier =
  1. | Forall
  2. | Exists
val pp_quantifier : Ppx_deriving_runtime.Format.formatter -> quantifier -> Ppx_deriving_runtime.unit
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
val pp_pattern_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id pattern_gen -> Ppx_deriving_runtime.unit
val show_pattern_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id pattern_gen -> Ppx_deriving_runtime.string
val pp_pattern_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id pattern_node -> Ppx_deriving_runtime.unit
val show_pattern_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id pattern_node -> Ppx_deriving_runtime.string
type pattern = lident pattern_gen
val pp_pattern : Ppx_deriving_runtime.Format.formatter -> pattern -> Ppx_deriving_runtime.unit
val show_pattern : pattern -> Ppx_deriving_runtime.string
type 'id call_kind =
  1. | Cid of 'id
  2. | Cconst of const
val pp_call_kind : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id call_kind -> Ppx_deriving_runtime.unit
val show_call_kind : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id call_kind -> Ppx_deriving_runtime.string
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
  13. | Pvar of 'id
  14. | Parray of 'id term_gen list
  15. | Plit of bval
  16. | Pdot of 'id term_gen * 'id
  17. | Pconst of const
  18. | Ptuple of 'id term_gen list
and 'id term_arg =
  1. | AExpr of 'id term_gen
  2. | AFun of 'id * ptyp * 'id term_gen
  3. | AEffect of ('id * operator * 'id term_gen) list
and 'id term_poly = 'id term_node struct_poly
and 'id term_gen = 'id term_poly
val pp_term_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id term_node -> Ppx_deriving_runtime.unit
val show_term_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id term_node -> Ppx_deriving_runtime.string
val pp_term_arg : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id term_arg -> Ppx_deriving_runtime.unit
val show_term_arg : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id term_arg -> Ppx_deriving_runtime.string
val pp_term_poly : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id term_poly -> Ppx_deriving_runtime.unit
val show_term_poly : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id term_poly -> Ppx_deriving_runtime.string
val pp_term_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id term_gen -> Ppx_deriving_runtime.unit
val show_term_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id term_gen -> Ppx_deriving_runtime.string
type pterm = lident term_gen
val pp_pterm : Ppx_deriving_runtime.Format.formatter -> pterm -> Ppx_deriving_runtime.unit
type pterm_arg = lident term_arg
val pp_pterm_arg : Ppx_deriving_runtime.Format.formatter -> pterm_arg -> Ppx_deriving_runtime.unit
val show_pterm_arg : pterm_arg -> Ppx_deriving_runtime.string
type 'id instruction_poly = {
  1. node : 'id instruction_node;
  2. label : string option;
  3. subvars : Ident.ident list;
  4. loc : Location.t;
}
and 'id instruction_node =
  1. | Iif of 'id term_gen * 'id instruction_gen * 'id instruction_gen
  2. | Ifor of 'id * '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. | Iseq of 'id instruction_gen list
  6. | Imatchwith of 'id term_gen * ('id pattern_gen * 'id instruction_gen) list
  7. | Iassign of assignment_operator * 'id * 'id term_gen
  8. | Irequire of bool * 'id term_gen
  9. | Itransfer of 'id term_gen * bool * 'id qualid_gen option
  10. | Ibreak
  11. | Iassert of 'id term_gen
  12. | Icall of 'id term_gen option * 'id call_kind * 'id term_arg list
  13. | Ireturn of 'id term_gen
  14. | Ilabel of 'id
and 'id instruction_gen = 'id instruction_poly
and instruction = lident instruction_poly
val pp_instruction_poly : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id instruction_poly -> Ppx_deriving_runtime.unit
val show_instruction_poly : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id instruction_poly -> Ppx_deriving_runtime.string
val pp_instruction_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id instruction_node -> Ppx_deriving_runtime.unit
val show_instruction_node : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id instruction_node -> Ppx_deriving_runtime.string
val pp_instruction_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id instruction_gen -> Ppx_deriving_runtime.unit
val show_instruction_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id instruction_gen -> Ppx_deriving_runtime.string
val pp_instruction : Ppx_deriving_runtime.Format.formatter -> instruction -> Ppx_deriving_runtime.unit
val show_instruction : instruction -> Ppx_deriving_runtime.string
type 'id decl_gen = {
  1. name : 'id;
  2. typ : ptyp option;
  3. default : 'id term_gen option;
  4. loc : Location.t;
}
val pp_decl_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id decl_gen -> Ppx_deriving_runtime.unit
val show_decl_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id decl_gen -> Ppx_deriving_runtime.string
type 'id label_term = {
  1. label : 'id option;
  2. term : 'id term_gen;
  3. loc : Location.t;
}
val pp_label_term : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id label_term -> Ppx_deriving_runtime.unit
val show_label_term : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id label_term -> Ppx_deriving_runtime.string
type 'id variable = {
  1. decl : 'id decl_gen;
  2. constant : bool;
  3. from : 'id qualid_gen option;
  4. to_ : 'id qualid_gen option;
  5. loc : Location.t;
}
val pp_variable : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id variable -> Ppx_deriving_runtime.unit
val show_variable : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id variable -> Ppx_deriving_runtime.string
type 'id predicate = {
  1. name : 'id;
  2. args : ('id * type_) list;
  3. body : 'id term_gen;
  4. loc : Location.t;
}
val pp_predicate : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id predicate -> Ppx_deriving_runtime.unit
val show_predicate : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id predicate -> Ppx_deriving_runtime.string
type 'id definition = {
  1. name : 'id;
  2. typ : type_;
  3. var : 'id;
  4. body : 'id term_gen;
  5. loc : Location.t;
}
val pp_definition : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id definition -> Ppx_deriving_runtime.unit
val show_definition : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id definition -> Ppx_deriving_runtime.string
type 'id invariant = {
  1. label : 'id;
  2. formulas : 'id term_gen list;
}
val pp_invariant : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id invariant -> Ppx_deriving_runtime.unit
val show_invariant : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id invariant -> Ppx_deriving_runtime.string
type 'id postcondition = {
  1. name : 'id;
  2. formula : 'id term_gen;
  3. invariants : 'id invariant list;
}
val pp_postcondition : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id postcondition -> Ppx_deriving_runtime.unit
val show_postcondition : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id postcondition -> Ppx_deriving_runtime.string
type 'id assert_ = {
  1. name : 'id;
  2. label : 'id;
  3. formula : 'id term_gen;
  4. invariants : 'id invariant 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 term_gen option;
  8. specs : 'id postcondition list;
  9. asserts : 'id assert_ list;
  10. loc : Location.t;
}
val pp_specification : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id specification -> Ppx_deriving_runtime.unit
val show_specification : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id specification -> Ppx_deriving_runtime.string
type action_description =
  1. | ADAny
  2. | ADOp of string * lident
val pp_action_description : Ppx_deriving_runtime.Format.formatter -> action_description -> Ppx_deriving_runtime.unit
val show_action_description : action_description -> Ppx_deriving_runtime.string
type security_role = lident
val pp_security_role : Ppx_deriving_runtime.Format.formatter -> security_role -> Ppx_deriving_runtime.unit
val show_security_role : security_role -> Ppx_deriving_runtime.string
type security_action =
  1. | Sany
  2. | Sentry of lident list
val pp_security_action : Ppx_deriving_runtime.Format.formatter -> security_action -> Ppx_deriving_runtime.unit
val show_security_action : security_action -> Ppx_deriving_runtime.string
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 pp_security_node : Ppx_deriving_runtime.Format.formatter -> security_node -> Ppx_deriving_runtime.unit
val show_security_node : security_node -> Ppx_deriving_runtime.string
type security_predicate = {
  1. s_node : security_node;
  2. loc : Location.t;
}
val pp_security_predicate : Ppx_deriving_runtime.Format.formatter -> security_predicate -> Ppx_deriving_runtime.unit
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 pp_security_item : Ppx_deriving_runtime.Format.formatter -> security_item -> Ppx_deriving_runtime.unit
val show_security_item : security_item -> Ppx_deriving_runtime.string
type security = {
  1. items : security_item list;
  2. loc : Location.t;
}
val pp_security : Ppx_deriving_runtime.Format.formatter -> security -> Ppx_deriving_runtime.unit
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. fvs : (Ident.ident * ptyp) list;
  7. loc : Location.t;
}
val pp_function_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id function_struct -> Ppx_deriving_runtime.unit
val show_function_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id function_struct -> Ppx_deriving_runtime.string
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 transition = {
  1. from : 'id sexpr_gen;
  2. on : ('id * 'id) option;
  3. trs : ('id * 'id term_gen option * 'id instruction_gen option) list;
}
val pp_transition : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id transition -> Ppx_deriving_runtime.unit
val show_transition : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id transition -> Ppx_deriving_runtime.string
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;
}
val pp_transaction_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id transaction_struct -> Ppx_deriving_runtime.unit
val show_transaction_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id transaction_struct -> Ppx_deriving_runtime.string
type transaction = lident transaction_struct
val pp_transaction : Ppx_deriving_runtime.Format.formatter -> transaction -> Ppx_deriving_runtime.unit
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;
}
val pp_enum_item_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id enum_item_struct -> Ppx_deriving_runtime.unit
val show_enum_item_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id enum_item_struct -> Ppx_deriving_runtime.string
type 'id enum_kind =
  1. | EKenum of 'id
  2. | EKstate
val pp_enum_kind : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id enum_kind -> Ppx_deriving_runtime.unit
val show_enum_kind : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id enum_kind -> Ppx_deriving_runtime.string
type 'id enum_struct = {
  1. kind : 'id enum_kind;
  2. items : 'id enum_item_struct list;
  3. loc : Location.t;
}
val pp_enum_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id enum_struct -> Ppx_deriving_runtime.unit
val show_enum_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id enum_struct -> Ppx_deriving_runtime.string
type enum = lident enum_struct
val pp_enum : Ppx_deriving_runtime.Format.formatter -> enum -> Ppx_deriving_runtime.unit
type 'id asset_struct = {
  1. name : 'id;
  2. fields : 'id decl_gen list;
  3. key : 'id option;
  4. sort : 'id list;
  5. state : 'id option;
  6. role : bool;
  7. init : 'id term_gen option;
  8. specs : 'id label_term list;
  9. loc : Location.t;
}
val pp_asset_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id asset_struct -> Ppx_deriving_runtime.unit
val show_asset_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id asset_struct -> Ppx_deriving_runtime.string
type asset = lident asset_struct
type 'id contract = {
  1. name : 'id;
  2. signatures : 'id signature list;
  3. init : 'id term_gen option;
  4. loc : Location.t;
}
val pp_contract : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id contract -> Ppx_deriving_runtime.unit
val show_contract : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id contract -> Ppx_deriving_runtime.string
type 'id model_struct = {
  1. name : 'id;
  2. variables : 'id variable list;
  3. assets : 'id asset_struct list;
  4. functions : 'id function_struct list;
  5. transactions : 'id transaction_struct list;
  6. enums : 'id enum_struct list;
  7. contracts : 'id contract list;
  8. specifications : 'id specification list;
  9. securities : security list;
  10. loc : Location.t;
}
and model = lident model_struct
val pp_model_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id model_struct -> Ppx_deriving_runtime.unit
val show_model_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id model_struct -> Ppx_deriving_runtime.string
val pp_model : Ppx_deriving_runtime.Format.formatter -> model -> Ppx_deriving_runtime.unit
val vtbool : 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 vtkey : ptyp
val mk_sp : ?label:Ident.ident -> ?loc:Location.t -> ?type_:ptyp -> 'a -> 'a struct_poly
val mk_instr : ?label:string -> ?loc:Location.t -> ?subvars:Ident.ident list -> 'a instruction_node -> 'a instruction_poly
val mk_label_term : ?label:'a -> ?loc:Location.t -> 'a term_gen -> 'a label_term
val mk_variable : ?constant:bool -> ?from:'a qualid_gen -> ?to_:'a qualid_gen -> ?loc:Location.t -> 'a decl_gen -> 'a variable
val mk_predicate : ?args:('a * type_) list -> ?loc:Location.t -> 'a -> 'a term_gen -> 'a predicate
val mk_definition : ?loc:Location.t -> 'a -> type_ -> 'a -> 'a term_gen -> 'a definition
val mk_invariant : ?formulas:'a term_gen list -> 'a -> 'a invariant
val mk_postcondition : ?invariants:'a invariant list -> 'a -> 'a term_gen -> 'a postcondition
val mk_assert : ?invariants:'a invariant list -> 'a -> 'a -> 'a term_gen -> 'a assert_
val 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 term_gen -> ?specs:'a postcondition list -> ?asserts:'a assert_ list -> ?loc:Location.t -> unit -> 'a specification
val mk_function_struct : ?args:'a decl_gen list -> ?specification:'a specification -> ?fvs:(Ident.ident * ptyp) list -> ?loc:Location.t -> 'a -> 'a instruction_gen -> ptyp -> 'a function_struct
val mk_transition : ?on:('a * 'a) -> ?trs:('a * 'a term_gen option * 'a instruction_gen option) list -> 'a sexpr_gen -> 'a transition
val 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
val mk_enum_item : ?initial:bool -> ?invariants:'id label_term list -> ?loc:Location.t -> 'id -> 'id enum_item_struct
val mk_enum : ?items:'a enum_item_struct list -> ?loc:Location.t -> 'a enum_kind -> 'a enum_struct
val mk_decl : ?typ:ptyp -> ?default:'a term_gen -> ?loc:Location.t -> 'a -> 'a decl_gen
val mk_asset : ?fields:'a decl_gen list -> ?key:'a -> ?sort:'a list -> ?state:'a -> ?role:bool -> ?init:'a term_gen -> ?specs:'a label_term list -> ?loc:Location.t -> 'a -> 'a asset_struct
val mk_contract : ?signatures:'a signature list -> ?init:'a term_gen -> ?loc:Location.t -> 'a -> 'a contract
val mk_model : ?variables:'a variable list -> ?assets:'a asset_struct list -> ?functions:'a function_struct list -> ?transactions:'a transaction_struct list -> ?enums:'a enum_struct list -> ?contracts:'a contract list -> ?specifications:'a specification list -> ?securities:security list -> ?loc:Location.t -> 'a -> 'a model_struct
val mk_id : ptyp -> lident -> qualid
val map_term_node : ('id term_gen -> 'id term_gen) -> 'id term_node -> 'id term_node
val map_instr_node : ('a instruction_gen -> 'a instruction_gen) -> 'a instruction_node -> 'a instruction_node
val map_gen_poly : ('a -> 'id -> 'id) -> 'a -> 'id struct_poly -> 'id struct_poly
val map_gen : ('a -> 'b instruction_node -> 'c instruction_node) -> 'a -> 'b instruction_poly -> 'c instruction_poly
val map_term : ('a term_gen -> 'a term_gen) -> 'a term_node struct_poly -> 'a term_node struct_poly
val map_instr : ('a instruction_gen -> 'a instruction_gen) -> 'a instruction_poly -> 'a instruction_poly
val fold_term : ('a -> 'id term_gen -> 'a) -> 'a -> 'id term_gen -> 'a
val fold_instr : ('a -> 'b instruction_gen -> 'a) -> 'a -> 'b instruction_poly -> 'a
val fold_instr_expr : ('a -> 'b instruction_gen as 'b -> 'a) -> ('a -> 'b term_gen -> 'a) -> 'a -> 'b -> 'a
val fold_map_term : ('id term_node -> 'term) -> ('a -> 'id term_gen -> 'id term_gen * 'a) -> 'a -> 'id term_gen -> 'term * 'a
val fold_map_instr_term : ('id instruction_node -> 'id instruction_gen) -> 'b -> ('a -> 'id instruction_gen -> 'id instruction_gen * 'a) -> ('a -> 'id term_gen -> 'id term_gen * 'a) -> 'a -> 'id instruction_poly -> 'id instruction_gen * 'a
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