| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
information.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| | |_|_|_|_|/
|/| | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This bug was present since the first patch adding universe polymorphism
handling in the VM (Coq 8.5). Note that unsoundness can probably be
observed even without universe polymorphism.
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
This ensures by construction that we never infer constraints outside
the variance model.
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
The part in Reduction should be semantics preserving, but Reductionops
only tried cumulativity if equality fails. This is probably wrong so I
changed it.
|
| | |_|/ / /
|/| | | | |
|
| | | | |/
| | |/| |
|
| | |/ /
|/| |
| | |
| | |
| | | |
Instead, we properly register a printer for such exception and update
the code.
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
|
| | | | | | |
|
| | | | | | |
|
| | |_|/ /
|/| | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This definitely qualifies as a micro-optimization, but it would not be
performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml
semantics, as it involves a fixpoint and changes potential non-termination.
In our case it doesn't matter semantically, but it is indeed observable
on computation intensive developments like UniMath.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| |\ \ |
|
Maxime Dénès
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Jasper Hugunin
Jasper Hugunin