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 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. | DifferentMemoSizeForSaplingVerifyUpdate of int * int
  34. | DivergentExpr
  35. | DoesNotSupportMethodCall
  36. | DuplicatedArgName of Ident.ident
  37. | DuplicatedCtorName of Ident.ident
  38. | DuplicatedFieldInAssetDecl of Ident.ident
  39. | DuplicatedFieldInAssetOrRecordLiteral of Ident.ident
  40. | DuplicatedFieldInRecordDecl of Ident.ident
  41. | DuplicatedInitMarkForCtor
  42. | DuplicatedPackingVar of Ident.ident
  43. | DuplicatedPkeyField of Ident.ident
  44. | DuplicatedVarDecl of Ident.ident
  45. | EffectInGlobalSpec
  46. | EmptyEnumDecl
  47. | ExpressionExpected
  48. | FileNotFound of Ident.ident
  49. | ForeignState of Ident.ident option * Ident.ident option
  50. | FormulaExpected
  51. | IncompatibleSpecSig
  52. | IncompatibleTypes of A.ptyp * A.ptyp
  53. | IndexOutOfBoundForTuple
  54. | InvalidArcheTypeDecl
  55. | InvalidAssetCollectionExpr of A.ptyp
  56. | InvalidAssetExpression
  57. | InvalidAssetGetContainer of A.container
  58. | InvalidCallByAsset
  59. | InvalidCallByExpression
  60. | InvalidContractValueForCreateContract
  61. | InvalidEffectForCtn of A.container * A.container list
  62. | InvalidEntryDescription
  63. | InvalidEntryExpression
  64. | InvalidEventType
  65. | InvalidExpression
  66. | InvalidExpressionForEffect
  67. | InvalidExprressionForTupleAccess
  68. | InvalidFailIdType of Ident.ident * A.ptyp * A.ptyp
  69. | InvalidFieldsCountInAssetOrRecordLiteral
  70. | InvalidFoldInit of A.ptyp
  71. | InvalidForIdentMap
  72. | InvalidForIdentSimple
  73. | InvalidFormula
  74. | InvalidInstruction
  75. | InvalidKeyFieldInAssetValueType
  76. | InvalidLValue
  77. | InvalidMapType
  78. | InvalidMethodInExec
  79. | InvalidMethodInFormula
  80. | InvalidMethodWithBigMap of Ident.ident
  81. | InvalidMethodWithIterableBigMap of Ident.ident
  82. | InvalidNumberOfArguments of int * int
  83. | InvalidNumberOfParameters of int * int
  84. | InvalidPackingExpr
  85. | InvalidPackingFormat
  86. | InvalidRecordFieldType
  87. | InvalidRoleExpression
  88. | InvalidSaplingEmptyStateArg
  89. | InvalidSecurityEntry
  90. | InvalidSecurityRole
  91. | InvalidShadowFieldAccess
  92. | InvalidShadowVariableAccess
  93. | InvalidSortingExpression
  94. | InvalidSourcedByAsset
  95. | InvalidSourcedByExpression
  96. | InvalidStateExpression
  97. | InvalidStringValue
  98. | InvalidTezValueOverflow
  99. | InvalidTypeDeclOpt
  100. | InvalidTypeForAddressToContract
  101. | InvalidTypeForBigMapKey
  102. | InvalidTypeForBigMapValue
  103. | InvalidTypeForCallview
  104. | InvalidTypeForContract
  105. | InvalidTypeForDoFailIf
  106. | InvalidTypeForDoRequire
  107. | InvalidTypeForEntrypoint
  108. | InvalidTypeForFail
  109. | InvalidTypeForFailSome
  110. | InvalidTypeForLambdaArgument
  111. | InvalidTypeForLambdaReturn
  112. | InvalidTypeForMake
  113. | InvalidTypeForMakeEvent
  114. | InvalidTypeForMapKey
  115. | InvalidTypeForMapOperator of A.ptyp
  116. | InvalidTypeForMapValue
  117. | InvalidTypeForOptionalAssign
  118. | InvalidTypeForOrLeft
  119. | InvalidTypeForOrRight
  120. | InvalidTypeForParameter
  121. | InvalidTypeForPk
  122. | InvalidTypeForSet
  123. | InvalidTypeForTuple
  124. | InvalidArlFile
  125. | InvalidTzFile
  126. | InvalidValueForCurrency
  127. | InvalidValueForMemoSize
  128. | InvalidVariableForMethod
  129. | InvalidVarOrArgType
  130. | LabelInNonInvariant
  131. | LetInElseInInstruction
  132. | LetInElseOnNonOption
  133. | MethodCallInPredicate
  134. | MisorderedPkeyFields
  135. | MissingFieldInAssetOrRecordLiteral of Ident.ident
  136. | MissingInitValueForShadowField
  137. | MixedAnonInAssetOrRecordLiteral
  138. | MixedFieldNamesInAssetOrRecordLiteral of Ident.ident list
  139. | MoreThanOneInitState of Ident.ident list
  140. | MultipleAssetStateDeclaration
  141. | MultipleInitialMarker
  142. | MultipleMatchingFunction of Ident.ident * A.ptyp list * (A.ptyp list * A.ptyp) list
  143. | MultipleMatchingOperator of PT.operator * A.ptyp list * opsig list
  144. | MultipleStateDeclaration
  145. | NameIsAlreadyBound of Ident.ident * Location.t option
  146. | NoLetInInstruction
  147. | NoMatchingFunction of Ident.ident * A.ptyp list
  148. | NoMatchingOperator of PT.operator * A.ptyp list
  149. | NonCodeLabel of Ident.ident
  150. | NonHomogeneousPattern of Ident.ident
  151. | NonIterable
  152. | NonIterableBigMapAsset of Ident.ident
  153. | NonLoopLabel of Ident.ident
  154. | NoSuchMethod of Ident.ident
  155. | NoSuchSecurityPredicate of Ident.ident
  156. | NotAKeyOfType
  157. | NotAnAssetType
  158. | NotAnEnumType
  159. | NotAPrimitiveType
  160. | NotARole of Ident.ident
  161. | NumericExpressionExpected
  162. | NumericOrCurrencyExpressionExpected
  163. | OpInRecordLiteral
  164. | OrphanedLabel of Ident.ident
  165. | PackUnpackOnNonPrimitive
  166. | PartialMatch of Ident.ident list
  167. | PostConditionInGlobalSpec
  168. | PredicateCallInExpr
  169. | ReadOnlyGlobal of Ident.ident
  170. | RecordExpected
  171. | ReturnInVoidContext
  172. | RecordUpdateDuplicatedFieldName of Ident.ident
  173. | RecordUpdateOnNonRecordOrAsset
  174. | RecordUpdateOnPKey
  175. | RecordUpdateWithInvalidFieldName
  176. | SecurityInExpr
  177. | ShadowPKey
  178. | ShadowSKey
  179. | SpecOperatorInExpr
  180. | StringLiteralExpected
  181. | TransferWithoutDest
  182. | UninitializedVar
  183. | UnknownAsset of Ident.ident
  184. | UnknownAssetToProperty of Ident.ident
  185. | UnknownCreateContractExtension of Ident.ident
  186. | UnknownEntry of Ident.ident
  187. | UnknownEnum of Ident.ident
  188. | UnknownFailId of Ident.ident
  189. | UnknownField of Ident.ident * Ident.ident
  190. | UnknownFieldName of Ident.ident
  191. | UnknownFunction of Ident.ident
  192. | UnknownGetter of Ident.ident
  193. | UnknownImport of Ident.ident
  194. | UnknownImportExtension of Ident.ident
  195. | UnknownView of Ident.ident
  196. | UnknownLabel of Ident.ident
  197. | UnknownLocalOrVariable of Ident.ident
  198. | UnknownProcedure of Ident.ident
  199. | UnknownState of Ident.ident
  200. | UnknownTypeName of Ident.ident
  201. | UnknownVariable of Ident.ident
  202. | UnpureInFormula
  203. | UpdateEffectOnPkey
  204. | UpdateEffectWithoutDefault
  205. | UselessPattern
  206. | UsePkeyOfInsteadOfAsset
  207. | VoidMethodInExpr
  208. | VSetInExpr
  209. | 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 = [
  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.lident;
  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.lident 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.lident;
  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.lident;
  2. vr_type : A.ptyp;
  3. vr_kind : [ `Constant | `Variable | `Ghost | `Enum ];
  4. vr_invs : A.lident 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.lident;
  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.lident;
  2. df_arg : A.lident * A.ptyp;
  3. df_asset : A.lident;
  4. 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
module Micheline : sig ... end
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
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 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 * 'a) * 'a | `Option of (A.lident * 'a) * 'a | `Or of (A.lident * 'a) * (A.lident * 'a) ] 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 -> 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 -> 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.lident A.term_gen * (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 -> 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 select_mop : ekind -> Ident.ident -> A.ptyp list -> PT.lident A.term_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 PT.lident A.term_node A.struct_poly Typed ] * PT.lident * PT.expr list) -> (A.pterm * (A.const * bool * (A.ptyp list * A.ptyp)) * A.lident A.term_gen 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_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 -> ('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 -> [< `Called | `Sourced ] -> PT.expr -> PT.lident A.term_node A.struct_poly option Location.loced list
val for_entry : env -> PT.entry_properties -> (PT.expr * 'a) option -> env * ((PT.lident A.term_node A.struct_poly option Location.loced list option * A.pterm option) * (PT.lident A.term_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_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 = {
  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.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 imports_of_vdecls : importdecl list -> A.import_struct 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 * bool) Location.loced list Location.loced option -> env * A.lident A.parameter 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
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