diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-10 15:05:21 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-02-11 22:28:39 +0100 |
| commit | 6c2d10b93b819f0735a43453c78566795de8ba5a (patch) | |
| tree | 14dffe59d0edfacf547b3912352f14420df047b8 /kernel/reduction.ml | |
| parent | 1ed0836a7e0c8e05b0288f85e344ef5249d5d228 (diff) | |
Use specialized function for inductive subtyping inference.
This ensures by construction that we never infer constraints outside
the variance model.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 083692e91..208a62ced 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -227,6 +227,10 @@ let get_cumulativity_constraints cv_pb cumi u u' = Univ.Variance.leq_constraints (Univ.ACumulativityInfo.variance cumi) u u' Univ.Constraint.empty +let inductive_cumulativity_arguments (mind,ind) = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> @@ -235,10 +239,7 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 | Declarations.Polymorphic_ind _ -> cmp_instances u1 u2 s | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in + let num_param_arity = inductive_cumulativity_arguments (mind,ind) in if not (Int.equal num_param_arity nargs) then cmp_instances u1 u2 s else @@ -249,6 +250,13 @@ let convert_inductives cv_pb ind nargs u1 u2 (s, check) = convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances cv_pb ind nargs u1 u2 s, check +let constructor_cumulativity_arguments (mind, ind, ctor) = + 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.(ctor - 1) + let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s = match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ -> @@ -257,13 +265,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u | Declarations.Polymorphic_ind _ -> cmp_instances u1 u2 s | Declarations.Cumulative_ind cumi -> - 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 + let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s else |