X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FautoCache.ml;h=b12b26c054853d8288ddbc68d7e5e9dd93927c34;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=4c18713888d4e789421474fe092759d3f4c4211c;hpb=4fdb66a6436a18128faff1b5b97637c6ffb61f34;p=helm.git

diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml
index 4c1871388..b12b26c05 100644
--- a/components/tactics/autoCache.ml
+++ b/components/tactics/autoCache.ml
@@ -23,99 +23,50 @@
  * 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 debug = false;;
+let prerr_endline s = 
+  if debug then prerr_endline s else ()
 ;;
 
-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 cache_empty = (Universe.empty,[]);;
 
-let index ((univ,oldcache) as cache) key term =
-  match key with
-  | Cic.Meta _ -> cache
-  | _ -> 
-      prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
-      (TI.index univ key term,oldcache)
+let get_candidates (univ,_) ty = 
+  if Universe.key ty = ty then
+    Universe.get_candidates univ ty
+  else 
+    []
 ;;
 
-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 (univ,cache) key term =
+  Universe.index univ key term,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_term_and_unfolded_term acc [] term (tyof term))
-    cache terms
+let index_term_and_unfolded_term (univ,cache) context t ty =
+  Universe.index_local_term univ context t ty, 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 ty = CicSubstitution.lift i t in
-          let elem = Cic.Rel i in
-	  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 ty = CicSubstitution.lift i t in
-          let elem = Cic.Rel i in
-	  index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
-      | Some (_,Cic.Def (t,None)) ->
-          let ctx = tail ctx in 
-          let ty = 
-	    CicSubstitution.lift i
-              (fst (CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph))
-          in
-          let elem = Cic.Rel i in
-	  index_term_and_unfolded_term acc context elem ty, i+1, tail ctx
-      |  _ -> acc,i+1,tail ctx)
-    (cache,1,context) context
+
+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
-  rc
-;;
+  univ, cache
 
 let cache_examine (_,oldcache) cache_key = 
-  try List.assoc cache_key oldcache with Not_found -> Notfound
+  prerr_endline ("examine : " ^ CicPp.ppterm cache_key);
+  try List.assoc cache_key oldcache with Not_found -> 
+    prerr_endline "notfound";
+    Notfound
 ;;
 let cache_replace (univ,oldcache) key v =
   let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
@@ -126,24 +77,46 @@ let cache_remove (univ,oldcache) key =
   univ,oldcache
 ;;
 let cache_add_failure cache cache_key depth =
+  prerr_endline 
+    ("CACHE: ADD FAIL " ^ CicPp.ppterm cache_key ^ 
+      " depth: " ^ string_of_int depth);
   match cache_examine cache cache_key with
   | Failed_in i when i > depth -> cache
   | Notfound  
   | Failed_in _ 
   | UnderInspection -> cache_replace cache cache_key (Failed_in depth)
-  | Succeded t -> 
+  | Succeded t -> cache 
+                  (*
       prerr_endline (CicPp.ppterm t);
-      assert false (* if succed it can't fail *)
+      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
-  (match cache_examine cache cache_key with
+  let u_key = Universe.key cache_key in
+  if u_key <> cache_key then
+    Universe.index univ u_key proof, snd cache
+  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)
+    | Succeded t -> (* we may decide to keep the smallest proof *) cache
+    | Notfound -> cache_replace cache cache_key (Succeded proof))
+(*
+  (if Universe.key cache_key = cache_key then
+    Universe.index univ cache_key proof
+  else
+    univ),snd
+  (prerr_endline ("CACHE: ADD SUCCESS" ^ CicPp.ppterm cache_key);
+  match cache_examine cache cache_key with
   | Failed_in _ -> cache_replace cache cache_key (Succeded proof)
   | UnderInspection -> cache_replace cache cache_key (Succeded proof)
   | Succeded t -> (* we may decide to keep the smallest proof *) cache
   | Notfound -> cache_replace cache cache_key (Succeded proof))
 ;;
+*)
 let cache_add_underinspection ((univ,oldcache) as cache) cache_key depth =
+  prerr_endline ("CACHE: ADD INSPECTING" ^ CicPp.ppterm cache_key);
   match cache_examine cache cache_key with
   | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
   | Notfound -> univ,(cache_key,UnderInspection)::oldcache
@@ -156,16 +129,19 @@ let cache_print context (_,oldcache) =
   String.concat "\n" 
     (HExtlib.filter_map 
       (function 
-        | (k,Succeded _) -> Some (CicPp.pp k names)
+        | (k,Succeded _) -> Some ("CACHE SUCCESS: " ^ CicPp.pp k names)
         | _ -> None)
       oldcache)
 ;;
 let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
+  prerr_endline ("CACHE: REMOVE INSPECTING" ^ CicPp.ppterm cache_key);
   match cache_examine cache cache_key with
   | Notfound 
+  | Failed_in _ (* -> assert false  *)
   | UnderInspection ->  cache_remove cache cache_key
-  | Failed_in _ -> assert false
-  | Succeded _ -> assert false (* it must be a new goal *)
+  | Succeded _ -> cache (* 
+      prerr_endline (CicPp.ppterm cache_key);            
+      assert false (* it must be a new goal *) *)
 ;;
 let cache_size (_,oldcache) = 
   List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)