Allow parsing of multi-arg \\or with \\left-assoc (#2861)

* (R) Add test

* (G) Parse \left-assoc for \or with two arguments

* Format with fourmolu

* (A) Remove commented-out code

* (R) Add test for multiple arg \or

* (G) Parse \or with arbitrary no. of arguments

* Add equivalent tests for \right-assoc

* (A) Factor out ParsedMultiOr type

* Format with fourmolu

* Update documentation

* Add test for failing case

* Format with fourmolu

Co-authored-by: github-actions <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

docs/kore-syntax.md

@@ -181,6 +181,9 @@ A sort is either a _sort variable_ or a _sort constructor_ applied to a list of
 <application-pattern> ::=
     <symbol-identifier> "{" <sorts> "}" "(" <patterns> ")"
 
+<multi-or> ::=
+    "\or" "{" <sort> "}" "(" <patterns> ")"
+
 <matching-logic-pattern>
   ::=
     // Connectives
@@ -210,7 +213,9 @@ A sort is either a _sort variable_ or a _sort constructor_ applied to a list of
     | "\dv" "{" <sort> "}" "(" <string-literal> ")"
     // Syntax sugar
     | "\left-assoc" "{" "}" "(" <application-pattern> ")"
+    | "\left-assoc" "{" "}" "(" <multi-or> ")"
     | "\right-assoc" "{" "}" "(" <application-pattern> ")"
+    | "\right-assoc" "{" "}" "(" <multi-or> ")"
 ```
 
 ### Attributes

kore/src/Kore/Parser/Parser.hs

@@ -136,7 +136,8 @@ parseSymbolHead = parseSymbolOrAliasDeclarationHead Symbol
 -}
 parsePattern :: Parser ParsedPattern
 parsePattern =
-    parseLiteral <|> (parseAnyId >>= parseRemainder)
+    parseLiteral
+        <|> (parseAnyId >>= parseRemainder)
   where
     parseRemainder identifier =
         parseVariableRemainder identifier
@@ -269,7 +270,7 @@ parseSymbolOrAliasRemainder symbolOrAliasConstructor = do
 @parseLeftAssoc@ assumes that the initial identifier has already been parsed.
 
 @
-_ '{' '}' '(' <application-pattern> ')'
+_ '{' '}' '(' <application-pattern> | <multi-or> ')'
 @
 -}
 parseLeftAssoc :: Parser ParsedPattern
@@ -280,7 +281,7 @@ parseLeftAssoc = parseAssoc foldl1
 @parseRightAssoc@ assumes that the initial identifier has already been parsed.
 
 @
-_ '{' '}' '(' <application-pattern> ')'
+_ '{' '}' '(' <application-pattern> | <multi-or> ')'
 @
 -}
 parseRightAssoc :: Parser ParsedPattern
@@ -300,12 +301,48 @@ parseAssoc ::
     Parser ParsedPattern
 parseAssoc foldAssoc = do
     braces $ pure ()
-    application <- parens $ parseApplication parsePattern
-    let mkApplication child1 child2 =
-            from application{applicationChildren = [child1, child2]}
-    case applicationChildren application of
-        [] -> fail "expected one or more arguments"
-        children -> pure (foldAssoc mkApplication children)
+    Parse.try withOr <|> withApplication
+  where
+    withApplication = do
+        application <- parens $ parseApplication parsePattern
+        let mkApplication child1 child2 =
+                from application{applicationChildren = [child1, child2]}
+        case applicationChildren application of
+            [] -> fail "expected one or more arguments"
+            children -> pure (foldAssoc mkApplication children)
+    withOr = do
+        ParsedMultiOr{multiOrSort, multiOrChildren} <-
+            parens $ parseMultiOr parsePattern
+        let mkOr child1 child2 =
+                from Or{orFirst = child1, orSecond = child2, orSort = multiOrSort}
+        case multiOrChildren of
+            [] -> fail "expected two or more arguments"
+            [_] -> fail "expected two or more arguments"
+            children -> return (foldAssoc mkOr children)
+
+-- | Datatype for representing multi-argument Or.
+data ParsedMultiOr child = ParsedMultiOr
+    { multiOrSort :: Sort
+    , multiOrChildren :: [child]
+    }
+
+{- | Parse an multi-argument Or occurring under an assoc syntatic sugar.
+
+@
+<multi-or> ::= "\or" "{" <sort> "}" "(" <patterns> ")"
+@
+-}
+parseMultiOr :: Parser child -> Parser (ParsedMultiOr child)
+parseMultiOr parseChild = do
+    parseAnyId >>= orLiteral
+    multiOrSort <- braces parseSort
+    multiOrChildren <- parens . list $ parseChild
+    return ParsedMultiOr{multiOrSort, multiOrChildren}
+  where
+    orLiteral identifier =
+        getSpecialId identifier >>= \case
+            "or" -> return ()
+            _ -> empty
 
 {- | Parse a built-in Kore (matching logic) pattern.
 
@@ -344,7 +381,9 @@ parseAssoc foldAssoc = do
 
     // Syntax sugar
     | "\left-assoc" "{" "}" "(" <application-pattern> ")"
+    | "\left-assoc" "{" "}" "(" <multi-or> ")"
     | "\right-assoc" "{" "}" "(" <application-pattern> ")"
+    | "\right-assoc" "{" "}" "(" <multi-or> ")"
 @
 
 Always starts with @\@.

kore/test/Test/Kore/Parser/Parser.hs

@@ -474,6 +474,35 @@ applicationPatternParserTests =
                                 ]
                         }
             )
+        , success
+            "\\left-assoc{}(\\or{s}(\"a\", \"b\"))"
+            ( embedParsedPattern $
+                OrF
+                    Or
+                        { orFirst = StringLiteral "a" & Const & StringLiteralF & embedParsedPattern
+                        , orSecond = StringLiteral "b" & Const & StringLiteralF & embedParsedPattern
+                        , orSort = sortVariableSort "s" :: Sort
+                        }
+            )
+        , success
+            "\\left-assoc{}(\\or{s}(\"a\", \"b\", \"c\"))"
+            ( embedParsedPattern $
+                OrF
+                    Or
+                        { orFirst =
+                            embedParsedPattern $
+                                OrF
+                                    Or
+                                        { orFirst =
+                                            StringLiteral "a" & Const & StringLiteralF & embedParsedPattern
+                                        , orSecond =
+                                            StringLiteral "b" & Const & StringLiteralF & embedParsedPattern
+                                        , orSort = sortVariableSort "s" :: Sort
+                                        }
+                        , orSecond = StringLiteral "c" & Const & StringLiteralF & embedParsedPattern
+                        , orSort = sortVariableSort "s" :: Sort
+                        }
+            )
         , success
             "\\right-assoc{}(c{}(\"a\"))"
             ( StringLiteral "a"
@@ -530,6 +559,35 @@ applicationPatternParserTests =
                                 ]
                         }
             )
+        , success
+            "\\right-assoc{}(\\or{s}(\"a\", \"b\"))"
+            ( embedParsedPattern $
+                OrF
+                    Or
+                        { orFirst = StringLiteral "a" & Const & StringLiteralF & embedParsedPattern
+                        , orSecond = StringLiteral "b" & Const & StringLiteralF & embedParsedPattern
+                        , orSort = sortVariableSort "s" :: Sort
+                        }
+            )
+        , success
+            "\\right-assoc{}(\\or{s}(\"a\", \"b\", \"c\"))"
+            ( embedParsedPattern $
+                OrF
+                    Or
+                        { orFirst = StringLiteral "a" & Const & StringLiteralF & embedParsedPattern
+                        , orSecond =
+                            embedParsedPattern $
+                                OrF
+                                    Or
+                                        { orFirst =
+                                            StringLiteral "b" & Const & StringLiteralF & embedParsedPattern
+                                        , orSecond =
+                                            StringLiteral "c" & Const & StringLiteralF & embedParsedPattern
+                                        , orSort = sortVariableSort "s" :: Sort
+                                        }
+                        , orSort = sortVariableSort "s" :: Sort
+                        }
+            )
         , FailureWithoutMessage
             [ ""
             , "var"
@@ -539,6 +597,7 @@ applicationPatternParserTests =
             , "c{s}"
             , "\\left-assoc{}(c{}())"
             , "\\right-assoc{}(c{}())"
+            , "\\or{s}(\"a\", \"b\", \"c\")"
             ]
         ]
 bottomPatternParserTests :: [TestTree]