Allow matching two empty KMaps

runtimeverification · Jul 28, 2023 · ef26fd1 · ef26fd1
1 parent 56c35eb
commit ef26fd1
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/library/Booster/Pattern/Match.hs b/library/Booster/Pattern/Match.hs
@@ -269,7 +269,12 @@ match1
             -- and, domain values, injections, maps: fail
             _other ->
                 failWith $ DifferentSymbols app subj
--- matching on maps unsupported
+----- KMap
+-- empty maps match trivially with an empty substitution
+match1
+    (KMap _ [] Nothing)
+    (KMap _ [] Nothing) = pure mempty
+-- matching on non-empty maps is not supported
 match1
     t1@KMap{}
     t2 = indeterminate t1 t2