1 files changed, 61 insertions, 66 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 336cdb653e..73d323426b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -270,8 +270,10 @@ module Level = struct
   let is_small x = 
     match data x with
     | Level _ -> false
-    | _ -> true
-
+    | Var _ -> false
+    | Prop -> true
+    | Set -> true
+ 
   let is_prop x =
     match data x with
     | Prop -> true
@@ -551,6 +553,10 @@ struct
     | Cons (l, _, Nil) -> Expr.is_level l
     | _ -> false
 
+  let rec is_levels l = match l with
+    | Cons (l, _, r) -> Expr.is_level l && is_levels r
+    | Nil -> true
+
   let level l = match l with
     | Cons (l, _, Nil) -> Expr.level l
     | _ -> None
@@ -655,7 +661,6 @@ type canonical_arc =
       lt: Level.t list;
       le: Level.t list;
       rank : int;
-      predicative : bool;
       mutable status : status;
       (** Guaranteed to be unset out of the [compare_neq] functions. It is used
           to do an imperative traversal of the graph, ensuring a O(1) check that
@@ -670,7 +675,7 @@ let arc_is_lt arc = match arc.status with
 | Unset | SetLe -> false
 | SetLt -> true
 
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
 
 module UMap :
 sig
@@ -720,6 +725,16 @@ let enter_arc ca g =
 
 (* Every Level.t has a unique canonical arc representative *)
 
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+  {(terminal u) with lt=[v]}
+    
+let empty_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal_lt Level.prop Level.set) g in
+    g
+
 (* repr : universes -> Level.t -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 
@@ -733,19 +748,28 @@ let rec repr g u =
     | Equiv v -> repr g v
     | Canonical arc -> arc
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
+let get_prop_arc g = repr g Level.prop
+let get_set_arc g = repr g Level.set
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
 
-let safe_repr g u =
-  let rec safe_repr_rec g u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec g v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec g u
-  with Not_found ->
-    let can = terminal u in
-    enter_arc can g, can
+exception AlreadyDeclared
+	    
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+	if strict then
+	  { arc with lt=vlev::arc.lt}
+	else 
+	  { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
 
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
@@ -789,7 +813,6 @@ let between g arcu arcv =
   in
   let good,_,_ = explore ([arcv],[],false) arcu in
     good
-
 (* We assume  compare(u,v) = LE with v canonical (see compare below).
    In this case List.hd(between g u v) = repr u
    Otherwise, between g u v = []
@@ -900,8 +923,9 @@ let get_explanation strict g arcu arcv =
         in
         find [] arc.lt
   in
+  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
   try
-    let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
+    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
     (** Reset all the touched arcs. *)
     let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
     List.rev c
@@ -972,7 +996,6 @@ let fast_compare_neq strict g arcu arcv =
     else process_le c to_revert (arc :: lt_todo) le_todo lt le
 
   in
-
   try
     let (to_revert, c) = cmp FastNLE [] [] [arcu] in
     (** Reset all the touched arcs. *)
@@ -1015,24 +1038,18 @@ 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
-  arcu == arcv
+  let arcu = repr g u and arcv = repr g v in
+    arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
 
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-let get_prop_arc g = snd (safe_repr g Level.prop)
-
 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 and arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
     is_prop_arc arcu 
-    || (is_set_arc arcu && arcv.predicative) 
+    || (is_set_arc arcu && not (is_prop_arc arcv))
     || is_leq g arcu arcv
 
 (** Then, checks on universes *)
@@ -1074,19 +1091,11 @@ let check_leq g u v =
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
-(** To speed up tests of Set </<= i *)
-let set_predicative g arcv = 
-  enter_arc {arcv with predicative = true} g
-
 (* setlt : Level.t -> Level.t -> reason -> unit *)
 (* forces u > v *)
 (* this is normally an update of u in g rather than a creation. *)
 let setlt g arcu arcv =
   let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
-  let g = 
-    if is_set_arc arcu then set_predicative g arcv
-    else g
-  in
     enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
@@ -1100,11 +1109,6 @@ let setlt_if (g,arcu) v =
 (* this is normally an update of u in g rather than a creation. *)
 let setleq g arcu arcv =
   let arcu' = {arcu with le=arcv.univ::arcu.le} in
-  let g = 
-    if is_set_arc arcu' then
-      set_predicative g arcv
-    else g
-  in
     enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
@@ -1120,7 +1124,8 @@ let merge g arcu arcv =
   (* we find the arc with the biggest rank, and we redirect all others to it *)
   let arcu, g, v =
     let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if Level.is_small arc.univ || arc.rank >= max_rank
+      if Level.is_small arc.univ ||
+	   (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
@@ -1150,7 +1155,7 @@ let merge g arcu arcv =
 (* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g arc1 arc2 =
-  let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
   let arcu, g = 
     if not (Int.equal arc1.rank arc2.rank) then arcu, g
     else
@@ -1173,12 +1178,11 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v (p:explanation option) =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforc_univ_eq : Level.t -> Level.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_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 and arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT ->
@@ -1197,8 +1201,7 @@ 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 and arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -1211,8 +1214,7 @@ 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 and arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -1225,18 +1227,10 @@ let enforce_univ_lt u v g =
         let p = get_explanation false g arcv arcu  in
         error_inconsistency Lt u v p
 
-let empty_universes = UMap.empty
-
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes = empty_universes
 
 let is_initial_universes g = UMap.equal (==) g initial_universes
-
-let add_universe vlev g = 
-  let v = terminal vlev in
-  let proparc = get_prop_arc g in
-    enter_arc {proparc with le=vlev::proparc.le}
-      (enter_arc v g)
       
 (* Constraints and sets of constraints. *)    
 
@@ -1370,10 +1364,12 @@ let check_univ_leq u v =
 
 let enforce_leq u v c =
   let open Universe.Huniv in
+  let rec aux acc v =
   match v with
-  | Cons (v, _, Nil) ->
-    fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+  | Cons (v, _, l) ->
+    aux (fold (fun u -> constraint_add_leq u v) u c) l
+  | Nil -> acc
+  in aux c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
@@ -1444,7 +1440,6 @@ let normalize_universes g =
         lt = LSet.elements lt;
         le = LSet.elements le;
 	rank = rank;
-	predicative = false;
 	status = Unset;
       }
   in
@@ -1589,7 +1584,7 @@ let sort_universes orig =
   let fold i accu u =
     if 0 < i then
       let pred = types.(i - 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
       UMap.add u (Canonical arc) accu
     else accu
   in