Match disjunction tool

hie-cabal.yaml

@@ -9,3 +9,4 @@ cradle:
   - { path: "./kore/app/parser", component: "kore:kore-parser" }
   - { path: "./kore/app/prof", component: "kore:kore-prof" }
   - { path: "./kore/app/repl", component: "kore:kore-repl" }
+  - { path: "./kore/app/match-disjunction", component: "kore:kore-match-disjunction" }

hie-stack.yaml

@@ -9,3 +9,4 @@ cradle:
   - { path: "./kore/app/parser", component: "kore:kore-parser" }
   - { path: "./kore/app/prof", component: "kore:kore-prof" }
   - { path: "./kore/app/repl", component: "kore:kore-repl" }
+  - { path: "./kore/app/match-disjunction", component: "kore:kore-match-disjunction" }

kore/Makefile

@@ -46,6 +46,8 @@ ghcid:
 ghcid-repl:
 	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-repl --work-dir .stack-work-ghci"
 
+ghcid-match:
+	$(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-match-disjunction --work-dir .stack-work-ghci"
 
 # TODO(Vladimir): remove 'hyperlink-source' when we upgrade from lts-12.10 (8.4.3)
 hoogle-gen:

kore/app/exec/Main.hs

@@ -55,19 +55,11 @@ import Kore.Internal.MultiAnd (
  )
 import qualified Kore.Internal.MultiAnd as MultiAnd
 import qualified Kore.Internal.OrPattern as OrPattern
-import Kore.Internal.Pattern (
-    Conditional (..),
-    Pattern,
- )
-import Kore.Internal.Predicate (
-    makePredicate,
- )
 import Kore.Internal.TermLike (
     TermLike,
     VariableName,
     mkSortVariable,
     mkTop,
-    pattern And_,
  )
 import Kore.Log (
     KoreLogOptions (..),
@@ -91,10 +83,6 @@ import Kore.Log.WarnIfLowProductivity (
 import qualified Kore.ModelChecker.Bounded as Bounded (
     CheckResult (..),
  )
-import Kore.Parser (
-    ParsedPattern,
-    parseKorePattern,
- )
 import Kore.Parser.ParserUtils (
     readPositiveIntegral,
  )
@@ -161,7 +149,6 @@ import Options.SMT (
 import Prelude.Kore
 import Pretty (
     Doc,
-    Pretty (..),
     hPutDoc,
     putDoc,
     vsep,
@@ -919,48 +906,12 @@ loadPattern mainModule (Just fileName) =
     mainPatternParseAndVerify mainModule fileName
 loadPattern _ Nothing = error "Missing: --pattern PATTERN_FILE"
 
-{- | IO action that parses a kore pattern from a filename and prints timing
- information.
--}
-mainPatternParse :: String -> Main ParsedPattern
-mainPatternParse = mainParse parseKorePattern
-
 renderResult :: KoreExecOptions -> Doc ann -> IO ()
 renderResult KoreExecOptions{outputFileName} doc =
     case outputFileName of
         Nothing -> putDoc doc
         Just outputFile -> withFile outputFile WriteMode (`hPutDoc` doc)
 
-{- | IO action that parses a kore pattern from a filename, verifies it,
- converts it to a pure pattern, and prints timing information.
--}
-mainPatternParseAndVerify ::
-    VerifiedModule StepperAttributes ->
-    String ->
-    Main (TermLike VariableName)
-mainPatternParseAndVerify indexedModule patternFileName =
-    mainPatternParse patternFileName >>= mainPatternVerify indexedModule
-
-mainParseSearchPattern ::
-    VerifiedModule StepperAttributes ->
-    String ->
-    Main (Pattern VariableName)
-mainParseSearchPattern indexedModule patternFileName = do
-    purePattern <- mainPatternParseAndVerify indexedModule patternFileName
-    case purePattern of
-        And_ _ term predicateTerm ->
-            return
-                Conditional
-                    { term
-                    , predicate =
-                        either
-                            (error . show . pretty)
-                            id
-                            (makePredicate predicateTerm)
-                    , substitution = mempty
-                    }
-        _ -> error "Unexpected non-conjunctive pattern"
-
 savedProofsModuleName :: ModuleName
 savedProofsModuleName =
     ModuleName

kore/app/match-disjunction/Main.hs

@@ -0,0 +1,192 @@
+module Main (main) where
+
+import GlobalMain
+import Kore.Attribute.Symbol (
+    StepperAttributes,
+ )
+import Kore.BugReport
+import Kore.Exec (matchDisjunction)
+import Kore.IndexedModule.IndexedModule (
+    VerifiedModule,
+ )
+import Kore.Internal.Pattern (Pattern)
+import qualified Kore.Internal.Pattern as Pattern
+import Kore.Internal.TermLike (
+    pattern Or_,
+ )
+import Kore.Log (
+    KoreLogOptions,
+    parseKoreLogOptions,
+    runKoreLog,
+ )
+import Kore.Rewrite.RewritingVariable (
+    RewritingVariableName,
+    mkRewritingPattern,
+ )
+import Kore.Syntax.Module (
+    ModuleName (..),
+ )
+import Kore.Unparser (
+    unparse,
+ )
+import Options.Applicative (
+    InfoMod,
+    Parser,
+    argument,
+    fullDesc,
+    header,
+    help,
+    long,
+    metavar,
+    progDesc,
+    str,
+    strOption,
+ )
+import Prelude.Kore
+import Pretty
+import System.Clock (
+    Clock (..),
+    TimeSpec,
+    getTime,
+ )
+import System.Exit (
+    exitWith,
+ )
+import System.IO (
+    IOMode (WriteMode),
+    withFile,
+ )
+
+exeName :: ExeName
+exeName = ExeName "kore-match-disjunction"
+
+envName :: String
+envName = "KORE_MATCH_DISJUNCTION_OPTS"
+
+data KoreMatchDisjunctionOptions = KoreMatchDisjunctionOptions
+    { -- | Name of file containing a definition to verify and use for execution
+      definitionFileName :: !FilePath
+    , -- | Name of file containing a disjunction to verify and use for matching
+      disjunctionFileName :: !FilePath
+    , -- | Name of file used to match with disjunction
+      matchFileName :: !FilePath
+    , -- | Name for file to contain the output pattern
+      outputFileName :: !(Maybe FilePath)
+    , -- | The name of the main module in the definition
+      mainModuleName :: !ModuleName
+    , bugReportOption :: !BugReportOption
+    , koreLogOptions :: !KoreLogOptions
+    }
+
+parseKoreMatchDisjunctionOptions :: TimeSpec -> Parser KoreMatchDisjunctionOptions
+parseKoreMatchDisjunctionOptions startTime =
+    KoreMatchDisjunctionOptions
+        <$> argument
+            str
+            ( metavar "DEFINITION_FILE"
+                <> help "Kore definition file to verify and use for execution."
+            )
+        <*> strOption
+            ( metavar "DISJUNCTION_FILE"
+                <> long "disjunction"
+                <> help "File containing a disjunction of concrete terms."
+            )
+        <*> strOption
+            ( metavar "MATCH_FILE"
+                <> long "match"
+                <> help "Kore source file representing pattern to search for."
+            )
+        <*> optional
+            ( strOption
+                ( metavar "PATTERN_OUTPUT_FILE"
+                    <> long "output"
+                    <> help "Output file to contain final Kore pattern."
+                )
+            )
+        <*> parseMainModuleName
+        <*> parseBugReportOption
+        <*> parseKoreLogOptions exeName startTime
+  where
+    parseMainModuleName =
+        GlobalMain.parseModuleName
+            "MODULE"
+            "module"
+            "The name of the main module in the Kore definition."
+
+parserInfoModifiers :: InfoMod options
+parserInfoModifiers =
+    fullDesc
+        <> progDesc "Matches Kore pattern in MATCH_FILE with Kore pattern in DISJUNCTION_FILE"
+        <> header "kore-match-disjunction - a tool for applying search patterns to disjunctions of configurations"
+
+main :: IO ()
+main = do
+    startTime <- getTime Monotonic
+    options <-
+        mainGlobal
+            exeName
+            (Just envName)
+            (parseKoreMatchDisjunctionOptions startTime)
+            parserInfoModifiers
+    for_ (localOptions options) mainWithOptions
+
+mainWithOptions :: KoreMatchDisjunctionOptions -> IO ()
+mainWithOptions options = do
+    exitCode <-
+        withBugReport exeName bugReportOption $ \tmpDir ->
+            koreMatchDisjunction options
+                & runKoreLog tmpDir koreLogOptions
+    exitWith exitCode
+  where
+    KoreMatchDisjunctionOptions{bugReportOption} = options
+    KoreMatchDisjunctionOptions{koreLogOptions} = options
+
+koreMatchDisjunction :: KoreMatchDisjunctionOptions -> Main ExitCode
+koreMatchDisjunction options = do
+    definition <- loadDefinitions [definitionFileName]
+    mainModule <- loadModule mainModuleName definition
+    matchPattern <- mainParseMatchPattern mainModule matchFileName
+    disjunctionPattern <-
+        mainParseDisjunctionPattern mainModule disjunctionFileName
+    final <-
+        clockSomethingIO "Executing" $
+            matchDisjunction mainModule matchPattern disjunctionPattern
+    lift $
+        renderResult
+            options
+            (unparse final)
+    return ExitSuccess
+  where
+    mainParseMatchPattern mainModule fileName =
+        mainParseSearchPattern mainModule fileName
+            <&> mkRewritingPattern
+    KoreMatchDisjunctionOptions
+        { definitionFileName
+        , disjunctionFileName
+        , matchFileName
+        , mainModuleName
+        } = options
+
+mainParseDisjunctionPattern ::
+    VerifiedModule StepperAttributes ->
+    String ->
+    Main [Pattern RewritingVariableName]
+mainParseDisjunctionPattern indexedModule patternFileName = do
+    purePattern <- mainPatternParseAndVerify indexedModule patternFileName
+    return $ parseDisjunction purePattern
+  where
+    parseDisjunction (Or_ _ term1 term2) =
+        parseDisjunction term1 <> parseDisjunction term2
+    parseDisjunction term =
+        let patt =
+                mkRewritingPattern
+                    . Pattern.fromTermLike
+                    $ term
+         in [patt]
+
+renderResult :: KoreMatchDisjunctionOptions -> Doc ann -> IO ()
+renderResult KoreMatchDisjunctionOptions{outputFileName} doc =
+    case outputFileName of
+        Nothing -> putDoc doc
+        Just outputFile ->
+            withFile outputFile WriteMode (`hPutDoc` doc)

kore/app/share/GlobalMain.hs

@@ -22,6 +22,8 @@ module GlobalMain (
     LoadedModule,
     loadDefinitions,
     loadModule,
+    mainParseSearchPattern,
+    mainPatternParseAndVerify,
 ) where
 
 import Control.Exception (
@@ -58,13 +60,20 @@ import Kore.Attribute.Definition (
 import Kore.Attribute.SourceLocation (
     notDefault,
  )
+import Kore.Attribute.Symbol (
+    StepperAttributes,
+ )
 import qualified Kore.Attribute.Symbol as Attribute (
     Symbol,
  )
 import qualified Kore.Builtin as Builtin
 import Kore.IndexedModule.IndexedModule (
     VerifiedModule,
  )
+import Kore.Internal.Conditional (Conditional (..))
+import Kore.Internal.Pattern (Pattern)
+import Kore.Internal.Predicate (makePredicate)
+import Kore.Internal.TermLike (TermLike, pattern And_)
 import Kore.Log as Log
 import Kore.Log.ErrorParse (
     errorParse,
@@ -75,6 +84,7 @@ import Kore.Log.ErrorVerify (
 import Kore.Parser (
     ParsedPattern,
     parseKoreDefinition,
+    parseKorePattern,
  )
 import qualified Kore.Parser.Lexer as Lexer
 import Kore.Parser.ParserUtils (
@@ -83,7 +93,7 @@ import Kore.Parser.ParserUtils (
 import Kore.Rewrite.Strategy (
     GraphSearchOrder (..),
  )
-import Kore.Syntax
+import Kore.Syntax hiding (Pattern)
 import Kore.Syntax.Definition (
     ModuleName (..),
     ParsedDefinition,
@@ -130,6 +140,7 @@ import qualified Paths_kore as MetaData (
     version,
  )
 import Prelude.Kore
+import qualified Pretty as KorePretty
 import System.Clock (
     Clock (Monotonic),
     diffTimeSpec,
@@ -513,3 +524,39 @@ loadDefinitions filePaths =
 
 loadModule :: ModuleName -> LoadedDefinition -> Main LoadedModule
 loadModule moduleName = lookupMainModule moduleName . indexedModules
+
+mainParseSearchPattern ::
+    VerifiedModule StepperAttributes ->
+    String ->
+    Main (Pattern VariableName)
+mainParseSearchPattern indexedModule patternFileName = do
+    purePattern <- mainPatternParseAndVerify indexedModule patternFileName
+    case purePattern of
+        And_ _ term predicateTerm ->
+            return
+                Conditional
+                    { term
+                    , predicate =
+                        either
+                            (error . show . KorePretty.pretty)
+                            id
+                            (makePredicate predicateTerm)
+                    , substitution = mempty
+                    }
+        _ -> error "Unexpected non-conjunctive pattern"
+
+{- | IO action that parses a kore pattern from a filename, verifies it,
+ converts it to a pure pattern, and prints timing information.
+-}
+mainPatternParseAndVerify ::
+    VerifiedModule StepperAttributes ->
+    String ->
+    Main (TermLike VariableName)
+mainPatternParseAndVerify indexedModule patternFileName =
+    mainPatternParse patternFileName >>= mainPatternVerify indexedModule
+
+{- | IO action that parses a kore pattern from a filename and prints timing
+ information.
+-}
+mainPatternParse :: String -> Main ParsedPattern
+mainPatternParse = mainParse parseKorePattern