| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | |/
|/| |
|
| |\ \
| | |
| | |
| | | |
subtyping.
|
| | |/
|/|
| |
| |
| |
| | |
Not sure it could have led to a soundness bug, but this is definitely
serious enough to deserve a backport. Also made the code robust by
listing all the constructors.
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
kernel typing.
|
| | | | |
| | | |
| | | |
| | | | |
Upper layers are still not able to handle mutual records though.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This brings more compatibility with handling of mutual primitive records
in the kernel.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This is a first step towards the acceptance of mutual record types in the
kernel.
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
When inferring [u <= v+k] I replaced the exception and instead add
[u <= v]. This is trivially sound and it doesn't seem possible to have
the one without the other (except specially for [Set <= v+k] which was
already handled).
I don't know an example where this used to fail and now succeeds (the
point was to remove an anomaly, but the example
~~~
Module Type SG. Definition DG := Type. End SG.
Module MG : SG. Definition DG := Type : Type. Fail End MG.
~~~
now fails with universe inconsistency.
Fix #7695 (soundness bug!).
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
Not sure if worth using in other places.
|
| | |_|_|_|/
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
There's probably a proof of false using subtyping if someone wants to
look.
NB: the checker doesn't handle algebraics on the right.
|
| |\ \ \ \ \ |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
This eliminates 3 uses of Obj from TCB.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This was completely wrong, such a term could not even be type-checked by
the kernel as it was internally using a match construct over a negative
record. They were luckily only used in upper layers, namley printing
and extraction.
Recomputing the projection body might be costly in detyping, but this only
happens when the compatibility flag is turned on, which is not the default.
Such flag is probably bound to disappear anyways.
Extraction should be fixed though so as to define directly primitive
projections, similarly to what has been done in native compute.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This field was not used inside the kernel and not used in
performance-critical code where caching is essential, so we extrude
the code that computes it out of the kernel.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This reduces kernel bloat and removes code from the TCB, as compatibility
projections are now retypechecked as normal definitions would have been.
This should have no effect on efficiency as this only happens once at
definition time.
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We untangle the implementation in several ways.
- No higher-order self argument function as there is only one caller.
- Compute composition of lifts + substitution on terms using a dedicated
function instead of mk_clos followed by to_constr.
- Take more advantage of identity substitutions.
|
| |\ \ \ \ |
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | | | | | | | |
|
| |/ / / / / /
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The renaming is internal only. I believe the name reloc is legacy and
a bit confusing now that the structure contains a full compilation
environment.
|
| | |_|/ / /
|/| | | |
| | | | |
| | | | |
| | | | |
| | | | | |
There is no need to expand a primitive projection with the section
parameters and universes, for one good reason: they are never applied
neither to parameters nor universe instances.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is an easy improvement on examples like:
Fixpoint zero (n : nat) :=
match n with
| O => O
| S p => zero p + zero p
end.
Definition foo := if true then zero 100 else 0.
Eval native_compute in if true then 0 else foo.
I didn't add a test case, because our current testing infrastructure is too
fragile for that.
|
| | |_|_|/
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | | |
It was actually a hack since those names are never used to represent
values, only to be passed as arguments to bytecode instructions. So
instead of reusing the structured_constant type, we follow the same
pattern as switch annotations.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | | |
We store the universe context in the inlined terms and apply it to
the instance provided to the substitution function. Technically the
context is not needed, but we use it to assert that the length of the
instance corresponds, just in case.
|
| | | |
| | |
| | |
| | | |
And similarly for fixpoint and cofixpoint.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Instead of having a constant-based compilation of projections, we
generate them at the compilation time of the inductive block to which
they pertain.
|
| |/ / |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | | |
Dependency analysis for separate compilation was not iterated properly
on rel_context and named_context.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
kernel closures.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Values containing (retroknowledge-based) matchine integers were not
recognized as literals.
|
| | | |_|_|/ /
| |/| | | |
| | | | | |
| | | | | |
| | | | | | |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
| | | | | | | |
|
| |/ / / / /
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Due to a bad interaction between PRs, the `Names.global_reference`
alias was removed in 8.9, where it should disappear in 8.10.
The original PR #6156 deprecated the alias in `Libnames`.
|
| | |_|/ /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We eta-expand cofixpoints when needed, so that their call-by-need
evaluation is correctly implemented by VM and native_compute.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| | | | | |
|
Pierre-Marie Pédrot
Maxime Dénès
Gaëtan Gilbert
Matthieu Sozeau
whitequark
Emilio Jesus Gallego Arias
SimonBoulier