package archetype

  1. Overview
  2. Docs
module L = Location
module PT = ParseTree
module M = Ast
module Type : sig ... end
type error_desc =
  1. | AssetExpected
  2. | AssetWithoutFields
  3. | BindingInExpr
  4. | CannotInferAnonRecord
  5. | CannotInferCollectionType
  6. | CollectionExpected
  7. | DivergentExpr
  8. | DuplicatedAssetName of Ident.ident
  9. | DuplicatedCtorName of Ident.ident
  10. | DuplicatedFieldInAssetDecl of Ident.ident
  11. | DuplicatedFieldInRecordLiteral of Ident.ident
  12. | DuplicatedInitMarkForCtor
  13. | DuplicatedPKey
  14. | DuplicatedVarDecl of Ident.ident
  15. | AnonymousFieldInEffect
  16. | EmptyStateDecl
  17. | ExpressionExpected
  18. | FormulaExpected
  19. | IncompatibleTypes of M.ptyp * M.ptyp
  20. | InvalidActionDescription
  21. | InvalidActionExpression
  22. | InvalidArcheTypeDecl
  23. | InvalidAssetCollectionExpr
  24. | InvalidAssetExpression
  25. | InvalidCallByExpression
  26. | InvalidExpressionForEffect
  27. | InvalidExpression
  28. | InvalidFieldsCountInRecordLiteral
  29. | InvalidLValue
  30. | InvalidFormula
  31. | InvalidInstruction
  32. | InvalidNumberOfArguments of int * int
  33. | InvalidRoleExpression
  34. | InvalidSecurityAction
  35. | InvalidSecurityRole
  36. | InvalidStateExpression
  37. | LetInElseInInstruction
  38. | MissingFieldInRecordLiteral of Ident.ident
  39. | MixedAnonInRecordLiteral
  40. | MixedFieldNamesInRecordLiteral of Ident.ident list
  41. | MoreThanOneInitState of Ident.ident list
  42. | MultipleInitialMarker
  43. | MultipleMatchingOperator
  44. | MultipleStateDeclaration
  45. | NameIsAlreadyBound of Ident.ident
  46. | NoMatchingOperator
  47. | NoSuchMethod of Ident.ident
  48. | NoSuchSecurityPredicate of Ident.ident
  49. | NonLoopLabel of Ident.ident
  50. | NotARole of Ident.ident
  51. | NumericExpressionExpected
  52. | OpInRecordLiteral
  53. | OrphanedLabel of Ident.ident
  54. | ReadOnlyGlobal of Ident.ident
  55. | SecurityInExpr
  56. | SpecOperatorInExpr
  57. | UnknownAction of Ident.ident
  58. | UnknownAsset of Ident.ident
  59. | UnknownField of Ident.ident * Ident.ident
  60. | UnknownFieldName of Ident.ident
  61. | UnknownLabel of Ident.ident
  62. | UnknownLocalOrVariable of Ident.ident
  63. | UnknownProcedure of Ident.ident
  64. | UnknownState of Ident.ident
  65. | UnknownTypeName of Ident.ident
  66. | UnpureInFormula
  67. | VoidMethodInExpr
  68. | AssetPartitionnedby of Ident.ident * Ident.ident list
val show_error_desc : error_desc -> Ppx_deriving_runtime.string
type error = L.t * error_desc
type argtype = [
  1. | `Type of M.type_
  2. | `Effect of Ident.ident
]
type procsig = {
  1. psl_sig : argtype list;
  2. psl_ret : M.ptyp;
}
type opsig = {
  1. osl_sig : M.ptyp list;
  2. osl_ret : M.ptyp;
}
val eqtypes : M.vtyp list
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 varfun = [
  1. | `Variable of PT.variable_decl
  2. | `Function of PT.s_function
]
type acttx = [
  1. | `Action of PT.action_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_varfuns : varfun Location.loced list;
  6. gr_acttxs : acttx Location.loced list;
  7. gr_specs : PT.specification Location.loced list;
  8. gr_secs : PT.security Location.loced list;
}
val globals : (string * M.const * M.ptyp) list
type method_ = {
  1. mth_name : M.const;
  2. mth_purity : [ `Pure | `Effect ];
  3. mth_totality : [ `Total | `Partial ];
  4. mth_sig : mthtyp list * mthtyp option;
}
and mthtyp = [
  1. | `T of M.ptyp
  2. | `The
  3. | `Pk
  4. | `Effect
  5. | `Asset
  6. | `SubColl
  7. | `Field
  8. | `Pred
  9. | `RExpr
  10. | `Ref of int
]
val methods : method_ Ident.Mid.t
type security_pred_ = {
  1. sp_sig : sptyp list;
}
and sptyp = [
  1. | `ActionDesc
  2. | `Role
  3. | `Action
]
val security_preds : security_pred_ Ident.Mid.t
type assetdecl = {
  1. as_name : M.lident;
  2. as_fields : (M.lident * M.ptyp) list;
  3. as_pk : M.lident;
  4. as_sortk : M.lident list;
  5. as_invs : (M.lident option * M.pterm) list;
}
type vardecl = {
  1. vr_name : M.lident;
  2. vr_type : M.ptyp;
  3. vr_kind : [ `Constant | `Variable | `Ghost ];
  4. vr_def : (M.pterm * [ `Inline | `Std ]) option;
  5. 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) 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
]
type 'env actiondecl = {
  1. ad_name : M.lident;
  2. ad_args : (M.lident * M.ptyp) list;
  3. ad_callby : M.lident list;
  4. ad_effect : M.instruction option;
  5. ad_reqs : (M.lident option * M.pterm) list;
  6. ad_fais : (M.lident option * M.pterm) list;
  7. ad_spec : 'env ispecification list;
}
type transitiondecl = {
  1. td_name : M.lident;
}
type statedecl = {
  1. sd_ctors : (M.lident * M.pterm list) list;
  2. sd_init : Ident.ident;
}
val pterm_arg_as_pterm : 'a M.term_arg -> 'a M.term_gen option
val procsig_of_operator : PT.operator -> procsig
val core_types : (string * M.ptyp) list
module Env : sig ... end
type env = Env.t
val empty : env
val check_and_emit_name_free : env -> M.lident -> 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
val get_asset_method : string -> 'a option
exception InvalidType
val for_type_exn : env -> PT.type_t -> M.ptyp
val for_type : env -> PT.type_t -> M.ptyp option
val for_literal : env -> PT.literal Location.loced -> M.bval
type emode_t = [
  1. | `Expr
  2. | `Formula
]
val for_xexpr : emode_t -> env -> ?ety:M.ptyp -> PT.expr -> PT.lident M.term_node M.struct_poly
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 -> PT.expr -> PT.lident M.term_gen * (assetdecl * M.container) option
val for_gen_method_call : emode_t -> env -> Location.t -> (PT.expr * PT.lident * PT.expr list) -> (PT.lident M.term_gen * assetdecl * method_ * PT.lident M.term_arg list * M.ptyp Tools.Mint.t) option
val for_arg_effect : emode_t -> env -> assetdecl -> PT.expr -> (PT.lident * M.operator * PT.lident M.term_gen) list option
val for_formula : env -> PT.expr -> M.pterm
val for_action_description : env -> PT.security_arg -> M.action_description
val for_security_action : env -> PT.security_arg -> M.security_action
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 : env -> ?ety:M.type_ -> PT.expr -> M.pterm
val for_lbl_expr : env -> PT.label_expr -> env * (M.lident option * M.pterm)
val for_lbls_expr : 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.pterm list
val for_arg_decl : env -> PT.lident_typ -> env * (PT.lident * M.ptyp) option
val for_args_decl : env -> PT.args -> env * (PT.lident * M.ptyp) option list
val for_lvalue : env -> PT.expr -> (M.lident * M.ptyp) option
val for_instruction : env -> PT.expr -> env * M.instruction
val for_specification_item : env -> PT.specification_item -> env * env ispecification
val for_security_item : env -> PT.security_item -> (env * M.security_item) option
val for_specification : env -> PT.specification -> env * env ispecification list
val for_security : env -> PT.security -> env * M.security
val for_named_state : env -> PT.lident -> Ident.ident option
val for_state : env -> PT.expr -> Ident.ident option
val for_function : env -> PT.s_function Location.loced -> unit
val for_callby : env -> PT.expr -> PT.lident list
val for_action_properties : env -> PT.action_properties -> env * (PT.lident list option * M.pterm list option * M.pterm list option * (env * env ispecification list) option * unit list)
val for_effect : env -> PT.expr -> env * M.instruction
val for_transition : env -> (PT.lident * (PT.expr * 'a) option * (PT.expr * 'b) option) -> Ident.ident option * M.pterm option * (env * M.instruction) option
type state = (PT.lident * PT.enum_option list) list
val for_state_decl : env -> state Location.loced -> env * (Ident.ident * (PT.lident * M.pterm list) list) option
val for_varfun_decl : env -> varfun Location.loced -> env * [> `Variable of vardecl ] option
val for_varfuns_decl : env -> varfun Location.loced list -> env * [> `Variable of vardecl ] option list
val for_asset_decl : env -> PT.asset_decl Location.loced -> env * assetdecl option
val for_assets_decl : env -> PT.asset_decl Location.loced list -> env * assetdecl option list
val for_acttx_decl : env -> acttx Location.loced -> Env.t * env actiondecl
val for_acttxs_decl : env -> acttx Location.loced list -> env * env actiondecl 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
val for_grouped_declarations : env -> (L.t * groups) -> env * (assetdecl option list * [> `Variable of vardecl ] option list * env actiondecl list * env ispecification list list * M.security list)
val assets_of_adecls : assetdecl option list -> M.lident M.asset_struct list
val variables_of_fdecls : [< `Variable of vardecl ] option list -> M.lident M.variable list
val specifications_of_ispecifications : env ispecification list -> M.lident M.specification
val transactions_of_tdecls : env actiondecl 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.