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. | EInvalidSource
  5. | EInvalidCondition of string
  6. | ENotFound
  7. | EKeyExists
  8. | EKeyExistsOrNotFound
  9. | EDivByZero
  10. | ENatNegAssign
  11. | ENoTransfer
  12. | EInvalidState
type ('i, 't) abstract_type =
  1. | Tyint
  2. | Tyuint
  3. | Tybool
  4. | Tystring
  5. | Tyrational
  6. | Tyaddr
  7. | Tytx_rollup_l2_address
  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
  33. | Tyor of 't * 't
  34. | Tylambda of 't * 't
  35. | Tybls12_381_fr
  36. | Tybls12_381_g1
  37. | Tybls12_381_g2
  38. | Tynever
  39. | Tychest
  40. | Tychest_key
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) -> 'i10 list -> 'i20 list
val map_abstract_type : ('i1 -> 'i2) -> ('t1 -> 't2) -> ('i10, 't10) abstract_type -> ('i20, 't20) abstract_type
val map_abstract_univ_decl : ('t1 -> 't2) -> ('i1 -> 'i2) -> ('t10, 'i10) abstract_univ_decl -> ('t20, 'i20) abstract_univ_decl
val map_pattern : ('a -> 'b) -> 'c pattern_node -> 'd pattern_node
val map_abstract_formula : ('e1 -> 'e2) -> ('i1 -> 'i2) -> ('e10, 'i10) abstract_formula -> ('e20, 'i20) abstract_formula
val map_abstract_fun_struct : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_fun_struct -> ('e20, 't20, 'i20) abstract_fun_struct
val map_abstract_struct_fail : ('e1 -> 'e2) -> ('i1 -> 'i2) -> ('e10, 'i10) abstract_struct_fail -> ('e20, 'i20) abstract_struct_fail
val map_exn : ('e1 -> 'e2) -> 'e10 exn -> 'e20 exn
val map_abstract_term : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_term -> ('e20, 't20, 'i20) abstract_term
val map_abstract_field : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_field -> ('e20, 't20, 'i20) abstract_field
val map_abstract_storage_struct : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_storage_struct -> ('e20, 't20, 'i20) abstract_storage_struct
val map_abstract_clone_subst : ('i1 -> 'i2) -> ('t1 -> 't2) -> ('i10, 't10) abstract_clone_subst -> ('i20, 't20) abstract_clone_subst
val map_abstract_decl : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_decl -> ('e20, 't20, 'i20) abstract_decl
val map_abstract_module : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_module -> ('e20, 't20, 'i20) abstract_module
val map_abstract_mlw_tree : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e10, 't10, 'i10) abstract_mlw_tree -> ('e20, 't20, 'i20) 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 -> 'b with_loc
val mk_loc : Location.t -> 'a -> 'b 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 -> 'b
val compare_fmod : fmod -> fmod -> bool
val compare_abstract_type : ('i -> 'i -> bool) -> ('t -> 't -> bool) -> ('i0, 't0) abstract_type -> ('i1, 't1) abstract_type -> bool
val compare_abstract_formula : ('e -> 'e -> bool) -> ('i -> 'i -> bool) -> ('e0, 'i0) abstract_formula -> ('e1, 'i1) abstract_formula -> bool
val compare_abstract_fun_struct : ('e -> 'e -> bool) -> ('t -> 't -> bool) -> ('i -> 'i -> bool) -> ('e0, 't0, 'i0) abstract_fun_struct -> ('e1, 't1, 'i1) abstract_fun_struct -> bool
val compare_pattern : ('a -> 'b -> bool) -> 'c pattern_node -> 'd pattern_node -> bool
val compare_abstract_term : ('e -> 'e -> bool) -> ('t -> 't -> bool) -> ('i -> 'i -> bool) -> ('e0, 't0, 'i0) abstract_term -> ('e1, 't1, 'i1) abstract_term -> bool
val compare_exn : ('e -> 'e -> bool) -> 'e0 exn -> 'e1 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 -> 'b
val loc_replace : loc_term -> ('a with_loc as 'b, loc_typ, loc_ident) abstract_term as 'a with_loc -> loc_term -> 'b
val replace : term -> (('a, typ, ident) abstract_term as 'a, typ, ident) abstract_term -> term -> 'a