Big commit and major code clean-up:

[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 695e0cffdf293d823013e5148348a289fcd38175..86b8dd921a246969fb26df7636c10ff0c5edf479 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -482,74 +482,77 @@ 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
+ try
+  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 = 
    (* 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
+    cleanup();
+    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,24 +668,11 @@ 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 ||