#!/usr/bin/env python3
"""Exercise unsupported-source rejection through the public CLI."""
from pathlib import Path
import subprocess
import textwrap

from test_support import project_temporary_directory

REPO = Path(__file__).resolve().parents[2]
FORMALSW = REPO / 'formalsw'


def stub(path):
    return subprocess.run([str(FORMALSW), '--stub', str(path)], cwd=REPO,
                          text=True, capture_output=True)


CASES = [
    ('unsupported code inside a parallel loop', '''
        from threading import Lock
        def f(mutex: Lock):
            """@formalsw: theorem bad : True"""
            while True:
                if False:
                    print("still unsupported")
                mutex.acquire()
                mutex.release()
    ''', 'parallel execution supports'),
    ('parallel chained comparison', '''
        from threading import Lock
        def f(n: int, mutex: Lock):
            """@formalsw: theorem bad : True"""
            while 0 < n < 10:
                n = n - 1
    ''', 'parallel comparisons currently support one operator'),
    ('rebound primitive inside a parallel loop', '''
        from threading import Lock
        sleep = lambda n: None
        def f(mutex: Lock):
            """@formalsw: theorem bad : True"""
            while True:
                sleep(0)
    ''', 'unshadowed from time import sleep'),
    ('special exception constructor', '''
        items = [1]
        def f(n: int):
            """@formalsw: Returns"""
            items.append(n)
            raise OSError(2, "missing")
    ''', 'special builtin exception constructors are unsupported'),
    ('dictionary global', '''
        items = {"n": 1}
        def f(n: int):
            """@formalsw: Returns"""
            return items["n"]
    ''', 'supported state is int, str, bool, or homogeneous scalar lists'),
    ('nested mutable global', '''
        items = [[1]]
        def f(n: int):
            """@formalsw: Returns"""
            return items[0]
    ''', 'supported state is int, str, bool, or homogeneous scalar lists'),
    ('unsupported heap method', '''
        items = [1]
        def f(n: int):
            """@formalsw: Returns"""
            items.pop()
    ''', 'Call expression is unsupported by heap execution'),
    ('unsupported dead heap code', '''
        items = [1]
        def f(n: int):
            """@formalsw: Returns"""
            items.append(n)
            return
            print(n)
    ''', 'Call expression is unsupported by heap execution'),
    ('recursive list comparison', '''
        items = [1]
        def f(n: int):
            """@formalsw: Returns"""
            return items == [n]
    ''', 'recursive list comparison is not yet supported'),
    ('nested heap write', '''
        items = [1]
        def f(n: int):
            """@formalsw: Returns"""
            items.append(items)
    ''', 'nested mutable containers are not yet supported'),
    ('unsupported augmented slice', '''
        items = [1]
        def f(n: int):
            """@formalsw: Returns"""
            items[:] += [n]
    ''', 'Slice expression is unsupported by heap execution'),
    ('shadowed heap len', '''
        items = [1]
        len = 3
        def f(n: int):
            """@formalsw: Returns"""
            return len(items)
    ''', 'Call expression is unsupported by heap execution'),
    ('scalar model cannot discard heap', '''
        items = [1]
        def f(n: int):
            """@formalsw: theorem bad : (scalarFunctionWithGlobals _this_module "f" [.int 1] []).Returns"""
            items.append(n)
    ''', 'mutable globals require Mutable.function'),
    ('Equiv validates counterpart with selected heap interpreter', '''
        items = [1]
        def f(n: int):
            """@formalsw: Equiv(g)"""
            items.append(n)
        def g(n: int):
            for i in range(n):
                pass
    ''', 'For statement is unsupported by heap execution'),
    ('explicit heap model validates its own subset', '''
        def f(n: int):
            """@formalsw: theorem bad : (Mutable.function _this_module "f" [.scalar (.int 1)] [] []).Returns"""
            for i in range(n):
                pass
    ''', 'For statement is unsupported by heap execution'),
    ('parallel descriptors need a model', '''
        class Node:
            @property
            def next(self):
                return self
        def f(node: Node):
            """@formalsw: theorem invalid :
              Not Ensures(Parallel([this_function [.ref 0]], {}), fun _ => True)
            """
            following = node.next
    ''', 'parallel objects currently support plain data fields'),
    ('parallel array element types', '''
        def f(data: list[int]):
            """@formalsw: theorem invalid :
              Not Ensures(Parallel([this_function [.ref 0]], {}), fun _ => True)
            """
            data[0] = "wrong type"
    ''', 'parallel list writes must preserve the annotated element type'),
    ('parallel field layout', '''
        class Box:
            def __init__(self):
                self.value = 0
        def f(box: Box):
            """@formalsw: theorem invalid :
              Not Ensures(Parallel([this_function [.ref 0]], {}), fun _ => True)
            """
            box.value = "wrong type"
    ''', 'parallel field writes must preserve the declared scalar or reference layout'),
    ('unmodeled parallel statement', '''
        from threading import Lock
        from time import sleep
        def f(counter: list[int], mutex: Lock):
            """@formalsw: theorem invalid :
              Not Ensures(Parallel([this_function [.ref 0, .lock 0]], { objects := [.array [.int 0]] }), fun _ => True)
            """
            print(counter)
    ''', 'parallel execution supports'),
    ('shadowed parallel primitive', '''
        from threading import Lock
        from time import sleep
        def sleep(n):
            pass
        def f(counter: list[int], mutex: Lock):
            """@formalsw: theorem invalid :
              CanReturn(Parallel([this_function [.ref 0, .lock 0]], { objects := [.array [.int 0]] }), {})
            """
            sleep(0)
    ''', 'parallel execution requires an unshadowed from time import sleep'),
    ('concurrent worker used as scalar execution', '''
        from threading import Lock
        from time import sleep
        def f(counter: list[int], mutex: Lock):
            """@formalsw: Returns"""
            pass
    ''', 'concurrent workers require a raw Parallel specification'),
    ('unmodeled parallel return', '''
        """@formalsw: theorem invalid :
          Not Ensures(Parallel([parallelFunction ProbeAst.module "f" [.int 0]], {}), fun _ => True)
        """
        def f(n: int):
            return n
    ''', 'parallel execution supports'),
    ('compound parallel heap expression', '''
        from threading import Lock
        from time import sleep
        def f(counter: list[int], mutex: Lock):
            """@formalsw: theorem invalid :
              Not Ensures(Parallel([this_function [.ref 0, .lock 0]], { objects := [.array [.int 0]] }), fun _ => True)
            """
            counter[1] = counter[0] + 2
    ''', 'split shared reads into separate statements'),
    ('nested marker', '''
        class Example:
            def method(self):
                """@formalsw: Returns"""
                return 1
    ''', 'requirements on nested functions and class methods are unsupported'),
    ('type-changing loop', '''
        def f(n: int):
            """@formalsw: Not Halts"""
            while n:
                n = "oops"
                n = n - 1
    ''', 'Sub on these operand types is unsupported'),
    ('range shadowing', '''
        def f(range: int):
            """@formalsw: Returns"""
            for n in range(3):
                pass
    ''', 'only for name in range(stop) is supported'),
    ('exception shadowing', '''
        def f(ValueError: int):
            """@formalsw: Halts"""
            raise ValueError()
    ''', 'only builtin exception constructors are supported'),
    ('unsupported Throws signature', '''
        def f(a: int, b: int):
            """@formalsw: Not Throws"""
            return a + b
    ''', 'Throws has no function model for this argument signature'),
    ('unsupported ReturnType signature', '''
        def f(n: int) -> str:
            """@formalsw: Not ReturnType"""
            return "a"
    ''', 'ReturnType currently requires matching supported argument and return annotations'),
    ('equivalence domains', '''
        def f(n: int):
            """@formalsw: Not Equiv(g)"""
            return n
        def g(n: str):
            return n
    ''', 'Equiv requires matching supported argument domains'),
    ('module raw dependency', '''
        """@formalsw: theorem invalid :
          Not (scalarFunction ProbeAst.module "f" [.int 0]).Halts
        """
        def f(n: int):
            return abs(n)
    ''', "call to 'abs' is unsupported"),
    ('unknown object', '''
        def f(n: int):
            """@formalsw: theorem invalid :
              Not Halts(.object "Unknown" < .object "Unknown")
            """
            return n
    ''', "object class 'Unknown' is not defined"),
    ('async function', '''
        async def f(n: int):
            """@formalsw: Returns"""
            return n
    ''', 'async functions are unsupported'),
    ('mutable default argument', '''
        def f(n: int = []):
            """@formalsw: Returns"""
            return n
    ''', 'default arguments require immutable scalar literals'),
    ('unrepresented annotation', '''
        def f(n: int) -> int | str:
            """@formalsw: theorem irrelevant : True"""
            return n
    ''', 'this return annotation is unsupported by the AST model'),
    ('raw property dependency', '''
        """@formalsw: theorem invalid :
          Not (FormalSW.Property.Function.Throws ProbeAst.module "f")
        """
        def f(n: int):
            return abs(n)
    ''', "call to 'abs' is unsupported"),
    ('raw list model mismatch', '''
        """@formalsw: theorem invalid :
          Not (listFunction ProbeAst.module "f" []).Halts
        """
        def f(n: int):
            return n
    ''', 'list execution currently supports only the exact merge-sort body'),
]

with project_temporary_directory(prefix='support-check-') as directory:
    path = Path(directory) / 'probe.py'
    for name, source, reason in CASES:
        path.write_text(textwrap.dedent(source))
        result = stub(path)
        assert result.returncode == 1, (name, result.stdout, result.stderr)
        assert reason in result.stderr, (name, result.stderr)
        assert result.stderr.count('cannot check ') == 1, (name, result.stderr)
        assert 'sorry' not in result.stdout, (name, result.stdout)

    # Change an actual comparison dependency while leaving the sorting AST intact.
    source = (REPO / 'tests/py/sort.py').read_text()
    path.write_text(source.replace('return self.value <= other.value', 'return abs(self.value) <= other.value'))
    result = stub(path)
    assert result.returncode == 1, result.stdout
    assert "call to 'abs' is unsupported" in result.stderr, result.stderr
    assert 'merge_sort_untyped -> DummyInt' in result.stderr, result.stderr

    # Supported scalar methods can still fall outside the legacy typed-list model.
    path.write_text(source.replace('return self.value <= other.value', 'while True:\n            pass'))
    result = stub(path)
    assert result.returncode == 1, result.stdout
    assert 'typed object lists require' in result.stderr, result.stderr

    path.write_text(source + '''
def twice_wrapped(values: list[int]) -> list[int]:
    """@formalsw: Not ReturnType"""
    return merge_sort_int(values)
''')
    result = stub(path)
    assert result.returncode == 1, result.stdout
    assert 'only one delegation directly to a sorting implementation' in result.stderr, result.stderr

    # Changing a previously recognized sorting body must invalidate its contracts.
    path.write_text(source.replace('middle = len(values) // 2', 'print(values)\n    middle = len(values) // 2'))
    result = stub(path)
    assert result.returncode == 1, result.stdout
    assert 'this body does not match' in result.stderr, result.stderr

result = stub(REPO / 'tests/py/fail/unsupported/b_mixed.py')
assert result.returncode == 1, result.stdout
assert result.stdout.count('sorry') == 1, result.stdout
assert 'theorem identity.«Returns»' in result.stdout, result.stdout
assert result.stderr.count('cannot check ') == 2, result.stderr
print('Unsupported-source CLI regressions passed')
