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