K-user mailing list

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

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