Simplify import rewrites, expand number of specs successfully parsing

Signed-off-by: Andrew Helwer <[email protected]>
tlaplus · Mar 29, 2024 · 89dc716 · 89dc716
1 parent ac24f7b
commit 89dc716
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 33 deletions.
diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py
@@ -54,19 +54,7 @@ def parse_module(path):
 
 manifest = tla_utils.load_json(manifest_path)
 
-specs_failing_unicode_parsing = [
-    # TLAPS.tla operator null in level-checking
-    'specifications/ewd840',
-    'specifications/sums_even',
-    'specifications/ewd998',
-    'specifications/TwoPhase',
-    'specifications/byzpaxos',
-]
-
 modules_failing_unicode_parsing = [
-    # this.operator null in level-checking
-    'specifications/SpecifyingSystems/Liveness/LiveHourClock.tla',
-    'specifications/SpecifyingSystems/Liveness/MCLiveWriteThroughCache.tla',
     # Unknown operator R
     'specifications/SpecifyingSystems/RealTime/MCRealTime.tla',
     'specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla',
@@ -79,20 +67,11 @@ def parse_module(path):
     'specifications/SpecifyingSystems/Standard/Reals.tla',
     'specifications/SpecifyingSystems/Standard/ProtoReals.tla', # root
     'specifications/SpecifyingSystems/Standard/Peano.tla',
-    # Level-checking of ASSUME
-    'specifications/NanoBlockchain/MCNano.tla',
-    'specifications/NanoBlockchain/Nano.tla', # root
     # PlusCal illegal lexeme
     'specifications/byzpaxos/BPConProof.tla',
     'specifications/byzpaxos/Consensus.tla', # root
     'specifications/byzpaxos/PConProof.tla', # root
     'specifications/byzpaxos/VoteProof.tla',
-    # TLAPS null operator when level-checking
-    'specifications/lamport_mutex/LamportMutex_proofs.tla',
-    'specifications/lamport_mutex/NaturalsInduction.tla',
-    'specifications/lamport_mutex/SequenceTheorems.tla',
-    'specifications/lamport_mutex/WellFoundedInduction.tla',
-    'specifications/lamport_mutex/TLAPS.tla', # root
 ]
 
 # List of all modules to parse and whether they should use TLAPS imports
@@ -101,7 +80,6 @@ def parse_module(path):
     for spec in manifest['specifications']
     for module in spec['modules']
         if normpath(module['path']) not in skip_modules
-        and spec['path'] not in specs_failing_unicode_parsing
         and module['path'] not in modules_failing_unicode_parsing
         and (only_modules == [] or normpath(module['path']) in only_modules)
 ]

diff --git a/.github/scripts/unicode_number_set_shim.py b/.github/scripts/unicode_number_set_shim.py
@@ -68,16 +68,16 @@ def build_imports_query(language):
     Builds query to get import locations for shim insertion.
     """
     queries = [
-        '(extends) @extends',
-        '(instance) @instance'
+        '(extends (identifier_ref) @import)',
+        '(instance (identifier_ref) @import)'
     ]
     return language.query(' '.join(queries))
 
-def node_to_string(module_bytes, node, byte_offset):
+def node_to_string(module_bytes, node):
     """
     Gets the string covered by the given parse tree node.
     """
-    return module_bytes[node.byte_range[0]+byte_offset:node.byte_range[1]+byte_offset].decode('utf-8')
+    return module_bytes[node.byte_range[0]:node.byte_range[1]].decode('utf-8')
 
 def replace_with_shim(module_bytes, node, byte_offset, shim):
     """
@@ -95,16 +95,12 @@ def replace_imports(module_bytes, tree, query):
     Replaces imports with unicode shim version.
     """
     shim_modules = {shim.module : shim for shim in shims}
-    captures = query.captures(tree.root_node)
-    byte_offset = 0
     imported_modules = [
         (imported_module, shim_modules[module_name])
-        for imported_module_set in [
-            node.named_children if 'extends' == capture_name else [node.named_child(0)] # @instance capture
-            for node, capture_name in captures
-        ] for imported_module in imported_module_set
-        if (module_name := node_to_string(module_bytes, imported_module, byte_offset)) in shim_modules
+        for imported_module, _ in query.captures(tree.root_node)
+        if (module_name := node_to_string(module_bytes, imported_module)) in shim_modules
     ]
+    byte_offset = 0
     for imported_module, shim in imported_modules:
         byte_offset = replace_with_shim(module_bytes, imported_module, byte_offset, shim)