Skip to content

Commit 94693a8

Browse files
goodlyrottenapplegithub-actionsjberthold
authored
Matching code cleanup (#3820)
This is a followup to #3810 which: - removes the bidirectional matching code and `IsNotMatch` as the substitution produced by this code will always be a matching one - re-factor the list and map matching code adding comments describing the match cases in more detail --------- Co-authored-by: github-actions <[email protected]> Co-authored-by: Jost Berthold <[email protected]>
1 parent 3828397 commit 94693a8

File tree

7 files changed

+355
-410
lines changed

7 files changed

+355
-410
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -806,11 +806,6 @@ mkLogRewriteTrace
806806
{ reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)
807807
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
808808
}
809-
IsNotMatch r _ _ ->
810-
Failure
811-
{ reason = "Produced a non-match"
812-
, _ruleId = fmap getUniqueId (uniqueId $ Definition.attributes r)
813-
}
814809
RewriteSortError r _ _ ->
815810
Failure
816811
{ reason = "Sort error while unifying"

‎booster/library/Booster/Pattern/Match.hs

Lines changed: 279 additions & 317 deletions
Large diffs are not rendered by default.

‎booster/library/Booster/Pattern/Rewrite.hs

Lines changed: 0 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -269,13 +269,6 @@ applyRule pat@Pattern{ceilConditions} rule = runRewriteRuleAppT $ do
269269
MatchSuccess substitution ->
270270
pure substitution
271271

272-
-- check it is a "matching" substitution (substitutes variables
273-
-- from the subject term only). Fail the entire rewrite if not.
274-
unless (Map.keysSet subst == freeVariables rule.lhs) $ do
275-
let violatingItems = Map.restrictKeys subst (Map.keysSet subst `Set.difference` freeVariables rule.lhs)
276-
failRewrite $
277-
IsNotMatch rule pat.term violatingItems
278-
279272
-- Also fail the whole rewrite if a rule applies but may introduce
280273
-- an undefined term.
281274
unless (null rule.computedAttributes.notPreservesDefinednessReasons) $
@@ -398,8 +391,6 @@ data RewriteFailed k
398391
RuleConditionUnclear (RewriteRule k) Predicate
399392
| -- | A rewrite rule does not preserve definedness
400393
DefinednessUnclear (RewriteRule k) Pattern [NotPreservesDefinednessReason]
401-
| -- | A matching produced a non-match substitution
402-
IsNotMatch (RewriteRule k) Term Substitution
403394
| -- | A sort error was detected during m,atching
404395
RewriteSortError (RewriteRule k) Term SortError
405396
| -- | An error was detected during matching
@@ -434,15 +425,6 @@ instance Pretty (RewriteFailed k) where
434425
, "because of:"
435426
]
436427
++ map pretty reasons
437-
pretty (IsNotMatch rule term subst) =
438-
hsep
439-
[ "Produced a non-match:"
440-
, pretty $ Map.toList subst
441-
, "when matching rule"
442-
, ruleLabelOrLoc rule
443-
, "with term"
444-
, pretty term
445-
]
446428
pretty (RewriteSortError rule term sortError) =
447429
hsep
448430
[ "Sort error while unifying"

‎booster/unit-tests/Test/Booster/Fixture.hs

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -147,6 +147,7 @@ emptyKMap
147147
, concreteKMapWithOneItem
148148
, concreteKMapWithTwoItems
149149
, concreteKMapWithOneItemAndRest
150+
, concreteKeySymbolicValueKMapWithRest
150151
, symbolicKMapWithOneItem
151152
, symbolicKMapWithTwoItems
152153
, concreteAndSymbolicKMapWithTwoItems
@@ -172,6 +173,15 @@ concreteKMapWithOneItemAndRest =
172173
)
173174
]
174175
(Just [trm| REST:SortTestKMap{}|])
176+
concreteKeySymbolicValueKMapWithRest =
177+
KMap
178+
testKMapDefinition
179+
[
180+
( [trm| \dv{SortTestKMapKey{}}("key") |]
181+
, [trm| A:SortTestKMapItem{} |]
182+
)
183+
]
184+
(Just [trm| REST:SortTestKMap{}|])
175185
concreteKMapWithTwoItems =
176186
KMap
177187
testKMapDefinition
@@ -190,7 +200,7 @@ symbolicKMapWithOneItem =
190200
testKMapDefinition
191201
[
192202
( [trm| \dv{SortTestKMapKey{}}("key") |]
193-
, [trm| A:SortTestKMapItem{} |]
203+
, [trm| B:SortTestKMapItem{} |]
194204
)
195205
]
196206
Nothing
@@ -234,7 +244,7 @@ functionKMapWithOneItem =
234244
testKMapDefinition
235245
[
236246
( [trm| g{}() |]
237-
, [trm| B:SortTestKMapItem{} |]
247+
, [trm| \dv{SortTestKMapItem{}}("value") |]
238248
)
239249
]
240250
Nothing

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

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ varsAndValues =
118118
, let v1 = var "X" someSort
119119
v2 = var "X" differentSort
120120
in test "same variable name, different sort" v1 v2 $
121-
failed (DifferentSorts v1 v2)
121+
failed (VariableConflict (Variable someSort "X") v1 v2)
122122
, let d1 = dv someSort "1"
123123
d2 = dv someSort "1"
124124
in test "same domain values (same sort)" d1 d2 $
@@ -145,7 +145,8 @@ varsAndValues =
145145
failed (DifferentSorts v d)
146146
, let v = var "X" someSort
147147
d = dv someSort ""
148-
in test "dv matching a var (on RHS): indeterminate" d v $
148+
in -- see https://github.com/runtimeverification/hs-backend-booster/issues/231
149+
test "dv matching a var (on RHS): indeterminate" d v $
149150
MatchIndeterminate $
150151
NE.singleton (d, v)
151152
, let d = dv someSort ""
@@ -177,7 +178,7 @@ andTerms =
177178
ca = app con1 [da]
178179
cb = app con1 [db]
179180
in test
180-
"And-term on the left, one unifies one fails"
181+
"And-term on the left, one matches one fails"
181182
(AndTerm ca cb)
182183
ca
183184
(failed $ DifferentValues db da)
@@ -209,17 +210,17 @@ kmapTerms =
209210
"Non-empty concrete KMap ~= empty KMap: fails"
210211
concreteKMapWithOneItem
211212
emptyKMap
212-
(failed $ DifferentValues concreteKMapWithOneItem emptyKMap)
213+
(failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap)
213214
, test
214215
"Non-empty symbolic KMap ~= empty KMap: fails"
215216
symbolicKMapWithOneItem
216217
emptyKMap
217-
(failed $ DifferentValues symbolicKMapWithOneItem emptyKMap)
218+
(failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap)
218219
, test
219220
"Non-empty symbolic KMap ~= non-empty concrete KMap, same key: matches contained value"
220221
symbolicKMapWithOneItem -- "key" -> A
221222
concreteKMapWithOneItem -- "key" -> "value"
222-
(success [("A", kmapElementSort, dv kmapElementSort "value")])
223+
(success [("B", kmapElementSort, dv kmapElementSort "value")])
223224
, test
224225
"One key and rest variable ~= same key: Match rest with empty map"
225226
concreteKMapWithOneItemAndRest
@@ -233,12 +234,11 @@ kmapTerms =
233234
in success [("REST", kmapSort, restMap)]
234235
)
235236
, -- pattern has more assocs than subject
236-
let patRest = kmap [(dv kmapKeySort "key2", dv kmapElementSort "value2")] Nothing
237-
in test
238-
"Extra concrete key in pattern, no rest in subject: fail on rest"
239-
concreteKMapWithTwoItems
240-
concreteKMapWithOneItem
241-
(failed $ DifferentValues patRest emptyKMap)
237+
test
238+
"Extra concrete key in pattern, no rest in subject: fail on rest"
239+
concreteKMapWithTwoItems
240+
concreteKMapWithOneItem
241+
(failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] emptyKMap)
242242
, -- cases with disjoint keys
243243
test
244244
"Variable key ~= concrete key (and common element) without rest: match key"
@@ -261,10 +261,10 @@ kmapTerms =
261261
concreteKMapWithTwoItems
262262
(MatchIndeterminate $ NE.singleton (patMap, concreteKMapWithTwoItems))
263263
, test
264-
"Keys disjoint and pattern keys are fully-concrete: fail"
264+
"Pattern keys are fully-concrete, subject key function: indeterminate"
265265
concreteKMapWithOneItemAndRest
266266
functionKMapWithOneItem
267-
(failed $ DifferentValues concreteKMapWithOneItemAndRest functionKMapWithOneItem)
267+
(MatchIndeterminate $ NE.singleton (concreteKMapWithOneItemAndRest, functionKMapWithOneItem))
268268
, let patMap =
269269
kmap
270270
[ (var "A" kmapKeySort, dv kmapElementSort "a")

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

Lines changed: 47 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ sorts =
6868
"sort variables"
6969
[ test "sort variable in pattern" (app con1 [varX]) (app con1 [dSome]) $
7070
sortErr (FoundSortVariable "sort me!")
71-
, test "sort variable in subject" (app con1 [dSub]) (app con1 [varZ]) $
71+
, test "sort variable in subject" (app con1 [varZ]) (app con1 [dSub]) $
7272
sortErr (FoundSortVariable "me, too!")
7373
, test "several sort variables" (app con3 [varX, varY]) (app con3 [dSome, varZ]) $
7474
sortErr (FoundSortVariable "sort me!")
@@ -85,7 +85,7 @@ sorts =
8585
constructors :: TestTree
8686
constructors =
8787
testGroup
88-
"Unifying constructors"
88+
"Matching constructors"
8989
[ test
9090
"same constructors, one variable argument"
9191
(app con1 [var "X" someSort])
@@ -176,7 +176,7 @@ varsAndValues =
176176
, let v1 = var "X" someSort
177177
v2 = var "Y" aSubsort
178178
in test "two variables (v2 subsort v1)" v1 v2 $
179-
success [("X", someSort, v2)]
179+
success [("X", someSort, inj aSubsort someSort v2)]
180180
, let v1 = var "X" aSubsort
181181
v2 = var "Y" someSort
182182
in test "two variables (v1 subsort v2)" v1 v2 $
@@ -276,22 +276,22 @@ internalLists =
276276
"Concrete lists of different length fail to match"
277277
two
278278
three
279-
(failed $ DifferentValues two three)
279+
(failed $ DifferentValues emptyList $ klist [headElem] Nothing)
280280
, test
281281
"Empty and non-empty list fail to match (symbolic tail)"
282282
headList
283283
emptyList
284284
(failed $ DifferentValues headList emptyList)
285285
, test
286-
"Empty and non-empty list fail to match (symbolic init)"
286+
"Non-empty and empty list fail to match (symbolic init)"
287287
tailList
288288
emptyList
289289
(failed $ DifferentValues tailList emptyList)
290290
, test
291-
"Unification failures may swap the argument lists"
291+
"Empty and non-empty list fail to match (symbolic init)"
292292
emptyList
293293
tailList
294-
(failed $ DifferentValues tailList emptyList)
294+
(failed $ DifferentValues emptyList tailList)
295295
, test
296296
"Head list and tail list produce indeterminate unification"
297297
headList
@@ -350,7 +350,7 @@ internalLists =
350350
(replicate 3 headElem)
351351
(Just (var "LIST2" listSort, replicate 3 lastElem))
352352
in test
353-
"Unifies two lists with symbolic middle (binding LIST1)"
353+
"Match two lists with symbolic middle (binding LIST1)"
354354
list1
355355
list2
356356
(success [("LIST1", listSort, klist [] (Just (var "LIST2" listSort, [lastElem])))])
@@ -363,10 +363,12 @@ internalLists =
363363
(replicate 3 headElem)
364364
(Just (var "LIST2" listSort, replicate 3 lastElem))
365365
in test
366-
"Unifies two lists with symbolic middle (binding LIST1), reverse direction"
366+
"Match two lists with symbolic middle, reverse direction indeterminate"
367367
list2
368368
list1
369-
(success [("LIST1", listSort, klist [] (Just (var "LIST2" listSort, [lastElem])))])
369+
( remainder
370+
[(klist [] (Just (var "LIST2" listSort, [lastElem])), klist [] (Just (var "LIST1" listSort, [])))]
371+
)
370372
]
371373
where
372374
headElem = [trm| \dv{SomeSort{}}("head") |]
@@ -389,23 +391,30 @@ internalMaps =
389391
concreteKMapWithTwoItems
390392
(success [])
391393
, test
392-
"Can match a concrete and symbolic map"
393-
concreteKMapWithOneItem
394+
"Can match a symbolic and concrete map"
394395
symbolicKMapWithOneItem
395-
(success [("A", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value")|])])
396+
concreteKMapWithOneItem
397+
(success [("B", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value")|])])
396398
, test
397-
"Can match a concrete and symbolic map with two elements"
398-
concreteKMapWithTwoItems
399+
"Can match a symbolic and concrete map with two elements"
399400
symbolicKMapWithTwoItems
401+
concreteKMapWithTwoItems
400402
( success
401403
[ ("A", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value")|])
402404
, ("B", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value2")|])
403405
]
404406
)
405407
, test
406-
"Can match {\"key\" |-> \"value\", ...REST} with {A |-> \"value\"}"
407-
concreteKMapWithOneItemAndRest
408+
"Can match {\"key\" |-> A, ...REST} with {\"key\" |-> B}"
409+
concreteKeySymbolicValueKMapWithRest
408410
symbolicKMapWithOneItem
411+
( success
412+
[("REST", kmapSort, emptyKMap), ("A", kmapElementSort, [trm| B:SortTestKMapItem{} |])]
413+
)
414+
, test
415+
"Can match {\"key\" |-> A, ...REST} with {\"key\" |-> \"value\"}"
416+
concreteKeySymbolicValueKMapWithRest
417+
concreteKMapWithOneItem
409418
( success
410419
[("REST", kmapSort, emptyKMap), ("A", kmapElementSort, [trm| \dv{SortTestKMapItem{}}("value")|])]
411420
)
@@ -428,28 +437,27 @@ internalMaps =
428437
)
429438
]
430439
)
431-
, -- TODO: re-enable once we re-factor the map matching
432-
-- this would not produce a matchign substitution and should therefore fail
440+
, -- this would not produce a matching substitution and should therefore fail
433441
-- at match time
434-
-- , test
435-
-- "Fails to match {\"key\" |-> \"value\", A |-> \"value2\"} with {\"key\" |-> \"value\", ...REST}"
436-
-- concreteAndSymbolicKMapWithTwoItems
437-
-- concreteKMapWithOneItemAndRest
438-
-- ( failed $
439-
-- DifferentSymbols
440-
-- ( KMap
441-
-- testKMapDefinition
442-
-- [
443-
-- ( [trm| A:SortTestKMapKey{}|]
444-
-- , [trm| \dv{SortTestKMapItem{}}("value2") |]
445-
-- )
446-
-- ]
447-
-- Nothing
448-
-- )
449-
-- (KMap testKMapDefinition [] (Just [trm| REST:SortTestKMap{}|]))
450-
-- )
451442
test
452-
"Can match {\"f()\" |-> \"value\", ...REST} with {\"f()\" |-> B}"
443+
"Fails to match {\"key\" |-> \"value\", A |-> \"value2\"} with {\"key\" |-> \"value\", ...REST}"
444+
concreteAndSymbolicKMapWithTwoItems
445+
concreteKMapWithOneItemAndRest
446+
( failed $
447+
DifferentSymbols
448+
( KMap
449+
testKMapDefinition
450+
[
451+
( [trm| A:SortTestKMapKey{}|]
452+
, [trm| \dv{SortTestKMapItem{}}("value2") |]
453+
)
454+
]
455+
Nothing
456+
)
457+
(KMap testKMapDefinition [] (Just [trm| REST:SortTestKMap{}|]))
458+
)
459+
, test
460+
"Can match {\"f()\" |-> \"value\", ...REST} with {\"f()\" |-> \"value\"}"
453461
functionKMapWithOneItemAndRest
454462
functionKMapWithOneItem
455463
( success
@@ -461,23 +469,18 @@ internalMaps =
461469
[]
462470
Nothing
463471
)
464-
,
465-
( "B"
466-
, SortApp "SortTestKMapItem" []
467-
, [trm| \dv{SortTestKMapItem{}}("value") |]
468-
)
469472
]
470473
)
471474
, test
472475
"Empty and non-empty concrete map fail to match"
473476
emptyKMap
474477
concreteKMapWithOneItem
475-
(failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key")|] emptyKMap)
478+
(failed $ DifferentSymbols emptyKMap concreteKMapWithOneItem)
476479
, test
477480
"Concrete maps of different length fail to match"
478481
concreteKMapWithTwoItems
479482
concreteKMapWithOneItem
480-
(failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] concreteKMapWithOneItem)
483+
(failed $ KeyNotFound [trm| \dv{SortTestKMapKey{}}("key2")|] emptyKMap)
481484
, test
482485
"Symbolic non-empty map and empty map fail to match"
483486
symbolicKMapWithOneItem

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

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -202,16 +202,9 @@ rewriteSuccess =
202202
, [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
203203
)
204204
unifyNotMatch =
205-
testCase "Indeterminate case when subject has variables" $ do
206-
let t =
207-
[trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
208-
-- "non-match" substitution:
209-
subst =
210-
Map.fromList
211-
[ (Variable someSort "X", dv someSort "otherThing")
212-
]
213-
[trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
214-
`failsWith` IsNotMatch rule3 t subst
205+
testCase "Stuck case when subject has variables" $
206+
getsStuck
207+
[trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
215208
definednessUnclear =
216209
testCase "con4 rewrite to f2 might become undefined" $ do
217210
let pcon4 =

0 commit comments

Comments
 (0)