| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
|/| |
|
| |/
|
|
| |
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.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | | |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | | |
|
| | | | | |
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \
| |_|_|_|/ /
|/| | | | | |
|
| | | | | | | |
|
| |\ \ \ \ \ \
| |_|/ / / /
|/| | | | | |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| | | | | |_|/
| | | |/| |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We simply treat them as as an application of an atom to its instance,
and in the decompilation phase we reconstruct the instance from the stack.
This grants wish BZ#5659.
|
| | | | | |/
| | | |/|
| | | | |
| | | | | |
Following up on #6791, we remove the option "Tactic Pattern Unification"
|
| | | | | | |
|
| | | |/ / |
|
| | |/ /
|/| |
| | |
| | |
| | | |
This simplifies the representation of values, and brings it closer to
the ones of the native compiler.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This commit was motivated by true spurious conversions arising in my
`to_constr` debug branch.
The changes here need careful review as the tradeoffs are subtle and
still a lot of clean up remains to be done in `vernac/*`.
We have opted for penalize [minimally] the few users coming from true
`Constr`-land, but I am sure we can tweak code in a much better way.
In particular, it is not clear if internalization should take an
`evar_map` even in the cases where it is not triggered, see the
changes under `plugins` for a good example.
Also, the new return type of `Pretyping.understand` should undergo
careful review.
We don't touch `Impargs` as it is not clear how to proceed, however,
the current type of `compute_implicits_gen` looks very suspicious as
it is called often with free evars.
Some TODOs are:
- impargs was calling whd_all, the Econstr equivalent can be either
+ Reductionops.whd_all [which does refolding and no sharing]
+ Reductionops.clos_whd_flags with all as a flag.
|
| | | |
|
Gaëtan Gilbert
Pierre-Marie Pédrot
Maxime Dénès
Emilio Jesus Gallego Arias
Hugo Herbelin
Matthieu Sozeau
mrmr1993
Enrico Tassi
Théo Zimmermann