From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 9 Oct 2006 16:33:24 +0000 (+0000)
Subject: Theorems from the library and from the context are indexed also in "unfolded"
X-Git-Tag: 0.4.95@7852~919
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4fdb66a6436a18128faff1b5b97637c6ffb61f34;p=helm.git

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 b4e074a64..4c1871388 100644
--- 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
 ;;