You'll need the following software:
I've really only tested this in Debian Linux, so things might not work elsewhere.
From the SourceForge download page, you can obtain an ltamer tarball for the main library and a ctpc tarball for the compiler.
In the directory where you unpacked the ltamer tarball, run:
./configure COQSRC=/path/to/coq/source/tree
and then
make
Make sure you've built Coq from source in the directory you've specified (by following the directions in the Coq source distribution) before runing make here. If you installed OCamlMakefile somewhere besides one of the recommended places, pass an additional configure command-line argument OCAMLMAKEFILE=/path/to/it.
In the directory where you unpacked the ctpc tarball, run:
./configure
and then
make
With a non-standard OCamlMakefile location, pass the same extra argument as above. If you haven't checked out the two tarballs into subdirectories of the same parent directory, then you'll need to pass configure a command-line argument specifying LTAMERHOME.
Unless you have a really beefy machine or are willing to let this build overnight, you probably want to run make with the environment variable LTAMER_DEBUG set to at least 1, which asserts as axioms some of the more computationally-expensive proofs associated with generic programming. At debug level 1, it is still possible to extract an executable compiler that really runs. If building is still too RAM-intensive, try setting LTAMER_DEBUG to 2, which will also assert as axioms some functions with real computational content. You won't be able to extract an executable compiler from the result of such a build.
From the directory where you've built ltamer, you can follow this interaction to load the simply-typed lambda calculus example language and trigger the automatic construction of syntactic support functions and their associated correctness proofs.
$ make coqtop
bin/coqtop -impredicative-set -R src/coq LambdaTamer
Welcome to Coq 8.0pl3 (Jan 2006)
Coq < Load "examples/STLC".
Coq < Syntactify term.
(* Various chatty output *)
Coq < Syntactify termDenote.
(* Various chatty output *)
Coq < Print Module Term.
(* Signature of Term module, containing auto-generated syntactic helper functions *)
Coq < Print Module TermDenote.
(* Signature of TermDenote module, containing auto-generated correctness proofs *)
Coq < Check Term.lift.
Term.lift
: forall (t' : ty) (G : list ty) (t : ty), term G t -> term (t' :: G) t
Coq < Check TermDenote.lift_sound.
TermDenote.lift_sound
: forall (G : list ty) (t : ty) (e : term G t)
(t' : ty) (v : tyDenote t') (s : Subst tyDenote G),
termDenote (Term.lift t' e) (SCons t' v s) = termDenote e s
To check that CTPC (the certified type-preserving compiler) built properly, try this from the directory where you unpacked the ctpc tarball:
$ bin/ctpc tests/id.src block1: r3 := r2.0 r4 := r2.1 r7 := r3 r6 := r1 r5 := r4 r1 := r6 r0 := r5 jump r7 main: r1 := new([r0], []) r2 := 1 r3 := new([r1,r0], [r2,r1]) r4 := r0.0 r5 := r0.1 r8 := r4 r7 := r3 r6 := r5 r1 := r7 r0 := r6 jump r8
You might also want to poke around the Coq development interactively:
$ make coqtop
$(LTAMERHOME)/bin/coqtop -impredicative-set -R $(LTAMERHOME)/src/coq LambdaTamer -R $(CTPCHOME)/src/coq CTPC
Welcome to Coq 8.0pl3 (Jan 2006)
Coq < Require Import CTPC.Compile.
Coq < Check compile_term.
compile_term
: forall t : Source.sty, Source.sterm List.nil t -> Asm.program
A word of warning about this code in general: There is some majorly computationally intensive stuff here, so don't be surprised at long build/run times! The main expensive things are brute-force proof search in the CTPC correctness proof and the delicate reflective stuff used for generic programming.
The Coq source is located in ltamer/src/coq. This part is rather sparsely-commented, since it's mostly nasty, and clients of the library would be better off not peeking into the implementation details.
| Module | Description |
|---|---|
| Ext | Assume the axiom of functional extensionality |
| ListT | Type-level and dependently-typed list variants |
| ListUtil | Regular list support code and theorems |
| Binding | Formalizing variable binding, contexts, and substitutions |
| AutoSyntax | The part of helper function generic programming that is implemented in Coq |
| LambdaTamer | Re-exports the modules needed to define new object languages |
In ltamer/src/ocaml, there is the OCaml code implementing a Coq extension to support generic programming of object language-specific helper functions. The implementation is very awful-looking, so I won't even begin trying to document it here! The Makefile should build a custom ltamer/bin/coqtop that supports this extension via the Syntactify command. Check ltamer/examples/STLC.v and the other contents of that directory to see how to use this stuff.
The Coq source is located in ctpc/src/coq.
| Module | Description |
|---|---|
| Dict | Applicative dictionaries |
| Trace | Co-inductive program traces |
| Source | The compiler's source language, simply-typed lambda calculus |
| Continuation | Some continuations support code |
| CPS | A linearized language with special continuation support |
| CPSify | Translation from Source to CPS with correctness proof |
| Cont | A linearized language with multiple-argument continuations |
| Contify | Translation from CPS to Cont with correctness proof |
| CC | Target language of closure conversion |
| CCify | Translation from Cont to CC with correctness proof |
| AllocMonad | A monadic description of heap manipulation |
| Alloc | Language with explicit heap-allocation of records |
| Allocify | Translation from CC to Alloc with correctness proof |
| Flat | Language with registers and no variables |
| Flatify | Translation from Alloc to Flat with correctness proof |
| Safety | Garbage collection safety theorem for Flat |
| Asm | The compiler's target language, an idealized assembly language |
| Asmify | Translation from Flat to Asm with correctness proof |
| Compile | Putting it all together |
The default make target will first compile all of the Coq sources and then extract OCaml code from the result into ctpc/src/ocaml/Compile.ml. The rest of the code in ctpc/src/ocaml implements parsing and type-checking of inputs and pretty-printing of outputs, mostly serving as a driver for the mammoth hunk of code in Compile.ml. Running ctpc/bin/ctpc filename.src tries to compile source file filename.src and pretty-print the result. Some example sources are found in ctpc/tests.