package archetype

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

Module Archetype.MlwtreeSource

Sourcetype exn =
  1. | Enotfound
  2. | Ekeyexist
  3. | Einvalidcaller
  4. | Einvalidcondition
  5. | Einvalidstate
  6. | Enotransfer
  7. | Ebreak
Sourcetype fmod =
  1. | Logic
  2. | Rec
  3. | NoMod
Sourcetype 'i abstract_qualid = 'i list
Sourcetype 'i abstract_type =
  1. | Tyint
  2. | Tyuint
  3. | Tybool
  4. | Tystring
  5. | Tyrational
  6. | Tyaddr
  7. | Tyrole
  8. | Tykey
  9. | Tydate
  10. | Tyduration
  11. | Tytez
  12. | Tystorage
  13. | Tytransfers
  14. | Tyunit
  15. | Tycontract of 'i
  16. | Tyrecord of 'i
  17. | Tycoll of 'i
  18. | Tymap of 'i
  19. | Tyasset of 'i
  20. | Typartition of 'i
  21. | Tystate
  22. | Tyenum of 'i
  23. | Tyoption of 'i abstract_type
  24. | Tylist of 'i abstract_type
  25. | Tytuple of 'i abstract_type list
Sourcetype ('t, 'i) abstract_univ_decl = 'i list * 't
Sourcetype 'i pattern_node =
  1. | Twild
  2. | Tconst 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. | 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, 'i) abstract_formula list * 'e
  8. | Ttry of 'e * (exn * 'e) list
  9. | Tvar of 'i
  10. | Trecord of 'e option * ('i * 'e) list
  11. | Tdot of 'e * 'e
  12. | Tdoti of 'i * 'i
  13. | Tename
  14. | Tcaller of 'i
  15. | Ttransferred of 'i
  16. | Tnow of 'i
  17. | Tadded of 'i
  18. | Trmed of 'i
  19. | Tlist of 'e list
  20. | Tnil
  21. | Temptycoll of 'i
  22. | Tcard of 'i * 'e
  23. | Tunshallow of 'i * 'e * 'e
  24. | Tshallow of 'i * 'e * 'e
  25. | Tmlist of 'e * 'i * 'i * 'i * 'e
  26. | Tcons of 'e * 'e
  27. | Tmkcoll of 'i * 'e
  28. | Tcontent of 'i * 'e
  29. | Tadd of 'i * 'e * 'e
  30. | Tremove of 'i * 'e * 'e
  31. | Tlistremove of 'i * 'e * 'e
  32. | Tget of 'i * 'e * 'e
  33. | Tset of 'i * 'e * 'e * 'e
  34. | Tcoll of 'i * 'e
  35. | Tassign of 'e * 'e
  36. | Traise of exn
  37. | Texn of exn
  38. | Tconcat of 'e * 'e
  39. | Tmktr of 'e * 'e
  40. | Ttradd of 'i
  41. | Ttrrm of 'i
  42. | Tplus of 't * 'e * 'e
  43. | Tminus of 't * 'e * 'e
  44. | Tuminus of 't * 'e
  45. | Tdiv of 't * 'e * 'e
  46. | Tmod of 't * 'e * 'e
  47. | Tnot of 'e
  48. | Tpand of 'e * 'e
  49. | Teq of 't * 'e * 'e
  50. | Tlt of 't * 'e * 'e
  51. | Tle of 't * 'e * 'e
  52. | Tgt of 't * 'e * 'e
  53. | Tge of 't * 'e * 'e
  54. | Tdlt of 't * 'e * 'e * 'e
  55. | Tdle of 't * 'e * 'e * 'e
  56. | Tdlet of 't * 'e * 'e * 'e
  57. | Tdlte of 't * 'e * 'e * 'e
  58. | Tint of Core.big_int
  59. | Taddr of string
  60. | Tforall of ('t, 'i) abstract_univ_decl list * 'e
  61. | Texists of ('t, 'i) abstract_univ_decl list * 'e
  62. | Tresult
  63. | Timpl of 'e * 'e
  64. | Tand of 'e * 'e
  65. | Tor of 'e * 'e
  66. | Told of 'e
  67. | Tat of 'e
  68. | Tfalse
  69. | Ttrue
  70. | Tunion of 'i * 'e * 'e
  71. | Tinter of 'i * 'e * 'e
  72. | Tdiff of 'i * 'e * 'e
  73. | Tsubset of 'i * 'e * 'e
  74. | Tassert of 'i option * 'e
  75. | Ttoiter of 'i * 'i * 'e
  76. | Tmem of 'i * 'e * 'e
  77. | Tlmem of 'i * 'e * 'e
  78. | Tcontains of 'i * 'e * 'e
  79. | Tempty of 'i * 'e
  80. | Tsingl of 'i * 'e
  81. | Thead of 'e * 'e
  82. | Ttail of 'e * 'e
  83. | Tnth of 'i * 'e * 'e
  84. | Twitness of 'i
  85. | Tnone
  86. | Tsome of 'e
  87. | Tenum of 'i
  88. | Ttobereplaced
  89. | 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. variants : 'e list;
  7. requires : ('e, 'i) abstract_formula list;
  8. ensures : ('e, 'i) abstract_formula list;
  9. 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 abstract_clone_subst =
  1. | Ctype of 'i * 'i
  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 'i abstract_qualid
  2. | Dval of 'i * 't
  3. | Dclone of 'i abstract_qualid * 'i * 'i 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
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 abstract_qualid -> 'i2 list
Sourceval map_abstract_type : ('i1 -> 'i2) -> 'i1 abstract_type -> 'i2 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_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) -> 'i1 abstract_clone_subst -> 'i2 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 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 mlw_module = (term, typ, ident) abstract_module
Sourcetype 'o with_loc = {
  1. obj : 'o;
  2. loc : Location.t;
}
Sourcetype loc_ident = string 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_exn : exn -> exn -> bool
Sourceval compare_fmod : fmod -> fmod -> bool
Sourceval compare_abstract_type : ('i -> 'i -> bool) -> 'i abstract_type -> 'i 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 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
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