Using the string "Type" as a syntax form causes an error

[canndrew]

I've just done the first tutorial video and I tried to compile this:

module MALK
    syntax Expr ::= Id
                  | Expr Expr
                  | "(" Id ":" Expr ")" "->" Expr
                  | "(" Id ":" Expr ")" "=>" Expr
                  | "Type"
endmodule

The causes an error:

[Error] Critical: Parse error: Syntax error near unexpected character '('
	File: /tmp/tcloop/k/include/builtins/symbolic-k.k
	Location: (160,42,160,42)

However, if rename "Type" to something else...

module MALK
    syntax Expr ::= Id
                  | Expr Expr
                  | "(" Id ":" Expr ")" "->" Expr
                  | "(" Id ":" Expr ")" "=>" Expr
                  | "Zkmfsdfjk"
endmodule

this compiles fine.

[dwightguth]

What version of K are you using? That include file looks obsolete to me.

[canndrew]

Oh wow, I didn't notice you'd replied immediately. Thanks!

I'm using KVM 3.4 I believe. I just downloaded it off the website today.

[canndrew]

kompile --version gives me:

K-framework version 3.4.
Git Revision: 08c9271
Build date: Tue Aug 26 13:56:56 PDT 2014

[canndrew]

Similarly, I get compile errors if I define an operator called =>. Is there a way to stop the syntax of my language from conflicting with the syntax of the meta-language? (I'm only up to the third tutorial video but I'm trying to play around with the concepts as they're introduced and I'm running into this problem already.)

[radumereuta]

=> is a reserved keyword for K. It is used in rules to specify rewriting rules. K3.4 is quite old and had some issues regarding modularity but in K4 you can avoid these by splitting your syntax into different modules: 1. module for semantics, 2. module for program syntax 3. module for common syntax. The idea is to put all the productions that conflict with the builtin K stuff in the second module and keep the rest in the common module which you can include in both.