History log of /seL4-l4v-10.1.1/HOL4/src/emit/EmitML.sig
Revision Date Author Comments
# 06c2f5c2 21-Mar-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix src/emit (phew!)


# 4761143b 10-Aug-2009 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!


# 8a9fb01c 24-Feb-2009 Konrad Slind <konrad.slind@gmail.com>

Changes to EmitML.


# 3fee4ee4 22-Feb-2009 Konrad Slind <konrad.slind@gmail.com>

Implement ML code generation for large records.


# 8654de63 07-Feb-2009 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories


# 7163eb34 19-Jun-2008 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Added EmitML.emitCAML for exporting to Ocaml. This has required a fair
amount of hackery, none of which should effect emitML. In particular,
CAML constructors must start with an uppercase letter and other values
must not. Also, types can't start with a lowercase letter. Constructors
are added to the constants map with ConstMapML.insert_cons.

(I will eventually check-in the script for generating CAML versions of the
code emitted to src/theoryML.)


# ec2041c1 23-Apr-2008 Anthony Fox <anthony.fox@cl.cam.ac.uk>

Moved EmitML code to a new directory src/emit.

Added a new structure EmitTeX. This allows HOL theories to be printed
as LaTeX source.

Added both of these structures to help/src/Keepers.sml