Univs: fix checker generating undeclared universes.

4 files changed, 34 insertions, 35 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 78fff1bbe..3ea5ed0d3 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -18,19 +18,27 @@ let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
   match hd with
       Sort (Type u) when not (Univ.is_univ_variable u) ->
-        let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in
-        mkArity (ctxt,Prop Null), 
-	  Univ.enforce_leq u u' Univ.empty_constraint
-    | _ -> ar, Univ.empty_constraint
+      let ul = Univ.Level.make empty_dirpath 1 in
+      let u' = Univ.Universe.make ul in
+      let cst = Univ.enforce_leq u u' Univ.empty_constraint in
+      let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in
+        mkArity (ctxt,Prop Null), ctx
+    | _ -> ar, Univ.ContextSet.empty
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn); pp_flush ();
-  let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in
+  let env' =
+    if cb.const_polymorphic then
+      let inst = Univ.make_abstract_instance cb.const_universes in
+      let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in
+        push_context ~strict:false ctx env
+    else push_context ~strict:true cb.const_universes env
+  in
   let envty, ty = 
     match cb.const_type with
       RegularArity ty ->
         let ty', cu = refresh_arity ty in
-        let envty = add_constraints cu env' in
+        let envty = push_context_set cu env' in
         let _ = infer_type envty ty' in envty, ty
     | TemplateArity(ctxt,par) ->
         let _ = check_ctxt env' ctxt in
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 8ddeea2a2..384d883ea 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -175,7 +175,7 @@ let sort_cmp env univ pb s0 s1 =
         then begin
           if !Flags.debug then begin
             let op = match pb with CONV -> "=" | CUMUL -> "<=" in
-            Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds
+            Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds
               (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut()
                ++ Univ.pr_universes univ))
           end;
diff --git a/checker/univ.ml b/checker/univ.ml
index 50c0367bb..648e47817 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -562,20 +562,6 @@ let repr g u =
 
 let get_set_arc g = repr g Level.set
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
-
-let safe_repr g u =
-  let rec safe_repr_rec u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec u
-  with Not_found ->
-    let can = terminal u in
-    enter_arc can g, can
-
 exception AlreadyDeclared
 	    
 let add_universe vlev strict g =
@@ -760,8 +746,8 @@ let is_lt g arcu arcv =
 (** First, checks on universe levels *)
 
 let check_equal g u v =
-  let g, arcu = safe_repr g u in
-  let _, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
@@ -770,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ
 let is_prop_arc u = Level.is_prop u.univ
 
 let check_smaller g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
@@ -921,8 +907,8 @@ let error_inconsistency o u v =
 (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT -> error_inconsistency Eq v u
@@ -937,8 +923,8 @@ let enforce_univ_eq u v g =
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -949,8 +935,8 @@ let enforce_univ_leq u v g =
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u in
+  let arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -962,7 +948,10 @@ let enforce_univ_lt u v g =
       | FastLE | FastLT -> error_inconsistency Lt u v
 
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal Level.prop) g in
+    enforce_univ_lt Level.prop Level.set g
 
 (* Constraints and sets of constraints. *)    
 
@@ -1167,7 +1156,7 @@ struct
 
   (** Universe contexts (variables as a list) *)
   let empty = (Instance.empty, Constraint.empty)
-
+  let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
 end
@@ -1180,6 +1169,7 @@ struct
   let empty = LSet.empty, Constraint.empty
   let constraints (_, cst) = cst
   let levels (ctx, _) = ctx
+  let make ctx cst = (ctx, cst)
 end
 type universe_context_set = ContextSet.t
 
diff --git a/checker/univ.mli b/checker/univ.mli
index 459adfcd6..02c1bbdb9 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -131,7 +131,7 @@ val check_constraints : constraints -> universes -> bool
 
 (** Polymorphic maps from universe levels to 'a *)
 module LMap : Map.S with type key = universe_level
-
+module LSet : CSig.SetS with type elt = universe_level
 type 'a universe_map = 'a LMap.t
 
 (** {6 Substitution} *)
@@ -184,7 +184,7 @@ sig
   type t
 
   val empty : t
-
+  val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
 
@@ -193,6 +193,7 @@ end
 module ContextSet :
   sig 
     type t
+    val make : LSet.t -> constraints -> t
     val empty : t
     val constraints : t -> constraints
   end