K-user mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

I have a K program with a rule like this:

    rule concatToConcat1(.Concat) => .
    rule concatToConcat1(C Cs) => C ~> concatToConcat1(Cs)

This works fine and it can only be applied to <k> configuration,
because in my program it's guaranteed that `concatToConcat1` can only
be placed in <k> (actually it's not guaranteed statically in the sense
that type safety is guaranteed statically by type systems, and I'm not
sure if such a thing is even possible, it's just guaranteed by other
rules, which never place this syntax in a place other than <k>).

But for some reason if I wrap this rule with <k> ... </k>, it no more works:

    rule <k> concatToConcat1(.Concat) => . </k>
    rule <k> concatToConcat1(C Cs) => C ~> concatToConcat1(Cs) </k>

Why is that?

(I'm not pasting my program because it's kinda big, but if required I
can paste K program and some simple input for demonstration)

Thanks,

---
Ömer Sinan Ağacan
http://osa1.net