| Age | Commit message (Collapse) | Author |
|---|
|
constraints.
|
|
We defer the computation of the universe quantification to the upper layer,
outside of the kernel.
|
|
Instead of using a linear representation, we simply use a table that maps
every kind of relocation to the list of positions it needs to be applied to.
|
|
The previous implementation used a list of pairs, which has size 9n where n
is the number of relocations. We instead use two arrays for a total memory
cost of 2n + 5 words.
The use of arrays may turn out to be problematic on 32-bit machines, I am unsure
if we will hit this limitation in practice.
|
|
Instead we thread a buffer.
|
|
This is actually not needed, as the only thing we do with this Bytes.t is to
pass it to a C function which will use it in a read-only way.
|
|
This shouldn't matter because the tcode_of_code function is pure, its only
effect being allocating a string and filling it with the translated bytecode.
|
|
This reduces the possibility to wreak havoc while making the API nicer.
|
|
|
|
|
|
|
|
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.
|
