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) -> 'i10 abstract_qualid -> 'i20 list
val map_abstract_type : ('i1 -> 'i2) -> 'i10 abstract_type -> 'i20 abstract_type
val map_abstract_univ_decl : ('t1 -> 't2) -> ('i1 -> 'i2) -> ('t10, 'i10) abstract_univ_decl -> ('t20, 'i20) abstract_univ_decl
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) -> 'i10 abstract_clone_subst -> 'i20 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 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 -> '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) -> 'i0 abstract_type -> 'i1 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_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