diff options
| author |  mlasson <marc.lasson@gmail.com> | 2015-06-22 21:14:20 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-07-09 11:41:55 +0200 |
| commit | 3a6b08286ac78c674d6d3e3073b38de26a610fdc (patch) | |
| tree | 112d68e4b412b9a096ba8e9fe62f0562fc43e5ac /kernel/indtypes.ml | |
| parent | 1bf30962d7cd5732393d7722ae6d263d4c812ec8 (diff) | |
Template polymorphism: A bug-fix for Bug #4258
Reviewed by M. Sozeau
This commit fixes template polymorphism and makes it more precise,
applying to non-linear uses of the same universe in parameters of
template-polymorphic inductives. See bug report and
https://github.com/coq/coq/pull/69 for full details.
I also removed some deadcode in checker/inductive.ml.
I do not know if it is also necessary to fix checker/indtypes.ml.
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 39 |
1 files changed, 11 insertions, 28 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6b909824b..e80a3a5a4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -175,36 +175,19 @@ let cumulate_arity_large_levels env sign = let is_impredicative env u = is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet) +(* Returns the list [x_1, ..., x_n] of levels contributing to template + polymorphism. The elements x_k is None if the k-th parameter (starting + from the most recent and ignoring let-definitions) is not contributing + or is Some u_k if its level is u_k and is contributing. *) let param_ccls params = - let has_some_univ u = function - | Some v when Univ.Level.equal u v -> true - | _ -> false + let fold acc = function (_, None, p) -> + (let c = strip_prod_assum p in + match kind_of_term c with + | Sort (Type u) -> Univ.Universe.level u + | _ -> None) :: acc + | _ -> acc in - let remove_some_univ u = function - | Some v when Univ.Level.equal u v -> None - | x -> x - in - let fold l (_, b, p) = match b with - | None -> - (* Parameter contributes to polymorphism only if explicit Type *) - let c = strip_prod_assum p in - (* Add Type levels to the ordered list of parameters contributing to *) - (* polymorphism unless there is aliasing (i.e. non distinct levels) *) - begin match kind_of_term c with - | Sort (Type u) -> - (match Univ.Universe.level u with - | Some u -> - if List.exists (has_some_univ u) l then - None :: List.map (remove_some_univ u) l - else - Some u :: l - | None -> None :: l) - | _ -> - None :: l - end - | _ -> l - in - List.fold_left fold [] params + List.fold_left fold [] params (* Type-check an inductive definition. Does not check positivity conditions. *) |