Skip to content

[Bug] kompile should allow macro productions on hooked sort #2488

@SchmErik

Description

@SchmErik

Description

The current implementation of macros on productions does not allow macro productions on hooked sorts.
Code like this:

syntax Int ::= "LABEL" [macro]
rule LABEL => 4 // or some other number

would result in errors like this:

$ kompile test.k
[Error] Compiler: Cannot add new constructors to hooked sort Int

However, "LABEL" in this case is not a constructor but a term that would be translated to 4 during compilation so this error is not applicable to productions that are macros. kompile needs to be fixed to allow cases like this.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions