Options.hs

{-# LANGUAGE TupleSections #-}

module Options
    (InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
     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 RefinementOption = RefDefault
                      | RefList [RefinementType]
                      | RefAll

data Options = Options { inputFormat :: InputFormat
                       , optVerbosity :: Int
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
                       , optProperties :: [Property]
                       , optRefinementType :: RefinementOption
                       , 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 = RefDefault
                       , optMinimizeRefinement = 0
                       , optSMTAuto = True
                       , optInvariant = False
                       , optOutput = Nothing
                       , outputFormat = OutDOT
                       , optUseProperties = True
                       , optPrintStructure = False
                       }

defaultOptions :: Options
defaultOptions = startOptions{ optProperties = [LayeredTermination, StrongConsensus] }

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 =
                            case optRefinementType opt of
                               RefDefault -> RefList [ref]
                               (RefList refs) -> RefList (refs ++ [ref])
                               RefAll -> RefAll
                    in case arg of
                                "none" -> Right opt { optRefinementType = RefList [] }
                                "trap" -> Right opt { optRefinementType = addRef TrapRefinement }
                                "siphon" -> Right opt { optRefinementType = addRef SiphonRefinement }
                                "utrap" -> Right opt { optRefinementType = addRef UTrapRefinement }
                                "usiphon" -> Right opt { optRefinementType = addRef USiphonRefinement }
                                "all" -> Right opt { optRefinementType = RefAll }
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
                )
                "METHOD")
        ("Refine with METHOD (trap, siphon, utrap, usiphon, none, all)")

        , 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
            ([], files, []) ->
                return $ (,files) <$> (return defaultOptions)
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

usageInformation :: String
usageInformation =
        usageInfo ("Usage: peregrine [OPTIONS] FILE\n") options