{-|
Module      : Idris.Options
Description : Compiler options for Idris.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveGeneric, PatternGuards #-}

module Idris.Options (Codegen(..), ConsoleWidth(..), HowMuchDocs(..), IRFormat(..),
                      LanguageExt(..), LogCat(..), Opt(..), Optimisation(..),
                      OutputFmt(..), REPLPort(..), codegenCats, elabCats, getBC,
                      getClient, getCodegen, getCodegenArgs, getColour, getConsoleWidth,
                      getEvalExpr, getExecScript, getFile, getIBCSubDir, getImportDir,
                      getLanguageExt, getOptLevel, getOptimisation, getOutput,
                      getOutputTy, getPkg, getPkgCheck, getPkgClean, getPkgDir,
                      getPkgIndex, getPkgMkDoc, getPkgREPL, getPkgTest, getPort,
                      getSourceDir, loggingCatsStr, opt, parserCats, strLogCat) where

import Data.Maybe
import GHC.Generics (Generic)
import IRTS.CodegenCommon (OutputType)
import Network.Socket (PortNumber)

data Opt = Filename String
         | Quiet
         | NoBanner
         | ColourREPL Bool
         | Idemode
         | IdemodeSocket
         | IndentWith Int
         | IndentClause Int
         | ShowAll
         | ShowLibs
         | ShowLibDir
         | ShowDocDir
         | ShowIncs
         | ShowPkgs
         | ShowLoggingCats
         | NoBasePkgs
         | NoPrelude
         | NoBuiltins -- only for the really primitive stuff!
         | NoREPL
         | OLogging Int
         | OLogCats [LogCat]
         | Output String
         | Interface
         | TypeCase
         | TypeInType
         | DefaultTotal
         | DefaultPartial
         | WarnPartial
         | WarnReach
         | AuditIPkg
         | EvalTypes
         | NoCoverage
         | ErrContext
         | ShowImpl
         | Verbose Int
         | Port REPLPort -- ^ REPL TCP port
         | IBCSubDir String
         | ImportDir String
         | SourceDir String
         | PkgBuild String
         | PkgInstall String
         | PkgClean String
         | PkgCheck String
         | PkgREPL String
         | PkgDocBuild String -- IdrisDoc
         | PkgDocInstall String
         | PkgTest String
         | PkgIndex FilePath
         | WarnOnly
         | Pkg String
         | BCAsm String
         | DumpDefun String
         | DumpCases String
         | UseCodegen Codegen
         | CodegenArgs String
         | OutputTy OutputType
         | Extension LanguageExt
         | InterpretScript String
         | EvalExpr String
         | TargetTriple String
         | TargetCPU String
         | OptLevel Int
         | AddOpt Optimisation
         | RemoveOpt Optimisation
         | Client String
         | ShowOrigErr
         | AutoWidth -- ^ Automatically adjust terminal width
         | AutoSolve -- ^ Automatically issue "solve" tactic in old-style interactive prover
         | UseConsoleWidth ConsoleWidth
         | DumpHighlights
         | DesugarNats
         | NoElimDeprecationWarnings      -- ^ Don't show deprecation warnings for %elim
         | NoOldTacticDeprecationWarnings -- ^ Don't show deprecation warnings for old-style tactics
    deriving (Show, Eq, Generic)


data REPLPort = DontListen | ListenPort PortNumber
  deriving (Eq, Generic, Show)


data Codegen = Via IRFormat String
             | Bytecode
    deriving (Show, Eq, Generic)


data LanguageExt = TypeProviders | ErrorReflection | UniquenessTypes
                 | DSLNotation   | ElabReflection  | FCReflection
                 | LinearTypes
  deriving (Show, Eq, Read, Ord, Generic)

data IRFormat = IBCFormat | JSONFormat deriving (Show, Eq, Generic)


-- | How wide is the console?
data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines should not be broken
                  | ColsWide Int   -- ^ Manually specified - must be positive
                  | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise
   deriving (Show, Eq, Generic)

data HowMuchDocs = FullDocs | OverviewDocs

data OutputFmt = HTMLOutput | LaTeXOutput

data Optimisation = PETransform -- ^ partial eval and associated transforms
  deriving (Show, Eq, Generic)

-- | Recognised logging categories for the Idris compiler.
--
-- @TODO add in sub categories.
data LogCat = IParse
            | IElab
            | ICodeGen
            | IErasure
            | ICoverage
            | IIBC
            deriving (Show, Eq, Ord, Generic)

strLogCat :: LogCat -> String
strLogCat IParse    = "parser"
strLogCat IElab     = "elab"
strLogCat ICodeGen  = "codegen"
strLogCat IErasure  = "erasure"
strLogCat ICoverage = "coverage"
strLogCat IIBC      = "ibc"

codegenCats :: [LogCat]
codegenCats =  [ICodeGen]

parserCats :: [LogCat]
parserCats = [IParse]

elabCats :: [LogCat]
elabCats = [IElab]

loggingCatsStr :: String
loggingCatsStr = unlines
    [ (strLogCat IParse)
    , (strLogCat IElab)
    , (strLogCat ICodeGen)
    , (strLogCat IErasure)
    , (strLogCat ICoverage)
    , (strLogCat IIBC)
    ]

getFile :: Opt -> Maybe String
getFile (Filename s) = Just s
getFile _ = Nothing

getBC :: Opt -> Maybe String
getBC (BCAsm s) = Just s
getBC _ = Nothing

getOutput :: Opt -> Maybe String
getOutput (Output s) = Just s
getOutput _ = Nothing

getIBCSubDir :: Opt -> Maybe String
getIBCSubDir (IBCSubDir s) = Just s
getIBCSubDir _ = Nothing

getImportDir :: Opt -> Maybe String
getImportDir (ImportDir s) = Just s
getImportDir _ = Nothing

getSourceDir :: Opt -> Maybe String
getSourceDir (SourceDir s) = Just s
getSourceDir _ = Nothing

getPkgDir :: Opt -> Maybe String
getPkgDir (Pkg s) = Just s
getPkgDir _ = Nothing

getPkg :: Opt -> Maybe (Bool, String)
getPkg (PkgBuild s)   = Just (False, s)
getPkg (PkgInstall s) = Just (True, s)
getPkg _ = Nothing

getPkgClean :: Opt -> Maybe String
getPkgClean (PkgClean s) = Just s
getPkgClean _ = Nothing

getPkgREPL :: Opt -> Maybe String
getPkgREPL (PkgREPL s) = Just s
getPkgREPL _ = Nothing

getPkgCheck :: Opt -> Maybe String
getPkgCheck (PkgCheck s) = Just s
getPkgCheck _              = Nothing

-- | Returns None if given an Opt which is not PkgMkDoc
--   Otherwise returns Just x, where x is the contents of PkgMkDoc
getPkgMkDoc :: Opt                  -- ^ Opt to extract
            -> Maybe (Bool, String) -- ^ Result
getPkgMkDoc (PkgDocBuild  str)  = Just (False,str)
getPkgMkDoc (PkgDocInstall str) = Just (True,str)
getPkgMkDoc _              = Nothing

getPkgTest :: Opt          -- ^ the option to extract
           -> Maybe String -- ^ the package file to test
getPkgTest (PkgTest f) = Just f
getPkgTest _ = Nothing

getCodegen :: Opt -> Maybe Codegen
getCodegen (UseCodegen x) = Just x
getCodegen _ = Nothing

getCodegenArgs :: Opt -> Maybe String
getCodegenArgs (CodegenArgs args) = Just args
getCodegenArgs _ = Nothing

getConsoleWidth :: Opt -> Maybe ConsoleWidth
getConsoleWidth (UseConsoleWidth x) = Just x
getConsoleWidth _ = Nothing

getExecScript :: Opt -> Maybe String
getExecScript (InterpretScript expr) = Just expr
getExecScript _ = Nothing

getPkgIndex :: Opt -> Maybe FilePath
getPkgIndex (PkgIndex file) = Just file
getPkgIndex _ = Nothing

getEvalExpr :: Opt -> Maybe String
getEvalExpr (EvalExpr expr) = Just expr
getEvalExpr _ = Nothing

getOutputTy :: Opt -> Maybe OutputType
getOutputTy (OutputTy t) = Just t
getOutputTy _ = Nothing

getLanguageExt :: Opt -> Maybe LanguageExt
getLanguageExt (Extension e) = Just e
getLanguageExt _ = Nothing

getTriple :: Opt -> Maybe String
getTriple (TargetTriple x) = Just x
getTriple _ = Nothing

getCPU :: Opt -> Maybe String
getCPU (TargetCPU x) = Just x
getCPU _ = Nothing

getOptLevel :: Opt -> Maybe Int
getOptLevel (OptLevel x) = Just x
getOptLevel _ = Nothing

getOptimisation :: Opt -> Maybe (Bool,Optimisation)
getOptimisation (AddOpt p)    = Just (True,  p)
getOptimisation (RemoveOpt p) = Just (False, p)
getOptimisation _             = Nothing

getColour :: Opt -> Maybe Bool
getColour (ColourREPL b) = Just b
getColour _ = Nothing

getClient :: Opt -> Maybe String
getClient (Client x) = Just x
getClient _ = Nothing

-- Get the first valid port
getPort :: [Opt] -> Maybe REPLPort
getPort []            = Nothing
getPort (Port p : _ ) = Just p
getPort (_      : xs) = getPort xs

opt :: (Opt -> Maybe a) -> [Opt] -> [a]
opt = mapMaybe