module Tip.Params where
import Options.Applicative
import Tip.Utils
import Data.List.Split
data Params = Params
{ include :: [FilePath]
, debug_flags :: [DebugFlag]
, prop_names :: Maybe [String]
, extra_names :: [String]
}
deriving Show
commaSep :: [String] -> [String]
commaSep = concatMap (splitOn ",")
parseParams :: Parser Params
parseParams = Params
<$> many (strOption (long "include" <> short 'i' <> metavar "PATH" <> help "Extra include directory"))
<*> many (foldr (<|>) empty [ flag' debug_flag (long (flagifyShow debug_flag) <> help (debugHelp debug_flag))
| debug_flag <- [minBound..maxBound]
])
<*> (pure Nothing <|> fmap (Just . commaSep) (many (strOption prop_opt)))
<*> fmap commaSep (many (strOption (long "extra" <> short 'e' <> metavar "NAME" <> help "Function declaration to add to theory")))
where
prop_opt = long "only" <> long "prop" <> short 'p' <> metavar "NAME" <> help "Property declaration to consider (default all)"
defaultParams :: Params
defaultParams = Params
{ include = []
, debug_flags = []
, prop_names = Nothing
, extra_names = []
}
data DebugFlag = PrintCore | PrintInitialTheory
deriving (Eq,Show,Enum,Bounded)
debugHelp :: DebugFlag -> String
debugHelp PrintCore = "Print core bindings from GHC"
debugHelp PrintInitialTheory = "Print initial theory"