Module Archetype.Typing

module L = Location
module PT = ParseTree
module A = Ast
module Type : sig ... end
type opsig = {
osl_sig : A.ptyp list;
osl_ret : A.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 =
| TODO
| AEntryExpected of A.ptyp
| AlienPattern
| AnonymousFieldInEffect
| AssertInGlobalSpec
| AssetExpected of A.ptyp
| AssetOrRecordExpected of A.ptyp
| AssetUpdateInNonFormula
| AssetWithoutFields
| AssetWithoutPKey
| BeforeIrrelevant of [ `Local | `State ]
| BeforeOrLabelInExpr
| BindingInExpr
| CannotAssignArgument of Ident.ident
| CannotAssignLoopIndex of Ident.ident
| CannotAssignPatternVariable of Ident.ident
| CannotCaptureLocal
| CannotInfer
| CannotInferAnonAssetOrRecord
| CannotInferCollectionType
| CannotInitShadowField
| CannotUpdatePKey
| CollectionExpected
| ContainerOfNonAsset
| ContractInvariantInLocalSpec
| DivergentExpr
| DoesNotSupportMethodCall
| DuplicatedArgName of Ident.ident
| DuplicatedCtorName of Ident.ident
| DuplicatedFieldInAssetDecl of Ident.ident
| DuplicatedFieldInAssetOrRecordLiteral of Ident.ident
| DuplicatedFieldInRecordDecl of Ident.ident
| DuplicatedInitMarkForCtor
| DuplicatedPackingVar of Ident.ident
| DuplicatedPkeyField of Ident.ident
| DuplicatedVarDecl of Ident.ident
| EffectInGlobalSpec
| EmptyEnumDecl
| ExpressionExpected
| ForeignState of Ident.ident option * Ident.ident option
| FormulaExpected
| IncompatibleSpecSig
| IncompatibleTypes of A.ptyp * A.ptyp
| IndexOutOfBoundForTuple
| InvalidArcheTypeDecl
| InvalidAssetCollectionExpr of A.ptyp
| InvalidAssetExpression
| InvalidCallByExpression
| InvalidEffectForCtn of A.container * A.container list
| InvalidEntryDescription
| InvalidEntryExpression
| InvalidExpression
| InvalidExpressionForEffect
| InvalidExprressionForTupleAccess
| InvalidFieldsCountInAssetOrRecordLiteral
| InvalidFoldInit of A.ptyp
| InvalidForIdentMap
| InvalidForIdentSimple
| InvalidFormula
| InvalidInstruction
| InvalidLValue
| InvalidMapType
| InvalidMethodInExec
| InvalidMethodInFormula
| InvalidMethodWithBigMap of Ident.ident
| InvalidNumberOfArguments of int * int
| InvalidNumberOfParameters of int * int
| InvalidPackingExpr
| InvalidPackingFormat
| InvalidRecordFieldType
| InvalidRoleExpression
| InvalidSecurityEntry
| InvalidSecurityRole
| InvalidShadowFieldAccess
| InvalidShadowVariableAccess
| InvalidSortingExpression
| InvalidStateExpression
| InvalidTypeForBigMapKey
| InvalidTypeForBigMapValue
| InvalidTypeForContract
| InvalidTypeForDoFailIf
| InvalidTypeForDoRequire
| InvalidTypeForEntrypoint
| InvalidTypeForFail
| InvalidTypeForLambdaArgument
| InvalidTypeForLambdaReturn
| InvalidTypeForMapOperator of A.ptyp
| InvalidTypeForMapKey
| InvalidTypeForMapValue
| InvalidTypeForParameter
| InvalidTypeForOrLeft
| InvalidTypeForOrRight
| InvalidTypeForPk
| InvalidTypeForSet
| InvalidValueForCurrency
| InvalidVarOrArgType
| InvalidValueForMemoSize
| LabelInNonInvariant
| LetInElseInInstruction
| LetInElseOnNonOption
| MethodCallInPredicate
| MisorderedPkeyFields
| MissingFieldInAssetOrRecordLiteral of Ident.ident
| MissingInitValueForShadowField
| MixedAnonInAssetOrRecordLiteral
| MixedFieldNamesInAssetOrRecordLiteral of Ident.ident list
| MoreThanOneInitState of Ident.ident list
| MultipleAssetStateDeclaration
| MultipleInitialMarker
| MultipleMatchingFunction of Ident.ident * A.ptyp list * (A.ptyp list * A.ptyp) list
| MultipleMatchingOperator of PT.operator * A.ptyp list * opsig list
| MultipleStateDeclaration
| NameIsAlreadyBound of Ident.ident * Location.t option
| NoLetInInstruction
| NoMatchingFunction of Ident.ident * A.ptyp list
| NoMatchingOperator of PT.operator * A.ptyp list
| NonCodeLabel of Ident.ident
| NonHomogeneousPattern of Ident.ident
| NonIterable
| NonIterableBigMapAsset of Ident.ident
| 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
| RecordExpected
| ReturnInVoidContext
| RecordUpdateDuplicatedFieldName of Ident.ident
| RecordUpdateOnNonRecordOrAsset
| RecordUpdateOnPKey
| RecordUpdateWithInvalidFieldName
| SecurityInExpr
| ShadowPKey
| ShadowSKey
| SpecOperatorInExpr
| StringLiteralExpected
| TransferWithoutDest
| UninitializedVar
| UnknownAsset of Ident.ident
| UnknownAssetToProperty of Ident.ident
| UnknownEntry of Ident.ident
| UnknownEnum of Ident.ident
| UnknownField of Ident.ident * Ident.ident
| UnknownFieldName of Ident.ident
| UnknownFunction of Ident.ident
| UnknownGetter of Ident.ident
| UnknownLabel of Ident.ident
| UnknownLocalOrVariable of Ident.ident
| UnknownProcedure of Ident.ident
| UnknownState of Ident.ident
| UnknownTypeName of Ident.ident
| UnknownVariable of Ident.ident
| UnpureInFormula
| UpdateEffectOnPkey
| UpdateEffectWithoutDefault
| UselessPattern
| UsePkeyOfInsteadOfAsset
| VoidMethodInExpr
| VSetInExpr
| VSetOnNonAsset
val pp_error_desc : Ppx_deriving_runtime.Format.formatter -> error_desc -> Ppx_deriving_runtime.unit
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 A.type_
| `Effect of Ident.ident
]
val cmptypes : A.vtyp list
val grptypes : A.vtyp list
val rgtypes : A.vtyp list
val cmpsigs : (PT.operator * (A.vtyp list * A.vtyp)) list
val tsigs : (PT.operator * (A.vtyp list * A.vtyp)) list
val opsigs : (PT.operator * (A.vtyp list * A.vtyp)) list
val opsigs2 : (PT.operator * (A.vtyp list * A.ptyp)) 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_records : PT.record_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_specfuns : PT.specfun Location.loced list;
gr_specvars : (PT.lident * PT.label_exprs) Location.loced list;
gr_specassets : (PT.lident * PT.label_exprs) Location.loced list;
gr_secs : PT.security Location.loced list;
}
val globals : (string * A.const * A.ptyp) list
val statename : string
type ('args, 'rty) gmethod_ = {
mth_name : A.const;
mth_place : [ `Both | `OnlyFormula | `OnlyExec ];
mth_purity : [ `Pure | `Effect of A.container list ];
mth_totality : [ `Total | `Partial ];
mth_map_type : [ `Both | `Standard ];
mth_sig : 'args * 'rty option;
}
type mthstyp = [
| `T of A.ptyp
]
type mthtyp = [
| mthstyp
| `The
| `Pk
| `ThePkForAggregate
| `Asset
| `Coll
| `SubColl
| `PkOrAsset
| `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 listmthstyp) gmethod_
type method_ = (mthatypmthtyp) gmethod_
val methods : (string * method_) list
val methods : method_ Ident.Mid.t
type opinfo = string * A.const * [ `Partial | `Total ] * A.type_ option * A.type_ list * A.type_ * Type.trestr Tools.Mint.t
val coreops : opinfo list
val optionops : opinfo list
val setops : opinfo list
val listops : opinfo list
val mapops : opinfo list
val bigmapops : opinfo list
val cryptoops : opinfo list
val packops : opinfo list
val opsops : opinfo list
val lambdaops : opinfo list
val voting_ops : opinfo list
val ticket_ops : opinfo list
val sapling_ops : opinfo list
val bls_ops : opinfo list
val allops : opinfo list
type assetdecl = {
as_name : A.lident;
as_fields : fielddecl list;
as_pkty : A.ptyp;
as_pk : A.lident list;
as_sortk : A.lident list;
as_bm : bool;
as_invs : (A.lident option * A.pterm) list;
as_state : A.lident option;
as_init : A.pterm list list;
}
and fielddecl = {
fd_name : A.lident;
fd_type : A.ptyp;
fd_dfl : A.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 recorddecl = {
rd_name : A.lident;
rd_fields : rfielddecl list;
rd_packing : rpacking option;
}
and rfielddecl = {
rfd_name : A.lident;
rfd_type : A.ptyp;
rfd_dfl : A.pterm option;
}
and rpacking =
| RLeaf of A.lident
| RNode of rpacking list
val pp_recorddecl : Ppx_deriving_runtime.Format.formatter -> recorddecl -> Ppx_deriving_runtime.unit
val show_recorddecl : recorddecl -> Ppx_deriving_runtime.string
val pp_rfielddecl : Ppx_deriving_runtime.Format.formatter -> rfielddecl -> Ppx_deriving_runtime.unit
val show_rfielddecl : rfielddecl -> Ppx_deriving_runtime.string
val pp_rpacking : Ppx_deriving_runtime.Format.formatter -> rpacking -> Ppx_deriving_runtime.unit
val show_rpacking : rpacking -> Ppx_deriving_runtime.string
val get_rfield : Ident.ident -> recorddecl -> rfielddecl option
type vardecl = {
vr_name : A.lident;
vr_type : A.ptyp;
vr_kind : [ `Constant | `Variable | `Ghost | `Enum ];
vr_invs : A.lident A.label_term list;
vr_def : (A.pterm * [ `Inline | `Std ]) option;
vr_core : A.const option;
}
type 'env ispecification = [
| `Predicate of A.lident * (A.lident * A.ptyp) list * A.pterm
| `Definition of A.lident * (A.lident * A.ptyp) * A.pterm
| `Fails of (A.lident * A.lident * A.ptyp * A.pterm) list
| `Variable of A.lident * A.pterm option
| `Asset of A.lident * A.pterm * (A.lident * A.pterm list) list * A.lident list
| `Effect of 'env * A.instruction
| `Postcondition of A.lident * A.pterm * (A.lident * A.pterm list) list * A.lident list
]
type 'env fundecl = {
fs_name : A.lident;
fs_kind : A.fun_kind;
fs_args : (A.lident * A.ptyp) list;
fs_retty : A.ptyp;
fs_body : A.instruction;
fs_spec : 'env ispecification list;
}
type preddecl = {
pr_name : A.lident;
pr_args : (A.lident * A.ptyp) list;
pr_body : A.pterm;
}
type txeffect = {
tx_state : A.lident;
tx_when : A.pterm option;
tx_effect : A.instruction option;
}
type 'env tentrydecl = {
ad_name : A.lident;
ad_args : (A.lident * A.ptyp) list;
ad_callby : A.pterm option Location.loced list;
ad_effect : [ `Raw of A.instruction | `Tx of transition ] option;
ad_funs : 'env fundecl option list;
ad_reqs : (A.lident option * A.pterm * A.pterm option) list;
ad_fais : (A.lident option * A.pterm * A.pterm option) list;
ad_spec : 'env ispecification list;
ad_actfs : bool;
}
and transition = A.sexpr * (A.lident * assetdecl) option * txeffect list
type statedecl = {
sd_name : A.lident;
sd_state : bool;
sd_ctors : ctordecl list;
sd_init : Ident.ident;
}
and ctordecl = A.lident * A.ptyp list * (A.lident option * A.pterm) list
val get_ctor : Ident.ident -> ctordecl list -> ctordecl option
type definitiondecl = {
df_name : A.lident;
df_arg : A.lident * A.ptyp;
df_asset : A.lident;
df_body : A.pterm;
}
val pterm_arg_as_pterm : 'a A.term_arg -> 'a A.term_gen option
val core_types : (string * A.ptyp) list
val ident_of_pname : ParseTree.pname -> Ident.ident
module Env : sig ... end
type env = Env.t
val coreloc : Location.t
val empty : env
val ty_of_init_ty : env -> A.ptyp -> A.ptyp
val check_and_emit_name_free : env -> A.lident -> bool
val select_operator : Env.t -> ?⁠formula:bool -> ?⁠asset:bool -> L.t -> (PT.operator * A.ptyp list) -> opsig option
val valid_var_or_arg_type : A.ptyp -> bool
val for_container : env -> PT.container -> A.container
val for_assignment_operator : PT.assignment_operator -> A.assignment_operator
val tt_logical_operator : PT.logical_operator -> A.logical_operator
val tt_arith_operator : PT.arithmetic_operator -> A.arithmetic_operator
val tt_cmp_operator : PT.comparison_operator -> A.comparison_operator
exception InvalidType
val for_type_exn : ?⁠pkey:Ident.ident list -> env -> PT.type_t -> A.ptyp
val for_type : ?⁠pkey:Ident.ident list -> env -> PT.type_t -> A.ptyp option
val for_asset_type : env -> PT.type_t -> A.lident option
val for_asset_keyof_type : env -> PT.type_t -> A.lident option
val for_literal : env -> A.type_ option -> PT.literal Location.loced -> A.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 decompile_match_with : [< `Enum | `List of 'b | `Option of 'c | `Or of 'd ] -> (A.pattern * 'a) list -> [> `List of (A.lident * A.lident * 'a) * 'a | `Option of (A.lident * 'a) * 'a | `Or of (A.lident * 'a) * (A.lident * 'a) ] option
val for_xexpr : emode_t -> ?⁠autoview:bool -> ?⁠capture:[ `No | `Yes of (Location.t * A.type_) Ident.Mid.t Stdlib.ref option ] -> env -> ?⁠ety:A.ptyp -> PT.expr -> PT.lident A.term_node A.struct_poly
val cast_expr : ?⁠autoview:bool -> env -> A.ptyp option -> PT.lident A.term_node A.struct_poly -> PT.lident A.term_gen
val join_expr : ?⁠autoview:bool -> env -> A.ptyp option -> PT.lident A.term_node A.struct_poly list -> A.type_ option * PT.lident A.term_gen list
val for_gen_matchwith : emode_t -> env -> Location.t -> PT.expr -> PT.branch list -> ([ `Enum | `List of A.type_ | `Option of A.type_ | `Or of A.type_ * A.type_ ] * ctordecl list * A.lident A.term_gen * (int option * int option Tools.Mstr.t * (A.lident * A.ptyp) list list) * PT.expr list) option
val for_asset_expr : emode_t -> env -> PT.expr -> PT.lident A.term_node A.struct_poly * assetdecl option
val for_asset_collection_expr : emode_t -> env -> [ `Parsed of PT.expr | `Typed of PT.lident A.term_node A.struct_poly ] -> PT.lident A.term_gen * (assetdecl * A.container) option
val for_api_call : emode_t -> env -> Location.t -> ([< `Parsed of PT.expr | `Typed of PT.lident A.term_node A.struct_poly Typed ] * PT.lident * PT.expr list) -> (A.pterm * smethod_ * A.lident A.term_arg list) option
val for_gen_method_call : emode_t -> env -> Location.t -> ([ `Parsed of PT.expr | `Typed of PT.lident A.term_node A.struct_poly ] * PT.lident * PT.expr list) -> (A.pterm * (assetdecl * A.container) * method_ * A.lident A.term_arg list * A.type_ Tools.Mint.t) option
val for_arg_effect : emode_t -> env -> update:bool -> assetdecl -> PT.expr -> (PT.lident * A.operator * PT.lident A.term_gen) list option
val for_assign_expr : ?⁠autoview:bool -> ?⁠asset:bool -> emode_t -> env -> Location.t -> (A.assignment_operator * A.ptyp * A.ptyp) -> PT.expr -> PT.lident A.term_gen
val for_formula : ?⁠invariant:bool -> env -> PT.expr -> A.pterm
val for_entry_description : env -> PT.security_arg -> A.entry_description
val for_security_entry : env -> PT.security_arg -> A.security_entry
val for_security_role : env -> PT.security_arg -> A.security_role list
val for_role : env -> PT.lident -> A.security_role option
val for_expr : imode_t -> ?⁠autoview:bool -> env -> ?⁠ety:A.type_ -> PT.expr -> A.pterm
val for_lbl_expr : ?⁠ety:A.type_ -> imode_t -> env -> PT.label_expr -> env * (A.lident option * A.pterm)
val for_lbls_expr : imode_t -> ?⁠ety:A.type_ -> env -> PT.label_exprs -> env * (A.lident option * A.pterm) list
val for_lbl_bexpr : imode_t -> env -> PT.label_expr -> env * (A.lident option * A.pterm)
val for_rf : imode_t -> ?⁠ety:A.type_ -> env -> (PT.lident * PT.expr * PT.expr option) list -> env * (A.lident option * A.pterm * A.pterm option) list
val for_rfs : imode_t -> env -> (PT.lident * PT.expr * PT.expr option) list -> env * (A.lident option * A.pterm * A.pterm option) list
val for_lbl_formula : env -> PT.label_expr -> env * (A.lident option * A.pterm)
val for_xlbls_formula : env -> PT.label_exprs -> env * (A.lident option * A.pterm) list
val for_lbls_formula : env -> PT.label_exprs -> env * (A.lident option * A.pterm) list
val for_arg_decl : ?⁠can_asset:bool -> env -> PT.lident_typ -> env * (PT.lident * A.ptyp) option
val for_args_decl : ?⁠can_asset:bool -> env -> PT.args -> env * (PT.lident * A.ptyp) option list
val for_lvalue : imode_t -> env -> PT.expr -> (A.lvalue * A.ptyp) option
val for_instruction_r : ret:A.type_ option -> imode_t -> env -> PT.expr -> env * A.instruction
val for_instruction : ret:A.type_ option -> imode_t -> env -> PT.expr -> env * A.instruction
val for_effect : imode_t -> env -> PT.expr -> Env.t * (env * A.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 * A.security_item) option
val for_security : env -> PT.security -> env * A.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 -> A.sexpr
val named_sig_compatible : ('a Location.loced * A.ptyp) option list -> ('a Location.loced * A.ptyp) option list -> bool
val for_function : ?⁠xspecs:PT.specfun Location.loced list -> env -> PT.s_function Location.loced -> Env.t * env fundecl option
val for_callby : env -> PT.expr -> A.pterm option Location.loced list
val for_entry_properties : (env * env) -> PT.entry_properties -> env * (A.pterm option Location.loced list option * (A.lident option * A.pterm * A.pterm option) list option * (A.lident option * A.pterm * A.pterm option) 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.type_t list * PT.enum_option list) list
val for_core_enum_decl : env -> enum_core Location.loced -> env * (Ident.ident * (PT.lident * A.ptyp list * 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_var_specs : env -> (PT.lident * PT.label_exprs) Location.loced list -> unit
val for_fun_decl : ?⁠xspecs:PT.specfun Location.loced list -> env -> PT.s_function Location.loced -> Env.t * env fundecl option
val for_funs_decl : env -> PT.s_function Location.loced list -> PT.specfun Location.loced list -> env * env fundecl option list
val for_fun_specs : env -> PT.specfun Location.loced list -> unit
type pre_assetdecl = {
pas_name : A.lident;
pas_fields : (string * A.ptyp * PT.expr option * bool) Location.loced list;
pas_pkty : A.ptyp;
pas_pk : A.lident list;
pas_sortk : A.lident list;
pas_bm : bool;
pas_invs : PT.label_exprs list;
pas_state : statedecl option;
pas_init : PT.expr list;
}
val for_asset_decl : ?⁠xspecs:(Ident.ident Location.loced * PT.label_exprs) Location.loced list -> 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 -> (Ident.ident Location.loced * PT.label_exprs) Location.loced list -> env * assetdecl option list
val for_asset_specs : env -> (PT.lident * PT.label_exprs) Location.loced list -> unit
val for_record_decl : env -> PT.record_decl Location.loced -> env * recorddecl option
val for_records_decl : env -> PT.record_decl Location.loced list -> env * recorddecl option list
val for_acttx_decl : ?⁠xspecs:PT.specfun Location.loced list -> env -> acttx Location.loced -> Env.t * env tentrydecl option
val for_acttxs_decl : env -> acttx Location.loced list -> PT.specfun 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 * A.security list
val group_declarations : PT.declaration list -> groups
type decls = {
state : statedecl option;
variables : vardecl option list;
enums : statedecl option list;
records : recorddecl option list;
assets : assetdecl option list;
functions : env fundecl option list;
acttxs : env tentrydecl option list;
specs : env ispecification list list;
secspecs : A.security list;
}
val for_grouped_declarations : env -> (L.t * groups) -> env * decls
val enums_of_statedecl : statedecl list -> A.enum list
val assets_of_adecls : assetdecl option list -> A.lident A.asset_struct list
val records_of_rdecls : recorddecl list -> A.lident A.record_struct list
val variables_of_vdecls : vardecl option list -> A.lident A.variable list
val specifications_of_ispecifications : env ispecification list -> A.lident A.specification
val functions_of_fdecls : env fundecl option list -> A.lident A.function_struct list
val transentrys_of_tdecls : env tentrydecl option list -> A.lident A.transaction_struct list
val for_parameters : ?⁠init:PT.expr_unloc Location.loced -> env -> (A.lident * PT.type_t * PT.expr option) Location.loced list Location.loced option -> env * A.lident A.parameter list
val for_declarations : ?⁠init:PT.expr_unloc Location.loced -> env -> PT.declaration list Location.loced -> A.ast
val typing : ?⁠init:PT.expr_unloc Location.loced -> env -> PT.archetype -> A.ast