K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

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