fix unit tests and merge the two implementation of map matching into …

…a single instance

library/Booster/JsonRpc.hs

@@ -816,6 +816,11 @@ mkLogRewriteTrace
                                             { reason = "Sort error while unifying"
                                             , _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
                                             }
+                                    InternalMatchError{} ->
+                                        Failure
+                                            { reason = "Internal match error"
+                                            , _ruleId = Nothing
+                                            }
                                 , origin = Booster
                                 }
             RewriteSimplified equationTraces Nothing

library/Booster/Pattern/Rewrite.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
 
 {- |
 Copyright   : (c) Runtime Verification, 2022
@@ -260,6 +261,8 @@ applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do
     subst <- case matchTerms Rule def rule.lhs pat.term of
         MatchFailed (SubsortingError sortError) ->
             failRewrite $ RewriteSortError rule pat.term sortError
+        MatchFailed err@ArgLengthsDiffer{} ->
+            failRewrite $ InternalMatchError $ renderText $ pretty err
         MatchFailed _reason ->
             fail "Rule matching failed"
         MatchIndeterminate remainder ->
@@ -400,6 +403,8 @@ data RewriteFailed k
       UnificationIsNotMatch (RewriteRule k) Term Substitution
     | -- | A sort error was detected during unification
       RewriteSortError (RewriteRule k) Term SortError
+    | -- | A sort error was detected during unification
+      InternalMatchError Text
     | -- | Term has index 'None', no rule should apply
       TermIndexIsNone Term
     deriving stock (Eq, Show)
@@ -450,6 +455,7 @@ instance Pretty (RewriteFailed k) where
             ]
     pretty (TermIndexIsNone term) =
         "Term index is None for term " <> pretty term
+    pretty (InternalMatchError err) = "An internal error occured" <> pretty err
 
 ruleLabelOrLoc :: RewriteRule k -> Doc a
 ruleLabelOrLoc rule =

unit-tests/Test/Booster/Fixture.hs

@@ -53,6 +53,7 @@ testDefinition =
                 , ("f1", f1)
                 , ("f2", f2)
                 , ("f3", f3)
+                , ("g", g)
                 , ("Lbl'UndsEqlsEqls'K'Und'", eqK)
                 , ("kseq", kseq)
                 , ("dotk", dotk)
@@ -89,14 +90,15 @@ app s = SymbolApplication s []
 inj :: Sort -> Sort -> Term -> Term
 inj = Injection
 
-con1, con2, con3, con4, f1, f2, f3, eqK, kseq, dotk :: Symbol
+con1, con2, con3, con4, f1, f2, f3, g, eqK, kseq, dotk :: Symbol
 con1 = [symb| symbol con1{}(SomeSort{}) : SomeSort{} [constructor{}()] |]
 con2 = [symb| symbol con2{}(SomeSort{}) : SomeSort{} [constructor{}()] |]
 con3 = [symb| symbol con3{}(SomeSort{}, SomeSort{}) : SomeSort{} [constructor{}()] |]
 con4 = [symb| symbol con4{}(SomeSort{}, SomeSort{}) : AnotherSort{} [constructor{}()] |]
 f1 = [symb| symbol f1{}(SomeSort{}) : SomeSort{} [function{}(), total{}()] |]
 f2 = [symb| symbol f2{}(SomeSort{}) : SomeSort{} [function{}()] |]
 f3 = [symb| symbol f3{}(SomeSort{}) : SortTestKMap{} [function{}()] |]
+g = [symb| symbol g{}() : SortTestKMapKey{} [function{}(), total{}()] |]
 eqK =
     Symbol
         { name = "Lbl'UndsEqlsEqls'K'Unds'"
@@ -106,7 +108,7 @@ eqK =
         , attributes =
             SymbolAttributes
                 { collectionMetadata = Nothing
-                , symbolType = TotalFunction
+                , symbolType = Function Total
                 , isIdem = IsNotIdem
                 , isAssoc = IsNotAssoc
                 , isMacroOrAlias = IsNotMacroOrAlias
@@ -222,7 +224,7 @@ functionKMapWithOneItemAndRest =
     KMap
         testKMapDefinition
         [
-            ( [trm| f1{}() |]
+            ( [trm| g{}() |]
             , [trm| \dv{SortTestKMapItem{}}("value") |]
             )
         ]
@@ -231,7 +233,7 @@ functionKMapWithOneItem =
     KMap
         testKMapDefinition
         [
-            ( [trm| f1{}() |]
+            ( [trm| g{}() |]
             , [trm| B:SortTestKMapItem{} |]
             )
         ]

unit-tests/Test/Booster/Pattern/Binary.hs

@@ -39,7 +39,7 @@ genSymbolUnknownSort =
     ( \name ->
         Symbol name [] [] (SortApp "UNKNOWN" []) $
             SymbolAttributes
-                PartialFunction
+                (Function Partial)
                 IsNotIdem
                 IsNotAssoc
                 IsNotMacroOrAlias

unit-tests/Test/Booster/Pattern/Match.hs → unit-tests/Test/Booster/Pattern/MatchFun.hs

@@ -1,22 +1,24 @@
+{-# LANGUAGE QuasiQuotes #-}
 {- |
 Copyright   : (c) Runtime Verification, 2022
 License     : BSD-3-Clause
 -}
-module Test.Booster.Pattern.Match (
-    test_match,
+module Test.Booster.Pattern.MatchFun (
+    test_match_fun,
 ) where
 
 import Data.Map qualified as Map
+import Data.List.NonEmpty qualified as NE
 import Test.Tasty
 import Test.Tasty.HUnit
 
 import Booster.Pattern.Base
-import Booster.Pattern.Match
-import Booster.Pattern.Unify (FailReason (..))
+import Booster.Pattern.UnifiedMatcher
+import Booster.Syntax.Json.Internalise (trm)
 import Test.Booster.Fixture
 
-test_match :: TestTree
-test_match =
+test_match_fun :: TestTree
+test_match_fun =
     testGroup
         "(equation) matching"
         [ symbols
@@ -48,11 +50,11 @@ symbols =
         , let pat = app con1 [var "X" someSort]
               subj = app f1 [var "Y" someSort]
            in test "constructor and function" pat subj $
-                MatchIndeterminate pat subj
+                MatchIndeterminate $ NE.singleton (pat, subj)
         , let pat = app f1 [var "X" someSort]
               subj = app con1 [var "Y" someSort]
            in test "function and constructor" pat subj $
-                MatchIndeterminate pat subj
+                MatchIndeterminate $ NE.singleton (pat, subj)
         , let x = var "X" someSort
               d = dv differentSort "something"
               pat = app con1 [x]
@@ -141,15 +143,15 @@ varsAndValues =
         , let v = var "X" someSort
               d = dv someSort ""
            in test "dv matching a var (on RHS): indeterminate" d v $
-                MatchIndeterminate d v
+                 MatchIndeterminate $ NE.singleton (d, v)
         , let d = dv someSort ""
               f = app f1 [d]
            in test "dv matching a function call (on RHS): indeterminate" d f $
-                MatchIndeterminate d f
+                 MatchIndeterminate $ NE.singleton (d, f)
         , let d = dv someSort ""
               c = app con1 [d]
            in test "dv matching a constructor (on RHS): fail" d c $
-                failed (DifferentValues d c)
+                failed (DifferentSymbols d c)
         ]
 
 andTerms :: TestTree
@@ -181,7 +183,7 @@ andTerms =
                 "And-term on the right, indeterminate"
                 d
                 (AndTerm fa fb)
-                (MatchIndeterminate d (AndTerm fa fb))
+                (MatchIndeterminate $ NE.singleton (d ,AndTerm fa fb))
         ]
 
 kmapTerms :: TestTree
@@ -198,21 +200,16 @@ kmapTerms =
             concreteKMapWithOneItem
             concreteKMapWithOneItem
             (success [])
-        , test
-            "Empty KMap ~= non-empty concrete KMap: fails"
-            emptyKMap
-            concreteKMapWithOneItem
-            (failed $ DifferentValues emptyKMap concreteKMapWithOneItem)
         , test
             "Non-empty concrete KMap ~= empty KMap: fails"
             concreteKMapWithOneItem
             emptyKMap
-            (failed $ DifferentValues concreteKMapWithOneItem emptyKMap)
+            (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap)
         , test
             "Non-empty symbolic KMap ~= empty KMap: fails"
             symbolicKMapWithOneItem
             emptyKMap
-            (failed $ DifferentValues symbolicKMapWithOneItem emptyKMap)
+            (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap)
         , test
             "Non-empty symbolic KMap ~= non-empty concrete KMap, same key: matches contained value"
             symbolicKMapWithOneItem -- "key" -> A
@@ -231,19 +228,11 @@ kmapTerms =
                in success [("REST", kmapSort, restMap)]
             )
         , -- pattern has more assocs than subject
-          let patRest = kmap [(dv kmapKeySort "key2", dv kmapElementSort "value2")] Nothing
-           in test
+          test
                 "Extra concrete key in pattern, no rest in subject: fail on rest"
                 concreteKMapWithTwoItems
                 concreteKMapWithOneItem
-                (failed $ DifferentValues patRest emptyKMap)
-        , let patRest =
-                kmap [(dv kmapKeySort "key2", dv kmapElementSort "value2")] Nothing
-           in test
-                "Extra concrete key in pattern, opaque rest in subject: indeterminate part"
-                concreteKMapWithTwoItems
-                concreteKMapWithOneItemAndRest
-                (MatchIndeterminate patRest (var "REST" kmapSort))
+                (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] emptyKMap)
         , -- cases with disjoint keys
           test
             "Variable key ~= concrete key (and common element) without rest: match key"
@@ -252,24 +241,24 @@ kmapTerms =
             ( success [("A", kmapKeySort, dv kmapKeySort "key2")]
             )
         , let patMap =
-                kmap [(var "K" kmapKeySort, var "V" kmapElementSort)] (Just "PATTERN")
+                kmap [([trm| K:SortTestKMapKey{} |], var "V" kmapElementSort)] (Just "PATTERN")
            in test
                 "Variable key ~= concrete key with rest in subject and pattern: indeterminate"
                 patMap
                 functionKMapWithOneItemAndRest
-                (MatchIndeterminate patMap functionKMapWithOneItemAndRest)
+                (MatchIndeterminate $ NE.singleton (patMap, functionKMapWithOneItemAndRest))
         , let patMap =
                 kmap [(var "K" kmapKeySort, var "V" kmapElementSort)] (Just "PATTERN")
            in test
                 "Variable key and opaque rest ~= two items: indeterminate"
                 patMap
                 concreteKMapWithTwoItems
-                (MatchIndeterminate patMap concreteKMapWithTwoItems)
+                (MatchIndeterminate $ NE.singleton (patMap, concreteKMapWithTwoItems))
         , test
             "Keys disjoint and pattern keys are fully-concrete: fail"
             concreteKMapWithOneItemAndRest
             functionKMapWithOneItem
-            (failed $ DifferentValues concreteKMapWithOneItemAndRest functionKMapWithOneItem)
+            (failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] functionKMapWithOneItem)
         , let patMap =
                 kmap
                     [ (var "A" kmapKeySort, dv kmapElementSort "a")
@@ -286,7 +275,7 @@ kmapTerms =
                 "Disjoint non-singleton maps, non-concrete keys in pattern: indeterminate"
                 patMap
                 subjMap
-                (MatchIndeterminate patMap subjMap)
+                (MatchIndeterminate $ NE.singleton (patMap, subjMap))
         ]
   where
     kmap :: [(Term, Term)] -> Maybe VarName -> Term
@@ -300,7 +289,7 @@ cornerCases =
 
 test :: String -> Term -> Term -> MatchResult -> TestTree
 test name pat subj expected =
-    testCase name $ matchTerm testDefinition pat subj @?= expected
+    testCase name $ matchTerms Fun testDefinition pat subj @?= expected
 
 success :: [(VarName, Sort, Term)] -> MatchResult
 success assocs =
@@ -311,11 +300,11 @@ success assocs =
             ]
 
 failed :: FailReason -> MatchResult
-failed = MatchFailed . General
+failed = MatchFailed 
 
 errors :: String -> Term -> Term -> TestTree
 errors name pat subj =
     testCase name $
-        case matchTerm testDefinition pat subj of
+        case matchTerms Fun testDefinition pat subj of
             MatchFailed _ -> pure ()
             other -> assertFailure $ "Expected MatchFailed, got " <> show other