K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

I'm not following this. Are you suggesting a way I could change the
semantics to do something different? That seems fine (altho I think
life is better when values are values, without the pain of extra
constructors), but I would like to understand why the existing program
doesn't do what I expect.

Robby

On Tue, Oct 2, 2012 at 10:24 PM, Patrick Meredith 
<pmeredit AT gmail.com>
 wrote:
> Also because your short circuit rule can apply to syntax since you make no
> distinction between syntax and kresults.  If you had some wrappers for bool
> and int sunk into kresult you could force your shortcircuit rule to only
> short circuit when both arguments have been evaluated (which you actually
> wouldn't want since it voids the purpose of short circuit!)
>
> -P
>
>
> On Oct 2, 2012 10:16 PM, "Patrick Meredith" 
> <pmeredit AT gmail.com>
>  wrote:
>>
>> Hi Robby,
>>
>> Replace seqstrict with strict.  Seqstrict is deterministic sequentially
>> (left to right)
>>
>> -Patrick
>>
>> On Oct 2, 2012 7:12 PM, "Robby Findler" 
>> <robby AT eecs.northwestern.edu>
>> wrote:
>>>
>>> Hi all: I'm having trouble understanding a K program's behavior and I
>>> wondered if I could get some help.
>>>
>>> Here's the program:
>>>
>>> module IMP
>>>   syntax AExp ::= Int
>>>                 | "(" AExp ")"    [bracket]
>>>                 | AExp "/" AExp   [seqstrict, left]
>>>   syntax BExp ::= Bool
>>>                 | "(" BExp ")"    [bracket]
>>>                 | AExp "<=" AExp  [seqstrict]
>>>                 > BExp "and" BExp [seqstrict]
>>>
>>>   syntax KResult ::= Bool | Int
>>>
>>>   rule <k> I1:Int / 0 ...</k> => <k> "div0" </k>
>>>   rule I1:Int <= I2:Int => I1 <=Int I2
>>>   rule true and B:BExp => B
>>>   rule false and _ => false
>>> endmodule
>>>
>>>
>>> and here's the IMP program I run:
>>>
>>>    false and (1/0 <= 3)
>>>
>>> I would have expected it to produce two out comes ("div0" and false)
>>> because of the seqstrict annotation on the "and" production in the 
>>> grammar.
>>> Specifically, I thought I'd get a heating/cooling rule that would apply to
>>> the program above that would move the (1/0 <= 3) expression to the front 
>>> of
>>> the K cell, and the the 1/0 would move to the front and then I'd get the
>>> div0 result. But instead I get this:
>>>
>>> $ ../k/bin/krun --do-search --maude-cmd search x.impSearch results:
>>>
>>> Solution 1, state 0:
>>>
>>> <k>
>>>  false
>>> </k>
>>>
>>> I do see that if I remove the short-circuiting 'and' rule that I get the
>>> div0, but I cannot seem to get them both at once.
>>>
>>> tia,
>>> Robby
>>>
>>> _______________________________________________
>>> k-user mailing list
>>> k-user AT cs.uiuc.edu
>>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>>