package archetype

  1. Overview
  2. Docs
type exn =
  1. | Enotfound
  2. | Ekeyexist
  3. | Einvalidcaller
  4. | Einvalidcondition
  5. | Enotransfer
  6. | Ebreak
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. | 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. | Tyenum of 'i
  22. | Tyoption of 'i abstract_type
  23. | Tylist of 'i abstract_type
  24. | Tytuple of 'i abstract_type list
type ('t, 'i) abstract_univ_decl = 'i list * 't
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. | Tapp of 'e * 'e list
  6. | Tfor of 'i * 'e * ('e, 'i) abstract_formula list * 'e
  7. | Ttry of 'e * (exn * 'e) list
  8. | Tvar of 'i
  9. | Trecord of 'e option * ('i * 'e) list
  10. | Tdot of 'e * 'e
  11. | Tdoti of 'i * 'i
  12. | Tename
  13. | Tcaller of 'i
  14. | Ttransferred of 'i
  15. | Tnow of 'i
  16. | Tadded of 'i
  17. | Trmed of 'i
  18. | Tlist of 'e list
  19. | Tnil
  20. | Temptycoll of 'i
  21. | Tcard of 'i * 'e
  22. | Tunshallow of 'i * 'e * 'e
  23. | Tshallow of 'i * 'e * 'e
  24. | Tmlist of 'e * 'i * 'i * 'i * 'e
  25. | Tcons of 'e * 'e
  26. | Tadd of 'i * 'e * 'e
  27. | Tremove of 'i * 'e * 'e
  28. | Tlistremove of 'i * 'e * 'e
  29. | Tget of 'i * 'e * 'e
  30. | Tset of 'i * 'e * 'e * 'e
  31. | Tcoll of 'i * 'e
  32. | Tassign of 'e * 'e
  33. | Traise of exn
  34. | Texn of exn
  35. | Tconcat of 'e * 'e
  36. | Tmktr of 'e * 'e
  37. | Ttradd of 'i
  38. | Ttrrm of 'i
  39. | Tplus of 't * 'e * 'e
  40. | Tminus of 't * 'e * 'e
  41. | Tuminus of 't * 'e
  42. | Tdiv of 't * 'e * 'e
  43. | Tmod of 't * 'e * 'e
  44. | Tnot of 'e
  45. | Tpand of 'e * 'e
  46. | Teq of 't * 'e * 'e
  47. | Tlt of 't * 'e * 'e
  48. | Tle of 't * 'e * 'e
  49. | Tgt of 't * 'e * 'e
  50. | Tge of 't * 'e * 'e
  51. | Tdlt of 't * 'e * 'e * 'e
  52. | Tdle of 't * 'e * 'e * 'e
  53. | Tdlet of 't * 'e * 'e * 'e
  54. | Tdlte of 't * 'e * 'e * 'e
  55. | Tint of Core.big_int
  56. | Taddr of string
  57. | Tforall of ('t, 'i) abstract_univ_decl list * 'e
  58. | Texists of ('t, 'i) abstract_univ_decl list * 'e
  59. | Tresult
  60. | Timpl of 'e * 'e
  61. | Tand of 'e * 'e
  62. | Tor of 'e * 'e
  63. | Told of 'e
  64. | Tat of 'e
  65. | Tfalse
  66. | Tunion of 'i * 'e * 'e
  67. | Tinter of 'i * 'e * 'e
  68. | Tdiff of 'i * 'e * 'e
  69. | Tsubset of 'i * 'e * 'e
  70. | Tassert of 'i option * 'e
  71. | Ttoiter of 'i * 'i * 'e
  72. | Tmem of 'i * 'e * 'e
  73. | Tlmem of 'i * 'e * 'e
  74. | Tcontains of 'i * 'e * 'e
  75. | Tempty of 'i * 'e
  76. | Tsingl of 'i * 'e
  77. | Thead of 'e * 'e
  78. | Ttail of 'e * 'e
  79. | Tnth of 'i * 'e * 'e
  80. | Tnone
  81. | Tsome of 'e
  82. | Tenum of 'i
  83. | Ttobereplaced
  84. | 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 '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
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_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_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