search

johnynek / bosatsu

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

fix totality check flake #1106

Closed johnynek closed 5 months ago

johnynek commented 6 months ago 
[info] - missing branches, if added are total and none of the missing are unreachable *** FAILED *** (82 milliseconds)
[info]   TestFailedException was thrown during property evaluation.
[info]     Message: after adding List(ListPat(List()), ListPat(List(Item(ListPat(List())), WildList)), ListPat(List(Item(ListPat(List(Item(WildCard)))), WildList)), ListPat(List(Item(ListPat(List(Item(WildCard), Item(WildCard), WildList))), Item(WildCard), WildList))) we still need List(ListPat(List(Item(StrPat(NonEmptyList(WildChar, WildChar, WildStr))), WildList)), ListPat(List(Item(StrPat(NonEmptyList(WildChar, LitStr()))))), ListPat(List(Item(StrPat(NonEmptyList(WildChar, LitStr()))), Item(StrPat(NonEmptyList(WildChar, WildChar, WildStr))), WildList)), ListPat(List(Item(StrPat(NonEmptyList(WildChar, LitStr()))), Item(StrPat(NonEmptyList(WildChar, LitStr()))), WildList)), ListPat(List(Item(StrPat(NonEmptyList(WildChar, LitStr()))), Item(StrPat(NonEmptyList(LitStr()))), WildList)), ListPat(List(Item(StrPat(NonEmptyList(LitStr()))), WildList)))
[info]     Location: (SetOpsLaws.scala:253)
[info]     Occurred when passed generated values (
[info]       arg0 = List(ListPat(List(NamedList(Name("kobpwjG")), Item(StrPat(NonEmptyList(NamedChar(Name("nh0nLwb")), List()))), Item(Named(Operator("?"), StrPat(NonEmptyList(NamedChar(Name("lday3stkt")), List())))), Item(Literal(Integer(-2607897800403171538))))), ListPat(List(Item(ListPat(List(Item(Var(Operator("$"))), Item(Var(Operator("%"))), WildList)))))) // 1 shrink
[info]     )
[info]   Init Seed: -8926999526878949353
johnynek commented 6 months ago

failed in PR: https://github.com/johnynek/bosatsu/pull/1102 so should fail against master 78a2951d96983f3f8ff9e45ec21787734e55075f

johnynek commented 6 months ago 
    List(
      ListPat(
        List(
          NamedList(Name("kobpwjG")),
          Item(StrPat(NonEmptyList(NamedChar(Name("nh0nLwb")), List()))),
          Item(Named(Operator("?"), StrPat(NonEmptyList(NamedChar(Name("lday3stkt")), List())))),
          Item(Literal(Integer(-2607897800403171538)))
        )
      ),
      ListPat(
        List(
          Item(ListPat(List(Item(Var(Operator("$"))), Item(Var(Operator("%"))), WildList)))
        )
      )
    )

Note this pattern is ill-typed anyway. No value is the same type as all the items in this list.

johnynek commented 6 months ago

simplifying this:

    // these are ill typed because the first pattern matches type
    // List[String] but the second matches List[List[String]]
    val r1 @ (_ :: _ :: _) = patterns("""[[*foo, "$.{_}", "1"], [[_, *_]]]""")

    patterns("""[[*foo, "$.{_}", "$.{_}"], [[b, *_]]]""") ::

so, test fails, but the pattern is ill typed, and all well typed translations seems to pass.