X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoCache.ml;h=5fb4640d71e2c8308280a64e090c0bb5a32d6494;hb=e00d05ab58597620345c2fd49b84a23efa8db34c;hp=0b42391fa63beb345d941aa34a773562cdf8fb97;hpb=4996fef9a745a372717fbc20bd5f0eef7a08552b;p=helm.git

diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml
index 0b42391fa..5fb4640d7 100644
--- a/components/tactics/autoCache.ml
+++ b/components/tactics/autoCache.ml
@@ -23,72 +23,40 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module Codomain = struct 
-  type t = Cic.term 
-  let compare = Pervasives.compare 
-end
-module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
-type universe = TI.t
-(* (proof,ty) list *)
 type cache_key = Cic.term
 type cache_elem = 
   | Failed_in of int
   | Succeded of Cic.term
   | UnderInspection
   | Notfound
-type cache = (universe * ((cache_key * cache_elem) list));;
+type cache = (Universe.universe * ((cache_key * cache_elem) list));;
 
-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 cache_empty = (Universe.empty,[]);;
 
-let rec collapse_head_metas = function 
-  | Cic.Appl(a::l) -> 
-      let a' = collapse_head_metas a in
-      (match a' with
-	| Cic.Meta(n,m) -> Cic.Meta(n,m)
-	| t -> 	
-	    let l' = List.map collapse_head_metas l in
-	       Cic.Appl(t::l'))
-  | t -> t
-;;
-  
-let rec head t = 
-  let rec aux = function
-  | Cic.Prod(_,_,t) -> 
-      CicSubstitution.subst (Cic.Meta (-1,[])) (aux t)
-  | t -> t
-  in collapse_head_metas (aux t)
+let get_candidates (univ,_) ty = 
+  if Universe.key ty = ty then
+    Universe.get_candidates univ ty
+  else 
+    []
 ;;
 
-let index (univ,oldcache) key term =
-  prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
-  (TI.index univ key term,oldcache)
+let index (univ,cache) key term =
+  Universe.index univ key term,cache
 ;;
 
-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 index_term_and_unfolded_term (univ,cache) context t ty =
+  Universe.index_local_term univ context t ty, cache
 ;;
 
-let cache_add_list cache context terms_and_types =
-  List.fold_left  
-    (fun acc (term,ty) -> 
-       index_term_and_unfolded_term acc context term ty)
-    cache terms_and_types
+let cache_add_list (univ,cache) context terms_and_types =
+  let univ = 
+    List.fold_left
+      (fun univ (t,ty) -> 
+	 Universe.index_local_term univ context t ty)
+      univ terms_and_types  
+  in
+  univ, cache
 
 let cache_examine (_,oldcache) cache_key = 
   try List.assoc cache_key oldcache with Not_found -> Notfound
@@ -112,7 +80,10 @@ let cache_add_failure cache cache_key depth =
       assert false (* if succed it can't fail *)
 ;;
 let cache_add_success ((univ,_) as cache) cache_key proof =
-  TI.index univ cache_key proof,snd
+  (if Universe.key cache_key = cache_key then
+    Universe.index univ cache_key proof
+  else
+    univ),snd
   (match cache_examine cache cache_key with
   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
   | UnderInspection -> cache_replace cache cache_key (Succeded proof)