Bug with non-sequential list matching

[DavePearce]

Issue by DavePearce
Thursday Sep 06, 2012 at 18:43 GMT
Originally opened as Whiley/WhileyCompiler#124

---

There is a bug related to non-sequential list matching which the following excerpt from the types examples illustrates:

term Tuple[Type...]

rewrite Tuple{And{Type... xs}, Type... rest}:
    => let ys = { Tuple(x ++ rest) | x in xs }
       in And(ys)

The problem is that the non-sequential match will automatically consider the type of rest as being a set --- when in fact, it should really be a list. However, it's not completely clear how to model this example correctly (since i'm just concatenating the field onto the beginning of the list rest which is clearly wrong).

[DavePearce]

Comment by DavePearce
Thursday Sep 06, 2012 at 19:13 GMT

---

A syntax like this would be quite an interesting solution:

rewrite Tuple[Type... front, And{Type... xs}, Type... back]:
    => let ys = { Tuple(front ++ x ++ back) | x in xs }
       in And(ys)

In this case, we have actually dropped the set-based non-sequential match for a list-based one. Interesting, huh?