| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
| |
|
|
|
|
| |
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.
|
| |/ |
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| |
|
|
| |
These are also convenient from `vernac` [to be used in future PRs].
|
| |
|
|
|
|
|
|
| |
We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.
Thanks to @SkySkimmer for lots of comments and bug-finding.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
|
| |
In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.
Universes of a monomorphic reference [c] are considered to appear in
the term [c].
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.
E.g mono@{i} := Type@{i} is printed as
mono@{mono.i} := Type@{mono.i}.
There can be a name clash if there's a module and a constant of the
same name. It is detected and is an error if the constant is first
but is not detected and the name for the constant not
registered (??) if the constant comes second.
Accept VarRef when registering universe binders
Fix two problems found by Gaëtan where binders were not registered properly
Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs
Fix an issue of the stronger restrict universe context + no evd leak
This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
|
| |
|
|
| |
We do up to `Term` which is the main bulk of the changes.
|
| |
|
|
| |
This will allow to merge back `Names` with `API.Names`
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
| |\
| |
| |
| | |
short econstr-cleaning of record.ml
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
| |
|
|
|
| |
For now we only normalize sorts, and we leave instances for the next
commit.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This removes code duplication between Evarutil and EConstr.
|
| |
|
|
|
|
| |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| |
|
|
|
|
| |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.
Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
|
| |
|
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Maxime Dénès
Théo Zimmermann
Cyprien Mangin
Matthieu Sozeau
Hugo Herbelin
Gaetan Gilbert
Enrico Tassi