Previous  Up  Next

Module V


module V: sig  end
remove the inverse of x.

type t = {
   find : (Term.t * Fact.justification option) Term.Map.t;
   inv : Term.Set.t Term.Map.t;
   removable : Term.Set.t;
} 
val eq : t -> t -> bool
Parameters:
s : t
t : t
 
val apply : t -> Term.Map.key -> Term.t * Fact.justification option
Parameters:
s : t
?? : Term.Map.key
 
val find : t -> Term.Map.key -> Term.Map.key * 'a option
Parameters:
s : t
x : Term.Map.key
 
val equality : t -> Term.Map.key -> Fact.equal
Parameters:
s : t
x : Term.Map.key
 
val inv : t -> Term.Map.key -> Term.Set.t
Parameters:
s : t
x : Term.Map.key
 
val removable : t -> Term.Set.t
Parameters:
s : t
 
val union : Term.Set.elt -> Term.Map.key -> Fact.justification option -> t -> t
Parameters:
x : Term.Set.elt
y : Term.Map.key
prf : Fact.justification option
s : t
 
val restrict : Term.Map.key -> t -> t
Parameters:
x : Term.Map.key
s : t
 
val gc : (Term.Set.elt -> bool) -> t -> t
Parameters:
f : Term.Set.elt -> bool
s : t
 
val is_equal : t -> Term.Map.key -> Term.Map.key -> bool
Variable equality modulo s.
Parameters:
s : t
x : Term.Map.key
y : Term.Map.key
 
val empty : t
The empty context.
val is_empty : t -> bool
Parameters:
s : t
 
val fold : t -> (Term.Set.elt -> 'a -> 'a) -> Term.Map.key -> 'a -> 'a
Starting from the canonical representative x' = find s x, the function f is applied to each y in inv s x' and the results are accumulated.
Parameters:
s : t
f : Term.Set.elt -> 'a -> 'a
x : Term.Map.key
 
val merge : Fact.equal -> t -> Term.Set.t * t
Adding a binding a |-> b to a context s.
Parameters:
e : Fact.equal
s : t
 
val ext : t -> Term.Map.key -> Term.Set.t
Extension of the equivalence class for x.
Parameters:
s : t
x : Term.Map.key

Iteration.

val iter : t -> (Term.Set.elt -> 'a) -> Term.Map.key -> unit
Parameters:
s : t
f : Term.Set.elt -> 'a
x : Term.Map.key
 
val exists : t -> (Term.Set.elt -> bool) -> Term.Map.key -> bool
Parameters:
s : t
p : Term.Set.elt -> bool
x : Term.Map.key
 
val for_all : t -> (Term.Set.elt -> bool) -> Term.Map.key -> bool
Parameters:
s : t
p : Term.Set.elt -> bool
x : Term.Map.key
 
exception Found
Choose an element satisfying some property.
val choose : t -> (Term.Set.elt -> 'a option) -> Term.Map.key -> 'a
Parameters:
s : t
p : Term.Set.elt -> 'a option
x : Term.Map.key
 
val canrepr : t -> Term.Set.t
Set of canonical representatives with non-trivial equivalence classes. These are the variables occurring in the codomain of find which are not themselves in the domain of find.
Parameters:
s : t
 
val partition : t -> Term.Set.t Term.Map.t
Representation of the equivalence classes as a map with the canonical representatives as domain and the corresponding extensions in the codomain. The following is not terribly efficient.
Parameters:
s : t
 
val pp : Format.formatter -> t -> unit
Pretty-printing.
Parameters:
fmt : Format.formatter
s : t