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 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
Sourcetype error = L.t * error_desc
Sourcetype argtype = [
  1. | `Type of M.type_
  2. | `Effect of Ident.ident
]
Sourcetype procsig = {
  1. psl_sig : argtype list;
  2. psl_ret : M.ptyp;
}
Sourcetype opsig = {
  1. osl_sig : M.ptyp list;
  2. osl_ret : M.ptyp;
}
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 varfun = [
  1. | `Variable of PT.variable_decl
  2. | `Function of PT.s_function
]
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_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;
}
Sourceval globals : (string * M.const * M.ptyp) list
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. | `Field
  8. | `Pred
  9. | `RExpr
  10. | `Ref of int
]
Sourcetype security_pred_ = {
  1. sp_sig : sptyp list;
}
Sourceand sptyp = [
  1. | `ActionDesc
  2. | `Role
  3. | `Action
]
Sourceval security_preds : security_pred_ Ident.Mid.t
Sourcetype 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;
}
Sourcetype 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;
}
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
  7. | `Effect of 'env * M.instruction
  8. | `Postcondition of M.lident * M.pterm * (M.lident * M.pterm list) list
]
Sourcetype '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;
}
Sourcetype transitiondecl = {
  1. td_name : M.lident;
}
Sourcetype statedecl = {
  1. sd_ctors : (M.lident * M.pterm list) list;
  2. sd_init : Ident.ident;
}
Sourceval pterm_arg_as_pterm : 'a M.term_arg -> 'a M.term_gen option
Sourceval procsig_of_operator : PT.operator -> procsig
Sourceval core_types : (string * M.ptyp) list
Sourcemodule Env : sig ... end
Sourcetype env = Env.t
Sourceval empty : env
Sourceval check_and_emit_name_free : env -> M.lident -> bool
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
Sourceval get_asset_method : string -> 'a option
Sourceexception InvalidType
Sourceval for_type_exn : env -> PT.type_t -> M.ptyp
Sourceval for_type : env -> PT.type_t -> M.ptyp option
Sourceval for_literal : env -> PT.literal Location.loced -> M.bval
Sourcetype emode_t = [
  1. | `Expr
  2. | `Formula
]
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 -> PT.expr -> PT.lident M.term_gen * (assetdecl * M.container) option
Sourceval 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
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 -> PT.label_expr -> env * (M.lident option * M.pterm)
Sourceval for_lbls_expr : 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.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.lident * M.ptyp) option
Sourceval for_instruction : env -> PT.expr -> env * M.instruction
Sourceval for_specification_item : env -> PT.specification_item -> env * env ispecification
Sourceval for_security_item : env -> PT.security_item -> (env * M.security_item) option
Sourceval for_specification : env -> PT.specification -> env * env ispecification list
Sourceval for_security : env -> PT.security -> env * M.security
Sourceval for_named_state : env -> PT.lident -> Ident.ident option
Sourceval for_state : env -> PT.expr -> Ident.ident option
Sourceval for_function : env -> PT.s_function Location.loced -> unit
Sourceval for_callby : env -> PT.expr -> PT.lident list
Sourceval 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)
Sourceval for_effect : env -> PT.expr -> env * M.instruction
Sourceval for_transition : env -> (PT.lident * (PT.expr * 'a) option * (PT.expr * 'b) option) -> Ident.ident option * M.pterm option * (env * M.instruction) option
Sourcetype state = (PT.lident * PT.enum_option list) list
Sourceval for_state_decl : env -> state Location.loced -> env * (Ident.ident * (PT.lident * M.pterm list) list) option
Sourceval for_varfun_decl : env -> varfun Location.loced -> env * [> `Variable of vardecl ] option
Sourceval for_varfuns_decl : env -> varfun Location.loced list -> env * [> `Variable of vardecl ] option list
Sourceval for_asset_decl : 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_acttx_decl : env -> acttx Location.loced -> Env.t * env actiondecl
Sourceval for_acttxs_decl : env -> acttx Location.loced list -> env * env actiondecl 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
Sourceval 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)
Sourceval assets_of_adecls : assetdecl option list -> M.lident M.asset_struct list
Sourceval variables_of_fdecls : [< `Variable of vardecl ] option list -> M.lident M.variable list
Sourceval specifications_of_ispecifications : env ispecification list -> M.lident M.specification
Sourceval transactions_of_tdecls : env actiondecl 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
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