# Copyright (c) 2025-2026, Chris Pressey, Cat's Eye Technologies.
# This file is distributed under a 2-clause BSD license.  See LICENSES/ dir.
# SPDX-License-Identifier: LicenseRef-BSD-2-Clause-X-Lome

import logging
import sys
from argparse import ArgumentParser
from typing import List

from .parser import Parser
from .checker import OK, Error, check_development


logger = logging.getLogger(__name__)


def main(args: List[str]) -> None:
    logging.basicConfig(level=logging.WARN)
    parser = ArgumentParser()

    parser.add_argument('filenames', metavar='FILENAME', type=str, nargs='+',
        help='Source files to process'
    )
    parser.add_argument('--debug', action='store_true',
        help='Produce debugging output during proof checking'
    )

    options = parser.parse_args(args)
    if options.debug:
        for module in ("main", "reduce", "checker"):
            logging.getLogger(f"lome.{module}").setLevel(logging.DEBUG)
        logger.debug("debug logging enabled")

    for filename in options.filenames:
        with open(filename, "r") as f:
            development_text = f.read()
        development = Parser(development_text).development()
        logger.debug(f"parsed development: {development}")

        results = check_development(development)
        successes = [r for r in results if isinstance(r, OK)]
        errors = [r for r in results if isinstance(r, Error)]
        logger.debug(f"successes: {successes}")
        logger.debug(f"failures: {errors}")
        print(f"{len(successes)}/{len(results)} proofs verified.")

        if errors:
            for error in errors:
                print(error.msg)
            sys.exit(1)


if __name__ == '__main__':
    main(sys.argv[1:])