K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

What is the definition of the anywhere label?

Is

rule A => B [anywhere]

equivalent to:

rule ... A => B ...

?


By the way, is there a list of all the possible labels one can use - and 
if possible of their definitions?

So far I've come across:

bracket

[seq]strict

[seq]strict(List of Ints)

function (how does this differ from "macro"?)

functional (?)

anywhere

klabel(Id)


Looking at k/kernel/src/main/java/org/kframework/kil/Attribute.java I 
can see:

builtin

function

assoc

comm

idem

unit

// sort

predicate

stream

anywhere

pattern

pattern-folding

hook

macro

lemma

trusted

simplification

freshGenerator

cellCollection

bitwidth

exponent

significand

smtlib

smt-lemma

smt-sort-flatten

cell

cellFragment

cellOptAbsent

equality

arity

impure

strict

seqstrict

bracket

transition

notInRules

variable

hybrid


But no "klabel", so no idea if this list is complete. :-(

Any pointers would be greatly appreciated!

Best,

Christos

On 22/07/2017 08:02, Mike Stay wrote:
> It looks like I need an [anywhere] annotation on the SKI rules.  I
> also found that <k> tags can have multiplicity *, so here's a working
> version of what I intended.
>
> module SKIC-SYNTAX
>    syntax Par ::= "|"
>    syntax SComb ::= "s"
>    syntax KComb ::= "k"
>    syntax IComb ::= "i"
>    syntax Comb ::= Par | SComb | KComb | IComb
>    syntax Apply ::= "(" Term Term ")"
>    syntax Term ::= Id | Comb | Apply
> endmodule
>
> module SKIC
>    imports SKIC-SYNTAX
>
>    configuration
>      <T>
>        <k multiplicity="*"> $PGM:Term </k>
>      </T>
>
>    rule (i X:Term) => X [anywhere]
>    rule ((k X:Term) Y:Term) => X [anywhere]
>    rule (((s X:Term) Y:Term) Z:Term) => ((X Z) (Y Z)) [anywhere]
>
>    rule <k> ((| T:Term) U:Term) </k> => <k> T </k> <k> U </k>
>
> endmodule