and update the code throughout `tlapm`,
because this commit changes the existing types in the
module `Expr.T`.

Signed-off-by: Ioannis Filippidis <[email protected]>

The change in this commit corrects a bug with function
definitions. Parsing of function definitions allowed using unbounded
declarations (and also mixing bounded and unbounded declarations).
For example, before this change, parsing allowed:

```tla
f[x \in S, y] == TRUE
```

and even:

```tla
f[x] == TRUE
```

These syntax errors are detected by SANY.
In any case, this change ensures that `tlapm` does not parse
such definitions.

The error was due to calling the function `bounds` within the
function `ophead`, instead of calling the function `boundeds`
(which was called before commit
5958dfa
in order to handle function constructors within the function
`atomic_expr`).

This commit also adds tests for this bug.

Signed-off-by: Ioannis Filippidis <[email protected]>

because TLA+ does not allow this kind of syntax.
A single rigid quantifier can include either:
- only unbounded declarations,
  for example `\E x, y, z:  ...`, or
- only bounded declarations,
  for example `\A x \in A, y \in B, z \in C:  ...`.

A single rigid quantifier cannot include both bounded and
unbounded declarations.

This syntax is caught by SANY.

Signed-off-by: Ioannis Filippidis <[email protected]>

in other words, that the following expression is not allowed:

```tla
[x \in S, y |-> TRUE]
```

and the following expression is allowed:

```tla
[x \in S, y \in S |-> TRUE]
```

Also, add a reminder in a comment in the parser code.

Signed-off-by: Ioannis Filippidis <[email protected]>

instead of appending during the fold.
This approach is more efficient.

Also:

- STY: blankspace formatting

Signed-off-by: Ioannis Filippidis <[email protected]>

Signed-off-by: Ioannis Filippidis <[email protected]>

## ENH: tuply declarations

This commit adds parsing and translation support for
tuply declarations that appear in:
- rigid quantification `\E ... here ...: ` and `\A ... here ...: `
- choose expressions `CHOOSE ... here ...: `
- set constructors
  `{... here ... \in ...:  ...}`
- set constructors `{...:  ... here ...}`
- function definitions `f[...here...] = ...`
- function constructors `[... here ... |-> ...]`

Commit 5958dfa introduced
parsing of tuple declarations in function constructors,
for example for expressions of the form:

```tla
[<<x, y>> \in A \X B |-> x + y]
```

This commit rewrites that functionality, and uses the
new functionality to parse tuple declarations that can
appear in function definitions, i.e., definitions of the form:

```tla
f[<<x, y>> \in A \X B] == x + y
```

The parsed tuply declarations are then transformed to either:

- optimized expressions that are simplified and do not
  contain additional `CHOOSE` operators, in the presence of
  a syntactically-recognizable Cartesian product of
  suitable length, or

- the expressions defined by TLA+ semantics (in most cases
  these expressions contain `CHOOSE`), otherwise.


This commit also adds tests for the above functionality.


## BUG: correctly represent tuple declarations in function constructors

In general, tuple declarations in function constructors
are defined using `CHOOSE` with tuple declarations,
which in turn is defined using unbounded `CHOOSE` and
quantification.

This was not how function constructors were implemented
in commit 5958dfa.
This commit corrects this error. The previous encoding
is closer to what is currently done when a Cartesian
product of the appropriate length is recognized in syntax.


## Tuplification

This commit adds a translation of function constructor
signatures that tuplifies comma-separated declarations,
and fuses the domain-bounds of such declarations into
a Cartesian product.

The motivation for doing so is that it enables passing
such functions (of tuples) to Isabelle and Zenon with
the existing support that is available in those backends
(for tuples and Cartesian products), and the proofs succeed.


## Other changes

- DOC: update file `todo.txt`

- ENH: add function `E_visit.name_operators` for
  converting syntax trees with positional operator
  references to syntax trees with operator
  references by name (i.e., conversion of `Ix` nodes
  to `Opaque` nodes).

Signed-off-by: Ioannis Filippidis <[email protected]>

Signed-off-by: Ioannis Filippidis <[email protected]>

Signed-off-by: Ioannis Filippidis <[email protected]>

<tlaplus#140>

Signed-off-by: Ioannis Filippidis <[email protected]>

Signed-off-by: Ioannis Filippidis <[email protected]>

Signed-off-by: Ioannis Filippidis <[email protected]>