[Agda] coverage in Agda-2.1.3

[Ulf Norell]

On Wed, May 7, 2008 at 12:26 PM, Ana Bove <bove at cs.chalmers.se> wrote:

> However, your original comments is still interesting to understand. I
> would also agree with you that we do have exhaustive patterns. Actually,
> this is a correct partial program in 2.1.3
>
> fpair : forall {m n} -> Fin m -> Fin n -> Fin (m * n)
> fpair fzero     i = ?
> fpair (fsucc j) i = ?
>
> I would have expect then that dotting the m will do it
> fpair : forall {m n} -> Fin m -> Fin n -> Fin (m * n)
> fpair {.(succ m)} {n} fzero     i = ?
> fpair {.(succ m)} {n} (fsucc j) i = ?
>
> but it does not....


Sure it does. There are some issues with variable bindings above (you can't
bind variables in dotted patterns), but if we fix that the code goes
through:

fpair : forall {m n} -> Fin m -> Fin n -> Fin (m * n)
> fpair {.(succ _)} {n} fzero     i = ?
> fpair {.(succ _)} {n} (fsucc j) i = ?
>

Thorsten's initial attempt:

 fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
>  fpair {succ m} {n} fz     i = finl {n} {m × n} i
>  fpair {succ m} {n} (fs j) i = finr {n} {m × n} (fpair j i)
>

The reason this doesn't work is that pattern matching is performed
left-to-right: The pattern matching equations will (conceptually) be turned
into a tree of simple case distinctions starting with the left-most argument
that is being matched on. In this case that's m, so the case tree
corresponding to the fpair function is:

fpair {m} {n} j i =
  case m of
    succ m -> case j of
      fz -> finl ...
      fs j -> finr ...

The first case distinction is clearly missing a case for zero.

Now by dotting the patterns for m (which is also what happens when you leave
m implicit) you explain to the system that there should be no pattern
matching on m at all -- the patterns inside the dots are forced by the
pattern matching on j. In this case the case tree becomes

fpair {m} {n} j i =
  case j of
    fz -> finl ...
    fs j -> finr ...

which is clearly exhaustive.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080507/aa477f6a/attachment.html