Skip to content

Commit f89bcc7

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents d4dc50c + eb2da06 commit f89bcc7

2 files changed

Lines changed: 145 additions & 0 deletions

File tree

‎booster/hs-backend-booster.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -471,6 +471,7 @@ test-suite unit-tests
471471
Test.Booster.Pattern.Binary
472472
Test.Booster.Pattern.Index
473473
Test.Booster.Pattern.InternalCollections
474+
Test.Booster.Pattern.MatchDispatch
474475
Test.Booster.Pattern.MatchEval
475476
Test.Booster.Pattern.MatchImplies
476477
Test.Booster.Pattern.MatchRewrite

‎booster/unit-tests/Test/Booster/Pattern/MatchDispatch.hs‎

Lines changed: 144 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,144 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2026
3+
License : BSD-3-Clause
4+
5+
Exhaustive dispatch-class test for the matcher: for every combination of
6+
match mode ('Rewrite', 'Eval', 'Implies') and top-level term-constructor
7+
pair, pin whether 'matchTerms' succeeds ('S'), fails decisively ('F'), or
8+
defers as indeterminate ('I').
9+
10+
The point of this module is the 'grid' tables: they are an explicit,
11+
reviewable statement of the matcher's dispatch policy over all
12+
3 x 9 x 9 = 243 (mode, pattern, subject) combinations. Any change to the
13+
@match1@ table in "Booster.Pattern.Match" shows up here as a grid-cell
14+
diff, making the behavioural surface of a matcher refactor visible at a
15+
glance. The companion fine-grained tests (Test.Booster.Pattern.MatchEval
16+
and friends) pin exact substitutions, failure reasons, and remainders;
17+
this module only pins the result /class/.
18+
19+
Each term constructor is represented by one canonical pattern term and
20+
one canonical subject term (see 'kinds'), chosen so that every cell's
21+
class is deterministic and, where the dispatch descends into contents
22+
(same-category pairs, \and decomposition, variable binding), the
23+
contents resolve cleanly:
24+
25+
* variables in canonical patterns are distinct from one another and from
26+
subject variables (so the shared-variable check never interferes);
27+
* the canonical \and subject has two /equal/ halves, so a variable
28+
pattern binds against both without conflict;
29+
* same-category canonical pairs match successfully (the diagonal is 'S'),
30+
except where the mode itself defers (e.g. function-vs-function outside
31+
'Eval');
32+
* the canonical variable pattern has sort @someSort@, so collection
33+
subjects (whose sorts are unrelated to @someSort@) exercise the
34+
sort-mismatch failure of @matchVar@.
35+
-}
36+
module Test.Booster.Pattern.MatchDispatch (
37+
test_match_dispatch,
38+
) where
39+
40+
import Test.Tasty
41+
import Test.Tasty.HUnit
42+
43+
import Booster.Pattern.Base
44+
import Booster.Pattern.Match
45+
import Test.Booster.Fixture
46+
import Test.Booster.Pattern.InternalCollections (emptyList, emptySet)
47+
48+
-- | Result class of a 'MatchResult'.
49+
data Outcome
50+
= -- | 'MatchSuccess'
51+
S
52+
| -- | 'MatchFailed' (decisive)
53+
F
54+
| -- | 'MatchIndeterminate' (deferred)
55+
I
56+
deriving stock (Eq, Show)
57+
58+
classOf :: MatchResult -> Outcome
59+
classOf MatchSuccess{} = S
60+
classOf MatchFailed{} = F
61+
classOf MatchIndeterminate{} = I
62+
63+
{- | One canonical (name, pattern term, subject term) triple per term
64+
constructor, in the fixed axis order used by 'grid':
65+
66+
@AndTerm, DomainValue, Injection, KMap, KList, KSet, ConsApplication, FunctionApplication, Var@
67+
-}
68+
kinds :: [(String, Term, Term)]
69+
kinds =
70+
[ ("AndTerm", AndTerm (var "P1" someSort) (var "P2" someSort), AndTerm subjCons subjCons)
71+
, ("DomainValue", dv someSort "d", dv someSort "d")
72+
,
73+
( "Injection"
74+
, Injection aSubsort someSort (var "PI" aSubsort)
75+
, Injection aSubsort someSort (dv aSubsort "i")
76+
)
77+
, ("KMap", emptyKMap, emptyKMap)
78+
, ("KList", emptyList, emptyList)
79+
, ("KSet", emptySet, emptySet)
80+
, ("ConsApplication", app con1 [var "PC" someSort], subjCons)
81+
, ("FunctionApplication", app f1 [var "PF" someSort], app f1 [dv someSort "f"])
82+
, ("Var", var "PX" someSort, var "SY" someSort)
83+
]
84+
where
85+
subjCons = app con1 [dv someSort "c"]
86+
87+
{- | Expected dispatch class per mode: rows are the pattern constructor,
88+
columns the subject constructor, both in 'kinds' order.
89+
90+
Read e.g. @grid Eval !! 7 !! 1 == F@ as: in 'Eval' mode, a
91+
'FunctionApplication' pattern against a 'DomainValue' subject fails
92+
decisively.
93+
-}
94+
grid :: MatchType -> [[Outcome]]
95+
grid Rewrite =
96+
-- And DV Inj Map List Set Cons Fun Var
97+
[ [S, S, S, F, F, F, S, S, S] -- AndTerm
98+
, [F, S, F, F, F, F, F, I, I] -- DomainValue
99+
, [F, F, S, F, F, F, F, I, I] -- Injection
100+
, [F, F, F, S, F, F, F, I, I] -- KMap
101+
, [F, F, F, F, S, F, F, I, I] -- KList
102+
, [F, F, F, F, F, S, F, I, I] -- KSet
103+
, [S, F, F, F, F, F, S, I, I] -- ConsApplication
104+
, [I, I, I, I, I, I, I, I, I] -- FunctionApplication
105+
, [S, S, S, F, F, F, S, S, S] -- Var
106+
]
107+
grid Eval =
108+
-- And DV Inj Map List Set Cons Fun Var
109+
[ [I, S, S, F, F, F, S, S, I] -- AndTerm
110+
, [I, S, F, F, F, F, F, I, I] -- DomainValue
111+
, [I, F, S, F, F, F, F, I, I] -- Injection
112+
, [I, F, I, S, F, F, F, I, I] -- KMap
113+
, [I, F, I, F, S, F, F, I, I] -- KList
114+
, [I, F, I, F, F, S, F, I, I] -- KSet
115+
, [I, F, F, F, F, F, S, I, I] -- ConsApplication
116+
, [I, F, F, F, F, F, I, S, I] -- FunctionApplication
117+
, [I, S, S, F, F, F, S, S, S] -- Var
118+
]
119+
grid Implies =
120+
-- And DV Inj Map List Set Cons Fun Var
121+
[ [S, S, S, F, F, F, S, S, S] -- AndTerm
122+
, [F, S, F, F, F, F, F, I, I] -- DomainValue
123+
, [F, F, S, F, F, F, F, I, I] -- Injection
124+
, [F, F, F, S, F, F, F, I, I] -- KMap
125+
, [F, F, F, F, S, F, F, I, I] -- KList
126+
, [F, F, F, F, F, S, F, I, I] -- KSet
127+
, [S, F, F, F, F, F, S, I, I] -- ConsApplication
128+
, [I, I, I, I, I, I, I, I, I] -- FunctionApplication
129+
, [S, S, S, F, F, F, S, S, S] -- Var
130+
]
131+
132+
test_match_dispatch :: TestTree
133+
test_match_dispatch =
134+
testGroup
135+
"matchTerms dispatch classes (mode x pattern x subject)"
136+
[ testGroup
137+
modeName
138+
[ testCase (patName <> " vs " <> subjName) $
139+
classOf (matchTerms mode testDefinition patTerm subjTerm) @?= expected
140+
| ((patName, patTerm, _), row) <- zip kinds (grid mode)
141+
, ((subjName, _, subjTerm), expected) <- zip kinds row
142+
]
143+
| (modeName, mode) <- [("Rewrite", Rewrite), ("Eval", Eval), ("Implies", Implies)]
144+
]

0 commit comments

Comments
 (0)