forbid extending sort K in the Java backend

Fixed https://github.com/kframework/k/issues/708

@dwightguth @radumereuta please review
Oh, I could not even imagine that we do different things in the Java and Maude backends.  We should definitely have the same K language in ALL backends.  There should be *nothing* special done in a particular backend.  The only differences between backends should be in the set of builtins that they implement/provide, and remember that also means the pm (pattern-match) function, which tells which patterns can be matched by the backend.  Thus, the only backend-specific error messages should be of the forms:

1) Backend XYZ does not support builtin operation FGH.
2) Backend XYZ does not support matching pattern PQR.

If we do anything else specific to a backend, then something is very wrong there and will be eventually changed.

Grigore


________________________________
From: Radu Mereuta [notifications@github.com]
Sent: Tuesday, July 15, 2014 12:30 PM
To: kframework/k
Subject: Re: [k] forbid extending sort K in the Java backend (#714)


In src/javasources/KTool/src/org/kframework/compile/checks/CheckSyntaxDecl.java:

>                  GlobalSettings.kem.register(new KException(KException.ExceptionType.ERROR, KException.KExceptionGroup.COMPILER, msg, getName(), node.getFilename(), node.getLocation()));
>              }
>          }
> +
> +        if (context.kompileOptions.backend.java()
> +                && !node.getFilename().startsWith(KPaths.getKBase(false) + File.separator + "include")
> +                && node.getSort().equals(KSorts.K)) {
> +            String msg = "Sort K is not user-extendable in the Java backend:\n\t" + node + "\n\tConsider extending KItem instead.";


Maybe we should do the same thing in both java and maude backends.
I always assumed that K is the base sort for all syntax, but since the java backend was introduced, it seems KItem is the preferred sort.
Maybe we should look over all the definitions, and I could go through the SDF stuff and fix all these inconsistencies.

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/714/files#r14949946>.