{-# LANGUAGE TupleSections #-}

module Options
    (InputFormat(..),OutputFormat(..),RefinementType(..),
     Options(..),startOptions,options,parseArgs,
     usageInformation)
where

import Control.Applicative ((<$>))
import System.Console.GetOpt
import System.Environment (getArgs)

import Property (Property(..))

data InputFormat = InPP deriving (Read)
data OutputFormat = OutDOT deriving (Read)

instance Show InputFormat where
        show InPP = "PP"
instance Show OutputFormat where
        show OutDOT = "DOT"

data RefinementType = TrapRefinement
                    | SiphonRefinement
                    | UTrapRefinement
                    | USiphonRefinement
                    deriving (Show,Read)

data Options = Options { inputFormat :: InputFormat
                       , optVerbosity :: Int
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
                       , optProperties :: [Property]
                       , optRefinementType :: Maybe [RefinementType]
                       , optMinimizeRefinement :: Int
                       , optSMTAuto :: Bool
                       , optInvariant :: Bool
                       , optOutput :: Maybe String
                       , outputFormat :: OutputFormat
                       , optUseProperties :: Bool
                       , optPrintStructure :: Bool
                       }

startOptions :: Options
startOptions = Options { inputFormat = InPP
                       , optVerbosity = 1
                       , optShowHelp = False
                       , optShowVersion = False
                       , optProperties = []
                       , optRefinementType = Just [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
                       , optMinimizeRefinement = 0
                       , optSMTAuto = True
                       , optInvariant = False
                       , optOutput = Nothing
                       , outputFormat = OutDOT
                       , optUseProperties = True
                       , optPrintStructure = False
                       }

options :: [ OptDescr (Options -> Either String Options) ]
options =
        [ Option "" ["layered-termination"]
        (NoArg (\opt -> Right opt {
                   optProperties = optProperties opt ++ [LayeredTermination]
               }))
        "Prove that the protocol satisfies layered termination"

        , Option "" ["strong-consensus"]
        (NoArg (\opt -> Right opt {
                   optProperties = optProperties opt ++ [StrongConsensus]
               }))
        "Prove that the protocol satisfies strong consensus"

        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

        , Option "r" ["refinement"]
        (ReqArg (\arg opt ->
                    let addRef ref =
                            Right opt { optRefinementType =
                                    case optRefinementType opt of
                                       Nothing -> Just [ref]
                                       Just(refs) -> Just (refs ++ [ref])

                            }
                    in case arg of
                                "trap" -> addRef TrapRefinement
                                "siphon" -> addRef SiphonRefinement
                                "utrap" -> addRef UTrapRefinement
                                "usiphon" -> addRef USiphonRefinement
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
                )
                "METHOD")
        ("Refine with METHOD (trap, siphon, utrap, usiphon)")

        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "Print structural information"


        , Option "" ["in-pp"]
        (NoArg (\opt -> Right opt { inputFormat = InPP }))
        "Use the population protocol input format"


        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
        "Write population protocol to FILE"

        , Option "" ["out-dot"]
        (NoArg (\opt -> Right opt { outputFormat = OutDOT }))
        "Use the dot output format"

        , Option "m" ["minimize"]
        (ReqArg (\arg opt -> case reads arg of
                        [(i, "")] -> Right opt { optMinimizeRefinement = i }
                        _ -> Left ("invalid argument for minimization method: " ++ arg)
                )
                "METHOD")
        "Minimize size of refinement structure by method METHOD (1-4)"

        , Option "" ["smt-disable-auto-config"]
        (NoArg (\opt -> Right opt { optSMTAuto = False }))
        "Disable automatic configuration of the SMT solver"

        , Option "v" ["verbose"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
        "Increase verbosity (may be specified more than once)"

        , Option "q" ["quiet"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt - 1 }))
        "Decrease verbosity (may be specified more than once)"

        , Option "V" ["version"]
        (NoArg (\opt -> Right opt { optShowVersion = True }))
        "Show version"

        , Option "h" ["help"]
        (NoArg (\opt -> Right opt { optShowHelp = True }))
        "Show help"
        ]

parseArgs :: IO (Either String (Options, [String]))
parseArgs = do
        args <- getArgs
        case getOpt Permute options args of
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

usageInformation :: String
usageInformation = usageInfo "Peregrine" options