From 256ca51bafc7200c8c006981cad60e57014e0dbc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 26 Feb 2017 21:14:52 +0100
Subject: Do not recompute twice the whnf of terms in conversion.

This performance bug was introduced 9 years ago in a8b0345, where the
responsibility of normalizing the term went from ccnv to eqappr in Reduction.
As a result, all recursive calls to eqappr that were preemptively reducing the
term ended up calling whd_stack twice, once by themselves, and once in the
subsequent call to eqappr.

This caused an important slowdown for conversion-intensive proofs, as the
whd_stack calls CClosure.zip to perfom in-place term sharing, leading to
useless huge re-allocations and repetitive write barriers.

Now that eqappr always head-normalizes the term beforehand, we simply don't
call whd_stack anymore when jumping to eqappr.
---
 kernel/reduction.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1ae89347ad..fc379fb7d8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -322,17 +322,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
          let (app1,app2) =
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
-             | Some def1 -> ((lft1, whd def1 v1), appr2)
+             | Some def1 -> ((lft1, (def1, v1)), appr2)
              | None ->
                (match unfold_reference infos fl2 with
-               | Some def2 -> (appr1, (lft2, whd def2 v2))
+               | Some def2 -> (appr1, (lft2, (def2, v2)))
 	       | None -> raise NotConvertible)
            else
 	     match unfold_reference infos fl2 with
-             | Some def2 -> (appr1, (lft2, whd def2 v2))
+             | Some def2 -> (appr1, (lft2, (def2, v2)))
              | None ->
                (match unfold_reference infos fl1 with
-               | Some def1 -> ((lft1, whd def1 v1), appr2)
+               | Some def1 -> ((lft1, (def1, v1)), appr2)
 	       | None -> raise NotConvertible) 
 	 in
            eqappr cv_pb l2r infos app1 app2 cuniv)
@@ -343,11 +343,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	 form *)
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) -> 
-	eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+	eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv
       | None ->
 	match unfold_projection infos p2 c2 with
 	| Some (def2,s2) ->
-	  eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+	  eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv
 	| None -> 
           if Constant.equal (Projection.constant p1) (Projection.constant p2)
 	     && compare_stack_shape v1 v2 then
@@ -359,26 +359,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FProj (p1,c1), t2) ->
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) ->
-         eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+         eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
 	     (match unfold_reference infos fl2 with
               | Some def2 ->
-		 eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+		 eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
     | (t1, FProj (p2,c2)) ->
       (match unfold_projection infos p2 c2 with
       | Some (def2,s2) -> 
-         eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+         eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->
 	     (match unfold_reference infos fl1 with
               | Some def1 ->
-		 eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+		 eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
@@ -424,7 +424,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FFlex fl1, c2)      ->
        (match unfold_reference infos fl1 with
 	| Some def1 ->
-	   eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+	   eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
 	| None -> 
 	   match c2 with
 	   | FConstruct ((ind2,j2),u2) ->
@@ -438,7 +438,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (c1, FFlex fl2)      ->
        (match unfold_reference infos fl2 with
         | Some def2 ->
-	   eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+	   eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
         | None -> 
 	   match c1 with
 	   | FConstruct ((ind1,j1),u1) ->
-- 
cgit v1.2.3


From ab86b9b3999f3860bdb69824f585b9cf461ff295 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 7 Apr 2017 12:44:12 +0200
Subject: Use inductive subtyping for conv/cumul

---
 kernel/reduction.ml | 139 +++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 94 insertions(+), 45 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b6786c045c..0d2399e025 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -191,6 +191,7 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    leq_inductives : flex:bool -> Univ.UInfoInd.t -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
@@ -207,6 +208,9 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
 
+let compare_leq_inductives ~flex uinfind u u' (s, check) =
+  (check.leq_inductives ~flex uinfind u u' s, check)
+
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
   match k1, k2 with
@@ -299,11 +303,11 @@ let unfold_projection infos p c =
   else None
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
-  eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+  eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Control.check_for_interrupt ();
   (* First head reduce both terms *)
   let whd = whd_stack (infos_with_reds infos betaiotazeta) in
@@ -328,13 +332,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	       sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
-	       then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	       then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if Evar.equal ev1 ev2 then
-          let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
-          convert_vect l2r infos el1 el2
+          let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in
+          convert_vect env l2r infos el1 el2
             (Array.map (mk_clos env1) args1)
             (Array.map (mk_clos env2) args2) cuniv
         else raise NotConvertible
@@ -342,14 +346,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 index known to be bound to no constant *)
     | (FRel n, FRel m) ->
         if Int.equal (reloc_rel n el1) (reloc_rel m el2)
-        then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+        then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
       (try
 	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
-	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	   convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = CClosure.oracle_of_infos infos in
@@ -369,7 +373,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
                | Some def1 -> ((lft1, (def1, v1)), appr2)
 	       | None -> raise NotConvertible) 
 	 in
-           eqappr cv_pb l2r infos app1 app2 cuniv)
+           eqappr env cv_pb l2r infos app1 app2 cuniv)
 
     | (FProj (p1,c1), FProj (p2, c2)) ->
       (* Projections: prefer unfolding to first-order unification,
@@ -377,42 +381,42 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	 form *)
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) -> 
-	eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv
+	eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
       | None ->
 	match unfold_projection infos p2 c2 with
 	| Some (def2,s2) ->
-	  eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv
+	  eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
 	| None -> 
           if Constant.equal (Projection.constant p1) (Projection.constant p2)
 	     && compare_stack_shape v1 v2 then
-	    let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
-	      convert_stacks l2r infos lft1 lft2 v1 v2 u1
+	    let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in
+	      convert_stacks env l2r infos lft1 lft2 v1 v2 u1
 	  else (* Two projections in WHNF: unfold *)
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) ->
-         eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv
+         eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
 	     (match unfold_reference infos fl2 with
               | Some def2 ->
-		 eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+		 eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
     | (t1, FProj (p2,c2)) ->
       (match unfold_projection infos p2 c2 with
       | Some (def2,s2) -> 
-         eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv
+         eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->
 	     (match unfold_reference infos fl1 with
               | Some def1 ->
-		 eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+		 eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
@@ -424,15 +428,15 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
-        let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
-        ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+        let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in
+        ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
 	(* Luo's system *)
-        let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
-        ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+        let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in
+        ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
 
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
@@ -442,7 +446,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           anomaly (Pp.str "conversion was given unreduced term (FLambda).")
         in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
-	eqappr CONV l2r infos
+	eqappr env CONV l2r infos
 	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
     | (_, FLambda _) ->
         let () = match v2 with
@@ -451,34 +455,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
 	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
-	eqappr CONV l2r infos
+	eqappr env CONV l2r infos
 	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
 	
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
        (match unfold_reference infos fl1 with
 	| Some def1 ->
-	   eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
+	   eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
 	| None -> 
 	   match c2 with
 	   | FConstruct ((ind2,j2),u2) ->
 	      (try
 	      let v2, v1 =
 		eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
-	      in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	      in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
 	      with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
     | (c1, FFlex fl2)      ->
        (match unfold_reference infos fl2 with
         | Some def2 ->
-	   eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
+	   eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
         | None -> 
 	   match c1 with
 	   | FConstruct ((ind1,j1),u1) ->
  	      (try let v1, v2 =
 	     	     eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-	     	   in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	     	   in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
 	       with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
@@ -487,15 +491,33 @@ 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_instances ~flex:false u1 u2 cuniv in
-             convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
+        begin
+          let mind = Environ.lookup_mind (fst ind1) env in
+          if mind.Declarations.mind_polymorphic then
+          begin
+            let num_param_arity =
+              Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
+            in
+            (if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
+               raise NotConvertible else ());
+            let uinfind = mind.Declarations.mind_universes in
+	    let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+            let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
+            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          end
+          else
+          begin
+            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          end
+        end
         else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
 	if Int.equal j1 j2 && eq_ind ind1 ind2
 	then
 	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
+           convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv)
         else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -503,14 +525,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (try
     	 let v1, v2 =
     	   eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-    	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+    	 in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,j2),u2)) ->
       (try
     	 let v2, v1 =
     	   eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
-    	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+    	 in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
@@ -521,11 +543,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-	  let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+	  let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
-            convert_vect l2r infos
+            convert_vect env l2r infos
 	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -536,11 +558,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-          let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+          let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
-	    convert_vect l2r infos
+	    convert_vect env l2r infos
 	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
@@ -551,13 +573,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      (* In all other cases, terms are not convertible *)
      | _ -> raise NotConvertible
 
-and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
-    (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
+    (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv)
     (eq_ind)
     lft1 stk1 lft2 stk2 cuniv
 
-and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
+and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
   let lv2 = Array.length v2 in
   if Int.equal lv1 lv2
@@ -565,7 +587,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
     let rec fold n cuniv =
       if n >= lv1 then cuniv
       else
-        let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
+        let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
         fold (n+1) cuniv in
     fold 0 cuniv
   else raise NotConvertible
@@ -573,7 +595,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
-  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+  ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
 
 let check_eq univs u u' = 
@@ -610,9 +632,24 @@ let check_convert_instances ~flex u u' univs =
   if UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
+let check_leq_inductives ~flex uinfind u u' univs =
+  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
+  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    begin
+     let comp_subst = (Univ.Instance.append u u') in
+     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
+     if UGraph.check_constraints comp_cst univs then univs
+     else raise NotConvertible
+    end
+
 let checked_universes =
   { compare = checked_sort_cmp_universes;
-    compare_instances = check_convert_instances }
+    compare_instances = check_convert_instances;
+    leq_inductives = check_leq_inductives }
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -649,9 +686,21 @@ let infer_cmp_universes env pb s0 s1 univs =
 let infer_convert_instances ~flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
 
+let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) =
+  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
+  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+     let comp_subst = (Univ.Instance.append u u') in
+     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
+     (univs, Univ.Constraint.union cstrs comp_cst)
+
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
-    compare_instances = infer_convert_instances }
+    compare_instances = infer_convert_instances;
+    leq_inductives = infer_leq_inductives }
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
-- 
cgit v1.2.3


From 0d884e0852ae388becc5b74c6a8cb30088f7b79b Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sat, 8 Apr 2017 16:10:19 +0200
Subject: Fix cum/conv for inductive types

Fall back to the equating levels in case inductive is not fully applied
instead of failing.
---
 kernel/reduction.ml | 24 ++++++++++++++----------
 1 file changed, 14 insertions(+), 10 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0d2399e025..c8fad60ebe 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -492,24 +492,28 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         if eq_ind ind1 ind2
 	then
         begin
+          let fall_back () =
+            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          in
           let mind = Environ.lookup_mind (fst ind1) env in
           if mind.Declarations.mind_polymorphic then
           begin
             let num_param_arity =
               Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
             in
-            (if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
-               raise NotConvertible else ());
-            let uinfind = mind.Declarations.mind_universes in
-	    let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-            let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+            if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
+              fall_back ()
+            else
+            begin
+              let uinfind = mind.Declarations.mind_universes in
+              let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+              let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
+              convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+            end
           end
           else
-          begin
-            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-          end
+            fall_back ()
         end
         else raise NotConvertible
 
-- 
cgit v1.2.3


From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sun, 21 May 2017 14:46:30 +0200
Subject: Squashed commit of the following:

Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.

This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!

commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon Apr 24 17:14:21 2017 +0200

    Revert STL to monomorphic

commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon Apr 24 17:02:42 2017 +0200

    Try unifying universes before apply subtyping

commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany <amintimany@gmail.com>
Date:   Sun Apr 23 13:49:04 2017 +0200

    Compile more of STL with universe polymorphism

commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany <amintimany@gmail.com>
Date:   Tue Apr 18 21:26:45 2017 +0200

    Made more progress on compiling the standard library

commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany <amintimany@gmail.com>
Date:   Sun Apr 16 22:55:19 2017 +0200

    Make more number theoretic modules monomorphic

commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany <amintimany@gmail.com>
Date:   Fri Apr 14 16:11:48 2017 +0200

    WIP more of standard library compiles

    Also: Matthieu fixed a bug in rewrite system which was faulty when
    introducing new morphisms (Add Morphism) command.

commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany <amintimany@gmail.com>
Date:   Fri Apr 14 11:39:21 2017 +0200

    WIP: more of the standard library compiles

    We have implemented convertibility of constructors up-to mutual
    subtyping of their corresponding inductive types. This is similar to
    the behavior of template polymorphism.

commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany <amintimany@gmail.com>
Date:   Wed Apr 12 19:02:39 2017 +0200

    WIP: trying to get the standard library compile with universe polymorphism

    We are trying to prune universes after section ends. Sections add a
    load of universes that are not appearing in the body, type or the
    constraints.
---
 kernel/reduction.ml | 70 +++++++++++++++++++++++++++++++++++++----------------
 1 file changed, 49 insertions(+), 21 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c8fad60ebe..a872a103a5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -489,8 +489,8 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if eq_ind ind1 ind2
-	then
+      if eq_ind ind1 ind2
+      then
         begin
           let fall_back () =
             let cuniv = convert_instances ~flex:false u1 u2 cuniv in
@@ -498,31 +498,54 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           in
           let mind = Environ.lookup_mind (fst ind1) env in
           if mind.Declarations.mind_polymorphic then
-          begin
-            let num_param_arity =
-              Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
-            in
-            if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
-              fall_back ()
-            else
             begin
-              let uinfind = mind.Declarations.mind_universes in
-              let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-              let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
-              convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+              let num_param_arity =
+                Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
+              in
+              if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
+                fall_back ()
+              else
+                begin
+                  let uinfind = mind.Declarations.mind_universes in
+                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+                  let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
+                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+                end
             end
-          end
           else
             fall_back ()
         end
-        else raise NotConvertible
+      else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	if Int.equal j1 j2 && eq_ind ind1 ind2
-	then
-	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-           convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv)
-        else raise NotConvertible
+      if Int.equal j1 j2 && eq_ind ind1 ind2
+      then
+        begin
+          let fall_back () =
+            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+          in
+          let mind = Environ.lookup_mind (fst ind1) env in
+          if mind.Declarations.mind_polymorphic then
+            begin
+              let num_cnstr_args =
+                let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in
+                nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1)
+              in
+              if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then
+                fall_back ()
+              else
+                begin (* we don't consider subtyping for constructors. *)
+                  let uinfind = mind.Declarations.mind_universes in
+                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
+                  let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in
+                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+                end
+            end
+          else
+            fall_back ()
+        end
+      else raise NotConvertible
 	  
     (* Eta expansion of records *)
     | (FConstruct ((ind1,j1),u1), _) ->
@@ -688,7 +711,12 @@ let infer_cmp_universes env pb s0 s1 univs =
         else univs
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
-  (univs, Univ.enforce_eq_instances u u' cstrs)
+  let cstrs' =
+    if flex then 
+      if UGraph.check_eq_instances univs u u' then cstrs
+      else raise NotConvertible
+    else Univ.enforce_eq_instances u u' cstrs
+  in (univs, cstrs')
 
 let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-- 
cgit v1.2.3


From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Wed, 26 Apr 2017 15:24:35 +0200
Subject: Fix bugs

---
 kernel/reduction.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a872a103a5..33dd53a5b1 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -500,7 +500,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           if mind.Declarations.mind_polymorphic then
             begin
               let num_param_arity =
-                Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt)
+                mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs
               in
               if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
                 fall_back ()
@@ -535,7 +535,7 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
               if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then
                 fall_back ()
               else
-                begin (* we don't consider subtyping for constructors. *)
+                begin (* we consider subtyping for constructors. *)
                   let uinfind = mind.Declarations.mind_universes in
                   let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
                   let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in
-- 
cgit v1.2.3


From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 27 Apr 2017 20:16:35 +0200
Subject: Fix bugs and add an option for cumulativity

---
 kernel/reduction.ml | 190 +++++++++++++++++++++++++++++++++-------------------
 1 file changed, 121 insertions(+), 69 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 33dd53a5b1..ea583fdac8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -191,7 +191,10 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
-    leq_inductives : flex:bool -> Univ.UInfoInd.t -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
+      Univ.Instance.t -> int -> 'a -> 'a;
+    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
+      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
@@ -207,9 +210,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
+  
+let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
+  (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
 
-let compare_leq_inductives ~flex uinfind u u' (s, check) =
-  (check.leq_inductives ~flex uinfind u u' s, check)
+let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
+  (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -487,64 +493,31 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   | _ -> raise NotConvertible)
        
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
-
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-      if eq_ind ind1 ind2
-      then
-        begin
-          let fall_back () =
-            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-          in
-          let mind = Environ.lookup_mind (fst ind1) env in
-          if mind.Declarations.mind_polymorphic then
-            begin
-              let num_param_arity =
-                mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs
-              in
-              if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then
-                fall_back ()
-              else
-                begin
-                  let uinfind = mind.Declarations.mind_universes in
-                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-                  let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in
-                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-                end
-            end
+      if eq_ind ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) env in
+        let cuniv =
+          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+            convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
+              u2 (CClosure.stack_args_size v2) cuniv
           else
-            fall_back ()
-        end
+            convert_instances ~flex:false u1 u2 cuniv
+        in
+        convert_stacks env 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
-        begin
-          let fall_back () =
-            let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-            convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-          in
-          let mind = Environ.lookup_mind (fst ind1) env in
-          if mind.Declarations.mind_polymorphic then
-            begin
-              let num_cnstr_args =
-                let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in
-                nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1)
-              in
-              if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then
-                fall_back ()
-              else
-                begin (* we consider subtyping for constructors. *)
-                  let uinfind = mind.Declarations.mind_universes in
-                  let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in
-                  let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in
-                  convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
-                end
-            end
+      if Int.equal j1 j2 && eq_ind ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) env in
+        let cuniv =
+          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+            convert_constructors
+              (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
+              u2 (CClosure.stack_args_size v2) cuniv
           else
-            fall_back ()
-        end
+            convert_instances ~flex:false u1 u2 cuniv
+        in
+        convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
@@ -659,24 +632,79 @@ let check_convert_instances ~flex u u' univs =
   if UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
-let check_leq_inductives ~flex uinfind u u' univs =
+(* general conversion and inference functions *)
+let infer_check_conv_inductives
+    infer_check_convert_instances
+    infer_check_inductive_instances
+    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+  if mind.Declarations.mind_polymorphic then
+    let num_param_arity =
+      mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      infer_check_convert_instances ~flex:false u1 u2 univs
+    else
+      let uinfind = mind.Declarations.mind_universes in
+      infer_check_inductive_instances cv_pb uinfind u1 u2 univs
+  else infer_check_convert_instances ~flex:false u1 u2 univs
+
+let infer_check_conv_constructors
+    infer_check_convert_instances
+    infer_check_inductive_instances
+    (mind, ind, cns) u1 sv1 u2 sv2 univs =
+  if mind.Declarations.mind_polymorphic then
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+    in
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      infer_check_convert_instances ~flex:false u1 u2 univs
+    else
+      let uinfind = mind.Declarations.mind_universes in
+      infer_check_inductive_instances CONV uinfind u1 u2 univs
+  else infer_check_convert_instances ~flex:false u1 u2 univs
+
+let check_inductive_instances cv_pb uinfind u u' univs =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
   let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
-    begin
-     let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
-     if UGraph.check_constraints comp_cst univs then univs
-     else raise NotConvertible
-    end
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    if (UGraph.check_constraints comp_cst univs) then univs
+    else raise NotConvertible
+
+let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+  infer_check_conv_inductives
+    check_convert_instances
+    check_inductive_instances
+    cv_pb ind u1 sv1 u2 sv2 univs
+
+let check_conv_constructors cns u1 sv1 u2 sv2 univs =
+  infer_check_conv_constructors
+    check_convert_instances
+    check_inductive_instances
+    cns u1 sv1 u2 sv2 univs
 
 let checked_universes =
   { compare = checked_sort_cmp_universes;
     compare_instances = check_convert_instances;
-    leq_inductives = check_leq_inductives }
+    conv_inductives = check_conv_inductives;
+    conv_constructors = check_conv_constructors}
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -718,21 +746,45 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) =
+let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) =
   let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
   let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
-     let comp_subst = (Univ.Instance.append u u') in
-     let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in
-     (univs, Univ.Constraint.union cstrs comp_cst)
-
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV -> 
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    (univs, Univ.Constraint.union cstrs comp_cst)
+
+
+let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+  infer_check_conv_inductives
+    infer_convert_instances
+    infer_inductive_instances
+    cv_pb ind u1 sv1 u2 sv2 univs
+
+let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
+  infer_check_conv_constructors
+    infer_convert_instances
+    infer_inductive_instances
+    cns u1 sv1 u2 sv2 univs
+    
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances;
-    leq_inductives = infer_leq_inductives }
+    conv_inductives = infer_conv_inductives;
+    conv_constructors = infer_conv_constructors}
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 kernel/reduction.ml | 67 ++++++++++++++++++++++++++++++++---------------------
 1 file changed, 41 insertions(+), 26 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ea583fdac8..8bf95e5de9 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -497,11 +497,12 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       if eq_ind ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) env in
         let cuniv =
-          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            convert_instances ~flex:false u1 u2 cuniv
+          | Declarations.Cumulative_ind cumi ->
             convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
               u2 (CClosure.stack_args_size v2) cuniv
-          else
-            convert_instances ~flex:false u1 u2 cuniv
         in
         convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
@@ -510,12 +511,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       if Int.equal j1 j2 && eq_ind ind1 ind2 then
         let mind = Environ.lookup_mind (fst ind1) env in
         let cuniv =
-          if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+          match mind.Declarations.mind_universes with
+          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+            convert_instances ~flex:false u1 u2 cuniv
+          | Declarations.Cumulative_ind _ ->
             convert_constructors
               (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
               u2 (CClosure.stack_args_size v2) cuniv
-          else
-            convert_instances ~flex:false u1 u2 cuniv
         in
         convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
@@ -637,22 +639,26 @@ let infer_check_conv_inductives
     infer_check_convert_instances
     infer_check_inductive_instances
     cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
-  if mind.Declarations.mind_polymorphic then
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+    infer_check_convert_instances ~flex:false u1 u2 univs
+  | Declarations.Cumulative_ind cumi ->
     let num_param_arity =
       mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
     in
     if not (num_param_arity = sv1 && num_param_arity = sv2) then
       infer_check_convert_instances ~flex:false u1 u2 univs
     else
-      let uinfind = mind.Declarations.mind_universes in
-      infer_check_inductive_instances cv_pb uinfind u1 u2 univs
-  else infer_check_convert_instances ~flex:false u1 u2 univs
+      infer_check_inductive_instances cv_pb cumi u1 u2 univs
 
 let infer_check_conv_constructors
     infer_check_convert_instances
     infer_check_inductive_instances
     (mind, ind, cns) u1 sv1 u2 sv2 univs =
-  if mind.Declarations.mind_polymorphic then
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+    infer_check_convert_instances ~flex:false u1 u2 univs
+  | Declarations.Cumulative_ind cumi ->
     let num_cnstr_args =
       let nparamsctxt =
         mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
@@ -662,26 +668,30 @@ let infer_check_conv_constructors
     if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
       infer_check_convert_instances ~flex:false u1 u2 univs
     else
-      let uinfind = mind.Declarations.mind_universes in
-      infer_check_inductive_instances CONV uinfind u1 u2 univs
-  else infer_check_convert_instances ~flex:false u1 u2 univs
+      infer_check_inductive_instances CONV cumi u1 u2 univs
 
-let check_inductive_instances cv_pb uinfind u u' univs =
-  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+let check_inductive_instances cv_pb cumi u u' univs =
+  let ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) 
+  in
+  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.subst_instance_constraints comp_subst ind_sbcst
+      Univ.UContext.constraints
+        (Univ.subst_instance_context comp_subst ind_subtypctx)
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
-        let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        let comp_cst' = 
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints 
+            (Univ.subst_instance_context comp_subst ind_subtypctx) 
+        in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
@@ -746,22 +756,27 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
     else Univ.enforce_eq_instances u u' cstrs
   in (univs, cstrs')
 
-let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) =
-  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
-  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
+  let ind_instance = 
+    Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) 
+  in
+  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
   if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
           (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-      Univ.subst_instance_constraints comp_subst ind_sbcst
+      Univ.UContext.constraints
+        (Univ.subst_instance_context comp_subst ind_subtypctx)
     in
     let comp_cst =
       match cv_pb with
         CONV -> 
-        let comp_subst = (Univ.Instance.append u' u) in
-        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        let comp_cst' = 
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints
+            (Univ.subst_instance_context comp_subst ind_subtypctx) in
         Univ.Constraint.union comp_cst comp_cst'
       | CUMUL -> comp_cst
     in
-- 
cgit v1.2.3


From ab0c49baa8d57ed92a79e7d0b0737267042210f8 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 17:46:16 +0200
Subject: Optimization

Only try using cumulativity in conversion/subtyping if the universe
instances are non-empty
---
 kernel/reduction.ml | 50 +++++++++++++++++++++++++++++---------------------
 1 file changed, 29 insertions(+), 21 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8bf95e5de9..a9e2ce78c7 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -495,31 +495,39 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
       if eq_ind ind1 ind2 then
-        let mind = Environ.lookup_mind (fst ind1) env in
-        let cuniv =
-          match mind.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-            convert_instances ~flex:false u1 u2 cuniv
-          | Declarations.Cumulative_ind cumi ->
-            convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
-              u2 (CClosure.stack_args_size v2) cuniv
-        in
-        convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        else
+          let mind = Environ.lookup_mind (fst ind1) env in
+          let cuniv =
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              convert_instances ~flex:false u1 u2 cuniv
+            | Declarations.Cumulative_ind cumi ->
+              convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
+                u2 (CClosure.stack_args_size v2) cuniv
+          in
+          convert_stacks env 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 mind = Environ.lookup_mind (fst ind1) env in
-        let cuniv =
-          match mind.Declarations.mind_universes with
-          | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
-            convert_instances ~flex:false u1 u2 cuniv
-          | Declarations.Cumulative_ind _ ->
-            convert_constructors
-              (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
-              u2 (CClosure.stack_args_size v2) cuniv
-        in
-        convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        else
+          let mind = Environ.lookup_mind (fst ind1) env in
+          let cuniv =
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              convert_instances ~flex:false u1 u2 cuniv
+            | Declarations.Cumulative_ind _ ->
+              convert_constructors
+                (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
+                u2 (CClosure.stack_args_size v2) cuniv
+          in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
-- 
cgit v1.2.3


From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 kernel/reduction.ml | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index a9e2ce78c7..605e9f314c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -679,12 +679,13 @@ let infer_check_conv_constructors
       infer_check_inductive_instances CONV cumi u1 u2 univs
 
 let check_inductive_instances cv_pb cumi u u' univs =
-  let ind_instance = 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) 
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
   in
   let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
      anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
@@ -765,13 +766,14 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
   in (univs, cstrs')
 
 let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
-  let ind_instance = 
-    Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi) 
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
   in
   let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
-  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
-          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
-     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
+    anomaly (Pp.str "Invalid inductive subtyping encountered!")
   else
     let comp_cst =
       let comp_subst = (Univ.Instance.append u u') in
-- 
cgit v1.2.3