Make kernel reduction code parametric over the handling of universes,

allowing fast conversion to be used during unification while respecting the
semantics of unification w.r.t universes.
- Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv
is used for module subtyping.
- Outside, infer_conv is wrapped in Reductionops to register the right constraints
in an evarmap.
- In univ, add a flag to universes to cache the fact that they are >= Set, the
most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).

7 files changed, 197 insertions, 112 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index fbcdc886b2..532d44d9ed 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -578,16 +578,18 @@ let leq_constr_univs univs m n =
       compare_leq m n
 
 let eq_constr_univs_infer univs m n =
-  if m == n then true, Constraint.empty
+  if m == n then true, UniverseConstraints.empty
   else 
-    let cstrs = ref Constraint.empty in
+    let cstrs = ref UniverseConstraints.empty in
     let eq_universes strict = Univ.Instance.check_eq 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
-	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	   true)
+	  if Univ.check_eq univs u1 u2 then true
+	  else
+	    (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs;
+	     true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -596,23 +598,26 @@ let eq_constr_univs_infer univs m n =
       res, !cstrs
 
 let leq_constr_univs_infer univs m n =
-  if m == n then true, Constraint.empty
+  if m == n then true, UniverseConstraints.empty
   else 
-    let cstrs = ref Constraint.empty in
+    let cstrs = ref UniverseConstraints.empty in
     let eq_universes strict l l' = Univ.Instance.check_eq 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
-	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	   true)
+	  if Univ.check_eq univs u1 u2 then true
+	  else (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs;
+		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
-	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	   true)
+	  if Univ.check_leq univs u1 u2 then true
+	  else
+	    (cstrs := Univ.UniverseConstraints.add (u1, Univ.ULe, u2) !cstrs; 
+	     true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
diff --git a/kernel/constr.mli b/kernel/constr.mli
index e9f7369034..c57c4c59b2 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -212,11 +212,11 @@ val leq_constr_univs : constr Univ.check_function
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
+val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe inequalities in [u]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
+val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained
 
 (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [c]. *)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 766e6513c7..5964ed70ed 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -70,7 +70,7 @@ and conv_atom pb lvl a1 a2 cu =
 	if not (eq_constant c1 c2) then raise NotConvertible;
 	cu
     | Asort s1, Asort s2 -> 
-	ignore(sort_cmp_universes pb s1 s2 (cu, None)); cu
+        check_sort_cmp_universes pb s1 s2 cu; cu
     | Avar id1, Avar id2 ->
 	if not (Id.equal id1 id2) then raise NotConvertible;
 	cu
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5024675bff..b62ca2045f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -153,25 +153,51 @@ type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_fun
 type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit
 type 'a trans_universe_conversion_function = 
   Names.transparent_state -> 'a universe_conversion_function
+
+exception NotConvertible
+exception NotConvertibleVect of int
+
+
+(* Convertibility of sorts *)
+
+(* The sort cumulativity is
+
+    Prop <= Set <= Type 1 <= ... <= Type i <= ...
+
+    and this holds whatever Set is predicative or impredicative
+*)
+
+type conv_pb =
+  | CONV
+  | CUMUL
+
+let is_cumul = function CUMUL -> true | CONV -> false
+let is_pos = function Pos -> true | Null -> false
+
+type 'a universe_compare = 
+  { (* Might raise NotConvertible *)
+    compare : conv_pb -> sorts -> sorts -> 'a -> 'a;
+    compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+  } 
+
+type 'a universe_state = 'a * 'a universe_compare
+
+type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
+
 type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
 
 type conv_universes = Univ.universes * Univ.constraints option
 
-exception NotConvertible
-exception NotConvertibleVect of int
+let sort_cmp_universes pb s0 s1 (u, check) =
+  (check.compare pb s0 s1 u, check)
+
+let convert_instances flex u u' (s, check) =
+  (check.compare_instances flex u u' s, check)
 
-let convert_universes (univs,cstrs as cuniv) u u' =
-  if Univ.Instance.check_eq univs u u' then cuniv
-  else
-    (match cstrs with 
-    | None -> raise NotConvertible
-    | Some cstrs -> 
-      (univs, Some (Univ.enforce_eq_instances u u' cstrs)))
-      
 let conv_table_key k1 k2 cuniv =
   match k1, k2 with
   | ConstKey (cst, u), ConstKey (cst', u') when eq_constant_key cst cst' ->
-    convert_universes cuniv u u'
+    convert_instances true u u' cuniv
   | _ -> raise NotConvertible
 
 let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
@@ -199,59 +225,6 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
   else raise NotConvertible
 
-(* Convertibility of sorts *)
-
-(* The sort cumulativity is
-
-    Prop <= Set <= Type 1 <= ... <= Type i <= ...
-
-    and this holds whatever Set is predicative or impredicative
-*)
-
-type conv_pb =
-  | CONV
-  | CUMUL
-
-let is_cumul = function CUMUL -> true | CONV -> false
-let is_pos = function Pos -> true | Null -> false
-
-let check_eq (univs, cstrs as cuniv) u u' = 
-  match cstrs with
-  | None -> if check_eq univs u u' then cuniv else raise NotConvertible
-  | Some cstrs -> 
-    univs, Some (Univ.enforce_eq u u' cstrs)
-
-let check_leq ?(record=false) (univs, cstrs as cuniv) u u' = 
-  match cstrs with
-  | None -> if check_leq univs u u' then cuniv else raise NotConvertible
-  | Some cstrs -> 
-    let cstrs' = Univ.enforce_leq u u' cstrs in
-    let cstrs' = if record then 
-	Univ.Constraint.add (Option.get (Univ.Universe.level u),Univ.Le,
-			     Option.get (Univ.Universe.level u')) cstrs' 
-      else cstrs' 
-    in
-      univs, Some cstrs'
-
-let sort_cmp_universes pb s0 s1 univs =
-  match (s0,s1) with
-    | (Prop c1, Prop c2) when is_cumul pb ->
-      begin match c1, c2 with
-      | Null, _ | _, Pos -> univs (* Prop <= Set *)
-      | _ -> raise NotConvertible
-      end
-    | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible
-    | (Prop c1, Type u) ->
-      let u0 = univ_of_sort s0 in
-	(match pb with
-	| CUMUL -> check_leq ~record:true univs u0 u
-	| CONV -> check_eq univs u0 u)
-    | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) -> 
-	(match pb with
-	| CUMUL -> check_leq univs u1 u2
-	| CONV -> check_eq univs u1 u2)
-
 let rec no_arg_available = function
   | [] -> true
   | Zupdate _ :: stk -> no_arg_available stk
@@ -489,14 +462,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
         if eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_universes cuniv u1 u2 in
+	  (let cuniv = convert_instances false u1 u2 cuniv in
              convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
 	if Int.equal j1 j2 && eq_ind ind1 ind2
 	then
-	  (let cuniv = convert_universes cuniv u1 u2 in
+	  (let cuniv = convert_instances false u1 u2 cuniv in
            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 	  
@@ -577,6 +550,80 @@ let clos_fconv trans cv_pb l2r evars env univs t1 t2 =
   let infos = create_clos_infos ~evars reds env in
   ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
+
+let check_eq univs u u' = 
+  if not (check_eq univs u u') then raise NotConvertible
+
+let check_leq univs u u' = 
+  if not (check_leq univs u u') then raise NotConvertible
+
+let check_sort_cmp_universes pb s0 s1 univs =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) when is_cumul pb ->
+      begin match c1, c2 with
+      | Null, _ | _, Pos -> () (* Prop <= Set *)
+      | _ -> raise NotConvertible
+      end
+    | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible
+    | (Prop c1, Type u) ->
+      let u0 = univ_of_sort s0 in
+	(match pb with
+	| CUMUL -> check_leq univs u0 u
+	| CONV -> check_eq univs u0 u)
+    | (Type u, Prop c) -> raise NotConvertible
+    | (Type u1, Type u2) -> 
+	(match pb with
+	| CUMUL -> check_leq univs u1 u2
+	| CONV -> check_eq univs u1 u2)
+
+let checked_sort_cmp_universes pb s0 s1 univs =
+  check_sort_cmp_universes pb s0 s1 univs; univs
+
+let check_convert_instances _flex u u' univs =
+  if Univ.Instance.check_eq univs u u' then univs
+  else raise NotConvertible
+
+let checked_universes =
+  { compare = checked_sort_cmp_universes;
+    compare_instances = check_convert_instances }
+
+let infer_eq (univs, cstrs as cuniv) u u' =
+  if Univ.check_eq univs u u' then cuniv
+  else
+    univs, (Univ.enforce_eq u u' cstrs)
+
+let infer_leq (univs, cstrs as cuniv) u u' =
+  if Univ.check_leq univs u u' then cuniv
+  else
+    let cstrs' = Univ.enforce_leq u u' cstrs in
+      univs, cstrs'
+
+let infer_cmp_universes pb s0 s1 univs =
+  match (s0,s1) with
+    | (Prop c1, Prop c2) when is_cumul pb ->
+      begin match c1, c2 with
+      | Null, _ | _, Pos -> univs (* Prop <= Set *)
+      | _ -> raise NotConvertible
+      end
+    | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible
+    | (Prop c1, Type u) ->
+      let u0 = univ_of_sort s0 in
+	(match pb with
+	| CUMUL -> infer_leq univs u0 u
+	| CONV -> infer_eq univs u0 u)
+    | (Type u, Prop c) -> raise NotConvertible
+    | (Type u1, Type u2) -> 
+	(match pb with
+	| CUMUL -> infer_leq univs u1 u2
+	| CONV -> infer_eq univs u1 u2)
+
+let infer_convert_instances flex u u' (univs,cstrs) =
+  (univs, Univ.enforce_eq_instances u u' cstrs)
+
+let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare = 
+  { compare = infer_cmp_universes;
+    compare_instances = infer_convert_instances }
+
 let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 =
   let b = 
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2 
@@ -584,7 +631,7 @@ let trans_fconv_universes reds cv_pb l2r evars env univs t1 t2 =
   in
     if b then ()
     else 
-      let _ = clos_fconv reds cv_pb l2r evars env (univs, None) t1 t2 in
+      let _ = clos_fconv reds cv_pb l2r evars env (univs, checked_universes) t1 t2 in
 	()
 
 (* Profiling *)
@@ -621,16 +668,21 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
     v1
     v2
 
+let generic_conv cv_pb l2r evars reds env univs t1 t2 =
+  let (s, _) = 
+    clos_fconv reds cv_pb l2r evars env univs t1 t2 
+  in s
+
 let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
-  let b, cstrs = 
-    if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 
+  let b, cstrs =
+    if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
     else Constr.eq_constr_univs_infer univs t1 t2
   in
-    if b then cstrs
-    else 
-      let (u, cstrs) = 
-	clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 
-      in Option.get cstrs
+    if b then (Univ.to_constraints univs cstrs)
+    else
+      let univs = ((univs, Univ.Constraint.empty), infered_universes) in
+      let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in
+	cstrs
 
 (* Profiling *)
 let infer_conv_universes = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index b9bd41f289..b45dca03e9 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -26,20 +26,29 @@ val nf_betaiota      : env -> constr -> constr
 exception NotConvertible
 exception NotConvertibleVect of int
 
-type conv_universes = Univ.universes * Univ.constraints option
-
 type 'a conversion_function = env -> 'a -> 'a -> unit
 type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function
 type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit
 type 'a trans_universe_conversion_function = 
   Names.transparent_state -> 'a universe_conversion_function
 
-type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
-
 type conv_pb = CONV | CUMUL
 
-val sort_cmp_universes :
-  conv_pb -> sorts -> sorts -> conv_universes -> conv_universes
+type 'a universe_compare = 
+  { (* Might raise NotConvertible *)
+    compare : conv_pb -> sorts -> sorts -> 'a -> 'a;
+    compare_instances: bool (* Instance of a flexible constant? *) -> 
+		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+  } 
+
+type 'a universe_state = 'a * 'a universe_compare
+
+type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b
+
+type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
+
+val check_sort_cmp_universes :
+  conv_pb -> sorts -> sorts -> Univ.universes -> unit
 
 (* val sort_cmp : *)
 (*     conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)
@@ -71,6 +80,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> types infer_conversion_function
 
+val generic_conv : conv_pb -> bool -> (existential->constr option) -> 
+  Names.transparent_state -> (constr,'a) generic_conversion_function
+
 (** option for conversion *)
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 46857ab275..1c60f2c3a1 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -401,6 +401,12 @@ module Level = struct
     | Prop -> true
     | _ -> false
 
+  let is_set x =
+    match data x with
+    | Set -> true
+    | _ -> false
+    
+
   (* A specialized comparison function: we compare the [int] part first.
      This way, most of the time, the [DirPath.t] part is not considered.
 
@@ -774,9 +780,10 @@ type canonical_arc =
     { univ: Level.t;
       lt: Level.t list;
       le: Level.t list;
-      rank : int}
+      rank : int;
+      predicative : bool}
 
-let terminal u = {univ=u; lt=[]; le=[]; rank=0}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false}
 
 module UMap :
 sig
@@ -1088,10 +1095,9 @@ let check_equal g u v =
   let _, arcv = safe_repr g v in
   arcu == arcv
 
-let set_arc g = 
-  snd (safe_repr g Level.set)
-  
-let prop_arc g = snd (safe_repr g Level.prop)
+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
@@ -1099,10 +1105,9 @@ let check_smaller g strict u v =
   if strict then
     is_lt g arcu arcv
   else
-    let proparc = prop_arc g in
-      arcu == proparc ||
-	((arcv != proparc && arcu == set_arc g) ||
-	    is_leq g arcu arcv)
+    is_prop_arc arcu 
+    || (is_set_arc arcu && arcv.predicative) 
+    || is_leq g arcu arcv
 
 (** Then, checks on universes *)
 
@@ -1166,12 +1171,20 @@ let check_leq =
 
 (** 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
-  enter_arc arcu' g, arcu'
+  let g = 
+    if is_set_arc arcu then set_predicative g arcv
+    else g
+  in
+    enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
 let setlt_if (g,arcu) v =
@@ -1184,8 +1197,12 @@ 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
-  enter_arc arcu' g, arcu'
-
+  let g = 
+    if is_set_arc arcu' then
+      set_predicative g arcv
+    else g
+  in
+    enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
 let setleq_if (g,arcu) v =
@@ -1321,7 +1338,7 @@ let is_initial_universes g = UMap.equal (==) g initial_universes
 
 let add_universe vlev g = 
   let v = terminal vlev in
-  let proparc = prop_arc g in
+  let proparc = get_prop_arc g in
     enter_arc {proparc with le=vlev::proparc.le}
       (enter_arc v g)
       
@@ -1433,8 +1450,6 @@ module UniverseConstraints = struct
   include S
   
   let add (l,d,r as cst) s = 
-    if (Option.is_empty (Universe.level r)) then 
-      prerr_endline "Algebraic universe on the right";
     if Universe.equal l r then s
     else add cst s
 
@@ -2028,6 +2043,7 @@ let normalize_universes g =
         lt = LSet.elements lt;
         le = LSet.elements le;
 	rank = rank;
+	predicative = false;
       }
   in
   UMap.mapi canonicalize g
@@ -2155,7 +2171,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} in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false} in
       UMap.add u (Canonical arc) accu
     else accu
   in
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 8e623415e7..0e91c79727 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -50,7 +50,7 @@ let rec conv_val pb k v1 v2 cu =
 
 and conv_whd pb k whd1 whd2 cu =
   match whd1, whd2 with
-  | Vsort s1, Vsort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu
+  | Vsort s1, Vsort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu
   | Vprod p1, Vprod p2 ->
       let cu = conv_val CONV k (dom p1) (dom p2) cu in
       conv_fun pb k (codom p1) (codom p2) cu
@@ -188,7 +188,7 @@ let rec conv_eq pb t1 t2 cu =
 	if Int.equal m1 m2 then cu else raise NotConvertible
     | Var id1, Var id2 ->
 	if Id.equal id1 id2 then cu else raise NotConvertible
-    | Sort s1, Sort s2 -> ignore(sort_cmp_universes pb s1 s2 (cu,None)); cu
+    | Sort s1, Sort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu
     | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu
     | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu
     | Prod (_,t1,c1), Prod (_,t2,c2) ->