API Reference

def load_toml(path: Path) -> TomlDocument:
    """Load a TOML file.

    Args:
        path: TOML file path.

    Returns:
        Parsed TOML document.

    Raises:
        ArtifactLoadError: If the file cannot be read or parsed.
    """
    try:
        with path.open("rb") as file_obj:
            data = tomllib.load(file_obj)
    except (OSError, tomllib.TOMLDecodeError) as exc:
        msg = f"Unable to read TOML file: {path}"
        raise ArtifactLoadError(msg) from exc

    return data

def read_text(path: Path) -> str:
    """Read a UTF-8 text file.

    Args:
        path: File path.

    Returns:
        File contents.

    Raises:
        ArtifactLoadError: If the file cannot be read.
    """
    try:
        return path.read_text(encoding="utf-8")
    except OSError as exc:
        msg = f"Unable to read text file: {path}"
        raise ArtifactLoadError(msg) from exc

def write_text(path: Path, content: str) -> None:
    """Write a UTF-8 text file, creating parent directories if needed.

    Args:
        path: Output path.
        content: Text content.

    Raises:
        ArtifactWriteError: If the file cannot be written.
    """
    try:
        path.parent.mkdir(parents=True, exist_ok=True)
        path.write_text(content, encoding="utf-8")
    except OSError as exc:
        msg = f"Unable to write text file: {path}"
        raise ArtifactWriteError(msg) from exc

def encode_json(payload: JsonObject) -> str:
    """Encode a JSON payload deterministically.

    The payload builder owns ordering. This encoder preserves insertion order
    rather than sorting keys.

    Args:
        payload: JSON-compatible object.

    Returns:
        Encoded JSON text ending with a newline.
    """
    return (
        json.dumps(
            payload,
            indent=2,
            sort_keys=False,
            ensure_ascii=True,
        )
        + "\n"
    )

def write_or_check_json(path: Path, payload: JsonObject, *, check: bool) -> bool:
    """Write a JSON payload or check whether the file is current.

    Args:
        path: Output path.
        payload: JSON payload.
        check: If true, check freshness without writing.

    Returns:
        True when current or written, otherwise false.
    """
    return write_or_check_text(path, encode_json(payload), check=check)

def write_or_check_text(path: Path, content: str, *, check: bool) -> bool:
    """Write a file or check whether it is current.

    Returns true when the file is current or was written.
    Returns false when check mode finds stale content.

    Args:
        path: Output path.
        content: Expected file content.
        check: If true, check freshness without writing.

    Returns:
        True when current or written, otherwise false.
    """
    if check:
        if not path.exists():
            print(f"[stale] {path.as_posix()} is missing")
            return False

        current = path.read_text(encoding="utf-8")
        if current != content:
            print(f"[stale] {path.as_posix()} is out of date")
            return False

        print(f"[ok   ] {path.as_posix()}")
        return True

    write_text(path, content)
    print(f"[write] {path.as_posix()}")
    return True

def find_repository_root(start: Path | None = None) -> Path:
    """Find the nearest repository root from a starting path.

    Args:
        start: Starting path. Defaults to the current working directory.

    Returns:
        Resolved repository root path.

    Raises:
        RepositoryRootError: If no repository root marker is found.
    """
    current = (start or Path.cwd()).resolve()

    if current.is_file():
        current = current.parent

    for candidate in (current, *current.parents):
        if any((candidate / marker).exists() for marker in ROOT_MARKERS):
            return candidate

    msg = f"Could not resolve repository root from {current}"
    raise RepositoryRootError(msg)

def lean_module_to_path(
    module: str,
    *,
    root: Path | None = None,
    lean_public_root: str,
) -> Path:
    """Resolve a Lean module name to its repository source path.

    Args:
        module: Lean module name.
        root: Repository root.
        lean_public_root: Expected public Lean root for the owning repository.

    Returns:
        Repository-contained Lean source path.

    Raises:
        PathResolutionError: If the module name is empty, path-like, malformed,
            or outside the declared public Lean root.
    """
    module_name = module.strip()

    if not module_name:
        msg = "Lean module name must be nonempty."
        raise PathResolutionError(msg)

    if "/" in module_name or "\\" in module_name:
        msg = f"Expected Lean module name, got path-like value: {module}"
        raise PathResolutionError(msg)

    parts = module_name.split(".")

    if any(not part for part in parts):
        msg = f"Malformed Lean module name: {module}"
        raise PathResolutionError(msg)

    if module_name != lean_public_root and not module_name.startswith(
        f"{lean_public_root}."
    ):
        msg = f"Expected Lean module under {lean_public_root}, got: {module_name}"
        raise PathResolutionError(msg)

    relative_path = Path(*parts).with_suffix(".lean")
    return resolve_repo_path(relative_path, root=root)

def reference_artifact_path(
    path: str | Path,
    *,
    root: Path | None = None,
    reference_dir_name: str = "reference",
) -> Path:
    """Resolve a declared reference artifact path.

    The declared path must be repository-relative and under the reference
    directory.

    Args:
        path: Declared repository-relative artifact path.
        root: Repository root.
        reference_dir_name: Name of the reference artifact directory.

    Returns:
        Resolved reference artifact path.

    Raises:
        PathResolutionError: If the path is outside the reference directory.
    """
    resolved = resolve_repo_path(path, root=root)
    reference_root = reference_dir(
        root=root,
        reference_dir_name=reference_dir_name,
    ).resolve()

    try:
        resolved.relative_to(reference_root)
    except ValueError as exc:
        msg = f"Reference artifact path is not under {reference_dir_name}/: {path}"
        raise PathResolutionError(msg) from exc

    return resolved

def reference_dir(
    *,
    root: Path | None = None,
    reference_dir_name: str = "reference",
) -> Path:
    """Return the repository reference directory."""
    return resolve_repo_path(reference_dir_name, root=root)

def repo_relative_path(path: Path, repo_root: Path) -> str:
    """Return a repository-relative POSIX path."""
    return path.resolve().relative_to(repo_root.resolve()).as_posix()

def resolve_repo_path(path: str | Path, *, root: Path | None = None) -> Path:
    """Resolve a path as repository-relative and contained within the repository.

    Args:
        path: Repository-relative path.
        root: Repository root. Defaults to nearest detected repository root.

    Returns:
        Resolved absolute path.

    Raises:
        PathResolutionError: If the path escapes the repository root.
    """
    repo_root = find_repository_root(root)
    resolved = (repo_root / path).resolve()

    try:
        resolved.relative_to(repo_root)
    except ValueError as exc:
        msg = f"Path escapes repository root: {path}"
        raise PathResolutionError(msg) from exc

    return resolved

def cannot_verify(
    check_id: str,
    message: str,
    *,
    artifact_id: str | None = None,
    path: Path | None = None,
    detail: JsonDetail | None = None,
) -> CheckResult:
    """Create a cannot-verify result."""
    return CheckResult(
        check_id=check_id,
        status=CheckStatus.CANNOT_VERIFY,
        severity=CheckSeverity.ERROR,
        message=message,
        artifact_id=artifact_id,
        path=path,
        detail={} if detail is None else detail,
    )

def empty_detail() -> JsonDetail:
    """Return an empty result detail dictionary."""
    return {}

def failure(
    check_id: str,
    message: str,
    *,
    artifact_id: str | None = None,
    path: Path | None = None,
    detail: JsonDetail | None = None,
) -> CheckResult:
    """Create an error failure result."""
    return CheckResult(
        check_id=check_id,
        status=CheckStatus.FAIL,
        severity=CheckSeverity.ERROR,
        message=message,
        artifact_id=artifact_id,
        path=path,
        detail={} if detail is None else detail,
    )

def ok(
    check_id: str,
    message: str,
    *,
    artifact_id: str | None = None,
    path: Path | None = None,
    detail: JsonDetail | None = None,
) -> CheckResult:
    """Create an ok result."""
    return CheckResult(
        check_id=check_id,
        status=CheckStatus.OK,
        severity=CheckSeverity.INFO,
        message=message,
        artifact_id=artifact_id,
        path=path,
        detail={} if detail is None else detail,
    )

def partial(
    check_id: str,
    message: str,
    *,
    artifact_id: str | None = None,
    path: Path | None = None,
    detail: JsonDetail | None = None,
) -> CheckResult:
    """Create a partial result."""
    return CheckResult(
        check_id=check_id,
        status=CheckStatus.PARTIAL,
        severity=CheckSeverity.WARNING,
        message=message,
        artifact_id=artifact_id,
        path=path,
        detail={} if detail is None else detail,
    )

def warning(
    check_id: str,
    message: str,
    *,
    artifact_id: str | None = None,
    path: Path | None = None,
    detail: JsonDetail | None = None,
) -> CheckResult:
    """Create a warning failure result."""
    return CheckResult(
        check_id=check_id,
        status=CheckStatus.FAIL,
        severity=CheckSeverity.WARNING,
        message=message,
        artifact_id=artifact_id,
        path=path,
        detail={} if detail is None else detail,
    )

def worst_status(results: Iterable[CheckResult]) -> CheckStatus:
    """Return the worst status across validation results."""
    rank = {
        CheckStatus.OK: 0,
        CheckStatus.PARTIAL: 1,
        CheckStatus.FAIL: 2,
        CheckStatus.CANNOT_VERIFY: 3,
    }

    worst = CheckStatus.OK
    for result in results:
        if rank[result.status] > rank[worst]:
            worst = result.status

    return worst

def configure_catalog_parser(subparsers: _SubParsersAction[Any]) -> None:
    """Configure the catalog subcommand."""
    parser = subparsers.add_parser(
        "catalog",
        help="Build the generated reference catalog.",
    )
    parser.add_argument(
        "--check",
        action="store_true",
        help="Check whether the generated catalog is current without writing.",
    )
    parser.set_defaults(handler=run_catalog_command)

def run_catalog_command(args: Namespace) -> int:
    """Run generated catalog export or freshness check."""
    root = None if args.root is None else Path(args.root)
    command_context = resolve_command_context(root=root)
    config = command_context.config

    if config.catalog_artifact_name is None:
        msg = (
            "theory-reference.toml must declare [export_map].catalog for catalog export"
        )
        raise RuntimeError(msg)
    if config.catalog_schema is None:
        msg = "theory-reference.toml must resolve a catalog schema for catalog export"
        raise RuntimeError(msg)

    namespace = (
        config.reference_namespace or f"se.{config.artifact_slug.replace('-', '_')}"
    )

    registry = build_registry_from_config(command_context.repo_root, config)

    payload = build_reference_catalog(
        registry=registry,
        schema=config.catalog_schema,
        repo_root=command_context.repo_root,
        source=config.repo_slug,
        namespace=namespace,
        artifact=config.catalog_artifact_name,
    )

    output_path = (
        command_context.repo_root
        / config.generated_data_dir
        / f"{config.catalog_artifact_name}.json"
    )

    current = write_or_check_text(
        output_path,
        encode_json(payload),
        check=bool(args.check),
    )

    if current:
        print(
            "Reference catalog is current."
            if args.check
            else "Reference catalog completed."
        )
        return 0

    print("Reference catalog is stale.")
    return 1

def configure_export_parser(subparsers: _SubParsersAction[Any]) -> None:
    """Configure the export subcommand."""
    parser = subparsers.add_parser(
        "export",
        help="Export generated data artifacts from reference artifacts.",
    )
    parser.add_argument(
        "--check",
        action="store_true",
        help="Check whether generated artifacts are current without writing.",
    )
    parser.set_defaults(handler=run_export_command)

def run_export_command(args: Namespace) -> int:
    """Run generated export or export freshness check."""
    raw_root = getattr(args, "root", None)
    root = None if raw_root is None else Path(raw_root)

    command_context = resolve_command_context(root=root)

    registry = build_registry_from_config(
        command_context.repo_root,
        command_context.config,
    )

    namespace = _reference_namespace(command_context.config)

    reference_root = (
        command_context.repo_root / command_context.config.reference_dir_name
    )
    output_root = command_context.repo_root / command_context.config.generated_data_dir

    results = export_registries(
        specs=command_context.export_specs,
        registry=registry,
        repo_root=command_context.repo_root,
        reference_root=reference_root,
        output_root=output_root,
        repo_slug=command_context.config.repo_slug,
        reference_namespace=namespace,
        check=bool(args.check),
    )

    if all(result.current for result in results):
        if args.check:
            print("Reference exports are current.")
        else:
            print("Reference export completed.")
        return 0

    print("Reference exports are stale.")
    return 1

def configure_inspect_parser(subparsers: _SubParsersAction[Any]) -> None:
    """Configure the inspect subcommand."""
    parser = subparsers.add_parser(
        "inspect",
        help="Inspect resolved theory-reference declarations.",
    )
    parser.set_defaults(handler=run_inspect_command)

def run_inspect_command(args: Namespace) -> int:
    """Inspect the resolved command context."""
    raw_root = getattr(args, "root", None)
    root = None if raw_root is None else Path(raw_root)

    command_context = resolve_command_context(root=root)
    config = command_context.config

    print(f"repo_root: {command_context.repo_root.as_posix()}")
    print(f"repo_slug: {config.repo_slug}")
    print(f"artifact_slug: {config.artifact_slug}")
    print(f"lean_public_root: {config.lean_public_root}")
    print(f"reference_dir: {config.reference_dir_name}")
    print(f"generated_data_dir: {config.generated_data_dir}")

    print("surface_kind_sources:")
    for kind, source in sorted(config.surface_kind_sources.items()):
        print(f"  {kind}: {source}")

    registry = build_registry_from_config(
        command_context.repo_root,
        config,
    )
    print(f"loaded_artifacts: {len(registry.artifacts)}")

    print("surface_symbols:")
    for kind, symbols in sorted(command_context.surface.by_kind.items()):
        print(f"  {kind}: {len(symbols)}")

    print(f"export_specs: {len(command_context.export_specs)}")
    for spec in command_context.export_specs:
        print(f"  {spec.source_name} -> {spec.output_name}")

    return 0

def build_parser() -> ArgumentParser:
    """Build the root argument parser."""
    parser = ArgumentParser(
        prog="se-theory-reference",
        description="Reference tooling for Structural Explainability theory repos.",
    )
    parser.add_argument(
        "--root",
        default=None,
        help="Repository root or path inside the target repository.",
    )

    subparsers = parser.add_subparsers(dest="command", required=True)

    configure_validate_parser(subparsers)
    configure_scaffold_parser(subparsers)
    configure_export_parser(subparsers)
    configure_catalog_parser(subparsers)
    configure_inspect_parser(subparsers)

    return parser

def main(argv: Sequence[str] | None = None) -> int:
    """Run the combined command-line interface."""
    parser = build_parser()
    args = parser.parse_args(argv)

    handler = getattr(args, "handler", None)
    if handler is None:
        parser.print_help()
        return 2

    return int(handler(args))

def configure_scaffold_parser(subparsers: _SubParsersAction[Any]) -> None:
    """Configure the scaffold subcommand."""
    parser = subparsers.add_parser(
        "scaffold",
        help="Scaffold missing reference entries from Lean source.",
    )
    parser.add_argument("--dry-run", action="store_true")
    parser.add_argument("--overwrite", action="store_true")
    parser.set_defaults(handler=run_scaffold_command)

def run_scaffold_command(args: Namespace) -> int:
    """Run reference scaffolding."""
    root = None if args.root is None else Path(args.root)
    command_context = resolve_command_context(root=root)

    print(f"repo_root: {command_context.repo_root.as_posix()}")
    print("Reference scaffolding command is wired.")
    print("Scaffold engine extraction is required before entries can be written.")

    if args.dry_run:
        print("mode: dry-run")
    if args.overwrite:
        print("mode: overwrite")

    return 0