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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct