From c209383c259aee0ca8b0859a4160d5c5757721b6 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 17 Oct 2023 06:02:39 -0500 Subject: [PATCH] remove parsing of \left-assoc and \right-assoc of \and and \or (#3675) 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. ### Scope: ### Estimate: --- ###### Review checklist The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed. - [ ] **Summary.** Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history. - [ ] **Documentation.** Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing. - [ ] **Tests.** Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests. - [ ] **Clean up.** The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes! --------- Co-authored-by: rv-jenkins --- kore/src/Kore/Parser/Parser.y | 24 ------------------------ test/issue-3508/disjunction.kore | 2 +- 2 files changed, 1 insertion(+), 25 deletions(-) diff --git a/kore/src/Kore/Parser/Parser.y b/kore/src/Kore/Parser/Parser.y index fd62df0944..50d06600f7 100644 --- 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 index c890190923..06eb46ca19 100644 --- 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"))))