From c031aa4ca97d0d563a772d7bd247ff7814c51b04 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 30 Apr 2008 15:50:06 +0000 Subject: [PATCH] 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! --- helm/software/components/cic/cicParser.ml | 11 ++++++----- helm/software/components/cic/cicUniv.ml | 12 ++++-------- helm/software/components/cic/cicUniv.mli | 1 + helm/software/components/cic_acic/cic2acic.ml | 2 +- .../components/cic_proof_checking/cicTypeChecker.mli | 4 +++- helm/software/components/library/librarySync.ml | 9 +++++---- 6 files changed, 20 insertions(+), 19 deletions(-) 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 -- 2.39.2