Moved JAX object storage fn to shared utils

docs/api_reference.md

@@ -11,7 +11,7 @@ All public symbols are importable from the top-level `pystl` package.
 from pystl import (
     Predicate, Interval,
     Formula, Not, And, Or, Always, Eventually, Until,
-    create_semantics, registry,
+    export_formula, create_semantics, registry,
 )
 ```
 
@@ -79,6 +79,16 @@ Evaluate robustness and the gradient w.r.t. the full signal trace.
 
 This is only supported by some semantics/backends (currently: D-GMSR with the NumPy backend). For JAX/PyTorch backends, prefer their native autodiff (`jax.grad` / `torch.autograd`).
 
+### `Formula.export(format="text")`
+
+Export the formula syntax tree to a string format, independent of semantics/backend.
+
+- `format="text"`: plain text (`always`, `eventually`, `until`)
+- `format="markdown"`: Markdown-friendly notation (`G`, `F`, `U`)
+- `format="latex"`: LaTeX notation (`\square`, `\lozenge`, `\mathcal{U}`)
+
+`format` aliases are accepted: `plain`, `txt`, `md`, `tex`.
+
 ### Operator shorthands
 
 | Expression | Equivalent |
@@ -90,6 +100,10 @@ This is only supported by some semantics/backends (currently: D-GMSR with the Nu
 | `phi.eventually(interval)` | `Eventually(phi, interval)` |
 | `phi1.until(phi2, interval)` | `Until(phi1, phi2, interval)` |
 
+### `export_formula(formula, format="text")`
+
+Module-level helper equivalent to `formula.export(format=...)`.
+
 ---
 
 ## `Not`

docs/unified_api.md

@@ -63,6 +63,16 @@ phi.until(psi, Interval(0, 5))
 
 Tuple shorthand is also accepted: `phi.always((0, 4))`.
 
+### Formula export
+
+Formula syntax can be exported without selecting any backend:
+
+```python
+phi.export("text")      # always/eventually/until
+phi.export("markdown")  # G/F/U
+phi.export("latex")     # \square/\lozenge/\mathcal{U}
+```
+
 #### Weighted operators
 
 `And`, `Or`, `always`, and `eventually` accept an optional `weights` argument to scale the contribution of each operand or time step. Weights are semantics-dependent — they are used by semantics that support them (e.g., AGM, D-GMSR) and ignored by those that don't (e.g., Classical).

pystl/__init__.py

@@ -1,4 +1,16 @@
-from .api import Or, And, Not, Until, Always, Formula, Interval, Predicate, Eventually
+from .api import (
+    Or,
+    And,
+    Not,
+    Until,
+    Always,
+    Formula,
+    Interval,
+    Predicate,
+    Eventually,
+    FormulaFormat,
+    export_formula,
+)
 from .semantics import (
     CtstlSemantics,
     DgmsrSemantics,
@@ -15,6 +27,7 @@
 
 __all__ = [
     "Formula",
+    "FormulaFormat",
     "Predicate",
     "Not",
     "And",
@@ -23,6 +36,7 @@
     "Eventually",
     "Until",
     "Interval",
+    "export_formula",
     "ClassicRobustSemantics",
     "SmoothRobustSemantics",
     "AgmRobustSemantics",

pystl/api.py

@@ -12,7 +12,7 @@
 from __future__ import annotations
 
 from abc import ABC, abstractmethod
-from typing import Any, Callable, Optional, Sequence, TypeAlias
+from typing import Any, Literal, Callable, Optional, Sequence, TypeAlias
 from dataclasses import dataclass
 
 import numpy as np
@@ -23,6 +23,7 @@
 Signal: TypeAlias = NDArray[np.float64]
 PredicateFn = Callable[[Signal, int], Any]
 PredicateGradFn = Callable[[Signal, int], NDArray[np.float64] | Sequence[float]]
+FormulaFormat: TypeAlias = Literal["text", "markdown", "latex"]
 
 
 @dataclass(frozen=True)
@@ -76,6 +77,11 @@ def evaluate_with_grad(
         value, grad = evaluator(self, signal, t=t, **kwargs)
         return value, np.asarray(grad, dtype=float)
 
+    def export(self, fmt: str = "text", **kwargs: Any) -> str:
+        """Export a formula as plain text, Markdown, or LaTeX."""
+
+        return export_formula(self, fmt=fmt, **kwargs)
+
     def __and__(self, other: "Formula") -> "And":
         return And(self, other)
 
@@ -296,9 +302,131 @@ def evaluate(self, signal: Signal, semantics: Semantics[Any], t: int = 0) -> Any
         )
 
 
+def _resolve_export_format(fmt: str, kwargs: dict[str, Any]) -> str:
+    format_alias = kwargs.pop("format", None)
+    if format_alias is not None:
+        if fmt != "text":
+            raise TypeError("Use either 'fmt' or 'format', not both.")
+        if not isinstance(format_alias, str):
+            raise TypeError("'format' must be a string.")
+        fmt = format_alias
+    if kwargs:
+        unknown = ", ".join(sorted(kwargs))
+        raise TypeError(f"Unexpected keyword argument(s): {unknown}.")
+    return fmt
+
+
+def _normalize_format(format_name: str) -> FormulaFormat:
+    key = format_name.strip().lower()
+    aliases: dict[str, FormulaFormat] = {
+        "text": "text",
+        "plain": "text",
+        "plaintext": "text",
+        "txt": "text",
+        "markdown": "markdown",
+        "md": "markdown",
+        "latex": "latex",
+        "tex": "latex",
+    }
+    if key not in aliases:
+        msg = "Unsupported export format. Use one of: 'text', 'markdown', 'latex'."
+        raise ValueError(msg)
+    return aliases[key]
+
+
+def _format_interval(interval: Interval, fmt: FormulaFormat) -> str:
+    if interval.end is None:
+        end = r"\infty" if fmt == "latex" else "inf"
+    else:
+        end = str(interval.end)
+    return f"[{interval.start}, {end}]"
+
+
+def _escape_latex(text: str) -> str:
+    chars = {
+        "\\": r"\textbackslash{}",
+        "{": r"\{",
+        "}": r"\}",
+        "_": r"\_",
+        "^": r"\^{}",
+        "#": r"\#",
+        "$": r"\$",
+        "%": r"\%",
+        "&": r"\&",
+        "~": r"\~{}",
+    }
+    return "".join(chars.get(ch, ch) for ch in text)
+
+
+def _wrap(expr: str, fmt: FormulaFormat) -> str:
+    if fmt == "latex":
+        return rf"\left({expr}\right)"
+    return f"({expr})"
+
+
+def _format_formula(formula: Formula, fmt: FormulaFormat) -> str:
+    if isinstance(formula, Predicate):
+        return _escape_latex(formula.name) if fmt == "latex" else formula.name
+
+    if isinstance(formula, Not):
+        child = _format_formula(formula.child, fmt)
+        if fmt == "latex":
+            return rf"\neg{_wrap(child, fmt)}"
+        return f"not {_wrap(child, fmt)}"
+
+    if isinstance(formula, And):
+        children = [_format_formula(child, fmt) for child in formula.children]
+        joiner = r" \wedge " if fmt == "latex" else " and "
+        return _wrap(joiner.join(children), fmt)
+
+    if isinstance(formula, Or):
+        children = [_format_formula(child, fmt) for child in formula.children]
+        joiner = r" \vee " if fmt == "latex" else " or "
+        return _wrap(joiner.join(children), fmt)
+
+    if isinstance(formula, Always):
+        child = _format_formula(formula.child, fmt)
+        interval = _format_interval(formula.interval, fmt)
+        if fmt == "text":
+            return f"always{interval}{_wrap(child, fmt)}"
+        if fmt == "markdown":
+            return f"G{interval}{_wrap(child, fmt)}"
+        return rf"\square_{{{interval}}}{_wrap(child, fmt)}"
+
+    if isinstance(formula, Eventually):
+        child = _format_formula(formula.child, fmt)
+        interval = _format_interval(formula.interval, fmt)
+        if fmt == "text":
+            return f"eventually{interval}{_wrap(child, fmt)}"
+        if fmt == "markdown":
+            return f"F{interval}{_wrap(child, fmt)}"
+        return rf"\lozenge_{{{interval}}}{_wrap(child, fmt)}"
+
+    if isinstance(formula, Until):
+        left = _format_formula(formula.left, fmt)
+        right = _format_formula(formula.right, fmt)
+        interval = _format_interval(formula.interval, fmt)
+        if fmt == "text":
+            return f"{_wrap(left, fmt)} until{interval} {_wrap(right, fmt)}"
+        if fmt == "markdown":
+            return f"{_wrap(left, fmt)} U{interval} {_wrap(right, fmt)}"
+        return rf"{_wrap(left, fmt)}\ \mathcal{{U}}_{{{interval}}}\ {_wrap(right, fmt)}"
+
+    raise TypeError(f"Unsupported formula node: {type(formula)!r}")
+
+
+def export_formula(formula: Formula, *, fmt: str = "text", **kwargs: Any) -> str:
+    """Export a formula as plain text, Markdown, or LaTeX."""
+
+    selected_fmt = _resolve_export_format(fmt, kwargs)
+    normalized_fmt = _normalize_format(selected_fmt)
+    return _format_formula(formula, normalized_fmt)
+
+
 __all__ = [
     "Signal",
     "PredicateFn",
+    "FormulaFormat",
     "Interval",
     "Formula",
     "Predicate",
@@ -308,4 +436,5 @@ def evaluate(self, signal: Signal, semantics: Semantics[Any], t: int = 0) -> Any
     "Always",
     "Eventually",
     "Until",
+    "export_formula",
 ]

tests/test_formula_export.py

@@ -0,0 +1,41 @@
+import pytest
+
+from pystl import Predicate, export_formula
+
+
+def test_formula_export_text_markdown_and_latex_tokens() -> None:
+    p1 = Predicate("speed_ok")
+    p2 = Predicate("alt_ok")
+    phi = (p1 & ~p2).always((0, 2)).eventually((1, 3))
+
+    text = phi.export("text")
+    markdown = phi.export("markdown")
+    latex = phi.export("latex")
+
+    assert text == "eventually[1, 3](always[0, 2]((speed_ok and not (alt_ok))))"
+    assert markdown == "F[1, 3](G[0, 2]((speed_ok and not (alt_ok))))"
+    assert r"\square_{[0, 2]}" in latex
+    assert r"\lozenge_{[1, 3]}" in latex
+    assert r"speed\_ok" in latex
+    assert r"alt\_ok" in latex
+
+
+def test_formula_export_until_and_open_interval() -> None:
+    p1 = Predicate("left")
+    p2 = Predicate("right")
+    phi = p1.until(p2, interval=(0, None))
+
+    assert phi.export("text") == "(left) until[0, inf] (right)"
+    assert phi.export("markdown") == "(left) U[0, inf] (right)"
+    assert r"\mathcal{U}_{[0, \infty]}" in phi.export("latex")
+
+
+def test_export_formula_aliases_and_validation() -> None:
+    phi = Predicate("x").always((0, 1))
+
+    assert export_formula(phi, format="md") == phi.export("markdown")
+    assert export_formula(phi, format="plain") == phi.export("text")
+    assert export_formula(phi, format="tex") == phi.export("latex")
+
+    with pytest.raises(ValueError):
+        phi.export("html")