| Age | Commit message (Collapse) | Author |
|---|
|
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
|
