import textwrap
from pathlib import Path

import pytest

from rflx.generator.optimizer import gnatprove_supports_limit_lines, optimize
from tests import utils


def test_optimize(tmp_path: Path) -> None:
    source_dir = tmp_path / "src"
    source_dir.mkdir()

    project_file = tmp_path / "test.gpr"
    project_file.write_text(
        f'project Test is\n   for Source_Dirs use ("{source_dir}");\nend Test;\n',
    )

    f = source_dir / "test-fsm.adb"
    f.write_text(
        textwrap.dedent(
            """\
            -- Generated by RecordFlux
            procedure Test with
               SPARK_Mode
            is
            begin
               if False then
                  goto Error;
               end if;
               <<Error>>
            end Test;
            """,
        ),
    )

    optimize(project_file)

    assert f.read_text() == textwrap.dedent(
        """\
        -- Generated by RecordFlux
        procedure Test with
           SPARK_Mode
        is
        begin
           <<Error>>
        end Test;
        """,
    )


@pytest.mark.skipif(utils.spark_version() != "24", reason="depends on SPARK 24")
def test_gnatprove_supports_limit_lines_24() -> None:
    assert not gnatprove_supports_limit_lines()


@pytest.mark.skipif(utils.spark_version() != "25", reason="depends on SPARK 25")
def test_gnatprove_supports_limit_lines_25() -> None:
    assert gnatprove_supports_limit_lines()
