# Path: strip_comments.py
# def strip_comments(contents):
#     """Strips the comments from coq code in contents.
# 
#     The strings in contents are only preserved if there are no
#     comment-like tokens inside of strings.  Stripping should be
#     successful and correct, regardless of whether or not there are
#     comment-like tokens in strings.
# 
#     The behavior of this method is undefined if there are any
#     notations which change the meaning of '(*', '*)', or '"'.
# 
#     Note that we take some extra care to leave *) untouched when it
#     does not terminate a comment.
#     """
#     contents = contents.replace('(*', ' (* ').replace('*)', ' *) ')
#     tokens = contents.split(' ')
#     rtn = []
#     is_string = False
#     comment_level = 0
#     for token in tokens:
#         do_append = (comment_level == 0)
#         if is_string:
#             if token.count('"') % 2 == 1: # there are an odd number of '"' characters, indicating that we've ended the string
#                 is_string = False
#         elif token.count('"') % 2 == 1: # there are an odd number of '"' characters, so we're starting a string
#             is_string = True
#         elif token == '(*':
#             comment_level += 1
#             do_append = False
#         elif comment_level > 0 and token == '*)':
#             comment_level -= 1
#         if do_append:
#             rtn.append(token)
#     return ' '.join(rtn).replace(' (* ', '(*').replace(' *) ', '*)').strip('\n\t ')
# 
# Path: custom_arguments.py
# DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])
# 
# Path: coq_version.py
# def get_coq_accepts_time(coqc_prog, **kwargs):
#     return get_coq_accepts_option(coqc_prog, '-time', **kwargs)
# 
# Path: util.py
# PY3 = False


from strip_comments import strip_comments
from custom_arguments import DEFAULT_LOG
from coq_version import get_coq_accepts_time
from util import PY3
if PY3: from util import raw_input
import subprocess
import re
import util
    for statement_num, statement in enumerate(statements):
        match = PROOF_TERM_REG.match(statement)
        if match:
            indent, after_proof_space, proof_term, post_space = match.groups()
            if re.split(r'\s', proof_term)[0] not in ('using', 'with'): # Proof using ... and Proof with ... are special
                if on_first_example:
                    on_first_example(statement_num, statement, proof_term)
                    on_first_example = None
                yield indent + 'Proof.'
                yield after_proof_space + 'exact (' + proof_term + ').'
                yield ' Qed.' + post_space
            else:
                yield statement
        else:
            yield statement
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))

RANGE_REG = re.compile(r'Chars ([0-9]+) - ([0-9]+) [^\s]+', flags=re.DOTALL)

def get_coq_statement_byte_ranges(file_name, coqc, **kwargs):
    kwargs = fill_kwargs(kwargs)

# Path: strip_comments.py
# def strip_comments(contents):
#     """Strips the comments from coq code in contents.
# 
#     The strings in contents are only preserved if there are no
#     comment-like tokens inside of strings.  Stripping should be
#     successful and correct, regardless of whether or not there are
#     comment-like tokens in strings.
# 
#     The behavior of this method is undefined if there are any
#     notations which change the meaning of '(*', '*)', or '"'.
# 
#     Note that we take some extra care to leave *) untouched when it
#     does not terminate a comment.
#     """
#     contents = contents.replace('(*', ' (* ').replace('*)', ' *) ')
#     tokens = contents.split(' ')
#     rtn = []
#     is_string = False
#     comment_level = 0
#     for token in tokens:
#         do_append = (comment_level == 0)
#         if is_string:
#             if token.count('"') % 2 == 1: # there are an odd number of '"' characters, indicating that we've ended the string
#                 is_string = False
#         elif token.count('"') % 2 == 1: # there are an odd number of '"' characters, so we're starting a string
#             is_string = True
#         elif token == '(*':
#             comment_level += 1
#             do_append = False
#         elif comment_level > 0 and token == '*)':
#             comment_level -= 1
#         if do_append:
#             rtn.append(token)
#     return ' '.join(rtn).replace(' (* ', '(*').replace(' *) ', '*)').strip('\n\t ')
# 
# Path: custom_arguments.py
# DEFAULT_LOG = make_logger([(DEFAULT_VERBOSITY, sys.stderr)])
# 
# Path: coq_version.py
# def get_coq_accepts_time(coqc_prog, **kwargs):
#     return get_coq_accepts_option(coqc_prog, '-time', **kwargs)
# 
# Path: util.py
# PY3 = False


# Path: split_file.py
from strip_comments import strip_comments
from custom_arguments import DEFAULT_LOG
from coq_version import get_coq_accepts_time
from util import PY3
if PY3: from util import raw_input
import subprocess
import re
import util

    for statement_num, statement in enumerate(statements):
        match = PROOF_TERM_REG.match(statement)
        if match:
            indent, after_proof_space, proof_term, post_space = match.groups()
            if re.split(r'\s', proof_term)[0] not in ('using', 'with'): # Proof using ... and Proof with ... are special
                if on_first_example:
                    on_first_example(statement_num, statement, proof_term)
                    on_first_example = None
                yield indent + 'Proof.'
                yield after_proof_space + 'exact (' + proof_term + ').'
                yield ' Qed.' + post_space
            else:
                yield statement
        else:
            yield statement
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))

RANGE_REG = re.compile(r'Chars ([0-9]+) - ([0-9]+) [^\s]+', flags=re.DOTALL)

def get_coq_statement_byte_ranges(file_name, coqc, **kwargs):
    kwargs = fill_kwargs(kwargs)

    if not get_coq_accepts_time(coqc, **kwargs):