From 2ee517d852ad53540881221ecb01b9ec1881cc6a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 20 Jul 2009 16:25:26 +0000
Subject: [PATCH] 1) The NG kernel now accepts only usage of declared universes
 2) Bug (badly) fixed in NCicElim: it used to generate undeclared universe   
 names.

---
 helm/software/components/ng_kernel/nCicEnvironment.ml  |  6 ++++++
 helm/software/components/ng_kernel/nCicEnvironment.mli |  1 +
 helm/software/components/ng_kernel/nCicTypeChecker.ml  |  7 ++++++-
 helm/software/components/ng_tactics/nCicElim.ml        | 10 +++++++++-
 4 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 07185a947..b3b1eda16 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -77,6 +77,12 @@ 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] -> 
diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli
index 0e0fe4845..778931706 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.mli
+++ b/helm/software/components/ng_kernel/nCicEnvironment.mli
@@ -27,6 +27,7 @@ val get_relevance: NReference.reference -> bool list
 
 val type0: NCic.universe
 val get_universes: unit -> NCic.universe list
+val is_declared: NCic.universe -> bool
 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
diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index c19561d35..695b2e531 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -391,7 +391,12 @@ let rec typeof ~subst ~metasenv context term =
         with Failure _ -> 
           raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
             ^" under: " ^ NCicPp.ppcontext ~metasenv ~subst context))))
-    | C.Sort (C.Type [false,u]) -> C.Sort (C.Type [true, u])
+    | C.Sort (C.Type ([false,u] as univ)) ->
+       if NCicEnvironment.is_declared univ then
+        C.Sort (C.Type [true, u])
+       else
+        raise (TypeCheckerFailure (lazy ("undeclared universe " ^
+         NUri.string_of_uri u)))
     | C.Sort (C.Type _) -> 
         raise (AssertFailure (lazy ("Cannot type an inferred type: "^
           NCicPp.ppterm ~subst ~metasenv ~context t)))
diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index ae472ae38..ef33ceeab 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -157,7 +157,15 @@ let mk_elims (uri,_,_,_,obj) =
       NCic.Prop -> `Prop,"ind"
     | NCic.Type u ->
        let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
-       `NType u, "rect_" ^ u
+       (try
+         if String.sub u 0 4 = "Type" then
+          `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
+         else if String.sub u 0 5 = "CProp" then
+          `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
+         else
+          (prerr_endline u;
+          assert false)
+        with Failure _ -> assert false)
  in
   match obj with
      NCic.Inductive (true,leftno,itl,_) ->
-- 
2.39.2