Skip to content

Commit a1f4525

Browse files
MirceaSMirceaS
committed
Moved option parser code to the library and added unit tests for it
1 parent fcd6940 commit a1f4525

File tree

4 files changed

+155
-96
lines changed

4 files changed

+155
-96
lines changed

‎kore/app/parser/Main.hs

Lines changed: 1 addition & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -8,22 +8,11 @@ import Control.Monad.Catch
88
, handle
99
)
1010
import qualified Data.Map.Strict as Map
11-
import Data.Text
12-
( Text
13-
)
1411
import Options.Applicative
1512
( InfoMod
16-
, Parser
17-
, argument
1813
, fullDesc
1914
, header
20-
, help
21-
, long
22-
, metavar
2315
, progDesc
24-
, str
25-
, strOption
26-
, value
2716
)
2817

2918
import Kore.AST.ApplicativeKore
@@ -46,6 +35,7 @@ import qualified Kore.Log as Log
4635
import Kore.Log.ErrorVerify
4736
( errorVerify
4837
)
38+
import Kore.OptionsParser
4939
import Kore.Parser
5040
( parseKoreDefinition
5141
, parseKorePattern
@@ -65,57 +55,6 @@ Main module to run kore-parser
6555
TODO: add command line argument tab-completion
6656
-}
6757

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 False
106-
"printing parsed definition to stdout [default disabled]"
107-
<*> enableDisableFlag "print-pattern"
108-
True False False
109-
"printing parsed pattern to stdout [default disabled]"
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-
11958
-- | modifiers for the Command line parser description
12059
parserInfoModifiers :: InfoMod options
12160
parserInfoModifiers =

‎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/src/Kore/OptionsParser.hs

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

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

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
module Test.Kore.OptionsParser
2+
( test_flags
3+
) where
4+
5+
import Prelude.Kore
6+
7+
import Data.Maybe
8+
( fromJust
9+
)
10+
11+
import Test.Tasty
12+
import Test.Tasty.HUnit.Ext
13+
14+
import Kore.OptionsParser
15+
16+
import Options.Applicative
17+
18+
test_flags :: [TestTree]
19+
test_flags =
20+
[ testGroup "print-definition"
21+
[ testCase "default is False" $ do
22+
let flag_value = willPrintDefinition $ runParser commandLineParser
23+
["mock/path/to/file"]
24+
assertEqual "Expected print-definition to be False by default"
25+
False flag_value
26+
, testCase "given explicitly is True" $ do
27+
let flag_value = willPrintDefinition $ runParser commandLineParser
28+
["mock/path/to/file", "--print-definition"]
29+
assertEqual "Expected --print-definition to give True"
30+
True flag_value
31+
, testCase "with `no` prefix is False" $ do
32+
let flag_value = willPrintDefinition $ runParser commandLineParser
33+
["mock/path/to/file", "--no-print-definition"]
34+
assertEqual "Expected --no-print-definition to give False"
35+
False flag_value
36+
]
37+
, testGroup "print-pattern"
38+
[ testCase "default is False" $ do
39+
let flag_value = willPrintPattern $ runParser commandLineParser
40+
["mock/path/to/file"]
41+
assertEqual "Expected print-pattern to be False by default"
42+
False flag_value
43+
, testCase "given explicitly is True" $ do
44+
let flag_value = willPrintPattern $ runParser commandLineParser
45+
["mock/path/to/file", "--print-pattern"]
46+
assertEqual "Expected --print-pattern to give True"
47+
True flag_value
48+
, testCase "with `no` prefix is False" $ do
49+
let flag_value = willPrintPattern $ runParser commandLineParser
50+
["mock/path/to/file", "--no-print-pattern"]
51+
assertEqual "Expected --no-print-pattern to give False"
52+
False flag_value
53+
]
54+
]
55+
56+
runParser :: Parser a -> [String] -> a
57+
runParser parser input = fromJust $ getParseResult parserResult
58+
where
59+
parserInfo = info parser mempty
60+
parserResult = execParserPure defaultPrefs parserInfo input

0 commit comments

Comments
 (0)