package archetype

  1. Overview
  2. Docs
module L = Location
module PT = ParseTree
module M = Ast
module Type : sig ... end
type opsig = {
  1. osl_sig : M.ptyp list;
  2. osl_ret : M.ptyp;
}
type error_desc =
  1. | AlienPattern
  2. | AnonymousFieldInEffect
  3. | AssertInGlobalSpec
  4. | AssetExpected of M.ptyp
  5. | AssetWithoutFields
  6. | BeforeIrrelevant of [ `Local | `State ]
  7. | BeforeOrLabelInExpr
  8. | BindingInExpr
  9. | CannotAssignArgument of Ident.ident
  10. | CannotAssignLoopIndex of Ident.ident
  11. | CannotCaptureLocal
  12. | CannotInfer
  13. | CannotInferAnonRecord
  14. | CannotInferCollectionType
  15. | CannotInitShadowField
  16. | CannotUpdatePKey
  17. | CollectionExpected
  18. | ContainerOfNonAsset
  19. | ContractInvariantInLocalSpec
  20. | DivergentExpr
  21. | DoesNotSupportMethodCall
  22. | DuplicatedArgName of Ident.ident
  23. | DuplicatedContractEntryName of Ident.ident
  24. | DuplicatedCtorName of Ident.ident
  25. | DuplicatedFieldInAssetDecl of Ident.ident
  26. | DuplicatedFieldInRecordLiteral of Ident.ident
  27. | DuplicatedInitMarkForCtor
  28. | DuplicatedPKey
  29. | DuplicatedVarDecl of Ident.ident
  30. | EffectInGlobalSpec
  31. | EmptyEnumDecl
  32. | ExpressionExpected
  33. | ForeignState of Ident.ident option * Ident.ident option
  34. | FormulaExpected
  35. | IncompatibleTypes of M.ptyp * M.ptyp
  36. | InvalidArcheTypeDecl
  37. | InvalidAssetCollectionExpr of M.ptyp
  38. | InvalidAssetExpression
  39. | InvalidCallByExpression
  40. | InvalidContractExpression
  41. | InvalidEffectForCtn of M.container * M.container list
  42. | InvalidEntryDescription
  43. | InvalidEntryExpression
  44. | InvalidExpression
  45. | InvalidExpressionForEffect
  46. | InvalidFieldsCountInRecordLiteral
  47. | InvalidFormula
  48. | InvalidInstruction
  49. | InvalidLValue
  50. | InvalidMethodInExec
  51. | InvalidMethodInFormula
  52. | InvalidNumberOfArguments of int * int
  53. | InvalidRoleExpression
  54. | InvalidSecurityEntry
  55. | InvalidSecurityRole
  56. | InvalidShadowFieldAccess
  57. | InvalidShadowVariableAccess
  58. | InvalidSortingExpression
  59. | InvalidStateExpression
  60. | InvalidTypeForPk
  61. | InvalidTypeForVarWithFromTo
  62. | InvalidVarOrArgType
  63. | LabelInNonInvariant
  64. | LetInElseInInstruction
  65. | LetInElseOnNonOption
  66. | MethodCallInPredicate
  67. | MissingFieldInRecordLiteral of Ident.ident
  68. | MissingInitValueForShadowField
  69. | MixedAnonInRecordLiteral
  70. | MixedFieldNamesInRecordLiteral of Ident.ident list
  71. | MoreThanOneInitState of Ident.ident list
  72. | MultipleAssetStateDeclaration
  73. | MultipleFromToInVarDecl
  74. | MultipleInitialMarker
  75. | MultipleMatchingFunction of Ident.ident * M.ptyp list * (M.ptyp list * M.ptyp) list
  76. | MultipleMatchingOperator of PT.operator * M.ptyp list * opsig list
  77. | MultipleStateDeclaration
  78. | NameIsAlreadyBound of Ident.ident * Location.t option
  79. | NoLetInInstruction
  80. | NoMatchingFunction of Ident.ident * M.ptyp list
  81. | NoMatchingOperator of PT.operator * M.ptyp list
  82. | NonCodeLabel of Ident.ident
  83. | NonIterable
  84. | NonLoopLabel of Ident.ident
  85. | NoSuchMethod of Ident.ident
  86. | NoSuchSecurityPredicate of Ident.ident
  87. | NotAKeyOfType
  88. | NotAnAssetType
  89. | NotAnEnumType
  90. | NotAPrimitiveType
  91. | NotARole of Ident.ident
  92. | NumericExpressionExpected
  93. | NumericOrCurrencyExpressionExpected
  94. | OpInRecordLiteral
  95. | OrphanedLabel of Ident.ident
  96. | PackUnpackOnNonPrimitive
  97. | PartialMatch of Ident.ident list
  98. | PostConditionInGlobalSpec
  99. | PredicateCallInExpr
  100. | ReadOnlyGlobal of Ident.ident
  101. | SecurityInExpr
  102. | ShadowPKey
  103. | ShadowSKey
  104. | SpecOperatorInExpr
  105. | TransferWithoutDest
  106. | UninitializedVar
  107. | UnknownAsset of Ident.ident
  108. | UnknownContractEntryPoint of Ident.ident * Ident.ident
  109. | UnknownEntry of Ident.ident
  110. | UnknownEnum of Ident.ident
  111. | UnknownField of Ident.ident * Ident.ident
  112. | UnknownFieldName of Ident.ident
  113. | UnknownLabel of Ident.ident
  114. | UnknownLocalOrVariable of Ident.ident
  115. | UnknownProcedure of Ident.ident
  116. | UnknownState of Ident.ident
  117. | UnknownTypeName of Ident.ident
  118. | UnpureInFormula
  119. | UpdateEffectOnPkey
  120. | UpdateEffectWithoutDefault
  121. | UselessPattern
  122. | UsePkeyOfInsteadOfAsset
  123. | VoidMethodInExpr
  124. | VSetInExpr
  125. | VSetOnNonAsset
val show_error_desc : error_desc -> Ppx_deriving_runtime.string
type error = L.t * error_desc
val pp_operator : Core.Format.formatter -> PT.operator -> unit
type argtype = [
  1. | `Type of M.type_
  2. | `Effect of Ident.ident
]
val cmptypes : M.vtyp list
val grptypes : M.vtyp list
val rgtypes : M.vtyp list
val cmpsigs : (PT.operator * (M.vtyp list * M.vtyp)) list
val opsigs : (PT.operator * opsig) list
type acttx = [
  1. | `Entry of PT.entry_decl
  2. | `Transition of PT.transition_decl
]
type groups = {
  1. gr_archetypes : (PT.lident * PT.exts) Location.loced list;
  2. gr_states : PT.enum_decl Location.loced list;
  3. gr_enums : (PT.lident * PT.enum_decl) Location.loced list;
  4. gr_assets : PT.asset_decl Location.loced list;
  5. gr_vars : PT.variable_decl Location.loced list;
  6. gr_funs : PT.s_function Location.loced list;
  7. gr_acttxs : acttx Location.loced list;
  8. gr_specs : PT.specification Location.loced list;
  9. gr_secs : PT.security Location.loced list;
  10. gr_externals : PT.contract_decl Location.loced list;
}
val globals : (string * M.const * M.ptyp) list
val statename : string
type ('args, 'rty) gmethod_ = {
  1. mth_name : M.const;
  2. mth_place : [ `Both | `OnlyFormula | `OnlyExec ];
  3. mth_purity : [ `Pure | `Effect of M.container list ];
  4. mth_totality : [ `Total | `Partial ];
  5. mth_sig : 'args * 'rty option;
}
type mthstyp = [
  1. | `T of M.ptyp
]
type mthtyp = [
  1. | mthstyp
  2. | `The
  3. | `Pk
  4. | `ThePkForAggregate
  5. | `Asset
  6. | `SubColl
  7. | `Cmp
  8. | `Pred of bool
  9. | `RExpr of bool
  10. | `Ef of bool
  11. | `Ref of int
]
and mthatyp = [
  1. | `Fixed of mthtyp list
  2. | `Multi of mthtyp
]
type smethod_ = (mthstyp list, mthstyp) gmethod_
type method_ = (mthatyp, mthtyp) gmethod_
val methods : method_ Ident.Mid.t
val coreops : (string * M.const * [> `Total ] * 'a option * M.ptyp list * M.ptyp) list
val optionops : (string * M.const * [> `Partial | `Total ] * M.ptyp option * 'a list * M.ptyp) list
val listops : (string * M.const * [> `Partial | `Total ] * M.ptyp option * M.ptyp list * M.ptyp) list
val cryptoops : (string * M.const * [> `Total ] * 'a option * M.ptyp list * M.ptyp) list
val packops : (string * M.const * [> `Total ] * 'a option * M.ptyp list * M.ptyp) list
val allops : (string * M.const * [> `Partial | `Total ] * M.ptyp option * M.ptyp list * M.ptyp) list
type assetdecl = {
  1. as_name : M.lident;
  2. as_fields : fielddecl list;
  3. as_pk : M.lident;
  4. as_sortk : M.lident list;
  5. as_invs : (M.lident option * M.pterm) list;
  6. as_state : M.lident option;
  7. as_init : M.pterm list list;
}
and fielddecl = {
  1. fd_name : M.lident;
  2. fd_type : M.ptyp;
  3. fd_dfl : M.pterm option;
  4. fd_ghost : bool;
}
val show_assetdecl : assetdecl -> Ppx_deriving_runtime.string
val show_fielddecl : fielddecl -> Ppx_deriving_runtime.string
val get_field : Ident.ident -> assetdecl -> fielddecl option
type vardecl = {
  1. vr_name : M.lident;
  2. vr_type : M.ptyp;
  3. vr_kind : [ `Constant | `Variable | `Ghost | `Enum ];
  4. vr_invs : M.lident M.label_term list;
  5. vr_def : (M.pterm * [ `Inline | `Std ]) option;
  6. vr_tgt : M.lident option * M.lident option;
  7. vr_core : M.const option;
}
type 'env ispecification = [
  1. | `Predicate of M.lident * (M.lident * M.ptyp) list * M.pterm
  2. | `Definition of M.lident * (M.lident * M.ptyp) * M.pterm
  3. | `Variable of M.lident * M.pterm option
  4. | `Asset of M.lident * M.pterm * (M.lident * M.pterm list) list * M.lident list
  5. | `Effect of 'env * M.instruction
  6. | `Postcondition of M.lident * M.pterm * (M.lident * M.pterm list) list * M.lident list
]
type 'env fundecl = {
  1. fs_name : M.lident;
  2. fs_args : (M.lident * M.ptyp) list;
  3. fs_retty : M.ptyp;
  4. fs_body : M.instruction;
  5. fs_spec : 'env ispecification list option;
}
type preddecl = {
  1. pr_name : M.lident;
  2. pr_args : (M.lident * M.ptyp) list;
  3. pr_body : M.pterm;
}
type txeffect = {
  1. tx_state : M.lident;
  2. tx_when : M.pterm option;
  3. tx_effect : M.instruction option;
}
type 'env tentrydecl = {
  1. ad_name : M.lident;
  2. ad_args : (M.lident * M.ptyp) list;
  3. ad_callby : M.pterm option Location.loced list;
  4. ad_effect : [ `Raw of M.instruction | `Tx of transition ] option;
  5. ad_funs : 'env fundecl option list;
  6. ad_reqs : (M.lident option * M.pterm) list;
  7. ad_fais : (M.lident option * M.pterm) list;
  8. ad_spec : 'env ispecification list;
  9. ad_actfs : bool;
}
and transition = M.sexpr * (M.lident * assetdecl) option * txeffect list
type statedecl = {
  1. sd_name : M.lident;
  2. sd_state : bool;
  3. sd_ctors : ctordecl list;
  4. sd_init : Ident.ident;
}
and ctordecl = M.lident * (M.lident option * M.pterm) list
type contractdecl = {
  1. ct_name : M.lident;
  2. ct_entries : (M.lident * (M.lident * M.ptyp) list) list;
}
type definitiondecl = {
  1. df_name : M.lident;
  2. df_arg : M.lident * M.ptyp;
  3. df_asset : M.lident;
  4. df_body : M.pterm;
}
val pterm_arg_as_pterm : 'a M.term_arg -> 'a M.term_gen option
val core_types : (string * M.ptyp) list
module Env : sig ... end
type env = Env.t
val coreloc : Location.t
val empty : env
val check_and_emit_name_free : env -> M.lident -> bool
val select_operator : Env.t -> ?asset:bool -> L.t -> (PT.operator * M.ptyp list) -> opsig option
val valid_var_or_arg_type : M.ptyp -> bool
val for_container : env -> PT.container -> M.container
val for_assignment_operator : PT.assignment_operator -> M.assignment_operator
val tt_logical_operator : PT.logical_operator -> M.logical_operator
exception InvalidType
val for_type_exn : ?pkey:Ident.ident list -> env -> PT.type_t -> M.ptyp
val for_type : ?pkey:Ident.ident list -> env -> PT.type_t -> M.ptyp option
val for_asset_type : env -> PT.type_t -> M.lident option
val for_asset_keyof_type : env -> PT.type_t -> M.lident option
val for_literal : env -> PT.literal Location.loced -> M.bval
type imode_t = [
  1. | `Ghost
  2. | `Concrete
]
type ekind = [
  1. | `Expr of imode_t
  2. | `Formula of bool
]
type emode_t = {
  1. em_kind : ekind;
  2. em_pred : bool;
}
val is_expr_kind : ekind -> bool
val is_form_kind : ekind -> bool
val expr_mode : imode_t -> emode_t
val form_mode : bool -> emode_t
val for_xexpr : emode_t -> ?autoview:bool -> ?capture:[ `No | `Yes of (Location.t * M.ptyp) Ident.Mid.t ref option ] -> env -> ?ety:M.ptyp -> PT.expr -> PT.lident M.term_node M.struct_poly
val cast_expr : ?autoview:bool -> env -> M.ptyp option -> PT.lident M.term_node M.struct_poly -> PT.lident M.term_node M.struct_poly
val join_expr : ?autoview:bool -> env -> M.ptyp option -> PT.lident M.term_node M.struct_poly list -> M.ptyp option * PT.lident M.term_gen list
val for_gen_matchwith : emode_t -> env -> Location.t -> PT.expr -> PT.branch list -> (statedecl * Tools.Mstr.key Location.loced M.term_gen * (int option * int option Tools.Mstr.t) * PT.expr list) option
val for_asset_expr : emode_t -> env -> PT.expr -> PT.lident M.term_node M.struct_poly * assetdecl option
val for_asset_collection_expr : emode_t -> env -> [ `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly ] -> PT.lident M.term_gen * (assetdecl * M.container) option
val for_contract_expr : emode_t -> env -> PT.expr -> PT.lident M.term_node M.struct_poly * contractdecl option
val for_api_call : emode_t -> env -> Location.t -> ([< `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly Typed ] * PT.lident * PT.expr list) -> (M.pterm * smethod_ * M.lident M.term_arg list) option
val for_gen_method_call : emode_t -> env -> Location.t -> ([ `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly ] * PT.lident * PT.expr list) -> (M.pterm * (assetdecl * M.container) * method_ * M.lident M.term_arg list * M.type_ Tools.Mint.t) option
val for_arg_effect : emode_t -> env -> update:bool -> assetdecl -> PT.expr -> (PT.lident * M.operator * PT.lident M.term_gen) list option
val for_assign_expr : ?autoview:bool -> ?asset:bool -> emode_t -> env -> Location.t -> (M.assignment_operator * M.ptyp * M.ptyp) -> PT.expr -> PT.lident M.term_gen
val for_formula : ?invariant:bool -> env -> PT.expr -> M.pterm
val for_entry_description : env -> PT.security_arg -> M.entry_description
val for_security_entry : env -> PT.security_arg -> M.security_entry
val for_security_role : env -> PT.security_arg -> M.security_role list
val for_role : env -> PT.lident -> M.security_role option
val for_expr : imode_t -> ?autoview:bool -> env -> ?ety:M.type_ -> PT.expr -> M.pterm
val for_lbl_expr : ?ety:M.type_ -> imode_t -> env -> PT.label_expr -> env * (M.lident option * M.pterm)
val for_lbls_expr : imode_t -> ?ety:M.type_ -> env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
val for_lbl_bexpr : imode_t -> env -> PT.label_expr -> env * (M.lident option * M.pterm)
val for_lbls_bexpr : imode_t -> env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
val for_lbl_formula : env -> PT.label_expr -> env * (M.lident option * M.pterm)
val for_xlbls_formula : env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
val for_lbls_formula : env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
val for_arg_decl : ?can_asset:bool -> env -> PT.lident_typ -> env * (PT.lident * M.ptyp) option
val for_args_decl : ?can_asset:bool -> env -> PT.args -> env * (PT.lident * M.ptyp) option list
val for_lvalue : imode_t -> env -> PT.expr -> (M.lvalue * M.ptyp) option
val for_instruction_r : imode_t -> env -> PT.expr -> env * M.instruction
val for_instruction : imode_t -> env -> PT.expr -> env * M.instruction
val for_effect : imode_t -> env -> PT.expr -> Env.t * (env * M.instruction)
type spmode = [
  1. | `Global
  2. | `Local
]
val for_specification_item : spmode -> (env * env) -> PT.specification_item -> (env * env) * env ispecification list
val for_specification : spmode -> (env * env) -> PT.specification -> env * env ispecification list
module SecurityPred : sig ... end
val for_security_item : env -> PT.security_item -> (env * M.security_item) option
val for_security : env -> PT.security -> env * M.security
val for_named_state : ?enum:Ident.ident -> env -> PT.lident -> Ident.ident Location.loced
val for_state_formula : ?enum:Ident.ident -> env -> PT.expr -> M.sexpr
val for_function : env -> PT.s_function Location.loced -> Env.t * env fundecl option
val for_callby : env -> PT.expr -> M.pterm option Location.loced list
val for_entry_properties : (env * env) -> PT.entry_properties -> env * (M.pterm option Location.loced list option * (M.lident option * M.pterm) list option * (M.lident option * M.pterm) list option * env ispecification list option * env fundecl option list)
val for_transition : ?enum:Ident.ident -> env -> (PT.lident * (PT.expr * 'a) option * (PT.expr * 'b) option) -> env * txeffect
type enum_core = (PT.lident * PT.enum_option list) list
val for_core_enum_decl : env -> enum_core Location.loced -> env * (Ident.ident * (PT.lident * PT.label_expr list) list) option
val for_enum_decl : env -> (PT.lident * PT.enum_decl) Location.loced -> env * (statedecl option * PT.label_expr list list option)
val for_enums_decl : env -> (PT.lident * PT.enum_decl) Location.loced list -> env * (statedecl option * PT.label_expr list list option) list
val for_var_decl : env -> PT.variable_decl Location.loced -> env * (vardecl option * PT.label_exprs option)
val for_vars_decl : env -> PT.variable_decl Location.loced list -> env * (vardecl option * PT.label_exprs option) list
val for_fun_decl : env -> PT.s_function Location.loced -> Env.t * env fundecl option
val for_funs_decl : env -> PT.s_function Location.loced list -> env * env fundecl option list
type pre_assetdecl = {
  1. pas_name : M.lident;
  2. pas_fields : (string * M.ptyp * PT.expr option * bool) Location.loced list;
  3. pas_pk : M.lident;
  4. pas_sortk : M.lident list;
  5. pas_invs : PT.label_exprs list;
  6. pas_state : statedecl option;
  7. pas_init : PT.expr list;
}
val for_asset_decl : Ident.ident list -> env -> (assetdecl * PT.asset_decl Location.loced) -> Env.t * pre_assetdecl option
val for_assets_decl : env -> PT.asset_decl Location.loced list -> env * assetdecl option list
val for_contract_decl : env -> PT.contract_decl Location.loced -> env * contractdecl option
val for_contracts_decl : env -> PT.contract_decl Location.loced list -> env * contractdecl option list
val for_acttx_decl : env -> acttx Location.loced -> Env.t * env tentrydecl option
val for_acttxs_decl : env -> acttx Location.loced list -> env * env tentrydecl option list
val for_specs_decl : env -> PT.specification Location.loced list -> env * env ispecification list list
val for_secs_decl : env -> PT.security Location.loced list -> env * M.security list
val group_declarations : PT.declaration list -> groups
type decls = {
  1. state : statedecl option;
  2. contracts : contractdecl option list;
  3. variables : vardecl option list;
  4. enums : statedecl option list;
  5. assets : assetdecl option list;
  6. functions : env fundecl option list;
  7. acttxs : env tentrydecl option list;
  8. specs : env ispecification list list;
  9. secspecs : M.security list;
}
val for_grouped_declarations : env -> (L.t * groups) -> env * decls
val enums_of_statedecl : statedecl list -> M.enum list
val assets_of_adecls : assetdecl option list -> M.lident M.asset_struct list
val variables_of_vdecls : vardecl option list -> M.lident M.variable list
val contracts_of_cdecls : contractdecl option list -> M.lident M.contract_struct list
val specifications_of_ispecifications : env ispecification list -> M.lident M.specification
val functions_of_fdecls : env fundecl option list -> M.lident M.function_struct list
val transentrys_of_tdecls : env tentrydecl option list -> M.lident M.transaction_struct list
val for_declarations : env -> PT.declaration list Location.loced -> M.model
val typing : env -> PT.archetype -> M.model
OCaml

Innovation. Community. Security.