| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
We seize the opportunity to simplify the code and hoist out computations
that can be avoided.
|
|
It was only used in Tacred, and with a type that forced to perform a
change of representation of stacks.
|
|
This highlights static invariants about the function.
|
|
|
|
|
|
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
Instead of costly linear reallocations, we share as much as possible of the
prefixes of the various environment subcomponents.
|
|
Fixes #12529
|
|
|
|
We factorize code between Cbn and Reductionops, and remove dead code as well.
|
|
|
|
This is a quick fix to avoid the anomaly, with a fallback on before
b1b8243b7fc.
|
|
eta-expansion of "match" branches
Reviewed-by: gares
Ack-by: ppedrot
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
At the same time, we propagate the correct binder relevance in detyping.
Note that this would be fixed by enforcing the context of branches in
the syntax of "Case".
|
|
This was useless, since we did not observe the difference on evars.
|
|
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
User time is unreliable for `native_compute`.
Also output time spent in conversion to native code, just in case that
is ever slow.
Note that this also removes spurious newlines in the output.
Fixes #11962
|
|
Reviewed-by: ppedrot
|
|
explicit applications
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
|
|
We inline the "with_evars := false" case.
|
|
The effects field of the UniqueProjection constructor was never accessed.
|
|
This makes some invariants explicit and is 1:1 equivalent.
|
|
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
While we're at it also compare instances in glob_constr although I
don't know if that changes any behaviour.
|
|
A quick analysis showed that most of the calls to whd do not lead to a
term which further triggers reduction, so there is no point in refolding
a potentiall huge term for no reason.
|
|
There is no point in using the exaggerately inefficient Reductionops machine.
We need to be call-by-name to preserve the shape of the reduced terms, as
call-by-need would introduce sharing and thus at-distance effects in term
refolding. Yet, the Reductionops machine is worse than that, since it performs
substitutions eagerly, leading to a catastrophical performance profile.
Instead, we use the kernel reduction in by-name mode to replace the Reductionops
machine in whd_betaiota_deltazeta_for_iota_state with all flags on. Since the
kernel is using explicit substitutions, this is algorithmically more efficient.
Apart from minor differences, this should produce the same normal form.
As showed by the benchmarks, this is a critical change for the odd-order proofs.
Ideally, we should use delayed substitutions in the Reductionops machine as well
for great profit, but due to code entanglement this is a much less self-contained
change.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
This makes code a bit more clear.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
|
|
- Removal of exported types and functions that were unused.
- Moving ad-hoc functions that were used once in the codebase to their call site.
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: gares
|
|
We use a more robust implementation that does not assume that the type
of the inductive is in ζ-normal form. This code path is not exercised,
because due to the kernel typing algorithm, let-bindings in the type
of a recursor are expanded away.
|
