K-user mailing list

[Emmanuel Castro <emmanuel.castro AT laposte.net>]

While experimenting the module 'k-visitor.k', I noticed oddities with --transition.

Consider the following K file (named visitest.k) :

require "modules/k-visitor.k"

module VISITEST

  imports K-VISITOR

  syntax KList ::= klist(K) // Encapsulate K to KList  

  rule klist(K:K) => K,,.KList

  

  syntax Expr ::= Expr "+" Expr [left]          

                | Id

  

  syntax K ::= trans(Expr) [klabel('trans)] // A Pseudo transformation 

  syntax Boolean ::= test(Expr) [klabel('test), predicate] // A pseudo test which is always true

  

  rule test(_) => true  [foo]

endmodule

  

A sample file (named visi)

visit klist(a+b) applying 'trans if 'test

Now, a standard execution of visi stops on trans (which is what is supposed to happen)

> kompile visitest.k && krun --graph --search-all visi

Search results:

Solution 1, State 0:

<k>

    trans ( (a + b) )

</k>

...

However, if I add the transition "foo", the result changes. Is this a bug?

> kompile --transition "foo" visitest.k && krun --graph --search-all visi

Search results:

Solution 1, State 0:

<k>

    visitedK ( (a + b) )

</k>

...

P.S. Technically, what is the difference between the attributes [function] and [predicate]?

Emmanuel