Parse all translated unicode specs (#142)

Signed-off-by: Andrew Helwer <[email protected]>

Author: ahelwer

.github/scripts/check_manifest_features.py

@@ -146,13 +146,13 @@ def get_community_imports(examples_root, tree, text, dir, has_proof, queries):
     """
     imports = set(
         [
-            text[node.start_byte:node.end_byte].decode('utf-8')
+            tla_utils.node_to_string(text, node)
             for node, _ in queries.imports.captures(tree.root_node)
         ]
     )
     modules_in_file = set(
         [
-            text[node.start_byte:node.end_byte].decode('utf-8')
+            tla_utils.node_to_string(text, node)
             for node, _ in queries.module_names.captures(tree.root_node)
         ]
     )

.github/scripts/check_markdown_table.py

@@ -180,7 +180,6 @@ def from_json(spec):
     for path, json, md in different_tlc_flag:
         print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a TLC Model flag in README.md table')
 
-'''
 # Ensure Apalache flag is correct
 different_apalache_flag = [
     (manifest_spec.path, manifest_spec.apalache, table_spec.apalache)
@@ -192,7 +191,6 @@ def from_json(spec):
     print('ERROR: Apalache Model flags in README.md table differ from model records in manifest.json:')
     for path, json, md in different_tlc_flag:
         print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' an Apalache Model flag in README.md table')
-'''
 
 if success:
     print('SUCCESS: manifest.json concords with README.md table')

.github/scripts/tla_utils.py

@@ -62,6 +62,12 @@ def parse_module(examples_root, parser, path):
     tree = parser.parse(module_text)
     return (tree, module_text, tree.root_node.has_error)
 
+def node_to_string(module_bytes, node):
+    """
+    Gets the string covered by the given tree-sitter parse tree node.
+    """
+    return module_bytes[node.start_byte:node.end_byte].decode('utf-8')
+
 def parse_timespan(unparsed):
     """
     Parses the timespan format used in the manifest.json format.

.github/scripts/unicode_number_set_shim.py

@@ -75,12 +75,6 @@ def build_imports_query(language):
     ]
     return language.query(' '.join(queries))
 
-def node_to_string(module_bytes, node):
-    """
-    Gets the string covered by the given parse tree node.
-    """
-    return module_bytes[node.byte_range[0]:node.byte_range[1]].decode('utf-8')
-
 def replace_with_shim(module_bytes, node, byte_offset, shim):
     """
     Replace the text covered by the given parse tree node with a reference to
@@ -100,7 +94,7 @@ def replace_imports(module_bytes, tree, query):
     imported_modules = [
         (imported_module, shim_modules[module_name])
         for imported_module, _ in query.captures(tree.root_node)
-        if (module_name := node_to_string(module_bytes, imported_module)) in shim_modules
+        if (module_name := tla_utils.node_to_string(module_bytes, imported_module)) in shim_modules
     ]
     byte_offset = 0
     for imported_module, shim in imported_modules:

.github/workflows/CI.yml

@@ -94,34 +94,17 @@ jobs:
           fi
       - name: Parse all modules
         run: |
-          # Need to have a nonempty list to pass as a skip parameter
-          SKIP=("does/not/exist")
-          if [ ${{ matrix.unicode }} ]; then
-            # These redefine Nat, Int, or Real so cannot be shimmed
-            SKIP+=(
-              "specifications/SpecifyingSystems/Standard/Naturals.tla"
-              "specifications/SpecifyingSystems/Standard/Peano.tla"
-              "specifications/SpecifyingSystems/Standard/Integers.tla"
-              "specifications/SpecifyingSystems/Standard/Reals.tla"
-              "specifications/SpecifyingSystems/Standard/ProtoReals.tla"
-              "specifications/SpecifyingSystems/RealTime/MCRealTime.tla"
-              "specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.tla"
-            )
-          fi
           python $SCRIPT_DIR/parse_modules.py                            \
             --tools_jar_path $DEPS_DIR/tools/tla2tools.jar               \
             --apalache_path $DEPS_DIR/apalache                           \
             --tlapm_lib_path $DEPS_DIR/tlapm/library                     \
             --community_modules_jar_path $DEPS_DIR/community/modules.jar \
-            --manifest_path manifest.json                                \
-            --skip "${SKIP[@]}"
+            --manifest_path manifest.json
       - name: Check small models
         run: |
           # Need to have a nonempty list to pass as a skip parameter
           SKIP=("does/not/exist")
           if [ ${{ matrix.unicode }} ]; then
-            # This redefines Real so cannot be shimmed
-            SKIP+=("specifications/SpecifyingSystems/RealTime/MCRealTimeHourClock.cfg")
             # Apalache does not yet support Unicode
             SKIP+=("specifications/EinsteinRiddle/Einstein.cfg")
           fi