Substitution as an argument of a function

[omarzd]

Before K4.0, using the substitution module, I could do something like this:

rule prep(A, Body, B) => prep(Body[A / B])

Now the substitution inside prep upsets the parser. So how should I do that?

[radumereuta]

Do you have more details about the error message? A simple test and version of K could suffice in this case.

[omarzd]

I tried to make a minimal example. I modified lesson2/lambda.k. This example doesn't make much sense, but it produces the same error I'm getting.

require "substitution.k"
module TEST
  imports SUBSTITUTION

  syntax Exp ::= Id
               | Exp "{" Id Id "}"              [left]
               | "(" Exp ")"          [bracket]
  syntax KVariable ::= Id
  
  syntax Exp ::= prep(Exp) [function]

  rule E:Exp {I1:Id I2:Id} => prep(E[I1 / I2])
endmodule

[omarzd]

@radumereuta Oh and I'm using the latest master!

[radumereuta]

The relation between K and the user defined sorts in the definition has changed. So now at the top there is K, and at the bottom there is KBot. Changing the prep production to something like:

syntax Exp ::= prep(K) [function]

avoids your error.