From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 7 Apr 2008 16:30:11 +0000 (+0000)
Subject: added invalidate to clear the cache and ease the comparison with the new kernel
X-Git-Tag: make_still_working~5417
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=92ff0c811f55b37004e2ee45dff0859c31857128;p=helm.git

added invalidate to clear the cache and ease the comparison with the new kernel
---

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml
index 8ae5c1b13..9875f17f6 100644
--- a/helm/software/components/cic_proof_checking/cicEnvironment.ml
+++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml
@@ -105,6 +105,7 @@ module Cache :
    val is_in_unchecked: UriManager.uri -> bool
    val is_in_cooked: UriManager.uri -> bool
    val list_all_cooked_uris: unit -> UriManager.uri list
+   val invalidate: unit -> unit
   end 
 =
   struct
@@ -143,6 +144,13 @@ module Cache :
     (* unchecked is used to store objects just fetched, nothing more. *)    
     let unchecked_list = ref [];;
 
+    let invalidate _ =
+      let l = HT.fold (fun k (o,g,gl) acc -> (k,(o,Some (g,gl)))::acc) cacheOfCookedObjects [] in
+      unchecked_list := l ;
+      frozen_list := [];
+      HT.clear cacheOfCookedObjects;
+    ;;
+
     let empty () = 
       HT.clear cacheOfCookedObjects;
       unchecked_list := [] ;
@@ -546,3 +554,7 @@ let list_obj () =
       debug_print (lazy "Who has removed the uri in the meanwhile?");
       raise Not_found
 ;;
+
+let invalidate _ = 
+   Cache.invalidate ()
+;;
diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.mli b/helm/software/components/cic_proof_checking/cicEnvironment.mli
index 55566a614..e449ade4a 100644
--- a/helm/software/components/cic_proof_checking/cicEnvironment.mli
+++ b/helm/software/components/cic_proof_checking/cicEnvironment.mli
@@ -133,4 +133,6 @@ val in_library: UriManager.uri -> bool
   (** total parsing time, only to benchmark the parser *)
 val total_parsing_time: float ref
 
+val invalidate: unit -> unit
+
 (* EOF *)