K-user mailing list

[Patrick Meredith <pmeredit AT gmail.com>]

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