Revisions of extracted/arithmetic.ml
http://cerco.cs.unibo.it/log/extracted/arithmetic.ml?rev=2746
Trac Log - Revisions of extracted/arithmetic.mlen-USTrac 1.2CerCohttp://cerco.cs.unibo.it/chrome/site/cerco_logo.png
http://cerco.cs.unibo.it/log/extracted/arithmetic.ml?rev=2746
sacerdotSat, 23 Feb 2013 00:16:55 GMTRevision 2717: Extracted code for the whole compiler.
The space cost model is not ...
http://cerco.cs.unibo.it/changeset/2717/extracted/arithmetic.ml
http://cerco.cs.unibo.it/changeset/2717/extracted/arithmetic.mlExtracted code for the whole compiler.
The space cost model is not there yet.
I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).
I have also changed all axioms to be implemented
so that they do not fail at initialization time.LogsacerdotThu, 07 Feb 2013 21:43:49 GMTRevision 2649: ...
http://cerco.cs.unibo.it/changeset/2649/extracted/arithmetic.ml
http://cerco.cs.unibo.it/changeset/2649/extracted/arithmetic.ml…LogsacerdotTue, 05 Feb 2013 12:36:31 GMTRevision 2601: Extraction to ocaml is now working, with a couple of bugs left.
One ...
http://cerco.cs.unibo.it/changeset/2601/extracted/arithmetic.ml
http://cerco.cs.unibo.it/changeset/2601/extracted/arithmetic.mlExtraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.
The extracted directory contains:
1. a snapshot of the .ml(i) files extracted from <a class="missing wiki">CerCo?</a> by running
ocamlc.opt -extract_ocaml compiler.ma
The files have been patched by hand to implement all strings and
fix the bugs.
2. a file PROBLEMS that describes the remaining problems, i.e. bugs
and axioms to be implemented
To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.Log