{-# LANGUAGE CPP #-}

module Agda.Interaction.Options
    ( CommandLineOptions(..)
    , Flag
    , checkOpts
    , parseStandardOptions
    , parsePragmaOptions
    , parsePluginOptions
    , defaultOptions
    , standardOptions_
    , isLiterate
    , mapFlag
    , usage
    , tests
    ) where

import Control.Monad.Error	( MonadError(catchError) )
import Data.List		( isSuffixOf )
import System.Console.GetOpt	(getOpt, usageInfo, ArgOrder(ReturnInOrder)
				, OptDescr(..), ArgDescr(..)
				)
import Agda.Utils.TestHelpers   ( runTests )
import Agda.Utils.QuickCheck    ( quickCheck' )
import Agda.Utils.Monad		( readM )
import Agda.Utils.FileName		( slash )
import Agda.Utils.List               ( wordsBy )
import Agda.Utils.Trie               ( Trie )
import qualified Agda.Utils.Trie as Trie

-- | This should probably go somewhere else.
isLiterate :: FilePath -> Bool
isLiterate file = ".lagda" `isSuffixOf` file

-- OptDescr is a Functor --------------------------------------------------

instance Functor OptDescr where
    fmap f (Option short long arg descr) = Option short long (fmap f arg) descr

instance Functor ArgDescr where
    fmap f (NoArg x)	= NoArg (f x)
    fmap f (ReqArg p s) = ReqArg (f . p) s
    fmap f (OptArg p s) = OptArg (f . p) s

data CommandLineOptions =
    Options { optProgramName	   :: String
	    , optInputFile	   :: Maybe FilePath
	    , optIncludeDirs	   :: [FilePath]
	    , optShowVersion	   :: Bool
	    , optShowHelp	   :: Bool
	    , optInteractive	   :: Bool
	    , optVerbose	   :: Trie String Int
	    , optProofIrrelevance  :: Bool
	    , optAllowUnsolved	   :: Bool
	    , optShowImplicit	   :: Bool
	    , optRunTests	   :: Bool
	    , optCompile	   :: Bool
	    , optGenerateVimFile   :: Bool
	    , optGenerateEmacsFile :: Bool
	    , optGenerateHTML      :: Bool
	    , optHTMLDir           :: FilePath
	    , optCSSFile           :: Maybe FilePath
	    , optIgnoreInterfaces  :: Bool
	    , optDisablePositivity :: Bool
	    , optCompileAlonzo     :: Bool
            , optCompileMAlonzo    :: Bool
            , optMAlonzoDir        :: FilePath
	    , optTerminationCheck  :: Bool
	    , optCompletenessCheck :: Bool
            , optUnreachableCheck  :: Bool
	    , optUniverseCheck     :: Bool
            , optSizedTypes        :: Bool
            , optGhcFlags          :: [String]
	    }
    deriving Show

-- | Map a function over the long options. Also removes the short options.
--   Will be used to add the plugin name to the plugin options.
mapFlag :: (String -> String) -> OptDescr a -> OptDescr a
mapFlag f (Option _ long arg descr) = Option [] (map f long) arg descr

defaultOptions :: CommandLineOptions
defaultOptions =
    Options { optProgramName	   = "agda"
	    , optInputFile	   = Nothing
	    , optIncludeDirs	   = []
	    , optShowVersion	   = False
	    , optShowHelp	   = False
	    , optInteractive	   = False
	    , optVerbose	   = Trie.singleton [] 1
	    , optProofIrrelevance  = False
	    , optAllowUnsolved	   = False
	    , optShowImplicit	   = False
	    , optRunTests	   = False
	    , optCompile	   = False
	    , optGenerateVimFile   = False
	    , optGenerateEmacsFile = False
	    , optGenerateHTML      = False
	    , optHTMLDir           = defaultHTMLDir
	    , optCSSFile           = Nothing
	    , optIgnoreInterfaces  = False
	    , optDisablePositivity = False
	    , optCompileAlonzo     = False
	    , optCompileMAlonzo    = False
            , optMAlonzoDir        = defaultMAlonzoDir
            , optTerminationCheck  = True
            , optCompletenessCheck = True
            , optUnreachableCheck  = True
            , optUniverseCheck     = True
            , optSizedTypes        = False
            , optGhcFlags          = []
	    }

-- | The default output directory for MAlonzo.

defaultMAlonzoDir = "."

-- | The default output directory for HTML.

defaultHTMLDir = "html"

prop_defaultOptions = case checkOpts defaultOptions of
  Left  _ -> False
  Right _ -> True

{- | @f :: Flag opts@  is an action on the option record that results from
     parsing an option.  @f opts@ produces either an error message or an
     updated options record
-}
type Flag opts	= opts -> Either String opts

-- | Checks that the given options are consistent.

checkOpts :: Flag CommandLineOptions
checkOpts opts
  | not (atMostOne compilerOpts) =
    Left "At most one compiler may be used.\n"
  | optAllowUnsolved opts && or compilerOpts = Left
      "Unsolved meta variables are not allowed when compiling.\n"
  | not (atMostOne [or compilerOpts, optInteractive opts]) =
      Left "Choose at most one: compiler or interactive mode.\n"
  | not (atMostOne [optGenerateHTML opts, optInteractive opts]) =
      Left "Choose at most one: HTML generator or interactive mode.\n"
  | otherwise = Right opts
  where
  atMostOne bs = length (filter id bs) <= 1

  compilerOpts =
    map ($ opts)
      [ optCompile
      , optCompileAlonzo
      , optCompileMAlonzo
      ]

inputFlag :: FilePath -> CommandLineOptions -> Either String CommandLineOptions
inputFlag f o	    =
    case optInputFile o of
	Nothing  -> checkOpts $ o { optInputFile = Just f }
	Just _	 -> fail "only one input file allowed"

versionFlag               o = checkOpts $ o { optShowVersion       = True }
helpFlag                  o = checkOpts $ o { optShowHelp	       = True }
proofIrrelevanceFlag      o = checkOpts $ o { optProofIrrelevance  = True }
ignoreInterfacesFlag      o = checkOpts $ o { optIgnoreInterfaces  = True }
allowUnsolvedFlag         o = checkOpts $ o { optAllowUnsolved     = True }
showImplicitFlag          o = checkOpts $ o { optShowImplicit      = True }
runTestsFlag              o = checkOpts $ o { optRunTests	       = True }
vimFlag                   o = checkOpts $ o { optGenerateVimFile   = True }
emacsFlag                 o = checkOpts $ o { optGenerateEmacsFile = True }
noPositivityFlag          o = checkOpts $ o { optDisablePositivity = True }
dontTerminationCheckFlag  o = checkOpts $ o { optTerminationCheck  = False }
dontCompletenessCheckFlag o = checkOpts $ o { optCompletenessCheck = False }
noUnreachableCheckFlag    o = checkOpts $ o { optUnreachableCheck  = False }
dontUniverseCheckFlag     o = checkOpts $ o { optUniverseCheck     = False }
sizedTypes                o = checkOpts $ o { optSizedTypes        = True }

interactiveFlag o = checkOpts $ o { optInteractive   = True
			          , optAllowUnsolved = True
			          }
compileFlag      o = checkOpts $ o { optCompileMAlonzo = True }
agateFlag        o = checkOpts $ o { optCompile        = True }
alonzoFlag       o = checkOpts $ o { optCompileAlonzo  = True }
malonzoFlag      o = checkOpts $ o { optCompileMAlonzo = True }
malonzoDirFlag f o = checkOpts $ o { optMAlonzoDir     = f }
ghcFlag        f o = checkOpts $ o { optGhcFlags       = f : optGhcFlags o }

htmlFlag      o = checkOpts $ o { optGenerateHTML = True }
htmlDirFlag d o = checkOpts $ o { optHTMLDir      = d }
cssFlag     f o = checkOpts $ o { optCSSFile      = Just f }

includeFlag d o	    = checkOpts $ o { optIncludeDirs   = d : optIncludeDirs o   }
verboseFlag s o	    =
    do	(k,n) <- parseVerbose s
	checkOpts $ o { optVerbose = Trie.insert k n $ optVerbose o }
  where
    parseVerbose s = case wordsBy (`elem` ":.") s of
      []  -> usage
      ss  -> do
        n <- readM (last ss) `catchError` \_ -> usage
        return (init ss, n)
    usage = fail "argument to verbose should be on the form x.y.z:N or N"

integerArgument :: String -> String -> Either String Int
integerArgument flag s =
    readM s `catchError` \_ ->
	fail $ "option '" ++ flag ++ "' requires an integer argument"

standardOptions :: [OptDescr (Flag CommandLineOptions)]
standardOptions =
    [ Option ['V']  ["version"]	(NoArg versionFlag) "show version number"
    , Option ['?']  ["help"]	(NoArg helpFlag)    "show this help"
    , Option ['I']  ["interactive"] (NoArg interactiveFlag)
		    "start in interactive mode"
    , Option ['c']  ["compile"] (NoArg compileFlag)
                    "compile program (experimental)"
    , Option []	    ["agate"] (NoArg agateFlag)
		    "use the Agate compiler (only with --compile)"
    , Option []     ["alonzo"] (NoArg alonzoFlag)
		    "use the Alonzo compiler (only with --compile)"
    , Option []     ["malonzo"] (NoArg malonzoFlag)
		    "use the MAlonzo compiler (DEFAULT) (only with --compile)"
    , Option []     ["malonzo-dir"] (ReqArg malonzoDirFlag "DIR")
		    ("directory for MAlonzo output (default: " ++
                     defaultMAlonzoDir ++ ")")
    , Option []     ["ghc-flag"] (ReqArg ghcFlag "GHC-FLAG")
                    "give the flag GHC-FLAG to GHC when compiling using MAlonzo"
    , Option []	    ["test"] (NoArg runTestsFlag)
		    "run internal test suite"
    , Option []	    ["vim"] (NoArg vimFlag)
		    "generate Vim highlighting files"
    , Option []	    ["emacs"] (NoArg emacsFlag)
		    "generate Emacs highlighting files"
    , Option []	    ["html"] (NoArg htmlFlag)
		    "generate HTML files with highlighted source code"
    , Option []	    ["html-dir"] (ReqArg htmlDirFlag "DIR")
                    ("directory in which HTML files are placed (default: " ++
                     defaultHTMLDir ++ ")")
    , Option []	    ["css"] (ReqArg cssFlag "URL")
		    "the CSS file used by the HTML files (can be relative)"
    , Option []	    ["ignore-interfaces"] (NoArg ignoreInterfacesFlag)
		    "ignore interface files (re-type check everything)"
    ] ++ pragmaOptions

pragmaOptions :: [OptDescr (Flag CommandLineOptions)]
pragmaOptions =
    [ Option ['i']  ["include-path"] (ReqArg includeFlag "DIR")
		    "look for imports in DIR"
    , Option ['v']  ["verbose"]	(ReqArg verboseFlag "N")
		    "set verbosity level to N"
    , Option []	    ["show-implicit"] (NoArg showImplicitFlag)
		    "show implicit arguments when printing"
    , Option []	    ["proof-irrelevance"] (NoArg proofIrrelevanceFlag)
		    "enable proof irrelevance (experimental feature)"
    , Option []	    ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)
		    "allow unsolved meta variables (only needed in batch mode)"
    , Option []	    ["no-positivity-check"] (NoArg noPositivityFlag)
		    "do not warn about not strictly positive data types"
    , Option []	    ["no-termination-check"] (NoArg dontTerminationCheckFlag)
		    "do not warn about possibly nonterminating code"
    , Option []	    ["no-coverage-check"] (NoArg dontCompletenessCheckFlag)
		    "do not warn about possibly incomplete pattern matches"
    , Option []	    ["no-unreachable-check"] (NoArg noUnreachableCheckFlag)
		    "do not warn about unreachable function clauses"
    , Option []	    ["type-in-type"] (NoArg dontUniverseCheckFlag)
		    "ignore universe levels (this makes Agda inconsistent)"
    , Option []     ["sized-types"] (NoArg sizedTypes)
                    "use sized datatypes"
    ]

-- | Used for printing usage info.
standardOptions_ :: [OptDescr ()]
standardOptions_ = map (fmap $ const ()) standardOptions

-- | Don't export
parseOptions' ::
    String -> [String] -> opts ->
    [OptDescr (Flag opts)] -> (String -> Flag opts) -> Either String opts
parseOptions' progName argv defaults opts fileArg =
    case (getOpt (ReturnInOrder fileArg) opts argv) of
	(o,_,[])    -> foldl (>>=) (return defaults) o
	(_,_,errs)  -> fail $ concat errs

-- | Parse the standard options.
parseStandardOptions :: String -> [String] -> Either String CommandLineOptions
parseStandardOptions progName argv =
    parseOptions' progName argv defaultOptions standardOptions inputFlag

-- | Parse options from an options pragma.
parsePragmaOptions :: [String] -> CommandLineOptions -> Either String CommandLineOptions
parsePragmaOptions argv opts =
    parseOptions' progName argv opts pragmaOptions $
    \s _ -> fail $ "Bad option in pragma: " ++ s
    where
	progName = optProgramName opts

-- | Parse options for a plugin.
parsePluginOptions ::
    String -> [String] ->
    opts -> [OptDescr (Flag opts)] ->
    Either String opts
parsePluginOptions progName argv defaults opts =
    parseOptions'
	progName argv defaults opts
	(\s _ -> fail $ "Internal error: Flag " ++ s ++ " passed to a plugin")

-- | The usage info message. The argument is the program name (probably
--   agdaLight).
usage :: [OptDescr ()] -> [(String, String, [String], [OptDescr ()])] -> String -> String
usage options pluginInfos progName =
	usageInfo (header progName) options ++
	"\nPlugins:\n" ++
        indent (concatMap pluginMsg pluginInfos)

    where
	header progName = unlines [ "Agda"
				  , ""
				  , "Usage: " ++ progName ++ " [OPTIONS...] FILE"
				  ]

	indent = unlines . map ("  " ++) . lines

        pluginMsg (name, help, inherited, opts)
            | null opts && null inherited = optHeader
            | otherwise = usageInfo (optHeader ++
                                     "  Plugin-specific options:" ++
				     inheritedOptions inherited
				     ) opts
            where
		optHeader = "\n" ++ name ++ "-plugin:\n" ++ indent help
		inheritedOptions [] = ""
		inheritedOptions pls =
		    "\n    Inherits options from: " ++ unwords pls

------------------------------------------------------------------------
-- All tests

tests :: IO Bool
tests = runTests "Agda.Interaction.Options"
  [ quickCheck' prop_defaultOptions
  ]