| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
This is a step towards cleanup of the `start` lemma path.
|
|
This module used to do retyping for the kernel in prototypes of SProp,
but was switched to only relevance inference before the merge.
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
This could have been at the root of strange behaviours (read unsoundness).
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
The call to is_anomaly actually destroyed the backtrace, because it would
call arbitrary code, in particular in Himsg which relied internally on
raising exceptions.
|
|
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: mattam82
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Instead of various termops and globnames aliases.
|
