Theorems from the library and from the context are indexed also in "unfolded"

version.

diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml
index b4e074a6450604cade8197f00a8f0df01520547e..4c18713888d4e789421474fe092759d3f4c4211c 100644 (file)
--- a/components/tactics/autoCache.ml
+++ b/components/tactics/autoCache.ml
@@ -43,10 +43,18 @@ let cache_empty = (TI.empty,[]);;
 let get_candidates (univ,_) ty = 
   S.elements (TI.retrieve_unifiables univ ty)
 ;;
+
+let rec unfold context = function
+  | Cic.Prod(name,s,t) -> 
+      let t' = unfold ((Some (name,Cic.Decl s))::context) t in
+       Cic.Prod(name,s,t')     
+  | t -> ProofEngineReduction.unfold context t
+  
 let rec head = function 
   | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
   | t -> t
 ;;
+
 let index ((univ,oldcache) as cache) key term =
   match key with
   | Cic.Meta _ -> cache
@@ -54,40 +62,54 @@ let index ((univ,oldcache) as cache) key term =
       prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
       (TI.index univ key term,oldcache)
 ;;
+
+let index_term_and_unfolded_term cache context t ty =
+  let key = head ty in
+  let cache = index cache key t in
+  try  
+    let key = head (unfold context ty) in
+    index cache key t
+  with ProofEngineTypes.Fail _ -> cache
+;;
+
 let cache_add_library dbd proof gl cache = 
   let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
   let terms = List.map CicUtil.term_of_uri univ in
   let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in
   List.fold_left 
     (fun acc term -> 
+      (* 
       let key = head (tyof term) in
-      index acc key term)
+      index acc key term
+      *)
+      index_term_and_unfolded_term acc [] term (tyof term))
     cache terms
 ;;
-let cache_add_context ctx metasenv cache =  
+let cache_add_context context metasenv cache =  
   let tail = function [] -> [] | h::tl -> tl in
   let rc,_,_ = 
     List.fold_left 
     (fun (acc,i,ctx) ctxentry ->
       match ctxentry with
       | Some (_,Cic.Decl t) -> 
-          let key = CicSubstitution.lift i (head t) in
+          let ty = CicSubstitution.lift i t in
           let elem = Cic.Rel i in
-          index acc key elem, i+1, tail ctx
+         index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
+          (* index acc key elem, i+1, tail ctx *)
       | Some (_,Cic.Def (_,Some t)) ->
-          let key = CicSubstitution.lift i (head t) in
+          let ty = CicSubstitution.lift i t in
           let elem = Cic.Rel i in
-          index acc key elem, i+1, tail ctx
+         index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
       | Some (_,Cic.Def (t,None)) ->
           let ctx = tail ctx in 
-          let key,_ = 
-            CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph
+          let ty = 
+           CicSubstitution.lift i
+              (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph))
           in
           let elem = Cic.Rel i in
-          let key = CicSubstitution.lift i (head key) in
-          index acc key elem, i+1, ctx
+         index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
       |  _ -> acc,i+1,tail ctx)
-    (cache,1,ctx) ctx
+    (cache,1,context) context
   in
   rc
 ;;