Support for writing GHC passes in Coq
In order to implement heterogeneous metaprogramming for GHC, I have produced a complete formalization of System FC1 in Coq. The extracted Haskell code links directly into GHC and works at the level of Core expressions.
There are four distinct representations for a given chunk of Haskell code: Core, Weak, Strong and Proof. Think of them like a pipeline.
Conversions in both directions between all adjacent representation pairs are provided. You can also turn a HaskProof into a LaTeX document showing the actual proof tree (here's an example). The emitted LaTeX code requires trfrac.sty and mathpartir. Keep in mind that for anything more than a trivial program the proof trees will get quite large (here's an example) and may require expanding your TeX limits.
Some parts of the HaskCore-to-HaskWeak translation are written in Haskell, and therefore no more trustworthy (from a type-system-provided guarantee perspective) than the rest of GHC. From HaskWeak onward everything is in Coq.
Invoking GHC with the new flag -fcoqpass will run all the top-level bindings through the function coqPassCoreToCore defined in Extraction.v immediately after the desugarer; the bindings returned by that function are then sent through the rest of the compiler. Invoking with the new flag -ddump-proofs will pass those bindings instead to coqPassCoreToString and dump the string it returns. Finally, -ddump-coqpass will dump the core expression returned by coqPassCoreToCore.
The gitweb is here
git clone http://git.megacz.com/coq-hetmet.git
There is a branch which has the extracted Haskell code “baked in”; use this branch if you don't have the Coq compiler installed on your local machine:
git clone -b coq-extraction-baked-in http://git.megacz.com/coq-hetmet.git
You can find nice pretty-printed PDFs (the scripts use weird unicode characters) of the key parts of the formalization here.
If you're in a hurry, paste these commands into a shell window and come back after lunch:
git clone http://git.megacz.com/ghc-hetmet.git
git clone -b coq-extraction-baked-in \
chmod +x sync-all
git clone http://git.megacz.com/ghc-base.git libraries/base
./sync-all -r http://darcs.haskell.org/ get
echo 'GhcStage1HcOpts = -O0 -fasm' >> mk/build.mk
echo 'GhcStage2HcOpts = -O0 -fasm' >> mk/build.mk
cp mk/build.mk.sample mk/build.mk
make BuildFlavour=quickest inplace/bin/ghc-stage2
echo -e 'main = putStrLn "Hello, World"' > HelloWorld.hs
inplace/bin/ghc-stage2 -ddump-proofs -ddump-to-file HelloWorld.hs
mv HelloWorld.coqpass HelloWorld.tex
and you should get this
All of the code for Coq-in-GHC resides in files whose name starts with Hask. In general:
The HaskXXXXToYYYY files are rarely (goal: never) imported by any other file; they are the leaves of the dependency tree. I try to keep all of the other files as clean and readable as possible, and let the HaskXXXXToYYYY get messy and convoluted at their expense.
Necessary Coq Patches