Statically enforce that ULub is only between levels.

7 files changed, 128 insertions, 100 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index e832a0688..0d55b92c2 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -579,15 +579,18 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
     CArray.fold_left3
       (fun cstrs v u u' ->
          let open Univ.Variance in
-         let u = Univ.Universe.make u in
-         let u' = Univ.Universe.make u' in
          match v with
-         | Irrelevant -> if !cumul_weak_constraints then Constraints.add (u,ULub,u') cstrs else cstrs
+         | Irrelevant -> if !cumul_weak_constraints then Constraints.add (ULub (u,u')) cstrs else cstrs
          | Covariant ->
+           let u = Univ.Universe.make u in
+           let u' = Univ.Universe.make u' in
            (match cv_pb with
-            | Reduction.CONV -> Constraints.add (u,UEq,u') cstrs
-            | Reduction.CUMUL -> Constraints.add (u,ULe,u') cstrs)
-         | Invariant -> Constraints.add (u,UEq,u') cstrs)
+            | Reduction.CONV -> Constraints.add (UEq (u,u')) cstrs
+            | Reduction.CUMUL -> Constraints.add (ULe (u,u')) cstrs)
+         | Invariant ->
+           let u = Univ.Universe.make u in
+           let u' = Univ.Universe.make u' in
+           Constraints.add (UEq (u,u')) cstrs)
       cstrs variances (Univ.Instance.to_array u) (Univ.Instance.to_array u')
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
@@ -648,7 +651,7 @@ let test_constr_universes env sigma leq m n =
       let s2 = ESorts.kind sigma (ESorts.make s2) in
       if Sorts.equal s1 s2 then true
       else (cstrs := Constraints.add 
-	      (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; 
+              (UEq (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	    true)
     in
     let leq_sorts s1 s2 = 
@@ -657,7 +660,7 @@ let test_constr_universes env sigma leq m n =
       if Sorts.equal s1 s2 then true
       else 
 	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; 
+           (ULe (Sorts.univ_of_sort s1,Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
     let rec eq_constr' nargs m n = compare_gen kind eq_universes eq_sorts eq_constr' nargs m n in
@@ -703,7 +706,7 @@ let eq_constr_universes_proj env sigma m n =
       if Sorts.equal s1 s2 then true
       else
 	(cstrs := Constraints.add 
-	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+           (UEq (Sorts.univ_of_sort s1, Sorts.univ_of_sort s2)) !cstrs;
 	 true)
     in
     let rec eq_constr' nargs m n =
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 2b6913c0b..fdb14b725 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -815,8 +815,7 @@ let subterm_source evk (loc,k) =
 
 let try_soft evd u u' =
   let open Universes in
-  let make = Univ.Universe.make in
-  try Evd.add_universe_constraints evd (Constraints.singleton (make u,ULub,make u'))
+  try Evd.add_universe_constraints evd (Constraints.singleton (ULub (u, u')))
   with UState.UniversesDiffer | Univ.UniverseInconsistency _ -> evd
 
 (* Add equality constraints for covariant/invariant positions. For
diff --git a/engine/evd.ml b/engine/evd.ml
index b7b87370e..f6e13e1f4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -857,15 +857,10 @@ let set_eq_sort env d s1 s2 =
   | Some (u1, u2) ->
     if not (type_in_type env) then
       add_universe_constraints d
-        (Universes.Constraints.singleton (u1,Universes.UEq,u2))
+        (Universes.Constraints.singleton (Universes.UEq (u1,u2)))
     else
       d
 
-let has_lub evd u1 u2 =
-  if Univ.Universe.equal u1 u2 then evd
-  else add_universe_constraints evd
-    (Universes.Constraints.singleton (u1,Universes.ULub,u2))
-
 let set_eq_level d u1 u2 =
   add_constraints d (Univ.enforce_eq_level u1 u2 Univ.Constraint.empty)
 
@@ -883,7 +878,7 @@ let set_leq_sort env evd s1 s2 =
   | None -> evd
   | Some (u1, u2) ->
      if not (type_in_type env) then
-       add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+       add_universe_constraints evd (Universes.Constraints.singleton (Universes.ULe (u1,u2)))
      else evd
 	    
 let check_eq evd s s' =
diff --git a/engine/evd.mli b/engine/evd.mli
index bd9d75c6b..911799c44 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -583,7 +583,6 @@ val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t
 
 val set_leq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
 val set_eq_sort : env -> evar_map -> Sorts.t -> Sorts.t -> evar_map
-val has_lub : evar_map -> Univ.Universe.t -> Univ.Universe.t -> evar_map
 val set_eq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_leq_level : evar_map -> Univ.Level.t -> Univ.Level.t -> evar_map
 val set_eq_instances : ?flex:bool -> 
diff --git a/engine/uState.ml b/engine/uState.ml
index e57afd743..8111ebffe 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -144,9 +144,15 @@ exception UniversesDiffer
 
 let process_universe_constraints ctx cstrs =
   let open Univ in
+  let open Universes in
   let univs = ctx.uctx_universes in
   let vars = ref ctx.uctx_univ_variables in
-  let normalize = Universes.normalize_universe_opt_subst vars in
+  let normalize = normalize_univ_variable_opt_subst vars in
+  let nf_constraint = function
+    | ULub (u, v) -> ULub (level_subst_of normalize u, level_subst_of normalize v)
+    | UEq (u, v) -> UEq (subst_univs_universe normalize u, subst_univs_universe normalize v)
+    | ULe (u, v) -> ULe (subst_univs_universe normalize u, subst_univs_universe normalize v)
+  in
   let is_local l = Univ.LMap.mem l !vars in
   let varinfo x =
     match Univ.Universe.level x with
@@ -185,12 +191,12 @@ let process_universe_constraints ctx cstrs =
     if UGraph.check_eq univs l r then local
     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
-  let unify_universes (l, d, r) local =
-    let l = normalize l and r = normalize r in
-      if Univ.Universe.equal l r then local
+  let unify_universes cst local =
+    let cst = nf_constraint cst in
+      if Constraints.is_trivial cst then local
       else 
-          match d with
-          | Universes.ULe ->
+          match cst with
+          | ULe (l, r) ->
             if UGraph.check_leq univs l r then
               (** Keep Prop/Set <= var around if var might be instantiated by prop or set
                   later. *)
@@ -218,16 +224,12 @@ let process_universe_constraints ctx cstrs =
                 else
                   Univ.enforce_leq l r local
               end
-          | Universes.ULub ->
-            begin match Universe.level l, Universe.level r with
-            | Some l', Some r' ->
-              equalize_variables true l l' r r' local
-            | _, _ -> assert false
-            end
-          | Universes.UEq -> equalize_universes l r local
+          | ULub (l, r) ->
+              equalize_variables true (Universe.make l) l (Universe.make r) r local
+          | UEq (l, r) -> equalize_universes l r local
   in
   let local = 
-    Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty
+    Constraints.fold unify_universes cstrs Univ.Constraint.empty
   in
     !vars, local
 
@@ -235,9 +237,11 @@ let add_constraints ctx cstrs =
   let univs, local = ctx.uctx_local in
   let cstrs' = Univ.Constraint.fold (fun (l,d,r) acc -> 
     let l = Univ.Universe.make l and r = Univ.Universe.make r in
-    let cstr' = 
-      if d == Univ.Lt then (Univ.Universe.super l, Universes.ULe, r)
-      else (l, (if d == Univ.Le then Universes.ULe else Universes.UEq), r)
+    let cstr' = match d with
+      | Univ.Lt ->
+        Universes.ULe (Univ.Universe.super l, r)
+      | Univ.Le -> Universes.ULe (l, r)
+      | Univ.Eq -> Universes.UEq (l, r)
     in Universes.Constraints.add cstr' acc)
     cstrs Universes.Constraints.empty
   in
diff --git a/engine/universes.ml b/engine/universes.ml
index 70ed6311e..ae5eef067 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -114,53 +114,56 @@ let universe_binders_with_opt_names ref levels = function
 let set_minimization = ref true
 let is_set_minimization () = !set_minimization
 			    
-type universe_constraint_type = ULe | UEq | ULub
-
-type universe_constraint = Universe.t * universe_constraint_type * Universe.t
+type universe_constraint =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
 
 module Constraints = struct
   module S = Set.Make(
   struct 
     type t = universe_constraint
 
-    let compare_type c c' =
-      match c, c' with
-      | ULe, ULe -> 0
-      | ULe, _ -> -1
-      | _, ULe -> 1
-      | UEq, UEq -> 0
-      | UEq, _ -> -1
-      | ULub, ULub -> 0
-      | ULub, _ -> 1
-      
-    let compare (u,c,v) (u',c',v') =
-      let i = compare_type c c' in
-	if Int.equal i 0 then
-	  let i' = Universe.compare u u' in
-	    if Int.equal i' 0 then Universe.compare v v'
-	    else 
-	      if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0
-	      else i'
-	else i
+    let compare x y =
+      match x, y with
+      | ULe (u, v), ULe (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else i
+      | UEq (u, v), UEq (u', v') ->
+        let i = Universe.compare u u' in
+        if Int.equal i 0 then Universe.compare v v'
+        else if Universe.equal u v' && Universe.equal v u' then 0
+        else i
+      | ULub (u, v), ULub (u', v') ->
+        let i = Level.compare u u' in
+        if Int.equal i 0 then Level.compare v v'
+        else if Level.equal u v' && Level.equal v u' then 0
+        else i
+      | ULe _, _ -> -1
+      | _, ULe _ -> 1
+      | UEq _, _ -> -1
+      | _, UEq _ -> 1
   end)
   
   include S
-  
-  let add (l,d,r as cst) s = 
-    if Universe.equal l r then s
-    else add cst s
 
-  let tr_dir = function
-    | ULe -> Le
-    | UEq -> Eq
-    | ULub -> Eq
+  let is_trivial = function
+    | ULe (u, v) | UEq (u, v) -> Universe.equal u v
+    | ULub (u, v) -> Level.equal u v
 
-  let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ "
+  let add cst s =
+    if is_trivial cst then s
+    else add cst s
+
+  let pr_one = function
+    | ULe (u, v) -> Universe.pr u ++ str " <= " ++ Universe.pr v
+    | UEq (u, v) -> Universe.pr u ++ str " = " ++ Universe.pr v
+    | ULub (u, v) -> Level.pr u ++ str " /\\ " ++ Level.pr v
 
   let pr c =
-    fold (fun (u1,op,u2) pp_std ->
-	pp_std ++ Universe.pr u1 ++ str (op_str op) ++
-	Universe.pr u2 ++ fnl ()) c (str "")
+    fold (fun cst pp_std ->
+        pp_std ++ pr_one cst ++ fnl ()) c (str "")
 
   let equal x y = 
     x == y || equal x y
@@ -174,13 +177,13 @@ type 'a universe_constrained = 'a * universe_constraints
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
 
 let enforce_eq_instances_univs strict x y c = 
-  let d = if strict then ULub else UEq in
+  let mk u v = if strict then ULub (u, v) else UEq (Universe.make u, Universe.make v) in
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
       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))
+      (fun x y -> Constraints.add (mk x y))
       ax ay c
 
 let enforce_univ_constraint (u,d,v) =
@@ -207,30 +210,59 @@ let subst_univs_constraints subst csts =
     (fun c cstrs -> subst_univs_constraint subst c cstrs)
     csts Constraint.empty
 
-let subst_univs_universe_constraint fn (u,d,v) =
-  let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+let level_subst_of f =
+  fun l ->
+    try let u = f l in
+          match Universe.level u with
+          | None -> l
+          | Some l -> l
+    with Not_found -> l
+
+let subst_univs_universe_constraint fn = function
+  | ULe (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
     if Universe.equal u' v' then None
-    else Some (u',d,v')
+    else Some (ULe (u',v'))
+  | UEq (u, v) ->
+    let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
+    if Universe.equal u' v' then None
+    else Some (ULe (u',v'))
+  | ULub (u, v) ->
+    let u' = level_subst_of fn u and v' = level_subst_of fn v in
+    if Level.equal u' v' then None
+    else Some (ULub (u',v'))
 
 let subst_univs_universe_constraints subst csts =
   Constraints.fold 
     (fun c -> Option.fold_right Constraints.add (subst_univs_universe_constraint subst c))
     csts Constraints.empty 
 
-
-let to_constraints g s = 
-  let tr (x,d,y) acc =
-    let add l d l' acc = Constraint.add (l,Constraints.tr_dir d,l') acc in
-      match Universe.level x, d, Universe.level y with
-      | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc
-      | _, ULe, Some l' -> enforce_leq x y acc
-      | _, ULub, _ -> acc
-      | _, d, _ -> 
-	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 to_constraints g s =
+  let invalid () =
+    raise (Invalid_argument "to_constraints: non-trivial algebraic constraint between universes")
+  in
+  let tr cst acc =
+    match cst with
+    | ULub (l, l') -> Constraint.add (l, Eq, l') acc
+    | ULe (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Le, l') acc
+        | None, Some _ -> enforce_leq l l' acc
+        | _, None ->
+          if UGraph.check_leq g l l'
+          then acc
+          else invalid ()
+      end
+    | UEq (l, l') ->
+      begin match Universe.level l, Universe.level l' with
+        | Some l, Some l' -> Constraint.add (l, Eq, l') acc
+        | None, _ | _, None ->
+          if UGraph.check_eq g l l'
+          then acc
+          else invalid ()
+      end
+  in
+  Constraints.fold tr s Constraint.empty
 
 (** Variant of [eq_constr_univs_infer] taking kind-of-term functions,
     to expose subterms of [m] and [n], arguments. *)
@@ -247,7 +279,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
     if Sorts.equal s1 s2 then true
     else
       let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-      match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with
+      match fold (Constraints.singleton (UEq (u1, u2))) !cstrs with
       | None -> false
       | Some accu -> cstrs := accu; true
   in
@@ -512,14 +544,6 @@ let choose_canonical ctx flexible algs s =
 	      let canon = LSet.choose algs in
 		canon, (global, rigid, LSet.remove canon flexible)
 
-let level_subst_of f =
-  fun l ->
-    try let u = f l in
-          match Universe.level u with
-          | None -> l
-          | Some l -> l
-    with Not_found -> l
-
 let subst_univs_fn_constr f c =
   let changed = ref false in
   let fu = Univ.subst_univs_universe f in
diff --git a/engine/universes.mli b/engine/universes.mli
index a86b9779b..4af944347 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -71,12 +71,16 @@ val new_sort_in_family : Sorts.family -> Sorts.t
     not be necessary if unfolding is performed.
 *)
 
-type universe_constraint_type = ULe | UEq | ULub
+type universe_constraint =
+  | ULe of Universe.t * Universe.t
+  | UEq of Universe.t * Universe.t
+  | ULub of Level.t * Level.t
 
-type universe_constraint = Universe.t * universe_constraint_type * Universe.t
 module Constraints : sig
   include Set.S with type elt = universe_constraint
 
+  val is_trivial : universe_constraint -> bool
+
   val pr : t -> Pp.t
 end