Pull in updated version of SANY to support Unicode specs

[ahelwer]

Now that SANY supports parsing Unicode TLA+ specs, it should be fairly straightforward to support Unicode here by updating to a newer version of SANY. Possible bugs include if your translation code looks at actual string representation (for example, "\\E" instead of TLAplusParserConstants.EXISTS) which was the case in SANY itself.

[konnov]

Possible bugs include if your translation code looks at actual string representation (for example, "\\E" instead of TLAplusParserConstants.EXISTS) which was the case in SANY itself.

Oh, we have a bunch of those :)

apalache/tla-io/src/main/scala/at/forsyte/apalache/tla/imp/OpApplTranslator.scala

Lines 627 to 667 in 34bdc61

	val simpleOpcodeToTlaOper: Map[String, TlaOper] = Map(
	("=", TlaOper.eq),
	("/=", TlaOper.ne),
	("'", TlaActionOper.prime),
	("\\lnot", TlaBoolOper.not),
	("\\lor", TlaBoolOper.or),
	("\\land", TlaBoolOper.and),
	("\\equiv", TlaBoolOper.equiv),
	("=>", TlaBoolOper.implies),
	("SUBSET", TlaSetOper.powerset),
	("UNION", TlaSetOper.union),
	("DOMAIN", TlaFunOper.domain),
	("\\subseteq", TlaSetOper.subseteq),
	("\\in", TlaSetOper.in),
	("\\notin", TlaSetOper.notin),
	("\\", TlaSetOper.setminus),
	("\\intersect", TlaSetOper.cap),
	("\\union", TlaSetOper.cup),
	("$CartesianProd", TlaSetOper.times),
	("~>", TlaTempOper.leadsTo),
	("[]", TlaTempOper.box),
	("<>", TlaTempOper.diamond),
	("ENABLED", TlaActionOper.enabled),
	("UNCHANGED", TlaActionOper.unchanged),
	("\\cdot", TlaActionOper.composition),
	("-+->", TlaTempOper.guarantees),
	("$AngleAct", TlaActionOper.nostutter),
	("$SquareAct", TlaActionOper.stutter),
	("$Tuple", TlaFunOper.tuple),
	("$Pair", TlaFunOper.tuple),
	("$ConjList", TlaBoolOper.and),
	("$DisjList", TlaBoolOper.or),
	("$Seq", TlaFunOper.tuple),
	("$FcnApply", TlaFunOper.app),
	("$IfThenElse", TlaControlOper.ifThenElse),
	("$RcdSelect", TlaFunOper.app),
	("$SetEnumerate", TlaSetOper.enumSet),
	("$SetOfFcns", TlaSetOper.funSet),
	("$SF", TlaTempOper.strongFairness),
	("$WF", TlaTempOper.weakFairness),
	)

[konnov]

instead of TLAplusParserConstants.EXISTS

Do you know how stable this table of constants going to be? It's autogenerated. I assume that the names will not change most likely?

[konnov]

@ahelwer do I understand it right that the unicode operators have their own names such as op_infix_neq_uc? I wonder where to get the actual mapping from without guessing.

[ahelwer]

Do you know how stable this table of constants going to be? It's autogenerated. I assume that the names will not change most likely?

It has been stable for about 10 years as far as I know, no plans to change it in the future.

do I understand it right that the unicode operators have their own names such as op_infix_neq_uc

No, they do not. They are all wrapped up into the same TLAplusParserConstants token IDs.

[ahelwer]

If you want a quick shortcut you could also just add all the different text-based unicode variants, defined here: https://github.com/tlaplus/tlaplus-standard/blob/main/unicode/tla-unicode.csv

Although this might make it more work if any of these mappings are ever changed.