universes are written with the URI inside objects, this allows

universes to be actually shared between objects and no duplication is necessary.
in this way the typechecker is more strict and unification can be an ungly beast implicitly
adding an = constranint between two universes. speedup granted!

diff --git a/helm/software/components/cic/cicParser.ml b/helm/software/components/cic/cicParser.ml
index 0f36f1a04d8b2ab886eb3861d904469efec20511..e61ee78eabd1a8bed218b2d75d569e6a6bc53dd9 100644 (file)
--- a/helm/software/components/cic/cicParser.ml
+++ b/helm/software/components/cic/cicParser.ml
@@ -311,11 +311,12 @@ let sort_of_string ctxt = function
       let len = String.length s in
       if not(len > 5) then parse_error ctxt "sort expected";
       if not(String.sub s 0 5 = "Type:") then parse_error ctxt "sort expected";
-      try 
-        Cic.Type 
-          (CicUniv.fresh 
-            ~uri:ctxt.uri 
-            ~id:(int_of_string (String.sub s 5 (len - 5))) ())
+      let s = String.sub s 5 (len - 5) in
+      let i = String.index s ':' in  
+      let id =  int_of_string (String.sub s 0 i) in
+      let suri = String.sub s (i+1) (len - 5 - i - 1) in
+      let uri = UriManager.uri_of_string suri in
+      try Cic.Type (CicUniv.fresh ~uri ~id ())
       with
       | Failure "int_of_string" 
       | Invalid_argument _ -> parse_error ctxt "sort expected" 

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index a936c16bf9fb688e399cb5e30c63fe6813323644..beb8a233fb58b3f56fb516131ca1b14188182bf0 100644 (file)
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -380,14 +380,7 @@ let fresh ?uri ?id () =
 let name_universe u uri =
   match u with
   | (i, None) -> (i, Some uri)
-  | (i, Some ouri) when UriManager.eq ouri uri -> u
-  | (i, Some ouri) ->
-      (* inside obj living at uri 'uri' should live only
-       * universes with uri None. Call Unshare.unshare ~fresh_univs:true
-       * if you want to reuse a Type in another object *)
-      prerr_endline ("Offending universe: " ^ string_of_universe u^
-        " found inside object " ^ UriManager.string_of_uri  uri);
-      assert false
+  | u -> u
 ;;
   
 let print_ugraph (g, _, o) = 
@@ -636,6 +629,9 @@ let write_xml_of_ugraph filename (m,_,_) l =
     Xml.pp ~gzip:true tokens (Some filename)
 
 let univno = fst
+let univuri = function 
+  | _,None -> assert false
+  | _,Some u -> u
 
  
 let rec clean_ugraph m already_contained f =

diff --git a/helm/software/components/cic/cicUniv.mli b/helm/software/components/cic/cicUniv.mli
index 7b422583f53f361da3e247fb5717ac313eb7f70c..6451a74ec619abf63c65bbc4a6a0c1efe16739ec 100644 (file)
--- a/helm/software/components/cic/cicUniv.mli
+++ b/helm/software/components/cic/cicUniv.mli
@@ -133,6 +133,7 @@ val restart_numbering:
   returns the universe number (used to save it do xml) 
 *) 
 val univno: universe -> int 
+val univuri: universe -> UriManager.uri
 
   (** re-hash-cons URIs contained in the given universe so that phisicaly
    * equality could be enforced. Mainly used by

diff --git a/helm/software/components/cic_acic/cic2acic.ml b/helm/software/components/cic_acic/cic2acic.ml
index c2f1616be8101e93899c97a1c9d28e8c8e09c1fa..b039b7e5ba0405ea1ca507916eff07935c7a131c 100644 (file)
--- a/helm/software/components/cic_acic/cic2acic.ml
+++ b/helm/software/components/cic_acic/cic2acic.ml
@@ -30,7 +30,7 @@ type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 let string_of_sort = function
   | `Prop -> "Prop"
   | `Set -> "Set"
-  | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u)
+  | `Type u -> "Type:" ^ string_of_int (CicUniv.univno u) ^ ":" ^ UriManager.string_of_uri (CicUniv.univuri u)
   | `CProp -> "CProp"
 
 let sort_of_sort = function

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.mli b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
index e1c113ef335609f9460efb981910518629f792ad..98cb72ad773577cd9d2b2e5dc3952dbdf57bc657 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.mli
@@ -47,7 +47,9 @@ val type_of_aux':
   Cic.term -> CicUniv.universe_graph -> 
   Cic.term * CicUniv.universe_graph
 
-(* typechecks the obj and puts it in the environment *)
+(* typechecks the obj and puts it in the environment
+ * empty universes are filed with the given uri, thus you should
+ * get the object again after calling this *)
 val typecheck_obj : UriManager.uri -> Cic.obj -> unit
 
 (* check_allowed_sort_elimination uri i s1 s2

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index fd89f77c8f7e89744e7a745bd8ff16f5df094b79..d70bd15453cea4b9562d7abf94db97d21eaf94ef 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -128,8 +128,7 @@ let save_object_to_disk uri obj ugraph univlist =
 
 let typecheck_obj =
  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri)
-  (Unshare.fresh_types obj)
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
  let profiler = HExtlib.profile "add_obj.index_obj" in
@@ -160,8 +159,10 @@ let add_single_obj uri obj refinement_toolkit =
       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
       (univ_time *. 100. /. total_time) (total_time) (univ_time)
       (UriManager.name_of_uri uri));*)
-    let _, ugraph, univlist = 
-      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+    let obj, ugraph, univlist = 
+      try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
+      with CicEnvironment.Object_not_found _ -> assert false
+    in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       try