{-# 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