| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
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
|
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias
Maxime Dénès
mrmr1993
Théo Zimmermann
Gaëtan Gilbert
Thomas Sibut-Pinote
Pierre Letouzey