# Path: argparse_compat.py

# 
# Path: split_file.py
# def split_coq_file_contents_with_comments(contents):
#     statements = re.split(r'(?<=[^\.]\.\.\.) |(?<=[^\.]\.) ',
#                           re.sub(r'((?<=[^\.]\.\.\.)\s|(?<=[^\.]\.)\s)', r' \1', contents))
#     #if contents != ''.join(statements):
#     #    print('Splitting failed (initial split)!')
#     #qstatements = list(merge_quotations(statements, sp=''))
#     #if contents != ''.join(qstatements):
#     #    print('Splitting failed (quote merge)!')
#     #cstatements = list(split_merge_comments(qstatements))
#     #if contents != ''.join(cstatements):
#     #    print('Splitting failed (comment merge)!')
#     return list(split_merge_comments(merge_quotations(statements, sp='')))
# 
# 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
# def add_logging_arguments(parser):
#     parser.add_argument('--verbose', '-v', dest='verbose',
#                         action='count',
#                         help='display some extra information by default (does not impact --verbose-log-file)')
#     parser.add_argument('--quiet', '-q', dest='quiet',
#                         action='count',
#                         help='the inverse of --verbose')
#     parser.add_argument('--log-file', '-l', dest='log_files', nargs='+', type=argparse.FileType('w'),
#                         default=[sys.stderr],
#                         help='The files to log output to.  Use - for stdout.')
#     parser.add_argument('--verbose-log-file', dest='verbose_log_files', nargs='+', type=TupleType(int, argparse.FileType('w')),
#                         default=[],
#                         help=(('The files to log output to at verbosity other than the default verbosity (%d if no -v/-q arguments are passed); ' +
#                                'each argument should be a pair of a verbosity level and a file name. '
#                                'Use - for stdout.') % DEFAULT_VERBOSITY))
# 
# def process_logging_arguments(args):
#     if args.verbose is None: args.verbose = DEFAULT_VERBOSITY
#     if args.quiet is None: args.quiet = 0
#     args.verbose -= args.quiet
#     args.log = make_logger([(args.verbose, f) for f in args.log_files]
#                            + args.verbose_log_files)
#     del args.quiet
#     del args.verbose
#     return args
# 
# LOG_ALWAYS=None
# 
# Path: file_util.py
# def write_to_file(file_name, contents, *args, **kwargs):
#     return write_bytes_to_file(file_name, contents.replace('\n', os.linesep).encode('utf-8'), *args, **kwargs)
# 
# Path: util.py
# PY3 = False


import os, sys, shutil, re
from argparse_compat import argparse
from split_file import split_coq_file_contents_with_comments
from strip_comments import strip_comments
from custom_arguments import add_logging_arguments, process_logging_arguments, LOG_ALWAYS
from file_util import write_to_file
from util import PY3
if PY3: from util import raw_input
                cur_statements = []
                deferred_copied_statements = []
        elif MOVE_UP_REG.match(i) or is_definition_full:
            kwargs['log']('Lifting: ' + repr(i), level=2)
            cur_statements.append(set_leading_space(i, orig_space_count))
        elif COPY_UP_REG.match(i) and cur_statement:
            kwargs['log']('Lift-copying: ' + repr(i), level=2)
            cur_statement.append(remove_leading_space(i, cur_diff_space_count))
            cur_statements.append(set_leading_space(i, orig_space_count))
            deferred_copied_statements.append(remove_leading_space(i, cur_diff_space_count))
        else:
            raw_input('WARNING: Unrecognized: %s' % repr(i))
        #print(cur_diff_space_count)
        #print(remove_leading_space(i, cur_diff_space_count))
    if cur_statements or deferred_statements or cur_statement:
        raw_input('WARNING: extra statements: %s' % repr((cur_statements, cur_statement, deferred_statements)))
        cur_statements.append(''.join(cur_statement))
        for i in deferred_statements:
            cur_statements.append(''.join(i))
        ret.extend(list(minimize_lifted_statements(cur_statements)))
    ret = ''.join(ret)
    if ret == contents:
        return
    if kwargs['inplace']:
        do_backup = kwargs['suffix'] is not None and len(kwargs['suffix']) > 0
        write_to_file(filename, ret, do_backup=do_backup, backup_ext=kwargs['suffix'])
    else:
        print(ret)

if __name__ == '__main__':

# Path: argparse_compat.py

# 
# Path: split_file.py
# def split_coq_file_contents_with_comments(contents):
#     statements = re.split(r'(?<=[^\.]\.\.\.) |(?<=[^\.]\.) ',
#                           re.sub(r'((?<=[^\.]\.\.\.)\s|(?<=[^\.]\.)\s)', r' \1', contents))
#     #if contents != ''.join(statements):
#     #    print('Splitting failed (initial split)!')
#     #qstatements = list(merge_quotations(statements, sp=''))
#     #if contents != ''.join(qstatements):
#     #    print('Splitting failed (quote merge)!')
#     #cstatements = list(split_merge_comments(qstatements))
#     #if contents != ''.join(cstatements):
#     #    print('Splitting failed (comment merge)!')
#     return list(split_merge_comments(merge_quotations(statements, sp='')))
# 
# 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
# def add_logging_arguments(parser):
#     parser.add_argument('--verbose', '-v', dest='verbose',
#                         action='count',
#                         help='display some extra information by default (does not impact --verbose-log-file)')
#     parser.add_argument('--quiet', '-q', dest='quiet',
#                         action='count',
#                         help='the inverse of --verbose')
#     parser.add_argument('--log-file', '-l', dest='log_files', nargs='+', type=argparse.FileType('w'),
#                         default=[sys.stderr],
#                         help='The files to log output to.  Use - for stdout.')
#     parser.add_argument('--verbose-log-file', dest='verbose_log_files', nargs='+', type=TupleType(int, argparse.FileType('w')),
#                         default=[],
#                         help=(('The files to log output to at verbosity other than the default verbosity (%d if no -v/-q arguments are passed); ' +
#                                'each argument should be a pair of a verbosity level and a file name. '
#                                'Use - for stdout.') % DEFAULT_VERBOSITY))
# 
# def process_logging_arguments(args):
#     if args.verbose is None: args.verbose = DEFAULT_VERBOSITY
#     if args.quiet is None: args.quiet = 0
#     args.verbose -= args.quiet
#     args.log = make_logger([(args.verbose, f) for f in args.log_files]
#                            + args.verbose_log_files)
#     del args.quiet
#     del args.verbose
#     return args
# 
# LOG_ALWAYS=None
# 
# Path: file_util.py
# def write_to_file(file_name, contents, *args, **kwargs):
#     return write_bytes_to_file(file_name, contents.replace('\n', os.linesep).encode('utf-8'), *args, **kwargs)
# 
# Path: util.py
# PY3 = False


# Path: move-vernaculars.py
import os, sys, shutil, re
from argparse_compat import argparse
from split_file import split_coq_file_contents_with_comments
from strip_comments import strip_comments
from custom_arguments import add_logging_arguments, process_logging_arguments, LOG_ALWAYS
from file_util import write_to_file
from util import PY3
if PY3: from util import raw_input

                cur_statements = []
                deferred_copied_statements = []
        elif MOVE_UP_REG.match(i) or is_definition_full:
            kwargs['log']('Lifting: ' + repr(i), level=2)
            cur_statements.append(set_leading_space(i, orig_space_count))
        elif COPY_UP_REG.match(i) and cur_statement:
            kwargs['log']('Lift-copying: ' + repr(i), level=2)
            cur_statement.append(remove_leading_space(i, cur_diff_space_count))
            cur_statements.append(set_leading_space(i, orig_space_count))
            deferred_copied_statements.append(remove_leading_space(i, cur_diff_space_count))
        else:
            raw_input('WARNING: Unrecognized: %s' % repr(i))
        #print(cur_diff_space_count)
        #print(remove_leading_space(i, cur_diff_space_count))
    if cur_statements or deferred_statements or cur_statement:
        raw_input('WARNING: extra statements: %s' % repr((cur_statements, cur_statement, deferred_statements)))
        cur_statements.append(''.join(cur_statement))
        for i in deferred_statements:
            cur_statements.append(''.join(i))
        ret.extend(list(minimize_lifted_statements(cur_statements)))
    ret = ''.join(ret)
    if ret == contents:
        return
    if kwargs['inplace']:
        do_backup = kwargs['suffix'] is not None and len(kwargs['suffix']) > 0
        write_to_file(filename, ret, do_backup=do_backup, backup_ext=kwargs['suffix'])
    else:
        print(ret)

if __name__ == '__main__':

    args = process_logging_arguments(parser.parse_args())