# 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
def minimize_lifted_statements(statements):
    statements = list(preminimize_lifted_statements(statements))
    sans_copy = [i for i in statements if COPY_UP_REG.match(i.strip()) is None]
    sans_copy_hint = [i for i in sans_copy if re.match(r'^(?:Local\s+|Global\s+)?Hint\s', i.strip()) is None]
    if len(sans_copy_hint) == 1:
        return sans_copy
    else:
        return statements

def move_from_proof(filename, **kwargs):
    kwargs['log']('Processing %s...' % filename)
    try:
        with open(filename, 'r') as f:
            contents = f.read()
    except IOError as e:
        kwargs['log']('Failed to process %s' % filename)
        kwargs['log'](repr(e), level=2)
        return
    ret = []
    cur_statements = []
    cur_statement = []
    deferred_copied_statements = []
    deferred_statements = []
    orig_space_count = 0
    cur_diff_space_count = 0
    if ''.join(split_coq_file_contents_with_comments(contents)) != contents:
        kwargs['log']('WARNING: Could not split %s' % filename, level=LOG_ALWAYS)
        return
    for i in split_coq_file_contents_with_comments(contents):
        is_definition_full = (ALL_DEFINITIONS_REG.match(i) is not None

# 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

def minimize_lifted_statements(statements):
    statements = list(preminimize_lifted_statements(statements))
    sans_copy = [i for i in statements if COPY_UP_REG.match(i.strip()) is None]
    sans_copy_hint = [i for i in sans_copy if re.match(r'^(?:Local\s+|Global\s+)?Hint\s', i.strip()) is None]
    if len(sans_copy_hint) == 1:
        return sans_copy
    else:
        return statements

def move_from_proof(filename, **kwargs):
    kwargs['log']('Processing %s...' % filename)
    try:
        with open(filename, 'r') as f:
            contents = f.read()
    except IOError as e:
        kwargs['log']('Failed to process %s' % filename)
        kwargs['log'](repr(e), level=2)
        return
    ret = []
    cur_statements = []
    cur_statement = []
    deferred_copied_statements = []
    deferred_statements = []
    orig_space_count = 0
    cur_diff_space_count = 0
    if ''.join(split_coq_file_contents_with_comments(contents)) != contents:
        kwargs['log']('WARNING: Could not split %s' % filename, level=LOG_ALWAYS)
        return
    for i in split_coq_file_contents_with_comments(contents):
        is_definition_full = (ALL_DEFINITIONS_REG.match(i) is not None

                              and (':=' in strip_parens(strip_comments(i))