forbid extending sort K in the Java backend

Fixed https://github.com/kframework/k/issues/708

@dwightguth @radumereuta please review
This is bad!  They probably sneaked because we decided to claim victory in unified-builtins2 if we pass everything with the Maude backend.  I volunteer to change all those places as soon as needed.

Grigore


________________________________
From: Yilong Li [notifications@github.com]
Sent: Tuesday, July 15, 2014 1:33 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.";


There are many places in the tutorial that extend K. I will add a TODO comment here for now. Maybe we can get back to it later?

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/714/files#r14954087>.