K-user mailing list

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

Ah I see, I was thinking that was the case, sort of like an "atomic" re-write. Thanks to you both.

---

From: Rosu, Grigore [grosu AT illinois.edu]
Sent: Wednesday, July 03, 2013 1:03 PM
To: Radu Mereuta; Charles Jacobsen
Cc: k-user AT cs.uiuc.edu
Subject: RE: [K-user] What does the [function] attribute accomplish?

Also, functions can be very fast in backends, because they are free to use their native means to implement them.  Their evaluation does not count as transition steps in the transition system associtated to a program.  Think of functions as "instantenous computations", which apply anywhere they match and don't even take one step.

 

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Radu Mereuta [headness13 AT gmail.com]
Sent: Wednesday, July 03, 2013 1:26 PM
To: Charles Jacobsen
Cc: k-user AT cs.uiuc.edu
Subject: Re: [K-user] What does the [function] attribute accomplish?

Hi Charles,

Usually when you write a rule, for example addition (rule I1:Int + I2:Int => I1 +Int I2), the kompiler adds automatically the <k> cells over it in order to limit the rule application only at the top of the k cell.

If you add the [function] attribute to a production, and you use it as a top production in a rule, then it's not going to add the <k> cell. This will allow you for example to use it in the "when" part of a rule as a predicate.

I think there are a few other restrictions, but if I'm wrong, someone please correct me :)

Radu,

K-developer

On Wed, Jul 3, 2013 at 8:33 PM, Charles Jacobsen <charlie.jacobsen AT utah.edu> wrote:

I've used this for simple "helper functions", but I'm not sure what it does. For example,

syntax Int ::= "countSet" Set [function]
rule countSet .Set => 0
rule countSet SetItem(K:K) S:Set => 1 +Int (countSet S)

This works as expected, but what does the [function] attribute indicate? I couldn't find any info in the overview/primer or by grepping the include dir or source.

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user