archetype 1.2.6 · OCaml Package

type fmod =

| LogicOnly
| Logic
| Rec
| NoMod

val pp_fmod : 
  Ppx_deriving_runtime.Format.formatter ->
  fmod ->
  Ppx_deriving_runtime.unit

val show_fmod : fmod -> Ppx_deriving_runtime.string

type 'e exn =

| Einvalid of string option
| Efail of int * 'e option
| EInvalidCaller
| EInvalidCondition of string
| ENotFound
| EOutOfBound
| EKeyExists
| EKeyExistsOrNotFound
| EDivByZero
| ENatAssign
| ENoTransfer
| EInvalidState

val pp_exn : 
  'e. (Ppx_deriving_runtime.Format.formatter ->
        'e ->
        Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'e exn ->
  Ppx_deriving_runtime.unit

val show_exn : 
  'e. (Ppx_deriving_runtime.Format.formatter ->
        'e ->
        Ppx_deriving_runtime.unit) ->
  'e exn ->
  Ppx_deriving_runtime.string

type ('i, 't) abstract_type =

| Tyint
| Tyuint
| Tybool
| Tystring
| Tyrational
| Tyaddr
| Tykey
| Tykeyhash
| Tydate
| Tyduration
| Tytez
| Tysignature
| Tybytes
| Tychainid
| Tystorage
| Tyoperation
| Tycontract
| Tyunit
| Tyrecord of 'i
| Tycoll of 'i
| Tyview of 'i
| Tymap of 'i
| Tyasset of 'i
| Typartition of 'i
| Tyaggregate of 'i
| Tystate
| Tyenum of 'i
| Tyoption of 't
| Tyset of 'i
| Tylist of 't
| Tytuple of 't list
| Tyor of 't * 't
| Tylambda of 't * 't
| Tybls12_381_fr
| Tybls12_381_g1
| Tybls12_381_g2
| Tynever

val pp_abstract_type : 
  'i 't. (Ppx_deriving_runtime.Format.formatter ->
           'i ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('i, 't) abstract_type ->
  Ppx_deriving_runtime.unit

val show_abstract_type : 
  'i 't. (Ppx_deriving_runtime.Format.formatter ->
           'i ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  ('i, 't) abstract_type ->
  Ppx_deriving_runtime.string

type ('t, 'i) abstract_univ_decl = 'i list * 't

val pp_abstract_univ_decl : 
  't 'i. (Ppx_deriving_runtime.Format.formatter ->
           't ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('t, 'i) abstract_univ_decl ->
  Ppx_deriving_runtime.unit

val show_abstract_univ_decl : 
  't 'i. (Ppx_deriving_runtime.Format.formatter ->
           't ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('t, 'i) abstract_univ_decl ->
  Ppx_deriving_runtime.string

type 'i pattern_node =

| Twild
| Tpignore
| Tconst of 'i
| Tpatt_tuple of 'i pattern_node list
| Tpsome of 'i
| Tpleft of 'i
| Tpright of 'i

val pp_pattern_node : 
  'i. (Ppx_deriving_runtime.Format.formatter ->
        'i ->
        Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'i pattern_node ->
  Ppx_deriving_runtime.unit

val show_pattern_node : 
  'i. (Ppx_deriving_runtime.Format.formatter ->
        'i ->
        Ppx_deriving_runtime.unit) ->
  'i pattern_node ->
  Ppx_deriving_runtime.string

type ('e, 't, 'i) abstract_term =

| Tseq of 'e list
| Tletin of bool * 'i * 't option * 'e * 'e
| Tletfun of ('e, 't, 'i) abstract_fun_struct * 'e
| Tlambda of 'i list * 'e
| Tif of 'e * 'e * 'e option
| Tmatch of 'e * ('i pattern_node * 'e) list
| Tmatchoption of 'e * 'i * 'e * 'e
| Tmatchor of 'e * 'i * 'e * 'i * 'e
| Tmatchlist of 'e * 'i * 'i * 'e * 'e
| Tapp of 'e * 'e list
| Tfor of 'i * 'e * 'e * ('e, 'i) abstract_formula list * 'e
| Twhile of 'e * ('e, 'i) abstract_formula list * 'e
| Ttry of 'e * ('e exn * 'e) list
| Tvar of 'i
| Ttuple of 'e list
| Ttupleaccess of 'e * int * int
| Tvlambda of 't * 'i * 't * 'e
| Texeclambda of 'e * 'e
| Tapplylambda of 'e * 'e
| Trecord of 'e option * ('i * 'e) list
| Tdot of 'e * 'e
| Tdoti of 'i * 'i
| Tename
| Tcaller of 'i
| Tsender of 'i
| Ttransferred of 'i
| Tnow of 'i
| Tadded of 'i
| Trmed of 'i
| Tchainid of 'i
| Tselfaddress of 'i
| Tdefaultaddr
| Temptystr
| Tlist of 'e list
| Tnil of 'i
| Temptycoll of 'i
| Temptyview of 'i
| Temptyfield of 'i
| Tcard of 'i * 'e
| Tfromfield of 'i * 'e * 'e
| Tfromview of 'i * 'e * 'e
| Ttoview of 'i * 'e
| Tviewtolist of 'i * 'e * 'e
| Telts of 'i * 'e
| Tshallow of 'i * 'e * 'e
| Tmlist of 'i * 'e * 'i * 'i * 'i * 'e
| Tcons of 'i * 'e * 'e
| Tprepend of 'i * 'e * 'e
| Tmkcoll of 'i * 'e list
| Tmkview of 'i * 'e
| Tcontent of 'i * 'e
| Tcontains of 'i * 'e * 'e
| Tvcontent of 'i * 'e
| Tlistreverse of 'i * 'e
| Tlistconcat of 'i * 'e * 'e
| Tlistmap of 'i * 'e * 'i * 'e
| Tfold of 'e * 'i * 'e
| Tadd of 'i * 'e * 'e
| Tvadd of 'i * 'e * 'e
| Tremove of 'i * 'e * 'e
| Tvremove of 'i * 'e * 'e
| Tupdate of 'i * 'e * 'e * 'e
| Tget of 'i * 'e * 'e
| Tgetforce of 'i * 'e * 'e
| Tfget of 'i * 'e * 'e
| Tset of 'i * 'e * 'e * 'e
| Tvsum of 'i * 'e * 'e
| Tcsum of 'i * 'e
| Tcsort of 'i * 'e
| Tvsort of 'i * 'e * 'e
| Tnth of 'i * 'e * 'e
| Tnthtuple of int * int * 'e
| Tcoll of 'i * 'e
| Tassign of 'e * 'e
| Traise of 'e exn
| Texn of 'e exn
| Tconcat of 'e * 'e
| Ttransfer of 'e * 'e
| Tcall of 'e * 'e * 'i * 'e
| Tmkoperation of 'e * 'e * 'e
| Tentrypoint of 'i * 'e
| Tfst of 'e
| Tsnd of 'e
| Tsndopt of 'e
| Tabs of 'e
| Tmktr of 'e * 'e
| Ttradd of 'i
| Ttrrm of 'i
| Tplus of 't * 'e * 'e
| Tminus of 't * 'e * 'e
| Tuminus of 't * 'e
| Tmult of 't * 'e * 'e
| Tdiv of 't * 'e * 'e
| Tmod of 't * 'e * 'e
| Tdivmod of 't * 'e * 'e
| Tthreewaycmp of 't * 'e * 'e
| Tshiftleft of 'e * 'e
| Tshiftright of 'e * 'e
| Tnot of 'e
| Tpand of 'e * 'e
| Teq of 't * 'e * 'e
| Teqfield of 'i * 'e * 'e
| Tneq of 't * 'e * 'e
| Tlt of 't * 'e * 'e
| Tle of 't * 'e * 'e
| Tgt of 't * 'e * 'e
| Tge of 't * 'e * 'e
| Tdlt of 't * 'e * 'e * 'e
| Tdle of 't * 'e * 'e * 'e
| Tdlet of 't * 'e * 'e * 'e
| Tdlte of 't * 'e * 'e * 'e
| Tint of Core.big_int
| Tstring of string
| Taddr of string
| Tbytes of string
| Tforall of ('t, 'i) abstract_univ_decl list * 'e
| Texists of ('t, 'i) abstract_univ_decl list * 'e
| Tresult
| Timpl of 'e * 'e
| Tequiv of 'e * 'e
| Tand of 'e * 'e
| Tor of 'e * 'e
| Txor of 't * 'e * 'e
| Told of 'e
| Tfalse
| Ttrue
| Tunion of 'i * 'e * 'e
| Tinter of 'i * 'e * 'e
| Tdiff of 'i * 'e * 'e
| Tsubset of 'i * 'e * 'e
| Tassert of 'i option * 'e
| Tmem of 'i * 'e * 'e
| Tvmem of 'i * 'e * 'e
| Tlmem of 'i * 'e * 'e
| Tccontains of 'i * 'e * 'e
| Tvcontains of 'i * 'e * 'e
| Tempty of 'i * 'e
| Tvempty of 'i * 'e
| Tsingl of 'i * 'e
| Tchead of 'i * 'e * 'e
| Tvhead of 'i * 'e * 'e
| Tctail of 'i * 'e * 'e
| Tvtail of 'i * 'e * 'e
| Tcnth of 'i * 'e * 'e
| Tvnth of 'i * 'e * 'e
| Tlnth of 'i * 'e * 'e
| Tselect of 'i * 'e * 'e
| Tcselect of 'i * 'i * 'e list * 'e
| Tvselect of 'i * 'i * 'e list * 'e * 'e
| Tremoveif of 'i * 'i * 'e list * 'e
| Tpremoveif of 'i * 'i * 'e list * 'e * 'e
| Tfremoveif of 'i * 'i * 'e list * 'e * 'e * 'e
| Tunionpred of 'i * 'i * 'e list * 'e
| Twitness of 'i
| Tnone
| Tsome of 'e
| Tleft of 't * 'e
| Tright of 't * 'e
| Tenum of 'i
| Tmark of 'i * 'e
| Tat of 'i * 'e
| Tunit
| Ttobereplaced
| Tnottranslated

and ('e, 'i) abstract_formula = {

id : 'i;
form : 'e;

}

and ('e, 't, 'i) abstract_fun_struct = {

name : 'i;
logic : fmod;
args : ('i * 't) list;
returns : 't;
raises : 'e list;
fails : ('e, 'i) abstract_struct_fail list;
variants : 'e list;
requires : ('e, 'i) abstract_formula list;
ensures : ('e, 'i) abstract_formula list;
body : 'e;

}

and ('e, 'i) abstract_struct_fail = {

fid : 'e;
expl : 'i option;
expr : 'e option;

}

val pp_abstract_term : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_term ->
  Ppx_deriving_runtime.unit

val show_abstract_term : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_term ->
  Ppx_deriving_runtime.string

val pp_abstract_formula : 
  'e 'i. (Ppx_deriving_runtime.Format.formatter ->
           'e ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 'i) abstract_formula ->
  Ppx_deriving_runtime.unit

val show_abstract_formula : 
  'e 'i. (Ppx_deriving_runtime.Format.formatter ->
           'e ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 'i) abstract_formula ->
  Ppx_deriving_runtime.string

val pp_abstract_fun_struct : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_fun_struct ->
  Ppx_deriving_runtime.unit

val show_abstract_fun_struct : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_fun_struct ->
  Ppx_deriving_runtime.string

val pp_abstract_struct_fail : 
  'e 'i. (Ppx_deriving_runtime.Format.formatter ->
           'e ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 'i) abstract_struct_fail ->
  Ppx_deriving_runtime.unit

val show_abstract_struct_fail : 
  'e 'i. (Ppx_deriving_runtime.Format.formatter ->
           'e ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 'i) abstract_struct_fail ->
  Ppx_deriving_runtime.string

type ('e, 't, 'i) abstract_field = {

name : 'i;
typ : 't;
init : 'e;
mutable_ : bool;

}

val pp_abstract_field : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_field ->
  Ppx_deriving_runtime.unit

val show_abstract_field : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_field ->
  Ppx_deriving_runtime.string

type ('e, 't, 'i) abstract_storage_struct = {

fields : ('e, 't, 'i) abstract_field list;
invariants : ('e, 'i) abstract_formula list;

}

val pp_abstract_storage_struct : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_storage_struct ->
  Ppx_deriving_runtime.unit

val show_abstract_storage_struct : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_storage_struct ->
  Ppx_deriving_runtime.string

type ('i, 't) abstract_clone_subst =

| Ctype of 'i * 't
| Cval of 'i * 'i
| Cfun of 'i * 'i
| Cpred of 'i * 'i

val pp_abstract_clone_subst : 
  'i 't. (Ppx_deriving_runtime.Format.formatter ->
           'i ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('i, 't) abstract_clone_subst ->
  Ppx_deriving_runtime.unit

val show_abstract_clone_subst : 
  'i 't. (Ppx_deriving_runtime.Format.formatter ->
           'i ->
           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  ('i, 't) abstract_clone_subst ->
  Ppx_deriving_runtime.string

type theotyp =

| Theo
| Axiom
| Lemma
| Goal

val pp_theotyp : 
  Ppx_deriving_runtime.Format.formatter ->
  theotyp ->
  Ppx_deriving_runtime.unit

val show_theotyp : theotyp -> Ppx_deriving_runtime.string

type ('e, 't, 'i) abstract_decl =

| Duse of bool * 'i list * string option
| Dval of bool * 'i * 't
| Dclone of 'i list * 'i * ('i, 't) abstract_clone_subst list
| Denum of 'i * 'i list
| Drecord of 'i * ('e, 't, 'i) abstract_field list
| Dstorage of ('e, 't, 'i) abstract_storage_struct
| Dtheorem of theotyp * 'i * 'e
| Dfun of ('e, 't, 'i) abstract_fun_struct
| Dexn of 'i * 't
| Dpred of 'i * ('i * 't) list * 'e

val pp_abstract_decl : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_decl ->
  Ppx_deriving_runtime.unit

val show_abstract_decl : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_decl ->
  Ppx_deriving_runtime.string

type ('e, 't, 'i) abstract_module = {

name : 'i;
decls : ('e, 't, 'i) abstract_decl list;

}

val pp_abstract_module : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_module ->
  Ppx_deriving_runtime.unit

val show_abstract_module : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_module ->
  Ppx_deriving_runtime.string

type ('e, 't, 'i) abstract_mlw_tree = ('e, 't, 'i) abstract_module list

val pp_abstract_mlw_tree : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('e, 't, 'i) abstract_mlw_tree ->
  Ppx_deriving_runtime.unit

val show_abstract_mlw_tree : 
  'e 't 'i. (Ppx_deriving_runtime.Format.formatter ->
              'e ->
              Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 't -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'i -> Ppx_deriving_runtime.unit) ->
  ('e, 't, 'i) abstract_mlw_tree ->
  Ppx_deriving_runtime.string

val map_abstract_qualid : ('i1 -> 'i2) -> 'i1 list -> 'i2 list

val map_abstract_type : 
  ('i1 -> 'i2) ->
  ('t1 -> 't2) ->
  ('i1, 't1) abstract_type ->
  ('i2, 't2) 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_struct_fail : 
  ('e1 -> 'e2) ->
  ('i1 -> 'i2) ->
  ('e1, 'i1) abstract_struct_fail ->
  ('e2, 'i2) abstract_struct_fail

val map_exn : ('e1 -> 'e2) -> 'e1 exn -> 'e2 exn

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) ->
  ('t1 -> 't2) ->
  ('i1, 't1) abstract_clone_subst ->
  ('i2, 't2) 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

val pp_ident : 
  Ppx_deriving_runtime.Format.formatter ->
  ident ->
  Ppx_deriving_runtime.unit

val show_ident : ident -> Ppx_deriving_runtime.string

type qualid = ident list

val pp_qualid : 
  Ppx_deriving_runtime.Format.formatter ->
  qualid ->
  Ppx_deriving_runtime.unit

val show_qualid : qualid -> Ppx_deriving_runtime.string

type typ = (ident, typ) abstract_type

val pp_typ : 
  Ppx_deriving_runtime.Format.formatter ->
  typ ->
  Ppx_deriving_runtime.unit

val show_typ : typ -> Ppx_deriving_runtime.string

type univ_decl = (typ, ident) abstract_univ_decl

val pp_univ_decl : 
  Ppx_deriving_runtime.Format.formatter ->
  univ_decl ->
  Ppx_deriving_runtime.unit

val show_univ_decl : univ_decl -> Ppx_deriving_runtime.string

type term = (term, typ, ident) abstract_term

val pp_term : 
  Ppx_deriving_runtime.Format.formatter ->
  term ->
  Ppx_deriving_runtime.unit

val show_term : term -> Ppx_deriving_runtime.string

type formula = (term, ident) abstract_formula

val pp_formula : 
  Ppx_deriving_runtime.Format.formatter ->
  formula ->
  Ppx_deriving_runtime.unit

val show_formula : formula -> Ppx_deriving_runtime.string

type field = (term, typ, ident) abstract_field

val pp_field : 
  Ppx_deriving_runtime.Format.formatter ->
  field ->
  Ppx_deriving_runtime.unit

val show_field : field -> Ppx_deriving_runtime.string

type fun_struct = (term, typ, ident) abstract_fun_struct

val pp_fun_struct : 
  Ppx_deriving_runtime.Format.formatter ->
  fun_struct ->
  Ppx_deriving_runtime.unit

val show_fun_struct : fun_struct -> Ppx_deriving_runtime.string

type storage_struct = (term, typ, ident) abstract_storage_struct

val pp_storage_struct : 
  Ppx_deriving_runtime.Format.formatter ->
  storage_struct ->
  Ppx_deriving_runtime.unit

val show_storage_struct : storage_struct -> Ppx_deriving_runtime.string

type clone_subst = (ident, typ) abstract_clone_subst

val pp_clone_subst : 
  Ppx_deriving_runtime.Format.formatter ->
  clone_subst ->
  Ppx_deriving_runtime.unit

val show_clone_subst : clone_subst -> Ppx_deriving_runtime.string

type decl = (term, typ, ident) abstract_decl

val pp_decl : 
  Ppx_deriving_runtime.Format.formatter ->
  decl ->
  Ppx_deriving_runtime.unit

val show_decl : decl -> Ppx_deriving_runtime.string

type mlw_module = (term, typ, ident) abstract_module

val pp_mlw_module : 
  Ppx_deriving_runtime.Format.formatter ->
  mlw_module ->
  Ppx_deriving_runtime.unit

val show_mlw_module : mlw_module -> Ppx_deriving_runtime.string

type mlw_tree = (term, typ, ident) abstract_mlw_tree

val pp_mlw_tree : 
  Ppx_deriving_runtime.Format.formatter ->
  mlw_tree ->
  Ppx_deriving_runtime.unit

val show_mlw_tree : mlw_tree -> Ppx_deriving_runtime.string

type 'o with_loc = {

obj : 'o;
loc : Location.t;

}

val pp_with_loc : 
  'o. (Ppx_deriving_runtime.Format.formatter ->
        'o ->
        Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  'o with_loc ->
  Ppx_deriving_runtime.unit

val show_with_loc : 
  'o. (Ppx_deriving_runtime.Format.formatter ->
        'o ->
        Ppx_deriving_runtime.unit) ->
  'o with_loc ->
  Ppx_deriving_runtime.string

type loc_ident = string with_loc

val pp_loc_ident : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_ident ->
  Ppx_deriving_runtime.unit

val show_loc_ident : loc_ident -> Ppx_deriving_runtime.string

type loc_qualid = loc_ident list with_loc

val pp_loc_qualid : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_qualid ->
  Ppx_deriving_runtime.unit

val show_loc_qualid : loc_qualid -> Ppx_deriving_runtime.string

type loc_typ = (loc_ident, loc_typ) abstract_type with_loc

val pp_loc_typ : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_typ ->
  Ppx_deriving_runtime.unit

val show_loc_typ : loc_typ -> Ppx_deriving_runtime.string

type loc_univ_decl = (loc_typ, loc_ident) abstract_univ_decl with_loc

val pp_loc_univ_decl : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_univ_decl ->
  Ppx_deriving_runtime.unit

val show_loc_univ_decl : loc_univ_decl -> Ppx_deriving_runtime.string

type loc_term = (loc_term, loc_typ, loc_ident) abstract_term with_loc

val pp_loc_term : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_term ->
  Ppx_deriving_runtime.unit

val show_loc_term : loc_term -> Ppx_deriving_runtime.string

type loc_formula = (loc_term, loc_ident) abstract_formula with_loc

val pp_loc_formula : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_formula ->
  Ppx_deriving_runtime.unit

val show_loc_formula : loc_formula -> Ppx_deriving_runtime.string

type loc_field = (loc_term, loc_typ, loc_ident) abstract_field with_loc

val pp_loc_field : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_field ->
  Ppx_deriving_runtime.unit

val show_loc_field : loc_field -> Ppx_deriving_runtime.string

type loc_fun_struct =
  (loc_term, loc_typ, loc_ident) abstract_fun_struct with_loc

val pp_loc_fun_struct : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_fun_struct ->
  Ppx_deriving_runtime.unit

val show_loc_fun_struct : loc_fun_struct -> Ppx_deriving_runtime.string

type loc_storage_struct =
  (loc_term, loc_typ, loc_ident) abstract_storage_struct with_loc

val pp_loc_storage_struct : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_storage_struct ->
  Ppx_deriving_runtime.unit

val show_loc_storage_struct : loc_storage_struct -> Ppx_deriving_runtime.string

type loc_clone_subst = (loc_ident, loc_typ) abstract_clone_subst with_loc

val pp_loc_clone_subst : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_clone_subst ->
  Ppx_deriving_runtime.unit

val show_loc_clone_subst : loc_clone_subst -> Ppx_deriving_runtime.string

type loc_decl = (loc_term, loc_typ, loc_ident) abstract_decl with_loc

val pp_loc_decl : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_decl ->
  Ppx_deriving_runtime.unit

val show_loc_decl : loc_decl -> Ppx_deriving_runtime.string

type loc_mlw_module = (loc_term, loc_typ, loc_ident) abstract_module

val pp_loc_mlw_module : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_mlw_module ->
  Ppx_deriving_runtime.unit

val show_loc_mlw_module : loc_mlw_module -> Ppx_deriving_runtime.string

type loc_mlw_tree = (loc_term, loc_typ, loc_ident) abstract_mlw_tree

val pp_loc_mlw_tree : 
  Ppx_deriving_runtime.Format.formatter ->
  loc_mlw_tree ->
  Ppx_deriving_runtime.unit

val show_loc_mlw_tree : loc_mlw_tree -> Ppx_deriving_runtime.string

type struct_fail = (loc_term, loc_ident) abstract_struct_fail

val mk_struct_fail : 
  ?expl:loc_ident ->
  ?expr:loc_term ->
  loc_term ->
  struct_fail

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 loc_decl : decl -> (loc_term, loc_typ, loc_ident) abstract_decl with_loc

val loc_field : field -> (loc_term, loc_typ, loc_ident) abstract_field with_loc

val deloc : 'a with_loc -> 'a

val compare_fmod : fmod -> fmod -> bool

val compare_abstract_type : 
  ('i -> 'i -> bool) ->
  ('t -> 't -> bool) ->
  ('i, 't) abstract_type ->
  ('i, 't) 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 compare_exn : ('e -> 'e -> bool) -> 'e exn -> 'e exn -> 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

package archetype