From 35e94fd4ecd72ad25d9f34cbe53b885429c51631 Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Tue, 23 Apr 2024 15:18:14 -0400 Subject: [PATCH] Properly translate number sets Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- Cargo.toml | 4 ++-- src/lib.rs | 17 +++++++++++++++++ 2 files changed, 19 insertions(+), 2 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 5f89fb3..a8e4bd2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,7 +1,7 @@ [package] name = "tlauc" description = "Rewrites TLA⁺ specs to use Unicode symbols instead of ASCII, and vice-versa" -version = "1.0.0" +version = "1.0.1" authors = ["Andrew Helwer <2n8rn1w1f@mozmail.com>"] repository = "https://github.com/tlaplus-community/tlauc" license = "MIT" @@ -17,7 +17,7 @@ clap = { version = "4.5.4", features = ["derive"] } csv = "1.3.0" serde = { version = "1.0.197", features = ["derive"] } tree-sitter = "0.22.5" -tree-sitter-tlaplus = "1.2.8" +tree-sitter-tlaplus = "1.3.3" [dev-dependencies] glob = "0.3.1" diff --git a/src/lib.rs b/src/lib.rs index 7249e13..16da666 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -804,6 +804,23 @@ op == /\ A ); } + // See https://github.com/tlaplus-community/tlauc/issues/11 + // Test translation of number sets in their three forms: + // 1. As an expression + // 2. As the left-hand-side of an operator definition + // 3. As a reference to an imported module + #[test] + fn test_translate_number_set() { + run_roundtrip_test( + r#" +---- MODULE Test ---- +Nat == Nat \union A!B!Nat +Int == Int \union A!B!Int +Real == Real \union A!B!Real +===="#, + ); + } + // https://github.com/tlaplus-community/tlauc/issues/1 #[ignore] #[test]