[WIP] equations environment using a union-find.

Olivier 4 months ago
parent 3d51f8eb5a
commit 00bf829884

@ -311,13 +311,78 @@ end (* Env *)
module IdTable = Hashtbl
module EqEnv : sig
module type EQUALITY_ENV = sig
type scope = int
val eq: variable S.structure -> variable S.structure -> scope option
end = struct
module EqUFEnv : EQUALITY_ENV = struct
type scope =
(* For each scope where an equality was introduced, we store a union-find
of type equality. There is no easy way to store the scope information
in the union-find. Indeed, we need to add (resp. remove) equality in the
union-find every time we enter (resp. exit) the scoping site of an
equality, and this may affect the scopes stored in the union-find. *)
(* When we check an equality, we find the lowest scope in which this equality
holds. To do this we traverse the array of union-find indexed by scope. *)
(* Our union-find data structure need a relatively efficient support for
copy, since we will copy it every time we enter a new equality scope. *)
module UF =
(* The nodes of our union-find are structures with rigid (but not flexible !)
variables as leaves. *)
type uf_store =
variable S.structure UF.store
(* Array of union-find data structures indexed by scope. *)
type t =
uf_store option Array.t
let empty () : t =
Array.make 8 None
(* When entering a new scope, we extend the array of union-find with a new
empty store. *)
let rec enter (s : scope) (env : t) : t =
let len = Array.length env in
if s < len then begin
env.(s) <- Some (UF.new_store ());
(* If the scope is out of bound, we double the size of the array and
try again. *)
let env' = Array.make (len * 2) None in
Array.blit env 0 env' 0 len;
enter s env'
(* Exiting a scope is just erasing the associated union-find. *)
let exit (s : scope) (env : t) : t =
assert (s < Array.length env);
env.(s) <- None;
(* We do not add redundant equalities. *)
let add_equality store s1 s2 =
(* Create new vertices for both [s1] and [s2]. *)
let v1 = UF.make store s1 in
let v2 = UF.make store s2 in
UF.union store v1 v2
let eq _ _ =
failwith "todo"
end (* EqUFEnv *)
module EqEnv : EQUALITY_ENV = struct
type scope =