package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Archetype.TypingSource

Sourcemodule L = Location
Sourcemodule PT = ParseTree
Sourcemodule M = Ast
Sourcemodule Type : sig ... end
Sourcetype opsig = {
  1. osl_sig : M.ptyp list;
  2. osl_ret : M.ptyp;
}
Sourcetype error_desc =
  1. | AlienPattern
  2. | AssetExpected of M.ptyp
  3. | AssetWithoutFields
  4. | BeforeOrLabelInExpr
  5. | BeforeIrrelevant of [ `Local | `State ]
  6. | BeforeWithLabel
  7. | BindingInExpr
  8. | CannotInferAnonRecord
  9. | CannotInferCollectionType
  10. | CollectionExpected
  11. | DivergentExpr
  12. | DuplicatedContractEntryName of Ident.ident
  13. | DuplicatedCtorName of Ident.ident
  14. | DuplicatedFieldInAssetDecl of Ident.ident
  15. | DuplicatedFieldInRecordLiteral of Ident.ident
  16. | DuplicatedInitMarkForCtor
  17. | DuplicatedPKey
  18. | DuplicatedVarDecl of Ident.ident
  19. | AnonymousFieldInEffect
  20. | EmptyEnumDecl
  21. | ExpressionExpected
  22. | ForeignState of Ident.ident option * Ident.ident option
  23. | FormulaExpected
  24. | IncompatibleTypes of M.ptyp * M.ptyp
  25. | InvalidActionDescription
  26. | InvalidActionExpression
  27. | InvalidArcheTypeDecl
  28. | InvalidAssetCollectionExpr of M.ptyp
  29. | InvalidAssetExpression
  30. | InvalidCallByExpression
  31. | InvalidExpressionForEffect
  32. | InvalidExpression
  33. | InvalidFieldsCountInRecordLiteral
  34. | InvalidLValue
  35. | InvalidFormula
  36. | InvalidInstruction
  37. | InvalidNumberOfArguments of int * int
  38. | InvalidRoleExpression
  39. | InvalidSecurityAction
  40. | InvalidSecurityRole
  41. | InvalidSortingExpression
  42. | InvalidStateExpression
  43. | InvalidTypeForVarWithFromTo
  44. | LetInElseInInstruction
  45. | LetInElseOnNonOption
  46. | MissingFieldInRecordLiteral of Ident.ident
  47. | MixedAnonInRecordLiteral
  48. | MixedFieldNamesInRecordLiteral of Ident.ident list
  49. | MoreThanOneInitState of Ident.ident list
  50. | MultipleAssetStateDeclaration
  51. | MultipleInitialMarker
  52. | MultipleMatchingOperator of PT.operator * M.ptyp list * opsig list
  53. | MultipleFromToInVarDecl
  54. | MultipleStateDeclaration
  55. | NameIsAlreadyBound of Ident.ident * Location.t option
  56. | NoMatchingOperator of PT.operator * M.ptyp list
  57. | NoSuchMethod of Ident.ident
  58. | NoSuchSecurityPredicate of Ident.ident
  59. | NonCodeLabel of Ident.ident
  60. | NonLoopLabel of Ident.ident
  61. | NotAKeyOfType
  62. | NotAnAssetType
  63. | NotAnEnumType
  64. | NotAPrimitiveType
  65. | NotARole of Ident.ident
  66. | NumericExpressionExpected
  67. | OpInRecordLiteral
  68. | OrphanedLabel of Ident.ident
  69. | PartialMatch of Ident.ident list
  70. | ReadOnlyGlobal of Ident.ident
  71. | SecurityInExpr
  72. | SpecOperatorInExpr
  73. | TransferWithoutDest
  74. | UninitializedVar
  75. | UnknownAction of Ident.ident
  76. | UnknownAsset of Ident.ident
  77. | UnknowContractEntryPoint of Ident.ident * Ident.ident
  78. | UnknownEnum of Ident.ident
  79. | UnknownField of Ident.ident * Ident.ident
  80. | UnknownFieldName of Ident.ident
  81. | UnknownLabel of Ident.ident
  82. | UnknownLocalOrVariable of Ident.ident
  83. | UnknownProcedure of Ident.ident
  84. | UnknownState of Ident.ident
  85. | UnknownTypeName of Ident.ident
  86. | UnpureInFormula
  87. | UselessPattern
  88. | VoidMethodInExpr
  89. | AssetPartitionnedby of Ident.ident * Ident.ident list
Sourcetype error = L.t * error_desc
Sourceval pp_operator : Core.Format.formatter -> PT.operator -> unit
Sourcetype argtype = [
  1. | `Type of M.type_
  2. | `Effect of Ident.ident
]
Sourceval eqtypes : M.vtyp list
Sourceval cmptypes : M.vtyp list
Sourceval grptypes : M.vtyp list
Sourceval rgtypes : M.vtyp list
Sourceval cmpsigs : (PT.operator * (M.vtyp list * M.vtyp)) list
Sourceval opsigs : (PT.operator * opsig) list
Sourcetype acttx = [
  1. | `Action of PT.action_decl
  2. | `Transition of PT.transition_decl
]
Sourcetype 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;
}
Sourceval globals : (string * M.const * M.ptyp) list
Sourceval statename : string
Sourcetype method_ = {
  1. mth_name : M.const;
  2. mth_purity : [ `Pure | `Effect ];
  3. mth_totality : [ `Total | `Partial ];
  4. mth_sig : mthtyp list * mthtyp option;
}
Sourceand mthtyp = [
  1. | `T of M.ptyp
  2. | `The
  3. | `Pk
  4. | `Effect
  5. | `Asset
  6. | `SubColl
  7. | `Cmp
  8. | `Pred
  9. | `RExpr
  10. | `Ref of int
]
Sourcetype 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;
}
Sourceand fielddecl = {
  1. fd_name : M.lident;
  2. fd_type : M.ptyp;
  3. fd_dfl : M.pterm option;
  4. fd_ghost : bool;
}
Sourceval get_field : Ident.ident -> assetdecl -> fielddecl option
Sourcetype 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;
}
Sourcetype 'env ispecification = [
  1. | `Predicate of M.lident * (M.lident * M.ptyp) list * M.pterm
  2. | `Definition of M.lident * (M.lident * M.ptyp) option * M.pterm
  3. | `Lemma of M.lident * M.pterm
  4. | `Theorem of M.lident * M.pterm
  5. | `Variable of M.lident * M.pterm option
  6. | `Assert of M.lident * M.pterm * (M.lident * M.pterm list) list * M.lident list
  7. | `Effect of 'env * M.instruction
  8. | `Postcondition of M.lident * M.pterm * (M.lident * M.pterm list) list * M.lident list
]
Sourcetype '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;
}
Sourcetype txeffect = {
  1. tx_state : M.lident;
  2. tx_when : M.pterm option;
  3. tx_effect : M.instruction option;
}
Sourcetype 'env tactiondecl = {
  1. ad_name : M.lident;
  2. ad_args : (M.lident * M.ptyp) list;
  3. ad_callby : M.lident list;
  4. ad_effect : [ `Raw of M.instruction | `Tx of M.lident * txeffect list ] 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;
}
Sourcetype statedecl = {
  1. sd_name : M.lident;
  2. sd_state : bool;
  3. sd_ctors : ctordecl list;
  4. sd_init : Ident.ident;
}
Sourceand ctordecl = M.lident * (M.lident option * M.pterm) list
Sourcetype contractdecl = {
  1. ct_name : M.lident;
  2. ct_entries : (M.lident * M.ptyp list) list;
}
Sourceval pterm_arg_as_pterm : 'a M.term_arg -> 'a M.term_gen option
Sourceval core_types : (string * M.ptyp) list
Sourcemodule Env : sig ... end
Sourcetype env = Env.t
Sourceval coreloc : Location.t
Sourceval empty : env
Sourceval check_and_emit_name_free : env -> M.lident -> bool
Sourceval select_operator : Env.t -> L.t -> (PT.operator * M.ptyp list) -> opsig option
Sourceval for_container : env -> PT.container -> M.container
Sourceval for_assignment_operator : PT.assignment_operator -> M.assignment_operator
Sourceval tt_logical_operator : PT.logical_operator -> M.logical_operator
Sourceexception InvalidType
Sourceval for_type_exn : env -> PT.type_t -> M.ptyp
Sourceval for_type : env -> PT.type_t -> M.ptyp option
Sourceval for_asset_type : env -> PT.type_t -> M.lident option
Sourceval for_asset_keyof_type : env -> PT.type_t -> M.lident option
Sourceval for_literal : env -> PT.literal Location.loced -> M.bval
Sourcetype emode_t = [
  1. | `Expr
  2. | `Formula
]
Sourceval 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
Sourceval for_asset_expr : emode_t -> env -> PT.expr -> PT.lident M.term_node M.struct_poly * assetdecl option
Sourceval for_asset_collection_expr : emode_t -> env -> [< `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly Parsed ] -> PT.lident M.term_gen * (assetdecl * M.container) option
Sourceval for_gen_method_call : emode_t -> env -> Location.t -> ([< `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly Parsed ] * PT.lident * PT.expr list) -> (PT.lident M.term_gen * assetdecl * method_ * PT.lident M.term_arg list * M.ptyp Tools.Mint.t) option
Sourceval for_arg_effect : emode_t -> env -> assetdecl -> PT.expr -> (PT.lident * M.operator * PT.lident M.term_gen) list option
Sourceval for_formula : env -> PT.expr -> M.pterm
Sourceval for_action_description : env -> PT.security_arg -> M.action_description
Sourceval for_security_action : env -> PT.security_arg -> M.security_action
Sourceval for_security_role : env -> PT.security_arg -> M.security_role list
Sourceval for_role : env -> PT.lident -> M.security_role option
Sourceval for_expr : env -> ?ety:M.type_ -> PT.expr -> M.pterm
Sourceval for_lbl_expr : env -> ?ety:M.type_ -> PT.label_expr -> env * (M.lident option * M.pterm)
Sourceval for_lbls_expr : env -> ?ety:M.type_ -> PT.label_exprs -> env * (M.lident option * M.pterm) list
Sourceval for_lbl_bexpr : env -> PT.label_expr -> env * (M.lident option * M.pterm)
Sourceval for_lbls_bexpr : env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
Sourceval for_lbl_formula : env -> PT.label_expr -> env * (M.lident option * M.pterm)
Sourceval for_xlbls_formula : env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
Sourceval for_lbls_formula : env -> PT.label_exprs -> env * (M.lident option * M.pterm) list
Sourceval for_arg_decl : env -> PT.lident_typ -> env * (PT.lident * M.ptyp) option
Sourceval for_args_decl : env -> PT.args -> env * (PT.lident * M.ptyp) option list
Sourceval for_lvalue : env -> PT.expr -> (M.lvalue * M.ptyp) option
Sourceval for_instruction : env -> PT.expr -> env * M.instruction
Sourceval for_effect : env -> PT.expr -> Env.t * (env * M.instruction)
Sourceval for_specification_item : (env * env) -> PT.specification_item -> (env * env) * env ispecification
Sourceval for_specification : (env * env) -> PT.specification -> env * env ispecification list
Sourcemodule SecurityPred : sig ... end
Sourceval for_security_item : env -> PT.security_item -> (env * M.security_item) option
Sourceval for_security : env -> PT.security -> env * M.security
Sourceval for_named_state : ?enum:Ident.ident -> env -> PT.lident -> Ident.ident Location.loced
Sourceval for_state : ?enum:Ident.ident -> env -> PT.expr -> M.lident
Sourceval for_function : env -> PT.s_function Location.loced -> Env.t * env fundecl option
Sourceval for_callby : env -> PT.expr -> PT.lident list
Sourceval for_action_properties : (env * env) -> PT.action_properties -> env * (PT.lident list option * (M.lident option * M.pterm) list option * (M.lident option * M.pterm) list option * env ispecification list option * env fundecl option list)
Sourceval for_transition : ?enum:Ident.ident -> env -> (PT.lident * (PT.expr * 'a) option * (PT.expr * 'b) option) -> env * txeffect
Sourcetype enum_core = (PT.lident * PT.enum_option list) list
Sourceval for_core_enum_decl : env -> enum_core Location.loced -> env * (Ident.ident * (PT.lident * (M.lident option * M.pterm) list) list) option
Sourceval for_enum_decl : env -> (PT.lident * PT.enum_decl) Location.loced -> env * statedecl option
Sourceval for_enums_decl : env -> (PT.lident * PT.enum_decl) Location.loced list -> env * statedecl option list
Sourceval for_var_decl : env -> PT.variable_decl Location.loced -> env * vardecl option
Sourceval for_vars_decl : env -> PT.variable_decl Location.loced list -> env * vardecl option list
Sourceval for_fun_decl : env -> PT.s_function Location.loced -> Env.t * env fundecl option
Sourceval for_funs_decl : env -> PT.s_function Location.loced list -> env * env fundecl option list
Sourceval for_asset_decl : ?force:bool -> env -> PT.asset_decl Location.loced -> env * assetdecl option
Sourceval for_assets_decl : env -> PT.asset_decl Location.loced list -> env * assetdecl option list
Sourceval for_contract_decl : env -> PT.contract_decl Location.loced -> env * contractdecl option
Sourceval for_contracts_decl : env -> PT.contract_decl Location.loced list -> env * contractdecl option list
Sourceval for_acttx_decl : env -> acttx Location.loced -> Env.t * env tactiondecl
Sourceval for_acttxs_decl : env -> acttx Location.loced list -> env * env tactiondecl list
Sourceval for_specs_decl : env -> PT.specification Location.loced list -> env * env ispecification list list
Sourceval for_secs_decl : env -> PT.security Location.loced list -> env * M.security list
Sourceval group_declarations : PT.declaration list -> groups
Sourcetype 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 tactiondecl list;
  8. specs : env ispecification list list;
  9. secspecs : M.security list;
}
Sourceval for_grouped_declarations : env -> (L.t * groups) -> env * decls
Sourceval enums_of_statedecl : statedecl list -> M.enum list
Sourceval assets_of_adecls : assetdecl option list -> M.lident M.asset_struct list
Sourceval variables_of_vdecls : vardecl option list -> M.lident M.variable list
Sourceval contracts_of_cdecls : contractdecl option list -> M.lident M.contract_struct list
Sourceval specifications_of_ispecifications : env ispecification list -> M.lident M.specification
Sourceval functions_of_fdecls : env fundecl option list -> M.lident M.function_struct list
Sourceval transactions_of_tdecls : env tactiondecl list -> M.lident M.transaction_struct list
Sourceval for_declarations : env -> PT.declaration list Location.loced -> M.model
Sourceval typing : env -> PT.archetype -> M.model