johnynek / bosatsu

A python-ish pure and total functional programming language
Apache License 2.0
223 stars 11 forks source link

Fix string pattern intersection commutativity issue #1086

Closed johnynek closed 7 months ago

johnynek commented 7 months ago
[info] TotalityTest:
[info] - intersection is commutative *** FAILED *** (37 milliseconds)
[info]   TestFailedException was thrown during property evaluation.
[info]     Message: eqA.eqv(a12, a21) was false List(StrPat(NonEmptyList(WildChar, WildStr, LitStr()))) != List(StrPat(NonEmptyList(WildChar, WildStr, WildStr, LitStr())))
[info]     Location: (SetOpsLaws.scala:24)
[info]     Occurred when passed generated values (
[info]       arg0 = StrPat(NonEmptyList(NamedStr(Operator("<")), List(WildChar))),
[info]       arg1 = StrPat(NonEmptyList(NamedStr(Name("d6qsd")), List(WildChar, WildStr))),
[info]       arg2 = org.bykn.bosatsu.TotalityTest$$anon$1@58dd1a19
[info]     )
[info]   Init Seed: 7409155706833916065

The intersection in both orders is semantically the same, but has two issues:

  1. there shouldn't be a trailing empty string
  2. we should not generate two adjacent WildStr values. Both of those are "unnormalized" patterns, but if we were to normalize the result is the same. Still it's better to fix it since it could have other cases where it fails in a serious way.