diff --git a/.github/scripts/parse_modules.py b/.github/scripts/parse_modules.py index 683e9837..d3ac5b86 100644 --- 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 index 890cef11..0cfc4aab 100644 --- 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)