Kore.Parser.Parser: De-sugar \right-assoc

Author: ttuegel

kore/src/Kore/Parser/Parser.hs

@@ -275,12 +275,39 @@ parseSymbolOrAliasRemainder symbolOrAliasConstructor = do
 
 {- | Parse the @\\left-assoc@ syntactic sugar.
 
+@parseLeftAssoc@ assumes that the initial identifier has already been parsed.
+
 @
-"\\left-assoc" '{' '}' '(' <application-pattern> ')'
+_ '{' '}' '(' <application-pattern> ')'
 @
  -}
 parseLeftAssoc :: Parser ParsedPattern
-parseLeftAssoc = do
+parseLeftAssoc = parseAssoc foldl1
+
+{- | Parse the @\\right-assoc@ syntactic sugar.
+
+@parseRightAssoc@ assumes that the initial identifier has already been parsed.
+
+@
+_ '{' '}' '(' <application-pattern> ')'
+@
+ -}
+parseRightAssoc :: Parser ParsedPattern
+parseRightAssoc = parseAssoc foldr1
+
+{- | Parse the @\\left-assoc@ or @\\right-assoc@ syntactic sugar.
+
+@parseAssoc@ assumes that the initial identifier has already been parsed.
+
+@
+_ '{' '}' '(' <application-pattern> ')'
+@
+ -}
+parseAssoc
+    :: (forall r. (r -> r -> r) -> [r] -> r)
+    -- ^ folding function: 'foldl1' or 'foldr1'
+    -> Parser ParsedPattern
+parseAssoc foldAssoc = do
     braces $ pure ()
     application <- parens $ parseApplication parsePattern
     let mkApplication child1 child2 =
@@ -289,7 +316,7 @@ parseLeftAssoc = do
             & embedParsedPattern
     case applicationChildren application of
         [] -> fail "expected one or more arguments"
-        children -> pure (foldl1 mkApplication children)
+        children -> pure (foldAssoc mkApplication children)
 
 {- | Parse a built-in Kore (matching logic) pattern.
 
@@ -361,6 +388,7 @@ parseKoreRemainder identifier =
         "dv" -> embedParsedPattern . DomainValueF <$> parseDomainValue
         -- Syntax sugar
         "left-assoc" -> parseLeftAssoc
+        "right-assoc" -> parseRightAssoc
 
         _ -> empty
 

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

@@ -365,12 +365,11 @@ applicationPatternParserTests =
                         , symbolOrAliasParams = []
                         }
                 , applicationChildren =
+                    map embedParsedPattern
                     [ StringLiteral "a"
                         & Const & StringLiteralF
-                        & embedParsedPattern
                     , StringLiteral "b"
                         & Const & StringLiteralF
-                        & embedParsedPattern
                     ]
                 }
             )
@@ -390,21 +389,62 @@ applicationPatternParserTests =
                                 , symbolOrAliasParams = []
                                 }
                         , applicationChildren =
-                            [ StringLiteral "a"
-                                & Const & StringLiteralF
-                                & embedParsedPattern
-                            , StringLiteral "b"
-                                & Const & StringLiteralF
-                                & embedParsedPattern
+                            map embedParsedPattern
+                            [ StringLiteral "a" & Const & StringLiteralF
+                            , StringLiteral "b" & Const & StringLiteralF
                             ]
                         }
                     , StringLiteral "c" & Const & StringLiteralF
                     ]
                 }
             )
+        , success "\\right-assoc{}(c{}(\"a\"))"
+            ( StringLiteral "a"
+                & Const & StringLiteralF
+                & embedParsedPattern
+            )
+        , success "\\right-assoc{}(c{}(\"a\", \"b\"))"
+            ( embedParsedPattern $ ApplicationF Application
+                { applicationSymbolOrAlias =
+                    SymbolOrAlias
+                        { symbolOrAliasConstructor = testId "c"
+                        , symbolOrAliasParams = []
+                        }
+                , applicationChildren =
+                    map embedParsedPattern
+                    [ StringLiteral "a" & Const & StringLiteralF
+                    , StringLiteral "b" & Const & StringLiteralF
+                    ]
+                }
+            )
+        , success "\\right-assoc{}(c{}(\"a\", \"b\", \"c\"))"
+            ( embedParsedPattern $ ApplicationF Application
+                { applicationSymbolOrAlias =
+                    SymbolOrAlias
+                        { symbolOrAliasConstructor = testId "c"
+                        , symbolOrAliasParams = []
+                        }
+                , applicationChildren =
+                    map embedParsedPattern
+                    [ StringLiteral "a" & Const & StringLiteralF
+                    , ApplicationF Application
+                        { applicationSymbolOrAlias =
+                            SymbolOrAlias
+                                { symbolOrAliasConstructor = testId "c"
+                                , symbolOrAliasParams = []
+                                }
+                        , applicationChildren =
+                            map embedParsedPattern
+                            [ StringLiteral "b" & Const & StringLiteralF
+                            , StringLiteral "c" & Const & StringLiteralF
+                            ]
+                        }
+                    ]
+                }
+            )
         , FailureWithoutMessage
             [ "", "var", "v:", ":s", "c(s)", "c{s}"
-            , "\\left-assoc{}(c{}())"
+            , "\\left-assoc{}(c{}())", "\\right-assoc{}(c{}())"
             ]
         ]
 bottomPatternParserTests :: [TestTree]