TLAPM parser incorrectly accepts recursive operator when it is a function literal

[ahelwer]

Found during work on #229; the root cause is that the parse tree does not distinguish between these two definitions:

f[x \in Nat] == 0
f == [x \in Nat |-> 0]

So the parser wrongly accepts this parse input; recursive functions should only be allowed when identifiers are introduced on the left side of ==:

---- MODULE Test ----
EXTENDS Naturals
factorial == [n \in Nat |-> IF n = 0 THEN 1 ELSE n * factorial[n - 1]]
====

SANY correctly rejects this input.

This has to do with how the parse tree represents operators with parameters; these two are equivalent (despite the second not being valid syntax, strictly speaking, but you get the idea):

op(x, y, z) == 0
op == LAMBDA x, y, z : 0

So when expanding an Expr.T.defn variant and matching it to an Operator (name : Util.hint, expr : Expr.T.expr) instance, operators with parameters are represented by expr matching to a Lambda variant. Function definitions of the form f[x \in Nat] == 0 are also represented as an Operator variant, where expr is a Fcn (function literal) variant. This means it parses the same as f == [x \in Nat |-> 0].

Since the parser can't distinguish these, it can't tell that recursive references are okay in the first case but not the second, so it just allows them in both. Small variations on the bad input will cause the parse to fail, for example TLAPM correctly rejects this input with an Operator "factorial" not found error:

---- MODULE Test ----
EXTENDS Naturals
factorial == [n \in Nat |-> IF n = 0 THEN 1 ELSE n * factorial[n - 1]] + 1
====

The reason for this is that the function definition is hidden below the "+" operator in the AST.