#9 Make case expressions compute better in CBV_CONV

[Michael Norrish]

The following illustrates the problem:

Hol_datatype `foo = D | E of num`;
Define`g x = case x of D -> FACT 100 || E y -> y`;

now typing

EVAL ``g (E 2)``;

causes an "infinite loop".

[Konrad Slind]

Logged In: YES
user_id=326915

This performance bug is known,. Its cause is the order of
arguments to "case" constants. Bruno was depressed about
this. In HOL we currently write, e.g.,

bool_case x y T = x
bool_case x y F = y

In order to evaluate these lazily, he'd want the definition
to be

bool_case T x y = x
bool_case F x y = y

because a simple transformation yields

bool_case T = \x y. x
bool_case F = \x y. y

which leads to evaluations where the test is evaluated and
then the correct subsequent expression is evaluated, instead
of the disastrous situation where all three are evaluated.

It is possible but tedious to go through and change the case
definitions from datatype declarations to have the "test"
expression come first. However, as you note, the performance
benefits are important.

Konrad.

[Michael Norrish]

Logged In: YES
user_id=13185

So, are you saying the right thing to do is to
switch case constants around so that the value being
switched on is the first argument?

I think I agree. I'm not volunteering to do it, and I'm
not sure it's critically important, but in the ideal world
the generated case constants should be fiddled with.
One reason it's not critical is that the problem only
arises for the RHSs of nullary constructors.

In, case e of C x -> ... x... || ...

this translates to

type_case (\x. ... x ...) ... e

and CBV_CONV won't do any work inside that lambda
abstraction until it gets its argument. If e isn't the
right sort of value, the work won't get done.