mindxtrain/ui/reasoning.py

"""The reasoning pass — logic and Socratic questioning before the model answers.

This is the oldest idea in the house and the one that keeps being right: **aGLM is not a model.** It is
a layer that augments whatever model you have — Socratic questioning, truth tables, autoepistemic and
nonmonotonic revision, BDI. Public documentation: <https://rage.pythai.net>. The lineage:
`GATERAGE/aglm` (`logic.py`, `socratic.py`, `reasoning.py`, `epistemic.py`, `nonmonotonic.py`,
`bdi.py`) and its eighteen UIUX iterations, whose real contribution was the *shape*: the UI calls a
reasoning layer, never a model directly.

Two ways this module works, and it says which one ran:

1. **the real aGLM** — when `aglm` is importable (`pip install -e ~/aglm`, or `MINDXTRAIN_AGLM=/path`),
   its `LogicTables` and `SocraticReasoning` do the work.
2. **the in-house fallback** — a small, zero-dependency version of the same two moves, so the pass is
   never simply absent: extract the claims, ask the questions a sceptic would ask, and check the
   claims for contradiction.

The pass never answers for the model. It writes scaffolding into the prompt — the questions the answer
should survive — and the model still has to answer. That distinction is why it improves a small model
instead of flattering it.
"""
from __future__ import annotations

import os
import re
import sys
from dataclasses import dataclass, field
from typing import Any

DOCS = "https://rage.pythai.net"

_SENT = re.compile(r"(?<=[.!?])\s+")
_HEDGE = re.compile(r"\b(always|never|every|all|none|must|cannot|impossible|certainly|proves?)\b", re.I)
_CAUSAL = re.compile(r"\b(because|therefore|so|thus|hence|since|implies|means that)\b", re.I)
_QUANT = re.compile(r"\b(\d+(?:\.\d+)?%?|\d+x|[a-z]+ per [a-z]+)\b", re.I)


# ── the real layer, if it is installed ────────────────────────────────────────
def _aglm():
    """Import aGLM if it is reachable. Never raises; returns None when it is not."""
    extra = os.environ.get("MINDXTRAIN_AGLM")
    if extra and extra not in sys.path:
        sys.path.insert(0, extra)
    try:
        from logic import LogicTables  # type: ignore
        from socratic import SocraticReasoning  # type: ignore
        return {"LogicTables": LogicTables, "SocraticReasoning": SocraticReasoning}
    except Exception:
        return None


def available() -> dict[str, Any]:
    a = _aglm()
    return {"aglm": bool(a), "docs": DOCS,
            "note": ("the real aGLM layer is in use" if a else
                     "aGLM is not importable here — the in-house fallback runs instead "
                     "(set MINDXTRAIN_AGLM=/path/to/aglm to use the original)")}


# ── the in-house fallback: the same two moves, written out ────────────────────
@dataclass
class Pass:
    claims: list[str] = field(default_factory=list)
    questions: list[str] = field(default_factory=list)
    contradictions: list[str] = field(default_factory=list)
    source: str = "fallback"

    def as_prompt(self) -> str:
        """What gets prepended. Questions, not answers — the model still has to do the work."""
        if not (self.claims or self.questions):
            return ""
        out = ["Before answering, hold these in view."]
        if self.claims:
            out.append("Claims detected in the question:\n" + "\n".join(f"- {c}" for c in self.claims))
        if self.questions:
            out.append("Questions the answer should survive:\n" + "\n".join(f"- {q}" for q in self.questions))
        if self.contradictions:
            out.append("Possible contradiction:\n" + "\n".join(f"- {c}" for c in self.contradictions))
        out.append("Answer plainly. Where the evidence does not reach, say so.")
        return "\n\n".join(out)

    def summary(self) -> str:
        return (f"{len(self.claims)} claims · {len(self.questions)} questions"
                + (f" · {len(self.contradictions)} contradiction(s)" if self.contradictions else "")
                + f" · via {self.source}")


def _claims(text: str) -> list[str]:
    """Sentences that assert something — a quantity, a causal link, or an absolute."""
    out = []
    for s in _SENT.split((text or "").strip()):
        s = s.strip()
        if len(s) < 8:
            continue
        if _HEDGE.search(s) or _CAUSAL.search(s) or _QUANT.search(s) or s.endswith("."):
            out.append(s if len(s) < 240 else s[:237] + "…")
    return out[:6]


def _socratic(text: str, claims: list[str]) -> list[str]:
    """The questions a sceptic asks. Chosen by what the text actually contains, not a fixed list."""
    q: list[str] = []
    if _HEDGE.search(text or ""):
        q.append("The claim is absolute (always / never / all). Is there one counter-example?")
    if _CAUSAL.search(text or ""):
        q.append("A cause is asserted. What would be true if the cause were absent?")
    if _QUANT.search(text or ""):
        q.append("A number is used. Measured how, over what, and compared with what?")
    if claims:
        q.append("What would have to be true for the first claim to be false?")
    q.append("What is being assumed that has not been stated?")
    q.append("What would change the answer?")
    return q[:6]


def _negates(a: str, b: str) -> bool:
    """True when `a` is a negated form of something `b` asserts."""
    if "not" not in a and "n't" not in a:
        return False
    neg = a.replace(" not ", " ").replace("n't", "").strip()
    return bool(neg) and neg in b


def _contradictions(claims: list[str]) -> list[str]:
    """A truth-table check in miniature: a claim and its negation both asserted.

    Tested in both directions: which of the pair the author happened to write first
    has no bearing on whether the two can both hold.
    """
    out = []
    norm = [re.sub(r"\s+", " ", c.lower().strip(" .")) for c in claims]
    for i, a in enumerate(norm):
        for b in norm[i + 1:]:
            if a == b:
                continue
            if _negates(a, b) or _negates(b, a):
                out.append(f"“{a}” and “{b}” cannot both hold")
    return out[:3]


def run(text: str, *, use_aglm: bool = True) -> Pass:
    """The pass. Uses aGLM when importable, the fallback otherwise, and records which."""
    text = (text or "").strip()
    if not text:
        return Pass(source="empty")
    if use_aglm:
        a = _aglm()
        if a:
            try:
                lt = a["LogicTables"]()
                sr = a["SocraticReasoning"]()
                claims = _claims(text)
                for c in claims:
                    try:
                        sr.add_premise(c)
                    except Exception:
                        pass
                try:
                    sr.draw_conclusion()
                except Exception:
                    pass
                qs = []
                for attr in ("questions", "socratic_questions", "log"):
                    v = getattr(sr, attr, None)
                    if isinstance(v, list) and v:
                        qs = [str(x)[:200] for x in v[:6]]
                        break
                contradictions = []
                try:
                    valid = lt.validate_truth(" and ".join(claims[:2])) if claims else None
                    if valid is False:
                        contradictions.append("LogicTables reports the conjunction of the first claims as invalid")
                except Exception:
                    pass
                return Pass(claims=claims, questions=qs or _socratic(text, claims),
                            contradictions=contradictions, source="aGLM")
            except Exception:
                pass
    claims = _claims(text)
    return Pass(claims=claims, questions=_socratic(text, claims),
                contradictions=_contradictions(claims), source="fallback")