-
Notifications
You must be signed in to change notification settings - Fork 44
kore-parser: Make --no-print-definition and --no-print-pattern default and make --module and --pattern mandatory to go together #2273
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
14 commits
Select commit
Hold shift + click to select a range
fcd6940
changed the dafault state of print-definition and print-pattern of th…
MirceaS a1f4525
Moved option parser code to the library and added unit tests for it
MirceaS bba3857
Added module header documentation
MirceaS 630ba49
kore-parser options pattern and module must now go together
MirceaS c4e388d
added unit tests for issue #2254
MirceaS 4c7c1db
updated code so that it uses new options type
MirceaS e2834fb
addressed PR comments
MirceaS 5210885
Merge branch 'master' into 2264
MirceaS 20b2de5
updated kore.cabal file
MirceaS ba1107c
Kore.Options: Sort imports
ttuegel 526d48f
Kore.Options.PatternOptions: Documentation
ttuegel 6e7b7bc
Kore.Options.PatternOptions: Documentation
ttuegel c2253c7
Kore.Options.KoreParserOptions: Documentation
ttuegel e4d10d9
Merge branch 'master' into 2264
ttuegel File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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]" | ||
| ) | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.