1 files changed, 152 insertions, 96 deletions

diff --git a/library/universes.ml b/library/universes.ml
index 7972c478..112b20a4 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -13,10 +13,11 @@ open Term
 open Environ
 open Univ
 open Globnames
+open Decl_kinds
 
 (** Global universe names *)
 type universe_names = 
-    Univ.universe_level Idmap.t * Id.t Univ.LMap.t
+  (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
 
 let global_universes =
   Summary.ref ~name:"Global universe names"
@@ -102,6 +103,7 @@ module Constraints = struct
 end
 
 type universe_constraints = Constraints.t
+type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option
 type 'a universe_constrained = 'a * universe_constraints
 
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
@@ -110,7 +112,7 @@ let enforce_eq_instances_univs strict x y c =
   let d = if strict then ULub else UEq in
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
-      Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
+      CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
 	       Pp.str " instances of different lengths");
     CArray.fold_right2
       (fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
@@ -135,82 +137,76 @@ let to_constraints g s =
       | _, ULe, Some l' -> enforce_leq x y acc
       | _, ULub, _ -> acc
       | _, d, _ -> 
-	let f = if d == ULe then check_leq else check_eq in
+	let f = if d == ULe then UGraph.check_leq else UGraph.check_eq in
 	  if f g x y then acc else 
 	    raise (Invalid_argument 
 		   "to_constraints: non-trivial algebraic constraint between universes")
   in Constraints.fold tr s Constraint.empty
 
-let eq_constr_univs_infer univs m n =
-  if m == n then true, Constraints.empty
+let eq_constr_univs_infer univs fold m n accu =
+  if m == n then Some accu
   else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict = Univ.Instance.check_eq univs in
+    let cstrs = ref accu in
+    let eq_universes strict = UGraph.check_eq_instances univs in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else
-	    (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-	     true)
+	match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+	| None -> false
+	| Some accu -> cstrs := accu; true
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    if res then Some !cstrs else None
 
 (** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
     to expose subterms of [m] and [n], arguments. *)
-let eq_constr_univs_infer_with kind1 kind2 univs m n =
+let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
   (* spiwack: duplicates the code of [eq_constr_univs_infer] because I
      haven't find a way to factor the code without destroying
      pointer-equality optimisations in [eq_constr_univs_infer].
      Pointer equality is not sufficient to ensure equality up to
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
-  let cstrs = ref Constraints.empty in
-  let eq_universes strict = Univ.Instance.check_eq univs in
+  let cstrs = ref accu in
+  let eq_universes strict = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 = 
     if Sorts.equal s1 s2 then true
     else
       let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      if Univ.check_eq univs u1 u2 then true
-      else
-	(cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-	 true)
+      match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+      | None -> false
+      | Some accu -> cstrs := accu; true
   in
   let rec eq_constr' m n = 
     Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n
   in
   let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in
-  res, !cstrs
+  if res then Some !cstrs else None
 
-let leq_constr_univs_infer univs m n =
-  if m == n then true, Constraints.empty
+let leq_constr_univs_infer univs fold m n accu =
+  if m == n then Some accu
   else 
-    let cstrs = ref Constraints.empty in
-    let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
+    let cstrs = ref accu in
+    let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	if Univ.check_eq univs u1 u2 then true
-	else (cstrs := Constraints.add (u1, UEq, u2) !cstrs;
-	      true)
+	match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+	| None -> false
+	| Some accu -> cstrs := accu; true
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then
-	    ((if Univ.is_type0_univ u1 then
-		cstrs := Constraints.add (u1, ULe, u2) !cstrs);
-	     true)
-	  else
-	    (cstrs := Constraints.add (u1, ULe, u2) !cstrs; 
-	     true)
+	match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with
+	| None -> false
+	| Some accu -> cstrs := accu; true
     in
     let rec eq_constr' m n = 
       m == n ||	Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -220,7 +216,7 @@ let leq_constr_univs_infer univs m n =
 	eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
-    res, !cstrs
+    if res then Some !cstrs else None
 
 let eq_constr_universes m n =
   if m == n then true, Constraints.empty
@@ -341,7 +337,7 @@ let existing_instance ctx inst =
     and a2 = Instance.to_array (UContext.instance ctx) in
     let len1 = Array.length a1 and len2 = Array.length a2 in 
       if not (len1 == len2) then
-	Errors.errorlabstrm "Universes"
+	CErrors.errorlabstrm "Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
 	     str" levels but was given " ++ int len1)
       else ()
@@ -650,14 +646,14 @@ let normalize_univ_variable_opt_subst ectx =
   in
   let update l b =
     assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    ectx := Univ.LMap.add l (Some b) !ectx; b
+    try ectx := Univ.LMap.add l (Some b) !ectx; b with Not_found -> assert false
   in normalize_univ_variable ~find ~update
 
 let normalize_univ_variable_subst subst =
   let find l = Univ.LMap.find l !subst in
   let update l b =
     assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
-    subst := Univ.LMap.add l b !subst; b in
+    try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in
     normalize_univ_variable ~find ~update
 
 let normalize_universe_opt_subst subst =
@@ -706,12 +702,45 @@ let pr_universe_body = function
 
 let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body
 
-exception Found of Level.t
+let compare_constraint_type d d' =
+  match d, d' with
+  | Eq, Eq -> 0
+  | Eq, _ -> -1
+  | _, Eq -> 1
+  | Le, Le -> 0
+  | Le, _ -> -1
+  | _, Le -> 1
+  | Lt, Lt -> 0
+
+type lowermap = constraint_type LMap.t
+
+let lower_union =
+  let merge k a b =
+    match a, b with
+    | Some _, None -> a
+    | None, Some _ -> b
+    | None, None -> None
+    | Some l, Some r ->
+       if compare_constraint_type l r >= 0 then a
+       else b
+  in LMap.merge merge
+
+let lower_add l c m =
+  try let c' = LMap.find l m in
+      if compare_constraint_type c c' > 0 then
+        LMap.add l c m
+      else m
+  with Not_found -> LMap.add l c m
+
+let lower_of_list l =
+  List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l
+
+exception Found of Level.t * lowermap
 let find_inst insts v =
-  try LMap.iter (fun k (enf,alg,v') ->
-    if not alg && enf && Universe.equal v' v then raise (Found k))
+  try LMap.iter (fun k (enf,alg,v',lower) ->
+    if not alg && enf && Universe.equal v' v then raise (Found (k, lower)))
 	insts; raise Not_found
-  with Found l -> l
+  with Found (f,l) -> (f,l)
 
 let compute_lbound left =
  (** The universe variable was not fixed yet.
@@ -730,27 +759,33 @@ let compute_lbound left =
 	 else None))
       None left
   
-let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) =
+let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) =
   if enforce then
     let inst = Universe.make u in
     let cstrs' = enforce_leq lbound inst cstrs in
       (ctx, us, LSet.remove u algs, 
-       LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst)
+       LMap.add u (enforce,alg,lbound,lower) insts, cstrs'),
+      (enforce, alg, inst, lower)
   else (* Actually instantiate *)
     (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs,
-     LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound)
+     LMap.add u (enforce,alg,lbound,lower) insts, cstrs),
+    (enforce, alg, lbound, lower)
 
 type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t
 
 let pr_constraints_map cmap =
   LMap.fold (fun l cstrs acc -> 
     Level.pr l ++ str " => " ++ 
-      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl ()
-    ++ acc)
+      prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++
+      fnl () ++ acc)
     cmap (mt ())
 
 let remove_alg l (ctx, us, algs, insts, cstrs) =
   (ctx, us, LSet.remove l algs, insts, cstrs)
+
+let remove_lower u lower =
+  let levels = Universe.levels u in
+  LSet.fold (fun l acc -> LMap.remove l acc) levels lower
     
 let minimize_univ_variables ctx us algs left right cstrs =
   let left, lbounds = 
@@ -760,22 +795,50 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let lbounds' = 
 	  match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with
 	  | None -> lbounds
-	  | Some lbound -> LMap.add r (true, false, lbound) lbounds
+	  | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower)
+                                   lbounds
 	in (Univ.LMap.remove r left, lbounds'))
       left (left, Univ.LMap.empty)
   in
   let rec instance (ctx', us, algs, insts, cstrs as acc) u =
-    let acc, left = 
-      try let l = LMap.find u left in
-	    List.fold_left
-	      (fun (acc, left') (d, l) -> 
-	       let acc', (enf,alg,l') = aux acc l in
-	       let l' = 
-		 if enf then Universe.make l 
-		 else l' 
-	       in acc', (d, l') :: left')
-	      (acc, []) l
-      with Not_found -> acc, []
+    let acc, left, lower =
+      try
+        let l = LMap.find u left in
+	let acc, left, newlow, lower =
+          List.fold_left
+	  (fun (acc, left', newlow, lower') (d, l) ->
+	   let acc', (enf,alg,l',lower) = aux acc l in
+	   let l' =
+	     if enf then Universe.make l
+	     else l'
+	   in acc', (d, l') :: left',
+              lower_add l d newlow, lower_union lower lower')
+	  (acc, [], LMap.empty, LMap.empty) l
+        in
+        let not_lower (d,l) =
+        (* We're checking if (d,l) is already implied by the lower
+	  constraints on some level u. If it represents l < u (d is Lt
+	  or d is Le and i > 0, the i < 0 case is impossible due to
+	  invariants of Univ), and the lower constraints only have l <=
+	  u then it is not implied. *)
+          Univ.Universe.exists
+          (fun (l,i) ->
+             let d =
+               if i == 0 then d
+               else match d with
+                    | Le -> Lt
+                    | d -> d
+             in
+             try let d' = LMap.find l lower in
+                 (* If d is stronger than the already implied lower
+                  * constraints we must keep it. *)
+                 compare_constraint_type d d' > 0
+             with Not_found ->
+               (** No constraint existing on l *) true) l
+        in
+        let left = List.uniquize (List.filter not_lower left) in
+        (acc, left, LMap.union newlow lower)
+      with Not_found -> acc, [], LMap.empty
     and right =
       try Some (LMap.find u right)
       with Not_found -> None
@@ -783,31 +846,33 @@ let minimize_univ_variables ctx us algs left right cstrs =
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
 	if alg then
-	  (* u is algebraic: we instantiate it with it's lower bound, if any, 
+	  (* u is algebraic: we instantiate it with its lower bound, if any,
               or enforce the constraints if it is bounded from the top. *)
-	  instantiate_with_lbound u lbound true false acc
+          let lower = remove_lower lbound lower in
+	  instantiate_with_lbound u lbound lower true false acc
 	else (* u is non algebraic *)
 	  match Universe.level lbound with
 	  | Some l -> (* The lowerbound is directly a level *) 
 	     (* u is not algebraic but has no upper bounds,
   	        we instantiate it with its lower bound if it is a 
 	        different level, otherwise we keep it. *)
+             let lower = LMap.remove l lower in
 	     if not (Level.equal l u) then
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
 	       let acc' = remove_alg l acc in
-		 instantiate_with_lbound u lbound false false acc'
-	     else acc, (true, false, lbound)
-	| None -> 
-	  try 
-	    (* if right <> None then raise Not_found; *)
-	    (* Another universe represents the same lower bound, 
-	       we can share them with no harm. *)
-	    let can = find_inst insts lbound in
-	      instantiate_with_lbound u (Universe.make can) false false acc
+		 instantiate_with_lbound u lbound lower false false acc'
+	     else acc, (true, false, lbound, lower)
+	  | None ->
+	     try
+	       (* Another universe represents the same lower bound,
+                  we can share them with no harm. *)
+	       let can, lower = find_inst insts lbound in
+               let lower = LMap.remove can lower in
+	       instantiate_with_lbound u (Universe.make can) lower false false acc
 	  with Not_found -> 
 	    (* We set u as the canonical universe representing lbound *)
-	    instantiate_with_lbound u lbound false true acc
+	    instantiate_with_lbound u lbound lower false true acc
     in
     let acc' acc = 
       match right with
@@ -816,7 +881,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
 	  if List.is_empty dangling then acc
 	  else
-	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in
+	    let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in
 	    let cstrs' = List.fold_left (fun cstrs (d, r) -> 
 	      if d == Univ.Le then
 		enforce_leq inst (Universe.make r) cstrs
@@ -828,15 +893,15 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    in
 	      (ctx', us, algs, insts, cstrs'), b
     in
-      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u))
+      if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower))
       else
 	let lbound = compute_lbound left in
 	  match lbound with
 	  | None -> (* Nothing to do *)
-	    acc' (acc, (true, false, Universe.make u))
+	    acc' (acc, (true, false, Universe.make u, lower))
 	  | Some lbound ->
 	     try acc' (instantiate_lbound lbound) 
-	     with Failure _ -> acc' (acc, (true, false, Universe.make u))
+	     with Failure _ -> acc' (acc, (true, false, Universe.make u, lower))
   and aux (ctx', us, algs, seen, cstrs as acc) u =
     try acc, LMap.find u seen 
     with Not_found -> instance acc u
@@ -869,27 +934,27 @@ let normalize_context_set ctx us algs =
   let csts = 
     (* We first put constraints in a normal-form: all self-loops are collapsed
        to equalities. *)
-    let g = Univ.LSet.fold (fun v g -> Univ.add_universe v false g)
-			   ctx Univ.empty_universes
+    let g = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g)
+			   ctx UGraph.empty_universes
     in
     let g =
       Univ.Constraint.fold
 	(fun (l, d, r) g ->
 	 let g =
 	   if not (Level.is_small l || LSet.mem l ctx) then
-	     try Univ.add_universe l false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe l false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in
 	 let g =
 	   if not (Level.is_small r || LSet.mem r ctx) then
-	     try Univ.add_universe r false g
-	     with Univ.AlreadyDeclared -> g
+	     try UGraph.add_universe r false g
+	     with UGraph.AlreadyDeclared -> g
 	   else g
 	 in g) csts g
     in
-    let g = Univ.Constraint.fold Univ.enforce_constraint csts g in
-      Univ.constraints_of_universes g
+    let g = Univ.Constraint.fold UGraph.enforce_constraint csts g in
+      UGraph.constraints_of_universes g
   in
   let noneqs =
     Constraint.fold (fun (l,d,r as cstr) noneqs ->
@@ -930,9 +995,7 @@ let normalize_context_set ctx us algs =
      mentionning other variables remain in noneqs. *)
   let noneqs, ucstrsl, ucstrsr = 
     Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> 
-      let lus = LMap.mem l us 
-      and rus = LMap.mem r us
-      in
+      let lus = LMap.mem l us and rus = LMap.mem r us in
       let ucstrsl' = 
 	if lus then add_list_map l (d, r) ucstrsl
 	else ucstrsl
@@ -959,10 +1022,10 @@ let universes_of_constr c =
   let rec aux s c = 
     match kind_of_term c with
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.union (Instance.levels u) s
+      LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
       let u = univ_of_sort u in
-	LSet.union (Universe.levels u) s
+      LSet.fold LSet.add (Universe.levels u) s
     | _ -> fold_constr aux s c
   in aux LSet.empty c
 
@@ -1027,7 +1090,7 @@ let refresh_constraints univs (ctx, cstrs) =
     Univ.Constraint.fold (fun c (cstrs', univs as acc) -> 
       let c = translate_cstr c in
       if is_trivial_leq c then acc
-      else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs))
+      else (Univ.Constraint.add c cstrs', UGraph.enforce_constraint c univs))
       cstrs (Univ.Constraint.empty, univs)
   in ((ctx, cstrs'), univs')
 
@@ -1094,13 +1157,6 @@ let solve_constraints_system levels level_bounds level_min =
     for j=0 to nind-1 do
       if not (Int.equal i j) && Int.Set.mem j clos.(i) then
 	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
-	 (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *)
     done;
-    (* for j=0 to nind-1 do *)
-    (*   match levels.(j) with *)
-    (*   | Some u when not (Univ.Level.is_small u) -> *)
-    (* 	 v.(i) <- univ_level_rem u v.(i) level_min.(i) *)
-    (*   | _ -> () *)
-    (* done *)
   done;
   v