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. | Enotfound
  2. | Ekeyexist
  3. | Enegassignnat
  4. | Einvalidcaller
  5. | Einvalidcondition
  6. | Einvalidstate
  7. | Enotransfer
  8. | Ebreak
  9. | Einvalid of string option
  10. | Efail of int * 'e option
type ('i, 't) abstract_type =
  1. | Tyint
  2. | Tyuint
  3. | Tybool
  4. | Tystring
  5. | Tyrational
  6. | Tyaddr
  7. | Tyrole
  8. | Tykey
  9. | Tykeyhash
  10. | Tydate
  11. | Tyduration
  12. | Tytez
  13. | Tysignature
  14. | Tybytes
  15. | Tychainid
  16. | Tystorage
  17. | Tyoperation
  18. | Tycontract
  19. | Tyunit
  20. | Tyrecord of 'i
  21. | Tycoll of 'i
  22. | Tyview of 'i
  23. | Tymap of 'i
  24. | Tyasset of 'i
  25. | Typartition of 'i
  26. | Tyaggregate of 'i
  27. | Tystate
  28. | Tyenum of 'i
  29. | Tyoption of 't
  30. | Tyset of 'i
  31. | Tylist of 't
  32. | Tytuple of 't list
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
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. | Tapp of 'e * 'e list
  8. | Tfor of 'i * 'e * 'e * ('e, 'i) abstract_formula list * 'e
  9. | Twhile of 'e * ('e, 'i) abstract_formula list * 'e
  10. | Ttry of 'e * ('e exn * 'e) list
  11. | Tvar of 'i
  12. | Ttuple of 'e list
  13. | Ttupleaccess of 'e * int * int
  14. | Trecord of 'e option * ('i * 'e) list
  15. | Tdot of 'e * 'e
  16. | Tdoti of 'i * 'i
  17. | Tename
  18. | Tcaller of 'i
  19. | Tsender of 'i
  20. | Ttransferred of 'i
  21. | Tnow of 'i
  22. | Tadded of 'i
  23. | Trmed of 'i
  24. | Tchainid of 'i
  25. | Tselfaddress of 'i
  26. | Tdefaultaddr
  27. | Temptystr
  28. | Tlist of 'e list
  29. | Tnil of 'i
  30. | Temptycoll of 'i
  31. | Temptyview of 'i
  32. | Temptyfield of 'i
  33. | Tcard of 'i * 'e
  34. | Tfromfield of 'i * 'e * 'e
  35. | Tfromview of 'i * 'e * 'e
  36. | Ttoview of 'i * 'e
  37. | Tviewtolist of 'i * 'e * 'e
  38. | Telts of 'i * 'e
  39. | Tshallow of 'i * 'e * 'e
  40. | Tmlist of 'i * 'e * 'i * 'i * 'i * 'e
  41. | Tcons of 'i * 'e * 'e
  42. | Tprepend of 'i * 'e * 'e
  43. | Tmkcoll of 'i * 'e list
  44. | Tmkview of 'i * 'e
  45. | Tcontent of 'i * 'e
  46. | Tcontains of 'i * 'e * 'e
  47. | Tvcontent of 'i * 'e
  48. | Tadd of 'i * 'e * 'e
  49. | Tvadd of 'i * 'e * 'e
  50. | Tremove of 'i * 'e * 'e
  51. | Tvremove of 'i * 'e * 'e
  52. | Tget of 'i * 'e * 'e
  53. | Tgetforce of 'i * 'e * 'e
  54. | Tfget of 'i * 'e * 'e
  55. | Tset of 'i * 'e * 'e * 'e
  56. | Tvsum of 'i * 'e * 'e
  57. | Tcsum of 'i * 'e
  58. | Tcsort of 'i * 'e
  59. | Tvsort of 'i * 'e * 'e
  60. | Tnth of 'i * 'e * 'e
  61. | Tnthtuple of int * int * 'e
  62. | Tcoll of 'i * 'e
  63. | Tassign of 'e * 'e
  64. | Traise of 'e exn
  65. | Texn of 'e exn
  66. | Tconcat of 'e * 'e
  67. | Ttransfer of 'e * 'e
  68. | Tcall of 'e * 'e * 'i * 'e
  69. | Tmkoperation of 'e * 'e * 'e
  70. | Tentrypoint of 'i * 'e
  71. | Tfst of 'e
  72. | Tsnd of 'e
  73. | Tsndopt of 'e
  74. | Tabs of 'e
  75. | Tmktr of 'e * 'e
  76. | Ttradd of 'i
  77. | Ttrrm of 'i
  78. | Tplus of 't * 'e * 'e
  79. | Tminus of 't * 'e * 'e
  80. | Tuminus of 't * 'e
  81. | Tmult of 't * 'e * 'e
  82. | Tdiv of 't * 'e * 'e
  83. | Tmod of 't * 'e * 'e
  84. | Tnot of 'e
  85. | Tpand of 'e * 'e
  86. | Teq of 't * 'e * 'e
  87. | Teqfield of 'i * 'e * 'e
  88. | Tneq of 't * 'e * 'e
  89. | Tlt of 't * 'e * 'e
  90. | Tle of 't * 'e * 'e
  91. | Tgt of 't * 'e * 'e
  92. | Tge of 't * 'e * 'e
  93. | Tdlt of 't * 'e * 'e * 'e
  94. | Tdle of 't * 'e * 'e * 'e
  95. | Tdlet of 't * 'e * 'e * 'e
  96. | Tdlte of 't * 'e * 'e * 'e
  97. | Tint of Core.big_int
  98. | Tstring of string
  99. | Taddr of string
  100. | Tbytes of string
  101. | Tforall of ('t, 'i) abstract_univ_decl list * 'e
  102. | Texists of ('t, 'i) abstract_univ_decl list * 'e
  103. | Tresult
  104. | Timpl of 'e * 'e
  105. | Tequiv of 'e * 'e
  106. | Tand of 'e * 'e
  107. | Tor of 'e * 'e
  108. | Txor of 't * 'e * 'e
  109. | Told of 'e
  110. | Tfalse
  111. | Ttrue
  112. | Tunion of 'i * 'e * 'e
  113. | Tinter of 'i * 'e * 'e
  114. | Tdiff of 'i * 'e * 'e
  115. | Tsubset of 'i * 'e * 'e
  116. | Tassert of 'i option * 'e
  117. | Tmem of 'i * 'e * 'e
  118. | Tvmem of 'i * 'e * 'e
  119. | Tlmem of 'i * 'e * 'e
  120. | Tccontains of 'i * 'e * 'e
  121. | Tvcontains of 'i * 'e * 'e
  122. | Tempty of 'i * 'e
  123. | Tvempty of 'i * 'e
  124. | Tsingl of 'i * 'e
  125. | Tchead of 'i * 'e * 'e
  126. | Tvhead of 'i * 'e * 'e
  127. | Tctail of 'i * 'e * 'e
  128. | Tvtail of 'i * 'e * 'e
  129. | Tcnth of 'i * 'e * 'e
  130. | Tvnth of 'i * 'e * 'e
  131. | Tlnth of 'i * 'e * 'e
  132. | Tselect of 'i * 'e * 'e
  133. | Tcselect of 'i * 'i * 'e list * 'e
  134. | Tvselect of 'i * 'i * 'e list * 'e * 'e
  135. | Tremoveif of 'i * 'i * 'e list * 'e
  136. | Tpremoveif of 'i * 'i * 'e list * 'e * 'e
  137. | Tfremoveif of 'i * 'i * 'e list * 'e * 'e * 'e
  138. | Tunionpred of 'i * 'i * 'e list * 'e
  139. | Twitness of 'i
  140. | Tnone
  141. | Tsome of 'e
  142. | Tenum of 'i
  143. | Tmark of 'i * 'e
  144. | Tat of 'i * 'e
  145. | Tunit
  146. | Ttobereplaced
  147. | 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 : ('i option * 'e) list;
  7. variants : 'e list;
  8. requires : ('e, 'i) abstract_formula list;
  9. ensures : ('e, 'i) abstract_formula list;
  10. body : 'e;
}
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_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 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