Functor Solution.Make


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.
Parameters:
Ext : Solution.EXT


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.
Parameters:
? : t
? : t
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.
Parameters:
? : t
val is_dependent : t -> Term.t -> bool
is_dependent s x holds iff there is an a such that x = a is in s.
Parameters:
? : t
? : Term.t
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.
Parameters:
? : t
? : Term.t
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.
Parameters:
? : Fact.Equal.t -> unit
? : t
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.
Parameters:
? : Fact.Equal.t -> 'a -> 'a
? : t
? : 'a
val for_all : (Fact.Equal.t -> bool) -> t -> bool
for_all f s checks if f e holds for all equalities e in s.
Parameters:
? : Fact.Equal.t -> bool
? : t
val exists : (Fact.Equal.t -> bool) -> t -> bool
exists f s checks if f e holds for all equalities e in s.
Parameters:
? : Fact.Equal.t -> bool
? : t
val to_list : t -> Fact.Equal.t list
to_list s builds up a list of equalities from the solved form s.
Parameters:
? : t
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.
Parameters:
? : t
? : Term.t
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.
Parameters:
? : t
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.
Parameters:
? : t
val inv : t -> Jst.Eqtrans.t
inv s a yields (x, rho) if rho |- x = a is in s with justification rho.
Parameters:
? : t
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.
Parameters:
? : t
? : Term.t
val ext : t -> ext
Return the value of the extension field.
Parameters:
? : t
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.
Parameters:
? : t
? : Term.t

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.
Parameters:
? : config
? : Fact.Equal.t
val diff : t -> t -> t
diff s1 s2 contains all equalities in s1 that are not in s2.
Parameters:
? : t
? : t
val copy : t -> t
Parameters:
? : t