GitLab

Not inlining proxy variables inside a [Efun].

Extraction of let x = e1 in e2

Fold_left for lists and sequences (wip)

Not printing parentheses around constants
(though still not completely satisfying

Optimization of proxy variables.

Why3 files from standard library are not extracted

Optimization of singleton record types.
Still missing treatment of record types defined in drivers

Preparing for the GT demo

Empty extracted modules (all definitions are defined in the driver)
are printed no more, independently of the extraction mode

New command line nearly done

Preparing for the new command line.

Preparing for the new command line.

Better treatment of partial applied constructors

in preparation of command-line option --mono

Support for recursive extraction and qualified names

Treatment of top-level constants

[Raise] expressions compiled and printed

For loops are now turned into a local recursive function.
This allows big integers to be used as indexes of the loop

Inlining of variables binded to unit

Constructors without arguments are now inlined in extracted code

Forgetting local variables identifiers

Treatment of top-level recursive definitions

Erasure of ghost code in statements sequence

Minor changes in compile.ml and ocaml_printer.ml

Working with the extraction driver