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 | |
| 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')
| -rw-r--r-- | kernel/reduction.ml | 24 | ||||
| -rw-r--r-- | kernel/reduction.mli | 3 |
2 files changed, 16 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 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index d064b3687..0e6a2b819 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -50,6 +50,9 @@ type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constrai val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t +val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int +val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int + val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare |