add -fsimpleopt-before-flatten
[ghc-hetmet.git] / compiler / main / DynFlags.hs
index 9b1b060..6fe6708 100644 (file)
@@ -1,6 +1,3 @@
-{-# OPTIONS_GHC -w #-}
--- Temporary, until rtsIsProfiled is fixed
-
 -- |
 -- Dynamic flags
 --
@@ -40,10 +37,12 @@ module DynFlags (
         extraGccViaCFlags, systemPackageConfig,
         pgm_L, pgm_P, pgm_F, pgm_c, pgm_s, pgm_a, pgm_l, pgm_dll, pgm_T,
         pgm_sysman, pgm_windres, pgm_lo, pgm_lc,
+        opt_L, opt_P, opt_F, opt_c, opt_m, opt_a, opt_l,
+        opt_windres, opt_lo, opt_lc,
 
 
         -- ** Manipulating DynFlags
-        defaultDynFlags,                -- DynFlags
+        defaultDynFlags,                -- Settings -> DynFlags
         initDynFlags,                   -- DynFlags -> IO DynFlags
 
         getOpts,                        -- DynFlags -> (DynFlags -> [a]) -> [a]
@@ -96,10 +95,14 @@ import Maybes           ( orElse )
 import SrcLoc
 import FastString
 import Outputable
+#ifdef GHCI
 import Foreign.C       ( CInt )
+#endif
 import {-# SOURCE #-} ErrUtils ( Severity(..), Message, mkLocMessage )
 
+#ifdef GHCI
 import System.IO.Unsafe        ( unsafePerformIO )
+#endif
 import Data.IORef
 import Control.Monad    ( when )
 
@@ -107,7 +110,7 @@ import Data.Char
 import Data.List
 import Data.Map (Map)
 import qualified Data.Map as Map
-import Data.Maybe
+-- import Data.Maybe
 import System.FilePath
 import System.IO        ( stderr, hPutChar )
 
@@ -187,6 +190,13 @@ data DynFlag
    | Opt_DoCmmLinting
    | Opt_DoAsmLinting
 
+   | Opt_F_coqpass                      -- run the core-to-core coqPass, but don't change anything (just "parse/unparse")
+   | Opt_F_skolemize                    -- run the core-to-core coqPass, skolemizing the proof
+   | Opt_F_flatten                      -- run the core-to-core coqPass, flattening the proof
+   | Opt_F_simpleopt_before_flatten     -- run the "simplPgmOpt" before the coqPass
+   | Opt_D_dump_proofs                  -- dump natural deduction typing proof of the coqpass input
+   | Opt_D_coqpass                      -- run the core-to-string coqPass and dumps the result
+
    | Opt_WarnIsError                    -- -Werror; makes warnings fatal
    | Opt_WarnDuplicateExports
    | Opt_WarnHiShadows
@@ -317,6 +327,7 @@ data ExtensionFlag
    | Opt_GHCForeignImportPrim
    | Opt_ParallelArrays                 -- Syntactic support for parallel arrays
    | Opt_Arrows                         -- Arrow-notation syntax
+   | Opt_ModalTypes                     -- Heterogeneous Metaprogramming (modal types, brackets, escape, CSP)
    | Opt_TemplateHaskell
    | Opt_QuasiQuotes
    | Opt_ImplicitParams
@@ -452,18 +463,6 @@ data DynFlags = DynFlags {
 
   hpcDir                :: String,      -- ^ Path to store the .mix files
 
-  -- options for particular phases
-  opt_L                 :: [String],
-  opt_P                 :: [String],
-  opt_F                 :: [String],
-  opt_c                 :: [String],
-  opt_m                 :: [String],
-  opt_a                 :: [String],
-  opt_l                 :: [String],
-  opt_windres           :: [String],
-  opt_lo                :: [String], -- LLVM: llvm optimiser
-  opt_lc                :: [String], -- LLVM: llc static compiler
-
   settings              :: Settings,
 
   --  For ghc -M
@@ -531,7 +530,19 @@ data Settings = Settings {
   sPgm_sysman            :: String,
   sPgm_windres           :: String,
   sPgm_lo                :: (String,[Option]), -- LLVM: opt llvm optimiser
-  sPgm_lc                :: (String,[Option])  -- LLVM: llc static compiler
+  sPgm_lc                :: (String,[Option]), -- LLVM: llc static compiler
+  -- options for particular phases
+  sOpt_L                 :: [String],
+  sOpt_P                 :: [String],
+  sOpt_F                 :: [String],
+  sOpt_c                 :: [String],
+  sOpt_m                 :: [String],
+  sOpt_a                 :: [String],
+  sOpt_l                 :: [String],
+  sOpt_windres           :: [String],
+  sOpt_lo                :: [String], -- LLVM: llvm optimiser
+  sOpt_lc                :: [String]  -- LLVM: llc static compiler
+
  }
 
 ghcUsagePath          :: DynFlags -> FilePath
@@ -574,6 +585,26 @@ pgm_lo                :: DynFlags -> (String,[Option])
 pgm_lo dflags = sPgm_lo (settings dflags)
 pgm_lc                :: DynFlags -> (String,[Option])
 pgm_lc dflags = sPgm_lc (settings dflags)
+opt_L                 :: DynFlags -> [String]
+opt_L dflags = sOpt_L (settings dflags)
+opt_P                 :: DynFlags -> [String]
+opt_P dflags = sOpt_P (settings dflags)
+opt_F                 :: DynFlags -> [String]
+opt_F dflags = sOpt_F (settings dflags)
+opt_c                 :: DynFlags -> [String]
+opt_c dflags = sOpt_c (settings dflags)
+opt_m                 :: DynFlags -> [String]
+opt_m dflags = sOpt_m (settings dflags)
+opt_a                 :: DynFlags -> [String]
+opt_a dflags = sOpt_a (settings dflags)
+opt_l                 :: DynFlags -> [String]
+opt_l dflags = sOpt_l (settings dflags)
+opt_windres           :: DynFlags -> [String]
+opt_windres dflags = sOpt_windres (settings dflags)
+opt_lo                :: DynFlags -> [String]
+opt_lo dflags = sOpt_lo (settings dflags)
+opt_lc                :: DynFlags -> [String]
+opt_lc dflags = sOpt_lc (settings dflags)
 
 wayNames :: DynFlags -> [WayName]
 wayNames = map wayName . ways
@@ -697,8 +728,8 @@ initDynFlags dflags = do
 
 -- | The normal 'DynFlags'. Note that they is not suitable for use in this form
 -- and must be fully initialized by 'GHC.newSession' first.
-defaultDynFlags :: DynFlags
-defaultDynFlags =
+defaultDynFlags :: Settings -> DynFlags
+defaultDynFlags mySettings =
      DynFlags {
         ghcMode                 = CompManager,
         ghcLink                 = LinkBinary,
@@ -753,19 +784,6 @@ defaultDynFlags =
 
         hpcDir                  = ".hpc",
 
-        opt_L                   = [],
-        opt_P                   = (if opt_PIC
-                                   then ["-D__PIC__", "-U __PIC__"] -- this list is reversed
-                                   else []),
-        opt_F                   = [],
-        opt_c                   = [],
-        opt_a                   = [],
-        opt_m                   = [],
-        opt_l                   = [],
-        opt_windres             = [],
-        opt_lo                  = [],
-        opt_lc                  = [],
-
         extraPkgConfs           = [],
         packageFlags            = [],
         pkgDatabase             = Nothing,
@@ -774,8 +792,7 @@ defaultDynFlags =
         buildTag                = panic "defaultDynFlags: No buildTag",
         rtsBuildTag             = panic "defaultDynFlags: No rtsBuildTag",
         splitInfo               = Nothing,
-        -- initSysTools fills this in:
-        settings                = panic "defaultDynFlags: No settings",
+        settings                = mySettings,
         -- ghc -M values
         depMakefile       = "Makefile",
         depIncludePkgDeps = False,
@@ -950,8 +967,8 @@ setDumpPrefixForce f d = d { dumpPrefixForce = f}
 -- XXX HACK: Prelude> words "'does not' work" ===> ["'does","not'","work"]
 -- Config.hs should really use Option.
 setPgmP   f = let (pgm:args) = words f in alterSettings (\s -> s { sPgm_P   = (pgm, map Option args)})
-addOptl   f d = d{ opt_l   = f : opt_l d}
-addOptP   f d = d{ opt_P   = f : opt_P d}
+addOptl   f = alterSettings (\s -> s { sOpt_l   = f : sOpt_l s})
+addOptP   f = alterSettings (\s -> s { sOpt_P   = f : sOpt_P s})
 
 
 setDepMakefile :: FilePath -> DynFlags -> DynFlags
@@ -1146,16 +1163,16 @@ dynamic_flags = [
   , Flag "pgmwindres"     (hasArg (\f -> alterSettings (\s -> s { sPgm_windres = f})))
 
     -- need to appear before -optl/-opta to be parsed as LLVM flags.
-  , Flag "optlo"          (hasArg (\f d -> d{ opt_lo  = f : opt_lo d}))
-  , Flag "optlc"          (hasArg (\f d -> d{ opt_lc  = f : opt_lc d}))
-  , Flag "optL"           (hasArg (\f d -> d{ opt_L   = f : opt_L d}))
+  , Flag "optlo"          (hasArg (\f -> alterSettings (\s -> s { sOpt_lo  = f : sOpt_lo s})))
+  , Flag "optlc"          (hasArg (\f -> alterSettings (\s -> s { sOpt_lc  = f : sOpt_lc s})))
+  , Flag "optL"           (hasArg (\f -> alterSettings (\s -> s { sOpt_L   = f : sOpt_L s})))
   , Flag "optP"           (hasArg addOptP)
-  , Flag "optF"           (hasArg (\f d -> d{ opt_F   = f : opt_F d}))
-  , Flag "optc"           (hasArg (\f d -> d{ opt_c   = f : opt_c d}))
-  , Flag "optm"           (hasArg (\f d -> d{ opt_m   = f : opt_m d}))
-  , Flag "opta"           (hasArg (\f d -> d{ opt_a   = f : opt_a d}))
+  , Flag "optF"           (hasArg (\f -> alterSettings (\s -> s { sOpt_F   = f : sOpt_F s})))
+  , Flag "optc"           (hasArg (\f -> alterSettings (\s -> s { sOpt_c   = f : sOpt_c s})))
+  , Flag "optm"           (hasArg (\f -> alterSettings (\s -> s { sOpt_m   = f : sOpt_m s})))
+  , Flag "opta"           (hasArg (\f -> alterSettings (\s -> s { sOpt_a   = f : sOpt_a s})))
   , Flag "optl"           (hasArg addOptl)
-  , Flag "optwindres"     (hasArg (\f d -> d{ opt_windres = f : opt_windres d}))
+  , Flag "optwindres"     (hasArg (\f -> alterSettings (\s -> s { sOpt_windres = f : sOpt_windres s})))
 
   , Flag "split-objs"
          (NoArg (if can_split 
@@ -1319,6 +1336,14 @@ dynamic_flags = [
                                               setVerbosity (Just 2)))
   , Flag "dfaststring-stats"       (NoArg (setDynFlag Opt_D_faststring_stats))
 
+        ------ Coq-in-GHC ---------------------------
+  , Flag "ddump-proofs"            (NoArg (setDynFlag Opt_D_dump_proofs))
+  , Flag "ddump-coqpass"           (NoArg (setDynFlag Opt_D_coqpass))
+  , Flag "fcoqpass"                (NoArg (setDynFlag Opt_F_coqpass))
+  , Flag "fsimpleopt-before-flatten"                (NoArg (setDynFlag Opt_F_simpleopt_before_flatten))
+  , Flag "fflatten"                (NoArg (do { setDynFlag Opt_F_coqpass ; setDynFlag Opt_F_flatten }))
+  , Flag "funsafe-skolemize"       (NoArg (do { setDynFlag Opt_F_coqpass ; setDynFlag Opt_F_flatten ; setDynFlag Opt_F_skolemize }))
+
         ------ Machine dependant (-m<blah>) stuff ---------------------------
 
   , Flag "monly-2-regs" (NoArg (addWarn "The -monly-2-regs flag does nothing; it will be removed in a future GHC release"))
@@ -1354,7 +1379,7 @@ dynamic_flags = [
   , Flag "fcontext-stack"              (intSuffix (\n d -> d{ ctxtStkDepth = n }))
   , Flag "fstrictness-before"          (intSuffix (\n d -> d{ strictnessBefore = n : strictnessBefore d }))
   , Flag "ffloat-lam-args"             (intSuffix (\n d -> d{ floatLamArgs = Just n }))
-  , Flag "ffloat-all-lams"             (intSuffix (\n d -> d{ floatLamArgs = Nothing }))
+  , Flag "ffloat-all-lams"             (noArg (\d -> d{ floatLamArgs = Nothing }))
 
         ------ Profiling ----------------------------------------------------
 
@@ -1618,6 +1643,7 @@ xFlags = [
     deprecatedForExtension "DoRec"),
   ( "DoRec",                            Opt_DoRec, nop ),
   ( "Arrows",                           Opt_Arrows, nop ),
+  ( "ModalTypes",                      Opt_ModalTypes, nop ),
   ( "ParallelArrays",                   Opt_ParallelArrays, nop ),
   ( "TemplateHaskell",                  Opt_TemplateHaskell, checkTemplateHaskellOk ),
   ( "QuasiQuotes",                      Opt_QuasiQuotes, nop ),
@@ -1710,6 +1736,11 @@ impliedFlags
     , (Opt_FlexibleInstances,         turnOn, Opt_TypeSynonymInstances)
     , (Opt_FunctionalDependencies,    turnOn, Opt_MultiParamTypeClasses)
 
+    , (Opt_ModalTypes,                 turnOn,  Opt_RankNTypes)
+    , (Opt_ModalTypes,                 turnOn,  Opt_ExplicitForAll)
+    --, (Opt_ModalTypes,                 turnOn,  Opt_RebindableSyntax)
+    , (Opt_ModalTypes,                 turnOff, Opt_MonomorphismRestriction)
+
     , (Opt_RebindableSyntax, turnOff, Opt_ImplicitPrelude)      -- NB: turn off!
 
     , (Opt_GADTs,            turnOn, Opt_GADTSyntax)
@@ -1870,18 +1901,20 @@ foreign import ccall unsafe "rts_isProfiled" rtsIsProfiledIO :: IO CInt
 
 rtsIsProfiled :: Bool
 rtsIsProfiled = unsafePerformIO rtsIsProfiledIO /= 0
+#endif
 
 checkTemplateHaskellOk :: Bool -> DynP ()
-checkTemplateHaskellOk turn_on 
+#ifdef GHCI
+checkTemplateHaskellOk turn_on
   | turn_on && rtsIsProfiled
   = addErr "You can't use Template Haskell with a profiled compiler"
   | otherwise
   = return ()
 #else
--- In stage 1 we don't know that the RTS has rts_isProfiled, 
+-- In stage 1 we don't know that the RTS has rts_isProfiled,
 -- so we simply say "ok".  It doesn't matter because TH isn't
 -- available in stage 1 anyway.
-checkTemplateHaskellOk turn_on = return ()
+checkTemplateHaskellOk _ = return ()
 #endif
 
 {- **********************************************************************
@@ -2190,7 +2223,7 @@ setOptHpcDir arg  = upd $ \ d -> d{hpcDir = arg}
 -- platform.
 
 machdepCCOpts :: DynFlags -> [String] -- flags for all C compilations
-machdepCCOpts dflags = cCcOpts ++ machdepCCOpts'
+machdepCCOpts _ = cCcOpts ++ machdepCCOpts'
 
 machdepCCOpts' :: [String] -- flags for all C compilations
 machdepCCOpts'