From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 30 Apr 2008 15:50:06 +0000 (+0000)
Subject: universes are written with the URI inside objects, this allows
X-Git-Tag: make_still_working~5276
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c031aa4ca97d0d563a772d7bd247ff7814c51b04;p=helm.git

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 0f36f1a04..e61ee78ea 100644
--- 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 a936c16bf..beb8a233f 100644
--- 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 7b422583f..6451a74ec 100644
--- 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 c2f1616be..b039b7e5b 100644
--- 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 e1c113ef3..98cb72ad7 100644
--- 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 fd89f77c8..d70bd1545 100644
--- 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