diff --git a/kore/app/parser/Main.hs b/kore/app/parser/Main.hs index a16e8bbadc..33c3632546 100644 --- a/kore/app/parser/Main.hs +++ b/kore/app/parser/Main.hs @@ -8,23 +8,6 @@ import Control.Monad.Catch , handle ) import qualified Data.Map.Strict as Map -import Data.Text - ( Text - ) -import Options.Applicative - ( InfoMod - , Parser - , argument - , fullDesc - , header - , help - , long - , metavar - , progDesc - , str - , strOption - , value - ) import Kore.AST.ApplicativeKore import Kore.ASTVerifier.DefinitionVerifier @@ -46,6 +29,7 @@ import qualified Kore.Log as Log import Kore.Log.ErrorVerify ( errorVerify ) +import Kore.Options import Kore.Parser ( parseKoreDefinition , parseKorePattern @@ -65,57 +49,6 @@ Main module to run kore-parser TODO: add command line argument tab-completion -} --- | Main options record -data KoreParserOptions = KoreParserOptions - { fileName :: !FilePath - -- ^ Name for a file containing a definition to parse and verify - , patternFileName :: !FilePath - -- ^ Name for file containing a pattern to parse and verify - , mainModuleName :: !Text - -- ^ the name of the main module in the definition - , willPrintDefinition :: !Bool - -- ^ Option to print definition - , willPrintPattern :: !Bool - -- ^ Option to print pattern - , willVerify :: !Bool - -- ^ Option to verify definition - , appKore :: !Bool - -- ^ Option to print in applicative Kore syntax - } - --- | Command Line Argument Parser -commandLineParser :: Parser KoreParserOptions -commandLineParser = - KoreParserOptions - <$> argument str - ( metavar "FILE" - <> help "Kore source file to parse [and verify]" ) - <*> strOption - ( metavar "PATTERN_FILE" - <> long "pattern" - <> help - "Kore pattern source file to parse [and verify]. Needs --module." - <> value "" ) - <*> strOption - ( metavar "MODULE" - <> long "module" - <> help "The name of the main module in the Kore definition" - <> value "" ) - <*> enableDisableFlag "print-definition" - True False True - "printing parsed definition to stdout [default enabled]" - <*> enableDisableFlag "print-pattern" - True False True - "printing parsed pattern to stdout [default enabled]" - <*> enableDisableFlag "verify" - True False True - "Verify well-formedness of parsed definition [default enabled]" - <*> enableDisableFlag "appkore" - True False False - ( "printing parsed definition in applicative Kore syntax " - ++ "[default disabled]" - ) - -- | modifiers for the Command line parser description parserInfoModifiers :: InfoMod options parserInfoModifiers = @@ -144,7 +77,7 @@ main = handleTop $ do mainGlobal (ExeName "kore-parser") Nothing -- environment variable name for extra arguments - commandLineParser + parseKoreParserOptions parserInfoModifiers for_ (localOptions options) $ \koreParserOptions -> flip runLoggerT Log.emptyLogger $ do @@ -164,11 +97,12 @@ main = handleTop $ do $ toVerifiedDefinition indexedModules else putDoc (debug parsedDefinition) - let KoreParserOptions { patternFileName } = koreParserOptions - unless (null patternFileName) $ do + let KoreParserOptions { patternOpt } = koreParserOptions + for_ patternOpt $ \patternOptions -> do + let PatternOptions { patternFileName } = patternOptions parsedPattern <- mainPatternParse patternFileName when willVerify $ do - let KoreParserOptions { mainModuleName } = koreParserOptions + let PatternOptions { mainModuleName } = patternOptions indexedModule <- lookupMainModule (ModuleName mainModuleName) @@ -176,7 +110,8 @@ main = handleTop $ do & lift _ <- mainPatternVerify indexedModule parsedPattern return () - let KoreParserOptions { willPrintPattern } = koreParserOptions + let KoreParserOptions { willPrintPattern } = + koreParserOptions when willPrintPattern $ lift $ putDoc (debug parsedPattern) diff --git a/kore/app/share/GlobalMain.hs b/kore/app/share/GlobalMain.hs index e01139538f..3b622b93cf 100644 --- a/kore/app/share/GlobalMain.hs +++ b/kore/app/share/GlobalMain.hs @@ -10,7 +10,6 @@ module GlobalMain , parseKoreProveOptions , parseKoreMergeOptions , mainGlobal - , enableDisableFlag , clockSomething , clockSomethingIO , mainPatternVerify @@ -76,13 +75,10 @@ import Options.Applicative , defaultPrefs , execParserPure , flag - , flag' , handleParseResult , help , helper - , hidden , info - , internal , long , maybeReader , metavar @@ -385,36 +381,6 @@ commandLineParse (ExeName exeName) maybeEnv parser infoMod = do ---------------------- -- Helper Functions -- -{-| -Parser builder to create an optional boolean flag, -with an enabled, disabled and default value. -Based on `enableDisableFlagNoDefault` -from commercialhaskell/stack: -https://github.com/commercialhaskell/stack/blob/master/src/Options/Applicative/Builder/Extra.hs --} -enableDisableFlag - :: String -- ^ flag name - -> option -- ^ enabled value - -> option -- ^ disabled value - -> option -- ^ default value - -> String -- ^ Help text suffix; appended to "Enable/disable " - -> Parser option -enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix = - flag' enabledVal - ( hidden - <> internal - <> long name - <> help helpSuffix) - <|> flag' disabledVal - ( hidden - <> internal - <> long ("no-" ++ name) - <> help helpSuffix ) - <|> flag' disabledVal - ( long ( "[no-]" ++ name ) - <> help ( "Enable/disable " ++ helpSuffix ) ) - <|> pure defaultVal - -- | Time a pure computation and print results. clockSomething :: String -> a -> Main a diff --git a/kore/kore.cabal b/kore/kore.cabal index db1c018bbd..7acdf5ed59 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -222,6 +222,7 @@ library Kore.ModelChecker.Bounded Kore.ModelChecker.Simplification Kore.ModelChecker.Step + Kore.Options Kore.Parser Kore.Parser.CString Kore.Parser.Lexer @@ -954,6 +955,7 @@ test-suite kore-test Test.Kore.Log.ErrorBottomTotalFunction Test.Kore.Log.WarnFunctionWithoutEvaluators Test.Kore.Log.WarnSymbolSMTRepresentation + Test.Kore.Options Test.Kore.Parser Test.Kore.Parser.Lexer Test.Kore.Parser.Parser diff --git a/kore/src/Kore/Options.hs b/kore/src/Kore/Options.hs new file mode 100644 index 0000000000..fcb7447e29 --- /dev/null +++ b/kore/src/Kore/Options.hs @@ -0,0 +1,110 @@ +{- | +Copyright : (c) Runtime Verification, 2020 +License : NCSA + +-} + +module Kore.Options + ( module Options.Applicative + , enableDisableFlag + , PatternOptions (..) + , KoreParserOptions (..) + , parseKoreParserOptions + ) where + +import Prelude.Kore + +import Data.Text + ( Text + ) + +import Options.Applicative + +{-| +Parser builder to create an optional boolean flag, +with an enabled, disabled and default value. +Based on `enableDisableFlagNoDefault` +from commercialhaskell/stack: +https://github.com/commercialhaskell/stack/blob/master/src/Options/Applicative/Builder/Extra.hs +-} +enableDisableFlag + :: String -- ^ flag name + -> option -- ^ enabled value + -> option -- ^ disabled value + -> option -- ^ default value + -> String -- ^ Help text suffix; appended to "Enable/disable " + -> Parser option +enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix = + flag' enabledVal + ( hidden + <> internal + <> long name + <> help helpSuffix) + <|> flag' disabledVal + ( hidden + <> internal + <> long ("no-" ++ name) + <> help helpSuffix ) + <|> flag' disabledVal + ( long ( "[no-]" ++ name ) + <> help ( "Enable/disable " ++ helpSuffix ) ) + <|> pure defaultVal + +{- | Options for parsing and verifying a pattern. + -} +data PatternOptions = PatternOptions + { patternFileName :: !FilePath + -- ^ name of file containing a pattern to parse and verify + , mainModuleName :: !Text + -- ^ the name of the main module in the definition + } + +-- | Main options record +data KoreParserOptions = KoreParserOptions + { fileName :: !FilePath + -- ^ Name for a file containing a definition to parse and verify + , patternOpt :: !(Maybe PatternOptions) + -- ^ Optionally, parse and verify a pattern relative to the definition. + , willPrintDefinition :: !Bool + -- ^ Option to print definition + , willPrintPattern :: !Bool + -- ^ Option to print pattern + , willVerify :: !Bool + -- ^ Option to verify definition + , appKore :: !Bool + -- ^ Option to print in applicative Kore syntax + } + +parsePatternOptions :: Parser PatternOptions +parsePatternOptions = PatternOptions + <$> strOption + ( metavar "PATTERN_FILE" + <> long "pattern" + <> help "Kore pattern source file to parse [and verify]. Needs --module.") + <*> strOption + ( metavar "MODULE" + <> long "module" + <> help "The name of the main module in the Kore definition") + +-- | Command Line Argument Parser +parseKoreParserOptions :: Parser KoreParserOptions +parseKoreParserOptions = + KoreParserOptions + <$> argument str + ( metavar "FILE" + <> help "Kore source file to parse [and verify]" ) + <*> optional parsePatternOptions + <*> enableDisableFlag "print-definition" + True False False + "printing parsed definition to stdout [default disabled]" + <*> enableDisableFlag "print-pattern" + True False False + "printing parsed pattern to stdout [default disabled]" + <*> enableDisableFlag "verify" + True False True + "Verify well-formedness of parsed definition [default enabled]" + <*> enableDisableFlag "appkore" + True False False + ( "printing parsed definition in applicative Kore syntax " + ++ "[default disabled]" + ) diff --git a/kore/test/Test/Kore/Options.hs b/kore/test/Test/Kore/Options.hs new file mode 100644 index 0000000000..ad146d2acb --- /dev/null +++ b/kore/test/Test/Kore/Options.hs @@ -0,0 +1,84 @@ +module Test.Kore.Options + ( test_flags + , test_options + ) where + +import Prelude.Kore + +import Data.Maybe + ( fromJust + ) + +import Test.Tasty +import Test.Tasty.HUnit.Ext + +import Kore.Options + +test_flags :: [TestTree] +test_flags = + [ testGroup "print-definition" + [ testCase "default is False" $ do + let flagValue = willPrintDefinition $ runParser parseKoreParserOptions + ["mock/path/to/def"] + assertEqual "Expected print-definition to be False by default" + False flagValue + , testCase "given explicitly is True" $ do + let flagValue = willPrintDefinition $ runParser parseKoreParserOptions + ["mock/path/to/def", "--print-definition"] + assertEqual "Expected --print-definition to give True" + True flagValue + , testCase "with `no` prefix is False" $ do + let flagValue = willPrintDefinition $ runParser parseKoreParserOptions + ["mock/path/to/def", "--no-print-definition"] + assertEqual "Expected --no-print-definition to give False" + False flagValue + ] + , testGroup "print-pattern" + [ testCase "default is False" $ do + let flagValue = willPrintPattern $ runParser parseKoreParserOptions + ["mock/path/to/def"] + assertEqual "Expected print-pattern to be False by default" + False flagValue + , testCase "given explicitly is True" $ do + let flagValue = willPrintPattern $ runParser parseKoreParserOptions + ["mock/path/to/def", "--print-pattern"] + assertEqual "Expected --print-pattern to give True" + True flagValue + , testCase "with `no` prefix is False" $ do + let flagValue = willPrintPattern $ runParser parseKoreParserOptions + ["mock/path/to/def", "--no-print-pattern"] + assertEqual "Expected --no-print-pattern to give False" + False flagValue + ] + ] + +test_options :: [TestTree] +test_options = + [ testGroup "pattern and module must go together" + [ testCase "pattern only" $ do + let result = runParser' parseKoreParserOptions + ["mock/path/to/def", "--pattern", "mock/path/to/pat"] + assertBool "Expected passing only the pattern option to fail" + $ isNothing result + , testCase "module only" $ do + let result = runParser' parseKoreParserOptions + ["mock/path/to/def", "--module", "mock_module"] + assertBool "Expected passing only the module option to fail" + $ isNothing result + , testCase "pattern and module" $ do + let result = runParser' parseKoreParserOptions + ["mock/path/to/def", "--pattern", "mock/path/to/pat" + , "--module", "mock_module"] + assertBool "Expected passing both pattern and module options to not fail" + $ isJust result + ] + ] + +runParser' :: Parser a -> [String] -> Maybe a +runParser' parser input = getParseResult parserResult + where + parserInfo = info parser mempty + parserResult = execParserPure defaultPrefs parserInfo input + +runParser :: Parser a -> [String] -> a +runParser parser input = fromJust $ runParser' parser input