depends

[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 78abb68019f37a9f5aa7d9aa8a91cd7087f80071..b3b1eda16eab228c19944d7f7f176e2ffd6433e9 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -18,6 +18,7 @@ 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 [];;
@@ -74,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] -> 
@@ -199,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) ->