| Age | Commit message (Collapse) | Author |
|---|
|
No need to store the case_info, all the data is reconstructible from the
context. Furthermore, this reconstruction is performed in a context where
we already access the environment, so performance is not at stake.
Hopefully this will also reduce the number of globally allocated VM values,
since the switch representation now only depends on the shape of the inductive
type.
|
|
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
entry struc_tuple
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Ack-by: backtracking
Reviewed-by: gares
|
|
This is just a fixup, likely all the places that are matching on
`UserErr` directly are just buggy.
|
|
Co-authored-by: <Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
|
|
Exceptions should not printed except for the top-level.
There is the weird anomaly-absorbing code in `Reductionops`, I wonder
how frequent that case is, but as the exception is absorbed printing
there could have a real impact.
|
|
This requires updating the parameter count at section end, I felt it
was easier to do with rebuild_function but it could be done in
discharge if needed.
Incidentally fixes #12649.
|
|
projection
Reviewed-by: ejgallego
Ack-by: gares
|
|
|
|
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
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.
|
|
|
|
Perhaps we should thread an evar map with the Var universes added
through to cs_pattern_of_constr but that would be significantly more invasive.
Fix #12528
|
|
|
|
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.
|
