K-user mailing list

[Charles Jacobsen <charlie.jacobsen AT utah.edu>]

Thanks to you both!

---

From: Rosu, Grigore [grosu AT illinois.edu]
Sent: Wednesday, July 10, 2013 2:17 PM
To: Charles Jacobsen; k-user AT cs.uiuc.edu
Subject: RE: Using [function] attribute does not add syntax to sort?

Just a simple stylistic comment, FYI.

 

Many people find it more elegant to write the totally equivalent

 

rule false && _ => false

instead of:

 

rule false && K:K => false

Also, if the sort of a variable is K, then you don't need to mention it, so the above is also equivalent to

 

rule false && K => false

Finally, keep in mind that any variable sorting except to K may yield a runtime sort membership checking.  If you don't really care whether the second argument of && is always a bool, or you know it for sure that it will always be, then you can drop the sorting ":K" of B in the second rule.

 

Cheers,

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Charles Jacobsen [charlie.jacobsen AT utah.edu]
Sent: Wednesday, July 10, 2013 3:00 PM
To: k-user AT cs.uiuc.edu
Subject: Re: [K-user] Using [function] attribute does not add syntax to sort?

(

Oops, forgot the Bool, sorry for the flood of emails:

syntax Bool ::= K "&&" K [function]
rule false && K:K => false
rule true && B:Bool => B

)

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Charles Jacobsen [charlie.jacobsen AT utah.edu]
Sent: Wednesday, July 10, 2013 1:59 PM
To: k-user AT cs.uiuc.edu
Subject: Re: [K-user] Using [function] attribute does not add syntax to sort?

Nevermind, unless you guys have a better way. I wrote a new conjunction construct:

syntax ::= K "&&" K [function]
rule false && K:K => false
rule true && B:Bool => B

This seems to work as expected, making && short-circuiting.

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Charles Jacobsen [charlie.jacobsen AT utah.edu]
Sent: Wednesday, July 10, 2013 12:35 PM
To: k-user AT cs.uiuc.edu
Subject: Re: [K-user] Using [function] attribute does not add syntax to sort?

(

I forgot to remove the comments from the second TEST module, should be:

module TEST

  syntax Val  ::= Int | Bool

  // -Not- using the [function] attribute on foo.
  syntax Bool ::= "foo" "(" Val ")" [function]
  rule foo(B:Bool) => B

  syntax Bool ::= "is-bool" "(" Val ")" [function]
  rule is-bool(B:Bool) => true
  rule is-bool(I:Int) => false

  // This expr -will- reduce to true.
  configuration <k> is-bool( foo(5) ) </k>

endmodule

)

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Charles Jacobsen [charlie.jacobsen AT utah.edu]
Sent: Wednesday, July 10, 2013 12:31 PM
To: k-user AT cs.uiuc.edu
Subject: [K-user] Using [function] attribute does not add syntax to sort?

When I kompile and krun the following, the k cell does not reduce to true, as I was expecting. Notice that I did not include a rule for foo when the input is an integer, so foo(5) cannot reduce.

module TEST

  syntax Val  ::= Int | Bool

  // Using the [function] attribute on foo.
  syntax Bool ::= "foo" "(" Val ")" [function]
  rule foo(B:Bool) => B

  syntax Bool ::= "is-bool" "(" Val ")" [function]
  rule is-bool(B:Bool) => true
  rule is-bool(I:Int) => false

  // This expr will not reduce to true.
  configuration <k> is-bool( foo(5) ) </k>

endmodule

The k-cell in the following -does- reduce when the [function] attribute is removed from foo:

module TEST

  syntax Val  ::= Int | Bool

  // Using the [function] attribute on foo.
  syntax Bool ::= "foo" "(" Val ")"
  rule foo(B:Bool) => B

  syntax Bool ::= "is-bool" "(" Val ")" [function]
  rule is-bool(B:Bool) => true
  rule is-bool(I:Int) => false

  // This expr will not reduce to true.
  configuration <k> is-bool( foo(5) ) </k>

endmodule

I'm trying to use andBool inside 'when' conditions without needing to worry about whether all terms reduce (if one reduces to false, that should be sufficient).

Thanks guys, Charlie