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
  3. | Utz
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
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 Core.date
  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 var_temporality =
  1. | VTbefore
  2. | VTat of Ident.ident
  3. | VTnone
val pp_var_temporality : Ppx_deriving_runtime.Format.formatter -> var_temporality -> Ppx_deriving_runtime.unit
val show_var_temporality : var_temporality -> 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 * 'id term_gen option
  13. | Pdeclvar of 'id * ptyp option * 'id term_gen
  14. | Pvar of var_temporality * '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
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
  4. | ASorting of bool * 'id
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. 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. | 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 * 'id lvalue_gen * 'id term_gen
  9. | Irequire of bool * 'id term_gen
  10. | Itransfer of 'id term_gen * 'id term_gen
  11. | Ibreak
  12. | Iassert of 'id term_gen
  13. | Icall of 'id term_gen option * 'id call_kind * 'id term_arg list
  14. | Ireturn of 'id term_gen
  15. | Ilabel of '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 term_gen * 'id
]
and lvalue = lident lvalue_gen
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
val pp_lvalue_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id lvalue_gen -> Ppx_deriving_runtime.unit
val show_lvalue_gen : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id lvalue_gen -> Ppx_deriving_runtime.string
val pp_lvalue : Ppx_deriving_runtime.Format.formatter -> lvalue -> Ppx_deriving_runtime.unit
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;
}
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. invs : 'id label_term list;
  6. 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;
  4. uses : 'id 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;
  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;
}
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. 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. init : 'id term_gen option;
  7. specs : 'id label_term list;
  8. 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_struct = {
  1. name : 'id;
  2. signatures : 'id signature list;
  3. init : 'id term_gen option;
  4. loc : Location.t;
}
and contract = lident contract_struct
val pp_contract_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'id contract_struct -> Ppx_deriving_runtime.unit
val show_contract_struct : 'id. (Ppx_deriving_runtime.Format.formatter -> 'id -> Ppx_deriving_runtime.unit) -> 'id contract_struct -> Ppx_deriving_runtime.string
val pp_contract : Ppx_deriving_runtime.Format.formatter -> contract -> Ppx_deriving_runtime.unit
val show_contract : 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_struct 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 -> '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 -> ?invs:'a label_term list -> ?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 -> ?uses:'a list -> 'a -> 'a term_gen -> 'a postcondition
val mk_assert : ?invariants:'a invariant list -> ?uses:'a 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 instruction_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 -> ?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 -> ?shadow:bool -> ?loc:Location.t -> 'a -> 'a decl_gen
val mk_asset : ?fields:'a decl_gen list -> ?key:'a -> ?sort:'a list -> ?state:'a -> ?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_struct
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_struct 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_arg : ('id term_gen -> 'id term_gen -> 'id term_gen) -> 'id term_gen -> 'id term_arg -> 'id term_gen
val fold_term : ('id term_gen -> 'id term_gen -> 'id term_gen) -> 'id term_gen -> 'id term_gen -> 'id term_gen
val fold_instr : ('a -> 'b instruction_gen -> 'a) -> 'a -> 'b instruction_poly -> 'a
val fold_instr_expr : ('a instruction_gen as 'a term_gen -> 'a -> 'a term_gen) -> ('a term_gen -> 'a term_gen -> 'a term_gen) -> 'a term_gen -> 'a instruction_poly -> 'a term_gen
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.