Is there a way to add a new constructors to hooked sort Int?

Question

I'm trying to migrate a semantic made with the version: K tool, version 3.6 (yeah...). We have this rule:

syntax Int
       ::= #cint(Int,Int)

and when I compile the semantic with the K version: 5.1.16 and the LLVM backend, I get this error:

[Error] Compiler: Cannot add new constructors to hooked sort Int

Is there a way to support this rule with the version 5.1.16 ?

Answer 1

The backends don't support extending the hooked sorts.

But you can use macros to bypass it:

$ cat test.k
module TEST
    imports INT
    configuration <k> one +Int 2 </k>
    syntax Int ::= "one"
    rule one => 1 [macro]
endmodule
$ kompile test.k
$ krun
<k>
  3 ~> .
</k>

Macros are handled in the front-end, and as long as you process all your constructors that way, you can get away with extending the hooked sorts.