package archetype

  1. Overview
  2. Docs
package archetype
Legend:
Library
Module
Module type
Parameter
Class
Class type
type exn =
  1. | Enotfound
  2. | Ekeyexist
  3. | Einvalidcaller
  4. | Einvalidcondition
  5. | Einvalidstate
  6. | Enotransfer
  7. | Ebreak
  8. | Einvalid of string option
type fmod =
  1. | Logic
  2. | Rec
  3. | NoMod
type 'i abstract_qualid = 'i list
type '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. | Tybytes
  13. | Tystorage
  14. | Tytransfers
  15. | Tyunit
  16. | Tycontract of 'i
  17. | Tyrecord of 'i
  18. | Tycoll of 'i
  19. | Tyview of 'i
  20. | Tymap of 'i
  21. | Tyasset of 'i
  22. | Typartition of 'i
  23. | Tystate
  24. | Tyenum of 'i
  25. | Tyoption of 'i abstract_type
  26. | Tylist of 'i abstract_type
  27. | Tytuple of 'i abstract_type list
type ('t, 'i) abstract_univ_decl = 'i list * 't
type 'i pattern_node =
  1. | Twild
  2. | Tconst of 'i
  3. | Tpatt_tuple of 'i pattern_node list
  4. | 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. | Trecord of 'e option * ('i * 'e) list
  12. | Tdot of 'e * 'e
  13. | Tdoti of 'i * 'i
  14. | Tename
  15. | Tcaller of 'i
  16. | Tsender of 'i
  17. | Ttransferred of 'i
  18. | Tnow of 'i
  19. | Tadded of 'i
  20. | Trmed of 'i
  21. | Tlist of 'e list
  22. | Tnil of 'i
  23. | Temptycoll of 'i
  24. | Tcard of 'i * 'e
  25. | Tvcard of 'i * 'e
  26. | Ttocoll of 'i * 'e * 'e
  27. | Ttoview of 'i * 'e
  28. | Tshallow of 'i * 'e * 'e
  29. | Tmlist of 'i * 'e * 'i * 'i * 'i * 'e
  30. | Tcons of 'i * 'e * 'e
  31. | Tmkcoll of 'i * 'e
  32. | Tcontent of 'i * 'e
  33. | Tadd of 'i * 'e * 'e
  34. | Tremove of 'i * 'e * 'e
  35. | Tvremove of 'i * 'e * 'e
  36. | Tget of 'i * 'e * 'e
  37. | Tset of 'i * 'e * 'e * 'e
  38. | Tsum of 'i * 'e * 'e
  39. | Tsort of 'i * 'e * 'e
  40. | Tcoll of 'i * 'e
  41. | Tassign of 'e * 'e
  42. | Traise of exn
  43. | Texn of exn
  44. | Tconcat of 'e * 'e
  45. | Ttransfer of 'e * 'e
  46. | Tcall of 'e
  47. | Tfst of 'e
  48. | Tsnd of 'e
  49. | Tabs of 'e
  50. | Tmktr of 'e * 'e
  51. | Ttradd of 'i
  52. | Ttrrm of 'i
  53. | Tplus of 't * 'e * 'e
  54. | Tminus of 't * 'e * 'e
  55. | Tuminus of 't * 'e
  56. | Tmult of 't * 'e * 'e
  57. | Tdiv of 't * 'e * 'e
  58. | Tmod of 't * 'e * 'e
  59. | Tnot of 'e
  60. | Tpand of 'e * 'e
  61. | Teq of 't * 'e * 'e
  62. | Teqview of 'i * 'e * 'e
  63. | Tneq of 't * 'e * 'e
  64. | Tlt of 't * 'e * 'e
  65. | Tle of 't * 'e * 'e
  66. | Tgt of 't * 'e * 'e
  67. | Tge of 't * 'e * 'e
  68. | Tdlt of 't * 'e * 'e * 'e
  69. | Tdle of 't * 'e * 'e * 'e
  70. | Tdlet of 't * 'e * 'e * 'e
  71. | Tdlte of 't * 'e * 'e * 'e
  72. | Tint of Core.big_int
  73. | Taddr of string
  74. | Tbytes of string
  75. | Tforall of ('t, 'i) abstract_univ_decl list * 'e
  76. | Texists of ('t, 'i) abstract_univ_decl list * 'e
  77. | Tresult
  78. | Timpl of 'e * 'e
  79. | Tand of 'e * 'e
  80. | Tor of 'e * 'e
  81. | Told of 'e
  82. | Tfalse
  83. | Ttrue
  84. | Tunion of 'i * 'e * 'e
  85. | Tinter of 'i * 'e * 'e
  86. | Tdiff of 'i * 'e * 'e
  87. | Tsubset of 'i * 'e * 'e
  88. | Tassert of 'i option * 'e
  89. | Ttoiter of 'i * 'i * 'e
  90. | Tmem of 'i * 'e * 'e
  91. | Tlmem of 'i * 'e * 'e
  92. | Tcontains of 'i * 'e * 'e
  93. | Tempty of 'i * 'e
  94. | Tvempty of 'i * 'e
  95. | Tsingl of 'i * 'e
  96. | Thead of 'i * 'e * 'e
  97. | Ttail of 'i * 'e * 'e
  98. | Tnth of 'i * 'e * 'e
  99. | Tlnth of 'i * 'e * 'e
  100. | Twitness of 'i
  101. | Tnone
  102. | Tsome of 'e
  103. | Tenum of 'i
  104. | Tmark of 'i * 'e
  105. | Tat of 'i * 'e
  106. | Tunit
  107. | Ttobereplaced
  108. | 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 abstract_clone_subst =
  1. | Ctype of 'i * 'i
  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 '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
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 abstract_qualid -> 'i2 list
val map_abstract_type : ('i1 -> 'i2) -> 'i1 abstract_type -> 'i2 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_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) -> 'i1 abstract_clone_subst -> 'i2 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 abstract_qualid
val show_qualid : qualid -> Ppx_deriving_runtime.string
type typ = ident 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 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
type loc_clone_subst = loc_ident abstract_clone_subst with_loc
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_exn : exn -> exn -> bool
val compare_fmod : fmod -> fmod -> bool
val compare_abstract_type : ('i -> 'i -> bool) -> 'i abstract_type -> 'i 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 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