| Age | Commit message (Collapse) | Author |
|---|
|
There is a hidden invariant that guarantees that the class index and its
reference field are the same.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
purely applicative stacks
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Probably a remnant of a time where the difference in code path was relevant.
|
|
It was only used there, and its API required to export an ad-hoc type
to represent pattern-matchings.
|
|
|
|
|
|
stacks.
|
|
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
|
