#!/usr/bin/env python3
"""Check ordered Python setup independently of proof execution."""
import ast
from pathlib import Path
import runpy
import sys

from test_support import project_temporary_directory

REPO = Path(__file__).resolve().parents[2]
sys.path.insert(0, str(REPO))
api = runpy.run_path(str(REPO / 'formalsw'))
from lang import spec_setup


with project_temporary_directory(prefix='setup-check-') as temporary:
    directory = Path(temporary)
    reference = directory / 'setup_reference.py'
    reference.write_text('def first(n: int) -> int: return n\n'
                         'def second(n: int) -> int: return n + 1\n')
    source = directory / 'consumer.py'
    source.write_text('''
"""
@formalsw: Py
    import setup_reference as reference
    target = reference.first
    threshold = 4
"""

# Loading specifications must not execute the program being checked.
raise RuntimeError("ordinary source was executed")

def f(n: int) -> int:
    """
    @formalsw: Equiv(target)
    @formalsw: Py
        target = reference.second

        threshold = sum(range(4))
        n = 999
    @formalsw: Requires(n >= threshold)
    @formalsw: Equiv(target)
    @formalsw: Py threshold = -1
    @formalsw: Requires(n > threshold)
    """
    return n

def g(n: int) -> int:
    """
    @formalsw: Requires(n >= threshold)
    @formalsw: Equiv(target)
    """
    return n
''')
    original_path = sys.path[:]
    program = api['source_module'](source)
    assert api['source_module'](source) is program
    assert sys.path == original_path
    f, g = [node for node in program.body if isinstance(node, ast.FunctionDef)]
    assert [marker.reference[2].name for marker in f.formalsw_markers if marker.reference] == ['first', 'second']
    assert [marker.predicate for marker in f.formalsw_markers if marker.predicate] == ['n >= 6', 'n > -1']
    assert g.formalsw_markers[0].predicate == 'n >= 4'
    assert g.formalsw_markers[1].reference[2].name == 'first'
    assert all(not marker.text.startswith('Py') for marker in f.formalsw_markers)

    original = source.read_text()
    source.write_text(original + '\n# edited after setup\n')
    try:
        api['source_module'](source)
    except api['InvalidRequirement'] as error:
        assert 'source changed after specification loading' in str(error)
    else:
        raise AssertionError('stale source snapshot accepted')
    source.write_text(original)

    # A later directive cannot retroactively bind a preceding annotation.
    late = ast.parse('''
def f(n: int) -> int:
    """
    @formalsw: Equiv(target)
    @formalsw: Py from setup_reference import first as target
    @formalsw: Equiv(target)
    """
    return n
''')
    api['prepare_specification'](source, late)
    assert late.body[0].formalsw_markers[0].reference is None
    assert late.body[0].formalsw_markers[1].reference[2].name == 'first'

    # Failed imports and syntax errors carry source coordinates, and paths are
    # restored even when arbitrary setup code raises or tries to exit.
    for code in ('import nonexistent_formalsw_module', 'if', 'raise SystemExit(2)'):
        try:
            spec_setup.execute(code, {}, source, 23)
        except spec_setup.SetupError as error:
            assert f'{source}:23:' in str(error), str(error)
        else:
            raise AssertionError(code)
        assert sys.path == original_path

    for marker in ('Py', 'Py\n        '):
        program = ast.parse(f'def f():\n    """\n    @formalsw: {marker}\n    """\n    pass\n')
        try:
            api['prepare_specification'](source, program)
        except api['InvalidRequirement'] as error:
            assert 'Py needs Python statements' in str(error)
        else:
            raise AssertionError('empty setup accepted')

    # Same Python module cache semantics as ordinary imports, but function code
    # that no longer matches the file cannot silently select a stale definition.
    imported = sys.modules.pop('setup_reference')
    imported.first.__code__ = imported.second.__code__
    reference.write_text('def second(n: int) -> int: return n + 2\n')
    try:
        api['resolve_python_function'](imported.first)
    except api['ContractError'] as error:
        assert 'differs from its source definition' in str(error)
    else:
        raise AssertionError('modified function accepted')
    try:
        api['source_module'](source)
    except api['InvalidRequirement'] as error:
        assert 'source changed after specification loading' in str(error)
    else:
        raise AssertionError('stale imported reference accepted')

print('Python setup scope, ordering, and source binding checks passed')
