From bd1e80fb01cfb419e256d5899ac5bf8818f11e64 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 23 Jun 2009 11:46:16 +0000 Subject: [PATCH] 1) NCicTypechecker.typecheck_obj removed, since it did not add to the environment (and thus all objects were type-checked at least twice) 2) NCicEnvironment.check_and_add_obj that checks and add an object 3) added NCicEnvironment.invalidate_obj that invalidate all objects after a given one (that comprised) 4) NCicLibrary.add_obj now calls the NCicEnvironment.check_and_add_obj; NCicLibrary.time_travel now calls NCicEnvironment.invalidate_obj Note: it could happen that an object is in the environment but not in the library and thus it could not be invalidated by time_travel. In practice, this is safe anyway and it will never happen. --- .../grafite_engine/grafiteEngine.ml | 6 +- helm/software/components/ng_kernel/check.ml | 6 +- .../components/ng_kernel/nCicEnvironment.ml | 104 +++++++++++------- .../components/ng_kernel/nCicEnvironment.mli | 5 + .../components/ng_kernel/nCicLibrary.ml | 11 +- .../components/ng_kernel/nCicLibrary.mli | 3 +- .../components/ng_kernel/nCicTypeChecker.mli | 3 - helm/software/components/ng_refiner/check.ml | 2 +- 8 files changed, 86 insertions(+), 54 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 5f64b1b0a..b6a8786f2 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -699,14 +699,12 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = | _ -> obj_kind in let obj = uri,height,[],[],obj_kind in - NCicTypeChecker.typecheck_obj obj; - let status = NCicLibrary.add_obj status uri obj in + let status = NCicLibrary.add_obj status obj in let objs = NCicElim.mk_elims obj in let timestamp,uris_rev = List.fold_left (fun (status,uris_rev) (uri,_,_,_,_) as obj -> - NCicTypeChecker.typecheck_obj obj; - let status = NCicLibrary.add_obj status uri obj in + let status = NCicLibrary.add_obj status obj in status,uri::uris_rev ) (status,[]) objs in let uris = uri::List.rev uris_rev in diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index d10b771aa..f5fb6841c 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -176,7 +176,7 @@ let _ = let o = NCicLibrary.get_obj uu in if print_object then prerr_endline (NCicPp.ppobj o); try - NCicTypeChecker.typecheck_obj o + NCicEnvironment.check_and_add_obj o with exn -> let rec aux = function @@ -204,9 +204,9 @@ let _ = let prima = Unix.gettimeofday () in List.iter (fun u -> - let u= OCic2NCic.nuri_of_ouri u in + let u= OCic2NCic.nuri_of_ouri u in indent := 0; - NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)) + ignore (NCicEnvironment.get_checked_obj u)) alluris; let dopo = Unix.gettimeofday () in Gc.compact (); diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index ef3bca22d..9cec01f60 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -113,57 +113,81 @@ let set_typecheck_obj f = ;; let cache = NUri.UriHash.create 313;; +let history = ref [];; let frozen_list = ref [];; +let invalidate_obj uri = +prerr_endline ("INVALIDO: " ^ NUri.string_of_uri uri); +List.iter (fun uri -> prerr_endline ("INH: " ^ NUri.string_of_uri uri)) !history; + let rec aux to_be_deleted = + function + [] -> assert false + | uri'::tl when NUri.eq uri uri' -> uri'::to_be_deleted,tl + | uri'::tl -> aux (uri'::to_be_deleted) tl + in + let to_be_deleted,h = aux [] !history in + history := h; + List.iter (fun uri -> NUri.UriHash.remove cache uri) to_be_deleted +;; + exception Propagate of NUri.uri * exn;; +let to_exn f x = + match f x with + `WellTyped o -> o + | `Exn e -> raise e +;; + +let check_and_add_obj ((u,_,_,_,_) as obj) = + let saved_frozen_list = !frozen_list in + try + frozen_list := (u,obj)::saved_frozen_list; + !typecheck_obj obj; + frozen_list := saved_frozen_list; + let obj = `WellTyped obj in + NUri.UriHash.add cache u obj; + history := u::!history; + obj + with + Sys.Break as e -> + frozen_list := saved_frozen_list; + raise e + | Propagate (u',old_exn) as e' -> + frozen_list := saved_frozen_list; + let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^ + " depends (recursively) on " ^ NUri.string_of_uri u' ^ + " which is not well-typed"), + match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in + NUri.UriHash.add cache u exn; + history := u::!history; + if saved_frozen_list = [] then + exn + else + raise e' + | e -> + frozen_list := saved_frozen_list; + let exn = `Exn e in + NUri.UriHash.add cache u exn; + history := u::!history; + if saved_frozen_list = [] then + exn + else + raise (Propagate (u,e)) +;; + let get_checked_obj u = if List.exists (fun (k,_) -> NUri.eq u k) !frozen_list then raise (CircularDependency (lazy (NUri.string_of_uri u))) else - let obj = - try NUri.UriHash.find cache u - with - Not_found -> - let saved_frozen_list = !frozen_list in - try - let obj = !get_obj u in - frozen_list := (u,obj)::saved_frozen_list; - !typecheck_obj obj; - frozen_list := saved_frozen_list; - let obj = `WellTyped obj in - NUri.UriHash.add cache u obj; - obj - with - Sys.Break as e -> - frozen_list := saved_frozen_list; - raise e - | Propagate (u',old_exn) as e' -> - frozen_list := saved_frozen_list; - let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^ - " depends (recursively) on " ^ NUri.string_of_uri u' ^ - " which is not well-typed"), - match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in - NUri.UriHash.add cache u exn; - if saved_frozen_list = [] then - exn - else - raise e' - | e -> - frozen_list := saved_frozen_list; - let exn = `Exn e in - NUri.UriHash.add cache u exn; - if saved_frozen_list = [] then - exn - else - raise (Propagate (u,e)) - in - match obj with - `WellTyped o -> o - | `Exn e -> raise e + try NUri.UriHash.find cache u + with Not_found -> check_and_add_obj (!get_obj u) ;; +let get_checked_obj u = to_exn get_checked_obj u;; + +let check_and_add_obj obj = ignore (to_exn check_and_add_obj obj);; + let get_checked_decl = function | Ref.Ref (uri, Ref.Decl) -> (match get_checked_obj uri with diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 862d71484..a9feb4d20 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -20,6 +20,8 @@ val set_get_obj: (NUri.uri -> NCic.obj) -> unit val get_checked_obj: NUri.uri -> NCic.obj +val check_and_add_obj: NCic.obj -> unit + val get_relevance: NReference.reference -> bool list val type0: NCic.universe @@ -48,6 +50,9 @@ val get_checked_fixes_or_cofixes: NReference.reference -> NCic.inductiveFun list * NCic.f_attr * int +(* invalidate the object and all those that entered the environment after it *) +val invalidate_obj: NUri.uri -> unit + val invalidate: unit -> unit val set_typecheck_obj: (NCic.obj -> unit) -> unit diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index 98f8903d8..1efe173e7 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -77,6 +77,7 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps= Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) []; close_out ch in let load_db () = + HExtlib.mkdir (Helm_registry.get "matita.basedir"); try let ga,im = require_path (db_path ()) in let ga = @@ -137,7 +138,12 @@ class status = let time_travel status = let sto,ali,cac,inc = status#timestamp in - storage := sto; local_aliases := ali; cache := cac; includes := inc + let diff_len = List.length !storage - List.length sto in + let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in + if List.length to_be_deleted > 0 then + let u,_ = HExtlib.list_last to_be_deleted in + NCicEnvironment.invalidate_obj u; + storage := sto; local_aliases := ali; cache := cac; includes := inc ;; let serialize ~baseuri dump = @@ -248,7 +254,8 @@ let aliases_of uri = Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri))) ;; -let add_obj status u obj = +let add_obj status ((u,_,_,_,_) as obj) = + NCicEnvironment.check_and_add_obj obj; storage := (u,obj)::!storage; let _,height,_,_,obj = obj in let references = diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index 326ef143e..91bf96c69 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -22,7 +22,8 @@ class status : method set_library_status: -> 'self end -val add_obj: #status as 'status -> NUri.uri -> NCic.obj -> 'status +(* it also checks it and add it to the environment *) +val add_obj: #status as 'status -> NCic.obj -> 'status val aliases_of: NUri.uri -> NReference.reference list val resolve: string -> NReference.reference list (* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.mli b/helm/software/components/ng_kernel/nCicTypeChecker.mli index df76faab7..af0f2cade 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.mli +++ b/helm/software/components/ng_kernel/nCicTypeChecker.mli @@ -25,9 +25,6 @@ val set_logger: val set_trust : (NCic.obj -> bool) -> unit -(* typechecks the object, raising an exception if illtyped *) -val typecheck_obj : NCic.obj -> unit - val typeof: subst:NCic.substitution -> metasenv:NCic.metasenv -> NCic.context -> NCic.term -> diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 2ab8185ab..f544d8dae 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -187,7 +187,7 @@ let _ = let o = NCicLibrary.get_obj uu in if print_object then prerr_endline (NCicPp.ppobj o); try - NCicTypeChecker.typecheck_obj o + NCicEnvironment.check_and_add_obj o with | NCicTypeChecker.AssertFailure s | NCicTypeChecker.TypeCheckerFailure s -- 2.39.2