| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
For some reason the code was returning int option when only the value of
the integer was relevant.
|
|
Simplify the newring hack
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The new implementation is 100% compatible with the previous one, but it
is more compact and does not use a tricky translation function from the
kernel.
|
|
|
|
|
|
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 know that when a fterm is marked as Whnf or Norm, the only thing that can
happen in the reduction machine is administrative reduction pushing the
destructured term on the stack. Thus there is no need to perform any
actual performative reduction.
Furthermore, every head subterm of those terms are recursively Whnf or Norm,
which implies that no update mark is pushed on the stack during the
destructuration. So there is no need to unzip the stack to unset FLOCKED
nodes as well.
|
|
The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers
to C-allocated strings standing for VM bytecode. If the the no-naked-pointers
option is set, we perform the check that a stack value lives on the OCaml heap
ourselves.
|
|
We allocate an additional header so that the accumulator is not a naked
pointer. Indeed, it is contained in accumulator blocks which are scanned by
the GC as their tags is 0.
|
|
This prevents the existence of a few naked pointers to C heap from the OCaml
heap. VM bytecode is represented as any block of size at least 1 whose first
field points to a C-allocated string.
This representation is compatible with the Coq VM representation of
(potentially recursive) closures, which are already specifically tailored
in the OCaml GC to be able to contain out-of-heap data.
|
|
|
|
|
|
This removes the Flags.univ_print in the kernel, making it possible to
put the univ printing flag ownership back in Detyping.
The lazyness is because getting an explanation may be costly and we
may discard it without printing.
See benches
- with lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/406/console
- without lazy
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/405/console
Notably without lazy mathcomp odd_order is +1.26% with some lines
showing significant changes, eg PFsection11 line 874 goes from 11.76s
to 13.23s (+12%).
(with lazy the same development has -1% overall and the same line goes
from 11.76s to 11.23s (-4%) which may be within noise range)
|
|
|
|
ie don't go through having Eq constraints but directly to the unionfind.
|
|
|
|
|
|
We also make the code of [compact] in kernel/univ.ml a bit clearer.
|
|
Recent commits introduced global flags, but these should be
module-specific so relocating.
Global flags are deprecated, and for 8.9 `Lib.Flags` will be reduced
to the truly global stuff.
|
|
|
|
|
|
The previous code was mimicking what the C implementation was doing, which
was a quadratic algorithm. We simply use the good old exponential reallocation
strategy that is amortized O(1).
|
|
|
|
|
|
We expected `nparams + nrealargs + consnrealargs` but the `nrealargs`
should not be there. This breaks cumulativity of constructors for any
inductive with indices (so records still work, explaining why the test
case in #6747 works).
|
|
|
|
|
|
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
|
|
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.
|
|
|
|
|
|
We limit fixpoints to Finite inductive types, so that BiFinite
inductives (non-recursive records) are excluded from fixpoint
construction. This is a regression in the sense that e.g. fixpoints
on unit records were allowed before. Primitive records with
eta-conversion are included in the BiFinite types.
Fix deprecation
Fix error message, the inductive type needs to be recursive for fix to work
|
