]> matita.cs.unibo.it Git - helm.git/commitdiff
universes are written with the URI inside objects, this allows
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 15:50:06 +0000 (15:50 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 30 Apr 2008 15:50:06 +0000 (15:50 +0000)
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!

helm/software/components/cic/cicParser.ml
helm/software/components/cic/cicUniv.ml
helm/software/components/cic/cicUniv.mli
helm/software/components/cic_acic/cic2acic.ml
helm/software/components/cic_proof_checking/cicTypeChecker.mli
helm/software/components/library/librarySync.ml

index 0f36f1a04d8b2ab886eb3861d904469efec20511..e61ee78eabd1a8bed218b2d75d569e6a6bc53dd9 100644 (file)
@@ -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" 
index a936c16bf9fb688e399cb5e30c63fe6813323644..beb8a233fb58b3f56fb516131ca1b14188182bf0 100644 (file)
@@ -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 =
index 7b422583f53f361da3e247fb5717ac313eb7f70c..6451a74ec619abf63c65bbc4a6a0c1efe16739ec 100644 (file)
@@ -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
index c2f1616be8101e93899c97a1c9d28e8c8e09c1fa..b039b7e5ba0405ea1ca507916eff07935c7a131c 100644 (file)
@@ -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
index e1c113ef335609f9460efb981910518629f792ad..98cb72ad773577cd9d2b2e5dc3952dbdf57bc657 100644 (file)
@@ -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
index fd89f77c8f7e89744e7a745bd8ff16f5df094b79..d70bd15453cea4b9562d7abf94db97d21eaf94ef 100644 (file)
@@ -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