OccursCheck.Make
This module traverses the data structure maintained by the unifier and offers an occurs check, that is, a cycle detection algorithm. It is parameterized by the term structure S
and by the unifier U
. Read-only access to the unifier's data structure suffices.
module S : sig ... end
module U : sig ... end
exception Cycle of U.variable
Cycle v
is raised by the occurs check.
val new_occurs_check : ( U.data -> bool ) -> U.variable -> unit
new_occurs_check is_young
initiates a cycle detection phase. It produces a function check
that can be applied to a number of roots. The function check
visits the vertices that are reachable from some root and that satisfy the user-supplied predicate is_young
. If a cycle is detected, then Cycle v
is raised, where v
is a vertex that participates in the cycle.
The function check
has internal state and records the vertices that it has visited, so no vertex is visited twice: the complexity of the occurs check is linear in the size of the graph fragment that is visited.