IMPORT_ABSOLUTIZE_TUPLE = ('lib', 'mod') ALL_ABSOLUTIZE_TUPLE = ('lib', 'proj', 'rec', 'ind', 'constr', 'def', 'syndef', 'class', 'thm', 'lem', 'prf', 'ax', 'inst', 'prfax', 'coind', 'scheme', 'vardef', 'mod')# , 'modtype') def add_libname_arguments(parser): add_libname_arguments_gen(parser, passing='') def update_env_with_libnames(env, args, default=(('.', 'Top'), ), include_passing=False, use_default=True, use_passing_default=True):
    all_keys = ('libnames', 'non_recursive_libnames', 'ocaml_dirnames', '_CoqProject', '_CoqProject_v_files', '_CoqProject_unknown')
    passing_opts = ('', ) if not include_passing else ('', 'passing_', 'nonpassing_')
    for passing in passing_opts:
        for key in all_keys:
            env[passing + key] = []
        if getattr(args, passing + 'CoqProjectFile'):
            for f in getattr(args, passing + 'CoqProjectFile'):
                env[passing + '_CoqProject'] = f.read()
                f.close()
        process_CoqProject(env, env[passing + '_CoqProject'], passing=passing)
        env[passing + 'libnames'].extend(getattr(args, passing + 'libnames'))
        env[passing + 'non_recursive_libnames'].extend(getattr(args, passing + 'non_recursive_libnames'))
        env[passing + 'ocaml_dirnames'].extend(getattr(args, passing + 'ocaml_dirnames'))
    if include_passing:
        # The nonpassing_ prefix is actually temporary; the semantics
        # are that, e.g., libnames = libnames + nonpassing_libnames,
        # while passing_libnames = libnames + passing_libnames
        for key in all_keys:
            env['passing_' + key] = env[key] + env['passing_' + key]
            env[key] = env[key] + env['nonpassing_' + key]
            del env['nonpassing_' + key]
    if use_default:
        update_env_with_libname_default(env, args, default=default)
    if use_passing_default and include_passing:
        update_env_with_libname_default(env, args, default=default, passing='passing_') def update_env_with_coqpath_folders(passing_prefix, env, *coqpaths):
    def do_with_path(path):
        env.get(passing_prefix + 'non_recursive_libnames', []).extend((os.path.join(path, d), d) for d in sorted(os.listdir(path)))
    for coqpath in coqpaths:
        if os.path.isdir(coqpath):
            do_with_path(coqpath)
        elif ';' in coqpath:
            for path in coqpath.split(';'):
                do_with_path(coqpath if coqpath != '' else '.')
        elif ':' in coqpath:
            for path in coqpath.split(':'):
                do_with_path(coqpath if coqpath != '' else '.') 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 def get_coqc_coqlib(coqc_prog, **kwargs):
    return [line[len('COQLIB='):] for line in get_coqc_config(coqc_prog, **kwargs).split('\n') if line.startswith('COQLIB=')][0] def include_imports(filename, as_modules=True, fast=False, log=DEFAULT_LOG, coqc='coqc', absolutize=ALL_ABSOLUTIZE_TUPLE, coq_makefile='coq_makefile', **kwargs):
    """Return the contents of filename, with any top-level imports inlined.

If as_modules == True, then the imports will be wrapped in modules.

This method requires access to the coqdep program if fast == False.
Without it, it will fall back to manual parsing of the imports,
which may change behavior.

>>> import tempfile, os
>>> f = tempfile.NamedTemporaryFile(dir='.', suffix='.v', delete=False)
>>> g = tempfile.NamedTemporaryFile(dir='.', suffix='.v', delete=False)
>>> g_name = os.path.relpath(g.name, '.')[:-2]
>>> f.write("  Require  Import %s Coq.Init.Logic Arith.\\n  Require  Export \tPArith\t Coq.Init.Logic.\\n  Require Bool.\\n Import Bool. (* asdf *)\\n Require Import QArith\\n  ZArith\\n  Setoid.\\nRequire Import %s.\\n Require\\n  Import\\n%s\\n\\n\t.\t(*foo*)\\n\\nInductive t := a | b.\\n\\n(*asdf*)" % (g_name, g_name, g_name))
>>> g.write(r"Require Export Ascii String.\\n\\nInductive q := c | d.")
>>> f.close()
>>> g.close()
>>> print(include_imports(f.name, as_modules=False))
Require Import Coq.Arith.Arith Coq.Bool.Bool Coq.Init.Logic Coq.PArith.PArith Coq.QArith.QArith Coq.Setoids.Setoid Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String.

Inductive q := c | d.
(* asdf *)


Inductive t := a | b.

(*asdf*)

>>> print(include_imports(f.name, as_modules=False, fast=True))
Require Import Arith Bool Coq.Init.Logic PArith QArith Setoid ZArith Ascii String.

Inductive q := c | d.
(* asdf *)


Inductive t := a | b.

(*asdf*)
>>> exts = ('.v', '.v.d', '.glob', '.vo', '.o', '.cmi', '.cmxs', '.native', '.cmx', '.vok', '.vos')
>>> names = [f.name[:-2] + ext for ext in exts] + [g.name[:-2] + ext for ext in exts]
>>> names = [i for i in names if os.path.exists(i)]
>>> for name in names: os.remove(name)
"""
    if 'make_coqc' in kwargs.keys():
        coqc = kwargs['make_coqc']
    if filename[-2:] != '.v': filename += '.v'
    lib = lib_of_filename(filename, **kwargs)
    all_imports = recursively_get_imports(lib, fast=fast, log=log, coqc=coqc, coq_makefile=coq_makefile, **kwargs)
    remaining_imports = []
    rtn = ''
    imports_done = []
    for import_name in all_imports:
        try:
            if as_modules:
                rtn += contents_as_module(import_name, imports_done, log=log, absolutize=absolutize, without_require=True, **kwargs) + '\n'
            else:
                rtn += contents_without_imports(import_name, log=log, absolutize=tuple(), **kwargs) + '\n'
            imports_done.append(import_name)
        except IOError:
            remaining_imports.append(import_name)
    if len(remaining_imports) > 0:
        log('remaining imports:', level=2)
        log(remaining_imports, level=2)
        if as_modules:
            pattern = 'Require %s.\n%s'
        else:
            pattern = 'Require Import %s.\n%s'
        for imp in reversed(remaining_imports):
            rtn = pattern % (imp, rtn)
    return rtn
import shutil, os, os.path, sys
from argparse_compat import argparse
from import_util import IMPORT_ABSOLUTIZE_TUPLE, ALL_ABSOLUTIZE_TUPLE
from custom_arguments import add_libname_arguments, update_env_with_libnames, update_env_with_coqpath_folders, add_logging_arguments, process_logging_arguments
from coq_version import get_coqc_coqlib
from replace_imports import include_imports
#!/usr/bin/env python

# {Windows,Python,coqtop} is terrible; we fail to write to (or read
# from?) coqtop.  But we can wrap it in a batch scrip, and it works
# fine.
SCRIPT_DIRECTORY = os.path.dirname(os.path.realpath(__file__))
DEFAULT_COQTOP = 'coqtop' if os.name != 'nt' else os.path.join(SCRIPT_DIRECTORY, 'coqtop.bat')

parser = argparse.ArgumentParser(description='Inline the imports of a file')
parser.add_argument('input_file', metavar='IN_FILE', type=argparse.FileType('r'),
                    help='a .v file to inline the imports of')
parser.add_argument('output_file', metavar='OUT_FILE', type=argparse.FileType('w'),
                    help='a .v file to write to')
parser.add_argument('--fast-merge-imports', dest='fast_merge_imports',
                    action='store_const', const=True, default=False,
                    help='Use a faster method for combining imports')
parser.add_argument('--no-deps', dest='walk_tree',
                    action='store_const', const=False, default=True,
                    help=("Don't do dependency analysis on all files in the current " +
                          "file tree."))
parser.add_argument('--no-wrap-modules', dest='wrap_modules',
                    action='store_const', const=False, default=True,
                    help=("Don't wrap imports in Modules.  By default, the " +
                          "contents of each file is wrapped in its own " +
                          "module to deal with renaming issues.  This " +
                          "can cause issues with subdirectories."))
parser.add_argument('--absolutize-constants', dest='absolutize',
                    action='store_const', default=IMPORT_ABSOLUTIZE_TUPLE, const=ALL_ABSOLUTIZE_TUPLE,
                    help=("Replace constants with fully qualified versions.  " +
                          "By default, all constants are not fully qualified.  If you have " +
                          "many overlapping file names in different directories " +
                          "and use partially qualified names that differ depending " +
                          "on which files have been Required, not absolutizing constants " +
                          "may cause name resolution to fail."))
parser.add_argument('--coqbin', metavar='COQBIN', dest='coqbin', type=str, default='',
                    help='The path to a folder containing the coqc and coqtop programs.')
parser.add_argument('--coqc', metavar='COQC', dest='coqc', type=str, default='coqc',
                    help='The path to the coqc program.')
parser.add_argument('--coqtop', metavar='COQTOP', dest='coqtop', type=str, default=DEFAULT_COQTOP,
                    help=('The path to the coqtop program (default: %s).' % DEFAULT_COQTOP))
parser.add_argument('--coqc-args', metavar='ARG', dest='coqc_args', type=str, nargs='?',
                    help='Arguments to pass to coqc; e.g., " -indices-matter" (leading and trailing spaces are stripped)')
parser.add_argument('--coqtop-args', metavar='ARG', dest='coqtop_args', type=str, nargs='?',
                    help='Arguments to pass to coqtop; e.g., " -indices-matter" (leading and trailing spaces are stripped)')
parser.add_argument('--coq_makefile', metavar='COQ_MAKEFILE', dest='coq_makefile', type=str, default='coq_makefile',
                    help='The path to the coq_makefile program.')
parser.add_argument('--inline-user-contrib', dest='inline_user_contrib',
                    action='store_const', const=True, default=False,
                    help=("Attempt to inline requires from the user-contrib folder"))
add_libname_arguments(parser)
add_logging_arguments(parser)

if __name__ == '__main__':
    args = process_logging_arguments(parser.parse_args())

    env = {
        'log': args.log,
        'coqc': (args.coqc if args.coqbin == '' else os.path.join(args.coqbin, args.coqc)),
        'absolutize': args.absolutize,
        'as_modules': args.wrap_modules,
        'fast': args.fast_merge_imports,
        'coq_makefile': args.coq_makefile,
        'walk_tree': args.walk_tree
        }

    update_env_with_libnames(env, args)