| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
This also allows to move the strong variant of cbn to the Cbn module.
|
|
Also works for simpl.
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
Reviewed-by: gares
|
|
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
There functions export the internal stack representation. The only real user
is unification, which is suffering from major performance issues due to the
naive representation of substitutions in processes.
|
|
|
|
Also includes minor layout or code changes.
|
|
|
|
It was only used there, and its API required to export an ad-hoc type
to represent pattern-matchings.
|
|
Ack-by: gares
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.
|
|
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>
|
|
|
|
It was only used in Tacred, and with a type that forced to perform a
change of representation of stacks.
|
|
|
|
We factorize code between Cbn and Reductionops, and remove dead code as well.
|
|
|
|
|
|
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.
|
|
- Removal of exported types and functions that were unused.
- Moving ad-hoc functions that were used once in the codebase to their call site.
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
Incidentally, this fixes #10056
|
|
There is no point, it is always called with refolding turned off.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
We also stop passing dummy env and evar maps.
|
|
The functions in `Termops.print_*` are meant to be debug printers,
however, they are sometimes used in non-debug code due to a API
confusion.
We thus wrap such functions into an `Internal` module, improve
documentation, and switch users to the right API.
|
|
|
|
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
We only ever call `reduction_effect_hook` on constants, so there's no
point allowing it to be declared with globrefs. There is also no point
using a constr map instead of constant map.
(Technically there was a call of the effect hook on projections, but
that can never match a globref so it was useless)
|
|
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
|
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.
|
|
|
|
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
|
|
|
|
|
