From 7cf80fda8af607bf7423989d561923c62b3deb65 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 12 Jun 2026 13:21:22 +0000 Subject: [PATCH] booster/unit-tests/Pattern/MatchDispatch: exhaustive dispatch-class grid test for matchTerms One canonical pattern/subject term per Term constructor, crossed over all three match modes: 243 (mode, pattern, subject) cells, each asserting only the MatchResult class (success / decisive failure / indeterminate) against an explicit per-mode 9x9 expectation grid. The grids are the artifact: any change to the match1 dispatch table in Booster.Pattern.Match surfaces as a reviewable grid-cell diff, and the test documents the matcher's entire dispatch policy at a glance. Companion fine-grained tests (MatchEval and friends) continue to pin exact substitutions, failure reasons, and remainders; this module pins only the class. Co-Authored-By: Claude Fable 5 --- booster/hs-backend-booster.cabal | 1 + .../Test/Booster/Pattern/MatchDispatch.hs | 144 ++++++++++++++++++ 2 files changed, 145 insertions(+) create mode 100644 booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs diff --git a/booster/hs-backend-booster.cabal b/booster/hs-backend-booster.cabal index 34970ecf96..9f1a2768b9 100644 --- a/booster/hs-backend-booster.cabal +++ b/booster/hs-backend-booster.cabal @@ -471,6 +471,7 @@ test-suite unit-tests Test.Booster.Pattern.Binary Test.Booster.Pattern.Index Test.Booster.Pattern.InternalCollections + Test.Booster.Pattern.MatchDispatch Test.Booster.Pattern.MatchEval Test.Booster.Pattern.MatchImplies Test.Booster.Pattern.MatchRewrite diff --git a/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs b/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs new file mode 100644 index 0000000000..84d6617f02 --- /dev/null +++ b/booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs @@ -0,0 +1,144 @@ +{- | +Copyright : (c) Runtime Verification, 2026 +License : BSD-3-Clause + +Exhaustive dispatch-class test for the matcher: for every combination of +match mode ('Rewrite', 'Eval', 'Implies') and top-level term-constructor +pair, pin whether 'matchTerms' succeeds ('S'), fails decisively ('F'), or +defers as indeterminate ('I'). + +The point of this module is the 'grid' tables: they are an explicit, +reviewable statement of the matcher's dispatch policy over all +3 x 9 x 9 = 243 (mode, pattern, subject) combinations. Any change to the +@match1@ table in "Booster.Pattern.Match" shows up here as a grid-cell +diff, making the behavioural surface of a matcher refactor visible at a +glance. The companion fine-grained tests (Test.Booster.Pattern.MatchEval +and friends) pin exact substitutions, failure reasons, and remainders; +this module only pins the result /class/. + +Each term constructor is represented by one canonical pattern term and +one canonical subject term (see 'kinds'), chosen so that every cell's +class is deterministic and, where the dispatch descends into contents +(same-category pairs, \and decomposition, variable binding), the +contents resolve cleanly: + +* variables in canonical patterns are distinct from one another and from + subject variables (so the shared-variable check never interferes); +* the canonical \and subject has two /equal/ halves, so a variable + pattern binds against both without conflict; +* same-category canonical pairs match successfully (the diagonal is 'S'), + except where the mode itself defers (e.g. function-vs-function outside + 'Eval'); +* the canonical variable pattern has sort @someSort@, so collection + subjects (whose sorts are unrelated to @someSort@) exercise the + sort-mismatch failure of @matchVar@. +-} +module Test.Booster.Pattern.MatchDispatch ( + test_match_dispatch, +) where + +import Test.Tasty +import Test.Tasty.HUnit + +import Booster.Pattern.Base +import Booster.Pattern.Match +import Test.Booster.Fixture +import Test.Booster.Pattern.InternalCollections (emptyList, emptySet) + +-- | Result class of a 'MatchResult'. +data Outcome + = -- | 'MatchSuccess' + S + | -- | 'MatchFailed' (decisive) + F + | -- | 'MatchIndeterminate' (deferred) + I + deriving stock (Eq, Show) + +classOf :: MatchResult -> Outcome +classOf MatchSuccess{} = S +classOf MatchFailed{} = F +classOf MatchIndeterminate{} = I + +{- | One canonical (name, pattern term, subject term) triple per term +constructor, in the fixed axis order used by 'grid': + +@AndTerm, DomainValue, Injection, KMap, KList, KSet, ConsApplication, FunctionApplication, Var@ +-} +kinds :: [(String, Term, Term)] +kinds = + [ ("AndTerm", AndTerm (var "P1" someSort) (var "P2" someSort), AndTerm subjCons subjCons) + , ("DomainValue", dv someSort "d", dv someSort "d") + , + ( "Injection" + , Injection aSubsort someSort (var "PI" aSubsort) + , Injection aSubsort someSort (dv aSubsort "i") + ) + , ("KMap", emptyKMap, emptyKMap) + , ("KList", emptyList, emptyList) + , ("KSet", emptySet, emptySet) + , ("ConsApplication", app con1 [var "PC" someSort], subjCons) + , ("FunctionApplication", app f1 [var "PF" someSort], app f1 [dv someSort "f"]) + , ("Var", var "PX" someSort, var "SY" someSort) + ] + where + subjCons = app con1 [dv someSort "c"] + +{- | Expected dispatch class per mode: rows are the pattern constructor, +columns the subject constructor, both in 'kinds' order. + +Read e.g. @grid Eval !! 7 !! 1 == F@ as: in 'Eval' mode, a +'FunctionApplication' pattern against a 'DomainValue' subject fails +decisively. +-} +grid :: MatchType -> [[Outcome]] +grid Rewrite = + -- And DV Inj Map List Set Cons Fun Var + [ [S, S, S, F, F, F, S, S, S] -- AndTerm + , [F, S, F, F, F, F, F, I, I] -- DomainValue + , [F, F, S, F, F, F, F, I, I] -- Injection + , [F, F, F, S, F, F, F, I, I] -- KMap + , [F, F, F, F, S, F, F, I, I] -- KList + , [F, F, F, F, F, S, F, I, I] -- KSet + , [S, F, F, F, F, F, S, I, I] -- ConsApplication + , [I, I, I, I, I, I, I, I, I] -- FunctionApplication + , [S, S, S, F, F, F, S, S, S] -- Var + ] +grid Eval = + -- And DV Inj Map List Set Cons Fun Var + [ [I, S, S, F, F, F, S, S, I] -- AndTerm + , [I, S, F, F, F, F, F, I, I] -- DomainValue + , [I, F, S, F, F, F, F, I, I] -- Injection + , [I, F, I, S, F, F, F, I, I] -- KMap + , [I, F, I, F, S, F, F, I, I] -- KList + , [I, F, I, F, F, S, F, I, I] -- KSet + , [I, F, F, F, F, F, S, I, I] -- ConsApplication + , [I, F, F, F, F, F, I, S, I] -- FunctionApplication + , [I, S, S, F, F, F, S, S, S] -- Var + ] +grid Implies = + -- And DV Inj Map List Set Cons Fun Var + [ [S, S, S, F, F, F, S, S, S] -- AndTerm + , [F, S, F, F, F, F, F, I, I] -- DomainValue + , [F, F, S, F, F, F, F, I, I] -- Injection + , [F, F, F, S, F, F, F, I, I] -- KMap + , [F, F, F, F, S, F, F, I, I] -- KList + , [F, F, F, F, F, S, F, I, I] -- KSet + , [S, F, F, F, F, F, S, I, I] -- ConsApplication + , [I, I, I, I, I, I, I, I, I] -- FunctionApplication + , [S, S, S, F, F, F, S, S, S] -- Var + ] + +test_match_dispatch :: TestTree +test_match_dispatch = + testGroup + "matchTerms dispatch classes (mode x pattern x subject)" + [ testGroup + modeName + [ testCase (patName <> " vs " <> subjName) $ + classOf (matchTerms mode testDefinition patTerm subjTerm) @?= expected + | ((patName, patTerm, _), row) <- zip kinds (grid mode) + , ((subjName, _, subjTerm), expected) <- zip kinds row + ] + | (modeName, mode) <- [("Rewrite", Rewrite), ("Eval", Eval), ("Implies", Implies)] + ]