Support multi-ary \and/\or in Haskell backend (#3666)

Part of #3542 

Essentially, we add support for \and and \or with 0 or more children.
The parser automatically desugars 0 or 1 children, so the AST will
always have at least 2 children. We modify the Internal modules to use a
new class, BinaryAnd and BinaryOr, which preserves the old
representation. Externalization and internalization then converts
between the two formats.

Most of this code is just needed to separate the `And` in
`Kore.Internal` from the `And` in `Kore.Syntax`. The actual changes are
relatively small.

### 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: github-actions <[email protected]>

kore-rpc-types/kore-rpc-types.cabal

@@ -76,6 +76,7 @@ common library
   build-depends: stm-conduit >= 4.0
   build-depends: text >=1.2
   build-depends: unliftio >= 0.2
+  build-depends: vector >= 0.12.3.1
 
 library
   import: haskell

kore-rpc-types/src/Kore/Syntax/Json/Types.hs

@@ -9,13 +9,16 @@ module Kore.Syntax.Json.Types (
 ) where
 
 import Data.Aeson as Json
+import Data.Aeson.Key qualified as Key
+import Data.Aeson.KeyMap qualified as KeyMap
 import Data.Aeson.Types qualified as Json
 import Data.Char (isAlpha, isDigit)
 import Data.Foldable ()
 import Data.List (nub)
 import Data.List.NonEmpty qualified as NE
 import Data.Text (Text)
 import Data.Text qualified as T
+import Data.Vector qualified as Vector
 import GHC.Generics (Generic)
 
 ------------------------------------------------------------
@@ -106,13 +109,11 @@ data KorePattern
         }
     | KJAnd
         { sort :: Sort
-        , first :: KorePattern
-        , second :: KorePattern
+        , patterns :: [KorePattern]
         }
     | KJOr
         { sort :: Sort
-        , first :: KorePattern
-        , second :: KorePattern
+        , patterns :: [KorePattern]
         }
     | KJImplies
         { sort :: Sort
@@ -217,7 +218,7 @@ instance ToJSON KorePattern where
     toJSON = genericToJSON codecOptions
 
 instance FromJSON KorePattern where
-    parseJSON v = genericParseJSON codecOptions v >>= lexicalCheck
+    parseJSON v = modifyAndOr v >>= genericParseJSON codecOptions >>= lexicalCheck
 
 codecOptions :: Json.Options
 codecOptions =
@@ -241,6 +242,26 @@ newtype Id = Id {getId :: Text}
     deriving stock (Eq, Show, Ord, Generic)
     deriving newtype (ToJSON, FromJSON)
 
+modifyAndOr :: Json.Value -> Json.Parser Json.Value
+modifyAndOr (Object v) = do
+    tag :: String <- v .: "tag"
+    case tag of
+        "And" -> flattenAndOr v
+        "Or" -> flattenAndOr v
+        _ -> return (Object v)
+modifyAndOr v = return v
+
+flattenAndOr :: Json.Object -> Json.Parser Json.Value
+flattenAndOr v = do
+    if KeyMap.member (Key.fromString "patterns") v
+        then return (Json.Object v)
+        else do
+            first :: Json.Value <- v .: "first"
+            second :: Json.Value <- v .: "second"
+            tag :: Json.Value <- v .: "tag"
+            sort :: Json.Value <- v .: "sort"
+            return $ Json.object ["tag" .= tag, "sort" .= sort, "patterns" .= Vector.fromList [first, second]]
+
 {- | Performs a (shallow, top-level, no recursion) lexical check of
  identifiers contained in the given node. For details see the check
  functions below.

kore/kore.cabal

@@ -501,6 +501,7 @@ library
     Kore.Substitute
     Kore.Syntax
     Kore.Syntax.And
+    Kore.Syntax.BinaryAnd
     Kore.Syntax.Application
     Kore.Syntax.Bottom
     Kore.Syntax.Ceil
@@ -523,6 +524,7 @@ library
     Kore.Syntax.Not
     Kore.Syntax.Nu
     Kore.Syntax.Or
+    Kore.Syntax.BinaryOr
     Kore.Syntax.Pattern
     Kore.Syntax.PatternF
     Kore.Syntax.Rewrites

kore/src/Kore/Attribute/Pattern/ConstructorLike.hs

@@ -61,7 +61,7 @@ newtype ConstructorLike = ConstructorLike
 instance Diff ConstructorLike where
     diffPrec = diffPrecIgnore
 
-instance Synthetic ConstructorLike (And sort) where
+instance Synthetic ConstructorLike (BinaryAnd sort) where
     synthetic = const (ConstructorLike Nothing)
     {-# INLINE synthetic #-}
 
@@ -158,7 +158,7 @@ instance Synthetic ConstructorLike (Nu sort) where
     synthetic = const (ConstructorLike Nothing)
     {-# INLINE synthetic #-}
 
-instance Synthetic ConstructorLike (Or sort) where
+instance Synthetic ConstructorLike (BinaryOr sort) where
     synthetic = const (ConstructorLike Nothing)
     {-# INLINE synthetic #-}
 

kore/src/Kore/Attribute/Pattern/Defined.hs

@@ -34,7 +34,7 @@ newtype Defined = Defined {isDefined :: Bool}
 alwaysDefined :: a -> Defined
 alwaysDefined = const (Defined True)
 
-instance Synthetic Defined (And sort) where
+instance Synthetic Defined (BinaryAnd sort) where
     synthetic = const (Defined False)
     {-# INLINE synthetic #-}
 
@@ -112,7 +112,7 @@ instance Synthetic Defined (Nu sort) where
     {-# INLINE synthetic #-}
 
 -- | An 'Or' pattern is 'Defined' if any of its subterms is 'Defined'.
-instance Synthetic Defined (Or sort) where
+instance Synthetic Defined (BinaryOr sort) where
     synthetic = Defined . getAny . foldMap (Any . isDefined)
     {-# INLINE synthetic #-}
 

kore/src/Kore/Attribute/Pattern/Function.hs

@@ -35,7 +35,7 @@ alwaysFunction :: a -> Function
 alwaysFunction = const (Function True)
 {-# INLINE alwaysFunction #-}
 
-instance Synthetic Function (And sort) where
+instance Synthetic Function (BinaryAnd sort) where
     -- TODO (thomas.tuegel):
     -- synthetic = getAny . Foldable.foldMap (Any . isFunction)
     synthetic = const (Function False)
@@ -113,7 +113,7 @@ instance Synthetic Function (Nu sort) where
     synthetic = const (Function False)
     {-# INLINE synthetic #-}
 
-instance Synthetic Function (Or sort) where
+instance Synthetic Function (BinaryOr sort) where
     synthetic = const (Function False)
     {-# INLINE synthetic #-}
 

kore/src/Kore/Attribute/Pattern/Simplified.hs

@@ -37,8 +37,9 @@ import Kore.Internal.SideCondition.SideCondition qualified as SideCondition (
     Representation,
  )
 import Kore.Syntax (
-    And,
     Application,
+    BinaryAnd,
+    BinaryOr,
     Bottom,
     Ceil,
     Const,
@@ -55,7 +56,6 @@ import Kore.Syntax (
     Next,
     Not,
     Nu,
-    Or,
     Rewrites,
     StringLiteral,
     Top,
@@ -306,11 +306,11 @@ instance Synthetic Simplified (Forall sort variable) where
     synthetic = notSimplified
     {-# INLINE synthetic #-}
 
-instance Synthetic Simplified (And sort) where
+instance Synthetic Simplified (BinaryAnd sort) where
     synthetic = notSimplified
     {-# INLINE synthetic #-}
 
-instance Synthetic Simplified (Or sort) where
+instance Synthetic Simplified (BinaryOr sort) where
     synthetic = notSimplified
     {-# INLINE synthetic #-}
 

kore/src/Kore/Attribute/Pattern/Total.hs

@@ -34,7 +34,7 @@ alwaysTotal :: a -> Total
 alwaysTotal = const (Total True)
 {-# INLINE alwaysTotal #-}
 
-instance Synthetic Total (And sort) where
+instance Synthetic Total (BinaryAnd sort) where
     synthetic = const (Total False)
     {-# INLINE synthetic #-}
 
@@ -107,7 +107,7 @@ instance Synthetic Total (Nu sort) where
     synthetic = const (Total False)
     {-# INLINE synthetic #-}
 
-instance Synthetic Total (Or sort) where
+instance Synthetic Total (BinaryOr sort) where
     synthetic = const (Total False)
     {-# INLINE synthetic #-}
 

kore/src/Kore/Internal/From.hs

@@ -24,7 +24,8 @@ import Kore.Attribute.Synthetic (
     Synthesize,
     synthesize,
  )
-import Kore.Syntax.And
+import Kore.Syntax.BinaryAnd
+import Kore.Syntax.BinaryOr
 import Kore.Syntax.Bottom
 import Kore.Syntax.Ceil
 import Kore.Syntax.Equals
@@ -35,7 +36,6 @@ import Kore.Syntax.Iff
 import Kore.Syntax.Implies
 import Kore.Syntax.In
 import Kore.Syntax.Not
-import Kore.Syntax.Or
 import Kore.Syntax.Top
 import Kore.Syntax.Variable
 import Prelude.Kore
@@ -83,15 +83,15 @@ synthesizeFrom = synthesize . into @(f v (p v))
 
 fromAnd ::
     forall a f v p.
-    SynthesizeFrom (And ()) a f v p p =>
+    SynthesizeFrom (BinaryAnd ()) a f v p p =>
     p v ->
     p v ->
     p v
 fromAnd andFirst andSecond =
-    synthesizeFrom And{andFirst, andSecond, andSort = ()}
+    synthesizeFrom BinaryAnd{andFirst, andSecond, andSort = ()}
 
-fromOr :: forall a f v p. SynthesizeFrom (Or ()) a f v p p => p v -> p v -> p v
-fromOr orFirst orSecond = synthesizeFrom Or{orFirst, orSecond, orSort = ()}
+fromOr :: forall a f v p. SynthesizeFrom (BinaryOr ()) a f v p p => p v -> p v -> p v
+fromOr orFirst orSecond = synthesizeFrom BinaryOr{orFirst, orSecond, orSort = ()}
 
 fromNot :: forall a f v p. SynthesizeFrom (Not ()) a f v p p => p v -> p v
 fromNot notChild = synthesizeFrom Not{notChild, notSort = ()}

kore/src/Kore/Internal/Predicate.hs

@@ -154,7 +154,7 @@ import Pretty qualified
 import SQL qualified
 
 data PredicateF variable child
-    = AndF !(And () child)
+    = AndF !(BinaryAnd () child)
     | BottomF !(Bottom () child)
     | CeilF !(Ceil () (TermLike variable))
     | EqualsF !(Equals () (TermLike variable))
@@ -165,7 +165,7 @@ data PredicateF variable child
     | ImpliesF !(Implies () child)
     | InF !(In () (TermLike variable))
     | NotF !(Not () child)
-    | OrF !(Or () child)
+    | OrF !(BinaryOr () child)
     | TopF !(Top () child)
     deriving stock (Eq, Ord, Show)
     deriving stock (Functor, Foldable, Traversable)
@@ -238,11 +238,11 @@ instance From (Forall () variable child) (PredicateF variable child) where
     from = ForallF
     {-# INLINE from #-}
 
-instance From (And () child) (PredicateF variable child) where
+instance From (BinaryAnd () child) (PredicateF variable child) where
     from = AndF
     {-# INLINE from #-}
 
-instance From (Or () child) (PredicateF variable child) where
+instance From (BinaryOr () child) (PredicateF variable child) where
     from = OrF
     {-# INLINE from #-}
 
@@ -529,12 +529,12 @@ pattern PredicateTrue <- (Recursive.project -> _ :< TopF _)
 pattern PredicateAnd ::
     Predicate variable -> Predicate variable -> Predicate variable
 pattern PredicateAnd p1 p2 <-
-    (Recursive.project -> _ :< AndF (And () p1 p2))
+    (Recursive.project -> _ :< AndF (BinaryAnd () p1 p2))
 
 pattern PredicateOr ::
     Predicate variable -> Predicate variable -> Predicate variable
 pattern PredicateOr p1 p2 <-
-    (Recursive.project -> _ :< OrF (Or () p1 p2))
+    (Recursive.project -> _ :< OrF (BinaryOr () p1 p2))
 
 pattern PredicateNot :: Predicate variable -> Predicate variable
 pattern PredicateNot p <-
@@ -571,7 +571,7 @@ fromPredicate sort = Recursive.fold worker
         TermLike.setSimplified
             (PredicatePattern.simplifiedAttribute pat)
             $ case predF of
-                AndF (And () t1 t2) -> TermLike.mkAnd t1 t2
+                AndF (BinaryAnd () t1 t2) -> TermLike.mkAnd t1 t2
                 BottomF _ -> TermLike.mkBottom sort
                 CeilF (Ceil () () t) -> TermLike.mkCeil sort t
                 EqualsF (Equals () () t1 t2) -> TermLike.mkEquals sort t1 t2
@@ -582,7 +582,7 @@ fromPredicate sort = Recursive.fold worker
                 ImpliesF (Implies () t1 t2) -> TermLike.mkImplies t1 t2
                 InF (In () () t1 t2) -> TermLike.mkIn sort t1 t2
                 NotF (Not () t) -> TermLike.mkNot t
-                OrF (Or () t1 t2) -> TermLike.mkOr t1 t2
+                OrF (BinaryOr () t1 t2) -> TermLike.mkOr t1 t2
                 TopF _ -> TermLike.mkTop sort
 
 {- | Simple type used to track whether a predicate building function performed
@@ -659,7 +659,7 @@ makeAndPredicate' p1 p2
     | otherwise =
         ( synthesize $
             AndF
-                And
+                BinaryAnd
                     { andSort = ()
                     , andFirst = p1
                     , andSecond = p2
@@ -688,7 +688,7 @@ makeOrPredicate' p1 p2
     | otherwise =
         ( synthesize $
             OrF
-                Or
+                BinaryOr
                     { orSort = ()
                     , orFirst = p1
                     , orSecond = p2

kore/src/Kore/Internal/TermLike.hs

@@ -157,7 +157,7 @@ module Kore.Internal.TermLike (
     Attribute.freeVariables,
     module Kore.Internal.Inj,
     module Kore.Internal.InternalBytes,
-    module Kore.Syntax.And,
+    module Kore.Syntax.BinaryAnd,
     module Kore.Syntax.Application,
     module Kore.Syntax.Bottom,
     module Kore.Syntax.Ceil,
@@ -174,7 +174,7 @@ module Kore.Internal.TermLike (
     module Kore.Syntax.Next,
     module Kore.Syntax.Not,
     module Kore.Syntax.Nu,
-    module Kore.Syntax.Or,
+    module Kore.Syntax.BinaryOr,
     module Kore.Syntax.Rewrites,
     module Kore.Syntax.StringLiteral,
     module Kore.Syntax.Top,
@@ -255,8 +255,9 @@ import Kore.Internal.TermLike.TermLike
 import Kore.Internal.Variable
 import Kore.Sort
 import Kore.Substitute
-import Kore.Syntax.And
 import Kore.Syntax.Application
+import Kore.Syntax.BinaryAnd
+import Kore.Syntax.BinaryOr
 import Kore.Syntax.Bottom
 import Kore.Syntax.Ceil
 import Kore.Syntax.Definition hiding (
@@ -279,7 +280,6 @@ import Kore.Syntax.Mu
 import Kore.Syntax.Next
 import Kore.Syntax.Not
 import Kore.Syntax.Nu
-import Kore.Syntax.Or
 import Kore.Syntax.Rewrites
 import Kore.Syntax.StringLiteral
 import Kore.Syntax.Top
@@ -790,7 +790,7 @@ mkAnd ::
 mkAnd t1 t2 = updateCallStack $ checkSortsAgree mkAndWorker t1 t2
   where
     mkAndWorker andFirst andSecond andSort =
-        synthesize (AndF And{andSort, andFirst, andSecond})
+        synthesize (AndF BinaryAnd{andSort, andFirst, andSecond})
 
 {- | Force the 'TermLike's to conform to their 'Sort's.
 
@@ -1263,7 +1263,7 @@ mkOr ::
 mkOr t1 t2 = updateCallStack $ checkSortsAgree mkOrWorker t1 t2
   where
     mkOrWorker orFirst orSecond orSort =
-        synthesize (OrF Or{orSort, orFirst, orSecond})
+        synthesize (OrF BinaryOr{orSort, orFirst, orSecond})
 
 -- | Construct a 'Rewrites' pattern.
 mkRewrites ::
@@ -1602,7 +1602,7 @@ pattern SetVar_ :: SetVariable variable -> TermLike variable
 pattern StringLiteral_ :: Text -> TermLike variable
 
 pattern And_ andSort andFirst andSecond <-
-    (Recursive.project -> _ :< AndF And{andSort, andFirst, andSecond})
+    (Recursive.project -> _ :< AndF BinaryAnd{andSort, andFirst, andSecond})
 
 pattern ApplyAlias_ applicationSymbolOrAlias applicationChildren <-
     ( Recursive.project ->
@@ -1744,7 +1744,7 @@ pattern Nu_ nuVariable nuChild <-
         )
 
 pattern Or_ orSort orFirst orSecond <-
-    (Recursive.project -> _ :< OrF Or{orSort, orFirst, orSecond})
+    (Recursive.project -> _ :< OrF BinaryOr{orSort, orFirst, orSecond})
 
 pattern Rewrites_ rewritesSort rewritesFirst rewritesSecond <-
     ( Recursive.project ->