package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Archetype.MlwtreeSource

Sourcetype fmod =
  1. | LogicOnly
  2. | Logic
  3. | Rec
  4. | NoMod
Sourcetype '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
Sourcetype ('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
Sourcetype ('t, 'i) abstract_univ_decl = 'i list * 't
Sourcetype 'i pattern_node =
  1. | Twild
  2. | Tpignore
  3. | Tconst of 'i
  4. | Tpatt_tuple of 'i pattern_node list
  5. | Tpsome of 'i
Sourcetype ('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
Sourceand ('e, 'i) abstract_formula = {
  1. id : 'i;
  2. form : 'e;
}
Sourceand ('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;
}
Sourcetype ('e, 't, 'i) abstract_field = {
  1. name : 'i;
  2. typ : 't;
  3. init : 'e;
  4. mutable_ : bool;
}
Sourcetype ('e, 't, 'i) abstract_storage_struct = {
  1. fields : ('e, 't, 'i) abstract_field list;
  2. invariants : ('e, 'i) abstract_formula list;
}
Sourcetype ('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
Sourcetype theotyp =
  1. | Theo
  2. | Axiom
  3. | Lemma
  4. | Goal
Sourcetype ('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
Sourcetype ('e, 't, 'i) abstract_module = {
  1. name : 'i;
  2. decls : ('e, 't, 'i) abstract_decl list;
}
Sourcetype ('e, 't, 'i) abstract_mlw_tree = ('e, 't, 'i) abstract_module list
Sourceval map_abstract_qualid : ('i1 -> 'i2) -> 'i1 list -> 'i2 list
Sourceval map_abstract_type : ('i1 -> 'i2) -> ('t1 -> 't2) -> ('i1, 't1) abstract_type -> ('i2, 't2) abstract_type
Sourceval map_abstract_univ_decl : ('t1 -> 't2) -> ('i1 -> 'i2) -> ('t1, 'i1) abstract_univ_decl -> ('t2, 'i2) abstract_univ_decl
Sourceval map_pattern : ('a -> 'b) -> 'a pattern_node -> 'b pattern_node
Sourceval map_abstract_formula : ('e1 -> 'e2) -> ('i1 -> 'i2) -> ('e1, 'i1) abstract_formula -> ('e2, 'i2) abstract_formula
Sourceval map_abstract_fun_struct : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_fun_struct -> ('e2, 't2, 'i2) abstract_fun_struct
Sourceval map_exn : ('e1 -> 'e2) -> 'e1 exn -> 'e2 exn
Sourceval map_abstract_term : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_term -> ('e2, 't2, 'i2) abstract_term
Sourceval map_abstract_field : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_field -> ('e2, 't2, 'i2) abstract_field
Sourceval map_abstract_storage_struct : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_storage_struct -> ('e2, 't2, 'i2) abstract_storage_struct
Sourceval map_abstract_clone_subst : ('i1 -> 'i2) -> ('t1 -> 't2) -> ('i1, 't1) abstract_clone_subst -> ('i2, 't2) abstract_clone_subst
Sourceval map_abstract_decl : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_decl -> ('e2, 't2, 'i2) abstract_decl
Sourceval map_abstract_module : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_module -> ('e2, 't2, 'i2) abstract_module
Sourceval map_abstract_mlw_tree : ('e1 -> 'e2) -> ('t1 -> 't2) -> ('i1 -> 'i2) -> ('e1, 't1, 'i1) abstract_mlw_tree -> ('e2, 't2, 'i2) abstract_module list
Sourcetype ident = string
Sourcetype qualid = ident list
Sourcetype univ_decl = (typ, ident) abstract_univ_decl
Sourcetype fun_struct = (term, typ, ident) abstract_fun_struct
Sourcetype storage_struct = (term, typ, ident) abstract_storage_struct
Sourcetype clone_subst = (ident, typ) abstract_clone_subst
Sourcetype mlw_module = (term, typ, ident) abstract_module
Sourcetype 'o with_loc = {
  1. obj : 'o;
  2. loc : Location.t;
}
Sourcetype loc_ident = string with_loc
Sourcetype loc_qualid = loc_ident list with_loc
Sourceval show_loc_storage_struct : loc_storage_struct -> Ppx_deriving_runtime.string
Sourceval unloc_tree : loc_mlw_tree -> mlw_tree
Sourceval unloc_term : loc_term -> term
Sourceval unloc_type : loc_typ -> typ
Sourceval unloc_ident : loc_ident -> ident
Sourceval unloc_decl : loc_decl -> (term, typ, ident) abstract_decl
Sourceval with_dummy_loc : 'a -> 'a with_loc
Sourceval mk_loc : Location.t -> 'a -> 'a with_loc
Sourceval loc_tree : mlw_tree -> loc_mlw_tree
Sourceval loc_term : term -> loc_term
Sourceval loc_type : typ -> loc_typ
Sourceval loc_ident : ident -> loc_ident
Sourceval deloc : 'a with_loc -> 'a
Sourceval compare_fmod : fmod -> fmod -> bool
Sourceval compare_abstract_type : ('i -> 'i -> bool) -> ('t -> 't -> bool) -> ('i, 't) abstract_type -> ('i, 't) abstract_type -> bool
Sourceval compare_abstract_formula : ('e -> 'e -> bool) -> ('i -> 'i -> bool) -> ('e, 'i) abstract_formula -> ('e, 'i) abstract_formula -> bool
Sourceval 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
Sourceval compare_pattern : ('a -> 'b -> bool) -> 'a pattern_node -> 'b pattern_node -> bool
Sourceval compare_abstract_term : ('e -> 'e -> bool) -> ('t -> 't -> bool) -> ('i -> 'i -> bool) -> ('e, 't, 'i) abstract_term -> ('e, 't, 'i) abstract_term -> bool
Sourceval compare_exn : ('e -> 'e -> bool) -> 'e exn -> 'e exn -> bool
Sourceval cmp_loc_ident : loc_ident -> loc_ident -> bool
Sourceval cmp_loc_type : loc_typ -> loc_typ -> bool
Sourceval cmp_loc_term : loc_term -> loc_term -> bool
Sourceval cmp_ident : ident -> ident -> bool
Sourceval cmp_type : typ -> typ -> bool
Sourceval cmp_term : term -> term -> bool
Sourceval id : 'a -> 'a
Sourceval loc_replace : loc_term -> (('a, loc_typ, loc_ident) abstract_term with_loc as 'a) -> loc_term -> 'a
Sourceval replace : term -> (('a, typ, ident) abstract_term as 'a) -> term -> 'a