module Make: functor (Ext : EXT) -> sig end
Functor for constructing an equality set for theory specification T.
Updates and restrictions have the respective side effects as before methods.
type t
Representation of a set of equalities of the form rho |- x = a,
where x is a variable, a a non-variable term, and rho is
a justification of the equality x = a.
type ext
Extension field.
val eq : t -> t -> bool
Test for identity of two solution sets.
val pp : t Pretty.printer
Pretty-printing a solution set. If Eqs.pp_index is set
to true, then the dependency index is printed, too.
val empty : t
The empty equality set.
val is_empty : t -> bool
is_empty s holds iff s does not contain any equalities.
val is_dependent : t -> Term.t -> bool
is_dependent s x holds iff there is an a such that x = a is in s.
val is_independent : t -> Term.t -> bool
is_independent s x holds iff x is a variable in some a with
y = a in s.
val iter : (Fact.Equal.t -> unit) -> t -> unit
iter f s applies f e for each equality fact e in s.
The order of application is unspecified.
val fold : (Fact.Equal.t -> 'a -> 'a) -> t -> 'a -> 'a
fold f s acc applies f e for each equality e in s
and accumulates the result starting with acc. The order of
application is unspecified.
val for_all : (Fact.Equal.t -> bool) -> t -> bool
for_all f s checks if f e holds for all equalities e in s.
val exists : (Fact.Equal.t -> bool) -> t -> bool
exists f s checks if f e holds for all equalities e in s.
val to_list : t -> Fact.Equal.t list
to_list s builds up a list of equalities from the solved form s.
val equality : t -> Term.t -> Fact.Equal.t
equality s x yields an equality e of the form x = a with
justification rho if x is a dependent variable. Otherwise,
Not_found is raised.
val apply : t -> Jst.Eqtrans.t
apply s x yields (b, rho) if x = b in s with justification rho;
if x is not a dependent variable, Not_found is raised.
val find : t -> Jst.Eqtrans.t
find s x yields (b, rho) if x is a dependent variable in s
with x = b; otherwise, (x, refl) is returned with refl a
justification of x = x.
val inv : t -> Jst.Eqtrans.t
inv s a yields (x, rho) if rho |- x = a is in s with
justification rho.
val dep : t -> Term.t -> Term.Var.Set.t
dep s y returns all x such that x = a in s, and
the variable y occurs in a. In this case, we also say
that x is dependent on y.
val ext : t -> ext
Return the value of the extension field.
module Dep: sig end
Iterators over dependency index.
val restrict : t -> Term.t -> unit
restrict s x removes equalities of the form x = a in s.
type config = Partition.t * t
val update : config -> Fact.Equal.t -> unit
update s e updates s with a
new equality of the form, say, x = a.
Any x = b already in the state, is removed.
val diff : t -> t -> t
diff s1 s2 contains all equalities in s1 that are not in s2.
val copy : t -> t