Source code for deal._cli._prove

from __future__ import annotations

import sys
from argparse import ArgumentParser
from pathlib import Path
from typing import TYPE_CHECKING, Iterator, TextIO

from .._colors import get_colors
from ..linter._extractors import get_contracts
from ._base import Command
from ._common import get_paths

    import deal_solver
except ImportError:
    deal_solver = None  # type: ignore[assignment]
    from deal_solver import Theorem
except ImportError:
    Theorem = object  # type: ignore[misc,assignment]

    import astroid

TEMPLATE_MOD = '{blue}{name}{end}'
TEMPLATE_FUN = '  {magenta}{name}{end}'
TEMPLATE_CON = '    {color}{p.conclusion.value}{end} {p}'

class DealTheorem(Theorem):
    def get_contracts(func: astroid.FunctionDef) -> Iterator[deal_solver.Contract]:
        for contract in get_contracts(func):
            yield deal_solver.Contract(
                args=contract.args,  # type: ignore[arg-type]

def run_solver(
    path: Path,
    stream: TextIO,
    show_skipped: bool,
    colors: dict[str, str],
) -> int:
    file_name_shown = False
    text = path.read_text()
    theorems = DealTheorem.from_text(text)
    failed_count = 0
    for theorem in theorems:

        proof = theorem.prove()
        assert proof.conclusion is not None
        if proof.conclusion == deal_solver.Conclusion.SKIP and not show_skipped:

        if not file_name_shown:
            line = TEMPLATE_MOD.format(name=path, **colors)
            print(line, file=stream)
            file_name_shown = True

        line = TEMPLATE_FUN.format(, **colors)
        print(line, file=stream)
        line = TEMPLATE_CON.format(p=proof, color=colors[proof.color], **colors)
        print(line, file=stream)
        failed_count += proof.conclusion == deal_solver.Conclusion.FAIL
    return failed_count

[docs]class ProveCommand(Command): """Verify correctness of code. ```bash python3 -m deal prove project/ ``` Options: + `--skipped`: show skipped functions. + `--nocolor`: disable colored output. Exit code is equal to the failed theorems count. See [Formal Verification][verification] documentation for more information. [verification]: """ @staticmethod def init_parser(parser: ArgumentParser) -> None: parser.add_argument('--skipped', action='store_true', help='show skipped') parser.add_argument('--nocolor', action='store_true', help='colorless output') parser.add_argument('paths', nargs='+') def __call__(self, args) -> int: if deal_solver is None: # pragma: no cover self.print('deal-solver is required but not installed') self.print(f'{sys.executable} -m pip install deal-solver') return 1 colors = get_colors(args) failed = 0 for arg in args.paths: for path in get_paths(Path(arg)): failed += run_solver( path=path,, show_skipped=args.skipped, colors=colors, ) return failed