From 0bb50db04d5ee3ab6e7fae36acd406f144a09277 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 19 Feb 2026 18:00:03 -0600 Subject: [PATCH 01/11] Add pyo3 to workspace and "python" feature flag --- Cargo.toml | 1 + kframework/Cargo.toml | 4 ++++ 2 files changed, 5 insertions(+) diff --git a/Cargo.toml b/Cargo.toml index 0a5b9e5..6785a40 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -20,3 +20,4 @@ clap = { version = "4.5.20", features = ["derive"] } serde = { version = "1.0.214", features = ["derive"] } serde_json = "1.0.132" indoc = "2.0.5" +pyo3 = "0.28.0" diff --git a/kframework/Cargo.toml b/kframework/Cargo.toml index 3eb90e2..d628b48 100644 --- a/kframework/Cargo.toml +++ b/kframework/Cargo.toml @@ -8,6 +8,10 @@ rust-version.workspace = true clap = { workspace = true } serde = { workspace = true } serde_json = { workspace = true } +pyo3 = { workspace = true } [dev-dependencies] indoc = { workspace = true } + +[features] +python = [] From ec4922b0b2b6037153e1ef20feb2e52cd472063e Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 19 Feb 2026 18:08:42 -0600 Subject: [PATCH 02/11] Add bindings/kframework_py crate (generated with the 'maturin' tool) where the python bindings will be packaged --- Cargo.toml | 1 + .../kframework_py/.github/workflows/CI.yml | 186 ++++++++++++++++++ bindings/kframework_py/.gitignore | 72 +++++++ bindings/kframework_py/Cargo.toml | 14 ++ bindings/kframework_py/pyproject.toml | 13 ++ bindings/kframework_py/src/lib.rs | 43 ++++ 6 files changed, 329 insertions(+) create mode 100644 bindings/kframework_py/.github/workflows/CI.yml create mode 100644 bindings/kframework_py/.gitignore create mode 100644 bindings/kframework_py/Cargo.toml create mode 100644 bindings/kframework_py/pyproject.toml create mode 100644 bindings/kframework_py/src/lib.rs diff --git a/Cargo.toml b/Cargo.toml index 6785a40..d2a97e7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,6 +2,7 @@ resolver = "2" members = [ + "bindings/kframework_py", "kframework", "kframework_ffi", ] diff --git a/bindings/kframework_py/.github/workflows/CI.yml b/bindings/kframework_py/.github/workflows/CI.yml new file mode 100644 index 0000000..c6d8bc5 --- /dev/null +++ b/bindings/kframework_py/.github/workflows/CI.yml @@ -0,0 +1,186 @@ +# This file is autogenerated by maturin v1.11.5 +# To update, run +# +# maturin generate-ci github +# +name: CI + +on: + push: + branches: + - main + - master + tags: + - '*' + pull_request: + workflow_dispatch: + +permissions: + contents: read + +jobs: + linux: + runs-on: ${{ matrix.platform.runner }} + strategy: + matrix: + platform: + - runner: ubuntu-22.04 + target: x86_64 + - runner: ubuntu-22.04 + target: x86 + - runner: ubuntu-22.04 + target: aarch64 + - runner: ubuntu-22.04 + target: armv7 + - runner: ubuntu-22.04 + target: s390x + - runner: ubuntu-22.04 + target: ppc64le + steps: + - uses: actions/checkout@v6 + - uses: actions/setup-python@v6 + with: + python-version: 3.x + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.platform.target }} + args: --release --out dist --find-interpreter + sccache: ${{ !startsWith(github.ref, 'refs/tags/') }} + manylinux: auto + - name: Upload wheels + uses: actions/upload-artifact@v5 + with: + name: wheels-linux-${{ matrix.platform.target }} + path: dist + + musllinux: + runs-on: ${{ matrix.platform.runner }} + strategy: + matrix: + platform: + - runner: ubuntu-22.04 + target: x86_64 + - runner: ubuntu-22.04 + target: x86 + - runner: ubuntu-22.04 + target: aarch64 + - runner: ubuntu-22.04 + target: armv7 + steps: + - uses: actions/checkout@v6 + - uses: actions/setup-python@v6 + with: + python-version: 3.x + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.platform.target }} + args: --release --out dist --find-interpreter + sccache: ${{ !startsWith(github.ref, 'refs/tags/') }} + manylinux: musllinux_1_2 + - name: Upload wheels + uses: actions/upload-artifact@v5 + with: + name: wheels-musllinux-${{ matrix.platform.target }} + path: dist + + windows: + runs-on: ${{ matrix.platform.runner }} + strategy: + matrix: + platform: + - runner: windows-latest + target: x64 + python_arch: x64 + - runner: windows-latest + target: x86 + python_arch: x86 + - runner: windows-11-arm + target: aarch64 + python_arch: arm64 + steps: + - uses: actions/checkout@v6 + - uses: actions/setup-python@v6 + with: + python-version: 3.13 + architecture: ${{ matrix.platform.python_arch }} + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.platform.target }} + args: --release --out dist --find-interpreter + sccache: ${{ !startsWith(github.ref, 'refs/tags/') }} + - name: Upload wheels + uses: actions/upload-artifact@v5 + with: + name: wheels-windows-${{ matrix.platform.target }} + path: dist + + macos: + runs-on: ${{ matrix.platform.runner }} + strategy: + matrix: + platform: + - runner: macos-15-intel + target: x86_64 + - runner: macos-latest + target: aarch64 + steps: + - uses: actions/checkout@v6 + - uses: actions/setup-python@v6 + with: + python-version: 3.x + - name: Build wheels + uses: PyO3/maturin-action@v1 + with: + target: ${{ matrix.platform.target }} + args: --release --out dist --find-interpreter + sccache: ${{ !startsWith(github.ref, 'refs/tags/') }} + - name: Upload wheels + uses: actions/upload-artifact@v5 + with: + name: wheels-macos-${{ matrix.platform.target }} + path: dist + + sdist: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - name: Build sdist + uses: PyO3/maturin-action@v1 + with: + command: sdist + args: --out dist + - name: Upload sdist + uses: actions/upload-artifact@v5 + with: + name: wheels-sdist + path: dist + + release: + name: Release + runs-on: ubuntu-latest + if: ${{ startsWith(github.ref, 'refs/tags/') || github.event_name == 'workflow_dispatch' }} + needs: [linux, musllinux, windows, macos, sdist] + permissions: + # Use to sign the release artifacts + id-token: write + # Used to upload release artifacts + contents: write + # Used to generate artifact attestation + attestations: write + steps: + - uses: actions/download-artifact@v6 + - name: Generate artifact attestation + uses: actions/attest-build-provenance@v3 + with: + subject-path: 'wheels-*/*' + - name: Install uv + if: ${{ startsWith(github.ref, 'refs/tags/') }} + uses: astral-sh/setup-uv@v7 + - name: Publish to PyPI + if: ${{ startsWith(github.ref, 'refs/tags/') }} + run: uv publish 'wheels-*/*' + env: + UV_PUBLISH_TOKEN: ${{ secrets.PYPI_API_TOKEN }} diff --git a/bindings/kframework_py/.gitignore b/bindings/kframework_py/.gitignore new file mode 100644 index 0000000..c8f0442 --- /dev/null +++ b/bindings/kframework_py/.gitignore @@ -0,0 +1,72 @@ +/target + +# Byte-compiled / optimized / DLL files +__pycache__/ +.pytest_cache/ +*.py[cod] + +# C extensions +*.so + +# Distribution / packaging +.Python +.venv/ +env/ +bin/ +build/ +develop-eggs/ +dist/ +eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +include/ +man/ +venv/ +*.egg-info/ +.installed.cfg +*.egg + +# Installer logs +pip-log.txt +pip-delete-this-directory.txt +pip-selfcheck.json + +# Unit test / coverage reports +htmlcov/ +.tox/ +.coverage +.cache +nosetests.xml +coverage.xml + +# Translations +*.mo + +# Mr Developer +.mr.developer.cfg +.project +.pydevproject + +# Rope +.ropeproject + +# Django stuff: +*.log +*.pot + +.DS_Store + +# Sphinx documentation +docs/_build/ + +# PyCharm +.idea/ + +# VSCode +.vscode/ + +# Pyenv +.python-version diff --git a/bindings/kframework_py/Cargo.toml b/bindings/kframework_py/Cargo.toml new file mode 100644 index 0000000..e77b692 --- /dev/null +++ b/bindings/kframework_py/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "kframework_py" +version.workspace = true +edition.workspace = true +rust-version.workspace = true + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html +[lib] +name = "kframework_py" +crate-type = ["cdylib"] + +[dependencies] +kframework = { path = "../../kframework", features = ["python"] } +pyo3 = { workspace = true } diff --git a/bindings/kframework_py/pyproject.toml b/bindings/kframework_py/pyproject.toml new file mode 100644 index 0000000..cc755c5 --- /dev/null +++ b/bindings/kframework_py/pyproject.toml @@ -0,0 +1,13 @@ +[build-system] +requires = ["maturin>=1.11,<2.0"] +build-backend = "maturin" + +[project] +name = "kframework_py" +requires-python = ">=3.8" +classifiers = [ + "Programming Language :: Rust", + "Programming Language :: Python :: Implementation :: CPython", + "Programming Language :: Python :: Implementation :: PyPy", +] +dynamic = ["version"] diff --git a/bindings/kframework_py/src/lib.rs b/bindings/kframework_py/src/lib.rs new file mode 100644 index 0000000..42eda80 --- /dev/null +++ b/bindings/kframework_py/src/lib.rs @@ -0,0 +1,43 @@ +use pyo3::prelude::*; + +// In order to get clean import semantics like "from a.b import c" for the +// bindings modules, the sys.modules dict needs to be updated with "a.b", +// "a.b.c", etc. +// +// We use this helper function to do that in #[pymodule_init] functions for each +// module. +fn create_sys_module(module: &Bound<'_, PyModule>, module_name: &str) -> PyResult<()> { + module + .py() + .import("sys")? + .getattr("modules")? + .set_item(module_name, module) +} + +/// A Python module implemented in Rust. +#[pymodule] +mod kframework_py { + use pyo3::prelude::*; + + #[pymodule] + mod kore { + use crate::create_sys_module; + use pyo3::prelude::*; + + #[pymodule_init] + fn init(module: &Bound<'_, PyModule>) -> PyResult<()> { + create_sys_module(module, "kframework_py.kore") + } + + #[pymodule] + mod syntax { + use crate::create_sys_module; + use pyo3::prelude::*; + + #[pymodule_init] + fn init(module: &Bound<'_, PyModule>) -> PyResult<()> { + create_sys_module(module, "kframework_py.kore.syntax") + } + } + } +} From 45e474f2e9227f73a9f57fbc93e8ba289167c009 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 20 Feb 2026 13:32:27 -0600 Subject: [PATCH 03/11] Make Id into a pyclass, with a constructor and a getter --- bindings/kframework_py/src/lib.rs | 3 +++ kframework/src/bindings/python.rs | 15 +++++++++++++++ kframework/src/kore/syntax.rs | 5 +++-- kframework/src/lib.rs | 3 +++ 4 files changed, 24 insertions(+), 2 deletions(-) create mode 100644 kframework/src/bindings/python.rs diff --git a/bindings/kframework_py/src/lib.rs b/bindings/kframework_py/src/lib.rs index 42eda80..358a38c 100644 --- a/bindings/kframework_py/src/lib.rs +++ b/bindings/kframework_py/src/lib.rs @@ -38,6 +38,9 @@ mod kframework_py { fn init(module: &Bound<'_, PyModule>) -> PyResult<()> { create_sys_module(module, "kframework_py.kore.syntax") } + + #[pymodule_export] + use kframework::kore::Id; } } } diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs new file mode 100644 index 0000000..3b7bad6 --- /dev/null +++ b/kframework/src/bindings/python.rs @@ -0,0 +1,15 @@ +use crate::kore::Id; +use pyo3::{exceptions::PyValueError, prelude::*}; + +#[pymethods] +impl Id { + #[new] + fn py_new(s: String) -> PyResult { + Self::new(s).map_err(|e| PyErr::new::(e)) + } + + #[getter(value)] + fn py_value(&self) -> &str { + self.value() + } +} diff --git a/kframework/src/kore/syntax.rs b/kframework/src/kore/syntax.rs index a1effe5..ee4cc25 100644 --- a/kframework/src/kore/syntax.rs +++ b/kframework/src/kore/syntax.rs @@ -1,3 +1,4 @@ +#[cfg_attr(feature = "python", pyo3::pyclass)] #[derive(Debug, PartialEq, Eq)] pub struct Id(pub(crate) String); @@ -24,8 +25,8 @@ impl Id { } } - pub fn value(self) -> String { - self.0 + pub fn value(&self) -> &str { + &self.0 } } diff --git a/kframework/src/lib.rs b/kframework/src/lib.rs index bdfddfd..0a153e6 100644 --- a/kframework/src/lib.rs +++ b/kframework/src/lib.rs @@ -1 +1,4 @@ pub mod kore; + +#[cfg(any(feature = "python"))] +pub mod bindings; From 66c1f3994b947eb5a8a73ed71249406c59a0bd53 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Fri, 20 Feb 2026 13:57:26 -0600 Subject: [PATCH 04/11] Add tests folder for kframework_py --- bindings/kframework_py/pyproject.toml | 5 +++++ bindings/kframework_py/tests/test_kore.py | 12 ++++++++++++ 2 files changed, 17 insertions(+) create mode 100644 bindings/kframework_py/tests/test_kore.py diff --git a/bindings/kframework_py/pyproject.toml b/bindings/kframework_py/pyproject.toml index cc755c5..ba1b2e5 100644 --- a/bindings/kframework_py/pyproject.toml +++ b/bindings/kframework_py/pyproject.toml @@ -11,3 +11,8 @@ classifiers = [ "Programming Language :: Python :: Implementation :: PyPy", ] dynamic = ["version"] + +[dependency-groups] +dev = [ + "pytest>=8.3.5", +] diff --git a/bindings/kframework_py/tests/test_kore.py b/bindings/kframework_py/tests/test_kore.py new file mode 100644 index 0000000..fb25cc8 --- /dev/null +++ b/bindings/kframework_py/tests/test_kore.py @@ -0,0 +1,12 @@ +from kframework_py.kore.syntax import Id + +def test_id(): + i = Id("foo") + + a = i.value + b = i.value + + assert a == "foo" + + # TODO: Fix this! + # assert a is b From f465271632cb188cb6c48b3f0776514c5548c0c9 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Mon, 23 Feb 2026 14:32:52 -0600 Subject: [PATCH 05/11] fixup! Make Id into a pyclass, with a constructor and a getter --- kframework/src/bindings.rs | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 kframework/src/bindings.rs diff --git a/kframework/src/bindings.rs b/kframework/src/bindings.rs new file mode 100644 index 0000000..a098fa3 --- /dev/null +++ b/kframework/src/bindings.rs @@ -0,0 +1,2 @@ +#[cfg(feature = "python")] +pub mod python; From e1567cdeda0c15f8f3e963012b0c4e28b8b779ee Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 24 Feb 2026 13:40:26 -0600 Subject: [PATCH 06/11] Create SortVar and SortApp classes, holding pointers to inner rust structs. --- bindings/kframework_py/src/lib.rs | 34 ++++++- kframework/src/bindings/python.rs | 160 +++++++++++++++++++++++++++++- kframework/src/kore/syntax.rs | 4 +- kframework/src/lib.rs | 2 +- 4 files changed, 191 insertions(+), 9 deletions(-) diff --git a/bindings/kframework_py/src/lib.rs b/bindings/kframework_py/src/lib.rs index 358a38c..224edf8 100644 --- a/bindings/kframework_py/src/lib.rs +++ b/bindings/kframework_py/src/lib.rs @@ -32,15 +32,43 @@ mod kframework_py { #[pymodule] mod syntax { use crate::create_sys_module; - use pyo3::prelude::*; + use pyo3::{ + prelude::*, + types::{IntoPyDict, PyDict, PyList, PyString}, + }; #[pymodule_init] fn init(module: &Bound<'_, PyModule>) -> PyResult<()> { - create_sys_module(module, "kframework_py.kore.syntax") + create_sys_module(module, "kframework_py.kore.syntax")?; + + let py = module.py(); + let sortvar = module.getattr("SortVar")?; + let sortapp = module.getattr("SortApp")?; + + let stringtype = py.get_type::(); + let listtype = py.get_type::(); + + let var_annotations = PyDict::new(py); + var_annotations.set_item("name", &stringtype)?; + sortvar.setattr("__annotations__", var_annotations)?; + + let app_annotations = PyDict::new(py); + app_annotations.set_item("name", &stringtype)?; + app_annotations.set_item("args", &listtype)?; + sortapp.setattr("__annotations__", app_annotations)?; + + let dataclass = py.import("dataclasses")?.getattr("dataclass")?; + let kwargs = Some([("init", false), ("frozen", true)].into_py_dict(py)?); + dataclass.call((sortvar,), kwargs.as_ref())?; + dataclass.call((sortapp,), kwargs.as_ref())?; + Ok(()) } #[pymodule_export] - use kframework::kore::Id; + use kframework::{ + bindings::python::{PySortNode, SortApp, SortVar}, + kore::Id, + }; } } } diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs index 3b7bad6..02baa80 100644 --- a/kframework/src/bindings/python.rs +++ b/kframework/src/bindings/python.rs @@ -1,11 +1,19 @@ -use crate::kore::Id; -use pyo3::{exceptions::PyValueError, prelude::*}; +#![allow(unused)] + +use std::collections::HashMap; + +use crate::kore::{Id, Sort}; +use pyo3::{ + exceptions::{PyTypeError, PyValueError}, + prelude::*, + types::{PyString, PyTuple}, +}; #[pymethods] impl Id { #[new] fn py_new(s: String) -> PyResult { - Self::new(s).map_err(|e| PyErr::new::(e)) + Self::new(s).map_err(PyValueError::new_err) } #[getter(value)] @@ -13,3 +21,149 @@ impl Id { self.value() } } + +/// A metatada struct for the root node of a Sort +#[pyclass(unsendable)] +struct PySortView { + root: Box, + /// A list of pointers to all sub-trees of the root + nodes: Vec<*const Sort>, + /// A list of children indices given a node index + children: Vec>, +} + +impl PySortView { + fn get(&self, idx: usize) -> Option<&Sort> { + self.nodes.get(idx).map(|p| unsafe { &**p }) + } +} + +impl Sort { + fn into_view(self) -> PySortView { + let root = Box::new(self); + + let mut nodes = Vec::new(); + let mut stack = vec![root.as_ref()]; + + while let Some(n) = stack.pop() { + nodes.push(n as *const Sort); + + if let Sort::App { args, .. } = n { + stack.extend(args) + }; + } + + let mut index_of = HashMap::new(); + + for (i, &ptr) in nodes.iter().enumerate() { + index_of.insert(ptr, i); + } + + let mut children: Vec> = Vec::with_capacity(nodes.len()); + for &p in &nodes { + let s = unsafe { &*p }; + let child_idxs = match s { + Sort::Var(_) => Vec::new(), + Sort::App { args, .. } => args + .iter() + .map(|c| { + let cp = c as *const Sort; + *index_of.get(&cp).expect("Pointer didn't exist in lookup") + }) + .collect(), + }; + children.push(child_idxs.into_boxed_slice()); + } + + PySortView { + root, + nodes, + children, + } + } +} + +#[pyclass(subclass, name = "Sort")] +pub struct PySortNode { + inner: Py, + idx: usize, +} + +fn create_node(view: &Bound<'_, PySortView>, idx: usize) -> PyResult> { + let py = view.py(); + let view_ref = view.borrow(); + let node = view_ref.get(idx).expect("Invalid node index"); + + let sort = PySortNode { + inner: view.clone().unbind(), + idx, + }; + let res: Py = match node { + Sort::Var(id) => { + let var = SortVar { + name: PyString::new(py, id.value()).unbind(), + }; + Py::new(py, (var, sort))?.into() + } + Sort::App { id, .. } => { + let children_idxs = view_ref.children.get(idx).expect("Invalid node index"); + let children = children_idxs + .iter() + .map(|idx| create_node(view, *idx)) + .collect::>>>()?; + let app = SortApp { + name: PyString::new(py, id.value()).unbind(), + args: PyTuple::new(py, children)?.into(), + }; + Py::new(py, (app, sort))?.into() + } + }; + Ok(res) +} + +#[pymethods] +impl PySortNode { + #[staticmethod] + fn parse(py: Python<'_>, s: &str) -> PyResult> { + use crate::kore::Parser; + let sort: Sort = Parser::new(s) + .and_then(|mut p| p.sort()) + .map_err(PyValueError::new_err)?; + let view = Bound::new(py, sort.into_view())?; + let res = create_node(&view, 0)?; + Ok(res.extract(py)?) + } +} + +#[pyclass(extends = PySortNode)] +pub struct SortVar { + #[pyo3(get)] + name: Py, +} + +#[pymethods] +impl SortVar { + #[new] + fn new_(py: Python<'_>, id: Py) -> PyResult> { + let view = if let Ok(id) = id.extract::(py) { + let sort = Sort::Var(id); + Ok(sort.into_view()) + } else if let Ok(id_str) = id.cast_bound::(py) { + let id = Id::new(id_str.to_string()).map_err(PyValueError::new_err)?; + let sort = Sort::Var(id); + Ok(sort.into_view()) + } else { + Err(PyTypeError::new_err("")) + }?; + let view_bound = Bound::new(py, view)?; + create_node(&view_bound, 0) + } +} + +#[pyclass(extends = PySortNode)] +pub struct SortApp { + #[pyo3(get)] + name: Py, + #[pyo3(get)] + args: Py, +} diff --git a/kframework/src/kore/syntax.rs b/kframework/src/kore/syntax.rs index ee4cc25..fb593da 100644 --- a/kframework/src/kore/syntax.rs +++ b/kframework/src/kore/syntax.rs @@ -1,5 +1,5 @@ -#[cfg_attr(feature = "python", pyo3::pyclass)] -#[derive(Debug, PartialEq, Eq)] +#[cfg_attr(feature = "python", pyo3::pyclass(from_py_object))] +#[derive(Clone, Debug, PartialEq, Eq)] pub struct Id(pub(crate) String); impl Id { diff --git a/kframework/src/lib.rs b/kframework/src/lib.rs index 0a153e6..a564109 100644 --- a/kframework/src/lib.rs +++ b/kframework/src/lib.rs @@ -1,4 +1,4 @@ pub mod kore; -#[cfg(any(feature = "python"))] +#[cfg(feature = "python")] pub mod bindings; From 8e12e1f45b57e5897a464f9ce14690da20d086fe Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 24 Feb 2026 16:11:56 -0600 Subject: [PATCH 07/11] Use Arc pointers for Sort::App children --- kframework/src/bindings/python.rs | 30 +++++++++++++++++------------- kframework/src/kore/deserialize.rs | 2 ++ kframework/src/kore/parser.rs | 3 +++ kframework/src/kore/serialize.rs | 3 ++- kframework/src/kore/syntax.rs | 4 +++- kframework/tests/kore/parser.rs | 14 ++++++++------ 6 files changed, 35 insertions(+), 21 deletions(-) diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs index 02baa80..b9906e8 100644 --- a/kframework/src/bindings/python.rs +++ b/kframework/src/bindings/python.rs @@ -1,6 +1,6 @@ #![allow(unused)] -use std::collections::HashMap; +use std::{collections::HashMap, sync::Arc}; use crate::kore::{Id, Sort}; use pyo3::{ @@ -25,10 +25,12 @@ impl Id { /// A metatada struct for the root node of a Sort #[pyclass(unsendable)] struct PySortView { - root: Box, + root: Arc, /// A list of pointers to all sub-trees of the root - nodes: Vec<*const Sort>, - /// A list of children indices given a node index + nodes: Vec>, + /// Reverse lookup to a node index from a raw pointer + index_of: HashMap<*const Sort, usize>, + /// List of child indices given a node index children: Vec>, } @@ -40,34 +42,35 @@ impl PySortView { impl Sort { fn into_view(self) -> PySortView { - let root = Box::new(self); + let root = Arc::new(self); let mut nodes = Vec::new(); - let mut stack = vec![root.as_ref()]; + let mut stack = vec![root.clone()]; while let Some(n) = stack.pop() { - nodes.push(n as *const Sort); + nodes.push(n.clone()); - if let Sort::App { args, .. } = n { + if let Sort::App { args, .. } = &*n { + let args: Vec> = args.to_vec(); stack.extend(args) }; } let mut index_of = HashMap::new(); - for (i, &ptr) in nodes.iter().enumerate() { - index_of.insert(ptr, i); + for (i, ptr) in nodes.iter().enumerate() { + index_of.insert(Arc::::into_raw(ptr.clone()), i); } let mut children: Vec> = Vec::with_capacity(nodes.len()); - for &p in &nodes { - let s = unsafe { &*p }; + for p in &nodes { + let s = &**p; let child_idxs = match s { Sort::Var(_) => Vec::new(), Sort::App { args, .. } => args .iter() .map(|c| { - let cp = c as *const Sort; + let cp = Arc::::into_raw(c.clone()); *index_of.get(&cp).expect("Pointer didn't exist in lookup") }) .collect(), @@ -78,6 +81,7 @@ impl Sort { PySortView { root, nodes, + index_of, children, } } diff --git a/kframework/src/kore/deserialize.rs b/kframework/src/kore/deserialize.rs index 0ee1ef4..7ba712d 100644 --- a/kframework/src/kore/deserialize.rs +++ b/kframework/src/kore/deserialize.rs @@ -2,6 +2,7 @@ use super::{App, Id, Pattern, SVar, SetVarId, Sort, Str, SymbolId, Var}; use serde; use serde::de::{Deserialize, Deserializer, Error, MapAccess, Unexpected, Visitor}; use std::fmt; +use std::sync::Arc; macro_rules! deserialize_for_id { ($struct:ident, $expecting:expr, $valid_value:expr) => { @@ -101,6 +102,7 @@ impl<'de> Deserialize<'de> for Sort { Tag::SortVar => Ok(Sort::Var(id)), Tag::SortApp => { let args = args.ok_or_else(|| Error::missing_field("args"))?; + let args = args.into_iter().map(Arc::new).collect::>(); Ok(Sort::App { id, args }) } } diff --git a/kframework/src/kore/parser.rs b/kframework/src/kore/parser.rs index 6a7d3aa..590ac64 100644 --- a/kframework/src/kore/parser.rs +++ b/kframework/src/kore/parser.rs @@ -1,3 +1,5 @@ +use std::sync::Arc; + use super::lexer::{Lexer, Token, TokenType}; use super::{ App, Definition, Id, Module, Pattern, SVar, Sentence, SetVarId, Sort, Str, SymbolId, Var, @@ -100,6 +102,7 @@ impl<'a> Parser<'a> { let id = self.id()?; let sort = if self.la.ty() == TokenType::LBrace { let args = self.sorts()?; + let args = args.into_iter().map(Arc::new).collect::>(); Sort::App { id, args } } else { Sort::Var(id) diff --git a/kframework/src/kore/serialize.rs b/kframework/src/kore/serialize.rs index 7bc1d09..e1936f8 100644 --- a/kframework/src/kore/serialize.rs +++ b/kframework/src/kore/serialize.rs @@ -18,7 +18,8 @@ impl Serialize for Sort { let mut state = serializer.serialize_struct("SortApp", 3)?; state.serialize_field("tag", "SortApp")?; state.serialize_field("name", &id.0)?; - state.serialize_field("args", args)?; + let args: Vec<&Sort> = args.iter().map(|sort| &**sort).collect(); + state.serialize_field("args", &args)?; state.end() } } diff --git a/kframework/src/kore/syntax.rs b/kframework/src/kore/syntax.rs index fb593da..d0801c5 100644 --- a/kframework/src/kore/syntax.rs +++ b/kframework/src/kore/syntax.rs @@ -1,3 +1,5 @@ +use std::sync::Arc; + #[cfg_attr(feature = "python", pyo3::pyclass(from_py_object))] #[derive(Clone, Debug, PartialEq, Eq)] pub struct Id(pub(crate) String); @@ -305,7 +307,7 @@ pub enum Sentence { #[derive(Debug, PartialEq, Eq)] pub enum Sort { Var(Id), - App { id: Id, args: Vec }, + App { id: Id, args: Box<[Arc]> }, } #[derive(Debug, PartialEq, Eq)] diff --git a/kframework/tests/kore/parser.rs b/kframework/tests/kore/parser.rs index 0df704c..0c7682e 100644 --- a/kframework/tests/kore/parser.rs +++ b/kframework/tests/kore/parser.rs @@ -1,3 +1,5 @@ +use std::sync::Arc; + use kframework::kore::{ App, Definition, Id, Module, Parser, Pattern, SVar, Sentence, SetVarId, Sort, SymbolId, Var, }; @@ -36,7 +38,7 @@ macro_rules! sort_tests { sort_tests! { test_sort_var: ("S", Sort::Var(id("S")?)), - test_sort_app: ("SortInt{}", Sort::App { id: id("SortInt")?, args: vec![] }), + test_sort_app: ("SortInt{}", Sort::App { id: id("SortInt")?, args: vec![].into() }), test_sort_app_with_params: ( "SortMap{X, Y}", Sort::App { @@ -44,7 +46,7 @@ sort_tests! { args: vec![ Sort::Var(id("X")?), Sort::Var(id("Y")?), - ], + ].into_iter().map(Arc::new).collect::>(), } ), } @@ -132,7 +134,7 @@ pattern_tests! { test_pattern_dv: ( r#"\dv{SortInt{}}("0")"#, Pattern::Dv { - sort: Sort::App { id: id("SortInt")?, args: vec![] }, + sort: Sort::App { id: id("SortInt")?, args: vec![].into() }, value: "0".into(), }, ), @@ -367,7 +369,7 @@ sentence_tests! { vars: vec![id("S")?, id("T")?], param_sorts: vec![ Sort::Var(id("S")?), - Sort::App { id: id("SortInt")?, args: vec![] }, + Sort::App { id: id("SortInt")?, args: vec![].into() }, ], sort: Sort::Var(id("T")?), attrs: vec![], @@ -381,7 +383,7 @@ sentence_tests! { vars: vec![id("S")?, id("T")?], param_sorts: vec![ Sort::Var(id("S")?), - Sort::App { id: id("SortInt")?, args: vec![] }, + Sort::App { id: id("SortInt")?, args: vec![].into() }, ], sort: Sort::Var(id("T")?), attrs: vec![], @@ -394,7 +396,7 @@ sentence_tests! { id: sym(r"\foo")?, vars: vec![id("S")?], param_sorts: vec![Sort::Var(id("S")?)], - sort: Sort::App { id: id("SortBool")?, args: vec![] }, + sort: Sort::App { id: id("SortBool")?, args: vec![].into() }, left: App { symbol: sym(r"\foo")?, sorts: vec![Sort::Var(id("S")?)], From ed70ba4681d575487b29d95f1beeb53f76153654 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Wed, 25 Feb 2026 09:10:30 -0600 Subject: [PATCH 08/11] Change PySortView to PySortArena, which can track all allocations of Sort --- kframework/src/bindings/python.rs | 157 ++++++++++++++---------------- 1 file changed, 74 insertions(+), 83 deletions(-) diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs index b9906e8..905501d 100644 --- a/kframework/src/bindings/python.rs +++ b/kframework/src/bindings/python.rs @@ -22,120 +22,109 @@ impl Id { } } -/// A metatada struct for the root node of a Sort #[pyclass(unsendable)] -struct PySortView { - root: Arc, - /// A list of pointers to all sub-trees of the root - nodes: Vec>, - /// Reverse lookup to a node index from a raw pointer +#[derive(Default)] +pub struct PySortArena { + inners: Vec>, index_of: HashMap<*const Sort, usize>, - /// List of child indices given a node index children: Vec>, + cache: HashMap>, } -impl PySortView { - fn get(&self, idx: usize) -> Option<&Sort> { - self.nodes.get(idx).map(|p| unsafe { &**p }) +impl PySortArena { + pub fn new() -> Self { + Self::default() } -} - -impl Sort { - fn into_view(self) -> PySortView { - let root = Arc::new(self); - let mut nodes = Vec::new(); - let mut stack = vec![root.clone()]; + pub fn add(&mut self, sort: Arc) -> usize { + let idx = self.inners.len(); + self.inners.push(sort.clone()); + self.index_of + .insert(Arc::::into_raw(sort.clone()), idx); + self.children.push(Box::new([])); - while let Some(n) = stack.pop() { - nodes.push(n.clone()); - - if let Sort::App { args, .. } = &*n { - let args: Vec> = args.to_vec(); - stack.extend(args) - }; + if let Sort::App { args, .. } = &*sort { + let children = args + .iter() + .map(|arg| self.add(arg.clone())) + .collect::>(); + self.children[idx] = children; } - let mut index_of = HashMap::new(); + idx + } +} - for (i, ptr) in nodes.iter().enumerate() { - index_of.insert(Arc::::into_raw(ptr.clone()), i); +#[pymethods] +impl PySortArena { + fn get<'py>( + slf: &Bound<'py, Self>, + py: Python<'py>, + idx: usize, + ) -> PyResult> { + let slf_ref = slf.borrow(); + + // Check the cache + if let Some(res) = &slf_ref.cache.get(&idx) { + return Ok(res.bind(py).clone()); } - let mut children: Vec> = Vec::with_capacity(nodes.len()); - for p in &nodes { - let s = &**p; - let child_idxs = match s { - Sort::Var(_) => Vec::new(), - Sort::App { args, .. } => args + // Otherwise create the python object for the node, update the cache + // with it (if possible), and return it + let sort = slf_ref.inners.get(idx).expect("Invalid node index"); + let node = PySortNode { + inner: slf.clone().unbind(), + idx, + }; + let res: Bound<'_, PyAny> = match &**sort { + Sort::Var(id) => { + let var = SortVar { + name: PyString::new(py, id.value()).unbind(), + }; + Bound::new(py, (var, node))?.into_any() + } + Sort::App { id, .. } => { + let children_idxs = slf_ref.children.get(idx).expect("Invalid node index"); + let children = children_idxs .iter() - .map(|c| { - let cp = Arc::::into_raw(c.clone()); - *index_of.get(&cp).expect("Pointer didn't exist in lookup") - }) - .collect(), - }; - children.push(child_idxs.into_boxed_slice()); + .map(|idx| PySortArena::get(slf, py, *idx)) + .collect::, _>>()?; + let app = SortApp { + name: PyString::new(py, id.value()).unbind(), + args: PyTuple::new(py, children)?.into(), + }; + Bound::new(py, (app, node))?.into_any() + } + }; + + drop(slf_ref); + + if let Ok(mut slf_ref_mut) = slf.try_borrow_mut() { + slf_ref_mut.cache.insert(idx, res.clone().unbind()); } - PySortView { - root, - nodes, - index_of, - children, - } + Ok(res) } } #[pyclass(subclass, name = "Sort")] pub struct PySortNode { - inner: Py, + inner: Py, idx: usize, } -fn create_node(view: &Bound<'_, PySortView>, idx: usize) -> PyResult> { - let py = view.py(); - let view_ref = view.borrow(); - let node = view_ref.get(idx).expect("Invalid node index"); - - let sort = PySortNode { - inner: view.clone().unbind(), - idx, - }; - let res: Py = match node { - Sort::Var(id) => { - let var = SortVar { - name: PyString::new(py, id.value()).unbind(), - }; - Py::new(py, (var, sort))?.into() - } - Sort::App { id, .. } => { - let children_idxs = view_ref.children.get(idx).expect("Invalid node index"); - let children = children_idxs - .iter() - .map(|idx| create_node(view, *idx)) - .collect::>>>()?; - let app = SortApp { - name: PyString::new(py, id.value()).unbind(), - args: PyTuple::new(py, children)?.into(), - }; - Py::new(py, (app, sort))?.into() - } - }; - Ok(res) -} - #[pymethods] impl PySortNode { #[staticmethod] - fn parse(py: Python<'_>, s: &str) -> PyResult> { + fn parse(py: Python<'_>, s: &str) -> PyResult> { use crate::kore::Parser; let sort: Sort = Parser::new(s) .and_then(|mut p| p.sort()) .map_err(PyValueError::new_err)?; - let view = Bound::new(py, sort.into_view())?; - let res = create_node(&view, 0)?; - Ok(res.extract(py)?) + let mut arena = PySortArena::new(); + let idx = arena.add(sort.into()); + let arena_bound = Bound::new(py, arena)?; + PySortArena::get(&arena_bound, py, idx).map(|a| a.into_any().unbind()) } } @@ -147,6 +136,7 @@ pub struct SortVar { #[pymethods] impl SortVar { + /* #[new] fn new_(py: Python<'_>, id: Py) -> PyResult> { let view = if let Ok(id) = id.extract::(py) { @@ -162,6 +152,7 @@ impl SortVar { let view_bound = Bound::new(py, view)?; create_node(&view_bound, 0) } + */ } #[pyclass(extends = PySortNode)] From 8bb1a784bb6a811ceeae96836dc4daa273ac767d Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 26 Feb 2026 18:50:41 -0600 Subject: [PATCH 09/11] Global arena + doc strings --- bindings/kframework_py/src/lib.rs | 20 +-- kframework/src/bindings/python.rs | 234 +++++++++++++++++++++--------- 2 files changed, 172 insertions(+), 82 deletions(-) diff --git a/bindings/kframework_py/src/lib.rs b/bindings/kframework_py/src/lib.rs index 224edf8..1086aac 100644 --- a/bindings/kframework_py/src/lib.rs +++ b/bindings/kframework_py/src/lib.rs @@ -32,10 +32,7 @@ mod kframework_py { #[pymodule] mod syntax { use crate::create_sys_module; - use pyo3::{ - prelude::*, - types::{IntoPyDict, PyDict, PyList, PyString}, - }; + use pyo3::{prelude::*, types::IntoPyDict}; #[pymodule_init] fn init(module: &Bound<'_, PyModule>) -> PyResult<()> { @@ -45,18 +42,9 @@ mod kframework_py { let sortvar = module.getattr("SortVar")?; let sortapp = module.getattr("SortApp")?; - let stringtype = py.get_type::(); - let listtype = py.get_type::(); - - let var_annotations = PyDict::new(py); - var_annotations.set_item("name", &stringtype)?; - sortvar.setattr("__annotations__", var_annotations)?; - - let app_annotations = PyDict::new(py); - app_annotations.set_item("name", &stringtype)?; - app_annotations.set_item("args", &listtype)?; - sortapp.setattr("__annotations__", app_annotations)?; - + // Each python class has the `__annotations__` attribute set. + // + // This allows us to call the `dataclass` decorator on them. let dataclass = py.import("dataclasses")?.getattr("dataclass")?; let kwargs = Some([("init", false), ("frozen", true)].into_py_dict(py)?); dataclass.call((sortvar,), kwargs.as_ref())?; diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs index 905501d..6c2bb1e 100644 --- a/kframework/src/bindings/python.rs +++ b/kframework/src/bindings/python.rs @@ -1,12 +1,15 @@ #![allow(unused)] -use std::{collections::HashMap, sync::Arc}; +use std::{ + collections::HashMap, + sync::{Arc, Mutex}, +}; use crate::kore::{Id, Sort}; use pyo3::{ exceptions::{PyTypeError, PyValueError}, prelude::*, - types::{PyString, PyTuple}, + types::{PyDict, PyList, PyString, PyTuple}, }; #[pymethods] @@ -22,13 +25,31 @@ impl Id { } } -#[pyclass(unsendable)] +impl TryFrom<&Bound<'_, PyAny>> for Id { + type Error = PyErr; + + fn try_from(value: &Bound<'_, PyAny>) -> PyResult { + if let Ok(id) = value.extract::() { + return Ok(id); + }; + let id_str = value.cast::()?; + let id = Id::new(id_str.to_string()).map_err(PyValueError::new_err)?; + Ok(id) + } +} + +/// [`PySortArena`] +/// +/// An arena containing pointers to allocated [`Sort`]s, as well as +/// some metadata about those objects and the arena itself. +#[pyclass] #[derive(Default)] pub struct PySortArena { inners: Vec>, - index_of: HashMap<*const Sort, usize>, - children: Vec>, - cache: HashMap>, + // A mapping of *const Sort (as usize) to indices of already existing members + index_of: HashMap, + // The python objects corresponding to the rust types, if they exist + cached_pys: Vec>>, } impl PySortArena { @@ -37,98 +58,143 @@ impl PySortArena { } pub fn add(&mut self, sort: Arc) -> usize { + // Check if this sort has already been added to the arena + if let Some(idx) = self.index_of.get(&(Arc::::as_ptr(&sort) as usize)) { + return *idx; + } + + // Otherwise, allocate space for the new sort let idx = self.inners.len(); self.inners.push(sort.clone()); self.index_of - .insert(Arc::::into_raw(sort.clone()), idx); - self.children.push(Box::new([])); + .insert(Arc::::as_ptr(&sort) as usize, idx); + self.cached_pys.push(None); if let Sort::App { args, .. } = &*sort { let children = args .iter() + // Add this sort's children to the arena as well .map(|arg| self.add(arg.clone())) .collect::>(); - self.children[idx] = children; } idx } + + pub fn get(&self, idx: usize) -> Arc { + self.inners.get(idx).cloned().expect("Invalid node index") + } } -#[pymethods] -impl PySortArena { - fn get<'py>( - slf: &Bound<'py, Self>, - py: Python<'py>, - idx: usize, - ) -> PyResult> { - let slf_ref = slf.borrow(); +/// [`PySort`] +/// +/// The base class for the python Sort types. +/// +/// This is just a pointer to a [`PySortArena`] and the +/// index in the arena that represents this object. +#[pyclass(subclass, name = "Sort")] +pub struct PySort { + inner: Py, + idx: usize, +} - // Check the cache - if let Some(res) = &slf_ref.cache.get(&idx) { +impl PySort { + fn get_inner(&self, py: Python<'_>) -> Arc { + let arena = self.inner.bind(py).borrow(); + arena.get(self.idx) + } + + fn get_arena<'py>(py: Python<'py>) -> PyResult> { + let cls = py.get_type::(); + let arena_attr = cls.getattr("__sort_arena__")?; + Ok(arena_attr.cast_into()?) + } + + /// Create a [`PySort`] from a [`Sort`] + /// + /// This relies on the [`PySort::__sort_arena__`] attribute to hold + /// all allocations of both the rust types and their python representations. + /// + /// This also updates the arena's cache with the created object + fn create(py: Python<'_>, sort: Arc) -> PyResult> { + let arena_bound = Self::get_arena(py)?; + + let mut arena = arena_bound.borrow_mut(); + let idx = arena.add(sort.clone()); + + // Check the arena's cache + if let Some(res) = arena.cached_pys.get(idx).expect("Invalid node index") { return Ok(res.bind(py).clone()); } - // Otherwise create the python object for the node, update the cache - // with it (if possible), and return it - let sort = slf_ref.inners.get(idx).expect("Invalid node index"); - let node = PySortNode { - inner: slf.clone().unbind(), + // Nested calls to `create` are coming up, so we drop + // the mutable borrow of the arena here to ensure interior mutability + drop(arena); + + let node = Self { + inner: arena_bound.clone().into(), idx, }; - let res: Bound<'_, PyAny> = match &**sort { + + let res: Bound<'_, PySort> = match &*sort { Sort::Var(id) => { let var = SortVar { name: PyString::new(py, id.value()).unbind(), }; - Bound::new(py, (var, node))?.into_any() + Bound::new(py, (var, node))?.into_super() } - Sort::App { id, .. } => { - let children_idxs = slf_ref.children.get(idx).expect("Invalid node index"); - let children = children_idxs + Sort::App { id, args } => { + let children = args .iter() - .map(|idx| PySortArena::get(slf, py, *idx)) + .map(|sort| Self::create(py, sort.clone())) .collect::, _>>()?; + let args = PyTuple::new(py, children)?; let app = SortApp { name: PyString::new(py, id.value()).unbind(), - args: PyTuple::new(py, children)?.into(), + args: args.into(), }; - Bound::new(py, (app, node))?.into_any() + Bound::new(py, (app, node))?.into_super() } }; - drop(slf_ref); - - if let Ok(mut slf_ref_mut) = slf.try_borrow_mut() { - slf_ref_mut.cache.insert(idx, res.clone().unbind()); - } + // Update the arena's cache + let mut arena_mut = arena_bound.borrow_mut(); + assert!(arena_mut + .cached_pys + .get(idx) + .expect("Invalid node index") + .is_none()); + arena_mut.cached_pys[idx] = Some(res.clone().unbind()); Ok(res) } } -#[pyclass(subclass, name = "Sort")] -pub struct PySortNode { - inner: Py, - idx: usize, -} - #[pymethods] -impl PySortNode { +impl PySort { #[staticmethod] - fn parse(py: Python<'_>, s: &str) -> PyResult> { + fn parse<'py>(py: Python<'py>, s: &str) -> PyResult> { use crate::kore::Parser; + let sort: Sort = Parser::new(s) .and_then(|mut p| p.sort()) .map_err(PyValueError::new_err)?; - let mut arena = PySortArena::new(); - let idx = arena.add(sort.into()); - let arena_bound = Bound::new(py, arena)?; - PySortArena::get(&arena_bound, py, idx).map(|a| a.into_any().unbind()) + + Self::create(py, sort.into()) + } + + /// [`PySort::__sort_arena__`] + /// + /// A class variable that holds onto a single persistent [`PySortArena`] + /// which holds all allocations of [`Sort`] and their corresponding [`PySort`] + /// during the lifetime of a python process + #[classattr] + fn __sort_arena__(py: Python<'_>) -> PyResult> { + Bound::new(py, PySortArena::new()) } } -#[pyclass(extends = PySortNode)] +#[pyclass(extends = PySort)] pub struct SortVar { #[pyo3(get)] name: Py, @@ -136,29 +202,65 @@ pub struct SortVar { #[pymethods] impl SortVar { - /* #[new] - fn new_(py: Python<'_>, id: Py) -> PyResult> { - let view = if let Ok(id) = id.extract::(py) { - let sort = Sort::Var(id); - Ok(sort.into_view()) - } else if let Ok(id_str) = id.cast_bound::(py) { - let id = Id::new(id_str.to_string()).map_err(PyValueError::new_err)?; - let sort = Sort::Var(id); - Ok(sort.into_view()) - } else { - Err(PyTypeError::new_err("")) - }?; - let view_bound = Bound::new(py, view)?; - create_node(&view_bound, 0) + fn new_(py: Python<'_>, id: &Bound<'_, PyAny>) -> PyResult> { + let id = Id::try_from(id)?; + let sort = Sort::Var(id); + + Ok(PySort::create(py, sort.into())? + .cast_into::()? + .into()) + } + + #[classattr] + fn __annotations__(py: Python<'_>) -> PyResult> { + let var_annotations = PyDict::new(py); + var_annotations.set_item("name", py.get_type::())?; + Ok(var_annotations) } - */ } -#[pyclass(extends = PySortNode)] +#[pyclass(extends = PySort)] pub struct SortApp { #[pyo3(get)] name: Py, #[pyo3(get)] args: Py, } + +#[pymethods] +impl SortApp { + #[new] + fn new_<'py>( + py: Python<'py>, + id: &Bound<'_, PyAny>, + args: &Bound<'_, PyTuple>, + ) -> PyResult> { + let id = Id::try_from(id)?; + + let args: Vec> = args + .iter() + .map(|obj| { + let node = obj.cast_into::(); + node.map(|arg| arg.borrow().get_inner(py)) + }) + .collect::, _>>()?; + + let sort = Sort::App { + id, + args: args.into(), + }; + + Ok(PySort::create(py, sort.into())? + .cast_into::()? + .into()) + } + + #[classattr] + fn __annotations__(py: Python<'_>) -> PyResult> { + let app_annotations = PyDict::new(py); + app_annotations.set_item("name", py.get_type::())?; + app_annotations.set_item("args", py.get_type::())?; + Ok(app_annotations) + } +} From 595506bc89a6a8c0662622af184ad871cb179a64 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 26 Feb 2026 19:03:21 -0600 Subject: [PATCH 10/11] Tests --- bindings/kframework_py/tests/test_kore.py | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/bindings/kframework_py/tests/test_kore.py b/bindings/kframework_py/tests/test_kore.py index fb25cc8..77a74d8 100644 --- a/bindings/kframework_py/tests/test_kore.py +++ b/bindings/kframework_py/tests/test_kore.py @@ -1,4 +1,4 @@ -from kframework_py.kore.syntax import Id +from kframework_py.kore.syntax import Id, Sort, SortVar, SortApp def test_id(): i = Id("foo") @@ -10,3 +10,22 @@ def test_id(): # TODO: Fix this! # assert a is b + +def test_sort(): + # Parsing + sort = Sort.parse("SortA{SortB{SortC}, SortD, SortE{SortF, SortG{}}}") + + # Getters and Constructors don't re-allocate + arg0 = sort.args[0] + arg1 = sort.args[1] + reused = SortApp("Reused", (arg0, arg1)) + assert arg0 is sort.args[0] + assert arg1 is reused.args[1] + + # Dataclass repr + expected_repr = "SortApp(name='SortB', args=(SortVar(name='SortC'),))" + assert arg0.__repr__() == expected_repr + + # Structural equivalence + app = SortApp("SortB", (SortVar("SortC"),)) + assert arg0 == app From 957f2b9c2f71aca1ab8eff9c3c9695659487c2cf Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 26 Feb 2026 19:20:39 -0600 Subject: [PATCH 11/11] Fixes/cleanups --- bindings/kframework_py/src/lib.rs | 2 +- kframework/src/bindings/python.rs | 27 ++++++++------------------- 2 files changed, 9 insertions(+), 20 deletions(-) diff --git a/bindings/kframework_py/src/lib.rs b/bindings/kframework_py/src/lib.rs index 1086aac..b8bb013 100644 --- a/bindings/kframework_py/src/lib.rs +++ b/bindings/kframework_py/src/lib.rs @@ -54,7 +54,7 @@ mod kframework_py { #[pymodule_export] use kframework::{ - bindings::python::{PySortNode, SortApp, SortVar}, + bindings::python::{PySort, SortApp, SortVar}, kore::Id, }; } diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs index 6c2bb1e..743c2d8 100644 --- a/kframework/src/bindings/python.rs +++ b/kframework/src/bindings/python.rs @@ -1,15 +1,10 @@ -#![allow(unused)] - -use std::{ - collections::HashMap, - sync::{Arc, Mutex}, -}; +use std::{collections::HashMap, sync::Arc}; use crate::kore::{Id, Sort}; use pyo3::{ - exceptions::{PyTypeError, PyValueError}, + exceptions::PyValueError, prelude::*, - types::{PyDict, PyList, PyString, PyTuple}, + types::{PyDict, PyString, PyTuple}, }; #[pymethods] @@ -71,11 +66,9 @@ impl PySortArena { self.cached_pys.push(None); if let Sort::App { args, .. } = &*sort { - let children = args - .iter() - // Add this sort's children to the arena as well - .map(|arg| self.add(arg.clone())) - .collect::>(); + for arg in args { + self.add(arg.clone()); + } } idx @@ -207,9 +200,7 @@ impl SortVar { let id = Id::try_from(id)?; let sort = Sort::Var(id); - Ok(PySort::create(py, sort.into())? - .cast_into::()? - .into()) + Ok(PySort::create(py, sort.into())?.cast_into::()?.into()) } #[classattr] @@ -251,9 +242,7 @@ impl SortApp { args: args.into(), }; - Ok(PySort::create(py, sort.into())? - .cast_into::()? - .into()) + Ok(PySort::create(py, sort.into())?.cast_into::()?.into()) } #[classattr]