Do other systems have better solutions to this problem? I vaguely remember coming across a huge flamewar on the epigram mailing list a while back about something very similar to this. Has there been any progress in avoiding unnecessary implicit case splits while still having a sound backing?<div>
<br></div><div>Thanks,</div><div>Dan<br><br><div class="gmail_quote">On Tue, Jun 12, 2012 at 10:54 AM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Paul,<br>
<br>
this is how to convince Agda. Just split one level deeper:<br>
<br>
withoutEQ (def f (x ∷ [])) () | no ¬p<br>
withoutEQ (def f (x ∷ x₁ ∷ xs)) () | no ¬p<br>
<br>
Now the unsolved meta is gone.<br>
<br>
The problem was that the equations given for a match do not always hold literally. In you case, this equation does not reduce:<br>
<br>
outerIsEq (def f (x ∷ xs)) | no ¬p = false<br>
<br>
This is because internally, Agda decided it wants to split on xs before reducing. I'd consider this unwanted behavior on the side of Agda. See:<br>
<br>
<a href="http://code.google.com/p/agda/issues/detail?id=408" target="_blank">http://code.google.com/p/agda/<u></u>issues/detail?id=408</a><br>
<br>
In a simple case, consider the equations<br>
<br>
and : Bool -> Bool -> Bool<br>
and false x = false<br>
and y false = false<br>
and _ _ = true<br>
<br>
One of<br>
<br>
and false x<br>
and y false<br>
<br>
will not reduce to false, since Agda converts this definition into a case tree, so it will either match on the first (likely) or the second argument. So you will likely get the equations<br>
<br>
and false x = false<br>
and true false = false<br>
and true true = true<br>
<br>
and the type<br>
<br>
and y false == false<br>
<br>
will not be empty.<br>
<br>
Why in your specific case you do not get the equations you specified, I cannot tell.<br>
<br>
Hope that helps.<br>
<br>
Cheers,<br>
Andreas<div><div><br>
<br>
On 12.06.2012 14:36, Paul van der Walt wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>
Dear all,<br>
<br>
I asked this question on IRC, but it was rather quiet there, so<br>
maybe someone here could help me out.<br>
<br>
I am using the Reflection API, and I'd like to manipulate a<br>
value of type Term which is returned by quoteTerm. I have a<br>
function which only works for Terms of the form (something ==<br>
true), and this function should return the LHS if the Term has<br>
this form. To make this function total, I also have a<br>
predicate (validity of input checker) which only returns true<br>
for the cases I want to take care of. See the functions here:<br>
<a href="http://hpaste.org/69846" target="_blank">http://hpaste.org/69846</a> (excuse the formatting)<br>
<br>
The problem is, one of the absurd patterns is accepted by Agda,<br>
but remains yellow. This causes problems when trying to use the<br>
module elsewhere. I can clearly see that this case can never be<br>
reached (order of patterns matters here), but Agda doesn't<br>
believe me.<br>
<br>
Does anyone know how I can solve this? Maybe my approach is<br>
really ugly?<br>
<br>
Thanks in advance, I hope my question is clear enough.<br>
<br>
Cheers,<br>
Paul van der Walt<br>
<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><span><font color="#888888"><br>
</font></span></blockquote><span><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br>
</div>