kore-parser: Make --no-print-definition and --no-print-pattern default and make --module and --pattern mandatory to go together

kore/app/parser/Main.hs

@@ -8,22 +8,11 @@ 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
@@ -46,6 +35,7 @@ import qualified Kore.Log as Log
 import Kore.Log.ErrorVerify
     ( errorVerify
     )
+import Kore.OptionsParser
 import Kore.Parser
     ( parseKoreDefinition
     , parseKorePattern
@@ -65,57 +55,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 =
@@ -164,21 +103,23 @@ main = handleTop $ do
                         $ toVerifiedDefinition indexedModules
                 else putDoc (debug parsedDefinition)
 
-            let KoreParserOptions { patternFileName } = koreParserOptions
-            unless (null patternFileName) $ do
-                parsedPattern <- mainPatternParse patternFileName
-                when willVerify $ do
-                    let KoreParserOptions { mainModuleName } = koreParserOptions
-                    indexedModule <-
-                        lookupMainModule
-                            (ModuleName mainModuleName)
-                            indexedModules
-                        & lift
-                    _ <- mainPatternVerify indexedModule parsedPattern
-                    return ()
-                let KoreParserOptions { willPrintPattern } = koreParserOptions
-                when willPrintPattern $
-                    lift $ putDoc (debug parsedPattern)
+            let KoreParserOptions { patternOpt } = koreParserOptions
+            case patternOpt of
+                Nothing -> pure ()
+                Just PatternOptions {patternFileName, mainModuleName} -> do
+                    parsedPattern <- mainPatternParse patternFileName
+                    when willVerify $ do
+                        indexedModule <-
+                            lookupMainModule
+                                (ModuleName mainModuleName)
+                                indexedModules
+                            & lift
+                        _ <- mainPatternVerify indexedModule parsedPattern
+                        return ()
+                    let KoreParserOptions { willPrintPattern } =
+                            koreParserOptions
+                    when willPrintPattern $
+                        lift $ putDoc (debug parsedPattern)
 
 -- | IO action that parses a kore definition from a filename and prints timing
 -- information.

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

kore/src/Kore/OptionsParser.hs

@@ -0,0 +1,112 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+-}
+
+module Kore.OptionsParser
+    ( enableDisableFlag
+    , PatternOptions (..)
+    , KoreParserOptions (..)
+    , commandLineParser
+    ) where
+
+import Data.Text
+    ( Text
+    )
+
+import Prelude.Kore
+
+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
+
+
+data PatternOptions = PatternOptions
+    { patternFileName     :: !FilePath
+    -- ^ Name for 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)
+    -- ^ Optional options for parsing a pattern
+    , 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]" )
+    <*> (   (Just <$>
+                (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")
+                )
+            )
+            <|> flag Nothing Nothing
+                (  long "definition-only"
+                <> help "No Kore pattern may be checked against the definition")
+        )
+    <*> 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]"
+        )

kore/test/Test/Kore/OptionsParser.hs

@@ -0,0 +1,86 @@
+module Test.Kore.OptionsParser
+    ( test_flags
+    , test_options
+    ) where
+
+import Prelude.Kore
+
+import Data.Maybe
+    ( fromJust
+    )
+
+import Test.Tasty
+import Test.Tasty.HUnit.Ext
+
+import Kore.OptionsParser
+
+import Options.Applicative
+
+test_flags :: [TestTree]
+test_flags =
+    [ testGroup "print-definition"
+        [ testCase "default is False" $ do
+            let flag_value = willPrintDefinition $ runParser commandLineParser
+                    ["mock/path/to/def"]
+            assertEqual "Expected print-definition to be False by default"
+                False flag_value
+        , testCase "given explicitly is True" $ do
+            let flag_value = willPrintDefinition $ runParser commandLineParser
+                    ["mock/path/to/def", "--print-definition"]
+            assertEqual "Expected --print-definition to give True"
+                True flag_value
+        , testCase "with `no` prefix is False" $ do
+            let flag_value = willPrintDefinition $ runParser commandLineParser
+                    ["mock/path/to/def", "--no-print-definition"]
+            assertEqual "Expected --no-print-definition to give False"
+                False flag_value
+        ]
+    , testGroup "print-pattern"
+        [ testCase "default is False" $ do
+            let flag_value = willPrintPattern $ runParser commandLineParser
+                    ["mock/path/to/def"]
+            assertEqual "Expected print-pattern to be False by default"
+                False flag_value
+        , testCase "given explicitly is True" $ do
+            let flag_value = willPrintPattern $ runParser commandLineParser
+                    ["mock/path/to/def", "--print-pattern"]
+            assertEqual "Expected --print-pattern to give True"
+                True flag_value
+        , testCase "with `no` prefix is False" $ do
+            let flag_value = willPrintPattern $ runParser commandLineParser
+                    ["mock/path/to/def", "--no-print-pattern"]
+            assertEqual "Expected --no-print-pattern to give False"
+                False flag_value
+        ]
+    ]
+
+test_options :: [TestTree]
+test_options =
+    [ testGroup "pattern and module must go together"
+        [ testCase "pattern only" $ do
+            let result = runParser' commandLineParser
+                    ["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' commandLineParser
+                    ["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' commandLineParser
+                    ["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