K-user mailing list

[Daniel Schnetzer Fava <danielsf AT ifi.uio.no>]

Hi,

I am not a K developer (I’m just a K user like you).

But I’ve looked into this a bit because I would like to do something similar; namely:  have a rewrite rule fire only when a subset of the other rewrite rules cannot fire.

I’ve been instructed to do is to look into “strategies” and the “strategy language”.  Here is what I’ve collected so far:

Quoting from a previous answer to the mailing list:

"strategies boil down to "wrapping" the rewrite engine with some context which allows you to do things like take snapshots of the current state, manipulate the state, or select which rules to apply to the state.”

"The file domains.k (at k-distribution/include/builtin/domains.k) has theBASIC-STRATEGY module, which you can import. You can look atgithub.com/kframework/kat for an example of using the strategy language to drive symbolic execution.”

The rewrite strategy for a particular program lives in a specially-designated top-level cell called <s>, which is added the the regular program configuration.

You may also find these useful:

Resources and leads

• Rewriting-Strategies wiki
• Program transformation example
• <blocked/>
• K Analysis Tool (KAT)
  • KAT
  • KAT-IMP
  • KAT-IMP-examples
• BASIC-STRATEGY module in domain.k
• K-REFLECTION module in domain.k

Daniel

On 30 Jan 2018, at 06:08, 璟临天下 <qjq793437528 AT 163.com> wrote:

there are multiple rules with the same configuration state which means they can be activated at the same time ,so i try to set the priority of rules. but how to do it . which the attribute it is or something else?

Thanks in advance.