\begin{code}
module Desugar ( deSugar, deSugarExpr ) where
-import TysWiredIn (unitDataConId)
import DynFlags
import StaticFlags
import HscTypes
import Name
import CoreSyn
import CoreSubst
+import CoqPass ( coqPassCoreToString, coqPassCoreToCore )
import PprCore
import DsMonad
import DsExpr
import OrdList
import Data.List
import Data.IORef
-import Control.Exception ( catch, ErrorCall, Exception(..) )
\end{code}
%************************************************************************
; (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
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 $
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}