| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
We can do this after the parent commit (Reductionops.nf_* don't use
empty env)
|
| |/ /
| |
| |
| |
| | |
- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction
|
| |/
|
|
|
|
|
|
|
|
|
|
|
| |
This heuristic is justified by the fact that during a conversion check
between a flexible and a rigid term, the flexible one is eventually going
to be fully weak-head normalized. So in this case instead of performing
many small reduction steps on the flexible term, we perform full weak-head
reduction, including delta.
It is slightly more efficient in actual developments, and it fixes a corner
case encountered by Jason Gross.
Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`.
|
| |\
| |
| |
| | |
records for cbv and native_compute
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We separate functions dealing with VM values (vmvalues.ml) and
interfaces of the bytecode interpreter (vm.ml). Only the former relies
on untyped constructions.
This also makes the VM architecture closer to the one of native_compute,
another patch could probably try to share more code between the two for
conversion and reification (not trivial, though).
This is also preliminary work for integers and arrays.
|
| |/
|
|
|
|
|
|
| |
The implementation of the subterm relation for primitive projections was
a bit wrong. I found the problem independently of this bug, and tried to
see if a proof of False could be derived, but I don't think so, due to
another check (check_is_subterm) that saves the kernel at the last
minute.
|
| |\
| |
| |
| | |
for primitive projections
|
| |\ \ |
|
| | |/
|/|
| |
| |
| |
| |
| | |
The constant_value function was actually not behaving the same as
constant_value_in w.r.t. projections. The former was not used, and
the only place that used the latter was in Tacred and was statically
insensitive to the use of projections.
|
| | |
| |
| |
| |
| | |
We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In practice, we only send to the kernel polymorphic definitions whose
side-effects have been exported first, and furthermore their bodies have
already been forced. Therefore, no constraints are generated by the kernel.
Nonetheless, it might be desirable in the future to also defer computation
of polymorphic proofs whose constraints have been explicited in the type.
It is not clear when this is going to be implemented. Nonetheless, the
current check is not too drastic as it only prevents monomorphic side-effects
to appear inside polymorphic opaque definitions. The only way I know of to
trigger such a situation is to generate a scheme in a proof, as even abstract
is actually preserving the polymorphism status of the surrounding proof. It
would be possible to work around such rare instances anyways.
As for internal constraints generated by a potentially deferred polymorphic
body, it is easy to check that they are a subset of the exported ones at a
higher level inside the future computation and fail there.
So in practice this patch is not too restrictive and it highlights a rather
strong invariant of the kernel code.
|
| |/ /
| |
| |
| | |
This exception was removed in
[on Oct 13, 2016](https://github.com/coq/coq/commit/57c6ffd23836364168ffd1c66dbddbecf830c7c6#diff-297bc4c11289c2c0ed18d5eebf817c47).
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
| | |
| |
| |
| |
| | |
This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
|
| | | |
|
| | | |
|
| |/
|
|
|
| |
We take advantage of the range structure to get a O(log n) retrieval of values
bound to a rel in an environment.
|
| |
|
|
|
|
|
|
| |
Unfortunately OCaml doesn't deprecate the constructors of a type when
the type alias is deprecated.
In this case it means that we don't get rid of the kernel dependency
unless we deprecate the constructors too.
|
| |\ |
|
| |\ \
| | |
| | |
| | | |
the kernel.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
We force the upper layers to extrude the universe constraints before sending
it to the kernel. This simplifies the suspicious handling of polymorphic
constraints for section-local definitions.
|
| | |/
| |
| |
| | |
This allows to statically ensure well-formedness properties.
|
| | |
| |
| | |
The comment had the type and value of the let-in swapped, which contradicted the listed types.
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Let definitions have the same behaviour if they are ended with a Qed or a
Defined command, i.e. they are treated as if they were transparent. Indeed,
it doesn't make sense for them to be opaque as they are going to be expanded
away at the end of the section.
For an unknown reason, handling of side-effects in Let definitions considers
them as if they were opaque, i.e. the effects are inlined in the definition.
This discrepancy has bad consequences in the kernel, where one is forced to
juggle with universe constraints generated by polymorphic Let definitions.
As a first phase of cleaning, we simply enforce by typing that Let definitions
should be purified before reaching the kernel.
This has the intended side-effect to make side-effects persistent in Let
definitions, as if they were indeed truly transparent.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We more the `recursivity_kind` type to `Declarations`, this indeed
makes sense, and now `Decl_kind` morally lives in `library` as it
should.
|
| |/ / / |
|
| |/ /
| |
| |
| |
| | |
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The patch has three parts:
- Introduction of a configure flag `-bytecode-compiler (yes|no)`
(due to static initialization this is a configure-time option)
- Installing the hooks that register the VM with the pretyper and the
kernel conditionally on the flag.
- Replacing the normalization function in `Redexpr` by compute if the
VM is disabled.
We also rename `Coq_config.no_native_compiler` to `native_compiler`
and `Flags.native_compiler` to `output_native_objects` [see #4607].
|
| |/
|
|
|
|
|
|
| |
They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
There don't really bring anything, we also correct some minor nits
with the printing function.
|
| |/
|
|
|
|
|
|
| |
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
| |\
| |
| |
| | |
constructs.
|
| | |
| |
| |
| |
| |
| | |
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
| | |
| |
| |
| |
| |
| |
| | |
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
|
| |/
|
|
|
|
| |
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
|
| |\ |
|
Maxime Dénès
Pierre-Marie Pédrot
Gaëtan Gilbert
Jasper Hugunin
Emilio Jesus Gallego Arias
Jasper Hugunin
Matthieu Sozeau