K-user mailing list

[Andrei Arusoaie <andrei.arusoaie AT gmail.com>]

Michael,

I can tell you my part of the story. The [function] attribute can be attached to syntax declarations. All the rules corresponding to that function are annotated automatically as [anywhere] which is only a rule attribute. However, if we want to say that a rule applies anywhere without being related to a function declaration, we simply annotate it with [anywhere] and the contextual transformation will not affect that rule. Therefore the functionality of [function] is implemented using [anywhere], and [anywhere] is an attribute which does not fill the context for that rule.

Andrei A.

2013/12/28 Michael D. Adams <adamsmd AT illinois.edu>

Does desugaring also apply to rules?  (I suspect that this could be a major difference between 'macro' and the others.)

I don't understand what you are saying about 'function' and 'anywhere'.  Is there any (current or planed for the future) difference in their behavior?

(Saying that 'function' is for functions and 'anywhere' applies anywhere doesn't help since we may have different understandings of what being a function and applying anywhere mean.)  An example showing how they behave differently might be enlightening.

Michael

On 12/25/2013 02:24 PM, Traian Florin Șerbănuță wrote:

They all generate the same code now.  However, they are semantically
different:

macro should only be used for desugaring, and should be applied to
programs before any evaluation is started.

function should only be used for annotating function declarations

anywhere should be used for rules which we want to apply anywhere,
disabling configuration concretization for them.

best wishes,
Traian

anywhere is

2013/12/25 Park, Daejun <dpark69 AT illinois.edu <mailto:dpark69 AT illinois.edu>>

    Hi,

    I have a simple question:
    What is the difference between 'macro', 'anywhere', and 'function'?
    The generated maude code seems to be same except metadata. Who
    makes, if any, a difference?

    Thanks,
    Daejun
    _______________________________________________
    k-user mailing list

    k-user AT cs.uiuc.edu <mailto: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

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