Skip to content

Commit 6bb84ec

Browse files
MirceaSttuegelrv-jenkins
authored
kore-parser: Parse and validate multiple pattern files
* made kore-parser accept multiple patterns for parsing/validation * fixed small issue * addressed PR comments * kore-parser: Use FilePath instead of String where appropriate * kore-parser: Clean up application logic * Fixed printing behaviour Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com> Co-authored-by: rv-jenkins <admin@runtimeverification.com>
1 parent 1d245bc commit 6bb84ec

File tree

3 files changed

+84
-49
lines changed

3 files changed

+84
-49
lines changed

‎kore/app/parser/Main.hs‎

Lines changed: 69 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,9 @@ import Kore.AST.ApplicativeKore
1313
import Kore.ASTVerifier.DefinitionVerifier
1414
( verifyAndIndexDefinition
1515
)
16-
import Kore.Attribute.Symbol
17-
( StepperAttributes
16+
import qualified Kore.ASTVerifier.PatternVerifier as PatternVerifier
17+
import qualified Kore.Attribute.Symbol as Attribute
18+
( Symbol
1819
)
1920
import qualified Kore.Builtin as Builtin
2021
import Kore.Debug
@@ -79,58 +80,51 @@ main = handleTop $ do
7980
Nothing -- environment variable name for extra arguments
8081
parseKoreParserOptions
8182
parserInfoModifiers
82-
for_ (localOptions options) $ \koreParserOptions ->
83-
flip runLoggerT Log.emptyLogger $ do
83+
for_ (localOptions options) $ \koreParserOptions -> runEmptyLogger $ do
84+
indexedModules <- do
8485
let KoreParserOptions { fileName } = koreParserOptions
8586
parsedDefinition <- mainDefinitionParse fileName
8687
let KoreParserOptions { willVerify } = koreParserOptions
87-
indexedModules <- if willVerify
88-
then lift $ mainVerify parsedDefinition
89-
else return Map.empty
88+
indexedModules <-
89+
if willVerify
90+
then fmap Just . lift $ mainVerify parsedDefinition
91+
else pure Nothing
9092
let KoreParserOptions { willPrintDefinition } = koreParserOptions
9193
let KoreParserOptions { appKore } = koreParserOptions
92-
lift $ when willPrintDefinition
93-
$ if appKore
94-
then putStrLn
95-
$ unparseToString2
96-
$ completeDefinition
97-
$ toVerifiedDefinition indexedModules
98-
else putDoc (debug parsedDefinition)
99-
100-
let KoreParserOptions { patternOpt } = koreParserOptions
101-
for_ patternOpt $ \patternOptions -> do
102-
let PatternOptions { patternFileName } = patternOptions
94+
when (willPrintDefinition && not appKore)
95+
$ putDebug parsedDefinition
96+
when appKore $ for_ indexedModules printAppKore
97+
pure indexedModules
98+
99+
let KoreParserOptions { patternOpt } = koreParserOptions
100+
for_ patternOpt $ \patternOptions -> do
101+
let PatternOptions { mainModuleName } = patternOptions
102+
moduleName = ModuleName mainModuleName
103+
indexedModule <-
104+
traverse (lookupMainModule moduleName) indexedModules
105+
let PatternOptions { patternFileNames } = patternOptions
106+
for_ patternFileNames $ \patternFileName -> do
103107
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)
108+
verifyPattern indexedModule parsedPattern
109+
let KoreParserOptions { willPrintPattern } = koreParserOptions
110+
when willPrintPattern $ putDebug parsedPattern
117111

118112
-- | IO action that parses a kore definition from a filename and prints timing
119113
-- information.
120-
mainDefinitionParse :: String -> Main ParsedDefinition
114+
mainDefinitionParse :: FilePath -> Main ParsedDefinition
121115
mainDefinitionParse = mainParse parseKoreDefinition
122116

123117
-- | IO action that parses a kore pattern from a filename and prints timing
124118
-- information.
125-
mainPatternParse :: String -> Main ParsedPattern
119+
mainPatternParse :: FilePath -> Main ParsedPattern
126120
mainPatternParse = mainParse parseKorePattern
127121

128122
-- | IO action verifies well-formedness of Kore definition and prints
129123
-- timing information.
130124
mainVerify
131125
:: ParsedDefinition
132126
-- ^ Parsed definition to check well-formedness
133-
-> IO (Map.Map ModuleName (VerifiedModule StepperAttributes))
127+
-> IO (Map.Map ModuleName (VerifiedModule Attribute.Symbol))
134128
mainVerify definition = flip runLoggerT Log.emptyLogger $ do
135129
verifyResult <-
136130
clockSomething "Verifying the definition"
@@ -139,3 +133,44 @@ mainVerify definition = flip runLoggerT Log.emptyLogger $ do
139133
definition
140134
)
141135
either errorVerify return verifyResult
136+
137+
{- | Validate a pattern relative to the provided module.
138+
139+
If the module is not provided, no validation is performed.
140+
141+
-}
142+
verifyPattern
143+
:: Maybe (VerifiedModule Attribute.Symbol)
144+
-- ^ Module containing definitions visible in the pattern.
145+
-> ParsedPattern -- ^ Parsed pattern to check well-formedness
146+
-> Main ()
147+
verifyPattern Nothing _ = pure ()
148+
verifyPattern (Just verifiedModule) patt = do
149+
verifyResult <-
150+
PatternVerifier.verifyStandalonePattern Nothing patt
151+
& PatternVerifier.runPatternVerifier context
152+
& clockSomething "Verifying the pattern"
153+
either errorVerify (\_ -> pure ()) verifyResult
154+
where
155+
context =
156+
PatternVerifier.verifiedModuleContext verifiedModule
157+
& PatternVerifier.withBuiltinVerifiers Builtin.koreVerifiers
158+
159+
-- | Print the valid definition in Applicative Kore syntax.
160+
printAppKore
161+
:: MonadIO io
162+
=> Map.Map ModuleName (VerifiedModule Attribute.Symbol)
163+
-> io ()
164+
printAppKore =
165+
liftIO
166+
. putStrLn
167+
. unparseToString2
168+
. completeDefinition
169+
. toVerifiedDefinition
170+
171+
-- | Print any 'Debug'-able type.
172+
putDebug :: Debug a => MonadIO io => a -> io ()
173+
putDebug = liftIO . putDoc . debug
174+
175+
runEmptyLogger :: Main a -> IO a
176+
runEmptyLogger = flip runLoggerT Log.emptyLogger

‎kore/app/share/GlobalMain.hs‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -427,9 +427,7 @@ mainPatternVerify verifiedModule patt = do
427427
lookupMainModule
428428
:: Monad monad
429429
=> ModuleName
430-
-> Map.Map
431-
ModuleName
432-
(VerifiedModule Attribute.Symbol)
430+
-> Map.Map ModuleName (VerifiedModule Attribute.Symbol)
433431
-> monad (VerifiedModule Attribute.Symbol)
434432
lookupMainModule name modules =
435433
case Map.lookup name modules of

‎kore/src/Kore/Options.hs‎

Lines changed: 14 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ enableDisableFlag name enabledVal disabledVal defaultVal helpSuffix =
5353
{- | Options for parsing and verifying a pattern.
5454
-}
5555
data PatternOptions = PatternOptions
56-
{ patternFileName :: !FilePath
56+
{ patternFileNames :: ![FilePath]
5757
-- ^ name of file containing a pattern to parse and verify
5858
, mainModuleName :: !Text
5959
-- ^ the name of the main module in the definition
@@ -77,34 +77,36 @@ data KoreParserOptions = KoreParserOptions
7777

7878
parsePatternOptions :: Parser PatternOptions
7979
parsePatternOptions = PatternOptions
80-
<$> strOption
81-
( metavar "PATTERN_FILE"
82-
<> long "pattern"
83-
<> help "Kore pattern source file to parse [and verify]. Needs --module.")
80+
<$> some parsePatternFileName
8481
<*> strOption
8582
( metavar "MODULE"
8683
<> long "module"
8784
<> help "The name of the main module in the Kore definition")
85+
where
86+
parsePatternFileName = strOption
87+
( metavar "PATTERN_FILE"
88+
<> long "pattern"
89+
<> help "Kore pattern source file to parse [and verify]. Needs --module.")
8890

8991
-- | Command Line Argument Parser
9092
parseKoreParserOptions :: Parser KoreParserOptions
9193
parseKoreParserOptions =
9294
KoreParserOptions
9395
<$> argument str
9496
( metavar "FILE"
95-
<> help "Kore source file to parse [and verify]" )
97+
<> help "Kore source file to parse and (optionally) validate." )
9698
<*> optional parsePatternOptions
9799
<*> enableDisableFlag "print-definition"
98100
True False False
99-
"printing parsed definition to stdout [default disabled]"
101+
"Print the parsed definition. [default: disabled]"
100102
<*> enableDisableFlag "print-pattern"
101103
True False False
102-
"printing parsed pattern to stdout [default disabled]"
104+
"Print the parsed pattern. [default: disabled]"
103105
<*> enableDisableFlag "verify"
104106
True False True
105-
"Verify well-formedness of parsed definition [default enabled]"
107+
"Verify well-formedness of parsed definition and pattern(s).\
108+
\ [default: enabled]"
106109
<*> enableDisableFlag "appkore"
107110
True False False
108-
( "printing parsed definition in applicative Kore syntax "
109-
++ "[default disabled]"
110-
)
111+
"Print the valid definition in applicative Kore syntax.\
112+
\ (Requires --verify.) [default: disabled]"

0 commit comments

Comments
 (0)