X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicEnvironment.ml;h=b3b1eda16eab228c19944d7f7f176e2ffd6433e9;hb=4a6973c769b96f569b4aa5410197e0e6c76dfc92;hp=9cec01f60c2ed9d96de0d84172a4e8eedd509d13;hpb=bd1e80fb01cfb419e256d5899ac5bf8818f11e64;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 9cec01f60..b3b1eda16 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -18,6 +18,11 @@ exception CircularDependency of string Lazy.t;;
 exception ObjectNotFound of string Lazy.t;;
 exception BadDependency of string Lazy.t * exn;;
 exception BadConstraint of string Lazy.t;;
+exception AlreadyDefined 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;;
@@ -70,6 +75,14 @@ let pp_constraints () =
 
 let universes = ref [];;
 
+let get_universes () = List.map (fun x -> [false,x]) !universes;;
+
+let is_declared u =
+ match u with
+    [false,x] -> List.exists (fun y -> NUri.eq x y) !universes
+  | _ -> assert false
+;;
+
 let add_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 
@@ -79,7 +92,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,22 +126,30 @@ let set_typecheck_obj f =
   end
 ;;
 
-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 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;;
@@ -144,10 +166,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;
@@ -159,7 +181,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
@@ -168,7 +190,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
@@ -186,7 +208,12 @@ let get_checked_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 check_and_add_obj ((u,_,_,_,_) as obj) =
+ if NUri.UriHash.mem cache u then
+  raise (AlreadyDefined (lazy (NUri.string_of_uri u)))
+ else
+  ignore (to_exn check_and_add_obj obj)
+;;
 
 let get_checked_decl = function
   | Ref.Ref (uri, Ref.Decl) ->