Bug pattern matching elements of a set?

[LaifsV1]

There appears to be a bug when pattern matching elements of a set.

For a minimal example, here's the K-file:

module TEST
  imports DOMAINS
  imports SET
  syntax Lib   ::= "call" Id | "import" Id Id Lib
  syntax Meth  ::= Id ":" Id
  configuration <T>
                  <k> $PGM:Lib </k>
		  <methods> .Set </methods>
	        </T>
		
  rule <k> import M T L => L ... </k>
       <methods> ... .Set => SetItem(M : T) ... </methods> [structural]
  rule <k> call M => T </k>
       <methods> ... SetItem(M : T) ... </methods>
endmodule

with the program:

import m1 A
import m2 B
import m3 C
import m4 D
call m2

Calling krun, I think it is sensible to expect B to be returned. However, this program gets stuck at call m2. In fact, call m1 and call m3 also get stuck. Only call m4 succeeds by returning D.

i.e.
call m4 results in:

Result ==K <T>
  <k>
    D
  </k>
  <methods>
    SetItem ( m1 : A )
    SetItem ( m2 : B )
    SetItem ( m3 : C )
    SetItem ( m4 : D )
  </methods>
</T>

while call m3 results in:

Result ==K <T>
  <k>
    call m3
  </k>
  <methods>
    SetItem ( m1 : A )
    SetItem ( m2 : B )
    SetItem ( m3 : C )
    SetItem ( m4 : D )
  </methods>
</T>

Is this behaviour intentional? If so, is there any way to do this without having to rely on a Map?

[dwightguth]

It sounds like a bug, but no, you will want to use a map for something like this.

[LaifsV1]

Ah. so Set won't always work to pattern match terms. I would need to use maps and identify the terms with something like KVar. Thanks for the reply!