diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 17:46:16 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | ab0c49baa8d57ed92a79e7d0b0737267042210f8 (patch) | |
| tree | 062d6d08f7b75cd2ea1abe10469265b882776a7e /checker/reduction.ml | |
| parent | 49e4acab949da9861adcd37b8511a89c221ae129 (diff) | |
Optimization
Only try using cumulativity in conversion/subtyping if the universe
instances are non-empty
Diffstat (limited to 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 38 |
1 files changed, 25 insertions, 13 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 *) |