From ffb6c4b91862a03af767d6b0e627d3d20539b79a Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Sat, 26 Oct 2024 15:51:36 -0400 Subject: [PATCH] Synced syntax tests Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- test/corpus/infix_op.txt | 75 ++++++++-- test/corpus/number.txt | 18 ++- test/corpus/proofs.txt | 187 +++++++++++++++++++++++-- test/corpus/quantification.txt | 229 +++++++++++++++++++++++++++++-- test/corpus/recursive.txt | 18 +++ test/corpus/regression.txt | 16 --- test/corpus/sets.txt | 42 +++++- test/corpus/step_expressions.txt | 24 ++++ test/corpus/subexpressions.txt | 2 +- test/corpus/use_or_hide.txt | 97 ++++++++++++- 10 files changed, 648 insertions(+), 60 deletions(-) diff --git a/test/corpus/infix_op.txt b/test/corpus/infix_op.txt index 053bcdc..d1660f0 100644 --- a/test/corpus/infix_op.txt +++ b/test/corpus/infix_op.txt @@ -1,3 +1,19 @@ +=============||| +Cartesian Product Infix Op Definition +=============||| + +---- MODULE Test ---- +x \X y == 0 +x \times y == 0 +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition parameter: (identifier) name: (infix_op_symbol (times)) parameter: (identifier) (def_eq) definition: (nat_number)) + (operator_definition parameter: (identifier) name: (infix_op_symbol (times)) parameter: (identifier) (def_eq) definition: (nat_number)) +(double_line))) + =============||| Infix Operator Definition =============||| @@ -100,8 +116,6 @@ x \succ y == 92 x \succeq y == 93 x \supset y == 94 x \supseteq y == 95 -x \X y == 96 -x \times y == 97 x \uplus y == 98 x | y == 99 x || y == 100 @@ -208,14 +222,28 @@ x \wr y == 101 (operator_definition parameter: (identifier) name: (infix_op_symbol (succeq)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (supset)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (supseteq)) parameter: (identifier) (def_eq) definition: (nat_number)) - (operator_definition parameter: (identifier) name: (infix_op_symbol (times)) parameter: (identifier) (def_eq) definition: (nat_number)) - (operator_definition parameter: (identifier) name: (infix_op_symbol (times)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (uplus)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (vert)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (vertvert)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (wr)) parameter: (identifier) (def_eq) definition: (nat_number)) (double_line))) +=============||| +Cartesian Product Declaration as Parameter +=============||| + +---- MODULE Test ---- +op(_ \X _, _ \times _) == TRUE +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) + parameter: (operator_declaration (placeholder) name: (infix_op_symbol (times)) (placeholder)) + parameter: (operator_declaration (placeholder) name: (infix_op_symbol (times)) (placeholder)) + (def_eq) definition: (boolean)) +(double_line))) =============||| Infix Operator Declaration as Parameter @@ -320,8 +348,6 @@ op( _ \succeq _, _ \supset _, _ \supseteq _, - _ \X _, - _ \times _, _ \uplus _, _ | _, _ || _, @@ -430,8 +456,6 @@ op( parameter: (operator_declaration (placeholder) name: (infix_op_symbol (succeq)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (supset)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (supseteq)) (placeholder)) - parameter: (operator_declaration (placeholder) name: (infix_op_symbol (times)) (placeholder)) - parameter: (operator_declaration (placeholder) name: (infix_op_symbol (times)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (uplus)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (vert)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (vertvert)) (placeholder)) @@ -663,6 +687,39 @@ op == { )) (double_line))) +=============||| +Cartesian Product as Parameter +=============||| + +---- MODULE Test ---- +op == f(\X, \times) +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_op name: (identifier_ref) + parameter: (infix_op_symbol (times)) + parameter: (infix_op_symbol (times)) + )) +(double_line))) + +=============||| +Infix Minus as Parameter +=============||| + +---- MODULE Test ---- +op == f ( - ) +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_op name: (identifier_ref) + parameter: (infix_op_symbol (minus)) + )) +(double_line))) + =============||| Infix Operators as Parameters =============||| @@ -717,7 +774,6 @@ op == f( <, <:, :>, - -, --, %, %%, @@ -824,7 +880,6 @@ op == f( parameter: (infix_op_symbol (lt)) parameter: (infix_op_symbol (map_from)) parameter: (infix_op_symbol (map_to)) - parameter: (infix_op_symbol (minus)) parameter: (infix_op_symbol (minusminus)) parameter: (infix_op_symbol (mod)) parameter: (infix_op_symbol (modmod)) diff --git a/test/corpus/number.txt b/test/corpus/number.txt index f91c5e2..a2016a8 100644 --- a/test/corpus/number.txt +++ b/test/corpus/number.txt @@ -1,10 +1,24 @@ ======================||| -All Number Formats +Common Number Formats ======================||| ---- MODULE Test ---- op == 12345 op == 12345.12345 +==== + +----------------------||| + +(source_file (module (header_line) (identifier) (header_line) + (operator_definition (identifier) (def_eq) (nat_number)) + (operator_definition (identifier) (def_eq) (real_number)) +(double_line))) + +======================||| +Bitfield Number Formats +======================||| + +---- MODULE Test ---- op == \b01010101 op == \B10101010 op == \o01234567 @@ -16,8 +30,6 @@ op == \H9876543210FEDCBA ----------------------||| (source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) (nat_number)) - (operator_definition (identifier) (def_eq) (real_number)) (operator_definition (identifier) (def_eq) (binary_number (format) (value))) (operator_definition (identifier) (def_eq) (binary_number (format) (value))) (operator_definition (identifier) (def_eq) (octal_number (format) (value))) diff --git a/test/corpus/proofs.txt b/test/corpus/proofs.txt index 792ec31..1864682 100644 --- a/test/corpus/proofs.txt +++ b/test/corpus/proofs.txt @@ -98,13 +98,10 @@ Proof by Multiple Definitions LEMMA TRUE PROOF BY ONLY P, - MODULE Naturals, - Q, - MODULE Integers + Q DEFS >, R, - MODULE Reals, = ==== @@ -115,27 +112,55 @@ PROOF BY ONLY (terminal_proof (use_body (use_body_expr (identifier_ref) - (module_ref (identifier_ref)) (identifier_ref) - (module_ref (identifier_ref)) ) (use_body_def (infix_op_symbol (gt)) (identifier_ref) - (module_ref (identifier_ref)) (infix_op_symbol (eq)) ) )) ) (double_line))) +===============================||| +Proof by Module References +===============================||| + +---- MODULE Test ---- +LEMMA TRUE +PROOF BY ONLY + MODULE Naturals, + MODULE Integers + DEFS + MODULE Reals, + MODULE Sequences +==== + +-------------------------------||| + +(source_file (module (header_line) (identifier) (header_line) + (theorem (boolean) + (terminal_proof (use_body + (use_body_expr + (module_ref (identifier_ref)) + (module_ref (identifier_ref)) + ) + (use_body_def + (module_ref (identifier_ref)) + (module_ref (identifier_ref)) + ) + )) + ) +(double_line))) + ===============================||| Proof by QED ===============================||| ---- MODULE Test ---- COROLLARY TRUE -PROOF <1>a QED BY <1>a, <*>a +PROOF <1>a QED BY <1>a, <1>b ==== -------------------------------||| @@ -153,6 +178,32 @@ PROOF <1>a QED BY <1>a, <*>a ) (double_line))) +===============================||| +Proof by QED with implicit step level +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +PROOF + <1>a TRUE + <1>b QED BY <*>a +==== + +-------------------------------||| + +(source_file (module (header_line) (identifier) (header_line) + (theorem (boolean) + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (suffices_proof_step (boolean))) + (qed_step (proof_step_id (level) (name)) + (terminal_proof (use_body (use_body_expr + (proof_step_ref (level) (name)) + ))) + ) + ) + ) +(double_line))) + ===============================||| Extra QED :error @@ -161,11 +212,11 @@ Extra QED ---- MODULE Test ---- THEOREM x == TRUE -<*> P +<1> P <+> Q <*> QED <*> QED -<*> QED +<1> QED ==== -------------------------------||| @@ -187,7 +238,6 @@ THEOREM TRUE <1>i..... PICK a, b, c : 7 <1>j..... HIDE 8 <1>k..... USE 9 -<1>l..... INSTANCE M <1>m..... QED ==== @@ -207,6 +257,26 @@ THEOREM TRUE (proof_step (proof_step_id (level) (name)) (pick_proof_step (identifier) (identifier) (identifier) (nat_number))) (proof_step (proof_step_id (level) (name)) (use_or_hide (use_body (use_body_expr (nat_number))))) (proof_step (proof_step_id (level) (name)) (use_or_hide (use_body (use_body_expr (nat_number))))) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Proof with INSTANCE step type +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1>a..... INSTANCE M +<1>b..... QED +==== + +-------------------------------||| + +(source_file (module (header_line) (identifier) (header_line) + (theorem (boolean) + (non_terminal_proof (proof_step (proof_step_id (level) (name)) (instance (identifier_ref))) (qed_step (proof_step_id (level) (name))) ) @@ -464,26 +534,75 @@ COROLLARY TRUE ) (double_line))) +===============================||| +Implicit Proof Steps With Names +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<*>abc 1 +<*>def QED +==== + +-------------------------------||| + +(source_file (module (header_line) (identifier) (header_line) + (theorem (boolean) + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Plus Proof Step With Name +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1>abc 1 + <+>def 2 + <2>ghi QED +<1>jkl QED +==== + +-------------------------------||| + +(source_file (module (header_line) (identifier) (header_line) + (theorem (boolean) + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number) + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) + (qed_step (proof_step_id (level) (name))) + ) + )) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + ==============================||| Proof Containing Jlist ==============================||| ---- MODULE Test ---- THEOREM TRUE -<*>a1a... +<*> /\ 1 /\ \/ 2 - <+>b2b... WITNESS + <+> WITNESS \/ 3 \/ /\ 4, /\ \/ 5 /\ 6 - <*>c3c... QED BY + <*> QED BY /\ 7 /\ \/ 8, \/ /\ 9 \/ 10 -<*>d4d... QED BY +<*> QED BY \/ 11 \/ /\ 12, /\ \/ 13 @@ -536,3 +655,41 @@ THEOREM TRUE )) (double_line))) + +==============================||| +Proof Level Change Terminates Jlist +==============================||| + +---- MODULE Test ---- +THEOREM TRUE +<*> /\ 1 + /\ 2 + <+> QED BY + \/ 1 + \/ 2 + <*> QED +==== + +------------------------------||| + + +(source_file (module (header_line) (identifier) (header_line) + (theorem (boolean) (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (suffices_proof_step + (conj_list + (conj_item (bullet_conj) (nat_number)) + (conj_item (bullet_conj) (nat_number)) + ) + (non_terminal_proof + (qed_step (proof_step_id (level) (name)) (terminal_proof (use_body (use_body_expr + (disj_list + (disj_item (bullet_disj) (nat_number)) + (disj_item (bullet_disj) (nat_number)) + ) + )))) + ) + )) + (qed_step (proof_step_id (level) (name))) + )) +(double_line))) + diff --git a/test/corpus/quantification.txt b/test/corpus/quantification.txt index 468f200..1353323 100644 --- a/test/corpus/quantification.txt +++ b/test/corpus/quantification.txt @@ -3,8 +3,8 @@ Bounded Quantification ==============================||| ---- MODULE Test ---- -op == \A x, y \in Nat, z \in Int, <> \in Real : FALSE -op == \E <> \in Nat, a, b \in Int : TRUE +op == \A x, y \in Nat, z \in Int, a, b, c \in Real : FALSE +op == \E x, y \in Nat, a, b \in Int : TRUE ==== ------------------------------||| @@ -14,7 +14,8 @@ op == \E <> \in Nat, a, b \in Int : TRUE definition: (bounded_quantification quantifier: (forall) bound: (quantifier_bound - intro: (identifier) intro: (identifier) + intro: (identifier) + intro: (identifier) (set_in) set: (nat_number_set) ) @@ -24,7 +25,9 @@ op == \E <> \in Nat, a, b \in Int : TRUE set: (int_number_set) ) bound: (quantifier_bound - intro: (tuple_of_identifiers (langle_bracket) (identifier) (identifier) (identifier) (rangle_bracket)) + intro: (identifier) + intro: (identifier) + intro: (identifier) (set_in) set: (real_number_set) ) @@ -35,12 +38,196 @@ op == \E <> \in Nat, a, b \in Int : TRUE definition: (bounded_quantification quantifier: (exists) bound: (quantifier_bound - intro: (tuple_of_identifiers (langle_bracket) (identifier) (identifier) (rangle_bracket)) + intro: (identifier) + intro: (identifier) (set_in) set: (nat_number_set) ) bound: (quantifier_bound - intro: (identifier) intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (int_number_set) + ) + expression: (boolean) + ) + ) +(double_line))) + +==============================||| +Verbose Bounded Quantification +==============================||| + +---- MODULE Test ---- +op == \forall x, y \in Nat, z \in Int, a, b, c \in Real : FALSE +op == \exists x, y \in Nat, a, b \in Int : TRUE +==== + +------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: (bounded_quantification + quantifier: (forall) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) + (set_in) + set: (nat_number_set) + ) + bound: (quantifier_bound + intro: (identifier) + (set_in) + set: (int_number_set) + ) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (real_number_set) + ) + expression: (boolean) + ) + ) + (operator_definition name: (identifier) (def_eq) + definition: (bounded_quantification + quantifier: (exists) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) + (set_in) + set: (nat_number_set) + ) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) + (set_in) + set: (int_number_set) + ) + expression: (boolean) + ) + ) +(double_line))) + +==============================||| +Bounded Quantification With Tuples +==============================||| + +---- MODULE Test ---- +op == \A <> \in Nat, <> \in Int, <> \in Real : FALSE +op == \E <> \in Nat, <> \in Int : TRUE +==== + +------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: (bounded_quantification + quantifier: (forall) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (nat_number_set) + ) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (rangle_bracket)) + (set_in) + set: (int_number_set) + ) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (real_number_set) + ) + expression: (boolean) + ) + ) + (operator_definition name: (identifier) (def_eq) + definition: (bounded_quantification + quantifier: (exists) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (nat_number_set) + ) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (int_number_set) + ) + expression: (boolean) + ) + ) +(double_line))) + +==============================||| +Mixed Bounded Quantification With Tuples +==============================||| + +---- MODULE Test ---- +op == \A x, y \in Nat, <> \in Int, a, b, c \in Real : FALSE +op == \E <> \in Nat, a, b \in Int : TRUE +==== + +------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: (bounded_quantification + quantifier: (forall) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) + (set_in) + set: (nat_number_set) + ) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (rangle_bracket)) + (set_in) + set: (int_number_set) + ) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (real_number_set) + ) + expression: (boolean) + ) + ) + (operator_definition name: (identifier) (def_eq) + definition: (bounded_quantification + quantifier: (exists) + bound: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (nat_number_set) + ) + bound: (quantifier_bound + intro: (identifier) + intro: (identifier) (set_in) set: (int_number_set) ) @@ -105,7 +292,6 @@ Bounded CHOOSE ---- MODULE Test ---- op == CHOOSE x \in Nat : TRUE -op == CHOOSE <> \in S : FALSE ==== ------------------------------||| @@ -119,6 +305,19 @@ op == CHOOSE <> \in S : FALSE expression: (boolean) ) ) +(double_line))) + +==============================||| +Bounded CHOOSE With Tuple +==============================||| + +---- MODULE Test ---- +op == CHOOSE <> \in S : FALSE +==== + +------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) definition: (choose intro: (tuple_of_identifiers (langle_bracket) (identifier) (identifier) (identifier) (rangle_bracket)) @@ -135,7 +334,6 @@ Unbounded CHOOSE ---- MODULE Test ---- op == CHOOSE x : TRUE -op == CHOOSE <> : FALSE ==== ------------------------------||| @@ -147,6 +345,20 @@ op == CHOOSE <> : FALSE expression: (boolean) ) ) +(double_line))) + + +==============================||| +Unbounded CHOOSE With Tuple +==============================||| + +---- MODULE Test ---- +op == CHOOSE <> : FALSE +==== + +------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) definition: (choose intro: (tuple_of_identifiers (langle_bracket) (identifier) (identifier) (identifier) (rangle_bracket)) @@ -154,4 +366,3 @@ op == CHOOSE <> : FALSE ) ) (double_line))) - diff --git a/test/corpus/recursive.txt b/test/corpus/recursive.txt index 2f4f264..31de4ba 100644 --- a/test/corpus/recursive.txt +++ b/test/corpus/recursive.txt @@ -12,6 +12,24 @@ RECURSIVE f(_) (recursive_declaration (operator_declaration (identifier) (placeholder))) (double_line))) +=============||| +Recursive Declaration With Reference +=============||| + +---- MODULE Test ---- +RECURSIVE f(_) +f(x) == f(x) +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (recursive_declaration (operator_declaration name: (identifier) parameter: (placeholder))) + (operator_definition name: (identifier) parameter: (identifier) (def_eq) definition: + (bound_op name: (identifier_ref) parameter: (identifier_ref)) + ) +(double_line))) + =============||| Recursive Declaration Without Parameters =============||| diff --git a/test/corpus/regression.txt b/test/corpus/regression.txt index 789ae92..1077f76 100644 --- a/test/corpus/regression.txt +++ b/test/corpus/regression.txt @@ -39,9 +39,7 @@ Junct Tokens as Higher-Level Parameters (TSTLA#GH96) ---- MODULE Test ---- op == op(/\, x, /\) -op == op(∧, x, ∧) op == op(\/, x, \/) -op == op(∨, x, ∨) ==== --------------||| @@ -54,20 +52,6 @@ op == op(∨, x, ∨) parameter: (infix_op_symbol (land)) ) ) - (operator_definition name: (identifier) (def_eq) definition: - (bound_op name: (identifier_ref) - parameter: (infix_op_symbol (land)) - parameter: (identifier_ref) - parameter: (infix_op_symbol (land)) - ) - ) - (operator_definition name: (identifier) (def_eq) definition: - (bound_op name: (identifier_ref) - parameter: (infix_op_symbol (lor)) - parameter: (identifier_ref) - parameter: (infix_op_symbol (lor)) - ) - ) (operator_definition name: (identifier) (def_eq) definition: (bound_op name: (identifier_ref) parameter: (infix_op_symbol (lor)) diff --git a/test/corpus/sets.txt b/test/corpus/sets.txt index 2297b57..6a9b90d 100644 --- a/test/corpus/sets.txt +++ b/test/corpus/sets.txt @@ -14,14 +14,39 @@ op == { } ) (double_line))) +======================||| +Mistaken Set Filter Test +======================||| + +---- MODULE Test ---- + +op == {x \in Nat} +op == {x \in BOOLEAN, y \in STRING} + +==== + +----------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: + (finite_set_literal + (bound_infix_op lhs: (identifier_ref) symbol: (in) rhs: (nat_number_set)) + ) + ) + (operator_definition name: (identifier) (def_eq) definition: + (finite_set_literal + (bound_infix_op lhs: (identifier_ref) symbol: (in) rhs: (boolean_set)) + (bound_infix_op lhs: (identifier_ref) symbol: (in) rhs: (string_set)) + ) + ) +(double_line))) + ======================||| Set Literal ======================||| ---- MODULE Test ---- op == { - x \in BOOLEAN, - y \in STRING, TRUE, FALSE, ((1 + 2) * 3), @@ -34,8 +59,6 @@ op == { (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) definition: (finite_set_literal - (bound_infix_op lhs: (identifier_ref) symbol: (in) rhs: (boolean_set)) - (bound_infix_op lhs: (identifier_ref) symbol: (in) rhs: (string_set)) (boolean) (boolean) (parentheses @@ -139,6 +162,17 @@ op == {x \in Nat : P(x)} ) (double_line))) +======================||| +Set Filter With Too Many Quantifiers +:error +======================||| + +---- MODULE Test ---- +op == {x \in Nat, y \in Int : P(x, y)} +==== + +----------------------||| + ======================||| Set Filter with Tuple ======================||| diff --git a/test/corpus/step_expressions.txt b/test/corpus/step_expressions.txt index 146cf33..7a02b47 100644 --- a/test/corpus/step_expressions.txt +++ b/test/corpus/step_expressions.txt @@ -38,6 +38,30 @@ op == <>_<> ) (double_line))) +=============||| +Step Expression With Parameterized Subscript +=============||| + +---- MODULE Test ---- +op == [A]_M(S)!vars +==== + +--------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: + (step_expr_or_stutter + (identifier_ref) + (prefixed_op + prefix: (subexpr_prefix (subexpr_component + (bound_op name: (identifier_ref) parameter: (identifier_ref)) + )) + op: (identifier_ref) + ) + ) + ) +(double_line))) + =============||| Step Expressions with Jlist =============||| diff --git a/test/corpus/subexpressions.txt b/test/corpus/subexpressions.txt index a7de273..c463dd0 100644 --- a/test/corpus/subexpressions.txt +++ b/test/corpus/subexpressions.txt @@ -53,7 +53,7 @@ Proof Step ID Subexpression Tree Navigation ---- MODULE Test ---- COROLLARY TRUE -PROOF <1>a QED BY <1>a!<>!3!(x, y)!:!@, <*>a!<>!3!(x, y)!:!@ +PROOF <1>a QED BY <1>a!<>!3!(x, y)!:!@, <1>a!<>!3!(x, y)!:!@ ==== -------------------------------||| diff --git a/test/corpus/use_or_hide.txt b/test/corpus/use_or_hide.txt index 1736a64..7503f28 100644 --- a/test/corpus/use_or_hide.txt +++ b/test/corpus/use_or_hide.txt @@ -1,5 +1,99 @@ =============||| -Use & Hide Declarations +Simple Use or Hide +=============||| + +---- MODULE Test ---- +USE X, Y +HIDE X +HIDE Y +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (use_or_hide (use_body + (use_body_expr + (identifier_ref) + (identifier_ref) + ) + )) + (use_or_hide (use_body + (use_body_expr + (identifier_ref) + ) + )) + (use_or_hide (use_body + (use_body_expr + (identifier_ref) + ) + )) +(double_line))) + +=============||| +Hide Multiple Definitions +=============||| + +---- MODULE Test ---- +HIDE X, Y +HIDE DEFS X, Y +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (use_or_hide (use_body + (use_body_expr + (identifier_ref) + (identifier_ref) + ) + )) + (use_or_hide (use_body + (use_body_def + (identifier_ref) + (identifier_ref) + ) + )) +(double_line))) + +=============||| +Complicated Use & Hide +=============||| + +---- MODULE Test ---- +USE x, 1 + 3 +HIDE DEFS -., *, ^+ +USE x DEF z, x +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (use_or_hide (use_body + (use_body_expr + (identifier_ref) + (bound_infix_op lhs: (nat_number) symbol: (plus) rhs: (nat_number)) + ) + )) + (use_or_hide (use_body + (use_body_def + (prefix_op_symbol (negative)) + (infix_op_symbol (mul)) + (postfix_op_symbol (sup_plus)) + ) + )) + (use_or_hide (use_body + (use_body_expr + (identifier_ref) + ) + (use_body_def + (identifier_ref) + (identifier_ref) + ) + )) +(double_line))) + +=============||| +Use & Hide Modules =============||| ---- MODULE Test ---- @@ -37,4 +131,3 @@ USE x, MODULE M DEF MODULE M, x ) )) (double_line))) -