case statement semantic in kernel language

[Peter Van Roy]

Dear Marko,

If the pattern is 'rec(a:2)' then the case statement is written
as follows in kernel language:

case X of rec(a:Y) then
    case Y of 2 then <success branch>
    else <failure branch> end
else <failure branch> end

If X=rec(a:1) then the failure will occur in the innermost case.
The point is that 'rec(a:2)' is already a nested structure.  Any
case statement occurring in a real program is rewritten as a
series of nested case statements with only simple patterns like
lbl(feat1:X1 ... featn:Xn) where X1, ..., Xn are identifiers.
The semantics only needs to handle this simple case.

Note also that a case statement does no unification.  I.e., a
case statement never by itself adds a binding to the store.  This
is a simple consequence of the semantics as you have written
it in your message.

Peter




Marko Zerdin wrote:

> Dear Peter,
>
> thank you for your prompt and comprehensive answer. Unfortunately, I 
> must've been unsuccessful when trying to get my point across, so I'm 
> going to have to try again.
>
> On page 67, it says the following when explaining the semantics of the 
> case statement (I'm quoting just the relevant part)::
> <snip>
> If the activation condition is true (E(<x>) is determined), then do 
> the following actions:
> * If the label of E(<x>) is <lit> and its arity is [<feat1> ... 
> <featn>], then push (<s1>, 
> E+{<x1>->E(<x>).<feat1>,...,<xn>->E(<x>).<featn>}) on the stack.
> * Otherwise, push (<s2>, E) on the stack.
> </snip>
> Based on this semantic, the match is determined solely based on the 
> record label and arity - as soon as those match, the alternative is 
> chosen. However, assume for a second that we are matching rec(a:1) 
> against rec(a:2). According to the described semantic, we have the 
> following chain of events:
> - Activation condition is obviously true, so the matching can proceed.
> - Both the label and arity match. Therefore, the match was found and 
> the new entry is added on the stack.
> The unfortunate fact in this case however is that we don't actually 
> have a match. When the new environment is created, unification failure 
> should occur because the binding 1->2 obviously won't be welcome in 
> the store. I don't think this case is actually addressed in the 
> semantic above. How is this resolved? What happens next?
>
> I don't want to presume that I thought of everything, so please let me 
> know if there is some simple fact that I'm missing in my reasoning.
>
> Kind regards,
>
> Marko.