From ad2e11471dbfc0894b4fdfedd895e7f0a75bd930 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 24 Sep 2014 11:16:11 +0200
Subject: First version of keyed subterm selection in unification.

---
 library/keys.ml       | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 library/keys.mli      | 15 +++++++++++++++
 library/library.mllib |  1 +
 3 files changed, 62 insertions(+)
 create mode 100644 library/keys.ml
 create mode 100644 library/keys.mli

(limited to 'library')

diff --git a/library/keys.ml b/library/keys.ml
new file mode 100644
index 0000000000..5c295a385f
--- /dev/null
+++ b/library/keys.ml
@@ -0,0 +1,46 @@
+open Globnames
+open Term
+open Libobject
+
+(* Union-find structure for references to be considered equivalent *)
+
+module RefUF = Unionfind.Make(Refset)(Refmap)
+
+let keys = (* Summary.ref ( *)RefUF.create ()(* ) ~name:"Keys_decl" *)
+
+let add_key k v = RefUF.union k v keys
+
+let equiv_keys k k' = RefUF.find k keys == RefUF.find k' keys
+
+(** Registration of keys as an object *)
+
+let load_key _ (_,(ref,ref')) =
+  add_key ref ref'
+
+let cache_key o =
+  load_key 1 o
+
+let subst_key (subst,(ref,ref')) =
+  (subst_global_reference subst ref,
+   subst_global_reference subst ref')
+
+let discharge_key (_,refs) =
+  match refs with 
+  | VarRef _, _ | _, VarRef _ -> None
+  | ref, ref' -> Some (pop_global_reference ref, pop_global_reference ref')
+
+let rebuild_key (ref,ref') = (ref, ref')
+
+type key_obj = global_reference * global_reference
+
+let inKeys : key_obj -> obj =
+  declare_object {(default_object "KEYS") with
+    cache_function = cache_key;
+    load_function = load_key;
+    subst_function = subst_key;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_key;
+    rebuild_function = rebuild_key }
+
+let declare_keys ref ref' =
+  Lib.add_anonymous_leaf (inKeys (ref,ref'))
diff --git a/library/keys.mli b/library/keys.mli
new file mode 100644
index 0000000000..4e6a803e4d
--- /dev/null
+++ b/library/keys.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Globnames
+
+val declare_keys : global_reference -> global_reference -> unit
+(** Declare two keys as being equivalent. *)
+
+val equiv_keys : global_reference -> global_reference -> bool
+(** Check equivalence of keys. *)
diff --git a/library/library.mllib b/library/library.mllib
index 6a58a1057b..04244160bb 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -17,3 +17,4 @@ Goptions
 Decls
 Heads
 Assumptions
+
-- 
cgit v1.2.3