orchestrata_ultimate.factory.amendment.syntactic

Reference › orchestrata_ultimate › factory › amendment › syntactic

syntactic is step 1 of the amendment classifier (SPEC-033 row B16, ADR-0020): the fragment of direction classification that clause shape alone decides. Its docstring gives a monotonicity argument for each change kind. Removing a clause or adding a body conjunct can only shrink what a predicate accepts, so both are tightening. Adding a clause or removing a conjunct can only widen it, so both are loosening. Any other change (argument patterns, reordered goals, a replaced body) has no such argument and is undetermined.

The parser is structural, not a full Prolog parser. parse_clauses masks comments and quoted strings with mask_non_code from scripts.prolog_meta_lint, splits text into clauses on a top-level full stop (_split_top_level_clauses), finds each clause's :- (_find_top_level_neck), splits the body into goals on top-level commas (_top_level_split) and groups clauses by name/arity (_predicate_identity) into ClauseRepr records. diff_clauses compares old and new text per predicate, matching clauses by head text, and returns a list of ClauseChange objects; a change confined to a comment produces none. _classify_body_pair uses _body_is_subsequence to tell an added or removed conjunct from another edit. classify_syntactic maps the changes to a Direction. This proves only the local clause claim, which is why classify still runs the ledger and coupling checks afterwards. Data types come from models; tests are in tests/factory/test_amendment_syntactic.py.

At a glance

Class diagram

Dependency diagram

API

Classes

ClauseRepr (dataclass)

Decorators: dataclass(frozen=True) · Line 61

One parsed clause: its predicate identity, head text, and ordered, whitespace-normalized body goals (empty tuple for a fact or a bare directive).

Functions

Source

Permalink: https://gitlab.com/MSamy/orchestrata-ultimate-architecture/-/blob/a4cbc2bdf/src/orchestrata_ultimate/factory/amendment/syntactic.py

"""The decidable fragment of amendment-direction classification (ADR-0020 step 1).

**Monotonicity argument** (why each :class:`~...models.ChangeKind` is provably
tightening or provably loosening, with no ledger evidence required):

- ``CLAUSE_REMOVED`` -- a predicate's extension is the union of what each of
  its clauses accepts. Removing a clause can only shrink that union: any fact
  the predicate still accepts, it accepted before. Provably **tightening**.
- ``BODY_CONJUNCT_ADDED`` -- a rule's body is a conjunction; the set of
  bindings satisfying ``G1, ..., Gn, Gnew`` is a subset of the set satisfying
  ``G1, ..., Gn`` (conjunction can only add constraints, never relax one --
  Prolog has no way to make ``,`` more permissive by adding a conjunct).
  Provably **tightening**, PROVIDED the added conjunct itself does not call
  new/changed machinery that shifts the picture -- which is exactly the
  "loosens only in unvisited fact-space" hole ADR-0020 names; this module
  proves only the LOCAL clause-shape claim, never global semantics. That is
  why :mod:`~orchestrata_ultimate.factory.amendment.classify` still runs the
  ledger screen and coupling check even after a syntactic TIGHTENING verdict.
- ``CLAUSE_ADDED`` -- symmetric to ``CLAUSE_REMOVED``: a wholly new clause can
  only add to the predicate's extension. Provably **loosening**.
- ``BODY_CONJUNCT_REMOVED`` -- symmetric to ``BODY_CONJUNCT_ADDED``: dropping
  a conjunct can only admit bindings the old body rejected. Provably
  **loosening**.
- ``BODY_OTHER`` -- anything else (argument-pattern changes, goal reordering
  that is not a pure subsequence extension/reduction, a body replaced outright)
  has no monotonicity argument available from clause SHAPE alone --
  **undetermined** by construction, not "assumed safe".

**Parser limits** (this is structural, not a full Prolog parser): clauses are
split on a top-level ``.`` (matching :mod:`scripts.prolog_meta_lint`'s
convention -- terminator followed by whitespace/EOF, at paren/bracket depth
0, with the ``=..`` univ-operator's second dot excluded). Body goals are
split on top-level ``,`` -- this is exactly the ADR-0020 caveat: ``,`` is
Prolog's conjunction operator and also its argument separator, and this
module treats every top-level comma in the body as conjunction (correct for
governance-rulebase clauses, which do not nest control constructs like
``;``/``->`` at the top level of a body goal list; a goal such as
``(A -> B ; C)`` is parenthesized and so counted as ONE goal, not three).
Comments and quoted-string content are masked to blank (via
:func:`scripts.prolog_meta_lint.mask_non_code`) before any of this -- a change
confined to a comment produces no :class:`~...models.ClauseChange` at all.
"""

from __future__ import annotations

import itertools
import re
from dataclasses import dataclass

from orchestrata_ultimate.factory.amendment.models import (
    ChangeKind,
    ClauseChange,
    Direction,
)

_HEAD_NAME_RE = re.compile(r"^\s*(?:[a-z_][A-Za-z0-9_]*:)?([a-z][A-Za-z0-9_]*)")
_WHITESPACE_RE = re.compile(r"\s+")


@dataclass(frozen=True)
class ClauseRepr:
    """One parsed clause: its predicate identity, head text, and ordered,
    whitespace-normalized body goals (empty tuple for a fact or a bare
    directive)."""

    predicate: str  # "name/arity"
    head_text: str  # normalized (whitespace-collapsed) head, args included
    body_goals: tuple[str, ...]
    raw: str  # normalized full clause text, for CLAUSE_ADDED/REMOVED detail


def _normalize_ws(text: str) -> str:
    return _WHITESPACE_RE.sub(" ", text).strip()


def _top_level_split(text: str, sep: str) -> list[str]:
    """Split ``text`` on ``sep`` at paren/bracket/brace depth 0."""
    parts: list[str] = []
    depth = 0
    start = 0
    for i, c in enumerate(text):
        if c in "([{":
            depth += 1
        elif c in ")]}":
            depth -= 1
        elif c == sep and depth == 0:
            parts.append(text[start:i])
            start = i + 1
    parts.append(text[start:])
    return parts


def _split_top_level_clauses(masked: str) -> list[str]:
    """Return clause texts (terminating '.' excluded), same convention as
    ``scripts.prolog_meta_lint._split_clauses``: a '.' at paren depth 0
    immediately followed by whitespace/EOF, excluding the ``=..`` univ
    operator's second dot."""
    clauses: list[str] = []
    depth = 0
    n = len(masked)
    clause_start = 0
    i = 0
    while i < n:
        c = masked[i]
        if c in "([{":
            depth += 1
        elif c in ")]}":
            depth -= 1
        elif c == "." and depth == 0:
            nxt = masked[i + 1] if i + 1 < n else ""
            is_univ_second_dot = i >= 2 and masked[i - 2 : i] == "=."
            if (nxt == "" or nxt.isspace()) and not is_univ_second_dot:
                clause_text = masked[clause_start:i]
                if clause_text.strip():
                    clauses.append(clause_text)
                clause_start = i + 1
        i += 1
    tail = masked[clause_start:n]
    if tail.strip():
        clauses.append(tail)
    return clauses


def _find_top_level_neck(clause: str) -> int:
    """Index of the clause's own top-level ``:-``, or -1 (a fact)."""
    depth = 0
    n = len(clause)
    i = 0
    while i < n:
        c = clause[i]
        if c in "([{":
            depth += 1
        elif c in ")]}":
            depth -= 1
        elif depth == 0 and clause[i : i + 2] == ":-":
            return i
        i += 1
    return -1


def _predicate_identity(head_text: str) -> str:
    """``name/arity`` for a head text, e.g. ``foo(X, Y)`` -> ``"foo/2"``,
    a bare atom head (no parens) -> arity 0."""
    m = _HEAD_NAME_RE.match(head_text)
    name = m.group(1) if m else "?"
    paren = head_text.find("(")
    if paren == -1:
        return f"{name}/0"
    # Match the closing paren for the arg list, respecting nesting.
    depth = 0
    end = -1
    for i in range(paren, len(head_text)):
        if head_text[i] == "(":
            depth += 1
        elif head_text[i] == ")":
            depth -= 1
            if depth == 0:
                end = i
                break
    args_text = head_text[paren + 1 : end] if end != -1 else ""
    if not args_text.strip():
        return f"{name}/0"
    args = [a for a in _top_level_split(args_text, ",") if a.strip()]
    return f"{name}/{len(args)}"


def parse_clauses(pl_text: str) -> dict[str, list[ClauseRepr]]:
    """Parse ``pl_text`` into ``{predicate: [ClauseRepr, ...]}``.

    Comments/quoted-literal content is masked to blank first (see module
    docstring for the parser's limits).
    """
    from scripts.prolog_meta_lint import mask_non_code

    masked = mask_non_code(pl_text)
    by_predicate: dict[str, list[ClauseRepr]] = {}
    for clause_text in _split_top_level_clauses(masked):
        stripped = clause_text.lstrip()
        if stripped.startswith(":-"):
            continue  # a bare directive has no head; out of scope for diffing
        neck = _find_top_level_neck(clause_text)
        if neck == -1:
            head_text = clause_text
            body_goals: tuple[str, ...] = ()
        else:
            head_text = clause_text[:neck]
            body_text = clause_text[neck + 2 :]
            goals = [_normalize_ws(g) for g in _top_level_split(body_text, ",")]
            body_goals = tuple(g for g in goals if g)
        head_norm = _normalize_ws(head_text)
        predicate = _predicate_identity(head_norm)
        raw = _normalize_ws(clause_text)
        by_predicate.setdefault(predicate, []).append(
            ClauseRepr(
                predicate=predicate,
                head_text=head_norm,
                body_goals=body_goals,
                raw=raw,
            )
        )
    return by_predicate


def _body_is_subsequence(shorter: tuple[str, ...], longer: tuple[str, ...]) -> bool:
    """True iff ``shorter`` is a (not-necessarily-contiguous) subsequence of
    ``longer``, in order. The standard greedy two-pointer test -- correct
    regardless of duplicate goals, since matching the earliest available
    occurrence of each element of ``shorter`` never forecloses a later match
    (a textbook subsequence fact, not a heuristic)."""
    pos = 0
    n = len(longer)
    for goal in shorter:
        while pos < n and longer[pos] != goal:
            pos += 1
        if pos == n:
            return False
        pos += 1
    return True


def _classify_body_pair(
    old_goals: tuple[str, ...], new_goals: tuple[str, ...]
) -> ChangeKind | None:
    """Classify one matched clause's body change; ``None`` means "unchanged"
    (no :class:`~...models.ClauseChange` should be emitted for this pair)."""
    if old_goals == new_goals:
        return None
    if len(new_goals) > len(old_goals) and _body_is_subsequence(old_goals, new_goals):
        return ChangeKind.BODY_CONJUNCT_ADDED
    if len(new_goals) < len(old_goals) and _body_is_subsequence(new_goals, old_goals):
        return ChangeKind.BODY_CONJUNCT_REMOVED
    return ChangeKind.BODY_OTHER


def _detail_for_body_change(
    kind: ChangeKind, old_goals: tuple[str, ...], new_goals: tuple[str, ...]
) -> str:
    if kind == ChangeKind.BODY_CONJUNCT_ADDED:
        added = [g for g in new_goals if g not in old_goals]
        return f"added conjunct(s): {', '.join(added)}"
    if kind == ChangeKind.BODY_CONJUNCT_REMOVED:
        removed = [g for g in old_goals if g not in new_goals]
        return f"removed conjunct(s): {', '.join(removed)}"
    return f"body changed: '{', '.join(old_goals)}' -> '{', '.join(new_goals)}'"


def diff_clauses(old_text: str, new_text: str) -> list[ClauseChange]:
    """Diff ``old_text`` -> ``new_text`` clause-by-clause, per predicate.

    Within a predicate, clauses are matched by ``head_text`` (positionally,
    for the rare case of a repeated head across clauses -- e.g. guard-style
    clauses). Unmatched old clauses are ``CLAUSE_REMOVED``; unmatched new
    clauses are ``CLAUSE_ADDED``; matched pairs with an unchanged body
    produce no entry; matched pairs with a changed body are classified per
    :func:`_classify_body_pair`.
    """
    old_by_pred = parse_clauses(old_text)
    new_by_pred = parse_clauses(new_text)
    return list(
        itertools.chain.from_iterable(
            _diff_predicate(
                predicate,
                old_by_pred.get(predicate, []),
                new_by_pred.get(predicate, []),
            )
            for predicate in sorted(set(old_by_pred) | set(new_by_pred))
        )
    )


def _group_by_head(clauses: list[ClauseRepr]) -> dict[str, list[ClauseRepr]]:
    grouped: dict[str, list[ClauseRepr]] = {}
    for clause in clauses:
        grouped.setdefault(clause.head_text, []).append(clause)
    return grouped


def _diff_predicate(
    predicate: str,
    old_clauses: list[ClauseRepr],
    new_clauses: list[ClauseRepr],
) -> list[ClauseChange]:
    """Diff one predicate's clauses, matched by ``head_text`` (positionally,
    for the rare case of a repeated head -- e.g. guard-style clauses)."""
    changes: list[ClauseChange] = []
    old_by_head = _group_by_head(old_clauses)
    new_by_head = _group_by_head(new_clauses)
    for head_text in sorted(set(old_by_head) | set(new_by_head)):
        olds = old_by_head.get(head_text, [])
        news = new_by_head.get(head_text, [])
        paired = min(len(olds), len(news))
        for i in range(paired):
            kind = _classify_body_pair(olds[i].body_goals, news[i].body_goals)
            if kind is None:
                continue
            detail = _detail_for_body_change(
                kind, olds[i].body_goals, news[i].body_goals
            )
            changes.append(ClauseChange(predicate=predicate, kind=kind, detail=detail))
        changes.extend(
            ClauseChange(
                predicate=predicate,
                kind=ChangeKind.CLAUSE_REMOVED,
                detail=f"removed clause: {extra_old.raw}",
            )
            for extra_old in olds[paired:]
        )
        changes.extend(
            ClauseChange(
                predicate=predicate,
                kind=ChangeKind.CLAUSE_ADDED,
                detail=f"added clause: {extra_new.raw}",
            )
            for extra_new in news[paired:]
        )
    return changes


def classify_syntactic(changes: list[ClauseChange]) -> Direction:
    """The ADR-0020 step-1 syntactic sufficient condition.

    Provably **tightening** iff every change is a
    ``CLAUSE_REMOVED``/``BODY_CONJUNCT_ADDED`` (each only ever removes
    solutions -- see module docstring). Provably **loosening** iff every
    change is a ``CLAUSE_ADDED``/``BODY_CONJUNCT_REMOVED``. A mix of both
    kinds, or any ``BODY_OTHER``, is **undetermined** -- the syntactic test
    cannot prove a direction, so it does not claim one.

    No changes at all (``changes == []``) is vacuously tightening: nothing
    was added anywhere, so nothing was newly accepted.
    """
    if not changes:
        return Direction.TIGHTENING
    kinds = {c.kind for c in changes}
    tightening_kinds = {ChangeKind.CLAUSE_REMOVED, ChangeKind.BODY_CONJUNCT_ADDED}
    loosening_kinds = {ChangeKind.CLAUSE_ADDED, ChangeKind.BODY_CONJUNCT_REMOVED}
    if kinds <= tightening_kinds:
        return Direction.TIGHTENING
    if kinds <= loosening_kinds:
        return Direction.LOOSENING
    return Direction.UNDETERMINED