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 Type : sig ... end
type opsig = {
  1. osl_sig : A.ptyp list;
  2. osl_ret : A.ptyp;
}
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. | CannotAssignLoopIndex of Ident.ident
  16. | CannotAssignPatternVariable of Ident.ident
  17. | CannotCaptureVariables
  18. | CannotInfer
  19. | CannotInferAnonAssetOrRecord
  20. | CannotInferCollectionType
  21. | CannotInitShadowField
  22. | CannotUpdatePKey
  23. | CollectionExpected
  24. | ContainerOfNonAsset
  25. | ContractInvariantInLocalSpec
  26. | DivergentExpr
  27. | DoesNotSupportMethodCall
  28. | DuplicatedArgName of Ident.ident
  29. | DuplicatedCtorName of Ident.ident
  30. | DuplicatedFieldInAssetDecl of Ident.ident
  31. | DuplicatedFieldInAssetOrRecordLiteral of Ident.ident
  32. | DuplicatedFieldInRecordDecl of Ident.ident
  33. | DuplicatedInitMarkForCtor
  34. | DuplicatedPackingVar of Ident.ident
  35. | DuplicatedPkeyField of Ident.ident
  36. | DuplicatedVarDecl of Ident.ident
  37. | EffectInGlobalSpec
  38. | EmptyEnumDecl
  39. | ExpressionExpected
  40. | ForeignState of Ident.ident option * Ident.ident option
  41. | FormulaExpected
  42. | IncompatibleSpecSig
  43. | IncompatibleTypes of A.ptyp * A.ptyp
  44. | IndexOutOfBoundForTuple
  45. | InvalidArcheTypeDecl
  46. | InvalidAssetCollectionExpr of A.ptyp
  47. | InvalidAssetExpression
  48. | InvalidCallByExpression
  49. | InvalidCallByAsset
  50. | InvalidEffectForCtn of A.container * A.container list
  51. | InvalidEntryDescription
  52. | InvalidEntryExpression
  53. | InvalidExpression
  54. | InvalidExpressionForEffect
  55. | InvalidExprressionForTupleAccess
  56. | InvalidFailIdType of Ident.ident * A.ptyp * A.ptyp
  57. | InvalidFieldsCountInAssetOrRecordLiteral
  58. | InvalidFoldInit of A.ptyp
  59. | InvalidForIdentMap
  60. | InvalidForIdentSimple
  61. | InvalidFormula
  62. | InvalidInstruction
  63. | InvalidLValue
  64. | InvalidMapType
  65. | InvalidMethodInExec
  66. | InvalidMethodInFormula
  67. | InvalidMethodWithBigMap of Ident.ident
  68. | InvalidNumberOfArguments of int * int
  69. | InvalidNumberOfParameters of int * int
  70. | InvalidPackingExpr
  71. | InvalidPackingFormat
  72. | InvalidRecordFieldType
  73. | InvalidRoleExpression
  74. | InvalidSaplingEmptyStateArg
  75. | InvalidSecurityEntry
  76. | InvalidSecurityRole
  77. | InvalidShadowFieldAccess
  78. | InvalidShadowVariableAccess
  79. | InvalidSortingExpression
  80. | InvalidSourcedByExpression
  81. | InvalidSourcedByAsset
  82. | InvalidStateExpression
  83. | InvalidStringValue
  84. | InvalidTypeForBigMapKey
  85. | InvalidTypeForBigMapValue
  86. | InvalidTypeForCallview
  87. | InvalidTypeForContract
  88. | InvalidTypeForDoFailIf
  89. | InvalidTypeForDoRequire
  90. | InvalidTypeForEntrypoint
  91. | InvalidTypeForFail
  92. | InvalidTypeForLambdaArgument
  93. | InvalidTypeForLambdaReturn
  94. | InvalidTypeForMapOperator of A.ptyp
  95. | InvalidTypeForMapKey
  96. | InvalidTypeForMapValue
  97. | InvalidTypeForParameter
  98. | InvalidTypeForOrLeft
  99. | InvalidTypeForOrRight
  100. | InvalidTypeForPk
  101. | InvalidTypeForSet
  102. | InvalidValueForCurrency
  103. | InvalidVariableForMethod
  104. | InvalidVarOrArgType
  105. | InvalidValueForMemoSize
  106. | LabelInNonInvariant
  107. | LetInElseInInstruction
  108. | LetInElseOnNonOption
  109. | MethodCallInPredicate
  110. | MisorderedPkeyFields
  111. | MissingFieldInAssetOrRecordLiteral of Ident.ident
  112. | MissingInitValueForShadowField
  113. | MixedAnonInAssetOrRecordLiteral
  114. | MixedFieldNamesInAssetOrRecordLiteral of Ident.ident list
  115. | MoreThanOneInitState of Ident.ident list
  116. | MultipleAssetStateDeclaration
  117. | MultipleInitialMarker
  118. | MultipleMatchingFunction of Ident.ident * A.ptyp list * (A.ptyp list * A.ptyp) list
  119. | MultipleMatchingOperator of PT.operator * A.ptyp list * opsig list
  120. | MultipleStateDeclaration
  121. | NameIsAlreadyBound of Ident.ident * Location.t option
  122. | NoLetInInstruction
  123. | NoMatchingFunction of Ident.ident * A.ptyp list
  124. | NoMatchingOperator of PT.operator * A.ptyp list
  125. | NonCodeLabel of Ident.ident
  126. | NonHomogeneousPattern of Ident.ident
  127. | NonIterable
  128. | NonIterableBigMapAsset of Ident.ident
  129. | NonLoopLabel of Ident.ident
  130. | NoSuchMethod of Ident.ident
  131. | NoSuchSecurityPredicate of Ident.ident
  132. | NotAKeyOfType
  133. | NotAnAssetType
  134. | NotAnEnumType
  135. | NotAPrimitiveType
  136. | NotARole of Ident.ident
  137. | NumericExpressionExpected
  138. | NumericOrCurrencyExpressionExpected
  139. | OpInRecordLiteral
  140. | OrphanedLabel of Ident.ident
  141. | PackUnpackOnNonPrimitive
  142. | PartialMatch of Ident.ident list
  143. | PostConditionInGlobalSpec
  144. | PredicateCallInExpr
  145. | ReadOnlyGlobal of Ident.ident
  146. | RecordExpected
  147. | ReturnInVoidContext
  148. | RecordUpdateDuplicatedFieldName of Ident.ident
  149. | RecordUpdateOnNonRecordOrAsset
  150. | RecordUpdateOnPKey
  151. | RecordUpdateWithInvalidFieldName
  152. | SecurityInExpr
  153. | ShadowPKey
  154. | ShadowSKey
  155. | SpecOperatorInExpr
  156. | StringLiteralExpected
  157. | TransferWithoutDest
  158. | UninitializedVar
  159. | UnknownAsset of Ident.ident
  160. | UnknownAssetToProperty of Ident.ident
  161. | UnknownEntry of Ident.ident
  162. | UnknownEnum of Ident.ident
  163. | UnknownFailId of Ident.ident
  164. | UnknownField of Ident.ident * Ident.ident
  165. | UnknownFieldName of Ident.ident
  166. | UnknownFunction of Ident.ident
  167. | UnknownGetter of Ident.ident
  168. | UnknownView of Ident.ident
  169. | UnknownLabel of Ident.ident
  170. | UnknownLocalOrVariable of Ident.ident
  171. | UnknownProcedure of Ident.ident
  172. | UnknownState of Ident.ident
  173. | UnknownTypeName of Ident.ident
  174. | UnknownVariable of Ident.ident
  175. | UnpureInFormula
  176. | UpdateEffectOnPkey
  177. | UpdateEffectWithoutDefault
  178. | UselessPattern
  179. | UsePkeyOfInsteadOfAsset
  180. | VoidMethodInExpr
  181. | VSetInExpr
  182. | 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
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_states : PT.enum_decl Location.loced list;
  3. gr_enums : (PT.lident * PT.enum_decl) Location.loced list;
  4. gr_assets : PT.asset_decl Location.loced list;
  5. gr_records : PT.record_decl Location.loced list;
  6. gr_vars : PT.variable_decl Location.loced list;
  7. gr_funs : PT.s_function Location.loced list;
  8. gr_acttxs : acttx Location.loced list;
  9. gr_specs : PT.specification Location.loced list;
  10. gr_specfuns : PT.specfun Location.loced list;
  11. gr_specvars : (PT.lident * PT.label_exprs) Location.loced list;
  12. gr_specassets : (PT.lident * PT.label_exprs) Location.loced list;
  13. 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. | `ThePkForAggregate
  5. | `Asset
  6. | `Coll
  7. | `SubColl
  8. | `PkOrAsset
  9. | `Cmp
  10. | `Pred of bool
  11. | `RExpr of bool
  12. | `Ef of bool
  13. | `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 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 sapling_ops : opinfo list
val bls_ops : opinfo list
val timelock_ops : opinfo list
val allops : opinfo list
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 : bool;
  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 show_assetdecl : assetdecl -> Ppx_deriving_runtime.string
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 show_recorddecl : recorddecl -> Ppx_deriving_runtime.string
val show_rfielddecl : rfielddecl -> Ppx_deriving_runtime.string
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;
  4. ad_callby : A.pterm option Location.loced list;
  5. ad_stateis : A.lident option;
  6. ad_effect : [ `Raw of A.instruction | `Tx of transition ] option;
  7. ad_funs : 'env fundecl option list;
  8. ad_reqs : (A.lident option * A.pterm * A.pterm option) list;
  9. ad_fais : (A.lident option * A.pterm * A.pterm option) list;
  10. ad_spec : 'env ispecification list;
  11. ad_actfs : bool;
}
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
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 imode_t = [
  1. | `Ghost
  2. | `Concrete
]
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 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_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_properties : (env * env) -> PT.entry_properties -> env * (PT.lident A.term_node A.struct_poly option Location.loced list option * PT.lident A.term_node A.struct_poly option Location.loced list option * Ident.ident Location.loced 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 = {
  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 : bool;
  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 : 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 = {
  1. state : statedecl option;
  2. variables : vardecl option list;
  3. enums : statedecl option list;
  4. records : recorddecl option list;
  5. assets : assetdecl option list;
  6. functions : env fundecl option list;
  7. acttxs : env tentrydecl option list;
  8. specs : env ispecification list list;
  9. 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 * bool) 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
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