forbid extending sort K in the Java backend

Fixed https://github.com/kframework/k/issues/708

@dwightguth @radumereuta please review
OK with me, at least until we run into limitations.

Grigore


________________________________
From: Traian Florin Șerbănuță [notifications@github.com]
Sent: Thursday, July 17, 2014 1:56 PM
To: kframework/k
Cc: Rosu, Grigore
Subject: Re: [k] forbid extending sort K in the Java backend (#714)


In include/builtins/symbolic-calculus.k:

> @@ -28,7 +28,7 @@ module SYMBOLIC-CALCULUS
>    This should be defined in a more generic way using ASTs.
>  */
>
> -  syntax K ::= K "[" K "/" K "]"
> +  syntax KItem ::= K "[" K "/" K "]"


So if we make it KItem it needs to be

syntax KItem ::= KItem "[" KItem "/" KItem "]"


because we don't want .K in the first position (.K [ 3 / X ] should evaluate to .K) or in the second position (X[.K/X] should evaluate to .K), and we don't ever want .K in the third position.

I would personally be in favor of that, and disallow applying substitution on .K

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/714/files#r15076817>.