Skip to content

Commit e2834fb

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

File tree

3 files changed

+53
-65
lines changed

3 files changed

+53
-65
lines changed

‎kore/app/parser/Main.hs

Lines changed: 18 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,6 @@ import Control.Monad.Catch
88
, handle
99
)
1010
import qualified Data.Map.Strict as Map
11-
import Options.Applicative
12-
( InfoMod
13-
, fullDesc
14-
, header
15-
, progDesc
16-
)
1711

1812
import Kore.AST.ApplicativeKore
1913
import Kore.ASTVerifier.DefinitionVerifier
@@ -35,7 +29,7 @@ import qualified Kore.Log as Log
3529
import Kore.Log.ErrorVerify
3630
( errorVerify
3731
)
38-
import Kore.OptionsParser
32+
import Kore.Options
3933
import Kore.Parser
4034
( parseKoreDefinition
4135
, parseKorePattern
@@ -83,7 +77,7 @@ main = handleTop $ do
8377
mainGlobal
8478
(ExeName "kore-parser")
8579
Nothing -- environment variable name for extra arguments
86-
commandLineParser
80+
parseKoreParserOptions
8781
parserInfoModifiers
8882
for_ (localOptions options) $ \koreParserOptions ->
8983
flip runLoggerT Log.emptyLogger $ do
@@ -104,22 +98,22 @@ main = handleTop $ do
10498
else putDoc (debug parsedDefinition)
10599

106100
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)
101+
for_ patternOpt $ \patternOptions -> do
102+
let PatternOptions { patternFileName } = patternOptions
103+
parsedPattern <- mainPatternParse patternFileName
104+
when willVerify $ do
105+
let PatternOptions { mainModuleName } = patternOptions
106+
indexedModule <-
107+
lookupMainModule
108+
(ModuleName mainModuleName)
109+
indexedModules
110+
& lift
111+
_ <- mainPatternVerify indexedModule parsedPattern
112+
return ()
113+
let KoreParserOptions { willPrintPattern } =
114+
koreParserOptions
115+
when willPrintPattern $
116+
lift $ putDoc (debug parsedPattern)
123117

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

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

Lines changed: 18 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,12 @@ 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

1415
import Data.Text
@@ -49,7 +50,6 @@ enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix =
4950
<> help ( "Enable/disable " ++ helpSuffix ) )
5051
<|> pure defaultVal
5152

52-
5353
data PatternOptions = PatternOptions
5454
{ patternFileName :: !FilePath
5555
-- ^ Name for file containing a pattern to parse and verify
@@ -73,29 +73,25 @@ data KoreParserOptions = KoreParserOptions
7373
-- ^ Option to print in applicative Kore syntax
7474
}
7575

76+
parsePatternOptions :: Parser PatternOptions
77+
parsePatternOptions = PatternOptions
78+
<$> strOption
79+
( metavar "PATTERN_FILE"
80+
<> long "pattern"
81+
<> help "Kore pattern source file to parse [and verify]. Needs --module.")
82+
<*> strOption
83+
( metavar "MODULE"
84+
<> long "module"
85+
<> help "The name of the main module in the Kore definition")
86+
7687
-- | Command Line Argument Parser
77-
commandLineParser :: Parser KoreParserOptions
78-
commandLineParser =
88+
parseKoreParserOptions :: Parser KoreParserOptions
89+
parseKoreParserOptions =
7990
KoreParserOptions
8091
<$> argument str
8192
( metavar "FILE"
8293
<> 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-
)
94+
<*> optional parsePatternOptions
9995
<*> enableDisableFlag "print-definition"
10096
True False False
10197
"printing parsed definition to stdout [default disabled]"

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

Lines changed: 17 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
module Test.Kore.OptionsParser
1+
module Test.Kore.Options
22
( test_flags
33
, test_options
44
) where
@@ -12,63 +12,61 @@ import Data.Maybe
1212
import Test.Tasty
1313
import Test.Tasty.HUnit.Ext
1414

15-
import Kore.OptionsParser
16-
17-
import Options.Applicative
15+
import Kore.Options
1816

1917
test_flags :: [TestTree]
2018
test_flags =
2119
[ testGroup "print-definition"
2220
[ testCase "default is False" $ do
23-
let flag_value = willPrintDefinition $ runParser commandLineParser
21+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
2422
["mock/path/to/def"]
2523
assertEqual "Expected print-definition to be False by default"
26-
False flag_value
24+
False flagValue
2725
, testCase "given explicitly is True" $ do
28-
let flag_value = willPrintDefinition $ runParser commandLineParser
26+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
2927
["mock/path/to/def", "--print-definition"]
3028
assertEqual "Expected --print-definition to give True"
31-
True flag_value
29+
True flagValue
3230
, testCase "with `no` prefix is False" $ do
33-
let flag_value = willPrintDefinition $ runParser commandLineParser
31+
let flagValue = willPrintDefinition $ runParser parseKoreParserOptions
3432
["mock/path/to/def", "--no-print-definition"]
3533
assertEqual "Expected --no-print-definition to give False"
36-
False flag_value
34+
False flagValue
3735
]
3836
, testGroup "print-pattern"
3937
[ testCase "default is False" $ do
40-
let flag_value = willPrintPattern $ runParser commandLineParser
38+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
4139
["mock/path/to/def"]
4240
assertEqual "Expected print-pattern to be False by default"
43-
False flag_value
41+
False flagValue
4442
, testCase "given explicitly is True" $ do
45-
let flag_value = willPrintPattern $ runParser commandLineParser
43+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
4644
["mock/path/to/def", "--print-pattern"]
4745
assertEqual "Expected --print-pattern to give True"
48-
True flag_value
46+
True flagValue
4947
, testCase "with `no` prefix is False" $ do
50-
let flag_value = willPrintPattern $ runParser commandLineParser
48+
let flagValue = willPrintPattern $ runParser parseKoreParserOptions
5149
["mock/path/to/def", "--no-print-pattern"]
5250
assertEqual "Expected --no-print-pattern to give False"
53-
False flag_value
51+
False flagValue
5452
]
5553
]
5654

5755
test_options :: [TestTree]
5856
test_options =
5957
[ testGroup "pattern and module must go together"
6058
[ testCase "pattern only" $ do
61-
let result = runParser' commandLineParser
59+
let result = runParser' parseKoreParserOptions
6260
["mock/path/to/def", "--pattern", "mock/path/to/pat"]
6361
assertBool "Expected passing only the pattern option to fail"
6462
$ isNothing result
6563
, testCase "module only" $ do
66-
let result = runParser' commandLineParser
64+
let result = runParser' parseKoreParserOptions
6765
["mock/path/to/def", "--module", "mock_module"]
6866
assertBool "Expected passing only the module option to fail"
6967
$ isNothing result
7068
, testCase "pattern and module" $ do
71-
let result = runParser' commandLineParser
69+
let result = runParser' parseKoreParserOptions
7270
["mock/path/to/def", "--pattern", "mock/path/to/pat"
7371
, "--module", "mock_module"]
7472
assertBool "Expected passing both pattern and module options to not fail"

0 commit comments

Comments
 (0)