| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
|
|
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>
|
|
|
|
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.
|
|
Add headers to a few files which were missing them.
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
|
|
|
|
|
|
|
|
|
|
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>
|
|
It seems that it was a remnant of a time where Reductionops would share the
same data types.
|
|
The use of a term is not needed for the fast typing algorithm of the
application case, so this tweak brings the best of both worlds.
|
|
There is little point to this as the type is dependent on an open value and
is never computed further.
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
We take advantage of the separation of implementation from CBV to remove
constant code.
|
|
|
|
Just like in the Sixth Sense, it turns out it was dead code all along.
|
|
We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.
Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.
|
|
The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
|
|
We untangle the implementation in several ways.
- No higher-order self argument function as there is only one caller.
- Compute composition of lifts + substitution on terms using a dedicated
function instead of mk_clos followed by to_constr.
- Take more advantage of identity substitutions.
|
|
The new implementation is 100% compatible with the previous one, but it
is more compact and does not use a tricky translation function from the
kernel.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This fixes the previous patch in rare corner-cases where unification code was
relying on both kernel conversion and specific transparent state.
|
|
- use Redflags.red_projection
- share unfold_projection between CClosure and Reduction
|
|
There don't really bring anything, we also correct some minor nits
with the printing function.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
|
|
This exports two functions:
- declare_reduction_effect: to declare a hook to be applied when some
constant are visited during the execution of some reduction functions
(primarily cbv, but also cbn, simpl, hnf, ...).
- set_reduction_effect: to declare a constant on which a given effect
hook should be called.
Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin.
Added support for printing effect in functions of tacred.ml.
|
|
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
|
