diff --git a/dune-project b/dune-project index 71b7406d..63304037 100644 --- a/dune-project +++ b/dune-project @@ -43,6 +43,7 @@ ocaml dune-site dune-build-info + sexp_diff sexplib cmdliner camlzip diff --git a/src/tlapm_lib.ml b/src/tlapm_lib.ml index 206b450e..a328d9ae 100644 --- a/src/tlapm_lib.ml +++ b/src/tlapm_lib.ml @@ -653,7 +653,7 @@ let modctx_of_string ~(content : string) ~(filename : string) ~loader_paths ~pre | None, None -> Error (None, Printexc.to_string e)) let module_of_string module_str = - let hparse = Tla_parser.P.use M_parser.parse in + let hparse = Tla_parser.P.use Module.Parser.parse in let (flex, _) = Alexer.lex_string module_str in Tla_parser.P.run hparse ~init:Tla_parser.init ~source:flex diff --git a/src/tlapm_lib.mli b/src/tlapm_lib.mli index 2285d5fd..dc22ba79 100644 --- a/src/tlapm_lib.mli +++ b/src/tlapm_lib.mli @@ -25,7 +25,7 @@ val modctx_of_string : from a specified string, assume it is located in the specified path. *) -val module_of_string : string -> M_t.mule option +val module_of_string : string -> Module.T.mule option (** Parse the specified string as a module. No dependencies are considered, nor proof obligations are elaborated. *) diff --git a/test/parser/dune b/test/parser/dune index edec5139..1318a281 100644 --- a/test/parser/dune +++ b/test/parser/dune @@ -1,7 +1,7 @@ (test (name parser_tests) (modes exe) - (libraries tlapm_lib ounit2 sexplib) + (libraries tlapm_lib ounit2 sexplib sexp_diff) (deps (glob_files_rec syntax_corpus/*)) (preprocess (pps ppx_deriving.show)) ) diff --git a/test/parser/parser_tests.ml b/test/parser/parser_tests.ml index f4409cdf..44439d92 100644 --- a/test/parser/parser_tests.ml +++ b/test/parser/parser_tests.ml @@ -1,93 +1,28 @@ -(** This test runs a battery of TLA+ syntax fragments against TLAPM's syntax - parser. In the future it will check the actual parse tree emitted by - TLAPM, but for now it just checks whether TLAPM parses without error all - the syntax it is expected to parse. Tests sourced from: +(** This file runs a battery of TLA+ syntax fragments against TLAPM's syntax + parser. It then takes the resulting parse tree and translates it into a + normalized S-expression form to compare with the associated expected AST. + Tests are sourced from the standardized syntax test corpus at: https://github.com/tlaplus/rfcs/tree/2a772d9dd11acec5d7dedf30abfab91a49de48b8/language_standard/tests/tlaplus_syntax *) +open Tlapm_lib;; + open Syntax_corpus_file_parser;; -open OUnit2;; (** Calls TLAPM's parser with the given input. Catches all exceptions and treats them as parse failures. @param input The TLA+ fragment to parse. @return None if parse failure, syntax tree root if successful. *) -let parse (input : string) : Tlapm_lib__M_t.mule option = - try Tlapm_lib.module_of_string input +let parse (input : string) : Module.T.mule option = + try module_of_string input with _ -> None -(** Datatype summarizing a run of all the syntax tests. *) -type test_run_summary = { - total : int; - succeeded : int; - failed : int; - skipped : int; - failures : syntax_test_info list; -} [@@deriving show] - -(** A blank test summary. *) -let test_summary_init = { - total = 0; - succeeded = 0; - failed = 0; - skipped = 0; - failures = []; -} - -(** Runs a given syntax test by determining its type then sending the input - into the TLAPM parser. - @param expect_failure Whether this test should fail due to a TLAPM bug. - @param test Information about the test itself. - @return Whether the test succeeded. -*) -let run_test (test : syntax_test) : bool = - match test.test with - | Error_test input -> parse input |> Option.is_none - | Expected_test (input, _) -> parse input |> Option.is_some - -(** Controls run of a given syntax test. Checks whether test should be - skipped and whether it is expected to fail, then runs test and returns - summary. - @param expect_failure Whether this test should fail due to a TLAPM bug. - @param acc Accumulation variable for test summarization. - @param test Information about the test itself. - @return Test run summary. -*) -let control_test_run - (expect_failure : syntax_test -> bool) - (acc : test_run_summary) - (test : syntax_test) - : test_run_summary = - let acc = {acc with total = acc.total + 1} in - if test.skip then {acc with skipped = acc.skipped + 1} else - if run_test test = expect_failure test - then {acc with failed = acc.failed + 1; failures = test.info :: acc.failures} - else {acc with succeeded = acc.succeeded + 1} - -(** Given a path to a directory containing a corpus of syntax tests, get all - the tests encoded in those files, filter them as appropriate, then run - them all and collect the results. - @param path Path to the directory containing the corpus of syntax tests. - @param expect_failure Whether a test should fail due to a TLAPM bug. - @param filter_predicate Whether to actually execute a test. - @return Accumulated summary of all test executions. -*) -let run_test_corpus - (path : string) - (expect_failure : syntax_test -> bool) - (filter_pred : syntax_test -> bool) - : test_run_summary = - path - |> get_all_tests_under - |> List.filter filter_pred - |> List.fold_left (control_test_run expect_failure) test_summary_init - (** Names of tests that are known to fail due to TLAPM parser bugs. @param test Information about the test. @return Whether the test is expected to fail. *) -let expect_failure (test : syntax_test) : bool = +let expect_parse_failure (test : syntax_test) : bool = List.mem test.info.name [ (* https://github.com/tlaplus/tlapm/issues/54#issuecomment-2435515180 *) @@ -142,24 +77,97 @@ let expect_failure (test : syntax_test) : bool = "Nonfix Double Exclamation Operator (GH TSTLA #GH97, GH tlaplus/tlaplus #884)"; ] -(** Filter predicate to control which tests to run. - @param name Optional; a test name to filter on. - @return Predicate matching all tests or tests with given name. +(** Names of tests that are unable to match the expected output tree, but not + because of a bug; instead, the TLAPM syntax tree doesn't contain the + (usually extraneous) necessary information to fully populate the output + tree with the expected children. + @param test Information about the test. + @return Whether the test should skip the tree comparison phase. +*) +let should_skip_tree_comparison (test : syntax_test) : bool = + List.mem test.info.name [ + (* In TLAPM's ASSUME/PROVE parsing, NEW identifiers with unspecified + level are by default Constant instead of Unknown *) + "Assume/Prove With New Identifier of Unspecified Level"; + + (* Jlist terminated by single line comment omitted in TLAPM AST *) + "Keyword-Unit-Terminated Conjlist"; + "Keyword-Unit-Terminated Disjlist"; + + (* Unnecessary parentheses omitted in TLAPM AST *) + "Nested Parentheses"; + + (* TLAPM AST does not distinguish between nonfix and infix ops *) + "Lexically-Conflicting Nonfix Operators"; + "Minus and Negative"; + "Nonfix Minus (GH tlaplus/tlaplus #GH884)"; + "Nonfix Prefix Operators"; + "Nonfix Infix Operators"; + "Nonfix Postfix Operators"; + + (* TLAPM uses function literals for function definitions *) + (* See: https://github.com/tlaplus/tlapm/issues/237 *) + "Function Literal"; + + (* TLAPM makes multi-parameter EXCEPT update statements into tuples *) + "Record Update with Multiple Parameters"; + "Record Update with Tuple and Non-Tuple Parameters"; + + (* TLAPM does not distinguish between <=> and \equiv *) + "IFF Disambiguation" + ] + +(** Names of tests that are expected to fail the tree comparison phase due to + bugs in TLAPM's syntax parser. + @param test Information about the test. + @return Whether the test is expected to fail the tree comparison phase. *) -let should_run ?name test = - match name with - | Some name -> String.equal test.info.name name - | None -> true +let expect_tree_comparison_failure (test : syntax_test) : bool = + List.mem test.info.name [ + (* TLAPM appears to simply return an empty set here? *) + (* https://github.com/tlaplus/tlapm/issues/235 *) + "Mistaken Set Filter Test"; + "Mistaken Set Filter Tuples Test"; + ] + +open OUnit2;; -(** The top-level test; runs all syntax tests, prints summary, then fails - with an assertion if any tests failed. +(** Gathers all syntax test files, parses them, then runs the cases they + contain as tests against TLAPM's syntax parser, skipping or expecting + failure as appropriate. *) -let () = - let test_results = - run_test_corpus - "syntax_corpus" - expect_failure - (should_run (*~name:"Proof Containing Jlist"*)) - in - print_endline (show_test_run_summary test_results); - assert_equal 0 test_results.failed; +let tests = "Standardized syntax test corpus" >::: ( + get_all_tests_under "syntax_corpus" + |> List.map (fun test -> + Format.sprintf "[%s] %s" test.info.path test.info.name >:: + (fun _ -> + skip_if test.skip "Test has skip attribute"; + match test.test with + | Error_test input -> ( + match parse input with + | None -> assert_bool "Expected error test to fail" (not (expect_parse_failure test)) + | Some _ -> assert_bool "Expected parse failure" (expect_parse_failure test) + ) + | Expected_test (input, expected) -> ( + match parse input with + | None -> assert_bool "Expected parse success" (expect_parse_failure test) + | Some tlapm_output -> + skip_if (should_skip_tree_comparison test) "Skipping parse tree comparison"; + let open Translate_syntax_tree in + let open Sexplib in + let actual = tlapm_output |> translate_tla_source_file |> ts_node_to_sexpr in + if Sexp.equal expected actual + then assert_bool "Expected parse test to fail" (not (expect_tree_comparison_failure test)) + else + let open Sexp_diff in + let diff = Algo.diff ~original:expected ~updated:actual () in + let options = Display.Display_options.(create Layout.Single_column) in + let text = Display.display_with_ansi_colors options diff in + assert_bool text (expect_tree_comparison_failure test) + ) + ) + ) +) + +(** The OUnit2 test entrypoint. *) +let () = run_test_tt_main tests diff --git a/test/parser/syntax_corpus/assume-prove.txt b/test/parser/syntax_corpus/assume-prove.txt index 198bdf15..b04f0584 100644 --- a/test/parser/syntax_corpus/assume-prove.txt +++ b/test/parser/syntax_corpus/assume-prove.txt @@ -23,13 +23,44 @@ OBVIOUS ) (double_line))) +===============================||| +Nested Assume/Prove +===============================||| + +---- MODULE Test ---- +THEOREM thm == + ASSUME + ASSUME P + PROVE Q + PROVE C +OMITTED +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem + name: (identifier) (def_eq) + statement: (assume_prove + assumption: (inner_assume_prove + (assume_prove + assumption: (identifier_ref) + conclusion: (identifier_ref) + ) + ) + conclusion: (identifier_ref) + ) + proof: (terminal_proof) + ) +(double_line))) + ===============================||| Nested Assume/Prove With Label ===============================||| ---- MODULE Test ---- THEOREM thm == - ASSUME asm :: + ASSUME asm :: ASSUME P PROVE Q PROVE C @@ -56,7 +87,31 @@ OMITTED (double_line))) ===============================||| -Assume/Prove With New Constant +Assume/Prove With New Identifier of Unspecified Level +===============================||| + +---- MODULE Test ---- +THEOREM thm == + ASSUME NEW x \in S + PROVE C +OBVIOUS +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem + name: (identifier) (def_eq) + statement: (assume_prove + assumption: (new (identifier) (set_in) (identifier_ref)) + conclusion: (identifier_ref) + ) + proof: (terminal_proof) + ) +(double_line))) + +===============================||| +Assume/Prove With New Bound Constant ===============================||| ---- MODULE Test ---- @@ -79,6 +134,79 @@ OBVIOUS ) (double_line))) +===============================||| +Assume/Prove With New Bound Variable +===============================||| + +---- MODULE Test ---- +THEOREM thm == + ASSUME NEW VARIABLE x + PROVE C +OBVIOUS +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem + name: (identifier) (def_eq) + statement: (assume_prove + assumption: (new (statement_level) (identifier)) + conclusion: (identifier_ref) + ) + proof: (terminal_proof) + ) +(double_line))) + +===============================||| +Assume/Prove With New Unbound Constant +===============================||| + +---- MODULE Test ---- +THEOREM thm == + ASSUME NEW CONSTANT x + PROVE C +OBVIOUS +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem + name: (identifier) (def_eq) + statement: (assume_prove + assumption: (new (statement_level) (identifier)) + conclusion: (identifier_ref) + ) + proof: (terminal_proof) + ) +(double_line))) + +===============================||| +Assume/Prove With Multiple New Bound Constants +===============================||| + +---- MODULE Test ---- +THEOREM thm == + ASSUME CONSTANT x \in S, CONSTANT y \in S + PROVE C +OBVIOUS +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem + name: (identifier) (def_eq) + statement: (assume_prove + assumption: (new (statement_level) (identifier) (set_in) (identifier_ref)) + assumption: (new (statement_level) (identifier) (set_in) (identifier_ref)) + conclusion: (identifier_ref) + ) + proof: (terminal_proof) + ) +(double_line))) + ===============================||| Assume/Prove With New Operator ===============================||| @@ -105,14 +233,42 @@ OMITTED ) (double_line))) +===============================||| +Assume/Prove with Multiple New Identifiers +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE + ASSUME NEW x, y \in S + PROVE TRUE +==== + +-------------------------------||| + +===============================||| +Assume/Prove with Tupled New Identifiers +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE + ASSUME NEW <> \in S + PROVE TRUE +==== + +-------------------------------||| + ===============================||| Assume/Prove in Suffices Step +:error ===============================||| ---- MODULE Test ---- THEOREM TRUE <1>a. SUFFICES ASSUME CONSTANT x \in S + ASSUME NEW x, y \in S PROVE TRUE <1>b. QED ==== @@ -140,7 +296,7 @@ Assume/Prove with Mixed Assumptions ---- MODULE Test ---- THEOREM thm == ASSUME - NEW f, + NEW CONSTANT f, 1 + 2, /\ 1 /\ 2, @@ -155,7 +311,7 @@ OMITTED (theorem name: (identifier) (def_eq) statement: (assume_prove - assumption: (new (identifier)) + assumption: (new (statement_level) (identifier)) assumption: (bound_infix_op lhs: (nat_number) symbol: (plus) rhs: (nat_number)) assumption: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number))) assumption: (inner_assume_prove diff --git a/test/parser/syntax_corpus/case.txt b/test/parser/syntax_corpus/case.txt index b3ce418f..220c3364 100644 --- a/test/parser/syntax_corpus/case.txt +++ b/test/parser/syntax_corpus/case.txt @@ -11,8 +11,8 @@ op == --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (nat_number) (case_arrow) (nat_number)) (case_box) (case_arm (nat_number) (case_arrow) (nat_number)) @@ -31,8 +31,8 @@ op == CASE 1 -> 2 --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (nat_number) (case_arrow) (nat_number))) ) (double_line))) @@ -50,8 +50,8 @@ op == --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (nat_number) (case_arrow) (case (case_arm (nat_number) (case_arrow) (nat_number)) @@ -75,8 +75,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) @@ -116,8 +116,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number))) @@ -152,8 +152,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) @@ -193,8 +193,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number))) @@ -230,8 +230,8 @@ op == --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) @@ -278,8 +278,8 @@ op3 == -------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (identifier_ref) (case_arrow) (conj_list (conj_item (bullet_conj) (case @@ -292,7 +292,7 @@ op3 == (case_arm (identifier_ref) (case_arrow) (identifier_ref)) ) ) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (identifier_ref) (case_arrow) (conj_list (conj_item (bullet_conj) (case @@ -305,7 +305,7 @@ op3 == (case_arm (identifier_ref) (case_arrow) (identifier_ref)) ) ) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (case (case_arm (identifier_ref) (case_arrow) (conj_list (conj_item (bullet_conj) diff --git a/test/parser/syntax_corpus/conjlist.txt b/test/parser/syntax_corpus/conjlist.txt index 967a6974..353e0171 100644 --- a/test/parser/syntax_corpus/conjlist.txt +++ b/test/parser/syntax_corpus/conjlist.txt @@ -10,8 +10,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -30,8 +30,8 @@ op == /\ 1 -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -51,8 +51,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -72,12 +72,12 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (conj_list (conj_item (bullet_conj) (nat_number))) - (land) - (nat_number) + lhs: (conj_list (conj_item (bullet_conj) (nat_number))) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -94,15 +94,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (bound_infix_op - (nat_number) - (land) - (nat_number) + lhs: (nat_number) + symbol: (land) + rhs: (nat_number) ) ) ) @@ -122,8 +122,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -145,8 +145,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -167,8 +167,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) @@ -195,8 +195,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (conj_list @@ -222,15 +222,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (bound_infix_op - (nat_number) - (plus) - (nat_number) + lhs: (nat_number) + symbol: (plus) + rhs: (nat_number) ) ) (conj_item (bullet_conj) (nat_number)) @@ -251,15 +251,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (bound_infix_op - (nat_number) - (slash) - (nat_number) + lhs: (nat_number) + symbol: (slash) + rhs: (nat_number) ) ) (conj_item (bullet_conj) (nat_number)) @@ -280,16 +280,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (bound_infix_op - (conj_list (conj_item (bullet_conj) (nat_number))) - (plus) - (nat_number) + lhs: (bound_infix_op + lhs: (conj_list (conj_item (bullet_conj) (nat_number))) + symbol: (plus) + rhs: (nat_number) ) - (land) - (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -307,16 +307,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (bound_infix_op - (conj_list (conj_item (bullet_conj) (nat_number))) - (slash) - (nat_number) + lhs: (bound_infix_op + lhs: (conj_list (conj_item (bullet_conj) (nat_number))) + symbol: (slash) + rhs: (nat_number) ) - (land) - (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -331,12 +331,12 @@ op == 1 /\ 2 -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (nat_number) - (land) - (nat_number) + lhs: (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -353,8 +353,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (parentheses (nat_number))) (conj_item (bullet_conj) (parentheses (nat_number))) @@ -375,14 +375,14 @@ op == ( -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (parentheses + lhs: (parentheses (conj_list (conj_item (bullet_conj) (nat_number))) ) - (land) - (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -402,10 +402,10 @@ op == ( -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (parentheses + lhs: (parentheses (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item @@ -417,8 +417,8 @@ op == ( ) ) ) - (land) - (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -440,8 +440,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item @@ -450,9 +450,9 @@ op == (conj_item (bullet_conj) (bound_infix_op - (nat_number) - (plus) - (parentheses + lhs: (nat_number) + symbol: (plus) + rhs: (parentheses (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -479,8 +479,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -522,36 +522,36 @@ op5 == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) ) (assumption (identifier_ref)) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) ) (local_definition (instance (identifier_ref))) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) ) (single_line) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) ) - (module (header_line) (identifier) (header_line) (double_line)) - (operator_definition (identifier) (def_eq) + (module (header_line) name: (identifier) (header_line) (double_line)) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) @@ -572,8 +572,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (tuple_literal (langle_bracket) (rangle_bracket))) @@ -593,8 +593,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (finite_set_literal)) diff --git a/test/parser/syntax_corpus/disjlist.txt b/test/parser/syntax_corpus/disjlist.txt index aad910e0..16b9b5ca 100644 --- a/test/parser/syntax_corpus/disjlist.txt +++ b/test/parser/syntax_corpus/disjlist.txt @@ -10,8 +10,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -30,8 +30,8 @@ op == \/ 1 -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -51,8 +51,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -72,12 +72,12 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (disj_list (disj_item (bullet_disj) (nat_number))) - (lor) - (nat_number) + lhs: (disj_list (disj_item (bullet_disj) (nat_number))) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -94,15 +94,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (bound_infix_op - (nat_number) - (lor) - (nat_number) + lhs: (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) ) @@ -122,8 +122,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -145,8 +145,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -167,8 +167,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) @@ -195,8 +195,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (disj_list @@ -222,15 +222,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (bound_infix_op - (nat_number) - (plus) - (nat_number) + lhs: (nat_number) + symbol: (plus) + rhs: (nat_number) ) ) (disj_item (bullet_disj) (nat_number)) @@ -251,15 +251,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (bound_infix_op - (nat_number) - (slash) - (nat_number) + lhs: (nat_number) + symbol: (slash) + rhs: (nat_number) ) ) (disj_item (bullet_disj) (nat_number)) @@ -280,16 +280,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (bound_infix_op - (disj_list (disj_item (bullet_disj) (nat_number))) - (plus) - (nat_number) + lhs: (bound_infix_op + lhs: (disj_list (disj_item (bullet_disj) (nat_number))) + symbol: (plus) + rhs: (nat_number) ) - (lor) - (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -307,16 +307,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (bound_infix_op - (disj_list (disj_item (bullet_disj) (nat_number))) - (slash) - (nat_number) + lhs: (bound_infix_op + lhs: (disj_list (disj_item (bullet_disj) (nat_number))) + symbol: (slash) + rhs: (nat_number) ) - (lor) - (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -331,12 +331,12 @@ op == 1 \/ 2 -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (nat_number) - (lor) - (nat_number) + lhs: (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -353,8 +353,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (parentheses (nat_number))) (disj_item (bullet_disj) (parentheses (nat_number))) @@ -375,14 +375,14 @@ op == ( -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (parentheses + lhs: (parentheses (disj_list (disj_item (bullet_disj) (nat_number))) ) - (lor) - (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -402,10 +402,10 @@ op == ( -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (parentheses + lhs: (parentheses (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item @@ -417,8 +417,8 @@ op == ( ) ) ) - (lor) - (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -440,8 +440,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item @@ -450,9 +450,9 @@ op == (disj_item (bullet_disj) (bound_infix_op - (nat_number) - (plus) - (parentheses + lhs: (nat_number) + symbol: (plus) + rhs: (parentheses (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -479,8 +479,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -522,36 +522,36 @@ op5 == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) ) (assumption (identifier_ref)) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) ) (local_definition (instance (identifier_ref))) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) ) (single_line) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) ) - (module (header_line) (identifier) (header_line) (double_line)) - (operator_definition (identifier) (def_eq) + (module (header_line) name: (identifier) (header_line) (double_line)) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) @@ -572,8 +572,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (tuple_literal (langle_bracket) (rangle_bracket))) @@ -593,8 +593,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (finite_set_literal)) diff --git a/test/parser/syntax_corpus/except.txt b/test/parser/syntax_corpus/except.txt index 3d8d8e2c..34eb4975 100644 --- a/test/parser/syntax_corpus/except.txt +++ b/test/parser/syntax_corpus/except.txt @@ -10,17 +10,115 @@ r == [a EXCEPT ![2] = "a"] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: - (except - expr_to_update: (identifier_ref) + definition: + (except + expr_to_update: (identifier_ref) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_fn_appl (nat_number))) new_val: (string)) )) (double_line))) +=============||| +Record Update with Multiple Parameters +=============||| + +---- MODULE Test ---- +r == [f EXCEPT ![1, 1] = 0] +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: + (except + expr_to_update: (identifier_ref) + (except_update + update_specifier: + (except_update_specifier + (except_update_fn_appl (nat_number) (nat_number))) + new_val: (nat_number)) + )) +(double_line))) + +=============||| +Record Update with Multi-Value Tuple Parameter +=============||| + +---- MODULE Test ---- +r == [f EXCEPT ![<<1, 1>>] = 0] +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: + (except + expr_to_update: (identifier_ref) + (except_update + update_specifier: + (except_update_specifier + (except_update_fn_appl (tuple_literal (langle_bracket) + (nat_number) (nat_number) + (rangle_bracket)))) + new_val: (nat_number)) + )) +(double_line))) + +=============||| +Record Update with Single-Value Tuple Parameter +=============||| + +---- MODULE Test ---- +r == [f EXCEPT ![<<1>>] = 0] +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: + (except + expr_to_update: (identifier_ref) + (except_update + update_specifier: + (except_update_specifier + (except_update_fn_appl (tuple_literal (langle_bracket) + (nat_number) + (rangle_bracket)))) + new_val: (nat_number)) + )) +(double_line))) + +=============||| +Record Update with Tuple and Non-Tuple Parameters +=============||| + +---- MODULE Test ---- +r == [f EXCEPT ![<<1, 1>>, 1] = 0] +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: + (except + expr_to_update: (identifier_ref) + (except_update + update_specifier: + (except_update_specifier + (except_update_fn_appl + (tuple_literal (langle_bracket) (nat_number)(nat_number) (rangle_bracket)) + (nat_number))) + new_val: (nat_number)) + )) +(double_line))) + =============||| Single nested record update =============||| @@ -33,8 +131,8 @@ r == [a EXCEPT ![2]["a"][3] = @ + 1] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: (except - expr_to_update: (identifier_ref) + definition: (except + expr_to_update: (identifier_ref) (except_update update_specifier: (except_update_specifier (except_update_fn_appl (nat_number)) @@ -59,11 +157,11 @@ r == [a EXCEPT !.x.y.z = "b"] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: - (except - expr_to_update: (identifier_ref) + definition: + (except + expr_to_update: (identifier_ref) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_record_field (identifier_ref)) (except_update_record_field (identifier_ref)) @@ -84,24 +182,24 @@ r == [a EXCEPT ![2]["a"][3] = @, !["b"][x] = 5, ![y][z] = "c"] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: - (except - expr_to_update: (identifier_ref) + definition: + (except + expr_to_update: (identifier_ref) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_fn_appl (nat_number)) (except_update_fn_appl (string)) (except_update_fn_appl (nat_number))) new_val: (prev_func_val)) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_fn_appl (string)) (except_update_fn_appl (identifier_ref))) new_val: (nat_number)) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_fn_appl (identifier_ref)) (except_update_fn_appl (identifier_ref))) @@ -121,18 +219,18 @@ r == [a EXCEPT !.a.b.c = @, !.b.x = 5] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: - (except - expr_to_update: (identifier_ref) + definition: + (except + expr_to_update: (identifier_ref) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_record_field (identifier_ref)) (except_update_record_field (identifier_ref)) (except_update_record_field (identifier_ref))) new_val: (prev_func_val)) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_record_field (identifier_ref)) (except_update_record_field (identifier_ref))) @@ -152,18 +250,18 @@ r == [a EXCEPT !.a.b["c"] = "b", ![2].x = @] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: - (except - expr_to_update: (identifier_ref) + definition: + (except + expr_to_update: (identifier_ref) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_record_field (identifier_ref)) (except_update_record_field (identifier_ref)) (except_update_fn_appl (string))) new_val: (string)) (except_update - update_specifier: + update_specifier: (except_update_specifier (except_update_fn_appl (nat_number)) (except_update_record_field (identifier_ref))) diff --git a/test/parser/syntax_corpus/fairness.txt b/test/parser/syntax_corpus/fairness.txt index 50d18fdd..7db093f1 100644 --- a/test/parser/syntax_corpus/fairness.txt +++ b/test/parser/syntax_corpus/fairness.txt @@ -8,8 +8,8 @@ op == WF_(vars)(x) ---------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (fairness (parentheses (identifier_ref)) (identifier_ref)) ) (double_line))) @@ -24,8 +24,8 @@ op == SF_(vars)(x) ---------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (fairness (parentheses (identifier_ref)) (identifier_ref)) ) (double_line))) @@ -40,8 +40,8 @@ op == WF_vars(x) ---------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (fairness (identifier_ref) (identifier_ref)) ) (double_line))) @@ -56,8 +56,8 @@ op == SF_vars(x) ---------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (fairness (identifier_ref) (identifier_ref)) ) (double_line))) diff --git a/test/parser/syntax_corpus/functions.txt b/test/parser/syntax_corpus/functions.txt index 785189ce..0338095b 100644 --- a/test/parser/syntax_corpus/functions.txt +++ b/test/parser/syntax_corpus/functions.txt @@ -6,7 +6,7 @@ Function Definition f[x \in Nat] == x f[x, y \in Nat] == x f[x, y \in Nat, z \in Real] == x -f[x \in [Nat -> (Nat)]] == x +f[x \in [Nat -> Nat]] == x ==== -------------------------------||| @@ -55,7 +55,7 @@ f[x \in [Nat -> (Nat)]] == x intro: (identifier) (set_in) set: (set_of_functions - (nat_number_set) (maps_to) (parentheses (nat_number_set)) + (nat_number_set) (maps_to) (nat_number_set) ) ) (def_eq) @@ -95,8 +95,8 @@ op == -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) @@ -124,11 +124,11 @@ op == [n \in Nat |-> 2*n] (source_file (module (header_line) name: (identifier) (header_line) (operator_definition name: (identifier) (def_eq) - definition: (function_literal - (quantifier_bound intro: (identifier) (set_in) set: (nat_number_set)) - (all_map_to) - (bound_infix_op lhs: (nat_number) symbol: (mul) rhs: (identifier_ref)) - ) + definition: + (function_literal + (quantifier_bound intro: (identifier) (set_in) set: (nat_number_set)) + (all_map_to) + (bound_infix_op lhs: (nat_number) symbol: (mul) rhs: (identifier_ref))) ) (double_line))) @@ -212,8 +212,8 @@ op == [ -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (set_of_functions (conj_list (conj_item (bullet_conj) (identifier_ref)) diff --git a/test/parser/syntax_corpus/if_then_else.txt b/test/parser/syntax_corpus/if_then_else.txt index 69607f29..0dd1f5d5 100644 --- a/test/parser/syntax_corpus/if_then_else.txt +++ b/test/parser/syntax_corpus/if_then_else.txt @@ -8,9 +8,9 @@ op == IF "A" THEN "B" ELSE "C" ------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) - (if_then_else (string) (string) (string)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: + (if_then_else if: (string) then: (string) else: (string)) ) (double_line))) @@ -28,15 +28,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (if_then_else - (nat_number) - (nat_number) - (nat_number) + if: (nat_number) + then: (nat_number) + else: (nat_number) ) ) (conj_item (bullet_conj) (nat_number)) @@ -59,15 +59,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (if_then_else - (conj_list + if: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) - (nat_number) - (nat_number) + then: (nat_number) + else: (nat_number) ) ) (double_line))) @@ -86,15 +86,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (if_then_else - (nat_number) - (nat_number) - (nat_number) + if: (nat_number) + then: (nat_number) + else: (nat_number) ) ) (disj_item (bullet_disj) (nat_number)) @@ -117,15 +117,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (if_then_else - (disj_list + if: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) - (nat_number) - (nat_number) + then: (nat_number) + else: (nat_number) ) ) (double_line))) + diff --git a/test/parser/syntax_corpus/infix_op.txt b/test/parser/syntax_corpus/infix_op.txt index d1660f06..11afc119 100644 --- a/test/parser/syntax_corpus/infix_op.txt +++ b/test/parser/syntax_corpus/infix_op.txt @@ -51,7 +51,6 @@ x \geq y == 27 x \gg y == 28 x > y == 29 x ## y == 30 -x <=> y == 31 x => y == 32 x \in y == 33 x /\ y == 34 @@ -157,7 +156,6 @@ x \wr y == 101 (operator_definition parameter: (identifier) name: (infix_op_symbol (gg)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (gt)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (hashhash)) parameter: (identifier) (def_eq) definition: (nat_number)) - (operator_definition parameter: (identifier) name: (infix_op_symbol (iff)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (implies)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (in)) parameter: (identifier) (def_eq) definition: (nat_number)) (operator_definition parameter: (identifier) name: (infix_op_symbol (land)) parameter: (identifier) (def_eq) definition: (nat_number)) @@ -283,7 +281,6 @@ op( _ \gg _, _ > _, _ ## _, - _ <=> _, _ => _, _ \in _, _ /\ _, @@ -391,7 +388,6 @@ op( parameter: (operator_declaration (placeholder) name: (infix_op_symbol (gg)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (gt)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (hashhash)) (placeholder)) - parameter: (operator_declaration (placeholder) name: (infix_op_symbol (iff)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (implies)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (in)) (placeholder)) parameter: (operator_declaration (placeholder) name: (infix_op_symbol (land)) (placeholder)) @@ -503,7 +499,6 @@ op == { x \gg y, x > y, x ## y, - x <=> y, x => y, x \in y, x /\ y, @@ -613,7 +608,6 @@ op == { (bound_infix_op lhs: (identifier_ref) symbol: (gg) rhs: (identifier_ref)) (bound_infix_op lhs: (identifier_ref) symbol: (gt) rhs: (identifier_ref)) (bound_infix_op lhs: (identifier_ref) symbol: (hashhash) rhs: (identifier_ref)) - (bound_infix_op lhs: (identifier_ref) symbol: (iff) rhs: (identifier_ref)) (bound_infix_op lhs: (identifier_ref) symbol: (implies) rhs: (identifier_ref)) (bound_infix_op lhs: (identifier_ref) symbol: (in) rhs: (identifier_ref)) (bound_infix_op lhs: (identifier_ref) symbol: (land) rhs: (identifier_ref)) @@ -757,7 +751,6 @@ op == f( \gg, >, ##, - <=>, =>, \in, /\, @@ -863,7 +856,6 @@ op == f( parameter: (infix_op_symbol (gg)) parameter: (infix_op_symbol (gt)) parameter: (infix_op_symbol (hashhash)) - parameter: (infix_op_symbol (iff)) parameter: (infix_op_symbol (implies)) parameter: (infix_op_symbol (in)) parameter: (infix_op_symbol (land)) @@ -970,7 +962,6 @@ op == { A!B!\gg(x, y), A!B!>(x, y), A!B!##(x, y), - A!B!<=>(x, y), A!B!=>(x, y), A!B!\in(x, y), A!B!\land(x, y), @@ -1106,8 +1097,6 @@ op == { (bound_nonfix_op symbol: (infix_op_symbol (gt)) (identifier_ref) (identifier_ref))) (prefixed_op prefix: (subexpr_prefix (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref))) op: (bound_nonfix_op symbol: (infix_op_symbol (hashhash)) (identifier_ref) (identifier_ref))) - (prefixed_op prefix: (subexpr_prefix (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref))) op: - (bound_nonfix_op symbol: (infix_op_symbol (iff)) (identifier_ref) (identifier_ref))) (prefixed_op prefix: (subexpr_prefix (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref))) op: (bound_nonfix_op symbol: (infix_op_symbol (implies)) (identifier_ref) (identifier_ref))) (prefixed_op prefix: (subexpr_prefix (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref))) op: @@ -1247,3 +1236,31 @@ op == { )) (double_line))) +=============||| +IFF Disambiguation +=============||| + +---- MODULE Test ---- +x <=> y == 0 +op(_ <=> _) == 0 +op == x <=> y +op == f(<=>) +op == A!B!<=>(x, y) +==== + +-------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition parameter: (identifier) name: (infix_op_symbol (iff)) parameter: (identifier) (def_eq) definition: (nat_number)) + (operator_definition name: (identifier) + parameter: (operator_declaration (placeholder) name: (infix_op_symbol (iff)) (placeholder)) + (def_eq) definition: (nat_number)) + (operator_definition name: (identifier) (def_eq) definition: + (bound_infix_op lhs: (identifier_ref) symbol: (iff) rhs: (identifier_ref))) + (operator_definition name: (identifier) (def_eq) definition: (bound_op name: (identifier_ref) + parameter: (infix_op_symbol (iff)))) + (operator_definition name: (identifier) (def_eq) definition: + (prefixed_op prefix: (subexpr_prefix (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref))) op: + (bound_nonfix_op symbol: (infix_op_symbol (iff)) (identifier_ref) (identifier_ref)))) +(double_line))) + diff --git a/test/parser/syntax_corpus/jlist.txt b/test/parser/syntax_corpus/jlist.txt index 3f44adda..e5db58a6 100644 --- a/test/parser/syntax_corpus/jlist.txt +++ b/test/parser/syntax_corpus/jlist.txt @@ -11,15 +11,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (conj_list + lhs: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) - (lor) - (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) (double_line))) @@ -37,15 +37,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (disj_list + lhs: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) - (land) - (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -68,25 +68,25 @@ opB == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (conj_list + lhs: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) - (lor) - (nat_number) + symbol: (lor) + rhs: (nat_number) ) ) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (bound_infix_op - (disj_list + lhs: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) - (land) - (nat_number) + symbol: (land) + rhs: (nat_number) ) ) (double_line))) @@ -107,8 +107,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) @@ -153,19 +153,31 @@ disj == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list - (conj_item (bullet_conj) (label (identifier) (label_as) (identifier_ref))) - (conj_item (bullet_conj) (bound_infix_op (identifier_ref) (assign) (identifier_ref))) - (conj_item (bullet_conj) (bound_infix_op (identifier_ref) (bnf_rule) (identifier_ref))) + (conj_item (bullet_conj) (label name: (identifier) (label_as) expression: (identifier_ref))) + (conj_item (bullet_conj) (bound_infix_op + lhs: (identifier_ref) + symbol: (assign) + rhs: (identifier_ref))) + (conj_item (bullet_conj) (bound_infix_op + lhs: (identifier_ref) + symbol: (bnf_rule) + rhs: (identifier_ref))) ) ) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (disj_list - (disj_item (bullet_disj) (label (identifier) (label_as) (identifier_ref))) - (disj_item (bullet_disj) (bound_infix_op (identifier_ref) (assign) (identifier_ref))) - (disj_item (bullet_disj) (bound_infix_op (identifier_ref) (bnf_rule) (identifier_ref))) + (disj_item (bullet_disj) (label name: (identifier) (label_as) expression: (identifier_ref))) + (disj_item (bullet_disj) (bound_infix_op + lhs: (identifier_ref) + symbol: (assign) + rhs: (identifier_ref))) + (disj_item (bullet_disj) (bound_infix_op + lhs: (identifier_ref) + symbol: (bnf_rule) + rhs: (identifier_ref))) ) ) (double_line))) diff --git a/test/parser/syntax_corpus/let_in.txt b/test/parser/syntax_corpus/let_in.txt index 877a71d9..6a830f98 100644 --- a/test/parser/syntax_corpus/let_in.txt +++ b/test/parser/syntax_corpus/let_in.txt @@ -12,15 +12,15 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) (let_in (recursive_declaration (operator_declaration (identifier) (placeholder))) - (operator_definition (identifier) (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) (if_then_else - (bound_infix_op (identifier_ref) (leq) (nat_number)) - (nat_number) - (bound_infix_op (identifier_ref) (mul) + if: (bound_infix_op (identifier_ref) (leq) (nat_number)) + then: (nat_number) + else: (bound_infix_op (identifier_ref) (mul) (bound_op (identifier_ref) (bound_infix_op (identifier_ref) (minus) (nat_number)) ) @@ -44,14 +44,14 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (let_in - (operator_definition (identifier) (def_eq) (nat_number)) - (nat_number) + definitions: (operator_definition name: (identifier) (def_eq) definition: (nat_number)) + expression: (nat_number) ) ) (conj_item (bullet_conj) (nat_number)) @@ -71,14 +71,14 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (let_in - (recursive_declaration (identifier)) - (identifier_ref) + definitions: (recursive_declaration (identifier)) + expression: (identifier_ref) ) ) (conj_item (bullet_conj) (identifier_ref)) @@ -98,14 +98,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (let_in - (module_definition (identifier) (def_eq) (instance (identifier_ref))) - (identifier_ref) + definitions: (module_definition + name: (identifier) (def_eq) + definition: (instance (identifier_ref))) + expression: (identifier_ref) ) ) (conj_item (bullet_conj) (identifier_ref)) @@ -128,16 +130,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (let_in - (operator_definition (identifier) (def_eq) + definitions: (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number)) ) ) - (nat_number) + expression: (nat_number) ) ) (double_line))) @@ -154,14 +156,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (let_in - (operator_definition (identifier) (def_eq) (nat_number)) - (nat_number) + definitions: (operator_definition + name: (identifier) (def_eq) + definition: (nat_number)) + expression: (nat_number) ) ) (disj_item (bullet_disj) (nat_number)) @@ -181,8 +185,8 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) (disj_list (disj_item (bullet_disj) @@ -208,14 +212,16 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (disj_list (disj_item (bullet_disj) (let_in - (module_definition (identifier) (def_eq) (instance (identifier_ref))) - (identifier_ref) + definitions: (module_definition + name: (identifier) (def_eq) + definition: (instance (identifier_ref))) + expression: (identifier_ref) ) ) (disj_item (bullet_disj) (identifier_ref)) @@ -238,16 +244,17 @@ op == -------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (let_in - (operator_definition (identifier) (def_eq) - (disj_list + definitions: (operator_definition + name: (identifier) (def_eq) + definition: (disj_list (disj_item (bullet_disj) (nat_number)) (disj_item (bullet_disj) (nat_number)) ) ) - (nat_number) + expression: (nat_number) ) ) (double_line))) diff --git a/test/parser/syntax_corpus/modules.txt b/test/parser/syntax_corpus/modules.txt index ce8868d0..a64e132b 100644 --- a/test/parser/syntax_corpus/modules.txt +++ b/test/parser/syntax_corpus/modules.txt @@ -8,7 +8,7 @@ Single module -------------||| (source_file - (module (header_line) (identifier) (header_line) (double_line)) + (module (header_line) name: (identifier) (header_line) (double_line)) ) =============||| @@ -21,7 +21,7 @@ EXTENDS M1, M2, M3 -------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (extends (identifier_ref) (identifier_ref) (identifier_ref)) (double_line))) @@ -64,9 +64,9 @@ Sequential Nested modules -------------||| (source_file - (module (header_line) (identifier) (header_line) - (module (header_line) (identifier) (header_line) (double_line)) - (module (header_line) (identifier) (header_line) (double_line)) + (module (header_line) name: (identifier) (header_line) + (module (header_line) name: (identifier) (header_line) (double_line)) + (module (header_line) name: (identifier) (header_line) (double_line)) (double_line)) ) diff --git a/test/parser/syntax_corpus/number.txt b/test/parser/syntax_corpus/number.txt index fc74a025..e9289769 100644 --- a/test/parser/syntax_corpus/number.txt +++ b/test/parser/syntax_corpus/number.txt @@ -9,9 +9,9 @@ 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)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (nat_number)) + (operator_definition name: (identifier) (def_eq) definition: (real_number)) (double_line))) ======================||| @@ -29,13 +29,13 @@ op == \H9876543210FEDCBA ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (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))) - (operator_definition (identifier) (def_eq) (octal_number (format) (value))) - (operator_definition (identifier) (def_eq) (hex_number (format) (value))) - (operator_definition (identifier) (def_eq) (hex_number (format) (value))) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (binary_number (format) (value))) + (operator_definition name: (identifier) (def_eq) definition: (binary_number (format) (value))) + (operator_definition name: (identifier) (def_eq) definition: (octal_number (format) (value))) + (operator_definition name: (identifier) (def_eq) definition: (octal_number (format) (value))) + (operator_definition name: (identifier) (def_eq) definition: (hex_number (format) (value))) + (operator_definition name: (identifier) (def_eq) definition: (hex_number (format) (value))) (double_line))) ======================||| @@ -99,6 +99,6 @@ op == .5 ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) (real_number)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (real_number)) (double_line))) diff --git a/test/parser/syntax_corpus/operators.txt b/test/parser/syntax_corpus/operators.txt index 74f55c68..7e3c99f6 100644 --- a/test/parser/syntax_corpus/operators.txt +++ b/test/parser/syntax_corpus/operators.txt @@ -8,9 +8,9 @@ conflicts_with_octal == \o (1,2) --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) - (bound_nonfix_op (infix_op_symbol (circ)) (nat_number) (nat_number)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: + (bound_nonfix_op symbol: (infix_op_symbol (circ)) (nat_number) (nat_number)) ) (double_line))) @@ -26,15 +26,15 @@ op == - 1 - 2 --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_nonfix_op (prefix_op_symbol (negative)) (nat_number)) ) - (operator_definition (identifier) (def_eq) - (bound_prefix_op (negative) (parentheses (nat_number))) + (operator_definition name: (identifier) (def_eq) definition: + (bound_prefix_op symbol: (negative) rhs: (parentheses (nat_number))) ) - (operator_definition (identifier) (def_eq) - (bound_infix_op (bound_prefix_op (negative) (nat_number)) (minus) (nat_number)) + (operator_definition name: (identifier) (def_eq) definition: + (bound_infix_op lhs: (bound_prefix_op symbol: (negative) rhs: (nat_number)) symbol: (minus) rhs: (nat_number)) ) (double_line))) @@ -48,14 +48,14 @@ f(x, g(_, _), _+_, -._, _^+) == x --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) - (identifier) - (operator_declaration (identifier) (placeholder) (placeholder)) - (operator_declaration (placeholder) (infix_op_symbol (plus)) (placeholder)) - (operator_declaration (prefix_op_symbol (negative)) (placeholder)) - (operator_declaration (placeholder) (postfix_op_symbol (sup_plus))) - (def_eq) (identifier_ref)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) + parameter: (identifier) + parameter: (operator_declaration name: (identifier) parameter: (placeholder) parameter: (placeholder)) + parameter: (operator_declaration (placeholder) name: (infix_op_symbol (plus)) (placeholder)) + parameter: (operator_declaration name: (prefix_op_symbol (negative)) (placeholder)) + parameter: (operator_declaration (placeholder) name: (postfix_op_symbol (sup_plus))) + (def_eq) definition: (identifier_ref)) (double_line))) =============||| @@ -87,8 +87,8 @@ op == - (1,2) --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (bound_nonfix_op (infix_op_symbol (minus)) (nat_number) (nat_number)) ) (double_line))) @@ -201,20 +201,20 @@ op == --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (conj_list (conj_item (bullet_conj) - (bound_infix_op (identifier_ref) (map_to) (identifier_ref)) + (bound_infix_op lhs: (identifier_ref) symbol: (map_to) rhs: (identifier_ref)) ) (conj_item (bullet_conj) - (bound_infix_op (identifier_ref) (assign) (identifier_ref)) + (bound_infix_op lhs: (identifier_ref) symbol: (assign) rhs: (identifier_ref)) ) (conj_item (bullet_conj) - (bound_infix_op (identifier_ref) (bnf_rule) (identifier_ref)) + (bound_infix_op lhs: (identifier_ref) symbol: (bnf_rule) rhs: (identifier_ref)) ) (conj_item (bullet_conj) - (label (identifier) (label_as) (identifier_ref)) + (label name: (identifier) (label_as) expression: (identifier_ref)) ) (conj_item (bullet_conj) (identifier_ref)) ) diff --git a/test/parser/syntax_corpus/proofs.txt b/test/parser/syntax_corpus/proofs.txt index 1ae8758d..f0482f48 100644 --- a/test/parser/syntax_corpus/proofs.txt +++ b/test/parser/syntax_corpus/proofs.txt @@ -8,8 +8,8 @@ THEOREM TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean)) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean)) (double_line))) ===============================||| @@ -22,8 +22,8 @@ PROPOSITION x == TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (identifier) (def_eq) (boolean)) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem name: (identifier) (def_eq) statement: (boolean)) (double_line))) ===============================||| @@ -37,8 +37,8 @@ OBVIOUS -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) (terminal_proof)) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (terminal_proof)) (double_line))) ===============================||| @@ -52,8 +52,8 @@ PROOF OBVIOUS -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (identifier) (def_eq) (boolean) (terminal_proof)) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem name: (identifier) (def_eq) statement: (boolean) proof: (terminal_proof)) (double_line))) ===============================||| @@ -67,8 +67,8 @@ PROOF OMITTED -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (identifier) (def_eq) (boolean) (terminal_proof)) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem name: (identifier) (def_eq) statement: (boolean) proof: (terminal_proof)) (double_line))) ===============================||| @@ -82,8 +82,8 @@ PROOF BY DEF > -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (terminal_proof (use_body (use_body_def (infix_op_symbol (gt))) )) @@ -107,8 +107,8 @@ PROOF BY ONLY -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (terminal_proof (use_body (use_body_expr (identifier_ref) @@ -139,8 +139,8 @@ PROOF BY ONLY -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (terminal_proof (use_body (use_body_expr (module_ref (identifier_ref)) @@ -165,8 +165,8 @@ PROOF <1>a QED BY <1>a, <1>b -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (qed_step (proof_step_id (level) (name)) (terminal_proof (use_body (use_body_expr @@ -191,8 +191,8 @@ PROOF -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (boolean))) (qed_step (proof_step_id (level) (name)) @@ -242,11 +242,11 @@ THEOREM TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof - (proof_step (proof_step_id (level) (name)) (definition_proof_step (operator_definition (identifier) (def_eq) (nat_number)))) - (proof_step (proof_step_id (level) (name)) (definition_proof_step (operator_definition (identifier) (def_eq) (nat_number)))) + (proof_step (proof_step_id (level) (name)) (definition_proof_step (operator_definition name: (identifier) (def_eq) definition: (nat_number)))) + (proof_step (proof_step_id (level) (name)) (definition_proof_step (operator_definition name: (identifier) (def_eq) definition: (nat_number)))) (proof_step (proof_step_id (level) (name)) (have_proof_step (nat_number))) (proof_step (proof_step_id (level) (name)) (witness_proof_step (nat_number) (nat_number))) (proof_step (proof_step_id (level) (name)) (take_proof_step (identifier) (identifier) (identifier))) @@ -273,8 +273,8 @@ THEOREM TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (instance (identifier_ref))) (qed_step (proof_step_id (level) (name))) @@ -297,8 +297,12 @@ PROOF -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (bound_infix_op (identifier_ref) (implies) (identifier_ref)) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (bound_infix_op + lhs: (identifier_ref) + symbol: (implies) + rhs: (identifier_ref) + ) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (identifier_ref))) (proof_step (proof_step_id (level) (name)) (suffices_proof_step (identifier_ref) @@ -325,8 +329,8 @@ LEMMA TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) @@ -354,8 +358,8 @@ COROLLARY TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) @@ -386,8 +390,8 @@ PROOF -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number) (non_terminal_proof @@ -423,8 +427,8 @@ PROOF -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (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))) @@ -467,8 +471,8 @@ PROOF -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (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))) @@ -510,8 +514,8 @@ COROLLARY TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (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) (non_terminal_proof @@ -545,8 +549,8 @@ THEOREM TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number))) (qed_step (proof_step_id (level) (name))) @@ -568,8 +572,8 @@ THEOREM TRUE -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (nat_number) (non_terminal_proof @@ -611,8 +615,8 @@ THEOREM TRUE ------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) (non_terminal_proof +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (conj_list (conj_item (bullet_conj) (nat_number)) @@ -671,8 +675,8 @@ THEOREM TRUE ------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (theorem (boolean) (non_terminal_proof +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: (non_terminal_proof (proof_step (proof_step_id (level) (name)) (suffices_proof_step (conj_list (conj_item (bullet_conj) (nat_number)) @@ -705,3 +709,398 @@ PROOF ------------------------------||| +===============================||| +Take Proof Steps +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> TAKE x +<1> TAKE x, y, z +<1> TAKE x \in S +<1> TAKE x, y, z \in S +<1> TAKE x \in S, y \in S, z \in S +<1> TAKE u, v, w \in S, x, y \in S, z \in S +<1> QED +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (take_proof_step + (identifier) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (identifier) (identifier) (identifier) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound + intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (identifier_ref)) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound + intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + (quantifier_bound + intro: (identifier) + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + (quantifier_bound + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + )) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Take Proof Steps With Tuples +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> TAKE <> \in S +<1> TAKE <> \in S +<1> TAKE <> \in S, <> \in S +<1> QED +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref)) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref)) + )) + (proof_step (proof_step_id (level) (name)) (take_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + )) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Pick Proof Steps +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> PICK x : TRUE +<1> PICK x, y, z : TRUE +<1> PICK x \in S : TRUE +<1> PICK x, y, z \in S : TRUE +<1> PICK x \in S, y \in S, z \in S : TRUE +<1> PICK u, v, w \in S, x, y \in S, z \in S : TRUE +<1> QED +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (identifier) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (identifier) (identifier) (identifier) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound + intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + (quantifier_bound intro: (identifier) (set_in) set: (identifier_ref)) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound + intro: (identifier) + intro: (identifier) + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + (quantifier_bound + intro: (identifier) + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + (quantifier_bound + intro: (identifier) + (set_in) + set: (identifier_ref) + ) + (boolean) + )) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Pick Proof Steps With Tuples +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> PICK <> \in S : TRUE +<1> PICK <> \in S : TRUE +<1> PICK <> \in S, <> \in S : TRUE +<1> QED +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + (boolean) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) + (identifier) + (identifier) + (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + (boolean) + )) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Proof Steps With Terminal Proofs +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> SUFFICES TRUE OBVIOUS +<1> TRUE OBVIOUS +<1> CASE TRUE OBVIOUS +<1> PICK x : TRUE OBVIOUS +<1> PICK <> \in S : TRUE OBVIOUS +<1> QED +==== + +-------------------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (theorem statement: (boolean) proof: + (non_terminal_proof + (proof_step (proof_step_id (level) (name)) (suffices_proof_step + (boolean) (terminal_proof) + )) + (proof_step (proof_step_id (level) (name)) (suffices_proof_step + (boolean) (terminal_proof) + )) + (proof_step (proof_step_id (level) (name)) (case_proof_step + (boolean) (terminal_proof) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (identifier) (boolean) (terminal_proof) + )) + (proof_step (proof_step_id (level) (name)) (pick_proof_step + (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) (identifier) (rangle_bracket)) + (set_in) + set: (identifier_ref) + ) + (boolean) (terminal_proof) + )) + (qed_step (proof_step_id (level) (name))) + ) + ) +(double_line))) + +===============================||| +Use Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> USE TRUE OBVIOUS +<1> QED +==== + +-------------------------------||| + +===============================||| +Hide Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> HIDE TRUE OBVIOUS +<1> QED +==== + +-------------------------------||| + +===============================||| +Define Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> x == TRUE OBVIOUS +<1> QED +==== + +-------------------------------||| + +===============================||| +Have Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> HAVE TRUE OBVIOUS +<1> QED +==== + +-------------------------------||| + +===============================||| +Witness Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> WITNESS TRUE OBVIOUS +<1> QED +==== + +-------------------------------||| + +===============================||| +Take Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> TAKE x OBVIOUS +<1> QED +==== + +-------------------------------||| + +===============================||| +Take Tuple Proof Step With Disallowed Terminal Proof +:error +===============================||| + +---- MODULE Test ---- +THEOREM TRUE +<1> TAKE <> \in S OBVIOUS +<1> QED +==== + +-------------------------------||| + diff --git a/test/parser/syntax_corpus/quantification.txt b/test/parser/syntax_corpus/quantification.txt index b230287b..c67b5fae 100644 --- a/test/parser/syntax_corpus/quantification.txt +++ b/test/parser/syntax_corpus/quantification.txt @@ -377,3 +377,92 @@ op == CHOOSE <> : FALSE ) ) (double_line))) + +==============================||| +Bounded CHOOSE with Multiple Identifiers +:error +==============================||| + +---- MODULE Test ---- +op == CHOOSE x, y \in S : TRUE +==== + +------------------------------||| + +==============================||| +Bounded Tuple CHOOSE with Multiple Identifiers +:error +==============================||| + +---- MODULE Test ---- +op == CHOOSE <>, <> \in S : TRUE +==== + +------------------------------||| + +==============================||| +Unbounded CHOOSE with Multiple Identifiers +:error +==============================||| + +---- MODULE Test ---- +op == CHOOSE x, y : TRUE +==== + +------------------------------||| + +==============================||| +Unbounded Tuple CHOOSE with Multiple Identifiers +:error +==============================||| + +---- MODULE Test ---- +op == CHOOSE <>, <> : TRUE +==== + +------------------------------||| + +==============================||| +Quantifier with Mixed Tuples and Standalone Identifiers +:error +==============================||| + +---- MODULE Test ---- +op == \A x, <>, z \in S : FALSE +==== + +------------------------------||| + +==============================||| +Quantifier with Multiple Tuples for Single Bound +:error +==============================||| + +---- MODULE Test ---- +op == \A <>, <> \in S : FALSE +==== + +------------------------------||| + +==============================||| +Mixed Bounded and Unbounded Quantifiers +:error +==============================||| + +---- MODULE Test ---- +op == \A x, y \in S, z : FALSE +==== + +------------------------------||| + +==============================||| +Quantifiers with Unbounded Tuple +:error +==============================||| + +---- MODULE Test ---- +op == \A <> : FALSE +==== + +------------------------------||| + diff --git a/test/parser/syntax_corpus/recursive.txt b/test/parser/syntax_corpus/recursive.txt index 31de4ba2..11c12624 100644 --- a/test/parser/syntax_corpus/recursive.txt +++ b/test/parser/syntax_corpus/recursive.txt @@ -8,8 +8,13 @@ RECURSIVE f(_) -------------||| -(source_file (module (header_line) (identifier) (header_line) - (recursive_declaration (operator_declaration (identifier) (placeholder))) +(source_file (module (header_line) name: (identifier) (header_line) + (recursive_declaration + (operator_declaration + name: (identifier) + parameter: (placeholder) + ) + ) (double_line))) =============||| @@ -40,8 +45,8 @@ RECURSIVE f -------------||| -(source_file (module (header_line) (identifier) (header_line) - (recursive_declaration (identifier)) +(source_file (module (header_line) name: (identifier) (header_line) + (recursive_declaration name: (identifier)) (double_line))) =============||| @@ -54,10 +59,10 @@ RECURSIVE f(_), g(_) -------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (recursive_declaration - (operator_declaration (identifier) (placeholder)) - (operator_declaration (identifier) (placeholder)) + (operator_declaration name: (identifier) parameter: (placeholder)) + (operator_declaration name: (identifier) parameter: (placeholder)) ) (double_line))) @@ -71,14 +76,14 @@ RECURSIVE f(_), g, h(_, _, _), _+_, -. _, _ ^+ -------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (recursive_declaration - (operator_declaration (identifier) (placeholder)) - (identifier) - (operator_declaration (identifier) (placeholder) (placeholder) (placeholder)) - (operator_declaration (placeholder) (infix_op_symbol (plus)) (placeholder)) - (operator_declaration (prefix_op_symbol (negative)) (placeholder)) - (operator_declaration (placeholder) (postfix_op_symbol (sup_plus))) + (operator_declaration name: (identifier) parameter: (placeholder)) + name: (identifier) + (operator_declaration name: (identifier) parameter: (placeholder) parameter: (placeholder) parameter: (placeholder)) + (operator_declaration (placeholder) name: (infix_op_symbol (plus)) (placeholder)) + (operator_declaration name: (prefix_op_symbol (negative)) (placeholder)) + (operator_declaration (placeholder) name: (postfix_op_symbol (sup_plus))) ) (double_line))) diff --git a/test/parser/syntax_corpus/sets.txt b/test/parser/syntax_corpus/sets.txt index 7c445da6..b3b4847a 100644 --- a/test/parser/syntax_corpus/sets.txt +++ b/test/parser/syntax_corpus/sets.txt @@ -8,8 +8,8 @@ op == { } ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (finite_set_literal) ) (double_line))) @@ -228,6 +228,29 @@ op == {<> \in Nat \X Int \X Real : P(x, y, z)} ) (double_line))) +======================||| +Set Filter with Single Element Tuple +======================||| + +---- MODULE Test ---- +op == {<> \in Nat : P(x, y, z)} +==== + +----------------------||| + +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) + definition: (set_filter + generator: (quantifier_bound + intro: (tuple_of_identifiers (langle_bracket) (identifier) (rangle_bracket)) + (set_in) + set: (nat_number_set) + ) + filter: (bound_op name: (identifier_ref) parameter: (identifier_ref) parameter: (identifier_ref) parameter: (identifier_ref)) + ) + ) +(double_line))) + =====================||| Set Filter Precedence =====================||| @@ -270,18 +293,18 @@ op == { ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (set_filter - (quantifier_bound - (identifier) (set_in) - (conj_list + generator: (quantifier_bound + intro: (identifier) (set_in) + set: (conj_list (conj_item (bullet_conj) (identifier_ref)) (conj_item (bullet_conj) (identifier_ref)) (conj_item (bullet_conj) (identifier_ref)) ) ) - (conj_list + filter: (conj_list (conj_item (bullet_conj) (identifier_ref)) (conj_item (bullet_conj) (identifier_ref)) (conj_item (bullet_conj) (identifier_ref)) diff --git a/test/parser/syntax_corpus/step_expressions.txt b/test/parser/syntax_corpus/step_expressions.txt index f1fb3b41..215ddaa6 100644 --- a/test/parser/syntax_corpus/step_expressions.txt +++ b/test/parser/syntax_corpus/step_expressions.txt @@ -8,8 +8,8 @@ op == [A]_<> --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (step_expr_or_stutter (identifier_ref) (tuple_literal (langle_bracket) (identifier_ref) (identifier_ref) (identifier_ref) (rangle_bracket)) @@ -27,8 +27,8 @@ op == <>_<> --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (step_expr_no_stutter (langle_bracket) (identifier_ref) @@ -82,14 +82,14 @@ op == << --------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (step_expr_or_stutter (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number))) (identifier_ref) ) ) - (operator_definition (identifier) (def_eq) + (operator_definition name: (identifier) (def_eq) definition: (step_expr_no_stutter (langle_bracket) (conj_list (conj_item (bullet_conj) (nat_number)) (conj_item (bullet_conj) (nat_number))) diff --git a/test/parser/syntax_corpus/string.txt b/test/parser/syntax_corpus/string.txt index 1b28d761..4079d988 100644 --- a/test/parser/syntax_corpus/string.txt +++ b/test/parser/syntax_corpus/string.txt @@ -8,8 +8,8 @@ op == "Hello, world!" ------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) (string)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (string)) (double_line))) ==================||| @@ -22,8 +22,8 @@ op == "The cow goes \"moo\", the chicken goes \"cluck cluck\"" ------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (string (escape_char) (escape_char) @@ -43,8 +43,8 @@ op == <<"/\\", "\\/">> ------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (tuple_literal (langle_bracket) (string (escape_char)) (string (escape_char)) @@ -62,17 +62,9 @@ op == "\*" ------------------||| -(source_file - (module - (header_line) - (identifier) - (header_line) - (operator_definition - (identifier) - (def_eq) - (string - (escape_char))) - (double_line))) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (string (escape_char))) +(double_line))) ==================||| String with block comment start @@ -84,16 +76,9 @@ op == "(*" ------------------||| -(source_file - (module - (header_line) - (identifier) - (header_line) - (operator_definition - (identifier) - (def_eq) - (string)) - (double_line))) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (string)) +(double_line))) ==================||| String Set @@ -142,7 +127,7 @@ op == "foo ` bar" ------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) (string)) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (string)) (double_line))) diff --git a/test/parser/syntax_corpus/subexpressions.txt b/test/parser/syntax_corpus/subexpressions.txt index c463dd00..57e25f42 100644 --- a/test/parser/syntax_corpus/subexpressions.txt +++ b/test/parser/syntax_corpus/subexpressions.txt @@ -8,15 +8,15 @@ op == M!X!Y!Z ------------------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (prefixed_op - (subexpr_prefix + prefix: (subexpr_prefix (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref)) (subexpr_component (identifier_ref)) ) - (identifier_ref) + op: (identifier_ref) ) ) (double_line))) diff --git a/test/parser/syntax_corpus/tuples.txt b/test/parser/syntax_corpus/tuples.txt index b7d47307..18ee8813 100644 --- a/test/parser/syntax_corpus/tuples.txt +++ b/test/parser/syntax_corpus/tuples.txt @@ -8,8 +8,8 @@ op == <<>> ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (tuple_literal (langle_bracket) (rangle_bracket)) ) (double_line))) @@ -24,8 +24,8 @@ op == <<1, 2, 3, 4, 5>> ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (tuple_literal (langle_bracket) (nat_number) (nat_number) @@ -46,8 +46,8 @@ op == <> ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (tuple_literal (langle_bracket) (identifier_ref) (identifier_ref) @@ -66,8 +66,8 @@ op == <<<>, <>>> ----------------------||| -(source_file (module (header_line) (identifier) (header_line) - (operator_definition (identifier) (def_eq) +(source_file (module (header_line) name: (identifier) (header_line) + (operator_definition name: (identifier) (def_eq) definition: (tuple_literal (langle_bracket) (tuple_literal (langle_bracket) (identifier_ref) diff --git a/test/parser/syntax_corpus/unit.txt b/test/parser/syntax_corpus/unit.txt index a13b2751..f654702d 100644 --- a/test/parser/syntax_corpus/unit.txt +++ b/test/parser/syntax_corpus/unit.txt @@ -9,7 +9,7 @@ VARIABLES x, y, z -------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (variable_declaration (identifier) (identifier) (identifier)) (variable_declaration (identifier) (identifier) (identifier)) (double_line))) @@ -25,13 +25,13 @@ CONSTANTS f(_, _), _+_, -._, _^+ -------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (constant_declaration (identifier) (identifier) (identifier)) (constant_declaration - (operator_declaration (identifier) (placeholder) (placeholder)) - (operator_declaration (placeholder) (infix_op_symbol (plus)) (placeholder)) - (operator_declaration (prefix_op_symbol (negative)) (placeholder)) - (operator_declaration (placeholder) (postfix_op_symbol (sup_plus))) + (operator_declaration name: (identifier) parameter: (placeholder) parameter: (placeholder)) + (operator_declaration (placeholder) name: (infix_op_symbol (plus)) (placeholder)) + (operator_declaration name: (prefix_op_symbol (negative)) (placeholder)) + (operator_declaration (placeholder) name: (postfix_op_symbol (sup_plus))) ) (double_line))) @@ -66,7 +66,7 @@ INSTANCE M WITH -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (instance (identifier_ref) (substitution (identifier_ref) (gets) (conj_list (conj_item (bullet_conj) (nat_number))) @@ -102,7 +102,7 @@ INSTANCE M WITH -------------------------------||| -(source_file (module (header_line) (identifier) (header_line) +(source_file (module (header_line) name: (identifier) (header_line) (instance (identifier_ref) (substitution (identifier_ref) (gets) (identifier_ref)) (substitution (prefix_op_symbol (powerset)) (gets) (identifier_ref)) diff --git a/test/parser/translate_syntax_tree.ml b/test/parser/translate_syntax_tree.ml new file mode 100644 index 00000000..e244d436 --- /dev/null +++ b/test/parser/translate_syntax_tree.ml @@ -0,0 +1,1268 @@ +(** This file contains functionality for translating TLAPM's syntax tree + format into the common TLA+ syntax corpus format, for comparison of + expected with actual parse trees for a given parse input. +*) + +open Sexplib;; +open Tlapm_lib;; + +type field_or_node = + | Field of string * ts_node + | Node of ts_node +and ts_node = { + name : string; + children : field_or_node list; +} + +let leaf_node (name : string) : ts_node = { + name; + children = [] +} + +let leaf (name : string) : field_or_node = Node (leaf_node name) + +let field_leaf (field_name : string) (name : string) : field_or_node = + Field (field_name, leaf_node name) + +let node_list (ls : ts_node list) : field_or_node list = + List.map (fun e -> Node e) ls + +let node_list_map (f : 'a -> ts_node) (ls : 'a list) : field_or_node list = + node_list (List.map f ls) + +let field_list (field : string) (ls : 'a list) : field_or_node list = + List.map (fun e -> Field (field, e)) ls + +let field_list_map (field : string) (f : 'a -> ts_node) (ls : 'a list) : field_or_node list = + field_list field (List.map f ls) + +let rec ts_node_to_sexpr (node : ts_node) : Sexp.t = + let flatten_child (child : field_or_node) : Sexp.t list = + match child with + | Field (name, node) -> [ + Atom (name ^ ":"); + ts_node_to_sexpr node + ] + | Node (node) -> [ts_node_to_sexpr node] + in + Sexp.(List + (Atom node.name :: + List.flatten (List.map flatten_child node.children) + ) + ) + +let rec repeat (count : int) (elem : 't) : 't list = + if count = 0 then [] else elem :: (repeat (count - 1) elem) + +let rec take (count : int) (ls : 't list) : 't list = + if count > (List.length ls) + then failwith (Printf.sprintf "Attempted to take %d elements from list of length %d" count (List.length ls)) + else match count, ls with + | 0, _ -> [] + | n, [] -> failwith (Printf.sprintf "Attempted to take %d elements from empty list" n) + | n, x :: xs -> x :: (take (n - 1) xs) + +let last (ls : 't list) : 't = List.nth ls ((List.length ls) - 1) + +type operator = + | Prefix of string + | Infix of string + | Postfix of string + | ProofStepId + | Named of string + +type op_shape = + | Declaration + | Reference + +(** The standardized test corpus requires counting escaped strings (for syntax + highlighting reasons) so we do a foldl over the characters of the string + determining whether each character was preceded by a backslash, counting + up the number of escaped characters in the string. +*) +let translate_string (str : string) : ts_node = { + name = "string"; + children = + let (_, escape_count) = String.fold_left ( + fun (is_escaped, acc) c -> + match is_escaped, c with + | (true, 't') -> (false, acc + 1) + | (true, 'n') -> (false, acc + 1) + | (true, 'r') -> (false, acc + 1) + | (true, 'f') -> (false, acc + 1) + | (true, '*') -> (false, acc + 1) + | (true, '"') -> (false, acc + 1) + | (true, '\\') -> (false, acc + 1) + | (_, '\\') -> (true, acc) + | _ -> (false, acc) + ) (false, 0) str in + repeat escape_count (leaf "escape_char") +} + +type proof_step_id_parse_state = +| Start +| LessThan +| Level +| Name + +(** Manual parsing function so we don't need to import a regex library. *) +let is_proof_step_id (id : string) : bool = + let is_number (c : char) : bool = + let ord = Char.code c in + 48 <= ord && ord <= 57 + in let is_letter (c : char) : bool = + let ord = Char.code c in + 65 <= ord && ord <= 90 || 97 <= ord && ord <= 122 + in let rec parse_proof_step_id (state : proof_step_id_parse_state) (idx : int) : bool = + if idx < (String.length id) + then let c = String.get id idx + in match state with + | Start -> + if c = '<' + then parse_proof_step_id LessThan (idx + 1) + else false + | LessThan -> + if is_number c + then parse_proof_step_id Level (idx + 1) + else false + | Level -> + if is_number c + then parse_proof_step_id Level (idx + 1) + else if c = '>' then parse_proof_step_id Name (idx + 1) else false + | Name -> + if is_letter c + then parse_proof_step_id Name (idx + 1) + else false + else match state with + | Name -> true + | _ -> false + in parse_proof_step_id Start 0 + +let str_to_op (op_str : string) : operator = + match op_str with + | "~" -> Prefix "lnot" + | "UNION" -> Prefix "union" + | "SUBSET" -> Prefix "powerset" + | "DOMAIN" -> Prefix "domain" + | "-." -> Prefix "negative" + | "ENABLED" -> Prefix "enabled" + | "UNCHANGED" -> Prefix "unchanged" + | "[]" -> Prefix "always" + | "<>" -> Prefix "eventually" + + | "=>" -> Infix "implies" + | "-+->" -> Infix "plus_arrow" + | "\\equiv" -> Infix "equiv" + | "<=>" -> Infix "equiv" + | "~>" -> Infix "leads_to" + | "/\\" -> Infix "land" + | "\\land" -> Infix "land" + | "\\/" -> Infix "lor" + | "\\lor" -> Infix "lor" + | ":=" -> Infix "assign" + | "::=" -> Infix "bnf_rule" + | "=" -> Infix "eq" + | "/=" -> Infix "neq" + | "#" -> Infix "neq" + | "<" -> Infix "lt" + | ">" -> Infix "gt" + | "<=" -> Infix "leq" + | "=<" -> Infix "leq" + | "\\leq" -> Infix "leq" + | ">=" -> Infix "geq" + | "\\geq" -> Infix "geq" + | "\\approx" -> Infix "approx" + | "|-" -> Infix "rs_ttile" + | "|=" -> Infix "rd_ttile" + | "-|" -> Infix "ls_ttile" + | "=|" -> Infix "ld_ttile" + | "\\asymp" -> Infix "asymp" + | "\\cong" -> Infix "cong" + | "\\doteq" -> Infix "doteq" + | "\\gg" -> Infix "gg" + | "\\ll" -> Infix "ll" + | "\\in" -> Infix "in" + | "\\notin" -> Infix "notin" + | "\\prec" -> Infix "prec" + | "\\succ" -> Infix "succ" + | "\\preceq" -> Infix "preceq" + | "\\succeq" -> Infix "succeq" + | "\\propto" -> Infix "propto" + | "\\sim" -> Infix "sim" + | "\\simeq" -> Infix "simeq" + | "\\sqsubset"-> Infix "sqsubset" + | "\\sqsupset"-> Infix "sqsupset" + | "\\sqsubseteq"-> Infix "sqsubseteq" + | "\\sqsupseteq"-> Infix "sqsupseteq" + | "\\subset" -> Infix "subset" + | "\\supset" -> Infix "supset" + | "\\subseteq"-> Infix "subseteq" + | "\\supseteq"-> Infix "supseteq" + | "@@" -> Infix "compose" + | ":>" -> Infix "map_to" + | "<:" -> Infix "map_from" + | "\\" -> Infix "setminus" + | "\\cap" -> Infix "cap" + | "\\intersect"-> Infix "cap" + | "\\cup" -> Infix "cup" + | "\\union" -> Infix "cup" + | ".." -> Infix "dots_2" + | "..." -> Infix "dots_3" + | "+" -> Infix "plus" + | "++" -> Infix "plusplus" + | "\\oplus" -> Infix "oplus" + | "(+)" -> Infix "oplus" + | "\\ominus" -> Infix "ominus" + | "(-)" -> Infix "ominus" + | "%" -> Infix "mod" + | "%%" -> Infix "modmod" + | "|" -> Infix "vert" + | "||" -> Infix "vertvert" + | "-" -> Infix "minus" + | "--" -> Infix "minusminus" + | "&" -> Infix "amp" + | "&&" -> Infix "ampamp" + | "\\odot" -> Infix "odot" + | "(.)" -> Infix "odot" + | "\\oslash" -> Infix "oslash" + | "(/)" -> Infix "oslash" + | "\\otimes" -> Infix "otimes" + | "(\\X)" -> Infix "otimes" + | "*" -> Infix "mul" + | "**" -> Infix "mulmul" + | "/" -> Infix "slash" + | "//" -> Infix "slashslash" + | "\\bigcirc" -> Infix "bigcirc" + | "\\bullet" -> Infix "bullet" + | "\\div" -> Infix "div" + | "\\o" -> Infix "circ" + | "\\circ" -> Infix "circ" + | "\\star" -> Infix "star" + | "!!" -> Infix "excl" + | "##" -> Infix "hashhash" + | "$" -> Infix "dol" + | "$$" -> Infix "doldol" + | "??" -> Infix "qq" + | "\\sqcap" -> Infix "sqcap" + | "\\sqcup" -> Infix "sqcup" + | "\\uplus" -> Infix "uplus" + | "\\times" -> Infix "times" + | "\\X" -> Infix "times" + | "\\wr" -> Infix "wr" + | "\\cdot" -> Infix "cdot" + | "^" -> Infix "pow" + | "^^" -> Infix "powpow" + + | "'" -> Postfix "prime" + | "^+" -> Postfix "sup_plus" + | "^#" -> Postfix "sup_hash" + | "^*" -> Postfix "asterisk" + + | _ -> if is_proof_step_id op_str then ProofStepId else Named op_str + +let translate_proof_step_id (shape : op_shape) : ts_node = { + name = (match shape with + | Reference -> "proof_step_ref" + | Declaration -> "proof_step_id"); + children = [leaf "level"; leaf "name"] +} + +let as_specific_name (shape : op_shape) (id : string) : ts_node = + match id with + | "Nat" -> leaf_node "nat_number_set" + | "Int" -> leaf_node "int_number_set" + | "Real" -> leaf_node "real_number_set" + | "FALSE" -> leaf_node "boolean" + | "TRUE" -> leaf_node "boolean" + | "STRING" -> leaf_node "string_set" + | _ -> leaf_node ( + match shape with + | Declaration -> "identifier" + | Reference -> "identifier_ref" + ) + +let op_to_node (shape : op_shape) (op : operator) : ts_node = + match op with + | Prefix symbol -> {name = "prefix_op_symbol"; children = [leaf symbol]} + | Infix symbol -> {name = "infix_op_symbol"; children = [leaf symbol]} + | Postfix symbol -> {name = "postfix_op_symbol"; children = [leaf symbol]} + | ProofStepId -> translate_proof_step_id shape + | Named name -> as_specific_name shape name + +let as_bound_op (op : Expr.T.expr) : operator = + match op.core with + | Opaque name -> Named name + | _ -> Named "expr_as_bound_op_ph" + +let builtin_to_op (builtin : Builtin.builtin) : operator = + match builtin with + | Nat -> Named "natural_number_set" + | Int -> Named "int_number_set" + | Real -> Named "real_number_set" + | TRUE -> Named "TRUE" + | FALSE -> Named "FALSE" + | BOOLEAN -> Named "BOOLEAN" + | STRING -> Named "STRING" + | UNCHANGED -> Prefix "unchanged" + | ENABLED -> Prefix "enabled" + | SUBSET -> Prefix "powerset" + | UNION -> Prefix "union" + | DOMAIN -> Prefix "domain" + | Neg -> Prefix "lnot" + | Box _ -> Prefix "always" + | Diamond -> Prefix "eventually" + | Plus -> Infix "plus" + | Minus -> Infix "minus" + | Times -> Infix "mul" + | Mem -> Infix "in" + | Notmem -> Infix "notin" + | Implies -> Infix "implies" + | Equiv -> Infix "equiv" + | Conj -> Infix "land" + | Disj -> Infix "lor" + | Eq -> Infix "eq" + | Neq -> Infix "neq" + | Setminus -> Infix "setminus" + | Cap -> Infix "cap" + | Cup -> Infix "cup" + | Subseteq -> Infix "subseteq" + | Leadsto -> Infix "leads_to" + | Cdot -> Infix "cdot" + | Actplus -> Infix "plus_arrow" + | Prime -> Postfix "prime" + | _ -> failwith "Translation failure: unknown built-in operator" + +let translate_operator_declaration (name : string) (arity : int) : ts_node = { + name = "operator_declaration"; + children = + let op = str_to_op name in + let symbol = op_to_node Declaration op in + match op with + | Prefix _ -> [ + Field ("name", symbol); + leaf "placeholder" + ] + | Infix _ -> [ + leaf "placeholder"; + Field ("name", symbol); + leaf "placeholder" + ] + | Postfix _ -> [ + leaf "placeholder"; + Field ("name", symbol); + ] + | Named _ -> (Field ("name", symbol)) :: (repeat arity (field_leaf "parameter" "placeholder")) + | ProofStepId -> failwith "Translation failure: Proof Step ID not allowed as operator declaration" + } + +let translate_extends (tree : Util.hints) : field_or_node list = + match tree with + | [] -> [] + | _ -> [(Node { + name = "extends"; + children = (List.map (fun _ -> leaf "identifier_ref") tree) + })] + +let translate_constant_decl ((name, shape) : (Util.hint * Expr.T.shape)) : field_or_node = + match shape with + | Shape_expr -> leaf "identifier" + | Shape_op arity -> Node (translate_operator_declaration name.core arity) + +let translate_variable_decl (_ : Util.hint) : field_or_node = + leaf "identifier" + +let translate_recursive_decl ((name, shape) : (Util.hint * Expr.T.shape)) : field_or_node = + match shape with + | Shape_expr -> field_leaf "name" "identifier" + | Shape_op arity -> Node (translate_operator_declaration name.core arity) + +let translate_operator_parameter ((name, shape) : Util.hint * Expr.T.shape) : field_or_node = + match shape with + | Shape_expr -> field_leaf "parameter" "identifier" + | Shape_op arity -> Field ("parameter", translate_operator_declaration name.core arity) + +let translate_number (_number : string) (decimal : string) : ts_node = + if String.empty = decimal + then leaf_node "nat_number" + else leaf_node "real_number" + +(** For expressions like \A x, y \in Nat : f(x, y), the first x will have + bound_domain variant Domain with an associated expression corresponding + to the set being enumerated, and the second variable y will have + bound_domain variant Ditto without any associated domain information; + this function regroups these into a list of identifiers underneath a + single set expression. It is different from the unditto function which + clones the set expression into the y variable bound_domain. +*) +let group_bounds (bounds : Expr.T.bound list) : (ts_node list * Expr.T.expr) list = + let (final_groups, _) = List.fold_right (fun ((_, _, domain) : Expr.T.bound) ((groups, partial_group) : ((ts_node list * Expr.T.expr) list) * ts_node list) -> + match domain with + | Ditto -> (groups, leaf_node "identifier" :: partial_group) + | Domain expr -> ((leaf_node "identifier" :: partial_group, expr) :: groups, []) + | No_domain -> failwith "Translation failure: encountered unbounded domain when grouping bounds" + ) bounds ([], []) + in final_groups + +let group_tuple_bounds (bounds : Expr.T.tuply_bound list) : (ts_node list * Expr.T.expr) list = + let (final_groups, _) = List.fold_right (fun ((names, domain) : Expr.T.tuply_bound) ((groups, partial_group) : ((ts_node list * Expr.T.expr) list) * ts_node list) -> + match names, domain with + | (Bound_name _, Ditto) -> (groups, leaf_node "identifier" :: partial_group) + | (Bound_name _, Domain expr) -> ((leaf_node "identifier" :: partial_group, expr) :: groups, []) + | (Bound_names names, Domain expr) -> ( + let tuple = { + name = "tuple_of_identifiers"; + children = List.flatten [ + [leaf "langle_bracket"]; + List.map (fun _ -> leaf "identifier") names; + [leaf "rangle_bracket"]; + ] + } in ([tuple], expr) :: groups, []) + | (Bound_names _, Ditto) -> failwith "Translation failure: combination of multiple bound names and ditto bound is never used" + | (_, No_domain) -> failwith "Translation failure: tuple quantifiers must have a domain; this should not be representable" + ) bounds ([], []) + in final_groups + +(** Translates the substitution component of INSTANCE statements like s <- expr *) +let rec translate_substitution ((hint, expr) : (Util.hint * Expr.T.expr)) : field_or_node = + Node { + name = "substitution"; + children = [ + Node (hint.core |> str_to_op |> op_to_node Reference); + leaf "gets"; + Node (translate_expr expr) + ] + } + +(** Translates statements like INSTANCE M WITH s1 <- e1, s2 <- e2 *) +and translate_instance (instance : Expr.T.instance) : ts_node = { + name = "instance"; + children = List.flatten [ + [leaf "identifier_ref"]; + List.map translate_substitution instance.inst_sub + ] +} + +and translate_cross_product (exprs : Expr.T.expr list) : ts_node = + match exprs with + | [] -> failwith "Translation failure: empty cross product" + | hd :: tl -> List.fold_left ( + fun lhs rhs -> { + name = "bound_infix_op"; + children = [ + Field ("lhs", lhs); + field_leaf "symbol" "times"; + Field ("rhs", translate_expr rhs); + ] + }) (translate_expr hd) tl + + +(** Subexpression selectors. The core difficulty with this translation is + that TLAPM groups the selectors as first_expr :: selectors, while the + output format expects selectors :: final_op. Depending on the nature of + the final op, the output format is either a prefixed_op (if the final op + is an operator) or a subexpression (if the final op is some kind of tree + navigation construct like @ or :). Thus this is quite a complicated + translation, with information being moved multiple levels up or down the + tree. +*) +and translate_subexpression (expr : Expr.T.expr) (selectors : Expr.T.sel list) : ts_node = + if selectors = [] then translate_expr expr else + let translate_subexpression_component (name : string) (args : Expr.T.expr list) : ts_node = + let op = name |> str_to_op in + match args with + (** If no args, then either this is a naked reference to a symbolic op + that ordinarily takes arguments (prefix, infix, or postfix), or it + is a bound operator that takes no arguments. + *) + | [] -> op_to_node Reference op + (** If there are args, then this is either a standard invocation of a + bound operator, or a nonfix invocation of a prefix, infix, or postfix + operator. Ordinarily the TLAPM parse tree does not disambiguate + between nonfix and standard-fix invocations of operators, but here we + know it must be nonfix like +(1, 2) as that is the only way to invoke + these operators when they are defined in other modules imported using + M == INSTANCE ModuleName. + *) + | args -> (match op with + | Named _ -> { + name = "bound_op"; + children = List.flatten [ + [Field ("name", (op_to_node Reference op))]; + List.map (fun arg -> Field ("parameter", (translate_expr arg))) args + ] + } + | _ -> { + name = "bound_nonfix_op"; + children = List.flatten [ + [Field ("symbol", (op_to_node Reference op))]; + node_list_map translate_expr args + ] + } + ) + in let as_wrapped_subexpr_component (component : ts_node) : ts_node = + {name = "subexpr_component"; children = [Node component]} + in let translate_selector ?(wrap_subexpr_component=true) (selector : Expr.T.sel) : ts_node = + match selector with + | Sel_down -> {name = "subexpr_tree_nav"; children = [leaf "colon"]} + | Sel_num _num -> {name = "subexpr_tree_nav"; children = [leaf "child_id"]} + | Sel_left -> {name = "subexpr_tree_nav"; children = [leaf "langle_bracket"]} + | Sel_right -> {name = "subexpr_tree_nav"; children = [leaf "rangle_bracket"]} + | Sel_at -> {name = "subexpr_tree_nav"; children = [leaf "address"]} + | Sel_inst exprs -> {name = "subexpr_tree_nav"; children = [Node {name = "operator_args"; children = node_list_map translate_expr exprs}]} + | Sel_lab (name, args) -> + let component = translate_subexpression_component name args in + if wrap_subexpr_component then as_wrapped_subexpr_component component else component + in let prefix = take (max ((List.length selectors) - 1) 0) selectors in + let final_op = last selectors in + (** The final op decides whether this is a prefixed_op or a subexpression. *) + match final_op with + | Sel_lab (_name, _args) -> { + name = "prefixed_op"; + children = [ + Field ("prefix", { + name = "subexpr_prefix"; + children = List.flatten [ + [Node (as_wrapped_subexpr_component (translate_expr expr))]; + node_list_map translate_selector prefix; + ] + }); + Field ("op", translate_selector ~wrap_subexpr_component:false final_op); + ] + } + | _ -> { + name = "subexpression"; + children = [ + Node { + name = "subexpr_prefix"; + children = List.flatten [ + [let node = translate_expr expr in + if node.name = "proof_step_ref" + then Node node + else Node (as_wrapped_subexpr_component node)]; + node_list_map translate_selector prefix; + ] + }; + Node (translate_selector final_op); + ] + } + +(** Translate conjunction & disjunction lists like + /\ e1 + /\ e2 + /\ e3 +*) +and translate_jlist (bullet : Expr.T.bullet) (juncts : Expr.T.expr list) : ts_node = + let jtype = + match bullet with + | And -> "conj" + | Or -> "disj" + | Refs -> failwith "Translation undefined for 'Refs' jlist bullet type" + in { + name = jtype ^ "_list"; + children = List.map (fun expr -> Node { + name = jtype ^ "_item"; + children = [leaf ("bullet_" ^ jtype); Node (translate_expr expr)] + }) juncts + } + +and translate_quantifier_bound ((names, domain) : (ts_node list * Expr.T.expr)) : ts_node = { + name = "quantifier_bound"; + children = List.flatten [ + field_list "intro" names; + [leaf "set_in"]; + [Field ("set", translate_expr domain)] + ] + } + +and translate_quantifier_bounds (bounds : Expr.T.bound list) : ts_node list = + bounds |> group_bounds |> List.map translate_quantifier_bound + +and translate_tuple_quantifier_bounds (bounds : Expr.T.tuply_bound list) : ts_node list = + bounds |> group_tuple_bounds |> List.map translate_quantifier_bound + +and translate_case_arm (index : int) ((pred, expr) : Expr.T.expr * Expr.T.expr) : field_or_node list = + let case = Node { + name = "case_arm"; + children = [ + Node (translate_expr pred); + leaf "case_arrow"; + Node (translate_expr expr); + ] + } in match index with + | 0 -> [case] + | _ -> [leaf "case_box"; case] + +and translate_default_arm (default : Expr.T.expr option) : field_or_node list = + match default with + | None -> [] + | Some expr -> [ + leaf "case_box"; + Node { + name = "other_arm"; + children = [ + leaf "case_arrow"; + Node (translate_expr expr) + ] + } + ] + +and translate_case (cases : (Expr.T.expr * Expr.T.expr) list) (default : Expr.T.expr option) : ts_node = { + name = "case"; + children = List.flatten [ + List.mapi translate_case_arm cases |> List.flatten; + translate_default_arm default + ] +} + +and translate_bound_op (callee : Expr.T.expr) (args : Expr.T.expr list) : ts_node = + let op : operator = + match callee.core with + | Opaque op -> str_to_op op + | Internal builtin -> builtin_to_op builtin + | _ -> failwith "Translation failure: bound operator callee must be a named operator or built-in" + in match op with + | Prefix op -> { + name = "bound_prefix_op"; + children = [ + field_leaf "symbol" op; + Field ("rhs", translate_expr (List.hd args)) + ] + } + | Infix op -> { + name = "bound_infix_op"; + children = [ + Field ("lhs", translate_expr (List.nth args 0)); + field_leaf "symbol" op; + Field ("rhs", translate_expr (List.nth args 1)); + ] + } + | Postfix op -> { + name = "bound_postfix_op"; + children = [ + Field ("lhs", translate_expr (List.hd args)); + field_leaf "symbol" op; + ] + } + | Named _name -> { + name = "bound_op"; + children = List.flatten [ + [field_leaf "name" "identifier_ref"]; + List.map (fun arg -> Field ("parameter", (translate_expr arg))) args + ] + } + | ProofStepId -> failwith "Translation failure: proof Step ID not allowed as bound operator" + +and translate_lambda (params : (Util.hint * Expr.T.shape) list) (expr : Expr.T.expr) : ts_node = { + name = "lambda"; + children = List.flatten [ + List.map (fun _ -> leaf "identifier") params; + [Node (translate_expr expr)] + ] +} + +and translate_parentheses (expr : Expr.T.expr) (pform : Expr.T.pform) : ts_node = + match pform.core with + | Syntax -> { + name = "parentheses"; + children = [Node (translate_expr expr)] + } + | Nlabel (_label_name, params) -> { + name = "label"; + children = List.flatten [ + [field_leaf "name" "identifier"]; + List.map (fun _ -> field_leaf "parameter" "identifier_ref") params; + [leaf "label_as"]; + [Field ("expression", translate_expr expr)] + ] + } + | Xlabel (_label_name, _indices) -> { + name = "inner_assume_prove"; + children = [leaf "identifier"; leaf "label_as"; Node (translate_expr expr)] + } + +and translate_set_filter (_name : Util.hint) (set : Expr.T.expr) (filter : Expr.T.expr) : ts_node = { + name = "set_filter"; + children = [ + Field ("generator", { + name = "quantifier_bound"; + children = [ + field_leaf "intro" "identifier"; + leaf "set_in"; + Field ("set", translate_expr set); + ] + }); + Field ("filter", translate_expr filter) + ] +} + +and translate_tuple_of_identifiers (names : Util.hint list) : ts_node = { + name = "tuple_of_identifiers"; + children = List.flatten [ + [leaf "langle_bracket"]; + List.map (fun _ -> leaf "identifier") names; + [leaf "rangle_bracket"]; + ] + } + +and translate_tuple_set_filter (names : Util.hint list) (set : Expr.T.expr) (filter : Expr.T.expr) : ts_node = { + name = "set_filter"; + children = [ + Field ("generator", { + name = "quantifier_bound"; + children = [ + Field ("intro", translate_tuple_of_identifiers names); + leaf "set_in"; + Field ("set", translate_expr set) + ] + }); + Field ("filter", translate_expr filter); + ] +} + +and translate_set_map (map : Expr.T.expr) (bounds : Expr.T.bound list) : ts_node = { + name = "set_map"; + children = List.flatten [ + [Field ("map", translate_expr map)]; + field_list "generator" (translate_quantifier_bounds bounds); + ] +} + +and translate_tuple_set_map (map : Expr.T.expr) (bounds : Expr.T.tuply_bound list) : ts_node = + let bounds = Expr.T.unditto_tuply bounds in { + name = "set_map"; + children = List.flatten [ + [Field ("map", translate_expr map)]; + bounds |> translate_tuple_quantifier_bounds |> field_list "generator"; + ] +} + +and is_bound (bounds : Expr.T.bound list) : bool = + List.for_all (fun (_, _, domain) -> match (domain : Expr.T.bound_domain) with | No_domain -> false | _ -> true ) bounds + +and translate_quantification (quantifier : Expr.T.quantifier) (bounds : Expr.T.bound list) (body : Expr.T.expr) : ts_node = + if is_bound bounds then { + name = "bounded_quantification"; + children = List.flatten [ + [field_leaf "quantifier" (match quantifier with | Forall -> "forall" | Exists -> "exists")]; + bounds |> translate_quantifier_bounds |> field_list "bound"; + [Field ("expression", translate_expr body)]; + ] + } else { + name = "unbounded_quantification"; + children = List.flatten [ + [field_leaf "quantifier" (match quantifier with | Forall -> "forall" | Exists -> "exists")]; + List.map (fun _ -> field_leaf "intro" "identifier") bounds; + [Field ("expression", translate_expr body)]; + ] + } + +and translate_tuple_bounded_quantification (quantifier : Expr.T.quantifier) (bounds : Expr.T.tuply_bound list) (body : Expr.T.expr) : ts_node = { + name = "bounded_quantification"; + children = List.flatten [ + [field_leaf "quantifier" (match quantifier with | Forall -> "forall" | Exists -> "exists")]; + bounds |> translate_tuple_quantifier_bounds |> field_list "bound"; + [Field ("expression", translate_expr body)]; + ] +} + +and translate_temporal_quantification (quantifier : Expr.T.quantifier) (names : Util.hints) (body : Expr.T.expr) : ts_node = { + name = "unbounded_quantification"; + children = List.flatten [ + [field_leaf "quantifier" (match quantifier with | Forall -> "temporal_forall" | Exists -> "temporal_exists")]; + List.map (fun _ -> field_leaf "intro" "identifier") names; + [Field ("expression", translate_expr body)]; + ] +} + +and translate_choose (_name : Util.hint) (set : Expr.T.expr option) (body : Expr.T.expr) : ts_node = { + name = "choose"; + children = List.flatten [ + [field_leaf "intro" "identifier"]; + (match set with | Some expr -> [leaf "set_in"; Field ("set", translate_expr expr)] | None -> []); + [Field ("expression", translate_expr body)] + ] +} + +and translate_tuple_choose (names : Util.hint list) (set : Expr.T.expr option) (body : Expr.T.expr) : ts_node = { + name = "choose"; + children = List.flatten [ + [Field ("intro", translate_tuple_of_identifiers names)]; + (match set with | Some expr -> [leaf "set_in"; Field ("set", translate_expr expr)] | None -> []); + [Field ("expression", translate_expr body)] + ] +} + +and translate_step_expr (mode : Expr.T.modal_op) (expr : Expr.T.expr) (sub : Expr.T.expr) : ts_node = + match mode with + | Box -> { + name = "step_expr_or_stutter"; + children = [Node (translate_expr expr); Node (translate_expr sub)] + } + | Dia -> { + name = "step_expr_no_stutter"; + children = [ + leaf "langle_bracket"; + Node (translate_expr expr); + leaf "rangle_bracket_sub"; + Node (translate_expr sub); + ] + } + +and translate_except (fn : Expr.T.expr) (excepts : (Expr.T.expoint list * Expr.T.expr) list) = + let translate_except_update_specifier (except_specifier : Expr.T.expoint) = + match except_specifier with + | Except_dot _record_field_name -> { + name = "except_update_record_field"; + children = [leaf "identifier_ref"] + } + | Except_apply expr -> { + name = "except_update_fn_appl"; + children = [Node (translate_expr expr)] + } + in let translate_except_update ((except_specifiers, new_val) : Expr.T.expoint list * Expr.T.expr) = { + name = "except_update"; + children = [ + Field ("update_specifier", { + name = "except_update_specifier"; + children = node_list_map translate_except_update_specifier except_specifiers + }); + Field ("new_val", translate_expr new_val) + ] + } in { + name = "except"; + children = List.flatten [ + [Field ("expr_to_update", translate_expr fn)]; + node_list_map translate_except_update excepts + ] + } + +and translate_use_body (usable : Proof.T.usable) : ts_node = + let translate_def (def : Proof.T.use_def Property.wrapped) : ts_node = + match def.core with + | Dvar name -> name |> str_to_op |> op_to_node Reference + | Dx _ -> failwith "Translation undefined for 'Dx' use definition" + in { + name = "use_body"; + children = List.flatten [ + (match usable.facts with + | [] -> [] + | facts -> [Node { + name = "use_body_expr"; + children = node_list_map translate_expr facts + }]); + (match usable.defs with + | [] -> [] + | defs -> [Node { + name = "use_body_def"; + children = node_list_map translate_def defs + }]); + ] + } + +and translate_use_or_hide (usable : Proof.T.usable) : ts_node = { + name = "use_or_hide"; + children = [Node (translate_use_body usable)] +} + +(** Top-level translation method for all expression types. *) +and translate_expr (expr : Expr.T.expr) : ts_node = + match expr.core with + | Num (number, decimal) -> translate_number number decimal + | String str -> translate_string str + | Opaque id -> id |> str_to_op |> op_to_node Reference + | Internal internal -> internal |> builtin_to_op |> op_to_node Reference + | List (bullet, juncts) -> translate_jlist bullet juncts + | Product exprs -> translate_cross_product exprs + | Apply (callee, args) -> translate_bound_op callee args + | Parens (expr, pform) -> translate_parentheses expr pform + | Lambda (params, expr) -> translate_lambda params expr + | SetEnum exprs -> {name = "finite_set_literal"; children = node_list_map translate_expr exprs } + | SetSt (name, set, filter) -> translate_set_filter name set filter + | SetStTuply (names, set, filter) -> translate_tuple_set_filter names set filter + | SetOf (map, bounds) -> translate_set_map map bounds + | SetOfTuply (map, bounds) -> translate_tuple_set_map map bounds + | Quant (quantifier, bounds, expr) -> translate_quantification quantifier bounds expr + | QuantTuply (quantifier, bounds, expr) -> translate_tuple_bounded_quantification quantifier bounds expr + | Tquant (quantifier, hints, expr) -> translate_temporal_quantification quantifier hints expr + | Choose (name, set, expr) -> translate_choose name set expr + | ChooseTuply (names, set, expr) -> translate_tuple_choose names set expr + | Except (fn, excepts) -> translate_except fn excepts + | At (_from_except) -> leaf_node "prev_func_val" + | Sub (mode, expr, sub) -> translate_step_expr mode expr sub + | Tsub (mode, expr, sub) -> { + name = "bound_prefix_op"; + children = [ + Field ("symbol", (match mode with | Box -> leaf_node "always" | Dia -> leaf_node "eventually")); + Field ("rhs", translate_step_expr mode expr sub); + ]; + } + | Fair (_op, sub, expr) -> { + name = "fairness"; + children = [ + Node (translate_expr sub); + Node (translate_expr expr); + ] + } + | Arrow (domain, range) -> { + name = "set_of_functions"; + children = [ + Node (translate_expr domain); + leaf "maps_to"; + Node (translate_expr range); + ] + } + | Fcn (bounds, expr) -> { + name = "function_literal"; + children = List.flatten [ + bounds |> translate_quantifier_bounds |> node_list; + [leaf "all_map_to"]; + [Node (translate_expr expr)] + ] + } + | FcnTuply (bounds, expr) -> { + name = "function_literal"; + children = List.flatten [ + bounds |> translate_tuple_quantifier_bounds |> node_list; + [leaf "all_map_to"]; + [Node (translate_expr expr)] + ] + } + | FcnApp (fn_expr, arg_exprs) -> { + name = "function_evaluation"; + children = List.flatten [ + [Node (translate_expr fn_expr)]; + node_list_map translate_expr arg_exprs + ] + } + | Let (definitions, expr) -> { + name = "let_in"; + children = List.flatten [ + field_list_map "definitions" translate_operator_definition definitions; + [Field ("expression", (translate_expr expr))] + ] + } + | Tuple expr_ls -> { + name = "tuple_literal"; + children = [leaf "langle_bracket"] @ (node_list_map translate_expr expr_ls) @ [leaf "rangle_bracket"] + } + | Rect fields -> { + name = "set_of_records"; + children = List.flatten (List.map (fun (_, expr) -> [leaf "identifier"; Node (translate_expr expr)]) fields) + } + | Record fields -> { + name = "record_literal"; + children = List.flatten (List.map (fun (_, expr) -> [leaf "identifier"; leaf "all_map_to"; Node (translate_expr expr)]) fields) + } + | Dot (expr, _) -> { + name = "record_value"; + children = [Node (translate_expr expr); leaf "identifier_ref"] + } + | If (i, t, e) -> { + name = "if_then_else"; + children = [ + Field ("if", translate_expr i); + Field ("then", translate_expr t); + Field ("else", translate_expr e); + ] + } + | Case (cases, other) -> translate_case cases other + | Bang (expr, selectors) -> translate_subexpression expr selectors + | Sequent sequent -> translate_assume_prove sequent + | Ix _ -> failwith "Translation undefined for 'Ix' expression" + | With (_, _) -> failwith "Translation undefined for 'With' expression" + +and translate_operator_definition (defn : Expr.T.defn) : ts_node = + match defn.core with + | Recursive (_name, _shape) -> leaf_node "recursive_ph" + | Operator (name, expr) -> ( + match expr.core with + (* Operators with parameters are represented by a LAMBDA expression. *) + | Lambda (params, expr) -> + let parameter = field_leaf "parameter" "identifier" in + let op = str_to_op name.core in + let opdef = match op with + | Prefix _ -> [Field ("name", op_to_node Declaration op); parameter] + | Infix _ -> [parameter; Field ("name", op_to_node Declaration op); parameter] + | Postfix _ -> [parameter; Field ("name", op_to_node Declaration op)] + | Named _op_name -> Field ("name", op_to_node Declaration op) + :: List.map (fun (param_op_name, shape : Util.hint * Expr.T.shape) -> + match shape with + | Shape_expr -> parameter + | Shape_op arity -> Field ("parameter", translate_operator_declaration param_op_name.core arity) + ) params + | ProofStepId -> failwith "Translation failure: proof Step ID not allowed in operator definition" + in { + name = "operator_definition"; + children = List.flatten [ + opdef; + [leaf "def_eq"]; + [Field ("definition", (translate_expr expr))] + ] + } + (* Function definitions are represented by a function literal. *) + | Fcn (bounds, expr) -> { + name = "function_definition"; + children = List.flatten [ + [field_leaf "name" "identifier"]; + bounds |> translate_quantifier_bounds |> node_list; + [leaf "def_eq"]; + [Field ("definition", translate_expr expr)] + ] + } + (* Operators without parameters are represented by a non-LAMBDA expression. *) + | _ -> { + name = "operator_definition"; + children = [ + Field ("name", (as_specific_name Declaration name.core)); + leaf "def_eq"; + Field ("definition", translate_expr expr) + ] + } + ) + | Instance (_hint, instance) -> { + name = "module_definition"; + children = List.flatten [ + [field_leaf "name" "identifier"]; + [leaf "def_eq"]; + [Field ("definition", (translate_instance instance))]; + ] + } + | Bpragma _ -> assert false + +and translate_assumption (name : Util.hint option) (expr : Expr.T.expr) : field_or_node list = + List.flatten [ + if Option.is_some name then [field_leaf "name" "identifier"; leaf "def_eq"] else []; + [Node (translate_expr expr)] + ] + +and translate_theorem (name : Util.hint option) (sequent : Expr.T.sequent) (_level : int) (proof1 : Proof.T.proof) (_proof2 : Proof.T.proof) (_summary : Module.T.summary) : field_or_node list = + List.flatten [ + if Option.is_some name then [field_leaf "name" "identifier"; leaf "def_eq"] else []; + [Field ("statement", translate_assume_prove sequent)]; + match translate_proof proof1 with + | Some proof -> [Field ("proof", proof)] + | None -> [] + ] + +and translate_assume_prove (sequent : Expr.T.sequent) : ts_node = + let translate_hypothesis (hyp : Expr.T.hyp) : ts_node = + match hyp.core with + | Fresh (name, shape, kind, domain) -> { + name = "new"; + children = List.flatten [ + (match kind with | Unknown -> [] | _ -> [leaf "statement_level"]); + match shape with + | Shape_expr -> leaf "identifier" :: ( + match domain with + | Unbounded -> [] + | Bounded (set, _visibility) -> [leaf "set_in"; Node (translate_expr set)] + ) + | Shape_op arity -> [Node (translate_operator_declaration name.core arity)] + ] + } + | FreshTuply (_hints, _hdom) -> failwith "Translation error: NEW tuples in ASSUME/PROVE blocks are invalid" + (* The Flex variant results from ASSUME NEW VARIABLE x *) + | Flex _name -> {name = "new"; children = [leaf "statement_level"; leaf "identifier"]} + | Defn (_defn, _where, _visiblity, _export) -> failwith "Translation undefined for 'Defn' hypothesis type" + | Fact (expr, _visibility, _time) -> ( + match expr.core with + | Sequent _ -> { + name = "inner_assume_prove"; + children = [Node (translate_expr expr)] + } + | _ -> translate_expr expr + ) + in match Tlapm_lib__Deque.to_list sequent.context with + (* No assumptions; this is a simple expression. *) + | [] -> translate_expr sequent.active + (* This is an ASSUME/PROVE statement with multiple assumptions. *) + | hypotheses -> { + name = "assume_prove"; + children = List.append + (field_list_map "assumption" translate_hypothesis hypotheses) + [Field ("conclusion", translate_expr sequent.active)] + } + +and translate_suffices_proof_step (sequent : Expr.T.sequent) (proof : Proof.T.proof) : ts_node = { + name = "suffices_proof_step"; + children = List.flatten [ + [Node (translate_assume_prove sequent)]; + match translate_proof proof with + | Some node -> [Node node] + | None -> [] + ] +} + +and translate_define_proof_step (definitions : Expr.T.defn list) : ts_node = { + name = "definition_proof_step"; + children = node_list_map translate_operator_definition definitions +} + +and translate_have_proof_step (expr : Expr.T.expr) : ts_node = { + name = "have_proof_step"; + children = [Node (translate_expr expr)] +} + +and translate_witness_proof_step (exprs : Expr.T.expr list) : ts_node = { + name = "witness_proof_step"; + children = node_list_map translate_expr exprs +} + +and translate_case_proof_step (expr : Expr.T.expr) (proof : Proof.T.proof) : ts_node = { + name = "case_proof_step"; + children = List.flatten [ + [Node (translate_expr expr)]; + match translate_proof proof with + | Some node -> [Node node] + | None -> [] + ] +} + +and translate_take_proof_step (bounds : Expr.T.bounds) : ts_node = { + name = "take_proof_step"; + children = + if is_bound bounds + then bounds |> group_bounds |> node_list_map translate_quantifier_bound + else List.map (fun _ -> leaf "identifier") bounds; +} + +and translate_take_tuple_proof_step (bounds : Expr.T.tuply_bounds) : ts_node = { + name = "take_proof_step"; + children = bounds |> group_tuple_bounds |> node_list_map translate_quantifier_bound +} + +and translate_pick_proof_step (bounds : Expr.T.bounds) (expr : Expr.T.expr) (proof : Proof.T.proof) : ts_node = { + name = "pick_proof_step"; + children = List.flatten [ + if is_bound bounds + then bounds |> group_bounds |> node_list_map translate_quantifier_bound + else List.map (fun _ -> leaf "identifier") bounds; + [Node (translate_expr expr)]; + match translate_proof proof with + | Some node -> [Node node] + | None -> [] + ] +} + +and translate_pick_tuple_proof_step (bounds : Expr.T.tuply_bounds) (expr : Expr.T.expr) (proof : Proof.T.proof) : ts_node = { + name = "pick_proof_step"; + children = List.flatten [ + bounds |> group_tuple_bounds |> node_list_map translate_quantifier_bound; + [Node (translate_expr expr)]; + match translate_proof proof with + | Some node -> [Node node] + | None -> [] + ] +} + +and translate_proof_step (step : Proof.T.step) : ts_node = { + name = "proof_step"; + children = [ + Node (translate_proof_step_id Declaration); + Node (match step.core with + | Suffices (sequent, proof) -> translate_suffices_proof_step sequent proof + | Assert (sequent, proof) -> translate_suffices_proof_step sequent proof + | Use (usable, _visility) -> translate_use_or_hide usable + | Hide usable -> translate_use_or_hide usable + | Define definitions -> translate_define_proof_step definitions + | Have expr -> translate_have_proof_step expr + | Witness exprs -> translate_witness_proof_step exprs + | Take bounds -> translate_take_proof_step bounds + | TakeTuply bounds -> translate_take_tuple_proof_step bounds + | Pcase (expr, proof) -> translate_case_proof_step expr proof + | Pick (bounds, expr, proof) -> translate_pick_proof_step bounds expr proof + | PickTuply (bounds, expr, proof) -> translate_pick_tuple_proof_step bounds expr proof + | Forget _ -> failwith "Translation undefined for 'Forget' proof step type" + )]} + +and translate_qed_step (qed_step : Proof.T.qed_step) : ts_node = { + name = "qed_step"; + children = List.flatten [ + [Node (translate_proof_step_id Declaration)]; + match qed_step.core with + | Qed proof -> ( + match translate_proof proof with + | Some node -> [Node node] + | None -> [] + ) + ] +} + +and translate_non_terminal_proof (steps : Proof.T.step list) (qed_step : Proof.T.qed_step) : ts_node = { + name = "non_terminal_proof"; + children = List.append + (node_list_map translate_proof_step steps) + [Node (translate_qed_step qed_step)] +} + +and translate_proof (proof : Proof.T.proof) : ts_node option = + match proof.core with + | Obvious -> Some (leaf_node "terminal_proof") + | Omitted omission -> ( + match omission with + | Implicit -> None + | Explicit -> Some (leaf_node "terminal_proof") + | Elsewhere _ -> failwith "Translation undefined for 'Elsewhere' Omitted proof type" + ) + | By (usable, _) -> Some { + name = "terminal_proof"; + children = [Node (translate_use_body usable)] + } + | Steps (steps, qed_step) -> Some (translate_non_terminal_proof steps qed_step) + | Error msg -> failwith ("Translation failure: proof type error " ^ msg) + +and translate_module (tree : Module.T.mule) : ts_node = { + name = "module"; + children = List.flatten [ + [leaf "header_line"]; + [field_leaf "name" "identifier"]; + [leaf "header_line"]; + translate_extends tree.core.extendees; + List.map translate_unit tree.core.body; + [leaf "double_line"]; + ] +} + +and translate_unit (unit : Module.T.modunit) : field_or_node = + match unit.core with + | Constants ls -> Node { + name = "constant_declaration"; + children = List.map translate_constant_decl ls + } + | Variables ls -> Node { + name = "variable_declaration"; + children = List.map translate_variable_decl ls + } + | Recursives ls -> Node { + name = "recursive_declaration"; + children = List.map translate_recursive_decl ls + } + | Definition (defn, _visibility, _wheredef, export) -> ( + match export with + | Local -> Node { + name = "local_definition"; + children = [Node (translate_operator_definition defn)] + } + | Export -> Node (translate_operator_definition defn) + ) + | Axiom (hint, expr) -> Node { + name = "assumption"; + children = translate_assumption hint expr + } + | Theorem (hint, sequent, level, proof1, proof2, summary) -> Node { + name = "theorem"; + children = translate_theorem hint sequent level proof1 proof2 summary + } + | Submod mule -> Node (translate_module mule) + | Mutate (`Use _, usable) -> Node (translate_use_or_hide usable) + | Mutate (`Hide, usable) -> Node (translate_use_or_hide usable) + | Anoninst (instance, Local) -> Node { + name = "local_definition"; + children = [Node (translate_instance instance)] + } + | Anoninst (instance, Export) -> Node (translate_instance instance) + +let translate_tla_source_file (tree : Module.T.mule) : ts_node = { + name = "source_file"; + children = [Node (translate_module tree)] + } diff --git a/tlapm.opam b/tlapm.opam index cc5575ee..872eb93f 100644 --- a/tlapm.opam +++ b/tlapm.opam @@ -30,6 +30,7 @@ depends: [ "ocaml" "dune-site" "dune-build-info" + "sexp_diff" "sexplib" "cmdliner" "camlzip"