package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
module L = Location
module PT = ParseTree
module A = Ast
module T = Michelson
module Type : sig ... end
type opsig = {
  1. osl_sig : A.ptyp list;
  2. osl_ret : A.ptyp;
}
val pp_opsig : Ppx_deriving_runtime.Format.formatter -> opsig -> Ppx_deriving_runtime.unit
type namespace =
  1. | Resolve
  2. | Current
  3. | Named of Ident.ident
val show_namespace : namespace -> Ppx_deriving_runtime.string
val uknm : namespace
type longident = namespace * Ident.ident
val show_longident : longident -> Ppx_deriving_runtime.string
val unloc_longident : A.longident -> Ident.ident
val mknm : (Ident.ident option * 'a) -> namespace * 'b
val unloc_nmid : (PT.id_scope * 'a Location.loced) -> namespace * 'b
val loc_nmid : (PT.id_scope * 'a Location.loced) -> Location.t
type error_desc =
  1. | TODO
  2. | AEntryExpected of A.ptyp
  3. | AlienPattern
  4. | AnonymousFieldInEffect
  5. | AssertInGlobalSpec
  6. | AssetExpected of A.ptyp
  7. | AssetOrRecordExpected of A.ptyp
  8. | AssetUpdateInNonFormula
  9. | AssetWithoutFields
  10. | AssetWithoutPKey
  11. | BeforeIrrelevant of [ `Local | `State ]
  12. | BeforeOrLabelInExpr
  13. | BindingInExpr
  14. | CannotAssignArgument of Ident.ident
  15. | CannotAssignConstVar of Ident.ident
  16. | CannotAssignLoopIndex of Ident.ident
  17. | CannotAssignPatternVariable of Ident.ident
  18. | CannotAssignStorageVariableInFunction of Ident.ident
  19. | CannotAssignStorageVariableInView of Ident.ident
  20. | CannotCallFunctionInView
  21. | CannotCaptureVariables
  22. | CannotEffectConstVar
  23. | CannotInfer
  24. | CannotInferAnonAssetOrRecord
  25. | CannotInferCollectionType
  26. | CannotInitShadowField
  27. | CannotUpdatePKey
  28. | CannotUseInstrWithSideEffectInFunction
  29. | CannotUseInstrWithSideEffectInView
  30. | CollectionExpected
  31. | ContainerOfNonAsset
  32. | ContractInvariantInLocalSpec
  33. | DetachInvalidExprFrom
  34. | DetachInvalidType of Ident.ident
  35. | DifferentMemoSizeForSaplingVerifyUpdate of int * int
  36. | DivergentExpr
  37. | DoesNotSupportMethodCall
  38. | DuplicatedArgName of Ident.ident
  39. | DuplicatedCtorName of Ident.ident
  40. | DuplicatedFieldInAssetDecl of Ident.ident
  41. | DuplicatedFieldInAssetOrRecordLiteral of Ident.ident
  42. | DuplicatedFieldInRecordDecl of Ident.ident
  43. | DuplicatedInitMarkForCtor
  44. | DuplicatedPackingVar of Ident.ident
  45. | DuplicatedPkeyField of Ident.ident
  46. | DuplicatedVarDecl of Ident.ident
  47. | EffectInGlobalSpec
  48. | EmptyEnumDecl
  49. | ExpressionExpected
  50. | FileNotFound of Ident.ident
  51. | ForeignState of Ident.ident option * Ident.ident option
  52. | FormulaExpected
  53. | IncompatibleSpecSig
  54. | IncompatibleTypes of A.ptyp * A.ptyp
  55. | IndexOutOfBoundForTuple
  56. | InvalidArcheTypeDecl
  57. | InvalidAssetCollectionExpr of A.ptyp
  58. | InvalidAssetExpression
  59. | InvalidAssetGetContainer of A.container
  60. | InvalidCallByAsset
  61. | InvalidCallByExpression
  62. | InvalidContractValueForCreateContract
  63. | InvalidEffectForCtn of A.container * A.container list
  64. | InvalidEntryDescription
  65. | InvalidEntryExpression
  66. | InvalidEventType
  67. | InvalidExpression
  68. | InvalidExpressionForEffect
  69. | InvalidExprressionForTupleAccess
  70. | InvalidFailIdType of Ident.ident * A.ptyp * A.ptyp
  71. | InvalidFieldsCountInAssetOrRecordLiteral
  72. | InvalidFoldInit of A.ptyp
  73. | InvalidForIdentMap
  74. | InvalidForIdentSimple
  75. | InvalidFormula
  76. | InvalidInstruction
  77. | InvalidKeyFieldInAssetValueType
  78. | InvalidLValue
  79. | InvalidMapType
  80. | InvalidMethodInExec
  81. | InvalidMethodInFormula
  82. | InvalidMethodWithBigMap of Ident.ident
  83. | InvalidMethodWithIterableBigMap of Ident.ident
  84. | InvalidNumberOfArguments of int * int
  85. | InvalidNumberOfParameters of int * int
  86. | InvalidPackingExpr
  87. | InvalidPackingFormat
  88. | InvalidRecordFieldType
  89. | InvalidRoleExpression
  90. | InvalidSaplingEmptyStateArg
  91. | InvalidSecurityEntry
  92. | InvalidSecurityRole
  93. | InvalidShadowFieldAccess
  94. | InvalidShadowVariableAccess
  95. | InvalidSortingExpression
  96. | InvalidSourcedByAsset
  97. | InvalidSourcedByExpression
  98. | InvalidStateExpression
  99. | InvalidStringValue
  100. | InvalidTezValueOverflow
  101. | InvalidTypeDeclOpt
  102. | InvalidTypeForAddressToContract
  103. | InvalidTypeForBigMapKey
  104. | InvalidTypeForBigMapValue
  105. | InvalidTypeForCallview
  106. | InvalidTypeForContract
  107. | InvalidTypeForDoFailIf
  108. | InvalidTypeForDoRequire
  109. | InvalidTypeForEntrypoint
  110. | InvalidTypeForFail
  111. | InvalidTypeForFailSome
  112. | InvalidTypeForLambdaArgument
  113. | InvalidTypeForLambdaReturn
  114. | InvalidTypeForMake
  115. | InvalidTypeForMakeEvent
  116. | InvalidTypeForMapKey
  117. | InvalidTypeForMapOperator of A.ptyp
  118. | InvalidTypeForMapValue
  119. | InvalidTypeForOptionalAssign
  120. | InvalidTypeForOrLeft
  121. | InvalidTypeForOrRight
  122. | InvalidTypeForParameter
  123. | InvalidTypeForPk
  124. | InvalidTypeForSet
  125. | InvalidTypeForTuple
  126. | InvalidArgumentType of A.ptyp * A.ptyp
  127. | InvalidArlFile
  128. | InvalidStorageType of A.ptyp * A.ptyp
  129. | InvalidTzFile
  130. | InvalidValueForCurrency
  131. | InvalidValueForMemoSize
  132. | InvalidVariableForMethod
  133. | InvalidVarOrArgType
  134. | LabelInNonInvariant
  135. | LetInElseInInstruction
  136. | LetInElseOnNonOption
  137. | MethodCallInPredicate
  138. | MisorderedPkeyFields
  139. | MissingFieldInAssetOrRecordLiteral of Ident.ident
  140. | MissingInitValueForShadowField
  141. | MixedAnonInAssetOrRecordLiteral
  142. | MixedFieldNamesInAssetOrRecordLiteral of longident list
  143. | MoreThanOneInitState of Ident.ident list
  144. | MultipleAssetStateDeclaration
  145. | MultipleInitialMarker
  146. | MultipleMatchingFunction of Ident.ident * A.ptyp list * (A.ptyp list * A.ptyp) list
  147. | MultipleMatchingOperator of PT.operator * A.ptyp list * opsig list
  148. | MultipleStateDeclaration
  149. | NameIsAlreadyBound of Ident.ident * Location.t option
  150. | NoLetInInstruction
  151. | NoMatchingFunction of Ident.ident * A.ptyp list
  152. | NoMatchingOperator of PT.operator * A.ptyp list
  153. | NonCodeLabel of Ident.ident
  154. | NonHomogeneousPattern of Ident.ident
  155. | NonIterable
  156. | NonIterableBigMapAsset of longident
  157. | NonLoopLabel of Ident.ident
  158. | NoSuchMethod of Ident.ident
  159. | NoSuchSecurityPredicate of Ident.ident
  160. | NotAKeyOfType
  161. | NotAnAssetType
  162. | NotAnEnumType
  163. | NotAPrimitiveType
  164. | NotARole of Ident.ident
  165. | NumericExpressionExpected
  166. | NumericOrCurrencyExpressionExpected
  167. | OpInRecordLiteral
  168. | OrphanedLabel of Ident.ident
  169. | PackUnpackOnNonPrimitive
  170. | PartialMatch of Ident.ident list
  171. | PostConditionInGlobalSpec
  172. | PredicateCallInExpr
  173. | ReadOnlyGlobal of Ident.ident
  174. | RecordExpected
  175. | ReturnInVoidContext
  176. | RecordUpdateDuplicatedFieldName of Ident.ident
  177. | RecordUpdateOnNonRecordOrAsset
  178. | RecordUpdateOnPKey
  179. | RecordUpdateWithInvalidFieldName
  180. | SecurityInExpr
  181. | ShadowPKey
  182. | ShadowSKey
  183. | SpecOperatorInExpr
  184. | StringLiteralExpected
  185. | TransferWithoutDest
  186. | UninitializedVar
  187. | UnknownAsset of Ident.ident
  188. | UnknownAssetToProperty of Ident.ident
  189. | UnknownCreateContractExtension of Ident.ident
  190. | UnknownEntry of Ident.ident
  191. | UnknownEnum of Ident.ident
  192. | UnknownFailId of Ident.ident
  193. | UnknownField of longident * Ident.ident
  194. | UnknownFieldName of Ident.ident
  195. | UnknownFunction of Ident.ident
  196. | UnknownGetter of Ident.ident
  197. | UnknownImport of Ident.ident
  198. | UnknownImportExtension of Ident.ident
  199. | UnknownView of Ident.ident
  200. | UnknownLabel of Ident.ident
  201. | UnknownLocalOrVariable of longident
  202. | UnknownProcedure of Ident.ident
  203. | UnknownState of Ident.ident
  204. | UnknownTypeName of longident
  205. | UnknownVariable of Ident.ident
  206. | UnpureInFormula
  207. | UpdateEffectOnPkey
  208. | UpdateEffectWithoutDefault
  209. | UselessPattern
  210. | UsePkeyOfInsteadOfAsset
  211. | VoidMethodInExpr
  212. | VSetInExpr
  213. | 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_namespace : Stdlib.Format.formatter -> namespace -> unit
val pp_longident : Stdlib.Format.formatter -> (namespace * Ident.ident) -> Ppx_deriving_runtime.unit
val pp_error_desc : Stdlib.Format.formatter -> error_desc -> Ppx_deriving_runtime.unit
type argtype = [
  1. | `Type of A.type_
  2. | `Effect of Ident.ident
]
val cmptypes : A.vtyp list
val grptypes : A.vtyp list
val rgtypes : A.vtyp list
val vt_comparable : A.ptyp list
val cmpsigs : (PT.operator * (A.vtyp list * A.vtyp)) list
val tsigs : (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 = [
  1. | `Entry of PT.entry_decl
  2. | `Transition of PT.transition_decl
]
type groups = {
  1. gr_archetypes : (PT.lident * PT.exts) Location.loced list;
  2. gr_imports : (PT.lident * PT.lident) Location.loced list;
  3. gr_states : PT.enum_decl Location.loced list;
  4. gr_enums : (PT.lident * PT.enum_decl) Location.loced list;
  5. gr_assets : PT.asset_decl Location.loced list;
  6. gr_records : PT.record_decl Location.loced list;
  7. gr_events : PT.record_decl Location.loced list;
  8. gr_vars : PT.variable_decl Location.loced list;
  9. gr_funs : PT.s_function Location.loced list;
  10. gr_acttxs : acttx Location.loced list;
  11. gr_specs : PT.specification Location.loced list;
  12. gr_specfuns : PT.specfun Location.loced list;
  13. gr_specvars : (PT.lident * PT.label_exprs) Location.loced list;
  14. gr_specassets : (PT.lident * PT.label_exprs) Location.loced list;
  15. gr_secs : PT.security Location.loced list;
}
val globals : (string * A.const * A.ptyp) list
val statename : string
type ('args, 'rty) gmethod_ = {
  1. mth_name : A.const;
  2. mth_place : [ `Both | `OnlyFormula | `OnlyExec ];
  3. mth_purity : [ `Pure | `Effect of A.container list ];
  4. mth_totality : [ `Total | `Partial ];
  5. mth_map_type : [ `Both | `Standard ];
  6. mth_sig : 'args * 'rty option;
}
type mthstyp = [
  1. | `T of A.ptyp
]
type mthtyp = [
  1. | mthstyp
  2. | `The
  3. | `Pk
  4. | `OPk
  5. | `ThePkForAggregate
  6. | `Asset
  7. | `Coll
  8. | `SubColl
  9. | `Container
  10. | `PkOrAsset
  11. | `OptVal
  12. | `Cmp
  13. | `Pred of bool
  14. | `RExpr of bool
  15. | `Ef of bool
  16. | `Ref of int
]
and mthatyp = [
  1. | `Fixed of mthtyp list
  2. | `Multi of mthtyp
]
type smethod_ = (mthstyp list, mthstyp) gmethod_
type method_ = (mthatyp, mthtyp) gmethod_
val methods : method_ Ident.Mid.t
type opinfo = {
  1. op_name : string;
  2. op_const : A.const;
  3. op_partial : [ `Partial | `Total ];
  4. op_thety : A.type_ option;
  5. op_sig : A.type_ list;
  6. op_resty : [ `Self | `Ty of A.type_ ];
  7. op_restr : Type.trestr Tools.Mint.t;
  8. op_filter : (A.type_ list -> A.pterm list -> bool) option;
}
val op : ?op_filter:(A.type_ list -> A.pterm list -> bool) -> string -> A.const -> [ `Partial | `Total ] -> A.type_ option -> A.type_ list -> [ `Self | `Ty of A.type_ ] -> Type.trestr Tools.Mint.t -> opinfo
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 iterablebigmapops : opinfo list
val cryptoops : opinfo list
val mathops : opinfo list
val packops : opinfo list
val opsops : opinfo list
val lambdaops : opinfo list
val ticket_ops : opinfo list
val bls_ops : opinfo list
val timelock_ops : opinfo list
val allops : opinfo list
type importdecl = {
  1. id_name : A.lident;
  2. id_path : A.lident;
  3. id_content : Michelson.obj_micheline option;
  4. id_ast : A.ast option;
  5. id_entrypoints : (Ident.ident * A.type_) list;
  6. id_views : (Ident.ident * (A.type_ * A.type_)) list;
}
val pp_importdecl : Ppx_deriving_runtime.Format.formatter -> importdecl -> Ppx_deriving_runtime.unit
val show_importdecl : importdecl -> Ppx_deriving_runtime.string
type assetdecl = {
  1. as_name : A.longident;
  2. as_fields : fielddecl list;
  3. as_pkty : A.ptyp;
  4. as_pk : A.lident list;
  5. as_sortk : A.lident list;
  6. as_bm : A.map_kind;
  7. as_invs : (A.lident option * A.pterm) list;
  8. as_state : A.longident option;
  9. as_init : A.pterm list list;
}
and fielddecl = {
  1. fd_name : A.lident;
  2. fd_type : A.ptyp;
  3. fd_dfl : A.pterm option;
  4. 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 = {
  1. rd_name : A.longident;
  2. rd_fields : rfielddecl list;
  3. rd_packing : rpacking option;
}
and rfielddecl = {
  1. rfd_name : A.lident;
  2. rfd_type : A.ptyp;
  3. rfd_dfl : A.pterm option;
}
and rpacking =
  1. | RLeaf of A.lident
  2. | 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 = {
  1. vr_name : A.longident;
  2. vr_type : A.ptyp;
  3. vr_kind : [ `Constant | `Variable | `Ghost | `Enum ];
  4. vr_invs : A.label_term list;
  5. vr_def : (A.pterm * [ `Inline | `Std ]) option;
  6. vr_core : A.const option;
}
type 'env ispecification = [
  1. | `Predicate of A.lident * (A.lident * A.ptyp) list * A.pterm
  2. | `Definition of A.lident * (A.lident * A.ptyp) * A.pterm
  3. | `Fails of (A.lident * A.lident option * A.lident * A.ptyp * A.pterm) list
  4. | `Variable of A.lident * A.pterm option
  5. | `Asset of A.lident * A.pterm * (A.lident * A.pterm list) list * A.lident list
  6. | `Effect of 'env * A.instruction
  7. | `Postcondition of A.lident * A.pterm * (A.lident * A.pterm list) list * A.lident list
]
type 'env fundecl = {
  1. fs_name : A.lident;
  2. fs_kind : A.fun_kind;
  3. fs_args : (A.lident * A.ptyp) list;
  4. fs_retty : A.ptyp;
  5. fs_body : A.instruction;
  6. fs_spec : 'env ispecification list;
}
type preddecl = {
  1. pr_name : A.lident;
  2. pr_args : (A.lident * A.ptyp) list;
  3. pr_body : A.pterm;
}
type txeffect = {
  1. tx_state : A.lident;
  2. tx_when : A.pterm option;
  3. tx_effect : A.instruction option;
}
type 'env tentrydecl = {
  1. ad_name : A.lident;
  2. ad_args : (A.lident * A.ptyp) list;
  3. ad_srcby : A.pterm option Location.loced list * A.pterm option;
  4. ad_callby : A.pterm option Location.loced list * A.pterm option;
  5. ad_stateis : (A.lident * A.pterm option) option;
  6. ad_effect : [ `Raw of A.instruction | `Tx of transition ] option;
  7. ad_funs : 'env fundecl option list;
  8. ad_csts : (A.lident option * A.pterm * A.pterm option) list;
  9. ad_reqs : (A.lident option * A.pterm * A.pterm option) list;
  10. ad_fais : (A.lident option * A.pterm * A.pterm option) list;
  11. ad_spec : 'env ispecification list;
  12. ad_actfs : bool * A.pterm option;
}
and transition = A.sexpr * (A.lident * assetdecl) option * txeffect list
type statedecl = {
  1. sd_name : A.longident;
  2. sd_state : bool;
  3. sd_ctors : ctordecl list;
  4. 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 = {
  1. df_name : A.longident;
  2. df_arg : A.lident * A.ptyp;
  3. df_asset : A.lident;
  4. df_body : A.pterm;
}
val pterm_arg_as_pterm : A.pterm_arg -> A.pterm option
val core_types : (string * A.ptyp) list
val ident_of_pname : ParseTree.pname -> Ident.ident
val as_pre : [> `Pre of 'a ] -> 'b
val as_full : [> `Full of 'a ] -> 'b
module Env : sig ... end
type env = Env.t
module Micheline : sig ... end
val coreloc : Location.t
val empty : env
val normalize_type : env -> A.type_ -> A.type_
val ty_of_init_ty : env -> A.ptyp -> A.ptyp
type prekind = [
  1. | `Record
  2. | `Event
  3. | `Asset
  4. | `Enum
]
val check_and_emit_name_free : env -> ?pre:prekind -> 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
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.longident option
val for_asset_keyof_type : env -> PT.type_t -> A.longident option
val for_literal : env -> A.type_ option -> PT.literal Location.loced -> A.bval
type concrete_place = [
  1. | `Init
  2. | `Entry
  3. | `Function
  4. | `View
]
type imode_t = [
  1. | `Ghost
  2. | `Concrete of concrete_place
]
type ekind = [
  1. | `Expr of imode_t
  2. | `Formula of bool
]
type emode_t = {
  1. em_kind : ekind;
  2. 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 * 'a0) * 'a1 | `Option of (A.lident * 'a2) * 'a3 | `Or of (A.lident * 'a4) * (A.lident * 'a5) ] option
type capture = {
  1. cp_global : bool;
  2. cp_local : [ `Only of Ident.Sid.t | `Yes of (L.t * A.ptyp) Ident.Mid.t Stdlib.ref option ];
}
val capture0 : capture
val extend_capture : capture -> Ident.ident list -> capture
val for_xexpr : emode_t -> ?autoview:bool -> ?capture:capture -> env -> ?ety:A.ptyp -> PT.expr -> A.pterm_node A.struct_poly
val cast_expr : ?autoview:bool -> env -> A.ptyp option -> A.pterm_node A.struct_poly -> A.pterm
val join_expr : ?autoview:bool -> env -> A.ptyp option -> A.pterm_node A.struct_poly list -> A.type_ option * A.pterm list
val for_gen_matchwith : emode_t -> capture -> 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.pterm * (int option * int option Tools.Mstr.t * (Ident.ident Location.loced * A.ptyp) list list) * PT.expr list) option
val for_asset_expr : emode_t -> env -> PT.expr -> A.pterm_node A.struct_poly * Env.asset option
val for_asset_collection_expr : emode_t -> env -> [ `Parsed of PT.expr | `Typed of A.pterm_node A.struct_poly ] -> A.pterm * (assetdecl * A.container) option
val select_mop : ekind -> Ident.ident -> A.ptyp list -> A.pterm_node A.struct_poly list -> opinfo -> (int * (A.const * bool * (A.ptyp list * A.ptyp))) option
val for_api_call : mode:emode_t -> ?autoview:bool -> ?capture:capture -> env -> ([< `Parsed of PT.expr | `Typed of A.pterm_node A.struct_poly Typed ] * PT.lident * PT.expr list) -> (A.pterm * (A.const * bool * (A.ptyp list * A.ptyp)) * A.pterm list) option
val for_gen_method_call : emode_t -> env -> Location.t -> ([ `Parsed of PT.expr | `Typed of A.pterm_node A.struct_poly ] * PT.lident * PT.expr list) -> (A.pterm * (assetdecl * A.container) * method_ * A.pterm_arg list * A.type_ Tools.Mint.t) option
val for_arg_effect : emode_t -> env -> update:bool -> assetdecl -> PT.expr -> (A.lident * A.operator * A.pterm) list option
val for_assign_expr : ?autoview:bool -> ?asset:bool -> emode_t -> env -> Location.t -> (A.assignment_operator * A.ptyp * A.ptyp) -> PT.expr -> A.pterm
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_cf : 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_cfs : 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_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 = [
  1. | `Global
  2. | `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 -> ('b 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 -> [< `Called | `Sourced ] -> PT.expr -> A.pterm_node A.struct_poly option Location.loced list
val for_entry : env -> PT.entry_properties -> (PT.expr * 'a) option -> env * ((A.pterm_node A.struct_poly option Location.loced list option * A.pterm option) * (A.pterm_node A.struct_poly option Location.loced list option * A.pterm option) * (Ident.ident Location.loced * A.pterm option) option * (bool * A.pterm option) * (A.lident option * A.pterm * A.pterm option) 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 * A.instruction option)
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_vardecl_init : env -> PT.variable_decl Location.loced -> env * vardecl option
val for_vardecls_init : env -> PT.variable_decl Location.loced list -> env * vardecl option list
val for_var_specs : env -> (PT.lident * PT.label_exprs) Location.loced list -> unit
val for_vars_decl : env -> PT.variable_decl Location.loced list -> env * (vardecl option * PT.label_exprs option) list
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 = {
  1. pas_name : A.lident;
  2. pas_fields : (string * A.ptyp * PT.expr option * bool) Location.loced list;
  3. pas_pkty : A.ptyp;
  4. pas_pk : A.lident list;
  5. pas_sortk : A.lident list;
  6. pas_bm : A.map_kind;
  7. pas_invs : PT.label_exprs list;
  8. pas_state : statedecl option;
  9. pas_init : PT.expr list;
}
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 : [< `Event | `Record ] -> 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_events_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 = {
  1. imports : importdecl list;
  2. state : statedecl option;
  3. variables : vardecl option list;
  4. enums : statedecl option list;
  5. records : recorddecl option list;
  6. events : recorddecl option list;
  7. assets : assetdecl option list;
  8. functions : env fundecl option list;
  9. acttxs : env tentrydecl option list;
  10. specs : env ispecification list list;
  11. secspecs : A.security list;
}
val enums_of_statedecl : statedecl list -> A.enum list
val assets_of_adecls : assetdecl option list -> A.asset list
val records_of_rdecls : recorddecl list -> A.record list
val variables_of_vdecls : vardecl option list -> A.variable list
val imports_of_vdecls : importdecl list -> A.import_struct list
val specifications_of_ispecifications : env ispecification list -> A.specification
val functions_of_fdecls : env fundecl option list -> A.function_ list
val transentrys_of_tdecls : env tentrydecl option list -> A.transaction list
val for_parameters : ?init:PT.expr_unloc Location.loced -> env -> (A.lident * PT.type_t * PT.expr option * bool) Location.loced list Location.loced option -> env * A.parameter list
val sort_decl : Tools.String.t list -> A.decl_ list -> A.decl_ list
val for_import_decl : env -> (PT.lident * PT.lident) Location.loced list -> env * importdecl list
val for_grouped_declarations : env -> (L.t * groups) -> env * decls
val for_declarations : ?init:PT.expr_unloc Location.loced -> env -> PT.declaration list Location.loced -> A.ast
val pretype : env -> PT.declaration list -> env