Allow matching empty sets (#4009)

This PR adds rudimentary matching of internalized sets: only empty sets
are allowed to match, and an indeterminate result is returned for
non-empty sets.

Author: geo2a

booster/library/Booster/Pattern/Match.hs

@@ -25,14 +25,15 @@ import Data.List (partition)
 import Data.List.NonEmpty as NE (NonEmpty, fromList)
 import Data.Map (Map)
 import Data.Map qualified as Map
+import Data.Maybe (isNothing)
 import Data.Sequence (Seq, (><), pattern (:<|), pattern (:|>))
 import Data.Sequence qualified as Seq
 
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Prettyprinter
 
-import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition)
+import Booster.Definition.Attributes.Base (KListDefinition, KMapDefinition, KSetDefinition)
 import Booster.Definition.Base
 import Booster.Pattern.Base
 import Booster.Pattern.Pretty
@@ -262,7 +263,7 @@ match1 Eval    t1@KSet{}                                  t2@Injection{}
 match1 _       t1@KSet{}                                  t2@Injection{}                             = failWith $ DifferentSymbols t1 t2
 match1 _       t1@KSet{}                                  t2@KMap{}                                  = failWith $ DifferentSymbols t1 t2
 match1 _       t1@KSet{}                                  t2@KList{}                                 = failWith $ DifferentSymbols t1 t2
-match1 _       t1@KSet{}                                  t2@KSet{}                                  = addIndeterminate t1 t2
+match1 _       t1@(KSet def1 patElements patRest)         t2@(KSet def2 subjElements subjRest)       = if def1 == def2 then matchSets def1 patElements patRest subjElements subjRest else failWith $ DifferentSorts t1 t2
 match1 _       t1@KSet{}                                  t2@ConsApplication{}                       = failWith $ DifferentSymbols t1 t2
 match1 _       t1@KSet{}                                  t2@FunctionApplication{}                   = addIndeterminate t1 t2
 match1 Rewrite t1@KSet{}                                  (Var t2)                                   = failWith $ SubjectVariableMatch t1 t2
@@ -626,6 +627,25 @@ containsOtherKeys = \case
     Rest OtherKey{} -> True
     Rest _ -> False
 
+------ Internalised Sets
+matchSets ::
+    KSetDefinition ->
+    [Term] ->
+    Maybe Term ->
+    [Term] ->
+    Maybe Term ->
+    StateT MatchState (Except MatchResult) ()
+matchSets
+    def
+    patElements
+    patRest
+    subjElements
+    subjRest = do
+        -- match only empty sets, indeterminate otherwise
+        if null patElements && null subjElements && isNothing patRest && isNothing subjRest
+            then pure ()
+            else addIndeterminate (KSet def patElements patRest) (KSet def subjElements subjRest)
+
 ------ Internalised Maps
 matchMaps ::
     KMapDefinition ->

booster/unit-tests/Test/Booster/Pattern/InternalCollections.hs

@@ -11,6 +11,7 @@ module Test.Booster.Pattern.InternalCollections (
     headList,
     tailList,
     mixedList,
+    emptySet,
 ) where
 
 import Data.ByteString.Char8 qualified as BS

booster/unit-tests/Test/Booster/Pattern/MatchEval.hs

@@ -17,6 +17,7 @@ import Booster.Pattern.Base
 import Booster.Pattern.Match
 import Booster.Syntax.Json.Internalise (trm)
 import Test.Booster.Fixture
+import Test.Booster.Pattern.InternalCollections
 
 test_match_eval :: TestTree
 test_match_eval =
@@ -28,6 +29,7 @@ test_match_eval =
         , andTerms
         , composite
         , kmapTerms
+        , internalSets
         ]
 
 symbols :: TestTree
@@ -293,6 +295,19 @@ cornerCases =
     let v = var "X" someSort
      in errors "identical variables" v v
 
+internalSets :: TestTree
+internalSets =
+    testGroup
+        "Internal sets"
+        [ test
+            "Can match an empty set with itself"
+            emptySet
+            emptySet
+            (success [])
+        ]
+
+----------------------------------------
+
 test :: String -> Term -> Term -> MatchResult -> TestTree
 test name pat subj expected =
     testCase name $ matchTerms Eval testDefinition pat subj @?= expected

booster/unit-tests/Test/Booster/Pattern/MatchImplies.hs

@@ -32,6 +32,7 @@ test_match_implies =
         , sorts
         , injections
         , internalLists
+        , internalSets
         , internalMaps
         ]
 
@@ -377,6 +378,17 @@ internalLists =
 
     klist = KList testKListDef
 
+internalSets :: TestTree
+internalSets =
+    testGroup
+        "Internal sets"
+        [ test
+            "Can match an empty set with itself"
+            emptySet
+            emptySet
+            (success [])
+        ]
+
 internalMaps :: TestTree
 internalMaps =
     testGroup

booster/unit-tests/Test/Booster/Pattern/MatchRewrite.hs

@@ -32,6 +32,7 @@ test_match_rewrite =
         , sorts
         , injections
         , internalLists
+        , internalSets
         , internalMaps
         ]
 
@@ -376,6 +377,17 @@ internalLists =
 
     klist = KList testKListDef
 
+internalSets :: TestTree
+internalSets =
+    testGroup
+        "Internal sets"
+        [ test
+            "Can match an empty set with itself"
+            emptySet
+            emptySet
+            (success [])
+        ]
+
 internalMaps :: TestTree
 internalMaps =
     testGroup