archetype 1.0.0 · 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 =

| AlienPattern
| AnonymousFieldInEffect
| AssertInGlobalSpec
| AssetExpected of M.ptyp
| AssetWithoutFields
| BeforeIrrelevant of [ `Local | `State ]
| BeforeOrLabelInExpr
| BindingInExpr
| CannotAssignArgument of Ident.ident
| CannotAssignLoopIndex of Ident.ident
| CannotCaptureLocal
| CannotInfer
| CannotInferAnonRecord
| CannotInferCollectionType
| CannotInitShadowField
| CannotUpdatePKey
| CollectionExpected
| ContainerOfNonAsset
| ContractInvariantInLocalSpec
| DivergentExpr
| DoesNotSupportMethodCall
| DuplicatedArgName of Ident.ident
| DuplicatedContractEntryName of Ident.ident
| DuplicatedCtorName of Ident.ident
| DuplicatedFieldInAssetDecl of Ident.ident
| DuplicatedFieldInRecordLiteral of Ident.ident
| DuplicatedInitMarkForCtor
| DuplicatedPKey
| DuplicatedVarDecl of Ident.ident
| EffectInGlobalSpec
| EmptyEnumDecl
| ExpressionExpected
| ForeignState of Ident.ident option * Ident.ident option
| FormulaExpected
| IncompatibleTypes of M.ptyp * M.ptyp
| InvalidArcheTypeDecl
| InvalidAssetCollectionExpr of M.ptyp
| InvalidAssetExpression
| InvalidCallByExpression
| InvalidContractExpression
| InvalidEffectForCtn of M.container * M.container list
| InvalidEntryDescription
| InvalidEntryExpression
| InvalidExpression
| InvalidExpressionForEffect
| InvalidFieldsCountInRecordLiteral
| InvalidFormula
| InvalidInstruction
| InvalidLValue
| InvalidMethodInExec
| InvalidMethodInFormula
| InvalidNumberOfArguments of int * int
| InvalidRoleExpression
| InvalidSecurityEntry
| InvalidSecurityRole
| InvalidShadowFieldAccess
| InvalidShadowVariableAccess
| InvalidSortingExpression
| InvalidStateExpression
| InvalidTypeForPk
| InvalidTypeForVarWithFromTo
| InvalidVarOrArgType
| LabelInNonInvariant
| LetInElseInInstruction
| LetInElseOnNonOption
| MethodCallInPredicate
| MissingFieldInRecordLiteral of Ident.ident
| MissingInitValueForShadowField
| MixedAnonInRecordLiteral
| MixedFieldNamesInRecordLiteral of Ident.ident list
| MoreThanOneInitState of Ident.ident list
| MultipleAssetStateDeclaration
| MultipleFromToInVarDecl
| MultipleInitialMarker
| MultipleMatchingFunction of Ident.ident * M.ptyp list * (M.ptyp list * M.ptyp) list
| MultipleMatchingOperator of PT.operator * M.ptyp list * opsig list
| MultipleStateDeclaration
| NameIsAlreadyBound of Ident.ident * Location.t option
| NoLetInInstruction
| NoMatchingFunction of Ident.ident * M.ptyp list
| NoMatchingOperator of PT.operator * M.ptyp list
| NonCodeLabel of Ident.ident
| NonIterable
| NonLoopLabel of Ident.ident
| NoSuchMethod of Ident.ident
| NoSuchSecurityPredicate of Ident.ident
| NotAKeyOfType
| NotAnAssetType
| NotAnEnumType
| NotAPrimitiveType
| NotARole of Ident.ident
| NumericExpressionExpected
| NumericOrCurrencyExpressionExpected
| OpInRecordLiteral
| OrphanedLabel of Ident.ident
| PackUnpackOnNonPrimitive
| PartialMatch of Ident.ident list
| PostConditionInGlobalSpec
| PredicateCallInExpr
| ReadOnlyGlobal of Ident.ident
| SecurityInExpr
| ShadowPKey
| ShadowSKey
| SpecOperatorInExpr
| TransferWithoutDest
| UninitializedVar
| UnknownAsset of Ident.ident
| UnknownContractEntryPoint of Ident.ident * Ident.ident
| UnknownEntry of Ident.ident
| UnknownEnum 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
| UpdateEffectOnPkey
| UpdateEffectWithoutDefault
| UselessPattern
| UsePkeyOfInsteadOfAsset
| VoidMethodInExpr
| VSetInExpr
| VSetOnNonAsset

val show_error_desc : error_desc -> Ppx_deriving_runtime.string

type error = L.t * error_desc

val pp_operator : Core.Format.formatter -> PT.operator -> unit

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

type argtype = [

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

]

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 = [

| `Entry of PT.entry_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;
gr_externals : PT.contract_decl Location.loced list;

}

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

val statename : string

type ('args, 'rty) gmethod_ = {

mth_name : M.const;
mth_place : [ `Both | `OnlyFormula | `OnlyExec ];
mth_purity : [ `Pure | `Effect of M.container list ];
mth_totality : [ `Total | `Partial ];
mth_sig : 'args * 'rty option;

}

type mthstyp = [

| `T of M.ptyp

]

type mthtyp = [

| mthstyp
| `The
| `Pk
| `ThePkForAggregate
| `Asset
| `SubColl
| `Cmp
| `Pred of bool
| `RExpr of bool
| `Ef of bool
| `Ref of int

]

and mthatyp = [

| `Fixed of mthtyp list
| `Multi of mthtyp

]

type smethod_ = (mthstyp list, mthstyp) gmethod_

type method_ = (mthatyp, mthtyp) gmethod_

val methods : method_ Ident.Mid.t

val coreops : 
  (string * M.const * [> `Total ] * 'a option * M.ptyp list * M.ptyp) list

val optionops : 
  (string * M.const * [> `Partial | `Total ] * M.ptyp option * 'a list * M.ptyp)
    list

val listops : 
  (string
   * M.const
   * [> `Partial | `Total ]
   * M.ptyp option
   * M.ptyp list
   * M.ptyp)
    list

val cryptoops : 
  (string * M.const * [> `Total ] * 'a option * M.ptyp list * M.ptyp) list

val packops : 
  (string * M.const * [> `Total ] * 'a option * M.ptyp list * M.ptyp) list

val allops : 
  (string
   * M.const
   * [> `Partial | `Total ]
   * M.ptyp option
   * M.ptyp list
   * M.ptyp)
    list

type assetdecl = {

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

}

and fielddecl = {

fd_name : M.lident;
fd_type : M.ptyp;
fd_dfl : M.pterm option;
fd_ghost : bool;

}

val pp_assetdecl : 
  Ppx_deriving_runtime.Format.formatter ->
  assetdecl ->
  Ppx_deriving_runtime.unit

val show_assetdecl : assetdecl -> Ppx_deriving_runtime.string

val pp_fielddecl : 
  Ppx_deriving_runtime.Format.formatter ->
  fielddecl ->
  Ppx_deriving_runtime.unit

val show_fielddecl : fielddecl -> Ppx_deriving_runtime.string

val get_field : Ident.ident -> assetdecl -> fielddecl option

type vardecl = {

vr_name : M.lident;
vr_type : M.ptyp;
vr_kind : [ `Constant | `Variable | `Ghost | `Enum ];
vr_invs : M.lident M.label_term list;
vr_def : (M.pterm * [ `Inline | `Std ]) option;
vr_tgt : M.lident option * M.lident 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) * M.pterm
| `Variable of M.lident * M.pterm option
| `Asset 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 'env fundecl = {

fs_name : M.lident;
fs_args : (M.lident * M.ptyp) list;
fs_retty : M.ptyp;
fs_body : M.instruction;
fs_spec : 'env ispecification list option;

}

type preddecl = {

pr_name : M.lident;
pr_args : (M.lident * M.ptyp) list;
pr_body : M.pterm;

}

type txeffect = {

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

}

type 'env tentrydecl = {

ad_name : M.lident;
ad_args : (M.lident * M.ptyp) list;
ad_callby : M.pterm option Location.loced list;
ad_effect : [ `Raw of M.instruction | `Tx of transition ] option;
ad_funs : 'env fundecl option list;
ad_reqs : (M.lident option * M.pterm) list;
ad_fais : (M.lident option * M.pterm) list;
ad_spec : 'env ispecification list;
ad_actfs : bool;

}

and transition = M.sexpr * (M.lident * assetdecl) option * txeffect list

type statedecl = {

sd_name : M.lident;
sd_state : bool;
sd_ctors : ctordecl list;
sd_init : Ident.ident;

}

and ctordecl = M.lident * (M.lident option * M.pterm) list

type contractdecl = {

ct_name : M.lident;
ct_entries : (M.lident * (M.lident * M.ptyp) list) list;

}

type definitiondecl = {

df_name : M.lident;
df_arg : M.lident * M.ptyp;
df_asset : M.lident;
df_body : M.pterm;

}

val pterm_arg_as_pterm : 'a M.term_arg -> 'a M.term_gen option

val core_types : (string * M.ptyp) list

module Env : sig ... end

type env = Env.t

val coreloc : Location.t

val empty : env

val check_and_emit_name_free : env -> M.lident -> bool

val select_operator : 
  Env.t ->
  ?asset:bool ->
  L.t ->
  (PT.operator * M.ptyp list) ->
  opsig option

val valid_var_or_arg_type : M.ptyp -> 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

exception InvalidType

val for_type_exn : ?pkey:Ident.ident list -> env -> PT.type_t -> M.ptyp

val for_type : ?pkey:Ident.ident list -> env -> PT.type_t -> M.ptyp option

val for_asset_type : env -> PT.type_t -> M.lident option

val for_asset_keyof_type : env -> PT.type_t -> M.lident option

val for_literal : env -> PT.literal Location.loced -> M.bval

type imode_t = [

| `Ghost
| `Concrete

]

type ekind = [

| `Expr of imode_t
| `Formula of bool

]

type emode_t = {

em_kind : ekind;
em_pred : bool;

}

val is_expr_kind : ekind -> bool

val is_form_kind : ekind -> bool

val expr_mode : imode_t -> emode_t

val form_mode : bool -> emode_t

val for_xexpr : 
  emode_t ->
  ?autoview:bool ->
  ?capture:
    [ `No | `Yes of (Location.t * M.ptyp) Ident.Mid.t Stdlib.ref option ] ->
  env ->
  ?ety:M.ptyp ->
  PT.expr ->
  PT.lident M.term_node M.struct_poly

val cast_expr : 
  ?autoview:bool ->
  env ->
  M.ptyp option ->
  PT.lident M.term_node M.struct_poly ->
  PT.lident M.term_node M.struct_poly

val join_expr : 
  ?autoview:bool ->
  env ->
  M.ptyp option ->
  PT.lident M.term_node M.struct_poly list ->
  M.ptyp option * PT.lident M.term_gen list

val 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

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 ->
  [ `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly ] ->
  PT.lident M.term_gen * (assetdecl * M.container) option

val for_contract_expr : 
  emode_t ->
  env ->
  PT.expr ->
  PT.lident M.term_node M.struct_poly * contractdecl option

val for_api_call : 
  emode_t ->
  env ->
  Location.t ->
  ([< `Parsed of PT.expr
   | `Typed of PT.lident M.term_node M.struct_poly Typed ]
   * PT.lident
   * PT.expr list) ->
  (M.pterm * smethod_ * M.lident M.term_arg list) option

val for_gen_method_call : 
  emode_t ->
  env ->
  Location.t ->
  ([ `Parsed of PT.expr | `Typed of PT.lident M.term_node M.struct_poly ]
   * PT.lident
   * PT.expr list) ->
  (M.pterm
   * (assetdecl * M.container)
   * method_
   * M.lident M.term_arg list
   * M.type_ Tools.Mint.t)
    option

val for_arg_effect : 
  emode_t ->
  env ->
  update:bool ->
  assetdecl ->
  PT.expr ->
  (PT.lident * M.operator * PT.lident M.term_gen) list option

val for_assign_expr : 
  ?autoview:bool ->
  ?asset:bool ->
  emode_t ->
  env ->
  Location.t ->
  (M.assignment_operator * M.ptyp * M.ptyp) ->
  PT.expr ->
  PT.lident M.term_gen

val for_formula : ?invariant:bool -> env -> PT.expr -> M.pterm

val for_entry_description : env -> PT.security_arg -> M.entry_description

val for_security_entry : env -> PT.security_arg -> M.security_entry

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 : 
  imode_t ->
  ?autoview:bool ->
  env ->
  ?ety:M.type_ ->
  PT.expr ->
  M.pterm

val for_lbl_expr : 
  ?ety:M.type_ ->
  imode_t ->
  env ->
  PT.label_expr ->
  env * (M.lident option * M.pterm)

val for_lbls_expr : 
  imode_t ->
  ?ety:M.type_ ->
  env ->
  PT.label_exprs ->
  env * (M.lident option * M.pterm) list

val for_lbl_bexpr : 
  imode_t ->
  env ->
  PT.label_expr ->
  env * (M.lident option * M.pterm)

val for_lbls_bexpr : 
  imode_t ->
  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 : 
  ?can_asset:bool ->
  env ->
  PT.lident_typ ->
  env * (PT.lident * M.ptyp) option

val for_args_decl : 
  ?can_asset:bool ->
  env ->
  PT.args ->
  env * (PT.lident * M.ptyp) option list

val for_lvalue : imode_t -> env -> PT.expr -> (M.lvalue * M.ptyp) option

val for_instruction_r : imode_t -> env -> PT.expr -> env * M.instruction

val for_instruction : imode_t -> env -> PT.expr -> env * M.instruction

val for_effect : imode_t -> env -> PT.expr -> Env.t * (env * M.instruction)

type spmode = [

| `Global
| `Local

]

val for_specification_item : 
  spmode ->
  (env * env) ->
  PT.specification_item ->
  (env * env) * env ispecification list

val for_specification : 
  spmode ->
  (env * env) ->
  PT.specification ->
  env * env ispecification list

module SecurityPred : sig ... end

val for_security_item : 
  env ->
  PT.security_item ->
  (env * M.security_item) option

val for_security : env -> PT.security -> env * M.security

val for_named_state : 
  ?enum:Ident.ident ->
  env ->
  PT.lident ->
  Ident.ident Location.loced

val for_state_formula : ?enum:Ident.ident -> env -> PT.expr -> M.sexpr

val for_function : 
  env ->
  PT.s_function Location.loced ->
  Env.t * env fundecl option

val for_callby : env -> PT.expr -> M.pterm option Location.loced list

val for_entry_properties : 
  (env * env) ->
  PT.entry_properties ->
  env
  * (M.pterm option Location.loced list option
     * (M.lident option * M.pterm) list option
     * (M.lident option * M.pterm) list option
     * env ispecification list option
     * env fundecl option list)

val for_transition : 
  ?enum:Ident.ident ->
  env ->
  (PT.lident * (PT.expr * 'a) option * (PT.expr * 'b) option) ->
  env * txeffect

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

val for_core_enum_decl : 
  env ->
  enum_core Location.loced ->
  env * (Ident.ident * (PT.lident * PT.label_expr list) list) option

val for_enum_decl : 
  env ->
  (PT.lident * PT.enum_decl) Location.loced ->
  env * (statedecl option * PT.label_expr list list option)

val for_enums_decl : 
  env ->
  (PT.lident * PT.enum_decl) Location.loced list ->
  env * (statedecl option * PT.label_expr list list option) list

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

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

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

val for_funs_decl : 
  env ->
  PT.s_function Location.loced list ->
  env * env fundecl option list

type pre_assetdecl = {

pas_name : M.lident;
pas_fields : (string * M.ptyp * PT.expr option * bool) Location.loced list;
pas_pk : M.lident;
pas_sortk : M.lident list;
pas_invs : PT.label_exprs list;
pas_state : statedecl option;
pas_init : PT.expr list;

}

val for_asset_decl : 
  Ident.ident list ->
  env ->
  (assetdecl * PT.asset_decl Location.loced) ->
  Env.t * pre_assetdecl option

val for_assets_decl : 
  env ->
  PT.asset_decl Location.loced list ->
  env * assetdecl option list

val for_contract_decl : 
  env ->
  PT.contract_decl Location.loced ->
  env * contractdecl option

val for_contracts_decl : 
  env ->
  PT.contract_decl Location.loced list ->
  env * contractdecl option list

val for_acttx_decl : 
  env ->
  acttx Location.loced ->
  Env.t * env tentrydecl option

val for_acttxs_decl : 
  env ->
  acttx Location.loced list ->
  env * env tentrydecl option 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

type decls = {

state : statedecl option;
contracts : contractdecl option list;
variables : vardecl option list;
enums : statedecl option list;
assets : assetdecl option list;
functions : env fundecl option list;
acttxs : env tentrydecl option list;
specs : env ispecification list list;
secspecs : M.security list;

}

val for_grouped_declarations : env -> (L.t * groups) -> env * decls

val enums_of_statedecl : statedecl list -> M.enum 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 contracts_of_cdecls : 
  contractdecl option list ->
  M.lident M.contract_struct list

val specifications_of_ispecifications : 
  env ispecification list ->
  M.lident M.specification

val functions_of_fdecls : 
  env fundecl option list ->
  M.lident M.function_struct list

val transentrys_of_tdecls : 
  env tentrydecl option 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