Skip to content

Commit bd765b7

Browse files
MirceaSttuegel
MirceaS
and
ttuegel
authored
kore-parser: Make --no-print-definition and --no-print-pattern default and make --module and --pattern mandatory to go together (#2273)
* changed the dafault state of print-definition and print-pattern of the parser to False * Moved option parser code to the library and added unit tests for it * Added module header documentation * kore-parser options pattern and module must now go together * added unit tests for issue #2254 * updated code so that it uses new options type * addressed PR comments * updated kore.cabal file * Kore.Options: Sort imports * Kore.Options.PatternOptions: Documentation * Kore.Options.PatternOptions: Documentation * Kore.Options.KoreParserOptions: Documentation Co-authored-by: Thomas Tuegel <[email protected]>
1 parent 572827a commit bd765b7

File tree

5 files changed

+204
-107
lines changed

5 files changed

+204
-107
lines changed

‎kore/app/parser/Main.hs

Lines changed: 8 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -8,23 +8,6 @@ import Control.Monad.Catch
88
, handle
99
)
1010
import qualified Data.Map.Strict as Map
11-
import Data.Text
12-
( Text
13-
)
14-
import Options.Applicative
15-
( InfoMod
16-
, Parser
17-
, argument
18-
, fullDesc
19-
, header
20-
, help
21-
, long
22-
, metavar
23-
, progDesc
24-
, str
25-
, strOption
26-
, value
27-
)
2811

2912
import Kore.AST.ApplicativeKore
3013
import Kore.ASTVerifier.DefinitionVerifier
@@ -46,6 +29,7 @@ import qualified Kore.Log as Log
4629
import Kore.Log.ErrorVerify
4730
( errorVerify
4831
)
32+
import Kore.Options
4933
import Kore.Parser
5034
( parseKoreDefinition
5135
, parseKorePattern
@@ -65,57 +49,6 @@ Main module to run kore-parser
6549
TODO: add command line argument tab-completion
6650
-}
6751

68-
-- | Main options record
69-
data KoreParserOptions = KoreParserOptions
70-
{ fileName :: !FilePath
71-
-- ^ Name for a file containing a definition to parse and verify
72-
, patternFileName :: !FilePath
73-
-- ^ Name for file containing a pattern to parse and verify
74-
, mainModuleName :: !Text
75-
-- ^ the name of the main module in the definition
76-
, willPrintDefinition :: !Bool
77-
-- ^ Option to print definition
78-
, willPrintPattern :: !Bool
79-
-- ^ Option to print pattern
80-
, willVerify :: !Bool
81-
-- ^ Option to verify definition
82-
, appKore :: !Bool
83-
-- ^ Option to print in applicative Kore syntax
84-
}
85-
86-
-- | Command Line Argument Parser
87-
commandLineParser :: Parser KoreParserOptions
88-
commandLineParser =
89-
KoreParserOptions
90-
<$> argument str
91-
( metavar "FILE"
92-
<> help "Kore source file to parse [and verify]" )
93-
<*> strOption
94-
( metavar "PATTERN_FILE"
95-
<> long "pattern"
96-
<> help
97-
"Kore pattern source file to parse [and verify]. Needs --module."
98-
<> value "" )
99-
<*> strOption
100-
( metavar "MODULE"
101-
<> long "module"
102-
<> help "The name of the main module in the Kore definition"
103-
<> value "" )
104-
<*> enableDisableFlag "print-definition"
105-
True False True
106-
"printing parsed definition to stdout [default enabled]"
107-
<*> enableDisableFlag "print-pattern"
108-
True False True
109-
"printing parsed pattern to stdout [default enabled]"
110-
<*> enableDisableFlag "verify"
111-
True False True
112-
"Verify well-formedness of parsed definition [default enabled]"
113-
<*> enableDisableFlag "appkore"
114-
True False False
115-
( "printing parsed definition in applicative Kore syntax "
116-
++ "[default disabled]"
117-
)
118-
11952
-- | modifiers for the Command line parser description
12053
parserInfoModifiers :: InfoMod options
12154
parserInfoModifiers =
@@ -144,7 +77,7 @@ main = handleTop $ do
14477
mainGlobal
14578
(ExeName "kore-parser")
14679
Nothing -- environment variable name for extra arguments
147-
commandLineParser
80+
parseKoreParserOptions
14881
parserInfoModifiers
14982
for_ (localOptions options) $ \koreParserOptions ->
15083
flip runLoggerT Log.emptyLogger $ do
@@ -164,19 +97,21 @@ main = handleTop $ do
16497
$ toVerifiedDefinition indexedModules
16598
else putDoc (debug parsedDefinition)
16699

167-
let KoreParserOptions { patternFileName } = koreParserOptions
168-
unless (null patternFileName) $ do
100+
let KoreParserOptions { patternOpt } = koreParserOptions
101+
for_ patternOpt $ \patternOptions -> do
102+
let PatternOptions { patternFileName } = patternOptions
169103
parsedPattern <- mainPatternParse patternFileName
170104
when willVerify $ do
171-
let KoreParserOptions { mainModuleName } = koreParserOptions
105+
let PatternOptions { mainModuleName } = patternOptions
172106
indexedModule <-
173107
lookupMainModule
174108
(ModuleName mainModuleName)
175109
indexedModules
176110
& lift
177111
_ <- mainPatternVerify indexedModule parsedPattern
178112
return ()
179-
let KoreParserOptions { willPrintPattern } = koreParserOptions
113+
let KoreParserOptions { willPrintPattern } =
114+
koreParserOptions
180115
when willPrintPattern $
181116
lift $ putDoc (debug parsedPattern)
182117

‎kore/app/share/GlobalMain.hs

Lines changed: 0 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ module GlobalMain
1010
, parseKoreProveOptions
1111
, parseKoreMergeOptions
1212
, mainGlobal
13-
, enableDisableFlag
1413
, clockSomething
1514
, clockSomethingIO
1615
, mainPatternVerify
@@ -76,13 +75,10 @@ import Options.Applicative
7675
, defaultPrefs
7776
, execParserPure
7877
, flag
79-
, flag'
8078
, handleParseResult
8179
, help
8280
, helper
83-
, hidden
8481
, info
85-
, internal
8682
, long
8783
, maybeReader
8884
, metavar
@@ -385,36 +381,6 @@ commandLineParse (ExeName exeName) maybeEnv parser infoMod = do
385381
----------------------
386382
-- Helper Functions --
387383

388-
{-|
389-
Parser builder to create an optional boolean flag,
390-
with an enabled, disabled and default value.
391-
Based on `enableDisableFlagNoDefault`
392-
from commercialhaskell/stack:
393-
https://github.com/commercialhaskell/stack/blob/master/src/Options/Applicative/Builder/Extra.hs
394-
-}
395-
enableDisableFlag
396-
:: String -- ^ flag name
397-
-> option -- ^ enabled value
398-
-> option -- ^ disabled value
399-
-> option -- ^ default value
400-
-> String -- ^ Help text suffix; appended to "Enable/disable "
401-
-> Parser option
402-
enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix =
403-
flag' enabledVal
404-
( hidden
405-
<> internal
406-
<> long name
407-
<> help helpSuffix)
408-
<|> flag' disabledVal
409-
( hidden
410-
<> internal
411-
<> long ("no-" ++ name)
412-
<> help helpSuffix )
413-
<|> flag' disabledVal
414-
( long ( "[no-]" ++ name )
415-
<> help ( "Enable/disable " ++ helpSuffix ) )
416-
<|> pure defaultVal
417-
418384

419385
-- | Time a pure computation and print results.
420386
clockSomething :: String -> a -> Main a

‎kore/kore.cabal

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -222,6 +222,7 @@ library
222222
Kore.ModelChecker.Bounded
223223
Kore.ModelChecker.Simplification
224224
Kore.ModelChecker.Step
225+
Kore.Options
225226
Kore.Parser
226227
Kore.Parser.CString
227228
Kore.Parser.Lexer
@@ -954,6 +955,7 @@ test-suite kore-test
954955
Test.Kore.Log.ErrorBottomTotalFunction
955956
Test.Kore.Log.WarnFunctionWithoutEvaluators
956957
Test.Kore.Log.WarnSymbolSMTRepresentation
958+
Test.Kore.Options
957959
Test.Kore.Parser
958960
Test.Kore.Parser.Lexer
959961
Test.Kore.Parser.Parser

‎kore/src/Kore/Options.hs

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2020
3+
License : NCSA
4+
5+
-}
6+
7+
module Kore.Options
8+
( module Options.Applicative
9+
, enableDisableFlag
10+
, PatternOptions (..)
11+
, KoreParserOptions (..)
12+
, parseKoreParserOptions
13+
) where
14+
15+
import Prelude.Kore
16+
17+
import Data.Text
18+
( Text
19+
)
20+
21+
import Options.Applicative
22+
23+
{-|
24+
Parser builder to create an optional boolean flag,
25+
with an enabled, disabled and default value.
26+
Based on `enableDisableFlagNoDefault`
27+
from commercialhaskell/stack:
28+
https://github.com/commercialhaskell/stack/blob/master/src/Options/Applicative/Builder/Extra.hs
29+
-}
30+
enableDisableFlag
31+
:: String -- ^ flag name
32+
-> option -- ^ enabled value
33+
-> option -- ^ disabled value
34+
-> option -- ^ default value
35+
-> String -- ^ Help text suffix; appended to "Enable/disable "
36+
-> Parser option
37+
enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix =
38+
flag' enabledVal
39+
( hidden
40+
<> internal
41+
<> long name
42+
<> help helpSuffix)
43+
<|> flag' disabledVal
44+
( hidden
45+
<> internal
46+
<> long ("no-" ++ name)
47+
<> help helpSuffix )
48+
<|> flag' disabledVal
49+
( long ( "[no-]" ++ name )
50+
<> help ( "Enable/disable " ++ helpSuffix ) )
51+
<|> pure defaultVal
52+
53+
{- | Options for parsing and verifying a pattern.
54+
-}
55+
data PatternOptions = PatternOptions
56+
{ patternFileName :: !FilePath
57+
-- ^ name of file containing a pattern to parse and verify
58+
, mainModuleName :: !Text
59+
-- ^ the name of the main module in the definition
60+
}
61+
62+
-- | Main options record
63+
data KoreParserOptions = KoreParserOptions
64+
{ fileName :: !FilePath
65+
-- ^ Name for a file containing a definition to parse and verify
66+
, patternOpt :: !(Maybe PatternOptions)
67+
-- ^ Optionally, parse and verify a pattern relative to the definition.
68+
, willPrintDefinition :: !Bool
69+
-- ^ Option to print definition
70+
, willPrintPattern :: !Bool
71+
-- ^ Option to print pattern
72+
, willVerify :: !Bool
73+
-- ^ Option to verify definition
74+
, appKore :: !Bool
75+
-- ^ Option to print in applicative Kore syntax
76+
}
77+
78+
parsePatternOptions :: Parser PatternOptions
79+
parsePatternOptions = PatternOptions
80+
<$> strOption
81+
( metavar "PATTERN_FILE"
82+
<> long "pattern"
83+
<> help "Kore pattern source file to parse [and verify]. Needs --module.")
84+
<*> strOption
85+
( metavar "MODULE"
86+
<> long "module"
87+
<> help "The name of the main module in the Kore definition")
88+
89+
-- | Command Line Argument Parser
90+
parseKoreParserOptions :: Parser KoreParserOptions
91+
parseKoreParserOptions =
92+
KoreParserOptions
93+
<$> argument str
94+
( metavar "FILE"
95+
<> help "Kore source file to parse [and verify]" )
96+
<*> optional parsePatternOptions
97+
<*> enableDisableFlag "print-definition"
98+
True False False
99+
"printing parsed definition to stdout [default disabled]"
100+
<*> enableDisableFlag "print-pattern"
101+
True False False
102+
"printing parsed pattern to stdout [default disabled]"
103+
<*> enableDisableFlag "verify"
104+
True False True
105+
"Verify well-formedness of parsed definition [default enabled]"
106+
<*> enableDisableFlag "appkore"
107+
True False False
108+
( "printing parsed definition in applicative Kore syntax "
109+
++ "[default disabled]"
110+
)

‎kore/test/Test/Kore/Options.hs

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
module Test.Kore.Options
2+
( test_flags
3+
, test_options
4+
) where
5+
6+
import Prelude.Kore
7+
8+
import Data.Maybe
9+
( fromJust
10+
)
11+
12+
import Test.Tasty
13+
import Test.Tasty.HUnit.Ext
14+
15+
import Kore.Options
16+
17+
test_flags :: [TestTree]
18+
test_flags =
19+
[ testGroup "print-definition"
20+
[ testCase "default is False" $ do
21+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
22+
["mock/path/to/def"]
23+
assertEqual "Expected print-definition to be False by default"
24+
False flagValue
25+
, testCase "given explicitly is True" $ do
26+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
27+
["mock/path/to/def", "--print-definition"]
28+
assertEqual "Expected --print-definition to give True"
29+
True flagValue
30+
, testCase "with `no` prefix is False" $ do
31+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
32+
["mock/path/to/def", "--no-print-definition"]
33+
assertEqual "Expected --no-print-definition to give False"
34+
False flagValue
35+
]
36+
, testGroup "print-pattern"
37+
[ testCase "default is False" $ do
38+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
39+
["mock/path/to/def"]
40+
assertEqual "Expected print-pattern to be False by default"
41+
False flagValue
42+
, testCase "given explicitly is True" $ do
43+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
44+
["mock/path/to/def", "--print-pattern"]
45+
assertEqual "Expected --print-pattern to give True"
46+
True flagValue
47+
, testCase "with `no` prefix is False" $ do
48+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
49+
["mock/path/to/def", "--no-print-pattern"]
50+
assertEqual "Expected --no-print-pattern to give False"
51+
False flagValue
52+
]
53+
]
54+
55+
test_options :: [TestTree]
56+
test_options =
57+
[ testGroup "pattern and module must go together"
58+
[ testCase "pattern only" $ do
59+
let result = runParser' parseKoreParserOptions
60+
["mock/path/to/def", "--pattern", "mock/path/to/pat"]
61+
assertBool "Expected passing only the pattern option to fail"
62+
$ isNothing result
63+
, testCase "module only" $ do
64+
let result = runParser' parseKoreParserOptions
65+
["mock/path/to/def", "--module", "mock_module"]
66+
assertBool "Expected passing only the module option to fail"
67+
$ isNothing result
68+
, testCase "pattern and module" $ do
69+
let result = runParser' parseKoreParserOptions
70+
["mock/path/to/def", "--pattern", "mock/path/to/pat"
71+
, "--module", "mock_module"]
72+
assertBool "Expected passing both pattern and module options to not fail"
73+
$ isJust result
74+
]
75+
]
76+
77+
runParser' :: Parser a -> [String] -> Maybe a
78+
runParser' parser input = getParseResult parserResult
79+
where
80+
parserInfo = info parser mempty
81+
parserResult = execParserPure defaultPrefs parserInfo input
82+
83+
runParser :: Parser a -> [String] -> a
84+
runParser parser input = fromJust $ runParser' parser input

0 commit comments

Comments
 (0)