ENH: parse and expand bound tuples #140

johnyf · 2024-06-26T16:45:10Z

Parsing and translation support for bound tuples, examples:

rigid quantification \E <<x, y>> \in A \X B: ...
choose expressions CHOOSE <<x, y>> \in A \X B: ...
set constructor for subset {<<x, y>> \in A \X B: ...}
set constructor {...: <<x, y>> \in A \X B}
function definitions f[<<x, y>> \in A \X B] = ...
function constructors [<<x, y>> \in A \X B |-> ...]

The syntax tree is changed to represent bound tuples. The translation is after the parser and before conversion to indexed identifiers. Subexpression references where bound tuples occur are not supported.

If a Cartesian product is found in the expression, of the same length as the bound tuple, for example <<x, y>> \in A \X B, then a rewriting to a simpler expression is applied. For example,

{<<x, y>> \in A \X B:
    P(x, y)}

is translated to (the names of auto-generated identifiers differ):

{y \in A \X B:
    LET
        a == y[1]
        b == y[2]
    IN
        P(a, b)}

Another case is:

{x + y: <<x, y>> \in A \X B}

which is translated to:

{x + y: x \in A, y \in B}

Otherwise the rewriting results in expressions that contain CHOOSE or quantification.

Includes fixes to parsing of declarations in function definitions and quantification.

Signed-off-by: Markus Alexander Kuppe <[email protected]>

ahelwer · 2024-11-04T14:36:11Z

@johnyf could you rebase on the latest changes in main to see whether these changes pass the new syntax tests from #159? I tried to rebase myself but could not successfully resolve the merge conflicts in src/expr/e_anon.ml.

johnyf · 2024-11-04T17:32:14Z

I will try to rebase the changes.

ahelwer · 2024-11-04T17:38:45Z

Great! You can run the parser tests with dune runtest test/parser --force --always-show-command-line; they should take less than a second. It should cause these tests to fail:

tlapm/test/parser/parser_tests.ml

Lines 92 to 97 in 56f33ef

    
           (* https://github.com/tlaplus/tlapm/issues/11 *) 
        
           "Bounded Quantification With Tuples"; 
        
           "Mixed Bounded Quantification With Tuples"; 
        
           "Bounded CHOOSE With Tuple"; 
        
           "Unbounded CHOOSE With Tuple"; 
        
           "Set Filter with Tuple";

If you delete those test names from the list then the test should pass if these changes fix all those cases.

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]>

johnyf · 2024-11-06T11:01:40Z

Thank you for noting how to configure the parser tests. Rebased (omitted blankspace and formatting changes) and updated to recent changes. The parsing tests pass, including also one more, about {x \in Nat}.

ahelwer · 2024-11-06T13:02:26Z

Okay great! Are you able to join the next TLA+ community call on November 12th and talk about these changes? They seem really great so I would like to get everybody talking about the best way to get them in.

johnyf · 2024-11-07T12:04:37Z

Yes, I can join the next TLA+ community call and talk about the changes. Thank you for suggesting it!

damiendoligez

This looks good but I have a few remarks and suggestions you might want to take into account.

src/expr/e_namespaces.ml

damiendoligez · 2024-07-23T11:28:54Z

src/expr/e_namespaces.ml

+
+(* Scheme 1: Planar coordinates
+
+Fresh identifier based on location.


Note that this method doesn't guarantee a fresh identifier, as the user could have an identifier in scope named somefile_line_123_column_45. We can probably ignore this problem as too unlinkely to happen in practice.

Indeed. The module E_namespaces was added to be used in the module E_tuply_declarations, but E_namespaces is currently not used, so it could be removed, or the function mint_from_hint removed.

(In coalescing a similar mapping was experimentally applied to all identifiers of a proof obligation (when with_unique_identifiers = true in Coalesce), but if applied partially identifiers can coincide with existing ones.)

I think it's better to avoid unused code and remove E_namespaces entirely, we can add it back if we need it in the future.

src/expr/e_namespaces.ml

src/expr/e_parser.ml

src/expr/e_visit.ml

src/global/intermediate.ml

src/module/m_visit.ml

johnyf · 2024-11-12T17:15:16Z

Thank you for reviewing! I will work on revising the changes.

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

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

johnyf

Thank you for the remarks and suggestions, I revised the changes by adding 2 new commits.

johnyf · 2024-11-13T14:28:37Z

src/expr/e_namespaces.ml

+
+(* Scheme 1: Planar coordinates
+
+Fresh identifier based on location.


Indeed. The module E_namespaces was added to be used in the module E_tuply_declarations, but E_namespaces is currently not used, so it could be removed, or the function mint_from_hint removed.

(In coalescing a similar mapping was experimentally applied to all identifiers of a proof obligation (when with_unique_identifiers = true in Coalesce), but if applied partially identifiers can coincide with existing ones.)

src/expr/e_namespaces.ml

src/expr/e_parser.ml

src/expr/e_visit.ml

src/global/intermediate.ml

src/module/m_visit.ml

src/util/fmtutil.ml

damiendoligez

Looks good. We can merge this after you remove E_namespaces or if you prefer to keep it.

johnyf · 2024-11-27T13:26:39Z

Thank you for approving the changes. I removed E_namespaces in a new commit.

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

lemmy added a commit to lemmy/pbft-tlaplus that referenced this pull request Sep 3, 2024

TLAPM does not (yet) support bound tuples (tlaplus/tlapm#140)

fda5046

Signed-off-by: Markus Alexander Kuppe <[email protected]>

lemmy added a commit to heidihoward/pbft-tlaplus that referenced this pull request Sep 6, 2024

TLAPM does not (yet) support bound tuples (tlaplus/tlapm#140)

ff2c91a

Signed-off-by: Markus Alexander Kuppe <[email protected]>

johnyf added 9 commits November 4, 2024 19:48

API: change syntax tree to represent also tuply declarations

893431d

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]>

REF: cons during fold, and reverse upon completion

2c61f99

instead of appending during the fold. This approach is more efficient. Also: - STY: blankspace formatting Signed-off-by: Ioannis Filippidis <[email protected]>

ENH: add class Module.deep_map

371fd71

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

TST: update parser tests for cases now parsed

5aea669

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

MNT: add tuple-declaration cases to patterns

303e7f8

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

johnyf force-pushed the tuple_declarations branch from a7e8d5e to 303e7f8 Compare November 6, 2024 10:43

damiendoligez reviewed Nov 12, 2024

View reviewed changes

johnyf added 2 commits November 13, 2024 15:01

MNT: apply changes from pull request review

3b69928

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

MNT: complete implementation of M_visit.deep_map

e702c3f

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

johnyf commented Nov 13, 2024

View reviewed changes

damiendoligez approved these changes Nov 26, 2024

View reviewed changes

MNT: rm E_namespaces

7af4592

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

johnyf force-pushed the tuple_declarations branch from 319335b to 7af4592 Compare November 27, 2024 13:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

ENH: parse and expand bound tuples #140

ENH: parse and expand bound tuples #140

johnyf commented Jun 26, 2024

ahelwer commented Nov 4, 2024

johnyf commented Nov 4, 2024

ahelwer commented Nov 4, 2024

johnyf commented Nov 6, 2024

ahelwer commented Nov 6, 2024

johnyf commented Nov 7, 2024

damiendoligez left a comment •

edited

Loading

damiendoligez Jul 23, 2024

johnyf Nov 13, 2024

damiendoligez Nov 26, 2024

johnyf commented Nov 12, 2024

johnyf left a comment

johnyf Nov 13, 2024

damiendoligez left a comment

johnyf commented Nov 27, 2024


		(* Scheme 1: Planar coordinates

		Fresh identifier based on location.

ENH: parse and expand bound tuples #140

Are you sure you want to change the base?

ENH: parse and expand bound tuples #140

Conversation

johnyf commented Jun 26, 2024

ahelwer commented Nov 4, 2024

johnyf commented Nov 4, 2024

ahelwer commented Nov 4, 2024

johnyf commented Nov 6, 2024

ahelwer commented Nov 6, 2024

johnyf commented Nov 7, 2024

damiendoligez left a comment • edited Loading

Choose a reason for hiding this comment

damiendoligez Jul 23, 2024

Choose a reason for hiding this comment

johnyf Nov 13, 2024

Choose a reason for hiding this comment

damiendoligez Nov 26, 2024

Choose a reason for hiding this comment

johnyf commented Nov 12, 2024

johnyf left a comment

Choose a reason for hiding this comment

johnyf Nov 13, 2024

Choose a reason for hiding this comment

damiendoligez left a comment

Choose a reason for hiding this comment

johnyf commented Nov 27, 2024

damiendoligez left a comment •

edited

Loading