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.
Yes.  this means we simply ignore Kitems where either the label or the list
is a variable.



2014-06-10 18:06 GMT+03:00 dwightguth <notifications@github.com>:

> In
> src/javasources/KTool/src/org/kframework/backend/java/symbolic/UnboundedTermsCollector.java:
>
> > +            @Override
> > +            public void visit(Term node) {
> > +                if (! boundVariables.contains(node)) {
> > +                    unboundedTerms.add(node);
> > +                }
> > +                super.visit(node);
> > +            }
> > +        });
> > +     }
> > +
> > +    private void handleBinderVariables(KItem kItem, boolean add) {
> > +        // TODO(AndreiS): fix binder when dealing with KLabel variables and non-concrete KLists
> > +        if (!(kItem.kLabel() instanceof KLabel) || !(kItem.kList() instanceof KList)) {
> > +            return;
> > +        }
> > +        assert kItem.kLabel() instanceof KLabel : "KLabel variables are not supported";
>
> but look at the lines above. if either of these conditions is false, the
> function returns.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/kframework/k/pull/512/files#r13598635>.
>