arborist/tests/test_claim_pack.py

"""Tests for the claim-pack source (Ticket #000029).

Covers the lenient JSON parser, document grain (one Document per
record), URI stability, edge emission for pillar-level cross-bundle
references, and metadata-sidecar contents.

No live JSON file from ``~/Downloads`` is read here. Fixtures are
in-test strings so the tests run anywhere.
"""

from __future__ import annotations

import json

import pytest

from arborist.document import Edge
from arborist.sources.claim_pack import (
    ClaimPackSource,
    _parse_lenient,
    _resolve_reference,
    _slugify,
)


# A minimal axiom bundle that mirrors the v2 pack's shape: markdown fence,
# a mix of properly-escaped (`\\to`) and lone-LaTeX (`\heart`) backslashes,
# one pillar with one axiom, and a pillar-level provenance.references
# pointing at the theorem bundle.
#
# Lone-backslash fields (`\heart`, `\Sigma`) trigger the lenient escape
# pass; double-backslash fields (`\\to`) are already legal JSON.
_MINI_AXIOM_BUNDLE = r"""```json
{
  "metadata": {
    "version": "1.0.5",
    "artifact_id": "test-axiom-bundle"
  },
  "pillars": {
    "I": {
      "title": "Logic Axioms (test)",
      "description": "Test pillar.",
      "provenance": {
        "delta": "\Sigma_1 \heart I",
        "nablaVerbose": "Sum from one to pillar one.",
        "references": [
          "theoremg4.json:pillar.I.logic.excludedMiddle"
        ]
      },
      "axioms": [
        {
          "name": "Axiom of Implication Introduction",
          "runicLabel": "ᚴᚵ",
          "delta": "A \\to (B \\to A)",
          "nablaVerbose": "Establishes that a true proposition is implied by any premise.",
          "nablaConcise": "A implies (B implies A).",
          "formal_language": "Propositional logic with implication (\\to)",
          "role": "Foundation for constructing implications.",
          "status": "Non-controversial.",
          "source_reference": "Mendelson 1997",
          "date_of_introduction": "1997",
          "foundational_group": "Classical First-Order Logic",
          "category": "Foundations of Logic",
          "subfield": "Propositional Logic"
        }
      ]
    }
  }
}
```"""

# A matching theorem bundle. References axiom-bundle pillar I at the pillar
# level. Has one theorem named "Law of Excluded Middle" so the cross-ref
# from the axiom bundle's `pillar.I.logic.excludedMiddle` resolves to the
# theorem record's URI.
_MINI_THEOREM_BUNDLE = r"""```json
{
  "metadata": {
    "version": "1.0.5",
    "artifact_id": "test-theorem-bundle"
  },
  "pillars": {
    "I": {
      "title": "Logic Theorems (test)",
      "description": "Test pillar.",
      "provenance": {
        "delta": "\Theta_1 \heart I",
        "nablaVerbose": "Sum from one to pillar one of the theorems.",
        "references": ["axiomsg4.json:pillar.I"]
      },
      "theorems": [
        {
          "name": "Law of Excluded Middle",
          "runicLabel": "ᚴᚵ",
          "delta": "A \\lor \\neg A",
          "nablaVerbose": "Either A or not A.",
          "nablaConcise": "A or not A.",
          "formal_language": "Propositional logic",
          "role": "Establishes binarity.",
          "source_reference": "Mendelson 1997",
          "date_of_introduction": "Ancient",
          "foundational_group": "Classical First-Order Logic",
          "category": "Foundations of Logic",
          "subfield": "Propositional Logic"
        }
      ]
    }
  }
}
```"""


# ---------------------------------------------------------------------------
# _parse_lenient
# ---------------------------------------------------------------------------


def test_parse_lenient_strips_fence_and_escapes_backslashes():
    bundle = _parse_lenient(_MINI_AXIOM_BUNDLE)
    assert bundle["metadata"]["version"] == "1.0.5"
    delta = bundle["pillars"]["I"]["axioms"][0]["delta"]
    # The lone-backslash escape preserves the LaTeX as a literal string.
    assert delta == r"A \to (B \to A)"


def test_parse_lenient_raises_on_malformed():
    with pytest.raises(json.JSONDecodeError):
        _parse_lenient("{not valid json")


def test_parse_lenient_handles_no_fence():
    raw = '{"metadata": {"version": "0.1"}, "pillars": {}}'
    out = _parse_lenient(raw)
    assert out["metadata"]["version"] == "0.1"


# ---------------------------------------------------------------------------
# _slugify
# ---------------------------------------------------------------------------


def test_slugify_strips_punctuation_and_diacritics():
    # Plain ASCII apostrophe is a non-slug char → produces a separator.
    assert _slugify("Pasch's Axiom") == "pasch-s-axiom"
    # Smart quote U+2019 has no NFKD decomposition AND drops on ASCII strip,
    # so neighboring letters collapse — the index in the URI disambiguates
    # any same-slug records inside one pillar.
    assert _slugify("Hilbert’s") == "hilberts"
    # Greek letters drop on ASCII strip; the dash survives as a separator.
    assert _slugify("β-Reduction") == "reduction"
    assert _slugify("") == "unnamed"
    # Sanity check: parens and spaces collapse to single dashes.
    assert _slugify("Newton's First Law (Inertia)") == "newton-s-first-law-inertia"


# ---------------------------------------------------------------------------
# _resolve_reference
# ---------------------------------------------------------------------------


def test_resolve_reference_pillar_only(tmp_path):
    bundles = {
        "axiomsg4-v2": _parse_lenient(_MINI_AXIOM_BUNDLE),
        "theoremsg4-v2": _parse_lenient(_MINI_THEOREM_BUNDLE),
    }
    matched, uri = _resolve_reference("axiomsg4.json:pillar.I", bundles)
    assert matched == "axiomsg4-v2"
    assert uri == "claim-pack://axiomsg4-v2/pillar/I"


def test_resolve_reference_resolves_named_leaf():
    bundles = {
        "axiomsg4-v2": _parse_lenient(_MINI_AXIOM_BUNDLE),
        "theoremsg4-v2": _parse_lenient(_MINI_THEOREM_BUNDLE),
    }
    matched, uri = _resolve_reference(
        "theoremg4.json:pillar.I.logic.excludedMiddle", bundles
    )
    assert matched == "theoremsg4-v2"
    # By-slug match against the theorem's name ("Law of Excluded Middle")
    # uses the LEAF of the reference path ("excludedMiddle") which slugs
    # to "excludedmiddle" — and the theorem's own slug is
    # "law-of-excluded-middle". They differ. Verify the helper falls back
    # to a pillar-level pointer rather than fabricating a wrong record URI.
    assert uri == "claim-pack://theoremsg4-v2/pillar/I"


def test_resolve_reference_unknown_bundle():
    bundles = {"axiomsg4-v2": _parse_lenient(_MINI_AXIOM_BUNDLE)}
    matched, uri = _resolve_reference(
        "unknownpack.json:pillar.X.foo.bar", bundles
    )
    assert matched is None
    # When nothing resolves, the original ref string falls through.
    assert uri == "unknownpack.json:pillar.X.foo.bar"


# ---------------------------------------------------------------------------
# ClaimPackSource — end-to-end iter_documents
# ---------------------------------------------------------------------------


def _write_bundles(tmp_path):
    """Helper: write the two mini bundles into tmp_path with stable names."""
    axiom_path = tmp_path / "axiomsg4-v2.json"
    theorem_path = tmp_path / "theoremsg4-v2.json"
    axiom_path.write_text(_MINI_AXIOM_BUNDLE, encoding="utf-8")
    theorem_path.write_text(_MINI_THEOREM_BUNDLE, encoding="utf-8")
    return axiom_path, theorem_path


def test_iter_documents_yields_one_doc_per_record(tmp_path):
    axiom_path, theorem_path = _write_bundles(tmp_path)
    src = ClaimPackSource([axiom_path, theorem_path])
    docs = list(src.iter_documents())
    assert len(docs) == 2
    # First bundle yields its single axiom; second yields its single theorem.
    assert docs[0].title == "Axiom of Implication Introduction"
    assert docs[1].title == "Law of Excluded Middle"
    for d in docs:
        assert d.source_type == "claim_pack"


def test_iter_documents_uri_stability(tmp_path):
    axiom_path, theorem_path = _write_bundles(tmp_path)
    src = ClaimPackSource([axiom_path, theorem_path])
    uris_a = [d.uri for d in src.iter_documents()]
    src2 = ClaimPackSource([axiom_path, theorem_path])
    uris_b = [d.uri for d in src2.iter_documents()]
    assert uris_a == uris_b
    assert uris_a[0] == (
        "claim-pack://axiomsg4-v2/pillar/I/axioms/000/"
        "axiom-of-implication-introduction"
    )
    assert uris_a[1] == (
        "claim-pack://theoremsg4-v2/pillar/I/theorems/000/"
        "law-of-excluded-middle"
    )


def test_iter_documents_content_layout(tmp_path):
    axiom_path, _ = _write_bundles(tmp_path)
    src = ClaimPackSource([axiom_path])
    doc = next(src.iter_documents())
    body = doc.content
    # Δ formula present (verbatim) — needed for quote-mode verification.
    assert r"A \to (B \to A)" in body
    # Concise + verbose ∇ both present.
    assert "A implies (B implies A)." in body
    assert "Establishes that a true proposition is implied by any premise." in body
    # Tail metadata projected into prose.
    assert "Role:" in body
    assert "Source: Mendelson 1997" in body
    assert "Subfield: Propositional Logic" in body


def test_iter_documents_extra_metadata(tmp_path):
    axiom_path, _ = _write_bundles(tmp_path)
    src = ClaimPackSource([axiom_path])
    doc = next(src.iter_documents())
    extra = doc.extra
    assert extra["bundle"] == "axiomsg4-v2"
    assert extra["bundle_id"] == "test-axiom-bundle"
    assert extra["version"] == "1.0.5"
    assert extra["pillar"] == "I"
    assert extra["kind"] == "axiom"
    assert extra["name"] == "Axiom of Implication Introduction"
    assert extra["runic"] == "ᚴᚵ"
    assert extra["category"] == "Foundations of Logic"
    assert extra["subfield"] == "Propositional Logic"
    assert extra["source_ref"] == "Mendelson 1997"
    assert extra["formal_lang"].startswith("Propositional logic")


def test_iter_documents_emits_pillar_reference_edges(tmp_path):
    axiom_path, theorem_path = _write_bundles(tmp_path)
    src = ClaimPackSource([axiom_path, theorem_path])
    docs = list(src.iter_documents())

    # First record of each pillar carries that pillar's `provenance.references`
    # as outbound Edge objects with edge_type='pillar_reference'.
    axiom_doc = docs[0]
    assert len(axiom_doc.edges) == 1
    e = axiom_doc.edges[0]
    assert isinstance(e, Edge)
    assert e.edge_type == "pillar_reference"
    # The reference resolves into the theorem bundle (pillar-level since the
    # leaf slug doesn't match the actual theorem name).
    assert e.dst_uri == "claim-pack://theoremsg4-v2/pillar/I"

    theorem_doc = docs[1]
    assert len(theorem_doc.edges) == 1
    assert theorem_doc.edges[0].edge_type == "pillar_reference"
    assert theorem_doc.edges[0].dst_uri == "claim-pack://axiomsg4-v2/pillar/I"


def test_missing_path_raises(tmp_path):
    with pytest.raises(FileNotFoundError):
        ClaimPackSource([tmp_path / "does-not-exist.json"])


def test_empty_paths_rejected():
    with pytest.raises(ValueError):
        ClaimPackSource([])


def test_skips_records_with_no_content(tmp_path):
    bundle = {
        "metadata": {"version": "0.1", "artifact_id": "x"},
        "pillars": {
            "I": {
                "title": "T",
                "description": "d",
                "axioms": [
                    {"name": "Real", "delta": "x", "nablaVerbose": "y"},
                    {},  # empty record — no name/delta/prose — should skip
                ],
            },
        },
    }
    p = tmp_path / "tiny.json"
    p.write_text(json.dumps(bundle), encoding="utf-8")
    src = ClaimPackSource([p])
    docs = list(src.iter_documents())
    assert len(docs) == 1
    assert docs[0].title == "Real"