example:

[helm.git] / helm / software / components / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml
index 535869b3525954d723c854827fe20a1f265073c6..ec12c8d01c80a790fec70c836ea5efa7cc4e1d3e 100644 (file)
--- 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,15 @@ 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 := 
+        HExtlib.list_uniq ~eq:(fun (x,_) (y,_) -> UriManager.eq x y)
+        (List.sort (fun (x,_) (y,_) -> UriManager.compare x y) (l @ !unchecked_list));
+      frozen_list := [];
+      HT.clear cacheOfCookedObjects;
+    ;;
+
     let empty () = 
       HT.clear cacheOfCookedObjects;
       unchecked_list := [] ;
@@ -217,6 +227,7 @@ module Cache :
            if List.mem_assq uri !frozen_list then
              (* CIRCULAR DEPENDENCY DETECTED, print the error and raise *)
              begin
+(*
                prerr_endline "\nCircularDependency!\nfrozen list: \n";
                List.iter (
                  fun (u,(_,o)) ->
@@ -224,6 +235,7 @@ module Cache :
                    let univ = if o = None then "NO_UNIV" else "" in
                    prerr_endline (su^" "^univ)) 
                  !frozen_list;
+*)
                raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
              end
            else
@@ -364,7 +376,7 @@ let get_object_to_add uri =
     match UriManager.bodyuri_of_uri uri with
        None -> None
     |  Some bodyuri ->
-        if Http_getter.exists' bodyuri then
+        if Http_getter.exists' ~local:false bodyuri then
           Some (Http_getter.getxml' bodyuri)
         else
           None
@@ -457,13 +469,13 @@ let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
     let o,u,l = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
     if trust && trust_obj uri then
       (* trusting means that we will fetch cook it on the fly *)
       let o,u,l = add_trusted_uri_to_cache uri in
-        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
     else
       (* we don't trust the uri, so we fail *)
       begin
@@ -491,14 +503,14 @@ let get_cooked_obj ?trust base_ugraph uri =
  *)
 let is_type_checked ?(trust=true) base_ugraph uri =
   try 
-    let o,u,_ = Cache.find_cooked uri in
-      CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)))
+    let o,u,l = Cache.find_cooked uri in
+      CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
   with Not_found ->
     (* this should return UncheckedObj *)
     if trust && trust_obj uri then
       (* trusting means that we will fetch cook it on the fly *)
-      let o,u,_ = add_trusted_uri_to_cache uri in
-        CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+      let o,u,l = add_trusted_uri_to_cache uri in
+        CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
     else
       let o,u,_ = find_or_add_to_unchecked uri in
       Cache.unchecked_to_frozen uri;
@@ -511,12 +523,12 @@ let is_type_checked ?(trust=true) base_ugraph uri =
 let get_obj base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
-    let o,u,_ = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+    let o,u,l = Cache.find_cooked uri in
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
-      let o,u,_ = find_or_add_to_unchecked uri in
-        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+      let o,u,l = find_or_add_to_unchecked uri in
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 ;; 
 
 let in_cache uri =
@@ -525,7 +537,7 @@ let in_cache uri =
 let add_type_checked_obj uri (obj,ugraph,univlist) =
  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
 
-let in_library uri = in_cache uri || Http_getter.exists' uri
+let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
 
 let remove_obj = Cache.remove
   
@@ -544,3 +556,7 @@ let list_obj () =
       debug_print (lazy "Who has removed the uri in the meanwhile?");
       raise Not_found
 ;;
+
+let invalidate _ = 
+   Cache.invalidate ()
+;;