X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=1f2c6be0e1704662c2c92fa46c51eb43a118c004;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=695e0cffdf293d823013e5148348a289fcd38175;hpb=46f19eadce5f3a11c0ae26934fd8d1b597906416;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 695e0cffd..1f2c6be0e 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -482,74 +482,55 @@ let empty = Cache.empty;;
 let total_parsing_time = ref 0.0
 
 let get_object_to_add uri =
- let filename = Http_getter.getxml' uri in
- let bodyfilename =
-   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 *)
-         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 = 
-   try 
-     let time = Unix.gettimeofday() in
-     let rc = CicParser.obj_of_xml uri filename bodyfilename in
-     total_parsing_time := 
-       !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 = 
+ try
+  let filename = Http_getter.getxml' uri in
+  let bodyfilename =
+    match UriManager.bodyuri_of_uri uri with
+       None -> None
+    |  Some bodyuri ->
+        if Http_getter.exists' bodyuri then
+          Some (Http_getter.getxml' bodyuri)
+        else
+          None
+  in
+  (* restarts the numbering of named universes (the ones inside the cic) *)
+  let _ = CicUniv.restart_numbering () in 
+  let obj = 
+    try 
+      let time = Unix.gettimeofday() in
+      let rc = CicParser.obj_of_xml uri filename bodyfilename in
+      total_parsing_time := 
+        !total_parsing_time +. ((Unix.gettimeofday()) -. time );
+      rc
+    with exn -> 
+      (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 = 
    (* FIXME: decomment this when the universes will be part of the library
-   try 
-     let filename_univ = 
-       Http_getter.getxml' (
-         UriManager.uri_of_string (
-           (UriManager.string_of_uri uri) ^ ".univ")) 
-     in
-       (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));
-       Inix.unlink
-     None,None
-     *)
-     (**********************************************
-       TASSI: should fail when universes will be ON
-     ***********************************************)
-     (Some CicUniv.empty_ugraph,None)
- in
-   cleanup();
-   obj,ugraph
+    try 
+      let filename_univ = 
+        Http_getter.getxml' (
+          UriManager.uri_of_string (
+            (UriManager.string_of_uri uri) ^ ".univ")) 
+      in
+        (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));
+        Inix.unlink
+      None,None
+      *)
+      (**********************************************
+        TASSI: should fail when universes will be ON
+      ***********************************************)
+      (Some CicUniv.empty_ugraph,None)
+  in
+  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 
@@ -665,31 +646,13 @@ let get_obj base_univ uri =
         o,(CicUniv.merge_ugraphs base_univ u)
 ;; 
 
-exception OnlyPutOfInductiveDefinitionsIsAllowed
-
-let put_inductive_definition uri (obj,ugraph) =
- match obj with
-    Cic.InductiveDefinition _ -> Cache.add_cooked uri (obj,ugraph)
-  | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
-;;
-
 let in_cache uri =
   Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 
-let add_type_checked_term uri (obj,ugraph) =
-  match obj with 
-      Cic.Constant (s,(Some bo),ty,ul,_) ->
-	Cache.add_cooked ~key:uri (obj,ugraph)
-    | _ -> 
-	assert false 
-;;
+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