Skip to content

Commit df3cbf4

Browse files
MirceaSMirceaS
committed
addressed PR comments
1 parent 4c7c1db commit df3cbf4

File tree

3 files changed

+55
-65
lines changed

3 files changed

+55
-65
lines changed

‎kore/app/parser/Main.hs

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ import qualified Kore.Log as Log
3535
import Kore.Log.ErrorVerify
3636
( errorVerify
3737
)
38-
import Kore.OptionsParser
38+
import Kore.Options
3939
import Kore.Parser
4040
( parseKoreDefinition
4141
, parseKorePattern
@@ -83,7 +83,7 @@ main = handleTop $ do
8383
mainGlobal
8484
(ExeName "kore-parser")
8585
Nothing -- environment variable name for extra arguments
86-
commandLineParser
86+
parseKoreParserOptions
8787
parserInfoModifiers
8888
for_ (localOptions options) $ \koreParserOptions ->
8989
flip runLoggerT Log.emptyLogger $ do
@@ -104,22 +104,22 @@ main = handleTop $ do
104104
else putDoc (debug parsedDefinition)
105105

106106
let KoreParserOptions { patternOpt } = koreParserOptions
107-
case patternOpt of
108-
Nothing -> pure ()
109-
Just PatternOptions {patternFileName, mainModuleName} -> do
110-
parsedPattern <- mainPatternParse patternFileName
111-
when willVerify $ do
112-
indexedModule <-
113-
lookupMainModule
114-
(ModuleName mainModuleName)
115-
indexedModules
116-
& lift
117-
_ <- mainPatternVerify indexedModule parsedPattern
118-
return ()
119-
let KoreParserOptions { willPrintPattern } =
120-
koreParserOptions
121-
when willPrintPattern $
122-
lift $ putDoc (debug parsedPattern)
107+
for_ patternOpt $ \patternOptions -> do
108+
let PatternOptions { patternFileName } = patternOptions
109+
parsedPattern <- mainPatternParse patternFileName
110+
when willVerify $ do
111+
let PatternOptions { mainModuleName } = patternOptions
112+
indexedModule <-
113+
lookupMainModule
114+
(ModuleName mainModuleName)
115+
indexedModules
116+
& lift
117+
_ <- mainPatternVerify indexedModule parsedPattern
118+
return ()
119+
let KoreParserOptions { willPrintPattern } =
120+
koreParserOptions
121+
when willPrintPattern $
122+
lift $ putDoc (debug parsedPattern)
123123

124124
-- | IO action that parses a kore definition from a filename and prints timing
125125
-- information.

‎kore/src/Kore/OptionsParser.hs renamed to ‎kore/src/Kore/Options.hs

Lines changed: 19 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,15 @@ License : NCSA
44
55
-}
66

7-
module Kore.OptionsParser
8-
( enableDisableFlag
7+
module Kore.Options
8+
( module Options.Applicative
9+
, enableDisableFlag
910
, PatternOptions (..)
1011
, KoreParserOptions (..)
11-
, commandLineParser
12+
, parseKoreParserOptions
1213
) where
1314

14-
import Data.Text
15-
( Text
16-
)
15+
import Data.Text ( Text )
1716

1817
import Prelude.Kore
1918

@@ -49,7 +48,6 @@ enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix =
4948
<> help ( "Enable/disable " ++ helpSuffix ) )
5049
<|> pure defaultVal
5150

52-
5351
data PatternOptions = PatternOptions
5452
{ patternFileName :: !FilePath
5553
-- ^ Name for file containing a pattern to parse and verify
@@ -73,29 +71,25 @@ data KoreParserOptions = KoreParserOptions
7371
-- ^ Option to print in applicative Kore syntax
7472
}
7573

74+
parsePatternOptions :: Parser PatternOptions
75+
parsePatternOptions = PatternOptions
76+
<$> strOption
77+
( metavar "PATTERN_FILE"
78+
<> long "pattern"
79+
<> help "Kore pattern source file to parse [and verify]. Needs --module.")
80+
<*> strOption
81+
( metavar "MODULE"
82+
<> long "module"
83+
<> help "The name of the main module in the Kore definition")
84+
7685
-- | Command Line Argument Parser
77-
commandLineParser :: Parser KoreParserOptions
78-
commandLineParser =
86+
parseKoreParserOptions :: Parser KoreParserOptions
87+
parseKoreParserOptions =
7988
KoreParserOptions
8089
<$> argument str
8190
( metavar "FILE"
8291
<> help "Kore source file to parse [and verify]" )
83-
<*> ( (Just <$>
84-
(PatternOptions
85-
<$> strOption
86-
( metavar "PATTERN_FILE"
87-
<> long "pattern"
88-
<> help "Kore pattern source file to parse [and verify]. Needs --module.")
89-
<*> strOption
90-
( metavar "MODULE"
91-
<> long "module"
92-
<> help "The name of the main module in the Kore definition")
93-
)
94-
)
95-
<|> flag Nothing Nothing
96-
( long "definition-only"
97-
<> help "No Kore pattern may be checked against the definition")
98-
)
92+
<*> optional parsePatternOptions
9993
<*> enableDisableFlag "print-definition"
10094
True False False
10195
"printing parsed definition to stdout [default disabled]"

‎kore/test/Test/Kore/OptionsParser.hs renamed to ‎kore/test/Test/Kore/Options.hs

Lines changed: 18 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,74 +1,70 @@
1-
module Test.Kore.OptionsParser
1+
module Test.Kore.Options
22
( test_flags
33
, test_options
44
) where
55

66
import Prelude.Kore
77

8-
import Data.Maybe
9-
( fromJust
10-
)
8+
import Data.Maybe ( fromJust )
119

1210
import Test.Tasty
1311
import Test.Tasty.HUnit.Ext
1412

15-
import Kore.OptionsParser
16-
17-
import Options.Applicative
13+
import Kore.Options
1814

1915
test_flags :: [TestTree]
2016
test_flags =
2117
[ testGroup "print-definition"
2218
[ testCase "default is False" $ do
23-
let flag_value = willPrintDefinition $ runParser commandLineParser
19+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
2420
["mock/path/to/def"]
2521
assertEqual "Expected print-definition to be False by default"
26-
False flag_value
22+
False flagValue
2723
, testCase "given explicitly is True" $ do
28-
let flag_value = willPrintDefinition $ runParser commandLineParser
24+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
2925
["mock/path/to/def", "--print-definition"]
3026
assertEqual "Expected --print-definition to give True"
31-
True flag_value
27+
True flagValue
3228
, testCase "with `no` prefix is False" $ do
33-
let flag_value = willPrintDefinition $ runParser commandLineParser
29+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
3430
["mock/path/to/def", "--no-print-definition"]
3531
assertEqual "Expected --no-print-definition to give False"
36-
False flag_value
32+
False flagValue
3733
]
3834
, testGroup "print-pattern"
3935
[ testCase "default is False" $ do
40-
let flag_value = willPrintPattern $ runParser commandLineParser
36+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
4137
["mock/path/to/def"]
4238
assertEqual "Expected print-pattern to be False by default"
43-
False flag_value
39+
False flagValue
4440
, testCase "given explicitly is True" $ do
45-
let flag_value = willPrintPattern $ runParser commandLineParser
41+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
4642
["mock/path/to/def", "--print-pattern"]
4743
assertEqual "Expected --print-pattern to give True"
48-
True flag_value
44+
True flagValue
4945
, testCase "with `no` prefix is False" $ do
50-
let flag_value = willPrintPattern $ runParser commandLineParser
46+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
5147
["mock/path/to/def", "--no-print-pattern"]
5248
assertEqual "Expected --no-print-pattern to give False"
53-
False flag_value
49+
False flagValue
5450
]
5551
]
5652

5753
test_options :: [TestTree]
5854
test_options =
5955
[ testGroup "pattern and module must go together"
6056
[ testCase "pattern only" $ do
61-
let result = runParser' commandLineParser
57+
let result = runParser' parseKoreParserOptions
6258
["mock/path/to/def", "--pattern", "mock/path/to/pat"]
6359
assertBool "Expected passing only the pattern option to fail"
6460
$ isNothing result
6561
, testCase "module only" $ do
66-
let result = runParser' commandLineParser
62+
let result = runParser' parseKoreParserOptions
6763
["mock/path/to/def", "--module", "mock_module"]
6864
assertBool "Expected passing only the module option to fail"
6965
$ isNothing result
7066
, testCase "pattern and module" $ do
71-
let result = runParser' commandLineParser
67+
let result = runParser' parseKoreParserOptions
7268
["mock/path/to/def", "--pattern", "mock/path/to/pat"
7369
, "--module", "mock_module"]
7470
assertBool "Expected passing both pattern and module options to not fail"

0 commit comments

Comments
 (0)