# 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-Ebfer

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

from .parser import Parser
from .checker import OK, Error, check_development
from .term import render_term
from .eval import eval_ebfer


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'
    )
    parser.add_argument('--no-check', action='store_true',
        help='Do not check the Lome proofs in the input'
    )
    parser.add_argument('--no-eval', action='store_true',
        help='Do not evaluate the Ebfer program in the input'
    )

    options = parser.parse_args(args)
    if options.debug:
        for module in ("main", "reduce", "checker"):
            logging.getLogger(f"ebfer.{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 = []
        successes = []
        errors = []
        if not options.no_check:
            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 not options.no_eval:
            result = eval_ebfer(development)
            print(render_term(result))


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