...

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 86b8dd921a246969fb26df7636c10ff0c5edf479..4a62aaa24741d672e46695cb237ec718557424a3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -430,18 +430,18 @@ module Cache :
               frozen_list := List.remove_assoc uri !frozen_list;
               frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
           | Some g -> 
-              debug_print (
+              debug_print (lazy (
                 "You are probably hacking an object already hacked or an"^
                 " object that has the universe file but is not"^
-                " yet committed.");
+                " yet committed."));
               assert false
      with
         Not_found -> 
-          debug_print (
+          debug_print (lazy (
             "You are hacking an object that is not in the"^
             " frozen_list, this means you are probably generating an"^
             " universe file for an object that already"^
-             " as an universe file");
+             " as an universe file"));
           assert false
    ;;
 
@@ -460,7 +460,11 @@ module Cache :
      if !frozen_list <> [] then
        failwith "CicEnvironment.remove while type checking"
      else
-       HT.remove cacheOfCookedObjects uri 
+      begin
+       HT.remove cacheOfCookedObjects uri;
+       unchecked_list :=
+        List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
+      end
    ;;
    
    let  list_all_cooked_uris () =
@@ -488,30 +492,11 @@ let get_object_to_add uri =
     match UriManager.bodyuri_of_uri uri with
        None -> None
     |  Some bodyuri ->
-        try
-         ignore (Http_getter.resolve' bodyuri) ;
-         (* The body exists ==> it is not an axiom *)
-         Some (Http_getter.getxml' bodyuri)
-        with
-         Http_getter_types.Key_not_found _ ->
-          (* The body does not exist ==> we consider it an axiom *)
+        if Http_getter.exists' bodyuri then
+          Some (Http_getter.getxml' bodyuri)
+        else
           None
   in
-  let cleanup () =
-    Unix.unlink filename ;
-    (*
-      begin
-        match filename_univ with
-          Some f -> Unix.unlink f
-        | None -> ()
-      end;
-    *)
-    begin
-      match bodyfilename with
-          Some f -> Unix.unlink f
-        | None -> ()
-    end 
-  in
   (* restarts the numbering of named universes (the ones inside the cic) *)
   let _ = CicUniv.restart_numbering () in 
   let obj = 
@@ -522,13 +507,12 @@ let get_object_to_add uri =
         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
       rc
     with exn -> 
-      cleanup ();
       (match exn with
       | CicParser.Getter_failure ("key_not_found", uri) ->
           raise (Object_not_found (UriManager.uri_of_string uri))
       | _ -> raise exn)
   in
- let ugraph,filename_univ = 
+  let ugraph,filename_univ = 
    (* FIXME: decomment this when the universes will be part of the library
     try 
       let filename_univ = 
@@ -539,8 +523,8 @@ let get_object_to_add uri =
         (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
     with Failure s ->
       
-      debug_print (
-        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
+      debug_print (lazy (
+        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
         Inix.unlink
       None,None
       *)
@@ -549,10 +533,8 @@ let get_object_to_add uri =
       ***********************************************)
       (Some CicUniv.empty_ugraph,None)
   in
-    cleanup();
-    obj,ugraph
- with
-  Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
+  obj,ugraph
+ with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
 ;;
  
 (* this is the function to fetch the object in the unchecked list and 
@@ -570,21 +552,21 @@ let find_or_add_to_unchecked uri =
 let set_type_checking_info ?(replace_ugraph=None) uri =
 (*
   if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
-    debug_print (
+    debug_print (lazy (
       "?replace_ugraph must be None if you are not committing an "^
       "object that has a universe graph associated "^
-      "(can happen only in the fase of universes graphs generation).");
+      "(can happen only in the fase of universes graphs generation)."));
     assert false
   else
 *)
   match Cache.can_be_cooked uri, replace_ugraph with
   | true, Some _
   | false, None ->
-      debug_print (
+      debug_print (lazy (
         "?replace_ugraph must be (Some ugraph) when committing an object that "^
         "has no associated universe graph. If this is in make_univ phase you "^
         "should drop this exception and let univ_make commit thi object with "^
-        "proper arguments");
+        "proper arguments"));
       assert false
   | _ ->
       (match replace_ugraph with 
@@ -620,7 +602,7 @@ let get_cooked_obj ?(trust=true) base_univ uri =
     else
       (* we don't trust the uri, so we fail *)
       begin
-        debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+        debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
         raise Not_found
       end
       
@@ -674,12 +656,7 @@ let in_cache uri =
 let add_type_checked_obj uri (obj,ugraph) =
  Cache.add_cooked ~key:uri (obj,ugraph)
 
-let in_library uri =
-  in_cache uri ||
-  (try
-    ignore (Http_getter.resolve' uri);
-    true
-  with Http_getter_types.Key_not_found _ -> false)
+let in_library uri = in_cache uri || Http_getter.exists' uri
 
 let remove_obj = Cache.remove
   
@@ -695,6 +672,6 @@ let list_obj () =
     (list_uri ())
   with
     Not_found -> 
-      debug_print "Who has removed the uri in the meanwhile?";
+      debug_print (lazy "Who has removed the uri in the meanwhile?");
       raise Not_found
 ;;