sig
type sfn1 =
Sfn_NOT
| Sfn_item
| Sfn_sorted
| Sfn_hd
| Sfn_tl
| Sfn_set_of_list
| Sfn_can_return
type sfn2 =
Sfn_list_lt
| Sfn_items
| Sfn_subset
| Sfn_once_in_list
| Sfn_set_minus
type sfn = Sfn_list | Sfn_set | Sfn_AND | Sfn_OR | Sfn_XOR | Sfn_undef
type sfn_grp = Sfn_plus | Sfn_pos
type id_internal1
type id_internal2
type id_internal3
type exp = private
Enum of int
| Eident of Exp.id_internal1 * Exp.id_internal2 * Exp.id_internal3
| Eeq of Exp.exp * Exp.exp
| Efun1 of Exp.sfn1 * Exp.exp
| Efun2 of Exp.sfn2 * Exp.exp * Exp.exp
| Efun of Exp.sfn * Exp.exp list
| Egrp of Exp.sfn_grp * int * Exp.ie_list
and ie_list = private IEnil | IEcons of Exp.exp * int * Exp.ie_list
type subst = Exp.exp -> Exp.exp
val string_of_sfn1 : Exp.sfn1 -> string
val string_of_sfn2 : Exp.sfn2 -> string
val string_of_sfn : Exp.sfn -> string
val string_of_sfn_grp : Exp.sfn_grp -> string
module Id :
sig
type t
val pathDec : Exp.Id.t
val pathInc : Exp.Id.t
val tid : Exp.Id.t
val mytid : Exp.Id.t
val result : Exp.Id.t
val junk : Exp.Id.t
val create : string -> Exp.Id.t
val tempid : unit -> Exp.Id.t
val gensym_str : string -> Exp.Id.t
val gensym_str_ex : string -> Exp.Id.t
val gensym_norm : Exp.Id.t -> Exp.Id.t
val gensym_garb : Exp.Id.t -> Exp.Id.t
val of_exp : Exp.exp -> Exp.Id.t
val compare : Exp.Id.t -> Exp.Id.t -> int
val level : int -> Exp.Id.t
val isLevel : Exp.Id.t -> int -> bool
val is_existential : Exp.Id.t -> bool
val is_no_junk_var : Exp.Id.t -> bool
val to_string : Exp.Id.t -> string
end
module IdSet :
sig
type elt = Id.t
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
end
module IdMap :
sig
type key = Id.t
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
end
module E :
sig
val zero : Exp.exp
val one : Exp.exp
val tid : Exp.exp
val empty_list : Exp.exp
val empty_set : Exp.exp
val undef : Exp.exp
val num : int -> Exp.exp
val id : Exp.Id.t -> Exp.exp
val band : Exp.exp list -> Exp.exp
val bnot : Exp.exp -> Exp.exp
val fun1 : Exp.sfn1 -> Exp.exp -> Exp.exp
val fun2 : Exp.sfn2 -> Exp.exp -> Exp.exp -> Exp.exp
val funn : Exp.sfn -> Exp.exp list -> Exp.exp
val xor : Exp.exp list -> Exp.exp
val add : Exp.exp -> Exp.exp -> Exp.exp
val sub : Exp.exp -> Exp.exp -> Exp.exp
val list : Exp.exp list -> Exp.exp
val set : Exp.exp list -> Exp.exp
val item : Exp.exp -> Exp.exp
val items : Exp.exp -> Exp.exp -> Exp.exp
val eq : Exp.exp -> Exp.exp -> Exp.exp
val neq : Exp.exp -> Exp.exp -> Exp.exp
val ltn : Exp.exp -> Exp.exp -> Exp.exp
val leq : Exp.exp -> Exp.exp -> Exp.exp
val not_in_list : Exp.exp -> Exp.exp -> Exp.exp
val once_in_list : Exp.exp -> Exp.exp -> Exp.exp
val fv : Exp.exp -> Exp.IdSet.t -> Exp.IdSet.t
val fhd : Exp.exp -> Exp.IdSet.t -> Exp.IdSet.t
val exfv : Exp.exp -> Exp.IdSet.t -> Exp.IdSet.t
val gensym_str : string -> Exp.exp
val gensym_str_ex : string -> Exp.exp
val forall_fv : (Exp.Id.t -> bool) -> Exp.exp -> bool
end
val equal_exp : Exp.exp -> Exp.exp -> bool
val compare_exp : Exp.exp -> Exp.exp -> int
val compare_exp_list : Exp.exp list -> Exp.exp list -> int
val abs_compare_exp : Exp.exp -> Exp.exp -> int
val mem_exp : Exp.exp -> Exp.exp list -> bool
val remdup_exp : Exp.exp list -> Exp.exp list
val existential_id : Exp.exp -> bool
val exp_fold : (Exp.exp -> 'a -> 'a) -> Exp.exp -> 'a -> 'a
val ie_fold : (Exp.exp -> int -> 'a -> 'a) -> Exp.ie_list -> 'a -> 'a
val ie_fold_exp : (Exp.exp -> 'a -> 'a) -> Exp.ie_list -> 'a -> 'a
val mk_fun_subst : Exp.subst -> Exp.subst
val mk_id_subst : (Exp.Id.t -> Exp.exp) -> Exp.subst
val mk_subst : (Exp.Id.t, Exp.exp) Misc.plist -> Exp.subst
val mk_single_subst : Exp.Id.t -> Exp.exp -> Exp.subst
val mk_gensym_garb_subst : Exp.Id.t -> Exp.subst
val mk_gensym_garb_subst_idset : Exp.IdSet.t -> Exp.subst
val mk_gensym_garb_subst_idset2 : Exp.IdSet.t -> Exp.subst * Exp.subst
val existentials_rename_tonormal_sub : Exp.IdSet.t -> Exp.subst * Exp.subst
val existentials_rename_sub : Exp.IdSet.t -> Exp.subst
val map_sub : ('a -> 'a) -> 'a list -> 'a list
val map_idset : Exp.subst -> Exp.IdSet.t -> Exp.IdSet.t
val exp_no_s : string -> Exp.exp -> bool
module Dset :
sig
type t
val emp : Exp.Dset.t
val add : Exp.exp -> Exp.Dset.t -> Exp.Dset.t
val remove : Exp.exp -> Exp.Dset.t -> Exp.Dset.t
val mem : Exp.exp -> Exp.Dset.t -> bool
val from_list : Exp.exp list -> Exp.Dset.t
val to_list : Exp.Dset.t -> Exp.exp list
val inter : Exp.Dset.t -> Exp.Dset.t -> Exp.Dset.t
val union : Exp.Dset.t -> Exp.Dset.t -> Exp.Dset.t
val subset : Exp.Dset.t -> Exp.Dset.t -> bool
val partition :
(Exp.exp -> bool) -> Exp.Dset.t -> Exp.exp list * Exp.Dset.t
val filter : (Exp.exp -> bool) -> Exp.Dset.t -> Exp.Dset.t
val fold : (Exp.exp -> 'a -> 'a) -> Exp.Dset.t -> 'a -> 'a
val compare : Exp.Dset.t -> Exp.Dset.t -> int
val abs_compare : Exp.Dset.t -> Exp.Dset.t -> int
val map : Exp.subst -> Exp.Dset.t -> Exp.Dset.t
val no_s : string -> Exp.Dset.t -> bool
end
module Fld :
sig
type t
val emp : Exp.Fld.t
val one : Misc.component -> Exp.exp -> Exp.Fld.t
val two :
Misc.component -> Exp.exp -> Misc.component -> Exp.exp -> Exp.Fld.t
val from_list : (Misc.component * Exp.exp) list -> Exp.Fld.t
val inter : Exp.Fld.t -> Exp.Fld.t -> Exp.Fld.t
val inter_num : Exp.Fld.t -> Exp.Fld.t -> Exp.Fld.t
val diff : Exp.Fld.t -> Exp.Fld.t -> Exp.Fld.t
val common :
Exp.Fld.t -> Exp.Fld.t -> Exp.Fld.t * Exp.Fld.t * Exp.Fld.t
val union : Exp.Fld.t -> Exp.Fld.t -> Exp.Fld.t
val hasfld : Misc.component -> Exp.Fld.t -> bool
val try_get : Misc.component -> Exp.Fld.t -> Exp.exp option
val get : Misc.component -> Exp.Fld.t -> Exp.exp
val get_extend : Misc.component -> Exp.Fld.t -> Exp.exp * Exp.Fld.t
val set : Misc.component -> Exp.exp -> Exp.Fld.t -> Exp.Fld.t
val mem : Misc.component -> Exp.exp -> Exp.Fld.t -> bool
val containing : Exp.exp -> Exp.Fld.t -> Misc.component
val exists : (Misc.component -> Exp.exp -> bool) -> Exp.Fld.t -> bool
val filter :
(Misc.component -> Exp.exp -> bool) -> Exp.Fld.t -> Exp.Fld.t
val remove : Misc.component -> Exp.Fld.t -> Exp.Fld.t
val fold :
(Misc.component -> Exp.exp -> 'a -> 'a) -> Exp.Fld.t -> 'a -> 'a
val fold_val : (Exp.exp -> 'a -> 'a) -> Exp.Fld.t -> 'a -> 'a
val iter_val : (Exp.exp -> unit) -> Exp.Fld.t -> unit
val components_equal : Exp.Fld.t -> Exp.Fld.t -> Exp.exp * Exp.Fld.t
val subset : Exp.Fld.t -> Exp.Fld.t -> Exp.exp
val compare : Exp.Fld.t -> Exp.Fld.t -> int
val abs_compare : Exp.Fld.t -> Exp.Fld.t -> int
val map : Exp.subst -> Exp.Fld.t -> Exp.Fld.t
val no_s : string -> Exp.Fld.t -> bool
end
val pp_ident : Format.formatter -> Exp.Id.t -> unit
val pp_idset : Format.formatter -> Exp.IdSet.t -> unit
val pp_exp : Format.formatter -> Exp.exp -> unit
val pp_exp_list : Format.formatter -> Exp.exp list -> unit
val pp_fld : Format.formatter -> Exp.Fld.t -> unit
type idpool
val idpool_new : (string -> Exp.Id.t) -> string -> Exp.idpool
val idpool_combine : Exp.idpool -> 'a list -> ('a, Exp.exp) Misc.plist
val idpool_combine2 : Exp.idpool -> Exp.IdSet.t -> Exp.subst * Exp.subst
end