Support TLA+ 2

[fhackett]

So far, PGo has been developed blissfully ignorant of TLA+ 2, and it had not caused problems.

When discussing how to implement the sum of a set of integers, however, it becomes apparent that we need at least a bit of TLA+ 2 in practice.

At minimum, this snippet of TLA+ declarations should work (taken from https://learntla.com/libraries/sets/):

Pick(S) == CHOOSE s \in S : TRUE
RECURSIVE SetReduce(_, _, _)
SetReduce(Op(_, _), S, value) == IF S = {} THEN value
                              ELSE LET s == Pick(S)
                              IN SetReduce(Op, S \ {s}, Op(s, value)) 

Note the RECURSIVE directive, which is what will not currently parse/scope.

I don't anticipate there being that much difficulty implementing this. The assumption that all operators are non-recursive is almost un-used in PGo as far as I recall, so the main obstacle would be getting parsing / scoping to cooperate with the new construct (especially in term rewrites!).

TLA+ 2 has a lot more features than just this, but perhaps those are less important. An initial PR would probably do well to have a limited scope.

Reference on TLA+ 2: http://lamport.azurewebsites.net/tla/tla2.html

[shayanh]

Having RECURSIVE only would be really helpful for our 538B project to easily implement sum.

Also wanted to note that our syntax highlighting currently doesn't support TLA+ 2 directives. We should update that too.