case statement semantic in kernel language

[Marko Zerdin]

Dear Peter,

Now I finally understand, and I also understand what you were telling me 
in your first response.

Thank you,

Marko.

Peter Van Roy wrote:

> 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.
>
>
>
>