#!/usr/bin/env python3
"""Check a Python file against its paired Lean AST proof file."""

from __future__ import annotations

import argparse
import ast
import json
import os
import re
import shutil
import subprocess
import sys
import textwrap
from dataclasses import dataclass, replace
from pathlib import Path

from lang.py.support import SupportChecker, UnsupportedConstruct, uses_parallel_model
from lang.py.trial import ScenarioError, ScenarioUnsupported
from lang.py.quotation import compile_quotation
from lang.py.lean_frontend import parse_imports, parse_theorem, guard_proposition
from lang.py.call_support import range_sum, reversed_list, uses_calls_model, has_partial_primitives, uses_heap_calls
from lang.py.contracts import ContractError, input_condition
from lang.py.defaults import literal_default
from lang.py.imports import bindings, resolve_function, resolve_python_function
from lang.py.linking import link_imports
from lang import spec_setup
from lang.runtime import lake_command, runtime_env
from lang.py.global_inputs import function_globals, merge_globals, annotation_kind


class UnsupportedSyntax(Exception):
    """Raised when the input uses Python syntax not represented by PyAst yet."""

    pass


class InvalidRequirement(Exception):
    """Raised when a `formalsw` proof marker is malformed."""

    pass


@dataclass(frozen=True)
class Requirement:
    """A proof obligation requested by a Python source marker."""

    theorem_name: str
    property_type: str
    source_path: Path
    source_line: int
    marker: str
    unsupported: tuple[UnsupportedConstruct, ...] = ()
    dependencies: tuple[Path, ...] = ()


@dataclass
class CheckReport:
    """Aggregate successful obligations and rejected source coverage across files."""

    passed: int = 0
    unsupported: int = 0
    failed_files: int = 0


@dataclass(frozen=True)
class Marker:
    """A proof marker extracted from a Python docstring."""

    text: str
    line: int
    reference: tuple | None = None
    predicate: str | None = None


@dataclass(frozen=True)
class RawTheoremRequirement:
    """A proof obligation requested with a raw Lean theorem statement."""

    theorem_name: str
    params: str
    property_type: str
    quotations: tuple[dict, ...] = ()


def print_diagnostic(*values, **kwargs) -> None:
    """
    Show current-project paths relative to cwd, including Lean diagnostics.

    Source identities and generated proof terms keep their absolute paths; only
    the human-facing stderr rendering changes.
    """
    root = str(Path.cwd().resolve())
    prefix = re.compile(r"(?<![\w./-])" + re.escape(root + os.sep))
    rendered = [prefix.sub('', str(value)) if root != os.sep else str(value) for value in values]
    print(*rendered, **dict(kwargs, file=sys.stderr))


def lean_string(value: str) -> str:
    """Return a Lean string literal for a Python string."""
    return json.dumps(value)


def indent(text: str, spaces: int) -> str:
    """Indent every non-empty line in `text` by `spaces` spaces."""
    prefix = " " * spaces
    return "\n".join(prefix + line if line else line for line in text.splitlines())


def proof_namespace_for_source(source: Path) -> str:
    """Return a source-oriented namespace for proof theorems."""
    try:
        source = source.resolve().relative_to(Path.cwd().resolve())
    except ValueError:
        pass
    path_without_suffix = source.with_suffix("")
    return ".".join(
        lean_import_component(component) for component in path_without_suffix.parts
    )


def proof_name_for_short_requirement(
    proof_namespace: str,
    function_name: str,
    property_name: str,
    args: list[str],
    marker: str,
) -> str:
    """Return a source-oriented theorem name for a short property marker."""
    match property_name, args:
        case "ReturnType" | "Returns" | "Halts", []:
            pass
        case "Throws", []:
            pass
        case "Equiv", [_]:
            pass
        case "EquivReturn", [_]:
            pass
        case "BigO", [_]:
            pass
        case "BigO", [_, _]:
            pass
        case _:
            raise InvalidRequirement(
                f"{function_name}: unsupported formalsw property marker: "
                f"{property_name}({', '.join(args)})"
            )
    if "«" in marker or "»" in marker:
        raise InvalidRequirement(
            f"{function_name}: formalsw marker cannot contain `«` or `»`: {marker}"
        )
    return f"{proof_namespace}.{lean_import_component(function_name)}.«{marker}»"


def scalar_lean_type(kind: str) -> str:
    return {"int": "Int", "str": "String", "bool": "Bool"}[kind]


def scalar_term(name: str, kind: str) -> str:
    constructor = {"int": "int", "str": "string", "bool": "bool"}[kind]
    return f'.{constructor} {name}'


def scalar_global_call(ast_namespace, function_name, arguments, globals):
    values = ", ".join(scalar_term(name, kind) for name, kind in arguments)
    state = ", ".join(f"({lean_string(key)}, {scalar_term(name, kind)})" for key, name, kind in globals)
    return (f'FormalSW.PyAst.scalarFunctionWithGlobals {ast_namespace}.module '
            f'{lean_string(function_name)} [{values}] [{state}]')


def mutable_global_call(ast_namespace, function_name, arguments, globals, heap="heap"):
    def value(name, kind):
        return f'.ref {name}' if kind.startswith('list[') else f'.scalar ({scalar_term(name, kind)})'
    values = ", ".join(value(name, kind) for name, kind in arguments)
    state = ", ".join(f"({lean_string(key)}, {value(name, kind)})" for key, name, kind in globals)
    return (f'FormalSW.PyAst.Mutable.function {ast_namespace}.module '
            f'{lean_string(function_name)} [{values}] [{state}] {heap}')


def mutable_domain(name, kind, heap):
    return f'FormalSW.PyAst.Mutable.Value.HasType {heap} (.ref {name}) {lean_string(kind)}'


def global_property_type(ast_namespace, function, property_name, args, negations, globals, conditions=()):
    """Quantify the shared initial state, then compare all observable final state."""
    arguments = [(arg.arg, annotation_kind(arg.annotation)) for arg in function.args.args]
    used = {name for name, _ in arguments}
    state = []
    for item in globals:
        name = item.name
        while name in used:
            name = "global_" + name
        used.add(name)
        state.append((item.name, name, item.kind))
    mutable = any(item.kind.startswith('list[') for item in globals) or any(kind.startswith('list[') for _, kind in arguments)
    heap = "heap"
    while heap in used:
        heap = "_" + heap
    domains = arguments + [(name, kind) for _, name, kind in state]
    binders = " ".join(f"({name} : {'Nat' if kind.startswith('list[') else scalar_lean_type(kind)})"
                       for name, kind in domains)
    if mutable:
        binders = f"({heap} : FormalSW.PyAst.Mutable.Heap) " + binders
        call_function = lambda name: mutable_global_call(ast_namespace, name, arguments, state, heap)
    else:
        call_function = lambda name: scalar_global_call(ast_namespace, name, arguments, state)
    call = call_function(function.name)
    if property_name in ("Returns", "Halts", "Throws"):
        body = f"({call}).{property_name}"
    elif property_name in ("Equiv", "EquivReturn"):
        other = call_function(args[0])
        body = f"({call}).{property_name} ({other})"
    elif property_name == "ReturnType":
        kind = annotation_kind(function.returns) or "None"
        body = f"({call}).ReturnType {lean_string(kind)}"
    else:
        raise InvalidRequirement(f"{property_name} has no global-state model")
    quantifier = "∃" if property_name == "Throws" else "∀"
    if mutable:
        constraints = [f"FormalSW.PyAst.Mutable.Heap.Valid {heap}"] + [
            mutable_domain(name, kind, heap) for name, kind in domains if kind.startswith('list[')]
        if property_name == "Throws":
            body = " ∧ ".join(f"({condition})" for condition in constraints) + f" ∧ ({body})"
        else:
            body = " → ".join(f"({condition})" for condition in constraints) + f" →\n{body}"
    body = guarded_type(body, conditions, existential=property_name == "Throws")
    result = f"{quantifier} {binders},\n{body}"
    for _ in range(negations):
        result = f"Not ({result})"
    return result


def property_type_for_short_requirement(
    ast_namespace: str,
    function_name: str,
    property_name: str,
    args: list[str],
    negations: int,
    function: ast.FunctionDef,
    module: ast.Module | None = None,
    conditions=(),
) -> str:
    """Return the Lean property type for a short property marker."""
    if module is not None:
        global_args = function_globals(module, function)
        if property_name in ("Equiv", "EquivReturn"):
            other = next(f for f in module.body if isinstance(f, ast.FunctionDef) and f.name == args[0])
            global_args = merge_globals(global_args, function_globals(module, other))
        if global_args:
            return global_property_type(ast_namespace, function, property_name, args, negations, global_args, conditions)
    match property_name, args:
        case "Returns" | "Halts", []:
            arguments = [*function.args.posonlyargs, *function.args.args]
            call = ", ".join(argument.arg for argument in arguments)
            property_type = raw_theorem_type_for_function(
                RawTheoremRequirement("", "", f"{property_name}(this_function({call}))"),
                function, ast_namespace,
                module,
            )
        case "ReturnType", []:
            property_type = (
                f'FormalSW.Property.Function.ReturnType {ast_namespace}.module '
                f'{lean_string(function_name)}'
            )
        case "Throws", []:
            property_type = (
                f'FormalSW.Property.Function.Throws {ast_namespace}.module '
                f'{lean_string(function_name)}'
            )
        case "Equiv", [other]:
            property_type = (
                f'FormalSW.Property.Function.Equiv {ast_namespace}.module '
                f'{lean_string(function_name)} {lean_string(other)}'
            )
        case "EquivReturn", [other]:
            property_type = (
                f'FormalSW.Property.Function.EquivReturn {ast_namespace}.module '
                f'{lean_string(function_name)} {lean_string(other)}'
            )
        case "BigO", [bound]:
            int_arguments = [
                argument.arg
                for argument in function.args.args
                if isinstance(argument.annotation, ast.Name)
                and argument.annotation.id == "int"
            ]
            if len(int_arguments) != 1:
                raise InvalidRequirement(
                    f"{function_name}: BigO without an explicit input-size binding "
                    "requires exactly one int argument"
                )
            argument = int_arguments[0]
            parameter = argument if re.search(rf"\b{re.escape(argument)}\b", bound) else "_"
            property_type = (
                f'FormalSW.Property.Function.BigO {ast_namespace}.module '
                f'{lean_string(function_name)} '
                f'(FormalSW.PyAst.InputSize.intToNat {lean_string(argument)}) '
                f'(fun {parameter} : Nat => {bound})'
            )
        case "BigO", [bound, measure]:
            parameter = "n" if re.search(r"\bn\b", bound) else "_"
            list_measure = re.fullmatch(
                r"len\(\s*([A-Za-z_][A-Za-z0-9_]*)\s*\)", measure
            )
            int_measure = re.fullmatch(r"([A-Za-z_][A-Za-z0-9_]*)", measure)
            if list_measure is not None:
                input_size = (
                    "FormalSW.PyAst.InputSize.listLength "
                    f"{lean_string(list_measure.group(1))}"
                )
            elif int_measure is not None:
                input_size = (
                    "FormalSW.PyAst.InputSize.intToNat "
                    f"{lean_string(int_measure.group(1))}"
                )
            else:
                raise InvalidRequirement(
                    f"{function_name}: unsupported BigO input size: n = {measure}"
                )
            property_type = (
                f'FormalSW.Property.Function.BigO {ast_namespace}.module '
                f'{lean_string(function_name)} ({input_size}) '
                f'(fun {parameter} : Nat => {bound})'
            )
        case _:
            raise InvalidRequirement(
                f"{function_name}: unsupported formalsw property marker: "
                f"{property_name}({', '.join(args)})"
            )
    if conditions:
        if property_name == "Throws":
            property_type = guarded_type(property_type, conditions, existential=True)
        else:
            property_type = raw_theorem_type_for_function(
                RawTheoremRequirement("", "", property_type), function, ast_namespace, module, conditions)
    for _ in range(negations):
        property_type = f"Not ({property_type})"
    return property_type


def parse_short_marker(marker: str) -> tuple[str, list[str], int] | None:
    """Parse a DSL marker, including any recursive `Not` prefixes."""
    negations = 0
    while marker.startswith("Not "):
        negations += 1
        marker = marker.removeprefix("Not ").strip()
    match = re.fullmatch(r"([A-Za-z_][A-Za-z0-9_]*)\s*(?:\((.*)\))?", marker)
    if match is None:
        return None
    property_name = match.group(1)
    args_text = match.group(2)
    if args_text is None:
        args = []
    elif property_name in ("Requires", "Equiv", "EquivReturn"):
        args = [args_text.strip()] if args_text.strip() else []
    elif property_name == "BigO":
        big_o_match = re.fullmatch(
            r"(.+),\s*n\s*=\s*(.+)", args_text.strip(), re.DOTALL
        )
        args = (
            [big_o_match.group(1).strip(), big_o_match.group(2).strip()]
            if big_o_match is not None
            else [args_text.strip()]
        )
    else:
        args = [arg.strip() for arg in args_text.split(",") if arg.strip()]
    return property_name, args, negations


def strip_marker_prefix(line: str) -> str | None:
    """Return a proof marker line without its marker prefix."""
    stripped = line.strip()
    match = re.fullmatch(r"(?:@formalsw|@lean|formalsw:)\s*:?\s*(.*)", stripped)
    if match is not None:
        return match.group(1).strip()
    return None


def parse_raw_theorem(marker: str) -> RawTheoremRequirement | None:
    """Parse a raw Lean theorem header into a typed proof obligation."""
    theorem = marker.strip().removesuffix(".").strip()
    if theorem.split(maxsplit=1)[0:1] != ["theorem"]:
        return None
    try:
        parsed = parse_theorem(theorem)
    except ScenarioError as error:
        raise InvalidRequirement(str(error)) from error
    return RawTheoremRequirement(parsed['name'], parsed['params'], parsed['type'], tuple(parsed['quotes']))


def raw_theorem_type(requirement: RawTheoremRequirement) -> str:
    """Return the proposition type expected by a raw theorem marker."""
    if requirement.params:
        return f"∀ {requirement.params},\n{requirement.property_type}"
    return requirement.property_type


def lean_type_for_python_annotation(annotation: ast.expr | None) -> str | None:
    """Translate a supported Python argument annotation to its modeled Lean domain."""
    if isinstance(annotation, ast.Name):
        return {
            "int": "Int",
            "bool": "Bool",
            "str": "String",
            "list": "List Value",
        }.get(annotation.id)
    if (
        isinstance(annotation, ast.Subscript)
        and isinstance(annotation.value, ast.Name)
        and annotation.value.id == "list"
        and isinstance(annotation.slice, ast.Name)
    ):
        if annotation.slice.id == "int":
            return "List Int"
        return "List Int"
    return None


def explicitly_bound_names(params: str) -> set[str]:
    """Find names introduced by ordinary parenthesized Lean binders."""
    names: set[str] = set()
    for match in re.finditer(r"[({[]\s*([^:(){}\[\]]+?)\s*:", params):
        names.update(re.findall(r"[A-Za-z_][A-Za-z0-9_']*", match.group(1)))
    return names


def guard_raw_requirement(requirement, function, conditions):
    bound = explicitly_bound_names(requirement.params)
    if not conditions:
        return requirement, bound
    inputs = [arg.arg for arg in function.args.args]
    captures = [name for name in inputs if any(f"«{name}»" in condition for condition in conditions)]
    try:
        guarded = guard_proposition(requirement.property_type,
            " ∧ ".join(f"({condition})" for condition in conditions), captures, inputs, bound)
    except ScenarioError as error:
        raise InvalidRequirement(str(error)) from error
    return replace(requirement, property_type=guarded['type']), bound | set(guarded['bound'])


def raw_theorem_type_for_function(
    requirement: RawTheoremRequirement,
    function: ast.FunctionDef,
    ast_namespace: str,
    module: ast.Module | None = None,
    conditions=(),
) -> str:
    """Infer referenced, unbound Python arguments in a function-level theorem."""
    requirement, bound = guard_raw_requirement(requirement, function, conditions)
    referenced_text = f"{requirement.params}\n{requirement.property_type}"
    inferred = []
    global_args = function_globals(module, function) if module is not None and re.search(r"\bthis_function\b", referenced_text) else ()
    mutable = any(item.kind.startswith('list[') for item in global_args)
    heap = "heap"
    taken = {arg.arg for arg in function.args.args} | {item.name for item in global_args}
    while heap in taken:
        heap = "_" + heap
    if mutable and heap not in bound:
        inferred.append(f"({heap} : FormalSW.PyAst.Mutable.Heap)")
    for argument in [*function.args.posonlyargs, *function.args.args]:
        if argument.arg in bound:
            continue
        if re.search(rf"\b{re.escape(argument.arg)}\b", referenced_text) is None:
            continue
        lean_type = ("Nat" if mutable and (annotation_kind(argument.annotation) or "").startswith('list[')
                     else lean_type_for_python_annotation(argument.annotation))
        if lean_type is None:
            raise InvalidRequirement(
                f"{function.name}: cannot infer a Lean domain for Python argument "
                f"{argument.arg!r}; bind it explicitly in the raw theorem"
            )
        inferred.append(f"({argument.arg} : {lean_type})")
    for item in global_args:
        if item.name not in bound:
            kind = "Nat" if item.kind.startswith('list[') else scalar_lean_type(item.kind)
            inferred.append(f"({item.name} : {kind})")
    params = " ".join([*inferred, requirement.params]).strip()
    property_type = requirement.property_type
    if params and not global_args:
        property_type = f"∀ {params},\n{property_type}"
    if re.search(r"\bthis_function\b", referenced_text):
        arguments = [*function.args.posonlyargs, *function.args.args]
        if "this_function" in bound or any(arg.arg == "this_function" for arg in arguments):
            raise InvalidRequirement(
                f"{function.name}: this_function is reserved for the enclosing Python function"
            )
        if function.args.kwonlyargs or function.args.vararg is not None or function.args.kwarg is not None:
            raise InvalidRequirement(
                f"{function.name}: this_function supports positional arguments without variadics"
            )
        annotations = [argument.annotation for argument in arguments]
        if mutable:
            names = [f"input_{index}" for index in range(len(arguments))]
            kinds = [annotation_kind(arg.annotation) for arg in arguments]
            lambda_params = " ".join(f"({name} : {'Nat' if kind.startswith('list[') else scalar_lean_type(kind)})"
                                     for name, kind in zip(names, kinds))
            binding = mutable_global_call(ast_namespace, function.name, list(zip(names, kinds)),
                [(item.name, item.name, item.kind) for item in global_args], heap)
            if names:
                binding = f"fun {lambda_params} => {binding}"
        elif uses_parallel_model(function) or re.search(r"\bParallel\(", referenced_text):
            binding = f"FormalSW.PyAst.parallelFunction {ast_namespace}.module {lean_string(function.name)}"
        elif len(arguments) == 1 and isinstance(annotations[0], ast.Name) and annotations[0].id == "list":
            binding = f"FormalSW.PyAst.listFunction {ast_namespace}.module {lean_string(function.name)}"
        elif all(isinstance(annotation, ast.Name) and annotation.id in {"int", "str", "bool"}
                 for annotation in annotations):
            names = [f"input_{index}" for index in range(len(arguments))]
            constructors = {"int": "int", "str": "string", "bool": "bool"}
            types = {"int": "Int", "str": "String", "bool": "Bool"}
            lambda_params = " ".join(f"({name} : {types[annotation.id]})"
                              for name, annotation in zip(names, annotations))
            values = ", ".join(f".{constructors[annotation.id]} {name}"
                               for name, annotation in zip(names, annotations))
            if global_args:
                binding = scalar_global_call(ast_namespace, function.name,
                    [(name, annotation.id) for name, annotation in zip(names, annotations)],
                    [(item.name, item.name, item.kind) for item in global_args])
            else:
                runtime = "Calls.function" if module is not None and uses_calls_model(module, function) else "scalarFunction"
                binding = (f"FormalSW.PyAst.{runtime} {ast_namespace}.module "
                           f"{lean_string(function.name)} [{values}]")
            if names:
                binding = f"fun {lambda_params} => {binding}"
        else:
            raise InvalidRequirement(
                f"{function.name}: this_function supports scalar int/str/bool arguments or one bare list"
            )
        property_type = f"let this_function := {binding};\n{property_type}"
    if params and global_args:
        property_type = f"∀ {params},\n{property_type}"
    # Always supply the module: Lean parses nested comparison expressions itself.
    property_type = f"let _this_module := {ast_namespace}.module;\n{property_type}"
    return property_type


def docstring_markers(docstring: str | None, start_line: int | None) -> list[Marker]:
    """Extract `formalsw` marker blocks from a Python docstring."""
    if docstring is None:
        return []
    markers: list[Marker] = []
    lines = docstring.splitlines()
    index = 0
    while index < len(lines):
        first = strip_marker_prefix(lines[index])
        if first is None:
            index += 1
            continue
        marker_line = (start_line or 1) + index
        if first == "Py":
            block = []
            marker_indent = len(lines[index]) - len(lines[index].lstrip())
            index += 1
            while index < len(lines):
                line = lines[index]
                if line.strip() and len(line) - len(line.lstrip()) <= marker_indent:
                    break
                block.append(line)
                index += 1
            markers.append(Marker("Py\n" + textwrap.dedent("\n".join(block)).rstrip(), marker_line))
        elif first.startswith("theorem "):
            block = [first]
            index += 1
            while index < len(lines):
                if not lines[index].strip():
                    break
                if strip_marker_prefix(lines[index]) is not None:
                    break
                block.append(lines[index])
                index += 1
            markers.append(Marker("\n".join(block), marker_line))
        else:
            markers.append(Marker(first, marker_line))
            index += 1
    return markers


def setup_predicate(text, environment, function):
    """Capture scalar setup values without evaluating symbolic function inputs."""
    expression = ast.parse(text, mode='eval')
    inputs = {arg.arg for arg in function.args.args} if function else set()
    inputs.update(node.id for node in ast.walk(expression)
                  if isinstance(node, ast.Name) and isinstance(node.ctx, ast.Store))

    class Capture(ast.NodeTransformer):
        def visit_Name(self, node):
            if node.id in inputs or node.id not in environment:
                return node
            value = environment[node.id]
            if type(value) not in (int, bool, str, type(None)):
                raise InvalidRequirement(f'Requires: setup binding {node.id!r} needs execution-model support; only scalar setup values can currently be captured')
            return ast.copy_location(ast.Constant(value=value), node)

    return ast.unparse(Capture().visit(expression))


def prepare_specification(source, module):
    """Execute ordered setup once and capture each subsequent marker's bindings."""
    if hasattr(module, 'formalsw_markers'):
        return

    def scope(node, environment):
        result = []
        for marker in docstring_markers(ast.get_docstring(node, clean=False), docstring_start_line(node)):
            if marker.text == 'Py' or marker.text.startswith(('Py ', 'Py\n')):
                code = marker.text[2:].lstrip(' \t')
                if not code.strip():
                    raise InvalidRequirement(f'{source}:{marker.line}: Py needs Python statements')
                spec_setup.execute(code, environment, source, marker.line)
                continue
            parsed = parse_short_marker(marker.text)
            if parsed and len(parsed[1]) == 1:
                expression = parsed[1][0]
                if parsed[0] in ('Equiv', 'EquivReturn'):
                    names = {part.id for part in ast.walk(ast.parse(expression, mode='eval')) if isinstance(part, ast.Name)}
                    if names & environment.keys():
                        value = spec_setup.evaluate(expression, environment, source, marker.line)
                        marker = replace(marker, reference=resolve_python_function(value))
                elif parsed[0] == 'Requires':
                    marker = replace(marker, predicate=setup_predicate(expression, environment,
                        node if isinstance(node, ast.FunctionDef) else None))
            result.append(marker)
        node.formalsw_markers = result

    try:
        environment = spec_setup.initial_environment(source)
        scope(module, environment)
        for node in module.body:
            if isinstance(node, (ast.FunctionDef, ast.AsyncFunctionDef)):
                scope(node, environment.copy())
    except (spec_setup.SetupError, ContractError, SyntaxError) as error:
        raise InvalidRequirement(str(error)) from error


_source_modules = {}
_source_loading = []


def validate_source_snapshots(source, module):
    snapshots = [(source, module)]
    visited = set()
    while snapshots:
        path, program = snapshots.pop()
        key = (path.resolve(), id(program))
        if key in visited:
            continue
        visited.add(key)
        original = getattr(program, 'formalsw_source_text', None)
        if original is not None and (not path.is_file() or path.read_text() != original):
            raise InvalidRequirement(f'{path}: source changed after specification loading; rerun the checker')
        for node in (program, *program.body):
            for marker in getattr(node, 'formalsw_markers', ()):
                if marker.reference:
                    snapshots.append(marker.reference[:2])
        for dependency in (path.resolve(), *getattr(program, 'formalsw_link_dependencies', ())):
            if dependency in _source_modules:
                snapshots.append((dependency, _source_modules[dependency]))


def source_module(source):
    """Share preparation between dependency discovery and obligation emission."""
    path = source.resolve()
    if path not in _source_modules:
        if path in _source_loading:
            raise InvalidRequirement('cyclic local Python imports: ' + ' -> '.join(map(str, [*_source_loading, path])))
        _source_loading.append(path)
        try:
            text = source.read_text()
            module = ast.parse(text, filename=str(source))
            module.formalsw_source = path
            module.formalsw_source_text = text
            prepare_specification(source, module)
            if proof_path_for_source(path).is_file() or any(
                    getattr(node, 'formalsw_markers', ()) for node in (module, *module.body)):
                link_imports(path, module, source_module)
            else:
                module.formalsw_link_dependencies = ()
            _source_modules[path] = module
        except ContractError as error:
            raise InvalidRequirement(str(error)) from error
        finally:
            _source_loading.pop()
    validate_source_snapshots(source, _source_modules[path])
    return _source_modules[path]


def docstring_start_line(node: ast.Module | ast.FunctionDef) -> int | None:
    """Return the source line where a module or function docstring starts."""
    body = node.body
    if not body:
        return None
    first = body[0]
    if not isinstance(first, ast.Expr):
        return None
    if not isinstance(first.value, ast.Constant) or not isinstance(first.value.value, str):
        return None
    return first.lineno


def guarded_type(body, conditions, *, existential=False):
    """Restrict quantified witnesses too: a false domain cannot witness Throws."""
    if not conditions:
        return body
    if existential:
        return " ∧ ".join(f"({condition})" for condition in conditions) + f" ∧ ({body})"
    return " → ".join(f"({condition})" for condition in conditions) + f" →\n({body})"


def collect_conditions(markers, function, module, namespace, prior_conditions=()):
    conditions, properties, unsupported = [], [], []
    for marker in markers:
        parsed = parse_short_marker(marker.text)
        if not parsed or parsed[0] != "Requires":
            properties.append(marker)
            continue
        if len(parsed[1]) != 1 or parsed[2]:
            raise InvalidRequirement("Requires takes one Python predicate and cannot be negated")
        try:
            predicate = input_condition(marker.predicate or parsed[1][0], function, module)
        except ContractError as error:
            raise InvalidRequirement(str(error)) from error
        unsupported.extend(predicate.unsupported)
        name = f"requires_{function.name if function else 'module'}_{len(conditions)}"
        if predicate.unsupported:
            conditions.append("False")
            continue
        module.formalsw_conditions[name] = predicate.expression
        env = "none"
        for arg in reversed(predicate.arguments):
            kind = annotation_kind(arg.annotation)
            env = f"if _arg = {lean_string(arg.arg)} then some ({scalar_term('«' + arg.arg + '»', kind)}) else {env}"
        if predicate.needs_coverage:
            covered = f"(FormalSW.PyAst.Calls.evaluate {namespace}.module (fun _arg => {env}) {namespace}.{name}).Supported"
            covered = guarded_type(covered, [*prior_conditions, *conditions])
            arguments = function.args.args if function else ()
            if arguments:
                binders = " ".join(f"(«{arg.arg}» : {scalar_lean_type(annotation_kind(arg.annotation))})" for arg in arguments)
                covered = f"∀ {binders},\n{covered}"
            module.formalsw_condition_coverage.append((name + '_supported', covered, marker.line))
        conditions.append(f"FormalSW.PyAst.Calls.Condition {namespace}.module (fun _arg => {env}) {namespace}.{name}")
    if function is not None and conditions and not properties:
        raise InvalidRequirement("Requires needs a property obligation")
    return conditions, properties, tuple(dict.fromkeys(unsupported))


def scalar_contract_type(module, function, namespace, property_name, conditions, negations, target=None, input_function=None):
    """Quantify scalar inputs and keep any explicit domain inside the quantifier."""
    arguments = (input_function or function).args.args
    kinds = [annotation_kind(arg.annotation) for arg in arguments]
    if any(kind not in ('int', 'str', 'bool') for kind in kinds):
        raise InvalidRequirement(f"{function.name}: this contract requires scalar argument annotations")
    names = [f"«{arg.arg}»" for arg in arguments]

    def call(program, func, ns):
        if bindings(program, func.name) != [func]:
            raise InvalidRequirement(f"{func.name}: contract functions must have one definition and must not be rebound")
        if function_globals(program, func):
            raise InvalidRequirement(f"{func.name}: constrained or imported contracts with globals are unsupported")
        if [annotation_kind(arg.annotation) for arg in func.args.args] != kinds:
            raise InvalidRequirement("Equiv requires matching supported argument domains")
        if uses_heap_calls(program, func):
            kind = annotation_kind(func.returns)
            if kind and kind.startswith('list['):
                values = ", ".join(f'.scalar ({scalar_term(name, kind)})' for name, kind in zip(names, kinds))
                return f'FormalSW.PyAst.HeapCalls.call {ns}.module {lean_string(func.name)} [{values}] []'
            if kind not in ('int', 'str', 'bytes', 'bool') and not (isinstance(func.returns, ast.Constant) and func.returns.value is None):
                raise InvalidRequirement("heap call contracts require a supported return annotation")
            runtime = "HeapCalls.scalarFunction"
        else:
            runtime = "Calls.function" if uses_calls_model(program, func) else "scalarFunction"
        values = ", ".join(scalar_term(name, kind) for name, kind in zip(names, kinds))
        return f'FormalSW.PyAst.{runtime} {ns}.module {lean_string(func.name)} [{values}]'

    left = call(module, function, namespace)
    body = f"({left}).{property_name}"
    if target:
        body += f" ({call(*target)})"
    if property_name == "ReturnType":
        kind = annotation_kind(function.returns)
        if kind is None and isinstance(function.returns, ast.Constant) and function.returns.value is None:
            kind = "None"
        if kind not in ("int", "bool", "str", "None") and not (uses_heap_calls(module, function) and kind and kind.startswith("list[")):
            raise InvalidRequirement("ReturnType needs a supported return annotation")
        body += f" {lean_string(kind)}"
    body = guarded_type(body, conditions, existential=property_name == "Throws")
    if names:
        binders = " ".join(f"({name} : {scalar_lean_type(kind)})" for name, kind in zip(names, kinds))
        quantifier = "∃" if property_name == "Throws" else "∀"
        body = f"{quantifier} {binders},\n{body}"
    for _ in range(negations):
        body = f"Not ({body})"
    return body


def collect_requirements(
    source_path: Path,
    module: ast.Module,
    proof_namespace: str,
    ast_namespace: str,
) -> list[Requirement]:
    """Collect proof obligations requested by source docstring markers."""
    requirements: list[Requirement] = []
    module.formalsw_source = source_path.resolve()
    prepare_specification(source_path, module)
    support = SupportChecker(module)
    module.formalsw_conditions = {}
    module.formalsw_condition_coverage = []
    raw_targets = {target for node in (module, *module.body)
                   for marker in getattr(node, 'formalsw_markers', ())
                   for _, target in support.execution_targets(marker.text)}
    module_conditions, module_markers, module_unsupported = collect_conditions(
        module.formalsw_markers,
        None, module, ast_namespace)
    for marker in module_markers:
        raw_theorem = parse_raw_theorem(marker.text)
        if raw_theorem is None:
            raise InvalidRequirement(f"module docstring: unsupported formalsw marker: {marker.text}")
        theorem_name = raw_theorem.theorem_name
        if "." not in theorem_name:
            theorem_name = f"{proof_namespace}.{theorem_name}"
        requirements.append(Requirement(
            theorem_name,
            guarded_type(raw_theorem_type(raw_theorem), module_conditions),
            source_path,
            marker.line,
            marker.text,
            module_unsupported + support.requirement(None, marker.text),
        ))
    for stmt in module.body:
        if not isinstance(stmt, (ast.FunctionDef, ast.AsyncFunctionDef)):
            continue
        if getattr(stmt, 'formalsw_imported', False):
            continue
        markers = stmt.formalsw_markers
        conditions, properties, condition_unsupported = collect_conditions(markers, stmt, module, ast_namespace, module_conditions)
        conditions = [*module_conditions, *conditions]
        condition_unsupported = (*module_unsupported, *condition_unsupported)
        first_requirement = len(requirements)
        coverage_targets = [(module, stmt, ast_namespace)]
        coverage_dependencies = []
        for marker in properties:
            parsed = parse_short_marker(marker.text)
            scalar_equiv = (parsed and parsed[0] in ("Equiv", "EquivReturn") and len(parsed[1]) == 1 and
                            (marker.reference is not None or uses_calls_model(module, stmt) or parsed[1][0] not in support.functions
                             or uses_calls_model(module, support.functions[parsed[1][0]])))
            scalar_property = (parsed and parsed[0] in ("Returns", "Halts", "Throws", "ReturnType", "Equiv", "EquivReturn")
                               and all(annotation_kind(arg.annotation) in ("int", "str", "bool") for arg in stmt.args.args)
                               and not support.check(stmt.name)
                               and not function_globals(module, stmt))
            if scalar_equiv or scalar_property and (conditions or uses_calls_model(module, stmt)):
                property_name, args, negations = parsed
                theorem_name = proof_name_for_short_requirement(
                    proof_namespace, stmt.name, property_name, args, marker.text)
                unsupported = list(support.check(stmt.name))
                target = None
                dependencies = ()
                if property_name in ("Equiv", "EquivReturn"):
                    target = None if marker.reference else support.functions.get(args[0])
                    if target is None:
                        try:
                            target_path, target_module, target = marker.reference or resolve_function(source_path, module, args[0])
                            target_module = source_module(target_path)
                            target = next(node for node in target_module.body
                                          if isinstance(node, ast.FunctionDef) and node.name == target.name)
                        except ContractError as error:
                            raise InvalidRequirement(str(error)) from error
                        target_namespace = namespace_for_source(target_path)
                        dependencies = (target_path,) if target_path != source_path.resolve() else ()
                        unsupported.extend(SupportChecker(target_module).check(target.name))
                    else:
                        target_module, target_namespace = module, ast_namespace
                        unsupported.extend(support.check(target.name))
                property_type = "False" if unsupported else scalar_contract_type(
                    module, stmt, ast_namespace, property_name, conditions, negations,
                    (target_module, target, target_namespace) if target else None)
                if target:
                    coverage_targets.append((target_module, target, target_namespace))
                    coverage_dependencies.extend(dependencies)
                requirements.append(Requirement(theorem_name, property_type, source_path,
                    marker.line, marker.text, tuple(unsupported), dependencies))
                continue
            raw_theorem = parse_raw_theorem(marker.text)
            if raw_theorem is not None and raw_theorem.quotations:
                unsupported = support.requirement(stmt.name, "theorem quotation : True")
                property_type = "False"
                if not unsupported:
                    try:
                        for quotation in raw_theorem.quotations:
                            compile_quotation(module, stmt, quotation['expression'], quotation['mode'])
                        property_type = (
                            f'python_context {lean_string(str(source_path))} {lean_string(stmt.name)} '
                            f'{ast_namespace}.module in\n{raw_theorem_type(guard_raw_requirement(raw_theorem, stmt, conditions)[0])}'
                        )
                    except ScenarioUnsupported as error:
                        unsupported = (UnsupportedConstruct(stmt.name, error.line, str(error)),)
                    except ScenarioError as error:
                        raise InvalidRequirement(str(error)) from error
                theorem_name = raw_theorem.theorem_name
                if "." not in theorem_name:
                    theorem_name = f"{proof_namespace}.{lean_import_component(stmt.name)}.{theorem_name}"
                requirements.append(Requirement(theorem_name, property_type, source_path,
                    marker.line, marker.text, unsupported))
                continue
            unsupported = support.requirement(stmt.name, marker.text)
            if raw_theorem is not None:
                theorem_name = raw_theorem.theorem_name
                if "." not in theorem_name:
                    theorem_name = f"{proof_namespace}.{lean_import_component(stmt.name)}.{theorem_name}"
                requirements.append(Requirement(
                    theorem_name,
                    "False" if unsupported else raw_theorem_type_for_function(raw_theorem, stmt, ast_namespace, module, conditions),
                    source_path,
                    marker.line,
                    marker.text,
                    unsupported,
                ))
                continue
            parsed = parse_short_marker(marker.text)
            if parsed is None:
                raise InvalidRequirement(
                    f"{stmt.name}: unsupported formalsw marker: {marker.text}"
                )
            property_name, args, negations = parsed
            requirements.append(Requirement(
                proof_name_for_short_requirement(
                    proof_namespace,
                    stmt.name,
                    property_name,
                    args,
                    marker.text,
                ),
                "False" if unsupported else property_type_for_short_requirement(
                    ast_namespace,
                    stmt.name,
                    property_name,
                    args,
                    negations,
                    stmt,
                    module,
                    conditions,
                ),
                source_path,
                marker.line,
                marker.text,
                unsupported,
            ))
        if (properties or stmt.name in raw_targets) and any(has_partial_primitives(program, function) or
                uses_calls_model(program, function) and uses_heap_calls(program, function)
                for program, function, _ in coverage_targets):
            covered = []
            issues = list(condition_unsupported)
            seen = set()
            for program, function, namespace in coverage_targets:
                if (namespace, function.name) in seen:
                    continue
                seen.add((namespace, function.name))
                function_issues = SupportChecker(program).check(function.name)
                issues.extend(function_issues)
                if not function_issues:
                    covered.append(scalar_contract_type(program, function, namespace,
                        'Supported', conditions, 0, input_function=stmt))
            property_type = 'False' if issues else ' ∧ '.join(f'({term})' for term in covered)
            requirements.append(Requirement(f'{proof_namespace}.{lean_import_component(stmt.name)}.«Supported»',
                property_type, source_path, stmt.lineno, 'execution model coverage',
                tuple(dict.fromkeys(issues)), tuple(dict.fromkeys(coverage_dependencies))))
        for index in range(first_requirement, len(requirements)):
            if condition_unsupported:
                requirements[index] = replace(requirements[index], property_type="False",
                    unsupported=tuple(dict.fromkeys((*condition_unsupported, *requirements[index].unsupported))))
    for name, property_type, line in module.formalsw_condition_coverage:
        requirements.append(Requirement(f'{proof_namespace}.{name}', property_type,
            source_path, line, 'precondition model coverage', ()))
    top_level = {id(stmt) for stmt in module.body}
    for stmt in ast.walk(module):
        if not isinstance(stmt, (ast.FunctionDef, ast.AsyncFunctionDef, ast.ClassDef)) or id(stmt) in top_level:
            continue
        for marker in docstring_markers(ast.get_docstring(stmt, clean=False), docstring_start_line(stmt)):
            requirements.append(Requirement(
                f"{proof_namespace}.{stmt.name}",
                "False",
                source_path,
                marker.line,
                marker.text,
                (UnsupportedConstruct(stmt.name, stmt.lineno,
                    "requirements on nested functions and class methods are unsupported"),),
            ))
    if module_conditions and not requirements:
        raise InvalidRequirement("Requires needs a property obligation")
    linked = getattr(module, 'formalsw_link_dependencies', ())
    if linked:
        requirements = [replace(requirement, dependencies=tuple(dict.fromkeys(
            (*linked, *requirement.dependencies)))) for requirement in requirements]
    return requirements


class RequirementEmitter:
    """Render a generated Lean wrapper that checks a proof and its obligations."""

    def __init__(
        self,
        proof_path: Path,
        proof_module: str,
        requirements: list[Requirement],
    ):
        """Store the proof import and the requirements it must expose."""
        self.proof_path = proof_path
        self.proof_module = proof_module
        self.requirements = requirements

    def emit(self) -> str:
        """Render the generated Lean requirements file."""
        checked_import = (
            self.proof_module
            if self.requirements
            else "FormalSW"
        )
        lines = [
            f"import {checked_import}",
            *dependency_imports(self.requirements),
            "",
            "open FormalSW.PyAst",
            "",
            "/-!",
            "Generated by formalsw. Do not edit by hand.",
            "",
            f"This file checks `{self.proof_path}` and its requested proof obligations.",
            "-/",
            "",
            "/- formalsw proof obligations -/",
            "",
        ]
        for requirement in self.requirements:
            lines.extend([
                "example :",
                f"{indent(requirement.property_type, 4)}",
                f"  := {requirement.theorem_name}",
                "",
            ])
        return "\n".join(lines)


class ProofStubEmitter:
    """Render a proof file containing every requested theorem with `sorry`."""

    def __init__(
        self,
        ast_module: str,
        proof_namespace: str,
        requirements: list[Requirement],
    ):
        """Store the generated AST import and requested proof obligations."""
        self.ast_module = ast_module
        self.proof_namespace = proof_namespace
        self.requirements = requirements

    def emit(self) -> str:
        """Render a complete Lean proof-file stub."""
        lines = [
            f"import {self.ast_module}",
            *dependency_imports(self.requirements),
            "import FormalSW",
            "",
            "open FormalSW.PyAst",
            "",
            f"namespace {self.proof_namespace}",
            "",
        ]

        def append_theorem(name: str, requirement: Requirement) -> None:
            """Append one theorem stub under its rendered declaration name."""
            lines.extend([
                f"theorem {name} :",
                indent(requirement.property_type, 4),
                "  := by",
                "  sorry",
                "",
            ])

        prefix = self.proof_namespace + "."
        for requirement in self.requirements:
            if requirement.theorem_name.startswith(prefix):
                append_theorem(requirement.theorem_name.removeprefix(prefix), requirement)
        lines.extend([
            f"end {self.proof_namespace}",
            "",
        ])
        for requirement in self.requirements:
            if not requirement.theorem_name.startswith(prefix):
                append_theorem(requirement.theorem_name, requirement)
        return "\n".join(lines)


class AstJsonEmitter:
    """Translate Python `ast` nodes into the versioned formalsw JSON schema."""

    def __init__(self, module: ast.Module, bindings_module: ast.Module | None = None):
        """Store the parsed Python module."""
        self.module = module
        self.bindings_module = module if bindings_module is None else bindings_module

    def emit(self) -> str:
        """Render the complete JSON document."""
        document = {
            "schema_version": 1,
            "ast": {
                "type": "Module",
                "body": [self.stmt(stmt) for stmt in self.module.body],
            },
        }
        return json.dumps(document, indent=2, ensure_ascii=False) + "\n"

    def stmt(self, stmt: ast.stmt) -> dict[str, object]:
        """Retain unsupported statements as explicit diagnostic AST nodes."""
        try:
            return self.supported_stmt(stmt)
        except UnsupportedSyntax as error:
            return {"type": "Unsupported", "description": str(error), "source": ast.dump(stmt)}

    def supported_stmt(self, stmt: ast.stmt) -> dict[str, object]:
        """Encode one represented Python statement."""
        match stmt:
            case ast.Import(names=names):
                return {"type": "Import", "names": [
                    {"name": alias.name, "binding": alias.asname or alias.name.split('.')[0]}
                    for alias in names]}
            case ast.ImportFrom(module=module, names=names, level=0) if module is not None:
                return {
                    "type": "ImportFrom",
                    "module": module,
                    "names": [{"name": alias.name, "binding": alias.asname or alias.name} for alias in names],
                }
            case ast.ClassDef(name=name, bases=[], keywords=[], body=body):
                if stmt.decorator_list:
                    raise UnsupportedSyntax(f"{name}: decorators are unsupported")
                return {
                    "type": "ClassDef",
                    "name": name,
                    "body": [self.stmt(child) for child in body],
                }
            case ast.FunctionDef(name=name, args=args, returns=returns, body=body):
                if stmt.decorator_list:
                    raise UnsupportedSyntax(f"{name}: decorators are unsupported")
                return {
                    "type": "FunctionDef",
                    "name": name,
                    "args": self.arguments(args),
                    "returns": self.expr(returns) if returns is not None else None,
                    "body": [self.stmt(child) for child in body],
                }
            case ast.Pass():
                return {"type": "Expr", "value": self.constant(None)}
            case ast.Break():
                return {"type": "Break"}
            case ast.Continue():
                return {"type": "Continue"}
            case ast.Return(value=value):
                return {
                    "type": "Return",
                    "value": self.expr(value) if value is not None else self.constant(None),
                }
            case ast.Assign(targets=targets, value=value):
                return {
                    "type": "Assign",
                    "targets": [self.expr(target) for target in targets],
                    "value": self.expr(value),
                }
            case ast.AnnAssign(target=target, annotation=annotation, value=value):
                return {"type": "AnnAssign", "target": self.expr(target),
                        "annotation": self.expr(annotation),
                        "value": self.expr(value) if value is not None else None}
            case ast.Global(names=names):
                return {"type": "Global", "names": names}
            case ast.AugAssign(target=target, op=op, value=value):
                return {
                    "type": "AugAssign",
                    "target": self.expr(target),
                    "op": self.binop(op),
                    "value": self.expr(value),
                }
            case ast.For(target=target, iter=iter_expr, body=body, orelse=orelse):
                return {
                    "type": "For",
                    "target": self.expr(target),
                    "iter": self.expr(iter_expr),
                    "body": [self.stmt(child) for child in body],
                    "orelse": [self.stmt(child) for child in orelse],
                }
            case ast.If(test=test, body=body, orelse=orelse):
                return {
                    "type": "If",
                    "test": self.expr(test),
                    "body": [self.stmt(child) for child in body],
                    "orelse": [self.stmt(child) for child in orelse],
                }
            case ast.While(test=test, body=body, orelse=orelse):
                return {
                    "type": "While",
                    "test": self.expr(test),
                    "body": [self.stmt(child) for child in body],
                    "orelse": [self.stmt(child) for child in orelse],
                }
            case ast.Assert(test=test, msg=msg):
                return {
                    "type": "Assert",
                    "test": self.expr(test),
                    "msg": self.expr(msg) if msg is not None else None,
                }
            case ast.Raise(exc=exc, cause=None):
                return {
                    "type": "Raise",
                    "exc": self.expr(exc) if exc is not None else None,
                }
            case ast.Raise():
                raise UnsupportedSyntax("raise ... from ... is unsupported")
            case ast.Expr(value=value):
                return {"type": "Expr", "value": self.expr(value)}
            case _:
                raise UnsupportedSyntax(f"unsupported statement: {type(stmt).__name__}")

    def arguments(self, args: ast.arguments) -> list[dict[str, object]]:
        """Encode supported Python function arguments."""
        if args.posonlyargs or args.vararg or args.kwonlyargs or args.kwarg:
            raise UnsupportedSyntax("only plain positional args supported")
        result = [self.arg(arg) for arg in args.args]
        for arg, default in zip(result[len(result) - len(args.defaults):], args.defaults):
            try:
                value = literal_default(default)
            except ValueError as error:
                raise UnsupportedSyntax(str(error)) from error
            arg['default'] = self.expr(ast.Constant(value=value))
        return result

    def arg(self, arg: ast.arg) -> dict[str, object]:
        """Encode one supported Python function argument."""
        return {
            "name": arg.arg,
            "annotation": self.expr(arg.annotation) if arg.annotation is not None else None,
        }

    def expr(self, expr: ast.expr) -> dict[str, object]:
        """Encode one Python expression."""
        comprehension = range_sum(expr)
        if comprehension is not None:
            return {"type": "SumRange", "name": comprehension.name,
                    "element": self.expr(comprehension.element),
                    "bounds": [self.expr(arg) for arg in comprehension.bounds],
                    "conditions": [self.expr(condition) for condition in comprehension.conditions]}
        match expr:
            case ast.Constant(value=value):
                return self.constant(value)
            case ast.Name(id=name):
                return {"type": "Name", "id": name}
            case ast.Attribute(value=value, attr=attr):
                return {
                    "type": "Attribute",
                    "value": self.expr(value),
                    "attr": attr,
                }
            case ast.List(elts=elts):
                return {"type": "List", "elts": [self.expr(elt) for elt in elts]}
            case ast.Tuple(elts=elts):
                return {"type": "Tuple", "elts": [self.expr(elt) for elt in elts]}
            case ast.BinOp(left=left, op=op, right=right):
                return {
                    "type": "BinOp",
                    "left": self.expr(left),
                    "op": self.binop(op),
                    "right": self.expr(right),
                }
            case ast.UnaryOp(op=op, operand=operand):
                return {
                    "type": "UnaryOp",
                    "op": self.unaryop(op),
                    "operand": self.expr(operand),
                }
            case ast.BoolOp(op=op, values=values):
                return {
                    "type": "BoolOp",
                    "op": self.boolop(op),
                    "values": [self.expr(value) for value in values],
                }
            case ast.IfExp(test=test, body=body, orelse=orelse):
                return {"type": "IfExp", "test": self.expr(test),
                        "body": self.expr(body), "orelse": self.expr(orelse)}
            case ast.Compare(left=left, ops=ops, comparators=comparators):
                return {
                    "type": "Compare",
                    "left": self.expr(left),
                    "ops": [self.cmpop(op) for op in ops],
                    "comparators": [self.expr(comparator) for comparator in comparators],
                }
            case ast.Call(func=func, args=args, keywords=[]):
                if isinstance(func, ast.Attribute) and func.attr == 'bit_length' and not args:
                    return {"type": "BuiltinCall", "name": "int.bit_length", "args": [self.expr(func.value)]}
                reversed_value = reversed_list(expr)
                if (reversed_value is not None
                        and not any(bindings(self.bindings_module, name) for name in ('list', 'reversed'))):
                    return {"type": "ReversedList", "value": self.expr(reversed_value)}
                if isinstance(func, ast.Name) and func.id in ('str', 'max') and not bindings(self.bindings_module, func.id):
                    return {"type": "BuiltinCall", "name": func.id,
                            "args": [self.expr(arg) for arg in args]}
                return {
                    "type": "Call",
                    "func": self.expr(func),
                    "args": [self.expr(arg) for arg in args],
                }
            case ast.Subscript(value=value, slice=slice_expr):
                return {
                    "type": "Subscript",
                    "value": self.expr(value),
                    "slice": self.expr(slice_expr),
                }
            case ast.Slice(lower=lower, upper=upper, step=step):
                return {
                    "type": "Slice",
                    "lower": self.expr(lower) if lower is not None else None,
                    "upper": self.expr(upper) if upper is not None else None,
                    "step": self.expr(step) if step is not None else None,
                }
            case _:
                raise UnsupportedSyntax(f"unsupported expression: {ast.dump(expr)}")

    def constant(self, value: object) -> dict[str, object]:
        """Encode one Python constant."""
        if isinstance(value, bytes):
            return {"type": "Bytes", "value": list(value)}
        if isinstance(value, (bool, int, str)) or value is None:
            return {"type": "Constant", "value": value}
        raise UnsupportedSyntax(f"unsupported constant: {value!r}")

    def unaryop(self, op: ast.unaryop) -> str:
        """Encode a supported Python unary operator."""
        match op:
            case ast.USub():
                return "USub"
            case ast.Not():
                return "Not"
            case _:
                raise UnsupportedSyntax(f"unsupported unary operator: {type(op).__name__}")

    def boolop(self, op: ast.boolop) -> str:
        """Encode a supported Python boolean operator."""
        match op:
            case ast.And():
                return "And"
            case ast.Or():
                return "Or"
            case _:
                raise UnsupportedSyntax(f"unsupported boolean operator: {type(op).__name__}")

    def binop(self, op: ast.operator) -> str:
        """Encode a supported Python binary operator."""
        match op:
            case ast.Add():
                return "Add"
            case ast.Sub():
                return "Sub"
            case ast.Mult():
                return "Mult"
            case ast.Pow():
                return "Pow"
            case ast.FloorDiv():
                return "FloorDiv"
            case ast.Mod():
                return "Mod"
            case _:
                raise UnsupportedSyntax(f"unsupported binary operator: {type(op).__name__}")

    def cmpop(self, op: ast.cmpop) -> str:
        """Encode a supported Python comparison operator."""
        match op:
            case ast.Eq():
                return "Eq"
            case ast.NotEq():
                return "NotEq"
            case ast.Lt():
                return "Lt"
            case ast.LtE():
                return "LtE"
            case ast.Gt():
                return "Gt"
            case ast.GtE():
                return "GtE"
            case _:
                raise UnsupportedSyntax(f"unsupported comparison: {type(op).__name__}")


class AstLeanBridgeEmitter:
    """Render the small Lean module that imports a generated JSON AST."""

    def __init__(self, json_path: Path, namespace: str, module: ast.Module, conditions=None):
        """Store the JSON file name and output Lean namespace."""
        self.json_path = json_path
        self.namespace = namespace
        self.conditions = conditions or {}
        self.expressions = AstJsonEmitter(module)

    def emit(self) -> str:
        """Render a Lean definition loaded from the adjacent JSON file."""
        return "\n".join([
            "import FormalSW",
            "",
            "/-! Generated by formalsw. Do not edit by hand. -/",
            "",
            f"namespace {self.namespace}",
            "open FormalSW.PyAst",
            "",
            "/-- The Python AST imported from the adjacent JSON document. -/",
            "def module : Module :=",
            f"  pyast_from_json% (include_str {lean_string(self.json_path.name)})",
            "",
            *(f"def {name} : Expr := pyexpr_from_json% {lean_string(json.dumps(self.expressions.expr(expr)))}"
              for name, expr in self.conditions.items()),
            "",
            f"end {self.namespace}",
            "",
        ])


def camel_component(component: str) -> str:
    """Convert one path/name component into a Lean namespace component."""
    words = re.split(r"[^0-9A-Za-z]+", component)
    return "".join(word[:1].upper() + word[1:] for word in words if word)


def lean_import_component(component: str) -> str:
    """Return one filesystem path component rendered as a Lean import component."""
    if re.fullmatch(r"[A-Za-z_][A-Za-z0-9_']*", component):
        return component
    return f"«{component}»"


def lean_module_for_path(path: Path) -> str:
    """Return the Lean module name for a `.lean` file under the current directory."""
    try:
        relative = path.resolve().relative_to(Path.cwd().resolve())
    except ValueError as error:
        raise SystemExit(
            f"error: {path}: proof files outside the current directory "
            "cannot be imported by formalsw"
        ) from error
    without_suffix = relative.with_suffix("")
    return ".".join(lean_import_component(component) for component in without_suffix.parts)


def namespace_for_source(source: Path) -> str:
    """Return the generated Lean namespace for a Python source file."""
    if source.stem[:1].isdigit():
        # Numeric filenames need an identifier prefix, and files in different
        # directories must remain importable together (e.g. two implementations).
        relative = source.resolve().relative_to(Path.cwd().resolve())
        return ".".join(
            [*(camel_component(part) for part in relative.parent.parts),
             "P" + camel_component(source.stem) + "Ast"]
        )
    return camel_component(source.stem) + "Ast"


def git_root_for_source(source: Path) -> Path | None:
    """Ask Git for the worktree root, ignoring invalid `.git` directories."""
    if shutil.which("git") is None:
        return None
    result = subprocess.run(
        ["git", "-C", str(source.resolve().parent), "rev-parse", "--show-toplevel"],
        text=True, capture_output=True,
    )
    return Path(result.stdout.strip()) if result.returncode == 0 else None


def generated_path_for_source(source: Path, suffix: str) -> Path:
    """Return a generated-file path for a Python source."""
    git_root = git_root_for_source(source)
    if git_root is not None:
        relative_source = source.resolve().relative_to(git_root)
        return git_root / ".formalsw" / relative_source.parent / f"{source.name}{suffix}"
    return source.parent / ".formalsw" / f"{source.name}{suffix}"


def ast_path_for_source(source: Path) -> Path:
    """Return the generated Lean JSON-import bridge for a Python source file."""
    return generated_path_for_source(source, ".ast.lean")


def ast_json_path_for_source(source: Path) -> Path:
    """Return the generated JSON AST path for a Python source file."""
    return generated_path_for_source(source, ".ast.json")


def proof_path_for_source(source: Path) -> Path:
    """Return the Lean proof path paired with a Python source file."""
    return source.with_name(source.name + ".lean")


def requirements_path_for_source(source: Path) -> Path:
    """Return the generated Lean requirements path for a Python source file."""
    return generated_path_for_source(source, ".reqs.lean")


def olean_path_for_lean(source: Path) -> Path:
    """Cache all source-bound modules in the same Lake object tree.

    Lean resolves a module prefix in one search-path directory. Splitting AST
    objects and proof objects between roots therefore breaks nested repositories,
    where their module names share a directory prefix.
    """
    try:
        relative = source.resolve().relative_to(Path.cwd().resolve())
    except ValueError as error:
        raise SystemExit(
            f"error: {source}: Lean files outside the current directory "
            "cannot be cached by formalsw"
        ) from error
    return Path.cwd() / ".lake/build/lib/lean" / relative.with_suffix(".olean")


def lean_env() -> dict[str, str]:
    """Use Lake's toolchain environment, prioritizing this project's objects.

    Dependencies can have their own generated `.formalsw` namespace. Lake puts
    dependency paths first, which would hide the current project's AST objects.
    """
    completed = subprocess.run(
        lake_command("env", sys.executable, "-c",
                     "import json, os; print(json.dumps(dict(os.environ)))"),
        env=runtime_env(), text=True, capture_output=True, check=True,
    )
    env = json.loads(completed.stdout)
    paths = [str(Path.cwd() / ".lake/build/lib/lean"), "."]
    if env.get("LEAN_PATH"):
        paths.append(env["LEAN_PATH"])
    env["LEAN_PATH"] = os.pathsep.join(paths)
    return env


def useful_diagnostic_lines(output: str) -> list[str]:
    """Return the short diagnostic lines worth showing to users."""
    lines = []
    for line in output.splitlines():
        stripped = line.strip()
        if not stripped:
            continue
        if stripped.startswith("Build completed successfully"):
            continue
        if stripped.startswith("✔ "):
            continue
        if "Traceback (most recent call last)" in stripped:
            continue
        if stripped.startswith("File ") or stripped.startswith("subprocess."):
            continue
        if "error" in stripped or "warning" in stripped or "Unknown identifier" in stripped:
            lines.append(line)
    if lines:
        return lines[:8]
    return [
        line for line in output.splitlines()
        if line.strip() and not line.startswith("Build completed successfully")
    ][:8]


def first_lean_error(output: str) -> tuple[Path, int, str] | None:
    """Return the first Lean diagnostic location and message from output."""
    pattern = re.compile(r"^(.+?):(\d+):\d+:\s+(?:error(?:\([^)]*\))?:\s*)?(.*)$")
    for line in output.splitlines():
        match = pattern.match(line.strip())
        if match is None:
            continue
        return Path(match.group(1)), int(match.group(2)), match.group(3).strip()
    return None


def first_sorry_line(path: Path) -> int | None:
    """Return the first line in a Lean file that contains `sorry`."""
    for index, line in enumerate(path.read_text().splitlines(), start=1):
        if re.search(r"\bsorry\b", line):
            return index
    return None


def proof_body_start_in_requirements(proof_path: Path) -> tuple[int, int]:
    """Return `(generated_start_line, original_start_line)` for embedded proof body."""
    proof_lines = proof_path.read_text().splitlines()
    import_count = 0
    while import_count < len(proof_lines) and (
        not proof_lines[import_count].strip()
        or proof_lines[import_count].startswith("import ")
    ):
        import_count += 1
    return import_count + 8, import_count + 1


def unknown_identifier(output: str) -> str | None:
    """Return the unknown identifier reported by Lean, if any."""
    match = re.search(r"Unknown identifier `([^`]+)`", output)
    if match is None:
        return None
    return match.group(1)


def final_error_line(
    completed: subprocess.CompletedProcess[str],
    proof_path: Path | None,
    requirements_path: Path | None,
    expected: list[Requirement] | None,
) -> str:
    """Return the final source-mapped user-facing error line."""
    output = completed.stdout + completed.stderr
    identifier = unknown_identifier(output)
    if identifier and expected:
        for requirement in expected:
            if requirement.theorem_name == identifier:
                return (
                    f"error: {requirement.source_path}:{requirement.source_line}: "
                    f"missing proof `{requirement.theorem_name}` for "
                    f"`@formalsw: {requirement.marker}`"
                )
    if "declaration uses `sorry`" in output and proof_path is not None:
        line = first_sorry_line(proof_path)
        if line is not None:
            return f"error: {proof_path}:{line}: proof uses `sorry`"
    diagnostic = first_lean_error(output)
    if diagnostic is not None:
        diagnostic_path, diagnostic_line, message = diagnostic
        if (
            proof_path is not None
            and requirements_path is not None
            and diagnostic_path == requirements_path
        ):
            generated_start, original_start = proof_body_start_in_requirements(proof_path)
            original_line = original_start + diagnostic_line - generated_start
            if original_line >= original_start:
                return f"error: {proof_path}:{original_line}: {message}"
        return f"error: {diagnostic_path}:{diagnostic_line}: {message}"
    return f"error: command failed with exit {completed.returncode}"


def print_command_failure(
    command: list[str],
    completed: subprocess.CompletedProcess[str],
    message: str,
    hint: str | None = None,
    expected: list[Requirement] | None = None,
    proof_path: Path | None = None,
    requirements_path: Path | None = None,
) -> None:
    """Print a compact, user-facing subprocess failure."""
    print_diagnostic(message, file=sys.stderr)
    if hint is not None:
        print_diagnostic(hint, file=sys.stderr)
    if expected:
        print_diagnostic("Expected proof obligations:", file=sys.stderr)
        for requirement in expected:
            print_diagnostic(f"  {requirement.theorem_name} :", file=sys.stderr)
            print_diagnostic(indent(requirement.property_type, 4), file=sys.stderr)
    diagnostics = useful_diagnostic_lines(completed.stdout + completed.stderr)
    if diagnostics:
        print_diagnostic("Lean diagnostic:", file=sys.stderr)
        for line in diagnostics:
            print_diagnostic(f"  {line}", file=sys.stderr)
    print_diagnostic(final_error_line(completed, proof_path, requirements_path, expected), file=sys.stderr)


def run(
    command: list[str],
    env: dict[str, str] | None = None,
    failure_message: str = "command failed",
    failure_hint: str | None = None,
    expected: list[Requirement] | None = None,
    proof_path: Path | None = None,
    requirements_path: Path | None = None,
) -> None:
    """Run a subprocess command, failing the entrypoint cleanly if it fails."""
    completed = subprocess.run(
        command,
        env=env,
        text=True,
        stdout=subprocess.PIPE,
        stderr=subprocess.PIPE,
        check=False,
    )
    if completed.returncode == 0:
        return
    print_command_failure(
        command,
        completed,
        failure_message,
        failure_hint,
        expected,
        proof_path,
        requirements_path,
    )
    raise SystemExit(completed.returncode)


def require_executable(name: str) -> None:
    """Fail with a clear message when an external executable is unavailable."""
    if shutil.which(name) is None:
        raise SystemExit(f"required executable not found on PATH: {name}")


def module_with_python_builtins(source: Path, module: ast.Module) -> ast.Module:
    """Append plain-Python builtin-class definitions to a program AST."""
    stdlib_source = Path(__file__).resolve().parent / "lang/py/builtin/type/str.py"
    if source.resolve().parent == stdlib_source.resolve().parent:
        return module
    if not stdlib_source.exists():
        raise SystemExit(
            f"required Python standard-library model not found: {stdlib_source}"
        )
    stdlib_module = ast.parse(
        stdlib_source.read_text(),
        filename=str(stdlib_source),
    )
    return ast.Module(
        body=[*module.body, *stdlib_module.body],
        type_ignores=[*module.type_ignores, *stdlib_module.type_ignores],
    )


def source_bindings(source: Path, module: ast.Module, semantic_module: ast.Module) -> ast.Module:
    """Builtin implementations use the appended model classes as constructors.

    Ordinary programs resolve Python builtins in their own source environment.
    """
    models = Path(__file__).resolve().parent / 'lang/py/builtin'
    return semantic_module if source.resolve().is_relative_to(models) else module


def check_source(source: Path, report: CheckReport) -> int:
    """Compile-check one Python file and its paired Lean proof."""
    ast_path = ast_path_for_source(source)
    ast_json_path = ast_json_path_for_source(source)
    proof_path = proof_path_for_source(source)
    requirements_path = requirements_path_for_source(source)
    namespace = namespace_for_source(source)
    proof_namespace = proof_namespace_for_source(source)
    proof_module = lean_module_for_path(proof_path)

    run(
        [sys.executable, "-m", "py_compile", str(source)],
        failure_message=f"Python syntax check failed for {source}",
        failure_hint="Fix the Python syntax error before running Lean proofs.",
    )
    module = source_module(source)
    rejected_before = report.unsupported
    requirements = collect_requirements(source, module, proof_namespace, namespace)
    requirements = filter_supported_requirements(requirements, report)
    if not requirements and report.unsupported > rejected_before:
        return 0
    if not requirements and not proof_path.exists():
        return 0
    semantic_module = module_with_python_builtins(source, module)
    bindings_module = source_bindings(source, module, semantic_module)
    if requirements and not proof_path.exists():
        first = requirements[0]
        print_diagnostic(
            f"error: {first.source_path}:{first.source_line}: "
            f"missing proof file {proof_path} for `@formalsw: {first.marker}`",
            file=sys.stderr,
        )
        raise SystemExit(1)
    ast_path.parent.mkdir(parents=True, exist_ok=True)
    requirements_path.parent.mkdir(parents=True, exist_ok=True)
    ast_json_path.write_text(AstJsonEmitter(semantic_module, bindings_module=bindings_module).emit())
    ast_path.write_text(AstLeanBridgeEmitter(ast_json_path, namespace, bindings_module, module.formalsw_conditions).emit())
    requirements_path.write_text(
        RequirementEmitter(proof_path, proof_module, requirements).emit()
    )
    ast_olean_path = olean_path_for_lean(ast_path)
    proof_olean_path = olean_path_for_lean(proof_path)
    requirements_olean_path = olean_path_for_lean(requirements_path)
    for lean_path, olean_path in [
        (ast_path, ast_olean_path),
        (proof_path, proof_olean_path),
        (requirements_path, requirements_olean_path),
    ]:
        olean_path.parent.mkdir(parents=True, exist_ok=True)
        lean_path.with_suffix(".olean").unlink(missing_ok=True)
    require_executable("lake")
    run(
        lake_command("build", "FormalSW", "lang.py.FormalSW"),
        env=runtime_env(),
        failure_message="failed to build the FormalSW core or Python model",
        failure_hint="Fix the Lean libraries before checking Python source proofs.",
    )
    run([
        "lean",
        "-o",
        str(ast_olean_path),
        str(ast_path),
    ],
        env=lean_env(),
        failure_message=f"generated JSON AST failed to import for {source}",
        failure_hint=(
            f"This usually means formalsw generated invalid JSON in {ast_json_path} "
            f"or an invalid Lean import bridge in {ast_path}."
        ),
    )
    run([
        "lean",
        "-DwarningAsError=true",
        "-o",
        str(proof_olean_path),
        str(proof_path),
    ],
        env=lean_env(),
        failure_message=f"proof check failed for {source}",
        failure_hint=(
            f"Complete {proof_path}; remove any `sorry`; and make sure it "
            "compiles before checking requested proof obligations."
        ),
        expected=requirements,
        proof_path=proof_path,
        requirements_path=requirements_path,
    )
    run([
        "lean",
        "-DwarningAsError=true",
        "-o",
        str(requirements_olean_path),
        str(requirements_path),
    ],
        env=lean_env(),
        failure_message=f"proof check failed for {source}",
        failure_hint=(
            f"Complete {proof_path}; remove any `sorry`; and make sure every "
            "`@formalsw:` requirement has a theorem with the expected name and type."
        ),
        expected=requirements,
        proof_path=proof_path,
        requirements_path=requirements_path,
    )
    return len(requirements)


def stub_source(source: Path, report: CheckReport) -> str:
    """Return a complete Lean proof stub for one Python source file."""
    module = source_module(source)
    AstJsonEmitter(module).emit()
    proof_namespace = proof_namespace_for_source(source)
    requirements = collect_requirements(
        source,
        module,
        proof_namespace,
        namespace_for_source(source),
    )
    requirements = filter_supported_requirements(requirements, report)
    return ProofStubEmitter(
        lean_module_for_path(ast_path_for_source(source)),
        proof_namespace,
        requirements,
    ).emit()


def iter_python_sources(directory: Path) -> list[Path]:
    """Return Python sources under a directory, excluding generated/cache trees."""
    sources = []
    for path in sorted(directory.rglob("*.py")):
        if any(part in {".formalsw", "__pycache__"} for part in path.parts):
            continue
        sources.append(path)
    return sources


def dependency_imports(requirements: list[Requirement]) -> list[str]:
    return [f"import {lean_module_for_path(proof_path_for_source(path))}"
            for path in dict.fromkeys(path for req in requirements for path in req.dependencies)]


def proof_dependencies(source: Path) -> list[Path]:
    """Find source-bound imports of adjacent Python proofs and generated ASTs."""
    proof = proof_path_for_source(source)
    module = source_module(source)
    functions = {stmt.name for stmt in module.body if isinstance(stmt, ast.FunctionDef)}
    dependencies = list(module.formalsw_link_dependencies)
    # Dependency discovery needs only the imported binding. Do not compile raw
    # Python quotations or elaborate requirements twice for every source file.
    for function in module.body:
        if not isinstance(function, (ast.FunctionDef, ast.AsyncFunctionDef)):
            continue
        if getattr(function, 'formalsw_imported', False):
            continue
        for marker in function.formalsw_markers:
            parsed = parse_short_marker(marker.text)
            if parsed and parsed[0] in ("Equiv", "EquivReturn") and len(parsed[1]) == 1 and (marker.reference is not None or parsed[1][0] not in functions):
                try:
                    path, _, _ = marker.reference or resolve_function(source, module, parsed[1][0])
                except ContractError as error:
                    raise InvalidRequirement(str(error)) from error
                if path != source.resolve() and path not in dependencies:
                    dependencies.append(path)
    for dependency in dependencies:
        if not proof_path_for_source(dependency).is_file():
            raise SystemExit(f"error: imported Python source or adjacent proof is missing: {dependency}")
    if not proof.is_file():
        return dependencies
    for parts in parse_imports(proof.read_text()):
        if parts[-1].endswith(".py"):
            dependency = Path.cwd().joinpath(*parts)
        elif parts[-1].endswith(".py.ast") and ".formalsw" in parts:
            parts = [part for part in parts if part != ".formalsw"]
            dependency = Path.cwd().joinpath(*parts).with_suffix("")
            if dependency.resolve() == source.resolve():
                continue
        else:
            continue
        dependency = dependency.resolve()
        if not dependency.is_relative_to(Path.cwd().resolve()):
            raise SystemExit(f"error: imported Python source is outside the project: {dependency}")
        if not dependency.is_file() or not proof_path_for_source(dependency).is_file():
            raise SystemExit(f"error: imported Python source or adjacent proof is missing: {dependency}")
        dependencies.append(dependency)
    return dependencies


def check_sources(sources: list[Path], report: CheckReport) -> None:
    """Check imported Python proofs first, once per invocation, without stale fallbacks."""
    checked: dict[Path, bool] = {}
    visiting: list[Path] = []

    def visit(source: Path) -> bool:
        source = source.resolve()
        if source in checked:
            return checked[source]
        if source in visiting:
            chain = " -> ".join(str(path) for path in [*visiting, source])
            print_diagnostic(f"error: cyclic Python proof imports: {chain}", file=sys.stderr)
            return False
        visiting.append(source)
        unsupported_before = report.unsupported
        failures_before = report.failed_files
        try:
            for dependency in proof_dependencies(source):
                if not visit(dependency):
                    raise SystemExit(f"error: {source}: imported Python proof failed: {dependency}")
            report.passed += check_source(source, report)
        except (UnsupportedSyntax, InvalidRequirement, ScenarioError, SyntaxError) as error:
            print_diagnostic(f"error: {source}: {error}", file=sys.stderr)
            report.failed_files += 1
        except SystemExit as error:
            if error.code != 0:
                if isinstance(error.code, str):
                    print_diagnostic(error.code, file=sys.stderr)
                report.failed_files += 1
        visiting.pop()
        checked[source] = (report.unsupported == unsupported_before
                           and report.failed_files == failures_before)
        return checked[source]

    for source in sources:
        visit(source)


def filter_supported_requirements(requirements: list[Requirement], report: CheckReport) -> list[Requirement]:
    supported = []
    for requirement in requirements:
        if not requirement.unsupported:
            supported.append(requirement)
            continue
        report.unsupported += 1
        print_diagnostic(f"error: {requirement.source_path}:{requirement.source_line}: "
              f"cannot check {requirement.theorem_name}: unsupported Python constructs", file=sys.stderr)
        for issue in requirement.unsupported:
            via = " -> ".join((*issue.dependency, issue.function))
            print_diagnostic(f"  {requirement.source_path}:{issue.line}: {via}: {issue.reason}", file=sys.stderr)
    return supported


def finish_report(report: CheckReport, *, stub: bool = False) -> None:
    if report.unsupported or report.failed_files:
        raise SystemExit(1)
    if not stub:
        print(f"All {report.passed} checks passed")


def main() -> None:
    """Compile-check Python source files against paired Lean proof files."""
    parser = argparse.ArgumentParser()
    parser.add_argument(
        "-S",
        "--stub",
        action="store_true",
        help="print a Lean proof-file stub to stdout",
    )
    parser.add_argument("source", type=Path)
    args = parser.parse_args()

    source = args.source
    report = CheckReport()
    if args.stub:
        if not source.is_file():
            parser.error("--stub requires one Python source file")
        try:
            print(stub_source(source, report), end="")
        except (UnsupportedSyntax, InvalidRequirement) as error:
            print_diagnostic(f"error: {source}: {error}", file=sys.stderr)
            report.failed_files += 1
        except SystemExit as error:
            if error.code != 0:
                if isinstance(error.code, str):
                    print_diagnostic(error.code, file=sys.stderr)
                report.failed_files += 1
        finish_report(report, stub=True)
        return
    sources = iter_python_sources(source) if source.is_dir() else [source]
    if not sources:
        raise SystemExit(f"error: {source}: no Python files found")
    check_sources(sources, report)
    finish_report(report)


if __name__ == "__main__":
    main()
