| Age | Commit message (Collapse) | Author |
|---|
|
|
|
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
|
|
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
|
|
In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.
We move all the files in `intf` to the lowest place their dependencies
can accommodate:
- `Misctypes`: is used by Declaremod, thus it has to go in `library`
or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
could be fixed, as this module should be declared in `interp` which
is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.
Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
contains evars
|
|
|
|
This is more efficient in general, because Termops.dependent doesn't take
advantage of the knowledge of its pattern argument.
|
|
This mitigates bug #6860.
|
|
We ensure that all original names in a spine of matched nested binders
are distinct.
Note: This enforces that two binders with same internal names are kept
disjoint but this does not enforce that we shall respect names exactly
as they are printed. Only the original prefix of the internal names
are preserved, not their "0" or "1" etc. suffix.
|
|
|
|
|
|
We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]
Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.
Now, grepping for `~abort:false` should return the questionable
parts of the system.
Not a lot of places had to be fixed, some comments:
- problems with the interface due to `Evd/Constr` [`Evd.define` being
the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.
A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.
|
|
This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
|
|
|
|
|
|
|
|
|
|
|
|
- In a situation like "match x with ... end" with no "return" clause
we don't warn for the implicit "as x" coming from repeating "x"
- In a multiple fixpoint, we don't warn for the recursive context
being distributed several times over the different mutual
components.
|
|
|
|
Answering to commit about #5500: we don't know in general if the
return predicate T(y1,..,yn,x) in the intermediate step of a nested
pattern-matching is a sort, but we don't even know if it is
well-typed: retyping is not enough, we need full typing.
|
|
This is a quick fix to check in nested pattern-matching that the
return clause is typed by an arity (there was already a check when the
return clause was given explicitly - in the 3rd section of
prepare_predicate -; it was automatically typed by a sort when the
return clause was coming by pattern-matching with the type constraint,
since the type constraint is a type; but it was not done when the
predicate was derived from a former predicate in nested
pattern-matching).
Indeed, in nested pattern-matching, we know that the return predicate
has the form λy1..yn.λx:I(y1,..,yn).T(y1,..,yn,x) and we know that
T(v1,...,vn,u) : Type for the effective u:I(v1,..,vn) we are matching
on, but we don't know if T(y1,..,yn,x) is itself a sort (e.g. it can
be a "match" which reduces to a sort when instantiated with v1..vn,
but whose evaluation remains blocked when the y1..yn are variables).
Note that in the bug report, the incorrect typing is produced by small
inversion. In practice, we can raise the anomaly also without small
inversion, so we fix it in the general case. See file 5500.v for
details.
|
|
|
|
For instance, error in "Goal forall a f, f a = 0" is now located.
|
|
The `reference` type contains some ad-hoc locations in its
constructors, but there is no reason not to handle them with the
standard attribute container provided by `CAst.t`.
An orthogonal topic to this commit is whether the `reference` type
should contain a location or not at all.
It seems that many places would become a bit clearer by splitting
`reference` into non-located `reference` and `lreference`, however
some other places become messier so we maintain the current status-quo
for now.
|
|
We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:
- module declarations
- intro patterns
- top-level sentences
Now, parsed documents should be full annotated by `CAst` nodes.
|
|
|
|
|
|
|
|
When comparing 2 irrelevant universes [u] and [v] we add a "weak
constraint" [UWeak(u,v)] to the UState. Then at minimization time a
weak constraint between unrelated universes where one is flexible
causes them to be unified.
|
|
|
|
|
|
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
|
|
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)
See modified test for more details of what is now possible.
Technical notes:
When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.
When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
|
|
|
|
|
|
|
|
|
|
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
|
|
if we cannot coerce one constructor type to the other. By invariant
they have a common supertype
|
|
- Nothing to check in conversion as they have a common supertype
by typing.
- In inference, enforce that one is lower than the other.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
