K-user mailing list

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

I'm sorry for this reply. I should have read ahead in my inbox!

Thanks Traian and Grigore! And just to be clear, I don't mean to
slight your design decisions or K or anything like that! I merely want
to understand what a K program does. (Altho, as you can see, my past
experience brings certain expectations to the table in ways that can
be unhelpful!)

Robby

On Wed, Oct 3, 2012 at 6:22 AM, Robby Findler
<robby AT eecs.northwestern.edu>
 wrote:
> What would this mean from the standpoint of the rules that seqstrict
> generates? (I understand the seqstrict annotation as a shorthand for
> generating rules, but I'm not sure that's right.)
>
> I thought it would generate a rule something like
>
>   A:KResult and B:BExp ~> everythingelse => A ~> (hole and B) ~> 
> everythingelse
>
> (apologies for my bad notation here "(hole and B)" is really something
> with a freezer around it and some substitutions and I'm not sure how
> to write "everythingelse" properly)
>
> Such a rule should fire!
>
> And indeed, if I just remove the 'and' shortcircuiting rule, then I do
> see the heating rule fire.
>
> Robby
>
> On Tue, Oct 2, 2012 at 10:36 PM, Patrick Meredith 
> <pmeredit AT gmail.com>
>  wrote:
>> Actually, that is a good point, and I'm not sure.  This is the behavior you
>> would normally want, but I'm not sure why it is working.  My best guess is
>> that seqstrict always plugs the heated value back in (cool) before it heats
>> the second value, deterministically, and that is where it is reducing your
>> short circuit (which doesn't care about the sort of the second argument).
>> This is what we'd want, so my guess is that is how it works.  I haven't 
>> used
>> seqstrict in any of my definitions.  Someone more knowledgeable can 
>> probably
>> confirm if I am correct.
>>
>> -Patrick
>>
>> On Oct 2, 2012 10:27 PM, "Robby Findler" 
>> <robby AT eecs.northwestern.edu>
>> wrote:
>>>
>>> But why should that preclude the heating/cooling from applying?
>>>
>>> Robby
>>>
>>> On Tue, Oct 2, 2012 at 10:26 PM, Patrick Meredith 
>>> <pmeredit AT gmail.com>
>>> wrote:
>>> > One definite issue is bool is in your syntax, so false and _ can be
>>> > applied
>>> > before any heating or cooling ever occurs.
>>> >
>>> > -Patrick
>>> >
>>> > On Oct 2, 2012 10:20 PM, "Robby Findler" 
>>> > <robby AT eecs.northwestern.edu>
>>> > wrote:
>>> >>
>>> >> Yes, but the left is already a KResult so the heating (or is it
>>> >> cooling?) rule should still fire. No?
>>> >>
>>> >> Robby
>>> >>
>>> >> On Tue, Oct 2, 2012 at 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
>>> >> >>
>>> >> >
>>> >> _______________________________________________
>>> >> k-user mailing list
>>> >> k-user AT cs.uiuc.edu
>>> >> http://lists.cs.uiuc.edu/mailman/listinfo/k-user