X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=695e0cffdf293d823013e5148348a289fcd38175;hb=f7759f86b755f4f7dc2b23edd52ed4d2e5c028fe;hp=6ad00d7643d948e2d8144a8b05b339893caa8729;hpb=531db3a11c2faa55884c490443d56ac308f9ac9f;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 6ad00d764..695e0cffd 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -44,7 +44,7 @@ let cleanup_tmp = true;;
 let trust = ref  (fun _ -> true);;
 let set_trust f = trust := f
 let trust_obj uri = !trust uri
-
+let debug_print = fun _ -> ()
 
 (* ************************************************************************** *
                                    TYPES 
@@ -165,6 +165,9 @@ module Cache :
               ) l
             in
              C.Meta(i,l')
+         | C.Sort (C.Type u) -> 
+             CicUniv.assert_univ u;
+             C.Sort (C.Type (CicUniv.recons_univ u))
          | C.Sort _ as t -> t
          | C.Implicit _ as t -> t
          | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
@@ -214,7 +217,7 @@ module Cache :
             in
              C.CoFix (i, liftedfl)
       in
-      function
+      function 
          C.Constant (name,bo,ty,params,attrs) ->
            let bo' =
              match bo with
@@ -299,7 +302,7 @@ module Cache :
             (***********************************************
                TSSI: FIXME add channel stuff for universes
             ************************************************)
-           (restore_uris v,u))
+           (restore_uris v, CicUniv.recons_graph u))
        restored
     ;;
 
@@ -393,6 +396,7 @@ module Cache :
 	    None -> 
 	      assert false (* only NON dummy universes can be committed *)
 	  | Some g ->
+              CicUniv.assert_univs_have_uri g;
 	      frozen_list := List.remove_assq uri !frozen_list ;
 	      HT.add cacheOfCookedObjects uri (obj,g) 
     with
@@ -426,14 +430,14 @@ module Cache :
 	       frozen_list := List.remove_assoc uri !frozen_list;
 	       frozen_list := (uri,(o,Some real_ugraph))::!frozen_list;
 	   | Some g -> 
-	       prerr_endline (
+	       debug_print (
 		 "You are probably hacking an object already hacked or an"^
 		 " object that has the universe file but is not"^
 		 " yet committed.");
 	       assert false
      with
 	 Not_found -> 
-	   prerr_endline (
+	   debug_print (
 	     "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"^
@@ -475,6 +479,8 @@ let dump_to_channel = Cache.dump_to_channel;;
 let restore_from_channel = Cache.restore_from_channel;;
 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 =
@@ -505,12 +511,15 @@ let get_object_to_add uri =
        | None -> ()
    end 
  in
- (* this brakes something : 
-  *   let _ = CicUniv.restart_numbering () in 
-  *)
+ (* restarts the numbering of named universes (the ones inside the cic) *)
+ let _ = CicUniv.restart_numbering () in 
  let obj = 
    try 
-     CicParser.obj_of_xml filename bodyfilename 
+     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
@@ -529,7 +538,7 @@ let get_object_to_add uri =
        (Some (CicUniv.ugraph_of_xml filename_univ),Some filename_univ)
    with Failure s ->
      
-     prerr_endline (
+     debug_print (
        "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri));
        Inix.unlink
      None,None
@@ -558,7 +567,7 @@ 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
-    prerr_endline (
+    debug_print (
       "?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).");
@@ -568,7 +577,7 @@ let set_type_checking_info ?(replace_ugraph=None) uri =
   match Cache.can_be_cooked uri, replace_ugraph with
   | true, Some _
   | false, None ->
-      prerr_endline (
+      debug_print (
         "?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 "^
@@ -608,7 +617,7 @@ let get_cooked_obj ?(trust=true) base_univ uri =
     else
       (* we don't trust the uri, so we fail *)
       begin
-        prerr_endline ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
+        debug_print ("CACHE MISS: " ^ (UriManager.string_of_uri uri));
         raise Not_found
       end
       
@@ -696,6 +705,6 @@ let list_obj () =
     (list_uri ())
   with
     Not_found -> 
-      prerr_endline "Who has removed the uri in the meanwhile?";
+      debug_print "Who has removed the uri in the meanwhile?";
       raise Not_found
 ;;