From 1c4f27169b04c34a48bef6c84684cb941dfb9f98 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 15:15:21 +0000 Subject: [PATCH] load the graph of objects that depend on the ones requested, rank universes and use them in the transformation to obtain terms with TypeK and not always Type0 --- helm/software/components/ng_kernel/check.ml | 47 +++++++++++++++---- .../components/ng_kernel/nCicEnvironment.ml | 13 +++-- .../components/ng_kernel/nCicEnvironment.mli | 2 + 3 files changed, 50 insertions(+), 12 deletions(-) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 750910611..513612f9b 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -1,17 +1,15 @@ let _ = let indent = ref 0 in -(* let do_indent () = String.make !indent ' ' in *) +(* let do_indent () = String.make !indent ' ' in *) NCicTypeChecker.set_logger (function | `Start_type_checking s -> (); -(* prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); +(* prerr_endline (do_indent () ^ "Start: " ^ NUri.string_of_uri s); *) incr indent -*) + | `Type_checking_completed s -> (); -(* decr indent; - prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s) -*) +(* prerr_endline (do_indent () ^ "End: " ^ NUri.string_of_uri s) *) ); NCicPp.set_ppterm NCicPp.trivial_pp_term; Helm_registry.load_from "conf.xml"; @@ -37,15 +35,46 @@ let _ = in let alluris = HExtlib.filter_map - (fun u -> try Some (NUri.nuri_of_ouri (UriManager.uri_of_string u)) with _ - -> None) alluris + (fun u -> try Some (UriManager.uri_of_string u) with _ -> None) alluris in + (* brutal *) + prerr_endline "loading graphs..."; + let dbd = HSql.quick_connect (LibraryDb.parse_dbd_conf ()) in + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); + let uniq l = + HExtlib.list_uniq (List.sort UriManager.compare l) + in + let who_uses u = + uniq (List.map fst (MetadataDeps.inverse_deps ~dbd u)) + in + let roots_alluris = + let rec fix acc l = + let acc, todo = + List.fold_left (fun (acc,todo) x -> + let w = who_uses x in + if w = [] then (x::acc,todo) else (acc,uniq (todo@w))) + (acc,[]) l + in + if todo = [] then uniq acc else fix acc todo + in + (fix [] alluris) + in + List.iter + (fun u -> + prerr_endline (" - "^UriManager.string_of_uri u); + try NCicEnvironment.load_graph u with exn -> ()) + roots_alluris; + prerr_endline "finished...."; + CicUniv.do_rank (NCicEnvironment.get_graph ()); + prerr_endline "ranked...."; prerr_endline "caching objects"; HExtlib.profiling_enabled := false; List.iter (fun uu -> + let uu= NUri.nuri_of_ouri uu in indent := 0; (* prerr_endline ("************* INIZIO **************** " ^ NUri.string_of_uri uu); *) let _,o = NCicEnvironment.get_obj uu in +(* prerr_endline (NCicPp.ppobj o); *) try NCicTypeChecker.typecheck_obj o; (* prerr_endline ("************* FINE ****************" ^ NUri.string_of_uri uu); *) @@ -65,6 +94,7 @@ let _ = let prima = Unix.gettimeofday () in List.iter (fun u -> + let u= NUri.nuri_of_ouri u in indent := 0; NCicTypeChecker.typecheck_obj (snd (NCicEnvironment.get_obj u))) alluris; @@ -73,7 +103,6 @@ let _ = let dopo2 = Unix.gettimeofday () in Printf.eprintf "NEW typing: %3.2f, gc: %3.2f\n%!" (dopo -. prima) (dopo2 -. dopo); CicEnvironment.invalidate (); - let alluris = List.map NUri.ouri_of_nuri alluris in Gc.compact (); let prima = Unix.gettimeofday () in List.iter (fun u -> ignore (CicTypeChecker.typecheck u)) alluris; diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 52c3ebca7..1076adbf5 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -1,5 +1,14 @@ let cache = NUri.UriHash.create 313;; +let oldg = ref CicUniv.empty_ugraph;; + +let load_graph uri = + let _,g = CicEnvironment.get_obj !oldg uri in + oldg := g +;; + +let get_graph _ = !oldg;; + let get_checked_obj u = try let b, o = NUri.UriHash.find cache u in if not b then assert false else o @@ -23,9 +32,7 @@ let get_obj u = with Not_found -> (* in th final implementation should get it from disk *) let ouri = NUri.ouri_of_nuri u in - let o,_ = - CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri - in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in let l = OCic2NCic.convert_obj ouri o in List.iter (fun (u,_,_,_,_ as o) -> (* prerr_endline ("+"^NUri.string_of_uri u); *) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 9c0a70fc0..6f224d527 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -50,5 +50,7 @@ val get_checked_cofix: val get_indty_leftno: NReference.reference -> int val invalidate: unit -> unit +val load_graph: UriManager.uri -> unit +val get_graph: unit -> CicUniv.universe_graph (* EOF *) -- 2.39.2