auto rewritten with only one tail recursive function.

[helm.git] / components / tactics / autoCache.ml

diff --git a/components/tactics/autoCache.ml b/components/tactics/autoCache.ml
index 5fb4640d71e2c8308280a64e090c0bb5a32d6494..b12b26c054853d8288ddbc68d7e5e9dd93927c34 100644 (file)
--- a/components/tactics/autoCache.ml
+++ b/components/tactics/autoCache.ml
@@ -31,6 +31,10 @@ type cache_elem =
   | Notfound
 type cache = (Universe.universe * ((cache_key * cache_elem) list));;
 
+let debug = false;;
+let prerr_endline s = 
+  if debug then prerr_endline s else ()
+;;
 
 let cache_empty = (Universe.empty,[]);;
 
@@ -59,7 +63,10 @@ let cache_add_list (univ,cache) context terms_and_types =
   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
@@ -70,27 +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 =
+  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
-  (match cache_examine cache cache_key with
+  (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
@@ -103,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)