Allow matching empty sets

runtimeverification · Jul 30, 2024 · bf05ef2 · bf05ef2
1 parent 7bdf0a7
commit bf05ef2
Showing 1 changed file with 22 additions and 2 deletions.
diff --git a/booster/library/Booster/Pattern/Match.hs b/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
@@ -627,6 +628,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 ->