Keyed unification option, compiling the whole standard library

(but deactivated still).

Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.

Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:

Declare Equivalent Keys f g.

This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.

For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.

INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.

3 files changed, 79 insertions, 43 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index cbbb2cea9..d88d6f106 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -542,17 +542,9 @@ let discharge_implicits (_,(req,l)) =
   | ImplInteractive (ref,flags,exp) ->
     (try
       let vars = section_segment_of_reference ref in
-      (* let isproj =  *)
-      (* 	 match ref with *)
-      (* 	 | ConstRef cst -> is_projection cst (Global.env ()) *)
-      (* 	 | _ -> false *)
-      (* in *)
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
-      let l' = 
-	(* if isproj then [ref',snd (List.hd l)] *)
-	(* else *)
-	  [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
@@ -560,10 +552,7 @@ let discharge_implicits (_,(req,l)) =
       let con' = pop_con con in
       let vars,_,_ = section_segment_of_constant con in
       let extra_impls = impls_of_context vars in
-      let newimpls = 
-	(* if is_projection con (Global.env()) then (snd (List.hd l)) *)
-	(* else *) List.map (add_section_impls vars extra_impls) (snd (List.hd l))
-      in
+      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
       let l' = [ConstRef con',newimpls] in
 	Some (ImplConstant (con',flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
diff --git a/library/keys.ml b/library/keys.ml
index c661e67fb..e4af0380b 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -1,8 +1,17 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Keys for unification and indexing *)
+
 open Globnames
 open Term
 open Libobject
 
-
 type key = 
   | KGlob of global_reference
   | KLam 
@@ -51,16 +60,23 @@ end
 module Keymap = HMap.Make(KeyOrdered)
 module Keyset = Keymap.Set
 
-(* Union-find structure for references to be considered equivalent *)
+(* Mapping structure for references to be considered equivalent *)
+
+type keys = Keyset.t Keymap.t
 
-module KeyUF = Unionfind.Make(Keyset)(Keymap)
+let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
 
-let keys = (* Summary.ref ( *)KeyUF.create ()(* ) ~name:"Keys_decl" *)
+let add_kv k v m =
+  try Keymap.modify k (fun k' vs -> Keyset.add v vs) m
+  with Not_found -> Keymap.add k (Keyset.singleton v) m
 
-let add_keys k v = KeyUF.union k v keys
+let add_keys k v = 
+  keys := add_kv k v (add_kv v k !keys)
 
 let equiv_keys k k' =
-  k == k' || KeyUF.find k keys == KeyUF.find k' keys
+  k == k' || KeyOrdered.equal k k' ||
+    try Keyset.mem k' (Keymap.find k !keys)
+    with Not_found -> false
 
 (** Registration of keys as an object *)
 
@@ -79,8 +95,8 @@ let subst_keys (subst,(k,k')) =
   (subst_key subst k, subst_key subst k')
 
 let discharge_key = function
-  | KGlob (VarRef _) -> None
-  | KGlob g -> Some (KGlob (pop_global_reference g))
+  | KGlob g when Lib.is_in_section g ->
+    if isVarRef g then None else Some (KGlob (pop_global_reference g))
   | x -> Some x
 
 let discharge_keys (_,(k,k')) =
@@ -101,26 +117,54 @@ let inKeys : key_obj -> obj =
     discharge_function = discharge_keys;
     rebuild_function = rebuild_keys }
 
-let declare_keys ref ref' =
+let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
-let rec constr_key c =
+let constr_key c =
   let open Globnames in 
-  match kind_of_term c with
-  | Const (c, _) -> KGlob (ConstRef c)
-  | Ind (i, u) -> KGlob (IndRef i)
-  | Construct (c,u) -> KGlob (ConstructRef c)
-  | Var id -> KGlob (VarRef id)
-  | App (f, _) -> constr_key f
-  | Proj (p, _) -> KGlob (ConstRef p)
-  | Cast (p, _, _) -> constr_key p
-  | Lambda _ -> KLam 
-  | Prod _ -> KProd
-  | Case _ -> KCase
-  | Fix _ -> KFix
-  | CoFix _ -> KCoFix
-  | Rel _ -> KRel
-  | Meta _ -> KMeta
-  | Evar _ -> KEvar
-  | Sort _ -> KSort 
-  | LetIn _ -> KLet
+  try 
+    let rec aux k = 
+      match kind_of_term k with
+      | Const (c, _) -> KGlob (ConstRef c)
+      | Ind (i, u) -> KGlob (IndRef i)
+      | Construct (c,u) -> KGlob (ConstructRef c)
+      | Var id -> KGlob (VarRef id)
+      | App (f, _) -> aux f
+      | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p))
+      | Cast (p, _, _) -> aux p
+      | Lambda _ -> KLam 
+      | Prod _ -> KProd
+      | Case _ -> KCase
+      | Fix _ -> KFix
+      | CoFix _ -> KCoFix
+      | Rel _ -> KRel
+      | Meta _ -> raise Not_found
+      | Evar _ -> raise Not_found
+      | Sort _ -> KSort 
+      | LetIn _ -> KLet
+    in Some (aux c)
+  with Not_found -> None
+
+open Pp
+
+let pr_key pr_global = function
+  | KGlob gr -> pr_global gr
+  | KLam -> str"Lambda"
+  | KLet -> str"Let"
+  | KProd -> str"Product"
+  | KSort -> str"Sort"
+  | KEvar -> str"Evar"
+  | KCase -> str"Case"
+  | KFix -> str"Fix"
+  | KCoFix -> str"CoFix"
+  | KRel -> str"Rel"
+  | KMeta -> str"Meta"
+
+let pr_keyset pr_global v = 
+  prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
+
+let pr_mapping pr_global k v = 
+  pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v
+
+let pr_keys pr_global =
+  Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt())
diff --git a/library/keys.mli b/library/keys.mli
index 87ba45558..36789c83b 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -10,11 +10,14 @@ open Globnames
 
 type key
 
-val declare_keys : key -> key -> unit
+val declare_equiv_keys : key -> key -> unit
 (** Declare two keys as being equivalent. *)
 
 val equiv_keys : key -> key -> bool
 (** Check equivalence of keys. *)
 
-val constr_key : Term.constr -> key
+val constr_key : Term.constr -> key option
 (** Compute the head key of a term. *)
+
+val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
+(** Pretty-print the mapping *)