diff --git a/Makefile b/Makefile index 009d8890be6..bd0937f2cfc 100644 --- a/Makefile +++ b/Makefile @@ -2,11 +2,9 @@ include include.mk .PHONY: all kore clean clean-execution docs haddock \ test test-kore test-k test-k-simplifierx test-simplifierx \ - kore-exec kore-repl kore-parser kore-check-functions \ - kore-format kore-match-disjunction + kore-exec kore-repl -all: kore-exec kore-repl kore-parser kore-check-functions kore-format \ - kore-match-disjunction +all: kore-exec kore-repl kore: all @@ -14,14 +12,6 @@ kore-exec: $(KORE_EXEC) kore-repl: $(KORE_REPL) -kore-parser: $(KORE_PARSER) - -kore-check-functions: $(KORE_CHECK_FUNCTIONS) - -kore-format: $(KORE_FORMAT) - -kore-match-disjunction: $(KORE_MATCH_DISJUNCTION) - docs: haddock haddock: diff --git a/kore/app/match-disjunction/Main.hs b/dev-tools/kore-match-disjunction/Main.hs similarity index 98% rename from kore/app/match-disjunction/Main.hs rename to dev-tools/kore-match-disjunction/Main.hs index 3a92f8c84e0..ad2517d947b 100644 --- a/kore/app/match-disjunction/Main.hs +++ b/dev-tools/kore-match-disjunction/Main.hs @@ -1,3 +1,6 @@ +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE NoImplicitPrelude #-} + module Main (main) where import GlobalMain diff --git a/kore/app/parser/Main.hs b/dev-tools/kore-parser/Main.hs similarity index 99% rename from kore/app/parser/Main.hs rename to dev-tools/kore-parser/Main.hs index ad0ffd2cf87..3fd0d68fac3 100644 --- a/kore/app/parser/Main.hs +++ b/dev-tools/kore-parser/Main.hs @@ -1,3 +1,5 @@ +{-# LANGUAGE NoImplicitPrelude #-} + module Main (main) where import Control.Monad.Catch ( diff --git a/dev-tools/package.yaml b/dev-tools/package.yaml index 756e553c10f..f014c4ef490 100644 --- a/dev-tools/package.yaml +++ b/dev-tools/package.yaml @@ -86,7 +86,7 @@ executables: - text - transformers ghc-options: - - -rtsopts + - -rtsopts parsetest-binary: source-dirs: parsetest-binary main: ParsetestBinary.hs @@ -98,7 +98,7 @@ executables: - hs-backend-booster - text ghc-options: - - -rtsopts + - -rtsopts pretty: source-dirs: pretty main: Pretty.hs @@ -111,7 +111,7 @@ executables: - text - transformers ghc-options: - - -rtsopts + - -rtsopts eventlog-parser: source-dirs: eventlog-parser main: EventlogParser.hs @@ -132,7 +132,7 @@ executables: - unix - unordered-containers ghc-options: - - -rtsopts + - -rtsopts kore-json-differ: source-dirs: kore-json-differ main: Main.hs @@ -141,6 +141,8 @@ executables: - bytestring - containers - hs-backend-booster + ghc-options: + - -rtsopts tarball-compare: source-dirs: tarball-compare main: Main @@ -189,3 +191,25 @@ executables: - -rtsopts - -threaded - -with-rtsopts=-N + kore-match-disjunction: + source-dirs: kore-match-disjunction + main: Main.hs + dependencies: + - base + - clock + - kore + - optparse-applicative + - transformers + ghc-options: + - -rtsopts + kore-parser: + source-dirs: kore-parser + main: Main.hs + dependencies: + - base + - bytestring + - containers + - exceptions + - kore + ghc-options: + - -rtsopts diff --git a/flake.nix b/flake.nix index e585fab99e2..e50b11aaa6d 100644 --- a/flake.nix +++ b/flake.nix @@ -73,8 +73,6 @@ ''; postInstall = '' ${drv.postInstall or ""} - rm $out/bin/kore-check-functions - rm $out/bin/kore-format ''; })).override { # bit pathological, but ghc-compact is already included with the ghc compiler @@ -237,10 +235,12 @@ haskell.lib.justStaticExecutables haskell-backend.pkgSet.kore; hs-backend-booster = with pkgs; haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster; + hs-backend-booster-dev-tools = with pkgs; + haskell.lib.justStaticExecutables haskell-backend.pkgSet.hs-backend-booster-dev-tools; in { kore-exec = withZ3 pkgs kore "kore-exec"; - kore-match-disjunction = withZ3 pkgs kore "kore-match-disjunction"; - kore-parser = withZ3 pkgs kore "kore-parser"; + kore-match-disjunction = withZ3 pkgs hs-backend-booster-dev-tools "kore-match-disjunction"; + kore-parser = withZ3 pkgs hs-backend-booster-dev-tools "kore-parser"; kore-repl = withZ3 pkgs kore "kore-repl"; kore-rpc = withZ3 pkgs kore "kore-rpc"; kore-rpc-booster = withZ3 pkgs hs-backend-booster "kore-rpc-booster"; diff --git a/include.mk b/include.mk index 478686aa51d..e35d22c0c5b 100644 --- a/include.mk +++ b/include.mk @@ -59,20 +59,8 @@ KORE_REPL_OPTS = --no-bug-report export KORE_REPL export KORE_REPL_OPTS -KORE_CHECK_FUNCTIONS = $(BUILD_DIR)/kore/bin/kore-check-functions -KORE_CHECK_FUNCTIONS_OPTS = --no-bug-report -export KORE_CHECK_FUNCTIONS -export KORE_CHECK_FUNCTIONS_OPTS - -KORE_FORMAT = $(BUILD_DIR)/kore/bin/kore-format -KORE_FORMAT_OPTS = --no-bug-report -export KORE_FORMAT -export KORE_FORMAT_OPTS - -KORE_MATCH_DISJUNCTION = $(BUILD_DIR)/kore/bin/kore-match-disjunction -KORE_MATCH_DISJUNCTION_OPTS = --no-bug-report -export KORE_MATCH_DISJUNCTION -export KORE_MATCH_DISJUNCTION_OPTS +$(BUILD_DIR)/kore/bin/kore-parser: + $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins hs-backend-booster-dev-tools:exe:kore-parser $(BUILD_DIR)/kore/bin/kore-exec: $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-exec @@ -80,14 +68,4 @@ $(BUILD_DIR)/kore/bin/kore-exec: $(BUILD_DIR)/kore/bin/kore-repl: $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-repl -$(BUILD_DIR)/kore/bin/kore-parser: - $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-parser - -$(BUILD_DIR)/kore/bin/kore-check-functions: - $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-check-functions - -$(BUILD_DIR)/kore/bin/kore-format: - $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-format -$(BUILD_DIR)/kore/bin/kore-match-disjunction: - $(STACK) $(STACK_BUILD) $(STACK_NO_PROFILE) --copy-bins kore:exe:kore-match-disjunction diff --git a/kore/Makefile b/kore/Makefile index cc8269fb731..c48ff8c49ea 100644 --- a/kore/Makefile +++ b/kore/Makefile @@ -46,21 +46,6 @@ 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" - -ghcid-check-func: - $(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-check-functions --work-dir .stack-work-ghci" - -ghcid-parser: - $(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-parser --work-dir .stack-work-ghci" - -ghcid-format: - $(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-format --work-dir .stack-work-ghci" - -ghcid-simplify: - $(stack) exec -- ghcid -c "stack ghci $(package) --test --ghci-options='-fobject-code -fno-warn-unused-do-bind' --main-is $(package):kore-simplify --work-dir .stack-work-ghci" - dev-deps: stack install ghcid diff --git a/kore/README.md b/kore/README.md deleted file mode 100644 index b8fa0da95fe..00000000000 --- a/kore/README.md +++ /dev/null @@ -1,37 +0,0 @@ -# Kore parser - -To build: `stack build`. -All dependencies are managed by stack. - -To run: `stack exec kore-parser FILE`. - -To run the tests: -`stack test --coverage` -or -`stack test --no-keep-going` -or -`stack test --test-arguments --hide-successes`. -If you need stack traces, then you probably want something like -`stack test --executable-profiling --test-arguments --hide-successes` - -To regenerate the golden data for regression tests: -`stack test --no-keep-going --ta --accept` - -To generate documentation: `stack build --haddock`. - -To test parsing performance: - -1. Run the command at the top of `src/test/performance/parsing-base.almost-kore` - to generate input files. -1. `stack build` -1. `time stack exec kore-parser ../src/test/performance/parsing-512.kore -- --noverify --noprint` - -## Debugging - -If building the test suite fails with some undecipherable error, add - -> -optF --debug - -to the `OPTION_GHC` pragma in `test/parser/Driver.hs`. The option will cause -`tasty-debug` to print the generated source code to the terminal; hopefully, -this reveals the error. diff --git a/kore/app/check-functions/Main.hs b/kore/app/check-functions/Main.hs deleted file mode 100644 index 1fa535f6ce1..00000000000 --- a/kore/app/check-functions/Main.hs +++ /dev/null @@ -1,153 +0,0 @@ -{- | -Copyright : (c) Runtime Verification, 2021 -License : BSD-3-Clause - -The @kore-check-functions@ executable checks the following properties of -function definitions: -1. For every equation in a function definition, the right-hand side of the -equation is a function pattern. -2. For every pair of equations in a function definition, the equations cannot -match the same term. --} -module Main (main) where - -import Control.Monad.Catch ( - handle, - ) -import GlobalMain ( - ExeName (..), - LocalOptions (..), - loadDefinitions, - loadModule, - localOptions, - mainGlobal, - parseModuleName, - ) -import Kore.BugReport ( - BugReportOption, - ExitCode (..), - parseBugReportOption, - withBugReport, - ) -import Kore.Exec ( - checkFunctions, - ) -import Kore.Log ( - KoreLogOptions, - parseKoreLogOptions, - runKoreLog, - ) -import Kore.Log.ErrorException ( - handleSomeException, - ) -import Kore.Options ( - InfoMod, - Parser, - argument, - fullDesc, - header, - help, - metavar, - progDesc, - str, - ) -import Kore.Syntax.Module ( - ModuleName, - ) -import Prelude.Kore -import SMT ( - defaultConfig, - runSMT, - ) -import System.Clock ( - Clock (Monotonic), - TimeSpec, - getTime, - ) -import System.Exit ( - exitWith, - ) - --- | Modifiers for the command line parser description -checkerInfoModifiers :: InfoMod options -checkerInfoModifiers = - fullDesc - <> progDesc - "Checks function definitions in FILE and verifies the following \ - \properties: \ - \1. For every equation in a function definition, the right-hand \ - \side of the equation is a function pattern. \ - \2. For every pair of equations in a function definition, the \ - \equations cannot match the same term." - <> header "kore-check-functions - a tool to check function definitions" - -data KoreCheckerOptions = KoreCheckerOptions - { fileName :: !FilePath - -- ^ Name for a file containing function definitions to verify. - , mainModuleName :: !ModuleName - -- ^ Name of the main module in the definition - , bugReportOption :: !BugReportOption - , koreLogOptions :: !KoreLogOptions - } - -parseKoreCheckerOptions :: TimeSpec -> Parser KoreCheckerOptions -parseKoreCheckerOptions startTime = - KoreCheckerOptions - <$> argument - str - ( metavar "FILE" - <> help "Kore source file to check." - ) - <*> parseMainModuleName - <*> parseBugReportOption - <*> parseKoreLogOptions exeName startTime - where - parseMainModuleName = - parseModuleName - "MODULE" - "module" - "The name of the main module in the Kore definition." - --- | Executable name -exeName :: ExeName -exeName = ExeName "kore-check-functions" - --- | Environment variable name for extra arguments -envName :: String -envName = "KORE_CHECK_FUNCTIONS_OPTS" - -main :: IO () -main = do - startTime <- getTime Monotonic - options <- - mainGlobal - exeName - (Just envName) -- environment variable name for extra arguments - (parseKoreCheckerOptions startTime) - checkerInfoModifiers - mapM_ mainWithOptions $ localOptions options - -mainWithOptions :: LocalOptions KoreCheckerOptions -> IO () -mainWithOptions localOptions@LocalOptions{execOptions} = - withBugReport - exeName - (bugReportOption execOptions) - (koreCheckFunctions localOptions) - >>= exitWith - -koreCheckFunctions :: LocalOptions KoreCheckerOptions -> FilePath -> IO ExitCode -koreCheckFunctions LocalOptions{execOptions} tmpDir = - do - definitions <- loadDefinitions [fileName] - loadedModule <- loadModule mainModuleName definitions - checkFunctions loadedModule - & SMT.runSMT defaultConfig (pure ()) - return ExitSuccess - & handle handleSomeException - & runKoreLog tmpDir koreLogOptions - where - KoreCheckerOptions - { fileName - , mainModuleName - , koreLogOptions - } = execOptions diff --git a/kore/app/format/Main.hs b/kore/app/format/Main.hs deleted file mode 100644 index d1b1f80b2e8..00000000000 --- a/kore/app/format/Main.hs +++ /dev/null @@ -1,84 +0,0 @@ -module Main (main) where - -import Data.Text.IO qualified as Text -import GlobalMain -import Kore.Parser ( - parseKoreDefinition, - ) -import Kore.Syntax.Definition ( - ParsedDefinition, - ) -import Kore.Unparser -import Options.Applicative -import Prelude.Kore -import Pretty ( - LayoutOptions (..), - PageWidth (..), - defaultLayoutOptions, - layoutPretty, - renderIO, - ) -import System.IO ( - stdout, - ) - -data KoreFormatOptions = KoreFormatOptions - { fileName :: FilePath - -- ^ file to unparse - , width :: Int - -- ^ line width - } - -commandLine :: Parser KoreFormatOptions -commandLine = - KoreFormatOptions - <$> argument - str - ( metavar "FILE" - <> help "Kore source file to parse" - ) - <*> option - auto - ( metavar "WIDTH" - <> long "width" - <> value 80 - <> help "Line width [default: 80; unlimited if WIDTH <= 0]" - ) - -infoMod :: InfoMod options -infoMod = - fullDesc - <> progDesc "Parse a Kore definition and render it in standard format" - <> header "kore-format - parse and render Kore definitions" - -main :: IO () -main = do - options <- - mainGlobal - (ExeName "kore-format") - Nothing -- environment variable name for extra arguments - commandLine - infoMod - for_ (localOptions options) mainWorker - where - mainWorker - LocalOptions - { execOptions = - KoreFormatOptions{fileName, width} - } = - do - defn <- readKoreOrDie fileName - let layoutOptions = - defaultLayoutOptions - { layoutPageWidth = - if width > 0 - then AvailablePerLine width 1.0 - else Unbounded - } - renderIO stdout (layoutPretty layoutOptions $ unparse defn) - --- | Read a 'KoreDefinition' from the given file name or signal an error. -readKoreOrDie :: FilePath -> IO ParsedDefinition -readKoreOrDie fileName = - Text.readFile fileName - >>= either error return . parseKoreDefinition fileName diff --git a/kore/app/simplify/Main.hs b/kore/app/simplify/Main.hs deleted file mode 100644 index 763426234b7..00000000000 --- a/kore/app/simplify/Main.hs +++ /dev/null @@ -1,173 +0,0 @@ -module Main (main) where - -import GlobalMain -import Kore.Attribute.Symbol ( - StepperAttributes, - ) -import Kore.BugReport -import Kore.Exec (simplify) -import Kore.IndexedModule.IndexedModule ( - IndexedModule (..), - VerifiedModule, - ) -import Kore.IndexedModule.MetadataToolsBuilder qualified as MetadataTools ( - build, - ) -import Kore.Internal.Pattern (Pattern) -import Kore.Internal.Pattern qualified as Pattern -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-simplify" - -envName :: String -envName = "KORE_SIMPLIFY_OPTS" - -data KoreSimplifyOptions = KoreSimplifyOptions - { definitionFileName :: !FilePath - -- ^ Name of file containing a definition to verify - , patternFileName :: !FilePath - -- ^ Name of file containing a pattern to verify and simplify - , outputFileName :: !(Maybe FilePath) - -- ^ Name for file to contain the output pattern - , mainModuleName :: !ModuleName - -- ^ The name of the main module in the definition - , bugReportOption :: !BugReportOption - , koreLogOptions :: !KoreLogOptions - } - -parseKoreSimplifyOptions :: TimeSpec -> Parser KoreSimplifyOptions -parseKoreSimplifyOptions startTime = - KoreSimplifyOptions - <$> argument - str - ( metavar "DEFINITION_FILE" - <> help "Kore definition file to verify and use for execution." - ) - <*> strOption - ( metavar "PATTERN_INPUT_FILE" - <> long "pattern" - <> help "File containing a pattern." - ) - <*> 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 "Simplifies and validates the Kore pattern in PATTERN_INPUT_FILE" - <> header "kore-simplify - a tool for simplifying patterns" - -main :: IO () -main = do - startTime <- getTime Monotonic - options <- - mainGlobal - exeName - (Just envName) - (parseKoreSimplifyOptions startTime) - parserInfoModifiers - for_ (localOptions options) mainWithOptions - -mainWithOptions :: LocalOptions KoreSimplifyOptions -> IO () -mainWithOptions localOptions@LocalOptions{execOptions} = do - exitCode <- - withBugReport exeName bugReportOption $ \tmpDir -> - koreSimplify localOptions - & runKoreLog tmpDir koreLogOptions - exitWith exitCode - where - KoreSimplifyOptions{bugReportOption, koreLogOptions} = execOptions - -koreSimplify :: LocalOptions KoreSimplifyOptions -> Main ExitCode -koreSimplify LocalOptions{execOptions} = do - definition <- loadDefinitions [definitionFileName] - mainModule <- loadModule mainModuleName definition - inputPattern <- - mainParseInputPattern mainModule patternFileName - final <- simplify inputPattern - lift $ - renderResult - execOptions - (unparse final) - return ExitSuccess - where - KoreSimplifyOptions - { definitionFileName - , patternFileName - , mainModuleName - } = execOptions - -mainParseInputPattern :: - VerifiedModule StepperAttributes -> - String -> - Main (Pattern RewritingVariableName) -mainParseInputPattern indexedModule patternFileName = do - let metadataTools = MetadataTools.build indexedModule - purePattern <- - mainPatternParseAndVerify metadataTools (indexedModuleSyntax indexedModule) patternFileName - return $ parsePattern purePattern - where - parsePattern = mkRewritingPattern . Pattern.fromTermLike - -renderResult :: KoreSimplifyOptions -> Doc ann -> IO () -renderResult KoreSimplifyOptions{outputFileName} doc = - case outputFileName of - Nothing -> putDoc doc - Just outputFile -> - withFile outputFile WriteMode (`hPutDoc` doc) diff --git a/kore/kore.cabal b/kore/kore.cabal index e76ed85bf0c..b57429cccc1 100644 --- a/kore/kore.cabal +++ b/kore/kore.cabal @@ -617,25 +617,6 @@ executable kore-rpc build-depends: optparse-applicative >=0.14 build-depends: time >=1.9.3 -executable kore-format - import: haskell - import: exe - main-is: Main.hs - hs-source-dirs: app/format - build-depends: kore - build-depends: optparse-applicative >=0.14 - build-depends: text >=1.2 - -executable kore-parser - import: haskell - import: exe - main-is: Main.hs - hs-source-dirs: app/parser - build-depends: kore - build-depends: bytestring >=0.10 - build-depends: containers >=0.5 - build-depends: exceptions >=0.10 - executable kore-repl import: haskell import: exe @@ -648,34 +629,6 @@ executable kore-repl build-depends: filepath >=1.4 build-depends: optparse-applicative >=0.14 -executable kore-match-disjunction - import: haskell - import: exe - main-is: Main.hs - hs-source-dirs: app/match-disjunction - build-depends: kore - build-depends: clock >=0.8 - build-depends: optparse-applicative >=0.14 - build-depends: transformers >= 0.5 - -executable kore-check-functions - import: haskell - import: exe - main-is: Main.hs - hs-source-dirs: app/check-functions - build-depends: kore - build-depends: clock >=0.8 - build-depends: exceptions >=0.10 - -executable kore-simplify - import: haskell - import: exe - main-is: Main.hs - hs-source-dirs: app/simplify - build-depends: kore - build-depends: clock >=0.8 - build-depends: optparse-applicative >=0.14 - test-suite kore-test import: haskell import: library