undo/serialization for universes implemented

[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.ml

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 2d5f03945f8d1fa69ae85444c2fdf58fbb842a57..78abb68019f37a9f5aa7d9aa8a91cd7087f80071 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -19,6 +19,10 @@ exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
 
+let cache = NUri.UriHash.create 313;;
+let history = ref [];;
+let frozen_list = ref [];;
+
 let get_obj = ref (fun _ -> assert false);;
 let set_get_obj f = get_obj := f;;
 
@@ -79,7 +83,8 @@ let add_constraint strict a b =
            ^ " to:\n" ^ pp_constraints ()))));
         universes := a2 :: b2 :: 
           List.filter (fun x -> not (NUri.eq x a2 || NUri.eq x b2)) !universes;
-        le_constraints := (strict,a2,b2) :: !le_constraints)
+        le_constraints := (strict,a2,b2) :: !le_constraints);
+        history := (`Constr (strict,a,b))::!history;
   | _ -> raise (BadConstraint
           (lazy "trying to add a constraint on an inferred universe"))
 ;;
@@ -112,20 +117,30 @@ let set_typecheck_obj f =
   end
 ;;
 
-let cache = NUri.UriHash.create 313;;
-let history = ref [];;
-let frozen_list = ref [];;
-
-let invalidate_obj uri =
+let invalidate_item item =
+ let item_eq a b = 
+   match a, b with
+   | `Obj (u1,_), `Obj (u2,_) -> NUri.eq u1 u2
+   | `Constr _, `Constr _ -> a=b (* MAKE EFFICIENT *)
+   | _ -> false
+ in
  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
+   | item'::tl when item_eq item item' -> item'::to_be_deleted,tl
+   | item'::tl -> aux (item'::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
+   List.iter 
+     (function 
+     | `Obj (uri,_) -> NUri.UriHash.remove cache uri
+     | `Constr (strict,[_,u1],[_,u2]) as c -> 
+          let w = strict,u1,u2 in
+          if not(List.mem c !history) then 
+           le_constraints := List.filter ((<>) w) !le_constraints;
+     | `Constr _ -> assert false
+     ) to_be_deleted
 ;;
 
 exception Propagate of NUri.uri * exn;;
@@ -142,10 +157,10 @@ let check_and_add_obj ((u,_,_,_,_) as obj) =
    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
+   let obj' = `WellTyped obj in
+   NUri.UriHash.add cache u obj';
+   history := (`Obj (u,obj))::!history;
+   obj'
  with
     Sys.Break as e ->
      frozen_list := saved_frozen_list;
@@ -157,7 +172,7 @@ let check_and_add_obj ((u,_,_,_,_) as obj) =
        " which is not well-typed"), 
        match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in
      NUri.UriHash.add cache u exn;
-     history := u::!history;
+     history := (`Obj (u,obj))::!history;
      if saved_frozen_list = [] then
       exn
      else
@@ -166,7 +181,7 @@ let check_and_add_obj ((u,_,_,_,_) as obj) =
      frozen_list := saved_frozen_list;
      let exn = `Exn e in
      NUri.UriHash.add cache u exn;
-     history := u::!history;
+     history := (`Obj (u,obj))::!history;
      if saved_frozen_list = [] then
       exn
      else