archetype 0.1.8 · OCaml Package

module L = Location

module PT = ParseTree

module M = Ast

module Type : sig ... end

type opsig = {

osl_sig : M.ptyp list;
osl_ret : M.ptyp;

}

val pp_opsig : 
  Ppx_deriving_runtime.Format.formatter ->
  opsig ->
  Ppx_deriving_runtime.unit

val show_opsig : opsig -> Ppx_deriving_runtime.string

type error_desc =

| AssetExpected
| AssetWithoutFields
| BeforeOnLocalVar
| BindingInExpr
| CannotInferAnonRecord
| CannotInferCollectionType
| CollectionExpected
| DivergentExpr
| DuplicatedAssetName of Ident.ident
| DuplicatedCtorName of Ident.ident
| DuplicatedFieldInAssetDecl of Ident.ident
| DuplicatedFieldInRecordLiteral of Ident.ident
| DuplicatedInitMarkForCtor
| DuplicatedPKey
| DuplicatedVarDecl of Ident.ident
| AnonymousFieldInEffect
| EmptyStateDecl
| ExpressionExpected
| FormulaExpected
| IncompatibleTypes of M.ptyp * M.ptyp
| InvalidActionDescription
| InvalidActionExpression
| InvalidArcheTypeDecl
| InvalidAssetCollectionExpr
| InvalidAssetExpression
| InvalidCallByExpression
| InvalidExpressionForEffect
| InvalidExpression
| InvalidFieldsCountInRecordLiteral
| InvalidLValue
| InvalidFormula
| InvalidInstruction
| InvalidNumberOfArguments of int * int
| InvalidRoleExpression
| InvalidSecurityAction
| InvalidSecurityRole
| InvalidSortingExpression
| InvalidStateExpression
| LetInElseInInstruction
| MissingFieldInRecordLiteral of Ident.ident
| MixedAnonInRecordLiteral
| MixedFieldNamesInRecordLiteral of Ident.ident list
| MoreThanOneInitState of Ident.ident list
| MultipleInitialMarker
| MultipleMatchingOperator of PT.operator * M.ptyp list * opsig list
| MultipleStateDeclaration
| NameIsAlreadyBound of Ident.ident
| NoMatchingOperator of PT.operator * M.ptyp list
| NoSuchMethod of Ident.ident
| NoSuchSecurityPredicate of Ident.ident
| NonLoopLabel of Ident.ident
| NotARole of Ident.ident
| NumericExpressionExpected
| OpInRecordLiteral
| OrphanedLabel of Ident.ident
| ReadOnlyGlobal of Ident.ident
| SecurityInExpr
| SpecOperatorInExpr
| UninitializedVar
| UnknownAction of Ident.ident
| UnknownAsset of Ident.ident
| UnknownField of Ident.ident * Ident.ident
| UnknownFieldName of Ident.ident
| UnknownLabel of Ident.ident
| UnknownLocalOrVariable of Ident.ident
| UnknownProcedure of Ident.ident
| UnknownState of Ident.ident
| UnknownTypeName of Ident.ident
| UnpureInFormula
| VoidMethodInExpr
| AssetPartitionnedby of Ident.ident * Ident.ident list

val show_error_desc : error_desc -> Ppx_deriving_runtime.string

type error = L.t * error_desc

val pp_error_desc : Format.formatter -> error_desc -> Ppx_deriving_runtime.unit

type argtype = [

| `Type of M.type_
| `Effect of Ident.ident

]

type procsig = {

psl_sig : argtype list;
psl_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 acttx = [

| `Action of PT.action_decl
| `Transition of PT.transition_decl

]

type groups = {

gr_archetypes : (PT.lident * PT.exts) Location.loced list;
gr_states : PT.enum_decl Location.loced list;
gr_enums : (PT.lident * PT.enum_decl) Location.loced list;
gr_assets : PT.asset_decl Location.loced list;
gr_vars : PT.variable_decl Location.loced list;
gr_funs : PT.s_function Location.loced list;
gr_acttxs : acttx Location.loced list;
gr_specs : PT.specification Location.loced list;
gr_secs : PT.security Location.loced list;

}

val globals : (string * M.const * M.ptyp) list

type method_ = {

mth_name : M.const;
mth_purity : [ `Pure | `Effect ];
mth_totality : [ `Total | `Partial ];
mth_sig : mthtyp list * mthtyp option;

}

and mthtyp = [

| `T of M.ptyp
| `The
| `Pk
| `Effect
| `Asset
| `SubColl
| `Cmp
| `Pred
| `RExpr
| `Ref of int

]

val methods : method_ Ident.Mid.t

type assetdecl = {

as_name : M.lident;
as_fields : (M.lident * M.ptyp) list;
as_pk : M.lident;
as_sortk : M.lident list;
as_invs : (M.lident option * M.pterm) list;

}

type vardecl = {

vr_name : M.lident;
vr_type : M.ptyp;
vr_kind : [ `Constant | `Variable | `Ghost ];
vr_def : (M.pterm * [ `Inline | `Std ]) option;
vr_core : M.const option;

}

type 'env ispecification = [

| `Predicate of M.lident * (M.lident * M.ptyp) list * M.pterm
| `Definition of M.lident * (M.lident * M.ptyp) option * M.pterm
| `Lemma of M.lident * M.pterm
| `Theorem of M.lident * M.pterm
| `Variable of M.lident * M.pterm option
| `Assert of M.lident * M.pterm * (M.lident * M.pterm list) list * M.lident list
| `Effect of 'env * M.instruction
| `Postcondition of M.lident * M.pterm * (M.lident * M.pterm list) list * M.lident list

]

type txeffect = {

tx_state : M.lident;
tx_when : M.pterm option;
tx_effect : M.instruction option;

}

type 'env tactiondecl = {

ad_name : M.lident;
ad_args : (M.lident * M.ptyp) list;
ad_callby : M.lident list;
ad_effect : [ `Raw of M.instruction | `Tx of M.lident * txeffect list ] option;
ad_reqs : (M.lident option * M.pterm) list;
ad_fais : (M.lident option * M.pterm) list;
ad_spec : 'env ispecification list;

}

type statedecl = {

sd_ctors : (M.lident * (M.lident option * M.pterm) list) list;
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 tt_arith_operator : PT.arithmetic_operator -> M.arithmetic_operator

val tt_cmp_operator : PT.comparison_operator -> M.comparison_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 = [

| `Expr
| `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_assign_expr : 
  emode_t ->
  env ->
  Location.t ->
  (M.assignment_operator * M.ptyp) ->
  PT.expr ->
  PT.lident M.term_gen

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.lident option * 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

module SecurityPred : sig ... end

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 Location.loced

val for_state : env -> PT.expr -> M.lident

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.lident option * M.pterm) list option
     * (M.lident option * M.pterm) list option
     * 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) ->
  env * txeffect

type state = (PT.lident * PT.enum_option list) list

val for_state_decl : 
  env ->
  state Location.loced ->
  env
  * (Ident.ident * (PT.lident * (M.lident option * M.pterm) list) list) option

val for_var_decl : 
  env ->
  PT.variable_decl Location.loced ->
  env * vardecl option

val for_vars_decl : 
  env ->
  PT.variable_decl Location.loced list ->
  env * vardecl option list

val for_fun_decl : env -> PT.s_function Location.loced -> Env.t * unit option

val for_funs_decl : 
  env ->
  PT.s_function Location.loced list ->
  env * unit 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 tactiondecl

val for_acttxs_decl : 
  env ->
  acttx Location.loced list ->
  env * env tactiondecl 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
     * vardecl option list
     * unit option list
     * env tactiondecl list
     * env ispecification list list
     * M.security 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 specifications_of_ispecifications : 
  env ispecification list ->
  M.lident M.specification

val transactions_of_tdecls : 
  env tactiondecl 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

package archetype