[Agda] Influencing pattern matching order [Was: Absurd pattern;
convincing Agda]
Dominique Devriese
dominique.devriese at cs.kuleuven.be
Tue Jun 12 15:50:27 CEST 2012
Paul,
The problem is indeed in the order of pattern matching in the
outerIsEq function.
When you write
outerIsEq : (t : Term) → Bool
outerIsEq (var x args) = false
outerIsEq (con c args) = false
outerIsEq (def f args) with Data.Nat._≟_ (length args) 4
outerIsEq (def f []) | yes ()
outerIsEq (def f (x ∷ [])) | yes
() (1)
outerIsEq (def f (x ∷ x₁ ∷ x₂ ∷ [])) | yes
() (2)
...
outerIsEq (def f []) | no ¬p = false
outerIsEq (def f (x ∷ xs)) | no ¬p = false
Agda's internal compiled version of outerIsEq will first pattern match
on args and only after that on the result of "Data.Nat._≟_ (length
args) 4". This means that it will only look at the result of the
latter after it has been able to decide between all alternatives for
args.
In your pattern that does not typecheck,
withoutEQ (def f (x ∷ xs)) () | no ¬p -- unsolved meta - why??
the type of the absurd pattern is "outerIsEq (def f (x ∷ xs)) | no
¬p". This does not reduce to "false = true", because Agda cannot
decide between all the patterns for args, since it only knows that
args = x ∷ xs, with xs unknown, which does not allow differentiating
between for example the patterns on lines marked (1) and (2) above.
Note: this means that your problem is not specific to the absurd pattern,
the problem is in the reduction behaviour of the type of the absurd
pattern, which would also lead to problems in similar situations without
an absurd pattern.
One solution that I have used before is the following. You can
influence the order of the pattern matches that Agda will compile your
outerIsEq function to by adding fake "with" pattern matches on known
values:
outerIsEq (def f args) with Data.Nat._≟_ (length args) 4
outerIsEq (def f args) | yes p with tt
outerIsEq (def f []) | yes () | tt
outerIsEq (def f (x ∷ [])) | yes () | tt
outerIsEq (def f (x ∷ x₁ ∷ [])) | yes () | tt
...
outerIsEq (def f args) | no ¬p with tt
outerIsEq (def f []) | no ¬p
| tt = false
outerIsEq (def f (x ∷ xs)) | no ¬p
| tt = false
This forces Agda to first pattern match on the result of "Data.Nat._≟_
(length args) 4" before it matches on args. Your absurd pattern then
compiles fine.
withoutEQ (def f []) () | no ¬p
withoutEQ (def f (x ∷ xs)) () | no ¬p
Note: there may be better solutions to this problem, and I'd be interested
to know about them.
Kind regards,
Dominique
2012/6/12 Paul van der Walt <paul at denknerd.org>:
> Dear all,
>
> I asked this question on IRC, but it was rather quiet there, so
> maybe someone here could help me out.
>
> I am using the Reflection API, and I'd like to manipulate a
> value of type Term which is returned by quoteTerm. I have a
> function which only works for Terms of the form (something ==
> true), and this function should return the LHS if the Term has
> this form. To make this function total, I also have a
> predicate (validity of input checker) which only returns true
> for the cases I want to take care of. See the functions here:
> http://hpaste.org/69846 (excuse the formatting)
>
> The problem is, one of the absurd patterns is accepted by Agda,
> but remains yellow. This causes problems when trying to use the
> module elsewhere. I can clearly see that this case can never be
> reached (order of patterns matters here), but Agda doesn't
> believe me.
>
> Does anyone know how I can solve this? Maybe my approach is
> really ugly?
>
> Thanks in advance, I hope my question is clear enough.
>
> Cheers,
> Paul van der Walt
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
More information about the Agda
mailing list