From aee44bbe090c356d649398a93e260d967a7c50db Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:48:48 -0800 Subject: [PATCH] add code for -dcoqpass, -fcoqpass, -ddump-coqpass --- .gitmodules | 3 +++ compiler/coq | 1 + compiler/deSugar/Desugar.lhs | 39 +++++++++++++-------------------------- compiler/ghc.cabal.in | 1 + compiler/main/DynFlags.hs | 9 +++++++++ ghc.mk | 12 ++++++++++++ 6 files changed, 39 insertions(+), 26 deletions(-) create mode 100644 .gitmodules create mode 160000 compiler/coq diff --git a/.gitmodules b/.gitmodules new file mode 100644 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 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 --- 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 --- 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 --- 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) stuff --------------------------- , Flag "monly-2-regs" (noArg (\s -> s{stolen_x86_regs = 2})) diff --git a/ghc.mk b/ghc.mk index 46b6c4e..f7d236b 100644 --- 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 $@ -- 1.7.10.4