package archetype

  1. Overview
  2. Docs
val lident_to_yojson : lident -> Yojson.Safe.t
val pp_lident : Format.formatter -> string Location.loced -> unit
type container =
  1. | Collection
  2. | Partition
val container_to_yojson : container -> Yojson.Safe.t
val show_container : container -> Ppx_deriving_runtime.string
type type_r =
  1. | Tref of lident
  2. | Tasset of lident
  3. | Tcontainer of type_t * container
  4. | Ttuple of type_t list
  5. | Toption of type_t
and type_t = type_r Location.loced
val type_r_to_yojson : type_r -> Yojson.Safe.t
val type_t_to_yojson : type_t -> Yojson.Safe.t
val show_type_r : type_r -> Ppx_deriving_runtime.string
val show_type_t : type_t -> Ppx_deriving_runtime.string
type logical_operator =
  1. | And
  2. | Or
  3. | Imply
  4. | Equiv
val logical_operator_to_yojson : logical_operator -> Yojson.Safe.t
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 comparison_operator_to_yojson : comparison_operator -> Yojson.Safe.t
val show_comparison_operator : comparison_operator -> Ppx_deriving_runtime.string
type arithmetic_operator =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | Div
  5. | Modulo
val arithmetic_operator_to_yojson : arithmetic_operator -> Yojson.Safe.t
val show_arithmetic_operator : arithmetic_operator -> Ppx_deriving_runtime.string
type unary_operator =
  1. | Uplus
  2. | Uminus
  3. | Not
val unary_operator_to_yojson : unary_operator -> Yojson.Safe.t
val show_unary_operator : unary_operator -> Ppx_deriving_runtime.string
type assignment_operator =
  1. | ValueAssign
  2. | PlusAssign
  3. | MinusAssign
  4. | MultAssign
  5. | DivAssign
  6. | AndAssign
  7. | OrAssign
val assignment_operator_to_yojson : assignment_operator -> Yojson.Safe.t
val show_assignment_operator : assignment_operator -> Ppx_deriving_runtime.string
type quantifier =
  1. | Forall
  2. | Exists
val quantifier_to_yojson : quantifier -> Yojson.Safe.t
val show_quantifier : quantifier -> 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_operator
]
val operator_to_yojson : operator -> Yojson.Safe.t
val show_operator : operator -> Ppx_deriving_runtime.string
type qualid =
  1. | Qident of lident
  2. | Qdot of qualid * lident
val qualid_to_yojson : qualid -> Yojson.Safe.t
val show_qualid : qualid -> Ppx_deriving_runtime.string
type pattern_unloc =
  1. | Pwild
  2. | Pref of lident
val pattern_unloc_to_yojson : pattern_unloc -> Yojson.Safe.t
val show_pattern_unloc : pattern_unloc -> Ppx_deriving_runtime.string
val pattern_to_yojson : pattern -> Yojson.Safe.t
val show_pattern : pattern -> Ppx_deriving_runtime.string
type expr_unloc =
  1. | Eterm of lident option * lident option * lident
  2. | Eliteral of literal
  3. | Earray of expr list
  4. | Erecord of record_item list
  5. | Etuple of expr list
  6. | Edot of expr * lident
  7. | Emulticomp of expr * (comparison_operator Location.loced * expr) list
  8. | Eapp of function_ * expr list
  9. | Emethod of expr * lident * expr list
  10. | Etransfer of expr * bool * lident option
  11. | Erequire of expr
  12. | Efailif of expr
  13. | Eassign of assignment_operator * expr * expr
  14. | Eif of expr * expr * expr option
  15. | Ebreak
  16. | Efor of lident option * lident * expr * expr
  17. | Eiter of lident option * lident * expr option * expr * expr
  18. | Eseq of expr * expr
  19. | Eletin of lident * type_t option * expr * expr * expr option
  20. | Ematchwith of expr * (pattern list * expr) list
  21. | Equantifier of quantifier * lident * quantifier_kind * expr
  22. | Eassert of lident
  23. | Ereturn of expr
  24. | Eoption of option_
  25. | Einvalid
and scope = [
  1. | `Added
  2. | `After
  3. | `Before
  4. | `Fixed
  5. | `Removed
  6. | `Stable
]
and quantifier_kind =
  1. | Qcollection of expr
  2. | Qtype of type_t
and option_ =
  1. | OSome of expr
  2. | ONone
and function_ =
  1. | Fident of lident
  2. | Foperator of operator Location.loced
and literal =
  1. | Lnumber of Core.big_int
  2. | Lrational of Core.big_int * Core.big_int
  3. | Ltz of Core.big_int
  4. | Lmtz of Core.big_int
  5. | Laddress of string
  6. | Lstring of string
  7. | Lbool of bool
  8. | Lduration of string
  9. | Ldate of string
and record_item = (assignment_operator * lident) option * expr
and lident_typ = lident * type_t * extension list option
and label_expr = (lident * expr) Location.loced
and label_exprs = label_expr list
and extension_unloc =
  1. | Eextension of lident * expr option
    (*

    extension

    *)
and exts = extension list option
val expr_unloc_to_yojson : expr_unloc -> Yojson.Safe.t
val scope_to_yojson : scope -> Yojson.Safe.t
val quantifier_kind_to_yojson : quantifier_kind -> Yojson.Safe.t
val option__to_yojson : option_ -> Yojson.Safe.t
val option__of_yojson : Yojson.Safe.t -> option_ Ppx_deriving_yojson_runtime.error_or
val function__to_yojson : function_ -> Yojson.Safe.t
val function__of_yojson : Yojson.Safe.t -> function_ Ppx_deriving_yojson_runtime.error_or
val literal_to_yojson : literal -> Yojson.Safe.t
val record_item_to_yojson : record_item -> Yojson.Safe.t
val expr_to_yojson : expr -> Yojson.Safe.t
val lident_typ_to_yojson : lident_typ -> Yojson.Safe.t
val label_expr_to_yojson : label_expr -> Yojson.Safe.t
val label_exprs_to_yojson : label_exprs -> Yojson.Safe.t
val extension_unloc_to_yojson : extension_unloc -> Yojson.Safe.t
val extension_to_yojson : extension -> Yojson.Safe.t
val exts_to_yojson : exts -> Yojson.Safe.t
val show_expr_unloc : expr_unloc -> Ppx_deriving_runtime.string
val show_quantifier_kind : quantifier_kind -> Ppx_deriving_runtime.string
val pp_option_ : Ppx_deriving_runtime.Format.formatter -> option_ -> Ppx_deriving_runtime.unit
val show_option_ : option_ -> Ppx_deriving_runtime.string
val pp_function_ : Ppx_deriving_runtime.Format.formatter -> function_ -> Ppx_deriving_runtime.unit
val show_function_ : function_ -> Ppx_deriving_runtime.string
val show_literal : literal -> Ppx_deriving_runtime.string
val show_record_item : record_item -> Ppx_deriving_runtime.string
val show_lident_typ : lident_typ -> Ppx_deriving_runtime.string
val show_label_expr : label_expr -> Ppx_deriving_runtime.string
val show_label_exprs : label_exprs -> Ppx_deriving_runtime.string
val show_extension_unloc : extension_unloc -> Ppx_deriving_runtime.string
val show_extension : extension -> Ppx_deriving_runtime.string
type field_unloc =
  1. | Ffield of lident * type_t * expr option * exts
    (*

    field

    *)
val field_unloc_to_yojson : field_unloc -> Yojson.Safe.t
val field_to_yojson : field -> Yojson.Safe.t
val show_field_unloc : field_unloc -> Ppx_deriving_runtime.string
type args = lident_typ list
val args_to_yojson : args -> Yojson.Safe.t
type invariants = (lident * expr list) list
val invariants_to_yojson : invariants -> Yojson.Safe.t
val show_invariants : invariants -> Ppx_deriving_runtime.string
type specification_item_unloc =
  1. | Vpredicate of lident * args * expr
  2. | Vdefinition of lident * type_t * lident * expr
  3. | Vlemma of lident * expr
  4. | Vtheorem of lident * expr
  5. | Vvariable of lident * type_t * expr option
  6. | Veffect of expr
  7. | Vassert of lident * expr * invariants
  8. | Vpostcondition of lident * expr * invariants
val specification_item_unloc_to_yojson : specification_item_unloc -> Yojson.Safe.t
val show_specification_item_unloc : specification_item_unloc -> Ppx_deriving_runtime.string
type specification_item = specification_item_unloc Location.loced
val specification_item_to_yojson : specification_item -> Yojson.Safe.t
val show_specification_item : specification_item -> Ppx_deriving_runtime.string
type specification_unloc = specification_item list * exts
val specification_unloc_to_yojson : specification_unloc -> Yojson.Safe.t
val show_specification_unloc : specification_unloc -> Ppx_deriving_runtime.string
type specification = specification_unloc Location.loced
val specification_to_yojson : specification -> Yojson.Safe.t
val show_specification : specification -> Ppx_deriving_runtime.string
type security_arg_unloc =
  1. | Sident of lident
  2. | Sdot of lident * lident
  3. | Slist of security_arg list
  4. | Sapp of lident * security_arg list
  5. | Sbut of lident * security_arg
  6. | Sto of lident * security_arg
val security_arg_unloc_to_yojson : security_arg_unloc -> Yojson.Safe.t
val security_arg_to_yojson : security_arg -> Yojson.Safe.t
val show_security_arg_unloc : security_arg_unloc -> Ppx_deriving_runtime.string
val show_security_arg : security_arg -> Ppx_deriving_runtime.string
type security_item_unloc = lident * lident * security_arg list
val security_item_unloc_to_yojson : security_item_unloc -> Yojson.Safe.t
val show_security_item_unloc : security_item_unloc -> Ppx_deriving_runtime.string
type security_item = security_item_unloc Location.loced
val security_item_to_yojson : security_item -> Yojson.Safe.t
val show_security_item : security_item -> Ppx_deriving_runtime.string
type security_unloc = security_item list * exts
val security_unloc_to_yojson : security_unloc -> Yojson.Safe.t
val security_to_yojson : security -> Yojson.Safe.t
val show_security_unloc : security_unloc -> Ppx_deriving_runtime.string
val show_security : security -> Ppx_deriving_runtime.string
type s_function = {
  1. name : lident;
  2. args : args;
  3. ret_t : type_t option;
  4. spec : specification option;
  5. body : expr;
}
val s_function_to_yojson : s_function -> Yojson.Safe.t
val show_s_function : s_function -> Ppx_deriving_runtime.string
type action_properties = {
  1. accept_transfer : bool;
  2. calledby : (expr * exts) option;
  3. require : (label_exprs * exts) option;
  4. failif : (label_exprs * exts) option;
  5. spec : specification option;
  6. functions : s_function Location.loced list;
}
val action_properties_to_yojson : action_properties -> Yojson.Safe.t
val show_action_properties : action_properties -> Ppx_deriving_runtime.string
type transition = (lident * (expr * exts) option * (expr * exts) option) list
val transition_to_yojson : transition -> Yojson.Safe.t
val show_transition : transition -> Ppx_deriving_runtime.string
type variable_kind =
  1. | VKvariable
  2. | VKconstant
val variable_kind_to_yojson : variable_kind -> Yojson.Safe.t
val show_variable_kind : variable_kind -> Ppx_deriving_runtime.string
type enum_kind =
  1. | EKenum of lident
  2. | EKstate
val enum_kind_to_yojson : enum_kind -> Yojson.Safe.t
val show_enum_kind : enum_kind -> Ppx_deriving_runtime.string
type declaration_unloc =
  1. | Darchetype of lident * exts
  2. | Dvariable of variable_decl
  3. | Dinstance of instance_decl
  4. | Denum of enum_kind * enum_decl
  5. | Dasset of asset_decl
  6. | Daction of action_decl
  7. | Dtransition of transition_decl
  8. | Dcontract of contract_decl
  9. | Dextension of extension_decl
  10. | Dnamespace of namespace_decl
  11. | Dfunction of s_function
  12. | Dspecification of specification
  13. | Dsecurity of security
  14. | Dinvalid
and variable_decl = lident * type_t * expr option * value_option list option * variable_kind * exts
and instance_decl = lident * lident * expr * exts
and enum_decl = (lident * enum_option list) list * exts
and asset_decl = lident * field list * asset_option list * asset_post_option list * asset_operation option * exts
and action_decl = lident * args * action_properties * (expr * exts) option * exts
and transition_decl = lident * args * (lident * lident) option * expr * action_properties * transition * exts
and contract_decl = lident * signature list * exts
and extension_decl = lident * expr option
and namespace_decl = lident * declaration list
and value_option =
  1. | VOfrom of lident
  2. | VOto of lident
and asset_option =
  1. | AOidentifiedby of lident
  2. | AOsortedby of lident
and asset_post_option =
  1. | APOstates of lident
  2. | APOconstraints of label_exprs
  3. | APOinit of expr
and enum_option =
  1. | EOinitial
  2. | EOspecification of label_exprs
and signature =
  1. | Ssignature of lident * type_t list
and asset_operation_enum =
  1. | AOadd
  2. | AOremove
  3. | AOupdate
and asset_operation =
  1. | AssetOperation of asset_operation_enum list * expr option
val declaration_unloc_to_yojson : declaration_unloc -> Yojson.Safe.t
val variable_decl_to_yojson : variable_decl -> Yojson.Safe.t
val instance_decl_to_yojson : instance_decl -> Yojson.Safe.t
val enum_decl_to_yojson : enum_decl -> Yojson.Safe.t
val asset_decl_to_yojson : asset_decl -> Yojson.Safe.t
val action_decl_to_yojson : action_decl -> Yojson.Safe.t
val transition_decl_to_yojson : transition_decl -> Yojson.Safe.t
val contract_decl_to_yojson : contract_decl -> Yojson.Safe.t
val extension_decl_to_yojson : extension_decl -> Yojson.Safe.t
val namespace_decl_to_yojson : namespace_decl -> Yojson.Safe.t
val value_option_to_yojson : value_option -> Yojson.Safe.t
val asset_option_to_yojson : asset_option -> Yojson.Safe.t
val asset_post_option_to_yojson : asset_post_option -> Yojson.Safe.t
val asset_post_option_of_yojson : Yojson.Safe.t -> asset_post_option Ppx_deriving_yojson_runtime.error_or
val enum_option_to_yojson : enum_option -> Yojson.Safe.t
val signature_to_yojson : signature -> Yojson.Safe.t
val declaration_to_yojson : declaration -> Yojson.Safe.t
val asset_operation_enum_to_yojson : asset_operation_enum -> Yojson.Safe.t
val asset_operation_to_yojson : asset_operation -> Yojson.Safe.t
val show_declaration_unloc : declaration_unloc -> Ppx_deriving_runtime.string
val show_variable_decl : variable_decl -> Ppx_deriving_runtime.string
val show_instance_decl : instance_decl -> Ppx_deriving_runtime.string
val show_enum_decl : enum_decl -> Ppx_deriving_runtime.string
val show_asset_decl : asset_decl -> Ppx_deriving_runtime.string
val show_action_decl : action_decl -> Ppx_deriving_runtime.string
val show_transition_decl : transition_decl -> Ppx_deriving_runtime.string
val show_contract_decl : contract_decl -> Ppx_deriving_runtime.string
val show_extension_decl : extension_decl -> Ppx_deriving_runtime.string
val show_namespace_decl : namespace_decl -> Ppx_deriving_runtime.string
val show_value_option : value_option -> Ppx_deriving_runtime.string
val show_asset_option : asset_option -> Ppx_deriving_runtime.string
val pp_asset_post_option : Ppx_deriving_runtime.Format.formatter -> asset_post_option -> Ppx_deriving_runtime.unit
val show_asset_post_option : asset_post_option -> Ppx_deriving_runtime.string
val show_enum_option : enum_option -> Ppx_deriving_runtime.string
val show_signature : signature -> Ppx_deriving_runtime.string
val show_declaration : declaration -> Ppx_deriving_runtime.string
val show_asset_operation_enum : asset_operation_enum -> Ppx_deriving_runtime.string
val show_asset_operation : asset_operation -> Ppx_deriving_runtime.string
type archetype_unloc =
  1. | Marchetype of declaration list
  2. | Mextension of lident * declaration list * declaration list
val archetype_unloc_to_yojson : archetype_unloc -> Yojson.Safe.t
val archetype_to_yojson : archetype -> Yojson.Safe.t
val _ : Yojson.Safe.t -> archetype Ppx_deriving_yojson_runtime.error_or
val show_archetype_unloc : archetype_unloc -> Ppx_deriving_runtime.string
val show_archetype : archetype -> Ppx_deriving_runtime.string
val mk_archetype : ?decls:declaration list -> ?loc:Location.t -> unit -> archetype_unloc Location.loced