diff --git a/Cargo.toml b/Cargo.toml index 0a5b9e5..d2a97e7 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,6 +2,7 @@ resolver = "2" members = [ + "bindings/kframework_py", "kframework", "kframework_ffi", ] @@ -20,3 +21,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/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..ba1b2e5 --- /dev/null +++ b/bindings/kframework_py/pyproject.toml @@ -0,0 +1,18 @@ +[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"] + +[dependency-groups] +dev = [ + "pytest>=8.3.5", +] diff --git a/bindings/kframework_py/src/lib.rs b/bindings/kframework_py/src/lib.rs new file mode 100644 index 0000000..b8bb013 --- /dev/null +++ b/bindings/kframework_py/src/lib.rs @@ -0,0 +1,62 @@ +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::*, types::IntoPyDict}; + + #[pymodule_init] + fn init(module: &Bound<'_, PyModule>) -> PyResult<()> { + create_sys_module(module, "kframework_py.kore.syntax")?; + + let py = module.py(); + let sortvar = module.getattr("SortVar")?; + let sortapp = module.getattr("SortApp")?; + + // 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())?; + dataclass.call((sortapp,), kwargs.as_ref())?; + Ok(()) + } + + #[pymodule_export] + use kframework::{ + bindings::python::{PySort, SortApp, SortVar}, + kore::Id, + }; + } + } +} diff --git a/bindings/kframework_py/tests/test_kore.py b/bindings/kframework_py/tests/test_kore.py new file mode 100644 index 0000000..77a74d8 --- /dev/null +++ b/bindings/kframework_py/tests/test_kore.py @@ -0,0 +1,31 @@ +from kframework_py.kore.syntax import Id, Sort, SortVar, SortApp + +def test_id(): + i = Id("foo") + + a = i.value + b = i.value + + assert a == "foo" + + # 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 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 = [] 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; diff --git a/kframework/src/bindings/python.rs b/kframework/src/bindings/python.rs new file mode 100644 index 0000000..743c2d8 --- /dev/null +++ b/kframework/src/bindings/python.rs @@ -0,0 +1,255 @@ +use std::{collections::HashMap, sync::Arc}; + +use crate::kore::{Id, Sort}; +use pyo3::{ + exceptions::PyValueError, + prelude::*, + types::{PyDict, PyString, PyTuple}, +}; + +#[pymethods] +impl Id { + #[new] + fn py_new(s: String) -> PyResult { + Self::new(s).map_err(PyValueError::new_err) + } + + #[getter(value)] + fn py_value(&self) -> &str { + self.value() + } +} + +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>, + // 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 { + pub fn new() -> Self { + Self::default() + } + + 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::::as_ptr(&sort) as usize, idx); + self.cached_pys.push(None); + + if let Sort::App { args, .. } = &*sort { + for arg in args { + self.add(arg.clone()); + } + } + + idx + } + + pub fn get(&self, idx: usize) -> Arc { + self.inners.get(idx).cloned().expect("Invalid node index") + } +} + +/// [`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, +} + +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()); + } + + // 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<'_, PySort> = match &*sort { + Sort::Var(id) => { + let var = SortVar { + name: PyString::new(py, id.value()).unbind(), + }; + Bound::new(py, (var, node))?.into_super() + } + Sort::App { id, args } => { + let children = args + .iter() + .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: args.into(), + }; + Bound::new(py, (app, node))?.into_super() + } + }; + + // 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) + } +} + +#[pymethods] +impl PySort { + #[staticmethod] + 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)?; + + 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 = PySort)] +pub struct SortVar { + #[pyo3(get)] + name: Py, +} + +#[pymethods] +impl SortVar { + #[new] + 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 = 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) + } +} 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 a1effe5..d0801c5 100644 --- a/kframework/src/kore/syntax.rs +++ b/kframework/src/kore/syntax.rs @@ -1,4 +1,7 @@ -#[derive(Debug, PartialEq, Eq)] +use std::sync::Arc; + +#[cfg_attr(feature = "python", pyo3::pyclass(from_py_object))] +#[derive(Clone, Debug, PartialEq, Eq)] pub struct Id(pub(crate) String); impl Id { @@ -24,8 +27,8 @@ impl Id { } } - pub fn value(self) -> String { - self.0 + pub fn value(&self) -> &str { + &self.0 } } @@ -304,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/src/lib.rs b/kframework/src/lib.rs index bdfddfd..a564109 100644 --- a/kframework/src/lib.rs +++ b/kframework/src/lib.rs @@ -1 +1,4 @@ pub mod kore; + +#[cfg(feature = "python")] +pub mod bindings; 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")?)],