Use upstream's Sprite annotations (/*@...*/)

[janvrany]

This PR scratches the worst of my itches when writing Sprite by hand. Still, there's more to fix (#193 and things I already forget)

[shingarov]

If we are already here, focusing our attention on properly parsing the upstream /*@...*/ annotation syntax, why not go all the way and remove ⟦...⟧, (changing the tests of course), this way we are char-for-char identical to the upstream? I recommend focusing on one topic per PR. This particular change would be named something like "Use upstream Sprite annotation syntax (/@…/)", and cherrypick this commit, change the tests, and remove the ⟦...⟧.

[shingarov]

I don't get it. Are you suggesing to depart from the upstream syntax here?

In upstream, if an id starts with uppercase, you know it's either a data constructor (see how ctorP calls cbind in Parse.hs), or a switch-case (altP in Parse.hs).

[shingarov]

Wait, how is this any different? I am looking at #word and it is PPCharSetPredicate on isAlphaNumeric, which is just isLetter or: [isDigit], no?

[janvrany]

I recommend focusing on one topic per PR. This particular change would be named something like "Use upstream Sprite annotation syntax (/@…/)", and cherrypick this commit, change the tests, and remove the ⟦...⟧.

OK, no problem.

Are you suggesing to depart from the upstream syntax here?

Yes.

Wait, how is this any different? I am looking at #word...

Ah, my bad. IIRC this has not been so in the early versions of PP, will drop that change.

[janvrany]

Are you suggesing to depart from the upstream syntax here?

Forget it, I'll deal with that differently some time in the future.

[shingarov]

Ok, this is excellent.

Now the next question is how to merge such things. Because if we merge into pure-z3, it will break all the branches. I think this simply means we should prioritize merging that whole zoo-of-branches into pure-z3 asap.

[janvrany]

We can drop last commit (removing support for [[ ]]) and add it later, once the rest is merged, or the other way round, Up to you.