So, the two parts of the change I proposed are dependent on each other. You
have to change both ResolveSyntaxPredicates and FlattenTerms. Since the
idea is for KAST to have the semantic sorts of variables, it is not correct
for FlattenTerms to set all the variable sorts to KItem. That is why I
proposed you change that class, and why I do not like the current solution.
But then, in order to make everything work, it's necessary that the sort be
changed later, hence the change to ResolveSyntaxPredicates.

You are explaining a lot of different changes here, and I am having trouble
following which problems you encountered under which version of the change.
Can you please explain specifically just the problem you encountered under
the solution I just named, and nothing else?


On Tue, May 20, 2014 at 10:08 AM, Liyi Li <notifications@github.com> wrote:

> In
> src/javasources/KTool/src/org/kframework/compile/transformers/ResolveSyntaxPredicates.java:
>
> > @@ -38,7 +44,8 @@ public ASTNode visit(Sentence node, Void _)  {
> >          for (Variable var : vars) {
> >  //            if (!var.isUserTyped()) continue;
> >              if (var.isSyntactic()) continue;
> > -            if (MetaK.isKSort(var.getSort())) continue;
> > +            if ((var.getExpectedSort()==null && MetaK.isKSort(var.getSort()))
>
> I mean I test the fixing in resolveSyntaxPredicate or variable class
> individually. Then I test to move flattenTerms before
> resolveSyntaxPredicate. For the above two solutions, The first cannot pass
> every test cases if I did not move flattenTerms before
> resolveSyntaxPredicate. The second one cannot pass all test cases even if I
> did not move flattenTerms before resolveSyntaxPredicate.
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/466/files#r12848772>
> .
>