K-user mailing list

["Park, Daejun" <dpark69 AT illinois.edu>]

Thank you very much, Traian. It helped me. Thanks to your comment, I realized that the undesirable behavior was caused by another factor. A krun in debugging mode works differently because I set 'kompile --transition="computational"' option to use 'krun --debug'.
 Probably this undesirable behavior is observed because I traverse only one possible trace, not having all possible traces with 'step-all' command, since it takes too much time.

On Feb 6, 2014, at 1:12 PM, Traian Florin Şerbănuţă <traian.serbanuta AT fmi.unibuc.ro> wrote:

well, since macros are not completed with cells while (most) other rules are, and since Maude does innermost rewriting, it means your macros will only compete for application with functions and anywhere rules.  Therefore most of the time they will just work as intended.

There was a plan (at least for the Maude backend) to separate macros in a different module and use that to preprocess the input, but it never seemed to get implemented.  Nevertheless doing this should be pretty straight-forward.

best wishes,

Traian

2014-02-06 Park, Daejun <dpark69 AT illinois.edu>:

Hi all,

Is there any way (or simple trick) to force all macro-rules to be resolved before applying other normal-rules?

I got an undesirable behavior since a rule is applied without resolving its inner macro-rules. Previously, I tackled this problem by separating two phases--macro expansion and normal rule rewriting--that are written in totally different K definitions, but now I cannot rely on the approach, because I need to merge two phases in a single K definition in order to support 'eval' semantics.

Thanks in advance.

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