add code for -dcoqpass, -fcoqpass, -ddump-coqpass

diff --git a/.gitmodules b/.gitmodules
new file mode 100644 (file)
index 0000000..162e65d
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "compiler/coq"]
+       path = compiler/coq
+       url = http://git.megacz.com/coq-garrows.git

diff --git a/compiler/coq b/compiler/coq
new file mode 160000 (submodule)
index 0000000..a764632
--- /dev/null
+++ b/compiler/coq
@@ -0,0 +1 @@
+Subproject commit a764632d29c79933e8c54633831e4aac0fb204f6

diff --git a/compiler/deSugar/Desugar.lhs b/compiler/deSugar/Desugar.lhs
index 14e4eea..cbf64e2 100644 (file)
--- a/compiler/deSugar/Desugar.lhs
+++ b/compiler/deSugar/Desugar.lhs
@@ -8,7 +8,6 @@ The Desugarer: turning HsSyn into Core.
 \begin{code}
 module Desugar ( deSugar, deSugarExpr ) where
 
-import TysWiredIn (unitDataConId)
 import DynFlags
 import StaticFlags
 import HscTypes
@@ -19,6 +18,7 @@ import Id
 import Name
 import CoreSyn
 import CoreSubst
+import CoqPass ( coqPassCoreToString, coqPassCoreToCore )
 import PprCore
 import DsMonad
 import DsExpr
@@ -41,7 +41,6 @@ import MonadUtils
 import OrdList
 import Data.List
 import Data.IORef
-import Control.Exception ( catch, ErrorCall, Exception(..) )
 \end{code}
 
 %************************************************************************
@@ -138,26 +137,16 @@ deSugar hsc_env
        ; (ds_binds, ds_rules_for_imps) <- simpleOptPgm dflags final_pgm rules_for_imps
                         -- The simpleOptPgm gets rid of type 
                         -- bindings plus any stupid dead code
-{-
-        ; dumpIfSet_dyn dflags Opt_D_dump_proof "input to flattener" (text $ showSDoc $ pprCoreBindings ds_binds)
-        ; let uhandler (err::ErrorCall)
-                      = dumpIfSet_dyn dflags Opt_D_dump_proof "System FC Proof"
-                                       (text $ "\\begin{verbatim}\n" ++
-                                               show err ++
-                                               "\\end{verbatim}\n\n")
-          in (dumpIfSet_dyn dflags Opt_D_dump_proof "System FC Proof" $
-               (vcat (map (\ bind -> let e = case bind of
-                                               NonRec b e -> e
-                                               Rec    lve -> Let (Rec lve) (Var unitDataConId)
-                                     in text $ "\\begin{verbatim}\n" ++
-                                               (showSDoc $ pprCoreBindings ds_binds) ++
-                                               "\\end{verbatim}\n\n" ++
-                                               "$$\n"++
-                                               (core2proofAndShow e) ++
-                                               "$$\n"
-                          ) ds_binds))) `Control.Exception.catch` uhandler
--}
-       ; endPass dflags CoreDesugar ds_binds ds_rules_for_imps
+
+        ; dumpIfSet_dyn dflags Opt_D_coqpass "Coq Pass Output" $ text $ coqPassCoreToString ds_binds
+
+        ; ds_binds' <- if dopt Opt_F_coqpass dflags
+                       then return $ coqPassCoreToCore ds_binds
+                       else return ds_binds
+
+        ; dumpIfSet_dyn dflags Opt_D_dump_coqpass "After Coq Pass" (text $ showSDoc $ pprCoreBindings ds_binds')
+
+       ; endPass dflags CoreDesugar ds_binds' ds_rules_for_imps
 
         ; let used_names = mkUsedNames tcg_env
        ; deps <- mkDependencies tcg_env
@@ -245,7 +234,7 @@ deSugarExpr :: HscEnv
 
 deSugarExpr hsc_env this_mod rdr_env type_env tc_expr = do
     let dflags = hsc_dflags hsc_env
-    showPass dflags "Desugarz"
+    showPass dflags "Desugar"
 
     -- Do desugaring
     (msgs, mb_core_expr) <- initDs hsc_env this_mod rdr_env type_env $
@@ -255,10 +244,8 @@ deSugarExpr hsc_env this_mod rdr_env type_env tc_expr = do
       Nothing   -> return (msgs, Nothing)
       Just expr -> do
 
-{-
         -- Dump output
-        dumpIfSet_dyn dflags Opt_D_dump_ds    "Desugared"            (text $ "$$\n"++(core2proofAndShow expr)++"$$\n")
--}
+        dumpIfSet_dyn dflags Opt_D_dump_ds "Desugared" (pprCoreExpr expr)
 
         return (msgs, Just expr)
 \end{code}

diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 32d13f8..8cb64ab 100644 (file)
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -269,6 +269,7 @@ Library
         CoreTidy
         CoreUnfold
         CoreUtils
+        CoqPass
         ExternalCore
         MkCore
         MkExternalCore

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 3990f04..bc30d60 100644 (file)
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -179,6 +179,10 @@ data DynFlag
    | Opt_DoCmmLinting
    | Opt_DoAsmLinting
 
+   | Opt_F_coqpass                      -- run the core-to-core   coqPass (does whatever CoqPass.hs says)
+   | Opt_D_coqpass                      -- run the core-to-string coqPass and dumps the result
+   | Opt_D_dump_coqpass                 -- dumps the output of the core-to-core coqPass
+
    | Opt_WarnIsError                    -- -Werror; makes warnings fatal
    | Opt_WarnDuplicateExports
    | Opt_WarnHiShadows
@@ -1292,6 +1296,11 @@ dynamic_flags = [
                                               setVerbosity (Just 2)))
   , Flag "dfaststring-stats"       (NoArg (setDynFlag Opt_D_faststring_stats))
 
+        ------ Coq-in-GHC ---------------------------
+  , Flag "dcoqpass"                (NoArg (setDynFlag Opt_D_coqpass))
+  , Flag "ddump-coqpass"           (NoArg (setDynFlag Opt_D_dump_coqpass))
+  , Flag "fcoqpass"                (NoArg (setDynFlag Opt_F_coqpass))
+
         ------ Machine dependant (-m<blah>) stuff ---------------------------
 
   , Flag "monly-2-regs" (noArg (\s -> s{stolen_x86_regs = 2}))

diff --git a/ghc.mk b/ghc.mk
index 46b6c4e..f7d236b 100644 (file)
--- a/ghc.mk
+++ b/ghc.mk
@@ -1212,3 +1212,15 @@ phase_0_builds: $(utils/genprimopcode_dist_depfile_c_asm)
 .PHONY: phase_1_builds
 phase_1_builds: $(PACKAGE_DATA_MKS)
 
+# -----------------------------------------------------------------------------
+# Support for writing GHC passes in Coq
+
+compiler/coq/:
+       git submodule update --init compiler/coq
+       cd compiler/coq/; git checkout master
+compiler/coq/build/CoqPass.hs: compiler/coq/ $(wildcard compiler/coq/src/*.v) $(wildcard compiler/coq/src/*.hs)
+       cd compiler/coq; make
+compiler/stage1/build/CoqPass.hs: compiler/coq/build/CoqPass.hs
+       cp compiler/coq/build/CoqPass.hs $@
+compiler/stage2/build/CoqPass.hs: compiler/coq/build/CoqPass.hs
+       cp compiler/coq/build/CoqPass.hs $@