package archetype

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

Innovation. Community. Security.