| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | |_|/
|/| |
| | |
| | |
| | | |
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.
|
| | |/ / |
|
Maxime Dénès
Pierre-Marie Pédrot
SimonBoulier
Matthieu Sozeau
Gaëtan Gilbert
Emilio Jesus Gallego Arias
Assia Mahboubi
Hugo Herbelin