X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Fmain%2FDynFlags.hs;h=e5bd6771c7ff6b04abb2b7249a2725fce1221366;hb=e5c3b478b3cd1707cf122833822f44b2ac09b8e9;hp=d80d2a63943929c436f697fe1aa5154f9220c484;hpb=2d4d636af091b8da27466b5cf90011395a9c2f66;p=ghc-hetmet.git

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index d80d2a6..e5bd677 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -204,6 +204,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
@@ -274,7 +281,6 @@ data DynFlag
    -- misc opts
    | Opt_Pp
    | Opt_ForceRecomp
-   | Opt_DryRun
    | Opt_ExcessPrecision
    | Opt_EagerBlackHoling
    | Opt_ReadUserPackageConf
@@ -334,6 +340,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
@@ -645,7 +652,6 @@ data HscTarget
   = HscC           -- ^ Generate C code.
   | HscAsm         -- ^ Generate assembly using the native code generator.
   | HscLlvm        -- ^ Generate assembly using the llvm code generator.
-  | HscJava        -- ^ Generate Java bytecode.
   | HscInterpreted -- ^ Generate bytecode.  (Requires 'LinkInMemory')
   | HscNothing     -- ^ Don't generate any code.  See notes above.
   deriving (Eq, Show)
@@ -654,7 +660,6 @@ showHscTargetFlag :: HscTarget -> String
 showHscTargetFlag HscC           = "-fvia-c"
 showHscTargetFlag HscAsm         = "-fasm"
 showHscTargetFlag HscLlvm        = "-fllvm"
-showHscTargetFlag HscJava        = panic "No flag for HscJava"
 showHscTargetFlag HscInterpreted = "-fbyte-code"
 showHscTargetFlag HscNothing     = "-fno-code"
 
@@ -765,9 +770,9 @@ defaultDynFlags mySettings =
         maxSimplIterations      = 4,
         shouldDumpSimplPhase    = Nothing,
         ruleCheck               = Nothing,
-        specConstrThreshold     = Just 200,
+        specConstrThreshold     = Just 2000,
         specConstrCount         = Just 3,
-        liberateCaseThreshold   = Just 200,
+        liberateCaseThreshold   = Just 2000,
         floatLamArgs            = Just 0,	-- Default: float only if no fvs
         strictnessBefore        = [],
 
@@ -876,7 +881,11 @@ languageExtensions Nothing
       -- But NB it's implied by GADTs etc
       -- SLPJ September 2010
     : Opt_NondecreasingIndentation -- This has been on by default for some time
-    : languageExtensions (Just Haskell2010)
+    : delete Opt_DatatypeContexts  -- The Haskell' committee decided to
+                                   -- remove datatype contexts from the
+                                   -- language:
+   -- http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html
+      (languageExtensions (Just Haskell2010))
 
 languageExtensions (Just Haskell98)
     = [Opt_ImplicitPrelude,
@@ -1152,7 +1161,7 @@ allFlags = map ('-':) $
 --------------- The main flags themselves ------------------
 dynamic_flags :: [Flag (CmdLineP DynFlags)]
 dynamic_flags = [
-    Flag "n"        (NoArg (setDynFlag Opt_DryRun))
+    Flag "n"        (NoArg (addWarn "The -n flag is deprecated and no longer has any effect"))
   , Flag "cpp"      (NoArg (setExtensionFlag Opt_Cpp)) 
   , Flag "F"        (NoArg (setDynFlag Opt_Pp)) 
   , Flag "#include" 
@@ -1361,6 +1370,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"))
@@ -1662,6 +1679,7 @@ xFlags = [
     deprecatedForExtension "DoRec"),
   ( "DoRec",                            Opt_DoRec, nop ),    -- Enables 'rec' keyword 
   ( "Arrows",                           Opt_Arrows, nop ),
+  ( "ModalTypes",			Opt_ModalTypes, nop ),
   ( "ParallelArrays",                   Opt_ParallelArrays, nop ),
   ( "TemplateHaskell",                  Opt_TemplateHaskell, checkTemplateHaskellOk ),
   ( "QuasiQuotes",                      Opt_QuasiQuotes, nop ),
@@ -1757,6 +1775,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)