Core case expression requires total pattern matches?

[phile314]

Hi Atze,

Running the first regression tests on the Agda UHC backend already did catch some first bugs.... which raised a question about UHC Core. When I compile Haskell programs, one Core case alternative is produced for each possible constructor. Eg the following HS produces following pseudo-core:

data A = B | C | D | E | F

f :: A -> Int
f C = 1
f _ = 2

produces

case temp of
    Tag 0 -> 2
    Tag 1 -> 2
    Tag 2 -> 1
    Tag 3 -> 2
    Tag 4 -> 2

Now it seems that stuff starts to break when I instead use the default-branch instead of replicating the default value for all not-covered constructors. Eg.

case temp of
    Tag 2 -> 1
    default -> 2

This will yield the wrong result.

What is the best way forward? Should I just generate "total" case alternatives as well? Speaking just for myself, I think using the default feels more elegant, but I don't care too much about it. Otherwise I would just document the current behaviour in the Core API and not expose the default-alternative anymore.

Philipp

[atzedijkstra]

Hi Philipp,

actually the default should be removed as it is mot used, hence it obviously breaks :-). So, for now, saturated alternatives are the way to go. I am considering, for some time already, a design where each alternative has a set of matching tags instead of just one, and/or a revival of the use of default. We can discuss this later.

A

Atze Dijkstra

On 17 dec. 2014, at 22:27, Philipp Hausmann notifications@github.com wrote:

Hi Atze,

Running the first regression tests on the Agda UHC backend already did catch some first bugs.... which raised a question about UHC Core. When I compile Haskell programs, one Core case alternative is produced for each possible constructor. Eg the following HS produces following pseudo-core:

data A = B | C | D | E | F

f :: A -> Int
f C = 1
f _ = 2
produces

case temp of
Tag 0 -> 2
Tag 1 -> 2
Tag 2 -> 1
Tag 3 -> 2
Tag 4 -> 2
Now it seems that stuff starts to break when I instead use the default-branch instead of replicating the default value for all not-covered constructors. Eg.

case temp of
Tag 2 -> 1
default -> 2
This will yield the wrong result.

What is the best way forward? Should I just generate "total" case alternatives as well? Speaking just for myself, I think using the default feels more elegant, but I don't care too much about it. Otherwise I would just document the current behaviour in the Core API and not expose the default-alternative anymore.

Philipp

—
Reply to this email directly or view it on GitHub.