# Path: split_file.py
# def postprocess_split_proof_term(statements, do_warn=True, **kwargs):
#     def do_warn_method(statement_num, statement, proof_term):
#         kwargs['log']("""Warning: Your version of Coq suffers from bug #5349 (https://coq.inria.fr/bugs/show_bug.cgi?id=5349)
# and does not support [Proof (term).] with -time.  Falling back to
# replacing [Proof (term).] with [Proof. exact (term). Qed.], which may fail.""")
#     if do_warn and 'log' in kwargs.keys():
#         do_warn = do_warn_method
#     else:
#         do_warn = None
#     return list(postprocess_split_proof_term_iter(statements, do_warn))
# 
# Path: coq_version.py
# def get_coq_accepts_time(coqc_prog, **kwargs):
#     return get_coq_accepts_option(coqc_prog, '-time', **kwargs)
# 
# Path: coq_running_support.py
# def get_proof_term_works_with_time(coqc_prog, **kwargs):
#     contents = r"""Lemma foo : forall _ : Type, Type.
# Proof (fun x => x)."""
#     output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-time', '-q'), contents, 1, verbose_base=3, **kwargs)
#     return 'Error: Attempt to save an incomplete proof' not in output
# 
# Path: custom_arguments.py
# DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])
# 
# LOG_ALWAYS=None


import re, time
import split_definitions_old
import util
from subprocess import Popen, PIPE, STDOUT
from split_file import postprocess_split_proof_term
from coq_version import get_coq_accepts_time
from coq_running_support import get_proof_term_works_with_time
from custom_arguments import DEFAULT_LOG, LOG_ALWAYS
    log('Done.  Splitting to definitions...')

    rtn = []
    cur_definition = {}
    last_definitions = '||'
    cur_definition_names = '||'
    last_char_end = 0

    #log('re.findall(' + repr(r'Chars ([0-9]+) - ([0-9]+) [^\s]+ (.*?)<prompt>([^<]*?) < ([0-9]+) ([^<]*?) ([0-9]+) < ([^<]*?)</prompt>'.replace(' ', r'\s*')) + ', ' + repr(stdout) + ', ' + 'flags=re.DOTALL)', level=3)
    for i, prompt in enumerate(stdout.split('</prompt>')):
        log('Processing:\n%s' % prompt, level=4)
        if prompt.strip() == '': continue
        times = chars_time_reg.findall(prompt)
        if len(times) == 0:
            if i == 0:
                log('Warning: ignoring %s' % repr(prompt), level=3)
            else:
                log('Warning: Could not find timing info in %s' % repr(prompt), level=1)
            continue
        elif len(times) > 1:
            log('Warning: found multiple timing info in %s: %s' % (repr(prompt), repr(times)), level=1)
        full_response_text = chars_time_reg.sub(' ', prompt)
        for char_start, char_end in times:
            char_start, char_end = int(char_start), int(char_end)
            # if we've travelled backwards in time, as in
            # COQBUG(https://github.com/coq/coq/issues/14475); we just
            # ignore this statement
            if char_end <= last_char_end: continue
            match = prompt_reg.match(full_response_text)
            if not match:

# Path: split_file.py
# def postprocess_split_proof_term(statements, do_warn=True, **kwargs):
#     def do_warn_method(statement_num, statement, proof_term):
#         kwargs['log']("""Warning: Your version of Coq suffers from bug #5349 (https://coq.inria.fr/bugs/show_bug.cgi?id=5349)
# and does not support [Proof (term).] with -time.  Falling back to
# replacing [Proof (term).] with [Proof. exact (term). Qed.], which may fail.""")
#     if do_warn and 'log' in kwargs.keys():
#         do_warn = do_warn_method
#     else:
#         do_warn = None
#     return list(postprocess_split_proof_term_iter(statements, do_warn))
# 
# Path: coq_version.py
# def get_coq_accepts_time(coqc_prog, **kwargs):
#     return get_coq_accepts_option(coqc_prog, '-time', **kwargs)
# 
# Path: coq_running_support.py
# def get_proof_term_works_with_time(coqc_prog, **kwargs):
#     contents = r"""Lemma foo : forall _ : Type, Type.
# Proof (fun x => x)."""
#     output, cmds, retcode, runtime = get_coq_output(coqc_prog, ('-time', '-q'), contents, 1, verbose_base=3, **kwargs)
#     return 'Error: Attempt to save an incomplete proof' not in output
# 
# Path: custom_arguments.py
# DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])
# 
# LOG_ALWAYS=None


# Path: split_definitions.py
import re, time
import split_definitions_old
import util
from subprocess import Popen, PIPE, STDOUT
from split_file import postprocess_split_proof_term
from coq_version import get_coq_accepts_time
from coq_running_support import get_proof_term_works_with_time
from custom_arguments import DEFAULT_LOG, LOG_ALWAYS

    log('Done.  Splitting to definitions...')

    rtn = []
    cur_definition = {}
    last_definitions = '||'
    cur_definition_names = '||'
    last_char_end = 0

    #log('re.findall(' + repr(r'Chars ([0-9]+) - ([0-9]+) [^\s]+ (.*?)<prompt>([^<]*?) < ([0-9]+) ([^<]*?) ([0-9]+) < ([^<]*?)</prompt>'.replace(' ', r'\s*')) + ', ' + repr(stdout) + ', ' + 'flags=re.DOTALL)', level=3)
    for i, prompt in enumerate(stdout.split('</prompt>')):
        log('Processing:\n%s' % prompt, level=4)
        if prompt.strip() == '': continue
        times = chars_time_reg.findall(prompt)
        if len(times) == 0:
            if i == 0:
                log('Warning: ignoring %s' % repr(prompt), level=3)
            else:
                log('Warning: Could not find timing info in %s' % repr(prompt), level=1)
            continue
        elif len(times) > 1:
            log('Warning: found multiple timing info in %s: %s' % (repr(prompt), repr(times)), level=1)
        full_response_text = chars_time_reg.sub(' ', prompt)
        for char_start, char_end in times:
            char_start, char_end = int(char_start), int(char_end)
            # if we've travelled backwards in time, as in
            # COQBUG(https://github.com/coq/coq/issues/14475); we just
            # ignore this statement
            if char_end <= last_char_end: continue
            match = prompt_reg.match(full_response_text)
            if not match:

                log('Warning: Could not find statements in %d:%d: %s' % (char_start, char_end, full_response_text), level=LOG_ALWAYS)