Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

fixes related to bounding of declarees in quantification and function definitions #60

Open
wants to merge 4 commits into
base: main
Choose a base branch
from
Open

fixes related to bounding of declarees in quantification and function definitions #60

wants to merge 4 commits into from

Commits on Jun 21, 2022

  1. API: change syntax tree to represent also tuply declarations 

    and update the code throughout `tlapm`,
because this commit changes the existing types in the
module `Expr.T`.
    @johnyf
    johnyf committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    2a81986 View commit details
    Browse the repository at this point in the history

  2. BUG: do not allow unbounded declarations in function definitions 

    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.
    @johnyf
    johnyf committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    460c378 View commit details
    Browse the repository at this point in the history

  3. BUG: do not allow both bounded and unbounded declarations in \E, \A 

    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.
    @johnyf
    johnyf committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    0667253 View commit details
    Browse the repository at this point in the history

  4. TST: that function constructors allow only bounded declarations 

    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.
    @johnyf
    johnyf committed Jun 21, 2022
    Configuration menu
    Copy the full SHA
    3845b04 View commit details
    Browse the repository at this point in the history