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.

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 5f64b1b0a91384c9fb77b7e34f1db2ccf30357c5..b6a8786f22e2dc933ac1bdf2756cb286238ccf38 100644 (file)
--- 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 d10b771aad2b249618ba4178db18ceba1cd955a6..f5fb6841c39a47efdc878408a1eb5a20f7f9deea 100644 (file)
--- 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 ef3bca22d06941ebfa20fe883d4423eb7ec87e0e..9cec01f60c2ed9d96de0d84172a4e8eedd509d13 100644 (file)
--- 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 862d7148432f5a6ba7525780d5e0b8d04f36b3f9..a9feb4d20f22007b8e2798cc1c6f9586d94d455b 100644 (file)
--- 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 98f8903d8a5d3783852e92705fc7ff667ae46d7d..1efe173e73620db5c17b3bdd23f781355e2bab4c 100644 (file)
--- 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 326ef143ea64d532b3670bbf832478bdd0905ac1..91bf96c69897b6eeb9968917f68b0e81e0e523f5 100644 (file)
--- 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 df76faab71255607b1763621d755232a79565fe2..af0f2cadeffb8d7528f05df5250c6f9e7b7262ff 100644 (file)
--- 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 2ab8185ab0e2e4725efb8f5eee309bf74852ab7c..f544d8daeed54aad2216322cc09f344e6bfacfa8 100644 (file)
--- 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