Java builtin (user-level) substitution

This push request contains an implementation of an user-level substitution mechanism for the Java backend.

Note however that it cannot be used directly instead of the one used in substitution.k because the java engine cannot process that file (and those depending on it).  

I have something written to address that in a separate branch (see  aeff8a8afa9ebf3dc4316d972b3a55a9308f9101 );  however, I would like to push this first as the substitution works and I have a provided a regression test for it.
I think here there was a case when people were redeclaring lambda to say
it's a result.  Maybe this is what Andrei tried to address here?


2014-06-09 17:02 GMT+03:00 dwightguth <notifications@github.com>:

> In
> src/javasources/KTool/src/org/kframework/backend/java/kil/KLabelConstant.java:
>
> >      public boolean isBinder() {
> > +        return hasAttribute("binder");
> > +    }
> > +
> > +    private boolean hasAttribute(String attribute) {
>
> this feels a bit strange to me. I'd feel better if a check were put in
> place to ensure that all productions with the same klabel had the same
> binder attribute. But then, it's Andrei's code, not mine. And I don't feel
> that strongly. So it's up to him.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/kframework/k/pull/512/files#r13541590>.
>