Merge branch 'master' into sam/slim-nix

runtimeverification · Oct 17, 2023 · 4c5a80e · 4c5a80e
2 parents 3cd32d1 + c209383
commit 4c5a80e
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 25 deletions.
diff --git a/kore/src/Kore/Parser/Parser.y b/kore/src/Kore/Parser/Parser.y
@@ -227,24 +227,8 @@ StringLiteral :: {StringLiteral}
 ApplicationPattern :: {ParsedPattern}
 		    : 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 '}' '(' ')'
                       { embedParsedPattern $ TopF Top{topSort = $3} }
                     | bottom '{' Sort '}' '(' ')'
@@ -442,14 +426,6 @@ the result. Namely, \\and, \\or, \\implies, and \\iff. Designed to be passed to
 foldl1' or foldr1.
 -}
 mkApply :: Token -> [Sort] -> ParsedPattern -> ParsedPattern -> ParsedPattern
-mkApply tok@(Token _ TokenAnd) [andSort] andFirst andSecond =
-    embedParsedPattern $ AndF And{andSort, andChildren=[andFirst, andSecond]}
-mkApply tok@(Token _ TokenOr) [orSort] orFirst orSecond =
-    embedParsedPattern $ OrF Or{orSort, orChildren=[orFirst, orSecond]}
-mkApply tok@(Token _ TokenImplies) [impliesSort] impliesFirst impliesSecond =
-    embedParsedPattern $ ImpliesF Implies{impliesSort, impliesFirst, impliesSecond}
-mkApply tok@(Token _ TokenIff) [iffSort] iffFirst iffSecond =
-    embedParsedPattern $ IffF Iff{iffSort, iffFirst, iffSecond}
 mkApply tok@(Token _ (TokenIdent _)) sorts first second =
     embedParsedPattern $ ApplicationF Application
        { applicationSymbolOrAlias = SymbolOrAlias { symbolOrAliasConstructor = mkId tok

diff --git a/test/issue-3508/disjunction.kore b/test/issue-3508/disjunction.kore
@@ -1,2 +1,2 @@
-\left-assoc{}(\or{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'threads'-GT-'{}(\left-assoc{}(Lbl'Unds'ThreadCellMap'Unds'{}(LblThreadCellMapItem{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'thread'-GT-'{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'env'-GT-'{}(Lbl'Stop'Map{}())))))),Lbl'-LT-'store'-GT-'{}(Lbl'Stop'Map{}()),Lbl'-LT-'input'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("")),dotk{}())))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'istream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("0"))))))),Lbl'-LT-'output'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("1")))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("60")),dotk{}())))))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))))
+\or{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'threads'-GT-'{}(\left-assoc{}(Lbl'Unds'ThreadCellMap'Unds'{}(LblThreadCellMapItem{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'thread'-GT-'{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'env'-GT-'{}(Lbl'Stop'Map{}())))))),Lbl'-LT-'store'-GT-'{}(Lbl'Stop'Map{}()),Lbl'-LT-'input'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("")),dotk{}())))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'istream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("0"))))))),Lbl'-LT-'output'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("1")))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("60")),dotk{}())))))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))))
Original file line number	Diff line number	Diff line change
		@@ -1,2 +1,2 @@
		\left-assoc{}(\or{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'threads'-GT-'{}(\left-assoc{}(Lbl'Unds'ThreadCellMap'Unds'{}(LblThreadCellMapItem{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'thread'-GT-'{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'env'-GT-'{}(Lbl'Stop'Map{}())))))),Lbl'-LT-'store'-GT-'{}(Lbl'Stop'Map{}()),Lbl'-LT-'input'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("")),dotk{}())))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'istream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("0"))))))),Lbl'-LT-'output'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("1")))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("60")),dotk{}())))))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))))
		\or{SortGeneratedTopCell{}}(Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'threads'-GT-'{}(\left-assoc{}(Lbl'Unds'ThreadCellMap'Unds'{}(LblThreadCellMapItem{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'thread'-GT-'{}(Lbl'-LT-'id'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'env'-GT-'{}(Lbl'Stop'Map{}())))))),Lbl'-LT-'store'-GT-'{}(Lbl'Stop'Map{}()),Lbl'-LT-'input'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("")),dotk{}())))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'istream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("0"))))))),Lbl'-LT-'output'-GT-'{}(\left-assoc{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'ostream'LParUndsRParUnds'K-IO'Unds'Stream'Unds'Int{}(\dv{SortInt{}}("1")))),LblListItem{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("off"))),LblListItem{}(inj{SortStream{}, SortKItem{}}(Lbl'Hash'buffer'LParUndsRParUnds'K-IO'Unds'Stream'Unds'K{}(kseq{}(inj{SortString{}, SortKItem{}}(\dv{SortString{}}("60")),dotk{}())))))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))))