[Agda] Overlapping patterns in function definition -- strange behavior

[Ulf Norell]

On Thu, Jun 16, 2011 at 4:55 PM, Alan Jeffrey <ajeffrey at bell-labs.com>wrote:

> Adding:
>
>  baz : Bool → String
>  baz true = "true"
>  baz false = "false"
>
>  main = run (putStrLn (baz (foo 1 true)))
>
> to your file and compiling with "agda -c" shows that MAlonzo agrees with
> your intuition.  The code generated by MAlonzo is essentially the direct
> translation of Agda pattern matching into Haskell pattern matching.
>
> This looks like a bug to me.  (Personally I think the compiler is right and
> the interpreter is wrong, but there may be subtleties I'm not aware of.)
>

The reason they disagree is that the compiler is using the Agda clauses as
they stand (more or less), whereas the interpreter compiles the pattern
matching to a case tree for evaluation. This looks like a bug in the case
tree generation.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110616/1d3deec5/attachment.html