From 811e94fbcaef8550a6a709a9ce793f7166457911 Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 30 Oct 2023 20:57:26 +1100
Subject: [PATCH] re-enable parsing older definitions (or in *assoc) (#3688)

This change brings back parsing of `\*-assoc{}(\or, ...)` constructs
which were used in `definition.kore` files before October 2023.
---
 kore/src/Kore/Parser/Parser.y | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/kore/src/Kore/Parser/Parser.y b/kore/src/Kore/Parser/Parser.y
index 50d06600f7..eed68d4590 100644
--- a/kore/src/Kore/Parser/Parser.y
+++ b/kore/src/Kore/Parser/Parser.y
@@ -177,7 +177,7 @@ AliasHead :: {Alias}
 
 SymbolHead :: {Symbol}
 	    : Id SortVariables { Symbol $1 $2 }
-	
+
 SortVariables :: {[SortVariable]}
 	       : '{' SortVariableList '}' { reverse $2 }
                | '{' '}' { [] }
@@ -229,6 +229,11 @@ ApplicationPattern :: {ParsedPattern}
                       { mkAssoc True $5 $6 $7 }
                     | rightAssoc '{' '}' '(' ident SortsBrace NePatterns ')'
                       { mkAssoc False $5 $6 $7 }
+                    -- special cases for multi-or in definitions prior to Oct 2023
+                    | rightAssoc '{' '}' '(' or SortsBrace NePatterns ')'
+                      { mkAssoc False $5 $6 $7 }
+                    | leftAssoc '{' '}' '(' or SortsBrace NePatterns ')'
+                      { mkAssoc True $5 $6 $7 }
                     | top '{' Sort '}' '(' ')'
                       { embedParsedPattern $ TopF Top{topSort = $3} }
                     | bottom '{' Sort '}' '(' ')'
@@ -426,6 +431,8 @@ 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 _ TokenOr) [orSort] orFirst orSecond =
+    embedParsedPattern $ OrF Or{orSort, orChildren=[orFirst, orSecond]}
 mkApply tok@(Token _ (TokenIdent _)) sorts first second =
     embedParsedPattern $ ApplicationF Application
        { applicationSymbolOrAlias = SymbolOrAlias { symbolOrAliasConstructor = mkId tok