From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 23 Dec 2010 10:32:44 +0000 (+0000)
Subject: 1. bug in addition of universe constraints fixed: the recursive
X-Git-Tag: make_still_working~2626
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77dbf2cad247bbcb13e39c4341573b220d1d08a9;p=helm.git

1. bug in addition of universe constraints fixed: the recursive
   inclusion does not add constraints to the NCicLibrary.storage
2. since we no longer perform recursive cleaning,
   NCicEnvironment.invalidate_item is no longer recursive. This fixed
   definitely the bugs in undo/redo linked to "include"s
---

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index c271448a7..2acf844b0 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -297,10 +297,6 @@ let index_eq_for_auto status uri =
    status)
 ;; 
 
-let basic_eval_add_constraint (u1,u2) status =
- NCicLibrary.add_constraint status u1 u2
-;;
-
 let inject_constraint =
  let basic_eval_add_constraint (u1,u2) 
      ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
@@ -309,7 +305,11 @@ let inject_constraint =
   if not alias_only then
    let u1 = refresh_uri_in_universe u1 in 
    let u2 = refresh_uri_in_universe u2 in 
-    basic_eval_add_constraint (u1,u2) status
+    (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
+     * and also to the storage (for undo/redo). During inclusion of compiled
+     * files the storage must not be touched. *)
+    NCicEnvironment.add_lt_constraint u1 u2;
+    status
   else
    status
  in
@@ -317,7 +317,7 @@ let inject_constraint =
 ;;
 
 let eval_add_constraint status u1 u2 = 
- let status = basic_eval_add_constraint (u1,u2) status in
+ let status = NCicLibrary.add_constraint status u1 u2 in
   NCicLibrary.dump_obj status (inject_constraint (u1,u2))
 ;;
 
@@ -543,16 +543,6 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
        (*prerr_endline (NCicPp.ppobj obj);*)
            let boxml = NCicElim.mk_elims obj in
            let boxml = boxml @ NCicElim.mk_projections obj in
-(*
-           let objs = [] in
-           let timestamp,uris_rev =
-             List.fold_left
-              (fun (status,uris_rev) (uri,_,_,_,_) as obj ->
-                let status = NCicLibrary.add_obj status obj in
-                 status,uri::uris_rev
-              ) (status,[]) objs in
-           let uris = uri::List.rev uris_rev in
-*)
            let status = status#set_ng_mode `CommandMode in
            let xxaliases = GrafiteDisambiguate.aliases_for_objs [uri] in
            let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
diff --git a/matita/components/ng_kernel/nCicEnvironment.ml b/matita/components/ng_kernel/nCicEnvironment.ml
index 738329689..c5c692733 100644
--- a/matita/components/ng_kernel/nCicEnvironment.ml
+++ b/matita/components/ng_kernel/nCicEnvironment.ml
@@ -254,6 +254,9 @@ let set_typecheck_obj f =
   end
 ;;
 
+(* CSC: old code that performs recursive invalidation; to be removed
+ * once we understand what we really want. Once we removed it, we can
+ * also remove the !history
 let invalidate_item item =
  let item_eq a b = 
    match a, b with
@@ -279,6 +282,16 @@ let invalidate_item item =
      | `Constr _ -> assert false
      ) to_be_deleted
 ;;
+*)
+
+let invalidate_item =
+ function
+    `Obj (uri,_) -> NUri.UriHash.remove cache uri
+  | `Constr ([_,u1],[_,u2]) -> 
+      let w = u1,u2 in
+      lt_constraints := List.filter ((<>) w) !lt_constraints;
+  | `Constr _ -> assert false
+;;
 
 exception Propagate of NUri.uri * exn;;
 
@@ -292,6 +305,7 @@ let check_and_add_obj ((u,_,_,_,_) as obj) =
  let saved_frozen_list = !frozen_list in
  try
    frozen_list := (u,obj)::saved_frozen_list;
+   HLog.warn ("Typechecking of " ^ NUri.string_of_uri u); 
    !typecheck_obj obj;
    frozen_list := saved_frozen_list;
    let obj' = `WellTyped obj in
diff --git a/matita/components/ng_kernel/nCicEnvironment.mli b/matita/components/ng_kernel/nCicEnvironment.mli
index 5128831be..8483b8a1f 100644
--- a/matita/components/ng_kernel/nCicEnvironment.mli
+++ b/matita/components/ng_kernel/nCicEnvironment.mli
@@ -37,7 +37,6 @@ 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_item: 
       [ `Obj of NUri.uri * NCic.obj 
       | `Constr of NCic.universe * NCic.universe ] -> unit
diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index a38a26ee2..65e0cd60e 100644
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -153,7 +153,7 @@ let time_travel status =
   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
-     NCicEnvironment.invalidate_item (HExtlib.list_last to_be_deleted);
+    List.iter NCicEnvironment.invalidate_item to_be_deleted;
    storage := sto; local_aliases := ali
 ;;
 
@@ -347,6 +347,13 @@ let add_obj status ((u,_,_,_,_) as obj) =
 ;;
 
 let add_constraint status u1 u2 = 
+  if
+   List.exists
+    (function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false)
+    !storage
+  then
+   (*CSC: raise an exception here! *)
+   (prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false);
   NCicEnvironment.add_lt_constraint u1 u2;
   storage := (`Constr (u1,u2)) :: !storage;
   status#set_timestamp (!storage,!local_aliases)