package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
type fmod =
  1. | LogicOnly
  2. | Logic
  3. | Rec
  4. | NoMod
type 'e exn =
  1. | Einvalid of string option
  2. | Efail of int * 'e option
  3. | EInvalidCaller
  4. | EInvalidCondition of string
  5. | ENotFound
  6. | EOutOfBound
  7. | EKeyExists
  8. | EKeyExistsOrNotFound
  9. | EDivByZero
  10. | ENatAssign
  11. | ENoTransfer
  12. | EInvalidState
type ('i, 't) abstract_type =
  1. | Tyint
  2. | Tyuint
  3. | Tybool
  4. | Tystring
  5. | Tyrational
  6. | Tyaddr
  7. | Tykey
  8. | Tykeyhash
  9. | Tydate
  10. | Tyduration
  11. | Tytez
  12. | Tysignature
  13. | Tybytes
  14. | Tychainid
  15. | Tystorage
  16. | Tyoperation
  17. | Tycontract
  18. | Tyunit
  19. | Tyrecord of 'i
  20. | Tycoll of 'i
  21. | Tyview of 'i
  22. | Tymap of 'i
  23. | Tyasset of 'i
  24. | Typartition of 'i
  25. | Tyaggregate of 'i
  26. | Tystate
  27. | Tyenum of 'i
  28. | Tyoption of 't
  29. | Tyset of 'i
  30. | Tylist of 't
  31. | Tytuple of 't list
  32. | Tyor of 't * 't
  33. | Tylambda of 't * 't
  34. | Tybls12_381_fr
  35. | Tybls12_381_g1
  36. | Tybls12_381_g2
  37. | Tynever
type ('t, 'i) abstract_univ_decl = 'i list * 't
type 'i pattern_node =
  1. | Twild
  2. | Tpignore
  3. | Tconst of 'i
  4. | Tpatt_tuple of 'i pattern_node list
  5. | Tpsome of 'i
  6. | Tpleft of 'i
  7. | Tpright of 'i
type ('e, 't, 'i) abstract_term =
  1. | Tseq of 'e list
  2. | Tletin of bool * 'i * 't option * 'e * 'e
  3. | Tletfun of ('e, 't, 'i) abstract_fun_struct * 'e
  4. | Tlambda of 'i list * 'e
  5. | Tif of 'e * 'e * 'e option
  6. | Tmatch of 'e * ('i pattern_node * 'e) list
  7. | Tmatchoption of 'e * 'i * 'e * 'e
  8. | Tmatchor of 'e * 'i * 'e * 'i * 'e
  9. | Tmatchlist of 'e * 'i * 'i * 'e * 'e
  10. | Tapp of 'e * 'e list
  11. | Tfor of 'i * 'e * 'e * ('e, 'i) abstract_formula list * 'e
  12. | Twhile of 'e * ('e, 'i) abstract_formula list * 'e
  13. | Ttry of 'e * ('e exn * 'e) list
  14. | Tvar of 'i
  15. | Ttuple of 'e list
  16. | Ttupleaccess of 'e * int * int
  17. | Tvlambda of 't * 'i * 't * 'e
  18. | Texeclambda of 'e * 'e
  19. | Tapplylambda of 'e * 'e
  20. | Trecord of 'e option * ('i * 'e) list
  21. | Tdot of 'e * 'e
  22. | Tdoti of 'i * 'i
  23. | Tename
  24. | Tcaller of 'i
  25. | Tsender of 'i
  26. | Ttransferred of 'i
  27. | Tnow of 'i
  28. | Tadded of 'i
  29. | Trmed of 'i
  30. | Tchainid of 'i
  31. | Tselfaddress of 'i
  32. | Tdefaultaddr
  33. | Temptystr
  34. | Tlist of 'e list
  35. | Tnil of 'i
  36. | Temptycoll of 'i
  37. | Temptyview of 'i
  38. | Temptyfield of 'i
  39. | Tcard of 'i * 'e
  40. | Tfromfield of 'i * 'e * 'e
  41. | Tfromview of 'i * 'e * 'e
  42. | Ttoview of 'i * 'e
  43. | Tviewtolist of 'i * 'e * 'e
  44. | Telts of 'i * 'e
  45. | Tshallow of 'i * 'e * 'e
  46. | Tmlist of 'i * 'e * 'i * 'i * 'i * 'e
  47. | Tcons of 'i * 'e * 'e
  48. | Tprepend of 'i * 'e * 'e
  49. | Tmkcoll of 'i * 'e list
  50. | Tmkview of 'i * 'e
  51. | Tcontent of 'i * 'e
  52. | Tcontains of 'i * 'e * 'e
  53. | Tvcontent of 'i * 'e
  54. | Tlistreverse of 'i * 'e
  55. | Tlistconcat of 'i * 'e * 'e
  56. | Tlistmap of 'i * 'e * 'i * 'e
  57. | Tfold of 'e * 'i * 'e
  58. | Tadd of 'i * 'e * 'e
  59. | Tvadd of 'i * 'e * 'e
  60. | Tremove of 'i * 'e * 'e
  61. | Tvremove of 'i * 'e * 'e
  62. | Tupdate of 'i * 'e * 'e * 'e
  63. | Tget of 'i * 'e * 'e
  64. | Tgetforce of 'i * 'e * 'e
  65. | Tfget of 'i * 'e * 'e
  66. | Tset of 'i * 'e * 'e * 'e
  67. | Tvsum of 'i * 'e * 'e
  68. | Tcsum of 'i * 'e
  69. | Tcsort of 'i * 'e
  70. | Tvsort of 'i * 'e * 'e
  71. | Tnth of 'i * 'e * 'e
  72. | Tnthtuple of int * int * 'e
  73. | Tcoll of 'i * 'e
  74. | Tassign of 'e * 'e
  75. | Traise of 'e exn
  76. | Texn of 'e exn
  77. | Tconcat of 'e * 'e
  78. | Ttransfer of 'e * 'e
  79. | Tcall of 'e * 'e * 'i * 'e
  80. | Tmkoperation of 'e * 'e * 'e
  81. | Tentrypoint of 'i * 'e
  82. | Tfst of 'e
  83. | Tsnd of 'e
  84. | Tsndopt of 'e
  85. | Tabs of 'e
  86. | Tmktr of 'e * 'e
  87. | Ttradd of 'i
  88. | Ttrrm of 'i
  89. | Tplus of 't * 'e * 'e
  90. | Tminus of 't * 'e * 'e
  91. | Tuminus of 't * 'e
  92. | Tmult of 't * 'e * 'e
  93. | Tdiv of 't * 'e * 'e
  94. | Tmod of 't * 'e * 'e
  95. | Tdivmod of 't * 'e * 'e
  96. | Tthreewaycmp of 't * 'e * 'e
  97. | Tshiftleft of 'e * 'e
  98. | Tshiftright of 'e * 'e
  99. | Tnot of 'e
  100. | Tpand of 'e * 'e
  101. | Teq of 't * 'e * 'e
  102. | Teqfield of 'i * 'e * 'e
  103. | Tneq of 't * 'e * 'e
  104. | Tlt of 't * 'e * 'e
  105. | Tle of 't * 'e * 'e
  106. | Tgt of 't * 'e * 'e
  107. | Tge of 't * 'e * 'e
  108. | Tdlt of 't * 'e * 'e * 'e
  109. | Tdle of 't * 'e * 'e * 'e
  110. | Tdlet of 't * 'e * 'e * 'e
  111. | Tdlte of 't * 'e * 'e * 'e
  112. | Tint of Core.big_int
  113. | Tstring of string
  114. | Taddr of string
  115. | Tbytes of string
  116. | Tforall of ('t, 'i) abstract_univ_decl list * 'e
  117. | Texists of ('t, 'i) abstract_univ_decl list * 'e
  118. | Tresult
  119. | Timpl of 'e * 'e
  120. | Tequiv of 'e * 'e
  121. | Tand of 'e * 'e
  122. | Tor of 'e * 'e
  123. | Txor of 't * 'e * 'e
  124. | Told of 'e
  125. | Tfalse
  126. | Ttrue
  127. | Tunion of 'i * 'e * 'e
  128. | Tinter of 'i * 'e * 'e
  129. | Tdiff of 'i * 'e * 'e
  130. | Tsubset of 'i * 'e * 'e
  131. | Tassert of 'i option * 'e
  132. | Tmem of 'i * 'e * 'e
  133. | Tvmem of 'i * 'e * 'e
  134. | Tlmem of 'i * 'e * 'e
  135. | Tccontains of 'i * 'e * 'e
  136. | Tvcontains of 'i * 'e * 'e
  137. | Tempty of 'i * 'e
  138. | Tvempty of 'i * 'e
  139. | Tsingl of 'i * 'e
  140. | Tchead of 'i * 'e * 'e
  141. | Tvhead of 'i * 'e * 'e
  142. | Tctail of 'i * 'e * 'e
  143. | Tvtail of 'i * 'e * 'e
  144. | Tcnth of 'i * 'e * 'e
  145. | Tvnth of 'i * 'e * 'e
  146. | Tlnth of 'i * 'e * 'e
  147. | Tselect of 'i * 'e * 'e
  148. | Tcselect of 'i * 'i * 'e list * 'e
  149. | Tvselect of 'i * 'i * 'e list * 'e * 'e
  150. | Tremoveif of 'i * 'i * 'e list * 'e
  151. | Tpremoveif of 'i * 'i * 'e list * 'e * 'e
  152. | Tfremoveif of 'i * 'i * 'e list * 'e * 'e * 'e
  153. | Tunionpred of 'i * 'i * 'e list * 'e
  154. | Twitness of 'i
  155. | Tnone
  156. | Tsome of 'e
  157. | Tleft of 't * 'e
  158. | Tright of 't * 'e
  159. | Tenum of 'i
  160. | Tmark of 'i * 'e
  161. | Tat of 'i * 'e
  162. | Tunit
  163. | Ttobereplaced
  164. | Tnottranslated
and ('e, 'i) abstract_formula = {
  1. id : 'i;
  2. form : 'e;
}
and ('e, 't, 'i) abstract_fun_struct = {
  1. name : 'i;
  2. logic : fmod;
  3. args : ('i * 't) list;
  4. returns : 't;
  5. raises : 'e list;
  6. fails : ('e, 'i) abstract_struct_fail list;
  7. variants : 'e list;
  8. requires : ('e, 'i) abstract_formula list;
  9. ensures : ('e, 'i) abstract_formula list;
  10. body : 'e;
}
and ('e, 'i) abstract_struct_fail = {
  1. fid : 'e;
  2. expl : 'i option;
  3. expr : 'e option;
}
type ('e, 't, 'i) abstract_field = {
  1. name : 'i;
  2. typ : 't;
  3. init : 'e;
  4. mutable_ : bool;
}
type ('e, 't, 'i) abstract_storage_struct = {
  1. fields : ('e, 't, 'i) abstract_field list;
  2. invariants : ('e, 'i) abstract_formula list;
}
type ('i, 't) abstract_clone_subst =
  1. | Ctype of 'i * 't
  2. | Cval of 'i * 'i
  3. | Cfun of 'i * 'i
  4. | Cpred of 'i * 'i
type theotyp =
  1. | Theo
  2. | Axiom
  3. | Lemma
  4. | Goal
val show_theotyp : theotyp -> Ppx_deriving_runtime.string
type ('e, 't, 'i) abstract_decl =
  1. | Duse of bool * 'i list * string option
  2. | Dval of bool * 'i * 't
  3. | Dclone of 'i list * 'i * ('i, 't) abstract_clone_subst list
  4. | Denum of 'i * 'i list
  5. | Drecord of 'i * ('e, 't, 'i) abstract_field list
  6. | Dstorage of ('e, 't, 'i) abstract_storage_struct
  7. | Dtheorem of theotyp * 'i * 'e
  8. | Dfun of ('e, 't, 'i) abstract_fun_struct
  9. | Dexn of 'i * 't
  10. | Dpred of 'i * ('i * 't) list * 'e
type ('e, 't, 'i) abstract_module = {
  1. name : 'i;
  2. decls : ('e, 't, 'i) abstract_decl list;
}
type ('e, 't, 'i) abstract_mlw_tree = ('e, 't, 'i) abstract_module list
val map_abstract_qualid : ('i1 -> 'i2) -> 'i1 list -> 'i2 list
val map_abstract_type : ('i1 -> 'i2) -> ('t1 -> 't2) -> ('i1, 't1) abstract_type -> ('i2, 't2) abstract_type
val map_abstract_univ_decl : ('t1 -> 't2) -> ('i1 -> 'i2) -> ('t1, 'i1) abstract_univ_decl -> ('t2, 'i2) abstract_univ_decl
val map_pattern : ('a -> 'b) -> 'a pattern_node -> 'b pattern_node
val map_abstract_formula : ('e1 -> 'e2) -> ('i1 -> 'i2) -> ('e1, 'i1) abstract_formula -> ('e2, 'i2) abstract_formula
val map_abstract_fun_struct : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_fun_struct -> ('e2, 't2, 'i2) abstract_fun_struct
val map_abstract_struct_fail : ('e1 -> 'e2) -> ('i1 -> 'i2) -> ('e1, 'i1) abstract_struct_fail -> ('e2, 'i2) abstract_struct_fail
val map_exn : ('e1 -> 'e2) -> 'e1 exn -> 'e2 exn
val map_abstract_term : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_term -> ('e2, 't2, 'i2) abstract_term
val map_abstract_field : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_field -> ('e2, 't2, 'i2) abstract_field
val map_abstract_storage_struct : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_storage_struct -> ('e2, 't2, 'i2) abstract_storage_struct
val map_abstract_clone_subst : ('i1 -> 'i2) -> ('t1 -> 't2) -> ('i1, 't1) abstract_clone_subst -> ('i2, 't2) abstract_clone_subst
val map_abstract_decl : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_decl -> ('e2, 't2, 'i2) abstract_decl
val map_abstract_module : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_module -> ('e2, 't2, 'i2) abstract_module
val map_abstract_mlw_tree : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_mlw_tree -> ('e2, 't2, 'i2) abstract_module list
type ident = string
type qualid = ident list
val show_qualid : qualid -> Ppx_deriving_runtime.string
type typ = (ident, typ) abstract_type
type univ_decl = (typ, ident) abstract_univ_decl
val show_univ_decl : univ_decl -> Ppx_deriving_runtime.string
type term = (term, typ, ident) abstract_term
type formula = (term, ident) abstract_formula
val show_formula : formula -> Ppx_deriving_runtime.string
type field = (term, typ, ident) abstract_field
type fun_struct = (term, typ, ident) abstract_fun_struct
val show_fun_struct : fun_struct -> Ppx_deriving_runtime.string
type storage_struct = (term, typ, ident) abstract_storage_struct
val show_storage_struct : storage_struct -> Ppx_deriving_runtime.string
type clone_subst = (ident, typ) abstract_clone_subst
val show_clone_subst : clone_subst -> Ppx_deriving_runtime.string
type decl = (term, typ, ident) abstract_decl
type mlw_module = (term, typ, ident) abstract_module
val show_mlw_module : mlw_module -> Ppx_deriving_runtime.string
type mlw_tree = (term, typ, ident) abstract_mlw_tree
val show_mlw_tree : mlw_tree -> Ppx_deriving_runtime.string
type 'o with_loc = {
  1. obj : 'o;
  2. loc : Location.t;
}
type loc_ident = string with_loc
val show_loc_ident : loc_ident -> Ppx_deriving_runtime.string
type loc_qualid = loc_ident list with_loc
val show_loc_qualid : loc_qualid -> Ppx_deriving_runtime.string
val show_loc_typ : loc_typ -> Ppx_deriving_runtime.string
val show_loc_univ_decl : loc_univ_decl -> Ppx_deriving_runtime.string
val show_loc_term : loc_term -> Ppx_deriving_runtime.string
val show_loc_formula : loc_formula -> Ppx_deriving_runtime.string
val show_loc_field : loc_field -> Ppx_deriving_runtime.string
val show_loc_fun_struct : loc_fun_struct -> Ppx_deriving_runtime.string
val show_loc_storage_struct : loc_storage_struct -> Ppx_deriving_runtime.string
val show_loc_clone_subst : loc_clone_subst -> Ppx_deriving_runtime.string
val show_loc_decl : loc_decl -> Ppx_deriving_runtime.string
type loc_mlw_module = (loc_term, loc_typ, loc_ident) abstract_module
val show_loc_mlw_module : loc_mlw_module -> Ppx_deriving_runtime.string
val show_loc_mlw_tree : loc_mlw_tree -> Ppx_deriving_runtime.string
val mk_struct_fail : ?expl:loc_ident -> ?expr:loc_term -> loc_term -> struct_fail
val unloc_tree : loc_mlw_tree -> mlw_tree
val unloc_term : loc_term -> term
val unloc_type : loc_typ -> typ
val unloc_ident : loc_ident -> ident
val unloc_decl : loc_decl -> (term, typ, ident) abstract_decl
val with_dummy_loc : 'a -> 'a with_loc
val mk_loc : Location.t -> 'a -> 'a with_loc
val loc_tree : mlw_tree -> loc_mlw_tree
val loc_term : term -> loc_term
val loc_type : typ -> loc_typ
val loc_ident : ident -> loc_ident
val deloc : 'a with_loc -> 'a
val compare_fmod : fmod -> fmod -> bool
val compare_abstract_type : ('i -> 'i -> bool) -> ('t -> 't -> bool) -> ('i, 't) abstract_type -> ('i, 't) abstract_type -> bool
val compare_abstract_formula : ('e -> 'e -> bool) -> ('i -> 'i -> bool) -> ('e, 'i) abstract_formula -> ('e, 'i) abstract_formula -> bool
val compare_abstract_fun_struct : ('e -> 'e -> bool) -> ('t -> 't -> bool) -> ('i -> 'i -> bool) -> ('e, 't, 'i) abstract_fun_struct -> ('e, 't, 'i) abstract_fun_struct -> bool
val compare_pattern : ('a -> 'b -> bool) -> 'a pattern_node -> 'b pattern_node -> bool
val compare_abstract_term : ('e -> 'e -> bool) -> ('t -> 't -> bool) -> ('i -> 'i -> bool) -> ('e, 't, 'i) abstract_term -> ('e, 't, 'i) abstract_term -> bool
val compare_exn : ('e -> 'e -> bool) -> 'e exn -> 'e exn -> bool
val cmp_loc_ident : loc_ident -> loc_ident -> bool
val cmp_loc_type : loc_typ -> loc_typ -> bool
val cmp_loc_term : loc_term -> loc_term -> bool
val cmp_ident : ident -> ident -> bool
val cmp_type : typ -> typ -> bool
val cmp_term : term -> term -> bool
val id : 'a -> 'a
val loc_replace : loc_term -> ('a, loc_typ, loc_ident) abstract_term with_loc as 'a -> loc_term -> 'a
val replace : term -> ('a, typ, ident) abstract_term as 'a -> term -> 'a
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