Merge branch 'textual-bump' into kcfg-key

Author: François Guyot

.github/workflows/test-pr.yml

@@ -18,7 +18,7 @@ jobs:
           token: ${{ secrets.JENKINS_GITHUB_PAT }}
           # fetch-depth 0 means deep clone the repo
           fetch-depth: 0
-      - name: 'Update Version'
+      - name: 'Update version'
         run: |
           set -x
           git config user.name devops
@@ -72,29 +72,42 @@ jobs:
   integration-tests:
     needs: code-quality-checks
     name: 'Integration Tests'
-    runs-on: [self-hosted, linux, normal-ephemeral]
+    runs-on: [self-hosted, linux, normal]
     strategy:
       matrix:
         python-version: ['3.10', '3.11']
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
-      - name: 'Install Python'
-        uses: actions/setup-python@v4
-        with:
-          python-version: ${{ matrix.python-version }}
-      - name: 'Install Poetry'
-        uses: Gr1N/setup-poetry@v8
-      - name: 'Install K'
+      - name: 'Build Docker image'
+        run: |
+          COMMIT=$(git rev-parse --short=7 HEAD)
+          K_VERSION=$(cut --delim=v --field=2 deps/k_release)
+
+          docker build .                                            \
+            --build-arg PYTHON_VERSION=${{ matrix.python-version }} \
+            --build-arg K_VERSION=${K_VERSION}                      \
+            --tag runtimeverificationinc/pyk-ci:${COMMIT}
+
+          docker run             \
+            --name pyk-ci        \
+            --rm                 \
+            --interactive        \
+            --tty                \
+            --detach             \
+            --workdir /home/user \
+            runtimeverificationinc/pyk-ci:${COMMIT}
+
+          docker cp . pyk-ci:/home/user
+          docker exec pyk-ci chown -R user:user /home/user
+      - name: 'Set Python version'
+        run: docker exec --user user pyk-ci poetry env use ${{ matrix.python-version }}
+      - name: 'Build and run integration tests'
+        run: docker exec --user user pyk-ci make cov-integration COV_ARGS=-n8
+      - name: 'Tear down Docker container'
+        if: always()
         run: |
-          K_VERSION=$(cat deps/k_release)
-          DEB_PACKAGE_NAME=kframework_${K_VERSION}_amd64_ubuntu_jammy.deb
-          wget https://github.com/runtimeverification/k/releases/download/v${K_VERSION}/${DEB_PACKAGE_NAME}
-          sudo apt-get update
-          sudo apt-get -y install graphviz ./${DEB_PACKAGE_NAME}
-          kompile --version
-      - name: 'Run integration tests'
-        run: make cov-integration COV_ARGS='-n8'
+          docker stop --time=0 pyk-ci
 
   build-on-nix:
     needs: code-quality-checks

.github/workflows/update-version.yml

@@ -0,0 +1,32 @@
+name: 'Update Version'
+on:
+  push:
+    branches:
+      - '_update-deps/runtimeverification/k'
+  workflow_dispatch:
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+
+  update-versions:
+    name: 'Update K Version'
+    runs-on: ubuntu-latest
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          submodules: recursive
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+      - name: 'Configure GitHub user'
+        run: |
+          git config user.name devops
+          git config user.email [email protected]
+      - name: 'Update K version'
+        run: |
+          K_VERSION=$(cat deps/k_release)
+          sed --in-place "s/^K_VERSION: Final = '.*'$/K_VERSION: Final = '${K_VERSION}'/" src/pyk/__init__.py
+          git add --update && git commit -m "Set K Version: ${K_VERSION}" || true
+      - name: 'Push updates'
+        run: git push

Dockerfile

@@ -4,12 +4,12 @@ FROM runtimeverificationinc/kframework-k:ubuntu-${K_DISTRO}-${K_VERSION}
 
 ARG PYTHON_VERSION=3.10
 
-RUN    apt-get -y update             \
-    && apt-get -y install            \
-         curl                        \
-         graphviz                    \
-         python${PYTHON_VERSION}     \
-         python${PYTHON_VERSION}-dev \
+RUN    apt-get -y update           \
+    && apt-get -y install          \
+         curl                      \
+         graphviz                  \
+         python$PYTHON_VERSION     \
+         python$PYTHON_VERSION-dev \
     && apt-get -y clean
 
 RUN    curl -sSL https://install.python-poetry.org | POETRY_HOME=/usr python3 - \

deps/k_release

@@ -1 +1 @@
-5.6.110
+5.6.114

package/version

@@ -1 +1,5 @@
+<<<<<<< HEAD
 0.1.306
+=======
+0.1.318
+>>>>>>> textual-bump

pyproject.toml

@@ -4,7 +4,11 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
+<<<<<<< HEAD
 version = "0.1.306"
+=======
+version = "0.1.318"
+>>>>>>> textual-bump
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -18,7 +22,7 @@ filelock = "^3.9.0"
 graphviz = "^0.20.1"
 psutil = "^5.9.4"
 pybind11 = "^2.10.3"
-textual = "^0.10.1"
+textual = "^0.27.0"
 tomli = "^2.0.1"
 
 [tool.poetry.group.dev.dependencies]
@@ -41,6 +45,7 @@ types-psutil = "^5.9.5.10"
 
 [tool.poetry.scripts]
 pyk = "pyk.__main__:main"
+pyk-covr = "pyk.kcovr:main"
 kbuild = "pyk.kbuild.__main__:main"
 krepl = "pyk.krepl.__main__:main"
 kore-exec-covr = "pyk.kore_exec_covr.__main__:main"

src/pyk/__init__.py

@@ -0,0 +1,9 @@
+from __future__ import annotations
+
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from typing import Final
+
+
+K_VERSION: Final = '5.6.114'

src/pyk/__main__.py

@@ -14,9 +14,10 @@
 from .kast.inner import KInner
 from .kast.manip import flatten_label, minimize_rule, minimize_term, propagate_up_constraints, remove_source_map
 from .kast.outer import read_kast_definition
+from .kast.pretty import PrettyPrinter
 from .kore.parser import KoreParser
 from .kore.syntax import Pattern
-from .ktool.kprint import KPrint, build_symbol_table, pretty_print_kast
+from .ktool.kprint import KPrint
 from .ktool.kprove import KProve
 from .prelude.k import GENERATED_TOP_CELL
 from .prelude.ml import is_top, mlAnd, mlOr
@@ -113,14 +114,14 @@ def exec_graph_imports(args: Namespace) -> None:
 
 def exec_coverage(args: Namespace) -> None:
     kompiled_dir: Path = args.definition_dir
-    json_definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json'))
-    symbol_table = build_symbol_table(json_definition)
+    definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json'))
+    pretty_printer = PrettyPrinter(definition)
     for rid in args.coverage_file:
-        rule = minimize_rule(strip_coverage_logger(get_rule_by_id(json_definition, rid.strip())))
+        rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip())))
         args.output.write('\n\n')
         args.output.write('Rule: ' + rid.strip())
         args.output.write('\nUnparsed:\n')
-        args.output.write(pretty_print_kast(rule, symbol_table))
+        args.output.write(pretty_printer.print(rule))
     _LOGGER.info(f'Wrote file: {args.output.name}')
 
 

src/pyk/kast/manip.py

@@ -37,6 +37,36 @@ def flatten_label(label: str, kast: KInner) -> list[KInner]:
     return [kast]
 
 
+def sort_assoc_label(label: str, kast: KInner) -> KInner:
+    res: KInner | None = None
+    if type(kast) is KApply and kast.label.name == label:
+        terms = sorted(flatten_label(label, kast))
+        for term in reversed(terms):
+            if not res:
+                res = term
+            else:
+                res = kast.label(term, res)
+        assert res is not None
+        return res
+    return kast
+
+
+def sort_ac_collections(definition: KDefinition, kast: KInner) -> KInner:
+    ac_hooks = {'MAP.concat', 'SET.concat', 'BAG.concat'}
+    ac_collections = [
+        prod.klabel.name
+        for prod in definition.productions
+        if prod.klabel is not None and 'hook' in prod.att and prod.att['hook'] in ac_hooks
+    ]
+
+    def _sort_ac_collections(_kast: KInner) -> KInner:
+        if type(_kast) is KApply and _kast.label.name in ac_collections:
+            return sort_assoc_label(_kast.label.name, _kast)
+        return _kast
+
+    return top_down(_sort_ac_collections, kast)
+
+
 def if_ktype(ktype: type[KI], then: Callable[[KI], KInner]) -> Callable[[KInner], KInner]:
     def fun(term: KInner) -> KInner:
         if isinstance(term, ktype):

src/pyk/kast/outer.py

@@ -1078,6 +1078,47 @@ def _compute_subsorts(self, sort: KSort) -> list[KSort]:
                 _subsorts.extend([_subsort] + self.subsorts(prod.items[0].sort))
         return list(set(_subsorts))
 
+    def sort(self, kast: KInner) -> KSort | None:
+        match kast:
+            case KToken(_, sort) | KVariable(_, sort):
+                return sort
+            case KRewrite(lhs, rhs):
+                sort = self.sort(lhs)
+                return sort if sort == self.sort(rhs) else None
+            case KSequence(_):
+                return KSort('K')
+            case KApply(label, _):
+                prod = self.production_for_klabel(label)
+                if prod.sort not in prod.params:
+                    return prod.sort
+                elif len(prod.params) == len(label.params):
+                    param_dict: dict[KSort, KSort] = {}
+                    for pparam, lparam in zip(prod.params, label.params, strict=True):
+                        if pparam not in param_dict:
+                            param_dict[pparam] = lparam
+                        elif param_dict[pparam] != lparam:
+                            return None
+                    if prod.sort in param_dict and param_dict[prod.sort] not in prod.params:
+                        return param_dict[prod.sort]
+                return None
+            case _:
+                return None
+
+    def sort_strict(self, kast: KInner) -> KSort:
+        sort = self.sort(kast)
+        if sort is None:
+            raise ValueError(f'Could not determine sort of term: {kast}')
+        return sort
+
+    def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None:
+        if sort1 == sort2:
+            return sort1
+        if sort1 in self.subsorts(sort2):
+            return sort1
+        if sort2 in self.subsorts(sort1):
+            return sort2
+        return None
+
     def sort_vars_subst(self, kast: KInner) -> Subst:
         _var_sort_occurrences = var_occurrences(kast)
         subst = {}
@@ -1100,21 +1141,14 @@ def _sort_contexts(_kast: KInner) -> None:
         collect(_sort_contexts, kast)
 
         for vname, _voccurrences in _var_sort_occurrences.items():
-            voccurrences = list(unique(_voccurrences))
-            if len(voccurrences) > 0:
-                vsort = voccurrences[0].sort
-                if len(voccurrences) > 1:
-                    for v in voccurrences[1:]:
-                        if vsort is None and v.sort is not None:
-                            vsort = v.sort
-                        elif vsort is not None and v.sort is not None:
-                            if vsort != v.sort:
-                                if v.sort in self.subsorts(vsort):
-                                    vsort = v.sort
-                                elif vsort not in self.subsorts(v.sort):
-                                    raise ValueError(
-                                        f'Could not find common subsort among variable occurrences: {voccurrences}'
-                                    )
+            vsorts = list(unique(v.sort for v in _voccurrences if v.sort is not None))
+            if len(vsorts) > 0:
+                vsort = vsorts[0]
+                for s in vsorts[1:]:
+                    _vsort = self.greatest_common_subsort(vsort, s)
+                    if _vsort is None:
+                        raise ValueError(f'Cannot compute greatest common subsort of {vname}: {(vsort, s)}')
+                    vsort = _vsort
                 subst[vname] = KVariable(vname, sort=vsort)
 
         return Subst(subst)
@@ -1126,6 +1160,33 @@ def sort_vars(self, kast: KInner, sort: KSort | None = None) -> KInner:
         subst = self.sort_vars_subst(kast)
         return subst(kast)
 
+    # Best-effort addition of sort parameters to klabels, context insensitive
+    def add_sort_params(self, kast: KInner) -> KInner:
+        def _add_sort_params(_k: KInner) -> KInner:
+            if type(_k) is KApply:
+                prod = self.production_for_klabel(_k.label)
+                if len(_k.label.params) == 0 and len(prod.params) > 0:
+                    sort_dict: dict[KSort, KSort] = {}
+                    for psort, asort in zip(prod.argument_sorts, map(self.sort, _k.args), strict=True):
+                        if asort is None:
+                            _LOGGER.warning(
+                                f'Failed to add sort parameter, unable to determine sort for argument in production: {(prod, psort, asort)}'
+                            )
+                            return _k
+                        if psort in prod.params:
+                            if psort in sort_dict and sort_dict[psort] != asort:
+                                _LOGGER.warning(
+                                    f'Failed to add sort parameter, sort mismatch between different occurances of sort parameter: {(prod, psort, sort_dict[psort], asort)}'
+                                )
+                                return _k
+                            elif psort not in sort_dict:
+                                sort_dict[psort] = asort
+                    if all(p in sort_dict for p in prod.params):
+                        return _k.let(label=KLabel(_k.label.name, [sort_dict[p] for p in prod.params]))
+            return _k
+
+        return bottom_up(_add_sort_params, kast)
+
     def add_cell_map_items(self, kast: KInner) -> KInner:
         # example:
         # syntax AccountCellMap [cellCollection, hook(MAP.Map)]