From bd1e80fb01cfb419e256d5899ac5bf8818f11e64 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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: <timestamp: timestamp; ..> -> '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