Optimization

Only try using cumulativity in conversion/subtyping if the universe
instances are non-empty

2 files changed, 54 insertions, 34 deletions

diff --git a/checker/reduction.ml b/checker/reduction.ml
index 5010920bc..95dc93f5d 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -431,23 +431,35 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
       if mind_equiv_infos infos ind1 ind2 then
-        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
-        let () =
-          convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
-            u2 (stack_args_size v2) univ
-        in
-        convert_stacks univ infos lft1 lft2 v1 v2
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          in
+          convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
       if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
-        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
-        let () =
-          convert_constructors
-            (mind, snd ind1, j1) u1 (stack_args_size v1)
-            u2 (stack_args_size v2) univ
-        in
-        convert_stacks univ infos lft1 lft2 v1 v2
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          begin
+            convert_universes univ u1 u2;
+            convert_stacks univ infos lft1 lft2 v1 v2
+          end
+        else
+          let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+          let () =
+            convert_constructors
+              (mind, snd ind1, j1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          in
+          convert_stacks univ infos lft1 lft2 v1 v2
       else raise NotConvertible
 
      (* Eta expansion of records *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8bf95e5de..a9e2ce78c 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 *)