From d6175b9980808ff91f1299ca26a9a49a117169ca Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Thu, 6 Apr 2017 17:34:23 +0200
Subject: Fix a normalization hotspot in computation of constr keys.

Getting a key only needs to observe the root of a term. This hotspot was
observed in HoTT.
---
 library/keys.ml               |  4 ++--
 library/keys.mli              |  2 +-
 plugins/ltac/extratactics.ml4 | 12 ++++++++----
 pretyping/unification.ml      |  4 ++--
 4 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/library/keys.ml b/library/keys.ml
index 057dc3b65..c9e325ee5 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -114,11 +114,11 @@ let inKeys : key_obj -> obj =
 let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
-let constr_key c =
+let constr_key kind c =
   let open Globnames in 
   try 
     let rec aux k = 
-      match kind_of_term k with
+      match kind k with
       | Const (c, _) -> KGlob (ConstRef c)
       | Ind (i, u) -> KGlob (IndRef i)
       | Construct (c,u) -> KGlob (ConstructRef c)
diff --git a/library/keys.mli b/library/keys.mli
index 69668590d..6abac4de4 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -16,7 +16,7 @@ val declare_equiv_keys : key -> key -> unit
 val equiv_keys : key -> key -> bool
 (** Check equivalence of keys. *)
 
-val constr_key : Term.constr -> key option
+val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option
 (** Compute the head key of a term. *)
 
 val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b34afd51b..1ec52718a 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1087,10 +1087,14 @@ END
 (** library/keys *)
 
 VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
-| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ 
-  let it c = EConstr.Unsafe.to_constr (snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c)) in 
-  let k1 = Keys.constr_key (it c) in
-  let k2 = Keys.constr_key (it c') in
+| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
+  let get_key c =
+    let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+    let kind c = EConstr.kind evd c in
+    Keys.constr_key kind c
+  in
+  let k1 = get_key c in
+  let k2 = get_key c' in
     match k1, k2 with
     | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
     | _ -> () ]
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 91781a076..eb90dfbdb 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1739,7 +1739,7 @@ let keyed_unify env evd kop =
     | None -> fun _ -> true
     | Some kop ->
       fun cl ->
-	let kc = Keys.constr_key (EConstr.to_constr evd cl) in
+	let kc = Keys.constr_key (fun c -> EConstr.kind evd c) cl in
 	  match kc with
 	  | None -> false
 	  | Some kc -> Keys.equiv_keys kop kc
@@ -1749,7 +1749,7 @@ let keyed_unify env evd kop =
    Fails if no match is found *)
 let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
   let bestexn = ref None in
-  let kop = Keys.constr_key (EConstr.to_constr evd op) in
+  let kop = Keys.constr_key (fun c -> EConstr.kind evd c) op in
   let rec matchrec cl =
     let cl = strip_outer_cast evd cl in
     (try
-- 
cgit v1.2.3