List test

Yes, I run all tests, no unexpected things.
This file list-syntax.k is completely written by me, so not there before.
Denis do have another same name (toKListWrap) function elsewhere, but such
function override is fine, and I actually think I can merge his into mine,
his change Exps to KListWrap.
I will clean up the code now.

On 1 January 2015 at 16:19, Grigore Rosu <notifications@github.com> wrote:

> In src/common/list-syntax.k
> <https://github.com/kframework/java-semantics/pull/19#discussion-diff-22402688>
> :
>
> > +
> > +module LIST-MACRO
> > +imports CORE-FUNCTIONS
> > +
> > +syntax KItem ::= toKListWrap(K) [function]
> > +                | toKListWrap(K, KListWrap) [function]
> > +
> > +rule toKListWrap(UL) => toKListWrap(UL,[.KList])
> > +
> > +rule toKListWrap(Label:KLabel(Hd,,Tl), [L:KList]) => toKListWrap(Tl, [L,,Hd])
> > +
> > +rule toKListWrap('.List`{""`}(.KList), KL:KListWrap) => KL
> > +rule toKListWrap('.List`{"`,"`}(.KList), KL:KListWrap) => KL
> > +rule toKListWrap('.List`{"."`}(.KList), KL:KListWrap) => KL
> > +rule toKListWrap('.List`{"&"`}(.KList), KL:KListWrap) => KL
> > +
>
> I guess you tested the resulting definition by running all the java
> programs in our testsuite, right? I just want to make sure that the rules
> above do not interfere in unexpected ways with the semantics. Were they
> there before, too, in Denis' original definition?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/kframework/java-semantics/pull/19/files#r22402688>.
>