From 50903c820e008402be9d91432e4587bad758de59 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Wed, 18 Oct 2023 21:25:50 +1100 Subject: [PATCH 1/2] Small tweaks to diff replacement code (#341) * not using a library from 2018 * catching unexpected `diff` process results We could go further and * eliminate `unsafePerformIO` * only store the actual diff output inside `TextDiff` or `JsonDiff` (the diff should always be non-empty) --- cabal.project.freeze | 1 - library/Booster/JsonRpc/Utils.hs | 28 ++++++++++++++-------------- package.yaml | 2 -- 3 files changed, 14 insertions(+), 17 deletions(-) diff --git a/cabal.project.freeze b/cabal.project.freeze index b22c69814..534876c13 100644 --- a/cabal.project.freeze +++ b/cabal.project.freeze @@ -1,6 +1,5 @@ active-repositories: hackage.haskell.org:merge constraints: any.Cabal ==3.6.3.0, - any.Diff ==0.4.1, any.Glob ==0.10.2, any.HUnit ==1.6.2.0, any.OneTuple ==0.3.1, diff --git a/library/Booster/JsonRpc/Utils.hs b/library/Booster/JsonRpc/Utils.hs index 8032848f8..ef57c069c 100644 --- a/library/Booster/JsonRpc/Utils.hs +++ b/library/Booster/JsonRpc/Utils.hs @@ -21,8 +21,9 @@ import Data.Aeson.Types (parseMaybe) import Data.ByteString.Lazy.Char8 qualified as BS import Data.Maybe (fromMaybe) import Network.JSONRPC -import System.IO (hFlush) -import System.IO.Temp (withSystemTempFile) +import System.Exit (ExitCode (..)) +import System.FilePath +import System.IO.Extra (withTempDir) import System.IO.Unsafe (unsafePerformIO) import System.Process (readProcessWithExitCode) @@ -201,17 +202,16 @@ rpcTypeOf = \case Cancel -> error "Cancel" ------------------------------------------------------------------- --- pretty diff output --- Currently using a String-based module from the Diff package but --- which should be rewritten to handle Text and Char8.ByteString +-- doing the actual diff when output is requested renderDiff :: BS.ByteString -> BS.ByteString -> BS.ByteString -renderDiff first second = unsafePerformIO $ do - withSystemTempFile "diff_file1.txt" $ \path1 handle1 -> do - withSystemTempFile "diff_file2.txt" $ \path2 handle2 -> do - BS.hPut handle1 first - BS.hPut handle2 second - hFlush handle1 - hFlush handle2 - (_, str, _) <- readProcessWithExitCode "diff" ["-w", path1, path2] "" - return $ BS.pack str +renderDiff first second = unsafePerformIO . withTempDir $ \dir -> do + let path1 = dir "diff_file1.txt" + path2 = dir "diff_file2.txt" + BS.writeFile path1 first + BS.writeFile path2 second + (result, str, _) <- readProcessWithExitCode "diff" ["-w", path1, path2] "" + case result of + ExitSuccess -> error "Unexpected result: identical content" + ExitFailure 1 -> pure $ BS.pack str + ExitFailure n -> error $ "diff process exited with code " <> show n diff --git a/package.yaml b/package.yaml index 8a1c8af25..368deb780 100644 --- a/package.yaml +++ b/package.yaml @@ -71,7 +71,6 @@ library: - containers - deepseq - deriving-aeson - - Diff - exceptions - extra - filepath @@ -93,7 +92,6 @@ library: - stm-conduit - syb - template-haskell - - temporary - text - transformers - unix From 0cc3ef5ccde0535828065e8acdf976149ed36e42 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 18 Oct 2023 07:29:49 -0500 Subject: [PATCH 2/2] remove \left-assoc and \right-assoc of \and and \or (#337) Blocked on https://github.com/runtimeverification/k/pull/3679 This completes the changes to the booster with respect to multi-ary \and and \or. Once the \left-assoc and \right-assoc syntax are no longer being emitted by the frontend, we can remove them from the backends. --------- Co-authored-by: devops Co-authored-by: rv-jenkins --- cabal.project | 4 +-- deps/haskell-backend_release | 2 +- deps/k_release | 2 +- flake.lock | 8 +++--- flake.nix | 2 +- library/Booster/Syntax/ParsedKore/Parser.y | 21 -------------- stack.yaml | 2 +- stack.yaml.lock | 10 +++---- test/rpc-integration/resources/diamond.kore | 24 ++++++++-------- .../resources/substitutions.kore | 28 +++++++++---------- 10 files changed, 41 insertions(+), 62 deletions(-) diff --git a/cabal.project b/cabal.project index d2d3e8a77..ff2389e9e 100644 --- a/cabal.project +++ b/cabal.project @@ -17,7 +17,7 @@ source-repository-package source-repository-package type: git location: https://github.com/runtimeverification/haskell-backend.git - tag: 3e1dd2a92e8a1f537260fe347f2d93462235d229 - --sha256: sha256-6Jfoa9vocBdhqrNLdX7aC2a5guixAj8CQUH9clw26Sg= + tag: c209383c259aee0ca8b0859a4160d5c5757721b6 + --sha256: sha256-GOf7T8VeC3sdpxNf5QyjzDWHAYeIZfbyCLd1aJVvfTI= subdir: kore kore-rpc-types diff --git a/deps/haskell-backend_release b/deps/haskell-backend_release index 8e552d633..ac02d2d44 100644 --- a/deps/haskell-backend_release +++ b/deps/haskell-backend_release @@ -1 +1 @@ -3e1dd2a92e8a1f537260fe347f2d93462235d229 +c209383c259aee0ca8b0859a4160d5c5757721b6 diff --git a/deps/k_release b/deps/k_release index ec729cdb0..48097dc02 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.0.125 +6.0.146 diff --git a/flake.lock b/flake.lock index f34521450..9427fddb7 100644 --- a/flake.lock +++ b/flake.lock @@ -193,17 +193,17 @@ "z3-src": "z3-src" }, "locked": { - "lastModified": 1697220192, - "narHash": "sha256-S28zhfxcxpuSN2oTC9t3aZ0HjxuZe7E/PuJPtem4Koc=", + "lastModified": 1697540559, + "narHash": "sha256-L7hjOmkUx/NOUy/T0FtKgsNU1/adXw76X17fTBZAPDE=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "3e1dd2a92e8a1f537260fe347f2d93462235d229", + "rev": "c209383c259aee0ca8b0859a4160d5c5757721b6", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "3e1dd2a92e8a1f537260fe347f2d93462235d229", + "rev": "c209383c259aee0ca8b0859a4160d5c5757721b6", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 8e83f6bc8..c8f97fba0 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "hs-backend-booster"; inputs = { - haskell-backend.url = "github:runtimeverification/haskell-backend/3e1dd2a92e8a1f537260fe347f2d93462235d229"; + haskell-backend.url = "github:runtimeverification/haskell-backend/c209383c259aee0ca8b0859a4160d5c5757721b6"; haskell-nix.follows = "haskell-backend/haskell-nix"; nixpkgs.follows = "haskell-backend/haskell-nix/nixpkgs-unstable"; flake-compat = { diff --git a/library/Booster/Syntax/ParsedKore/Parser.y b/library/Booster/Syntax/ParsedKore/Parser.y index 0d0f98f58..d3fc4cf80 100644 --- a/library/Booster/Syntax/ParsedKore/Parser.y +++ b/library/Booster/Syntax/ParsedKore/Parser.y @@ -206,24 +206,8 @@ StringLiteral :: { Text } ApplicationPattern :: { KorePattern } : leftAssoc '{' '}' '(' ident SortsBrace NePatterns ')' { mkAssoc True $5 $6 $7 } - | leftAssoc '{' '}' '(' and SortsBrace NePatterns ')' - { mkAssoc True $5 $6 $7 } - | leftAssoc '{' '}' '(' or SortsBrace NePatterns ')' - { mkAssoc True $5 $6 $7 } - | leftAssoc '{' '}' '(' implies SortsBrace NePatterns ')' - { mkAssoc True $5 $6 $7 } - | leftAssoc '{' '}' '(' iff SortsBrace NePatterns ')' - { mkAssoc True $5 $6 $7 } | rightAssoc '{' '}' '(' ident SortsBrace NePatterns ')' { mkAssoc False $5 $6 $7 } - | rightAssoc '{' '}' '(' and SortsBrace NePatterns ')' - { mkAssoc False $5 $6 $7 } - | rightAssoc '{' '}' '(' or SortsBrace NePatterns ')' - { mkAssoc False $5 $6 $7 } - | rightAssoc '{' '}' '(' implies SortsBrace NePatterns ')' - { mkAssoc False $5 $6 $7 } - | rightAssoc '{' '}' '(' iff SortsBrace NePatterns ')' - { mkAssoc False $5 $6 $7 } | top '{' Sort '}' '(' ')' { KJTop {sort = $3} } | bottom '{' Sort '}' '(' ')' @@ -419,11 +403,6 @@ the result. Namely, \\and, \\or, \\implies, and \\iff. Designed to be passed to foldl1' or foldr1. -} mkApply :: Token -> [Sort] -> KorePattern -> KorePattern -> KorePattern -mkApply tok [sort] first second - | Token _ TokenAnd <- tok = KJAnd sort [first, second] - | Token _ TokenOr <- tok = KJOr sort [first, second] - | Token _ TokenImplies <- tok = KJImplies sort first second - | Token _ TokenIff <- tok = KJIff sort first second mkApply tok sorts@[_, _] first second | Token _ (TokenIdent _) <- tok = KJApp (mkId tok) sorts [first, second] mkApply other _ _ _ = error $ "mkApply: unsupported token " <> show other diff --git a/stack.yaml b/stack.yaml index a5ce1e17f..ecf60347d 100644 --- a/stack.yaml +++ b/stack.yaml @@ -11,7 +11,7 @@ extra-deps: - typerep-map-0.5.0.0 - monad-validate-1.2.0.1 - git: https://github.com/runtimeverification/haskell-backend.git - commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229 + commit: c209383c259aee0ca8b0859a4160d5c5757721b6 subdirs: - kore - kore-rpc-types diff --git a/stack.yaml.lock b/stack.yaml.lock index 7b5da8f48..b8c0c9555 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -40,20 +40,20 @@ packages: original: hackage: monad-validate-1.2.0.1 - completed: - commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229 + commit: c209383c259aee0ca8b0859a4160d5c5757721b6 git: https://github.com/runtimeverification/haskell-backend.git name: kore pantry-tree: - sha256: 6c277d8786183e157d20488aef9f76fe5b7a4cdb6da5b4b9965a1d15a2e1b1cb + sha256: a6d0a2d6a079a06a1988249ced87ce7ddd58ab6bf151e3a8861f18b263f66f32 size: 44685 subdir: kore version: 0.60.0.0 original: - commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229 + commit: c209383c259aee0ca8b0859a4160d5c5757721b6 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore - completed: - commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229 + commit: c209383c259aee0ca8b0859a4160d5c5757721b6 git: https://github.com/runtimeverification/haskell-backend.git name: kore-rpc-types pantry-tree: @@ -62,7 +62,7 @@ packages: subdir: kore-rpc-types version: 0.60.0.0 original: - commit: 3e1dd2a92e8a1f537260fe347f2d93462235d229 + commit: c209383c259aee0ca8b0859a4160d5c5757721b6 git: https://github.com/runtimeverification/haskell-backend.git subdir: kore-rpc-types snapshots: diff --git a/test/rpc-integration/resources/diamond.kore b/test/rpc-integration/resources/diamond.kore index be6f12fe4..4822692f3 100644 --- a/test/rpc-integration/resources/diamond.kore +++ b/test/rpc-integration/resources/diamond.kore @@ -318,18 +318,18 @@ module TEST axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(K0:SortSet{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Tild'Int'Unds'{}(K0:SortInt{}))) [functional{}()] // functional - axiom{} \right-assoc{}(\or{SortKItem{}} (\exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \right-assoc{}(\or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \right-assoc{}(\or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \right-assoc{}(\or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk + axiom{} \or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk + axiom{} \or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) // rules // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1369,8,1369,102)), org.kframework.attributes.Source(Source(/nix/store/392hsax8839a1kk18xkx3cs4hvz3411w-k-6.0.87-3997d65c227fde4e67cedfca83a8a2d2436229e6-maven/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})] diff --git a/test/rpc-integration/resources/substitutions.kore b/test/rpc-integration/resources/substitutions.kore index b7b599e05..f87bd4001 100644 --- a/test/rpc-integration/resources/substitutions.kore +++ b/test/rpc-integration/resources/substitutions.kore @@ -335,20 +335,20 @@ module TEST axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(K0:SortSet{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Tild'Int'Unds'{}(K0:SortInt{}))) [functional{}()] // functional - axiom{} \right-assoc{}(\or{SortJntCellOpt{}} (LblnoJntCell{}(), \exists{SortJntCellOpt{}} (Val:SortJntCell{}, inj{SortJntCell{}, SortJntCellOpt{}} (Val:SortJntCell{})), \bottom{SortJntCellOpt{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKItem{}} (\exists{SortKItem{}} (Val:SortJntCellOpt{}, inj{SortJntCellOpt{}, SortKItem{}} (Val:SortJntCellOpt{})), \exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortJntCell{}, inj{SortJntCell{}, SortKItem{}} (Val:SortJntCell{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \right-assoc{}(\or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \right-assoc{}(\or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortJntCell{}} (\exists{SortJntCell{}} (X0:SortInt{}, Lbl'-LT-'jnt'-GT-'{}(X0:SortInt{})), \bottom{SortJntCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) - axiom{} \right-assoc{}(\or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortJntCell{}, \exists{SortGeneratedTopCell{}} (X3:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortJntCell{}, X3:SortGeneratedCounterCell{}))))), \bottom{SortGeneratedTopCell{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X2:SortJntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}, X2:SortJntCellOpt{})))), \bottom{SortGeneratedTopCellFragment{}}())) [constructor{}()] // no junk - axiom{} \right-assoc{}(\or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}())) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortJntCellOpt{}} (LblnoJntCell{}(), \exists{SortJntCellOpt{}} (Val:SortJntCell{}, inj{SortJntCell{}, SortJntCellOpt{}} (Val:SortJntCell{})), \bottom{SortJntCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (Val:SortJntCellOpt{}, inj{SortJntCellOpt{}, SortKItem{}} (Val:SortJntCellOpt{})), \exists{SortKItem{}} (Val:SortIntCellOpt{}, inj{SortIntCellOpt{}, SortKItem{}} (Val:SortIntCellOpt{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortKItem{}} (Val:SortIntCell{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortJntCell{}, inj{SortJntCell{}, SortKItem{}} (Val:SortJntCell{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortState{}, inj{SortState{}, SortKItem{}} (Val:SortState{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk + axiom{} \or{SortIntCellOpt{}} (LblnoIntCell{}(), \exists{SortIntCellOpt{}} (Val:SortIntCell{}, inj{SortIntCell{}, SortIntCellOpt{}} (Val:SortIntCell{})), \bottom{SortIntCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortIntCell{}} (\exists{SortIntCell{}} (X0:SortInt{}, Lbl'-LT-'int'-GT-'{}(X0:SortInt{})), \bottom{SortIntCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortJntCell{}} (\exists{SortJntCell{}} (X0:SortInt{}, Lbl'-LT-'jnt'-GT-'{}(X0:SortInt{})), \bottom{SortJntCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortIntCell{}, \exists{SortGeneratedTopCell{}} (X2:SortJntCell{}, \exists{SortGeneratedTopCell{}} (X3:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortIntCell{}, X2:SortJntCell{}, X3:SortGeneratedCounterCell{}))))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortIntCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X2:SortJntCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortIntCellOpt{}, X2:SortJntCellOpt{})))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk + axiom{} \or{SortState{}} (\top{SortState{}}(), \bottom{SortState{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) // rules // rule #Ceil{Int,#SortParam}(`_%Int_`(@I1,@I2))=>#And{#SortParam}(#And{#SortParam}(#Equals{Bool,#SortParam}(`_=/=Int_`(@I2,#token("0","Int")),#token("true","Bool")),#Ceil{Int,#SortParam}(@I1)),#Ceil{Int,#SortParam}(@I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(277564ad2537209fd698729ceaa01973f97125176cf1078f98e2edb7cc190f34), org.kframework.attributes.Location(Location(1369,8,1369,102)), org.kframework.attributes.Source(Source(/nix/store/qwnhmnw5d9wc7df6fqz6mzrzbxqc9a8m-k-6.0.81-c48595825908f32e643816d929a5d4fa3a8b1227-maven/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification, sortParams({Q0})]