From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 13:15:23 +0000 (+0000)
Subject: 1) added a function to retrieve all the universes currently in use
X-Git-Tag: make_still_working~3672
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0264ee034e3f485baf7070ad9b43cf69db94131b;p=helm.git

1) added a function to retrieve all the universes currently in use
2) INCONSISTENCY BUG FIXED: it was possible to _redefine_ an already defined
   constant. Thus it was very easy to prove False!
---

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 78abb6801..07185a947 100644
--- 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,8 @@ let pp_constraints () =
 
 let universes = ref [];;
 
+let get_universes () = List.map (fun x -> [false,x]) !universes;;
+
 let add_constraint strict a b = 
   match a,b with
   | [false,a2],[false,b2] -> 
@@ -199,7 +202,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) ->
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 5252ddb8b..0e0fe4845 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -15,6 +15,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;;
 
 val set_get_obj: (NUri.uri -> NCic.obj) -> unit
 
@@ -25,6 +26,7 @@ val check_and_add_obj: NCic.obj -> unit
 val get_relevance: NReference.reference -> bool list
 
 val type0: NCic.universe
+val get_universes: unit -> NCic.universe list
 val max: NCic.universe -> NCic.universe -> NCic.universe
 (* universe_* raise BadConstraints if the second arg. is an inferred universe *)
 val universe_eq: NCic.universe -> NCic.universe -> bool