moved MaSh's Python code into Isabelle
authorblanchet
Mon Nov 26 12:04:32 2012 +0100 (2012-11-26)
changeset 5022090280d85cd03
parent 50219 f6b95f0bba78
child 50221 355aaa57ac39
moved MaSh's Python code into Isabelle
etc/components
src/HOL/Tools/Sledgehammer/MaSh/etc/settings
src/HOL/Tools/Sledgehammer/MaSh/src/argparse.py
src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py
src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py
src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py
src/HOL/Tools/Sledgehammer/MaSh/src/readData.py
src/HOL/Tools/Sledgehammer/MaSh/src/snow.py
src/HOL/Tools/Sledgehammer/MaSh/src/stats.py
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/etc/components	Mon Nov 26 11:46:19 2012 +0100
     1.2 +++ b/etc/components	Mon Nov 26 12:04:32 2012 +0100
     1.3 @@ -7,5 +7,6 @@
     1.4  src/HOL/Library/Sum_of_Squares
     1.5  src/HOL/Tools/ATP
     1.6  src/HOL/Tools/Predicate_Compile
     1.7 +src/HOL/Tools/Sledgehammer/MaSh
     1.8  src/HOL/Tools/SMT
     1.9  src/HOL/TPTP
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/etc/settings	Mon Nov 26 12:04:32 2012 +0100
     2.3 @@ -0,0 +1,3 @@
     2.4 +# -*- shell-script -*- :mode=shellscript:
     2.5 +
     2.6 +ISABELLE_SLEDGEHAMMER_MASH="$COMPONENT"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/argparse.py	Mon Nov 26 12:04:32 2012 +0100
     3.3 @@ -0,0 +1,2353 @@
     3.4 +# -*- coding: utf-8 -*-
     3.5 +
     3.6 +# Copyright © 2006-2009 Steven J. Bethard <steven.bethard@gmail.com>.
     3.7 +#
     3.8 +# Licensed under the Apache License, Version 2.0 (the "License"); you may not
     3.9 +# use this file except in compliance with the License. You may obtain a copy
    3.10 +# of the License at
    3.11 +#
    3.12 +#     http://www.apache.org/licenses/LICENSE-2.0
    3.13 +#
    3.14 +# Unless required by applicable law or agreed to in writing, software
    3.15 +# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
    3.16 +# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
    3.17 +# License for the specific language governing permissions and limitations
    3.18 +# under the License.
    3.19 +
    3.20 +"""Command-line parsing library
    3.21 +
    3.22 +This module is an optparse-inspired command-line parsing library that:
    3.23 +
    3.24 +    - handles both optional and positional arguments
    3.25 +    - produces highly informative usage messages
    3.26 +    - supports parsers that dispatch to sub-parsers
    3.27 +
    3.28 +The following is a simple usage example that sums integers from the
    3.29 +command-line and writes the result to a file::
    3.30 +
    3.31 +    parser = argparse.ArgumentParser(
    3.32 +        description='sum the integers at the command line')
    3.33 +    parser.add_argument(
    3.34 +        'integers', metavar='int', nargs='+', type=int,
    3.35 +        help='an integer to be summed')
    3.36 +    parser.add_argument(
    3.37 +        '--log', default=sys.stdout, type=argparse.FileType('w'),
    3.38 +        help='the file where the sum should be written')
    3.39 +    args = parser.parse_args()
    3.40 +    args.log.write('%s' % sum(args.integers))
    3.41 +    args.log.close()
    3.42 +
    3.43 +The module contains the following public classes:
    3.44 +
    3.45 +    - ArgumentParser -- The main entry point for command-line parsing. As the
    3.46 +        example above shows, the add_argument() method is used to populate
    3.47 +        the parser with actions for optional and positional arguments. Then
    3.48 +        the parse_args() method is invoked to convert the args at the
    3.49 +        command-line into an object with attributes.
    3.50 +
    3.51 +    - ArgumentError -- The exception raised by ArgumentParser objects when
    3.52 +        there are errors with the parser's actions. Errors raised while
    3.53 +        parsing the command-line are caught by ArgumentParser and emitted
    3.54 +        as command-line messages.
    3.55 +
    3.56 +    - FileType -- A factory for defining types of files to be created. As the
    3.57 +        example above shows, instances of FileType are typically passed as
    3.58 +        the type= argument of add_argument() calls.
    3.59 +
    3.60 +    - Action -- The base class for parser actions. Typically actions are
    3.61 +        selected by passing strings like 'store_true' or 'append_const' to
    3.62 +        the action= argument of add_argument(). However, for greater
    3.63 +        customization of ArgumentParser actions, subclasses of Action may
    3.64 +        be defined and passed as the action= argument.
    3.65 +
    3.66 +    - HelpFormatter, RawDescriptionHelpFormatter, RawTextHelpFormatter,
    3.67 +        ArgumentDefaultsHelpFormatter -- Formatter classes which
    3.68 +        may be passed as the formatter_class= argument to the
    3.69 +        ArgumentParser constructor. HelpFormatter is the default,
    3.70 +        RawDescriptionHelpFormatter and RawTextHelpFormatter tell the parser
    3.71 +        not to change the formatting for help text, and
    3.72 +        ArgumentDefaultsHelpFormatter adds information about argument defaults
    3.73 +        to the help.
    3.74 +
    3.75 +All other classes in this module are considered implementation details.
    3.76 +(Also note that HelpFormatter and RawDescriptionHelpFormatter are only
    3.77 +considered public as object names -- the API of the formatter objects is
    3.78 +still considered an implementation detail.)
    3.79 +"""
    3.80 +
    3.81 +__version__ = '1.1'
    3.82 +__all__ = [
    3.83 +    'ArgumentParser',
    3.84 +    'ArgumentError',
    3.85 +    'Namespace',
    3.86 +    'Action',
    3.87 +    'FileType',
    3.88 +    'HelpFormatter',
    3.89 +    'RawDescriptionHelpFormatter',
    3.90 +    'RawTextHelpFormatter',
    3.91 +    'ArgumentDefaultsHelpFormatter',
    3.92 +]
    3.93 +
    3.94 +
    3.95 +import copy as _copy
    3.96 +import os as _os
    3.97 +import re as _re
    3.98 +import sys as _sys
    3.99 +import textwrap as _textwrap
   3.100 +
   3.101 +from gettext import gettext as _
   3.102 +
   3.103 +try:
   3.104 +    _set = set
   3.105 +except NameError:
   3.106 +    from sets import Set as _set
   3.107 +
   3.108 +try:
   3.109 +    _basestring = basestring
   3.110 +except NameError:
   3.111 +    _basestring = str
   3.112 +
   3.113 +try:
   3.114 +    _sorted = sorted
   3.115 +except NameError:
   3.116 +
   3.117 +    def _sorted(iterable, reverse=False):
   3.118 +        result = list(iterable)
   3.119 +        result.sort()
   3.120 +        if reverse:
   3.121 +            result.reverse()
   3.122 +        return result
   3.123 +
   3.124 +
   3.125 +def _callable(obj):
   3.126 +    return hasattr(obj, '__call__') or hasattr(obj, '__bases__')
   3.127 +
   3.128 +# silence Python 2.6 buggy warnings about Exception.message
   3.129 +if _sys.version_info[:2] == (2, 6):
   3.130 +    import warnings
   3.131 +    warnings.filterwarnings(
   3.132 +        action='ignore',
   3.133 +        message='BaseException.message has been deprecated as of Python 2.6',
   3.134 +        category=DeprecationWarning,
   3.135 +        module='argparse')
   3.136 +
   3.137 +
   3.138 +SUPPRESS = '==SUPPRESS=='
   3.139 +
   3.140 +OPTIONAL = '?'
   3.141 +ZERO_OR_MORE = '*'
   3.142 +ONE_OR_MORE = '+'
   3.143 +PARSER = 'A...'
   3.144 +REMAINDER = '...'
   3.145 +
   3.146 +# =============================
   3.147 +# Utility functions and classes
   3.148 +# =============================
   3.149 +
   3.150 +class _AttributeHolder(object):
   3.151 +    """Abstract base class that provides __repr__.
   3.152 +
   3.153 +    The __repr__ method returns a string in the format::
   3.154 +        ClassName(attr=name, attr=name, ...)
   3.155 +    The attributes are determined either by a class-level attribute,
   3.156 +    '_kwarg_names', or by inspecting the instance __dict__.
   3.157 +    """
   3.158 +
   3.159 +    def __repr__(self):
   3.160 +        type_name = type(self).__name__
   3.161 +        arg_strings = []
   3.162 +        for arg in self._get_args():
   3.163 +            arg_strings.append(repr(arg))
   3.164 +        for name, value in self._get_kwargs():
   3.165 +            arg_strings.append('%s=%r' % (name, value))
   3.166 +        return '%s(%s)' % (type_name, ', '.join(arg_strings))
   3.167 +
   3.168 +    def _get_kwargs(self):
   3.169 +        return _sorted(self.__dict__.items())
   3.170 +
   3.171 +    def _get_args(self):
   3.172 +        return []
   3.173 +
   3.174 +
   3.175 +def _ensure_value(namespace, name, value):
   3.176 +    if getattr(namespace, name, None) is None:
   3.177 +        setattr(namespace, name, value)
   3.178 +    return getattr(namespace, name)
   3.179 +
   3.180 +
   3.181 +# ===============
   3.182 +# Formatting Help
   3.183 +# ===============
   3.184 +
   3.185 +class HelpFormatter(object):
   3.186 +    """Formatter for generating usage messages and argument help strings.
   3.187 +
   3.188 +    Only the name of this class is considered a public API. All the methods
   3.189 +    provided by the class are considered an implementation detail.
   3.190 +    """
   3.191 +
   3.192 +    def __init__(self,
   3.193 +                 prog,
   3.194 +                 indent_increment=2,
   3.195 +                 max_help_position=24,
   3.196 +                 width=None):
   3.197 +
   3.198 +        # default setting for width
   3.199 +        if width is None:
   3.200 +            try:
   3.201 +                width = int(_os.environ['COLUMNS'])
   3.202 +            except (KeyError, ValueError):
   3.203 +                width = 80
   3.204 +            width -= 2
   3.205 +
   3.206 +        self._prog = prog
   3.207 +        self._indent_increment = indent_increment
   3.208 +        self._max_help_position = max_help_position
   3.209 +        self._width = width
   3.210 +
   3.211 +        self._current_indent = 0
   3.212 +        self._level = 0
   3.213 +        self._action_max_length = 0
   3.214 +
   3.215 +        self._root_section = self._Section(self, None)
   3.216 +        self._current_section = self._root_section
   3.217 +
   3.218 +        self._whitespace_matcher = _re.compile(r'\s+')
   3.219 +        self._long_break_matcher = _re.compile(r'\n\n\n+')
   3.220 +
   3.221 +    # ===============================
   3.222 +    # Section and indentation methods
   3.223 +    # ===============================
   3.224 +    def _indent(self):
   3.225 +        self._current_indent += self._indent_increment
   3.226 +        self._level += 1
   3.227 +
   3.228 +    def _dedent(self):
   3.229 +        self._current_indent -= self._indent_increment
   3.230 +        assert self._current_indent >= 0, 'Indent decreased below 0.'
   3.231 +        self._level -= 1
   3.232 +
   3.233 +    class _Section(object):
   3.234 +
   3.235 +        def __init__(self, formatter, parent, heading=None):
   3.236 +            self.formatter = formatter
   3.237 +            self.parent = parent
   3.238 +            self.heading = heading
   3.239 +            self.items = []
   3.240 +
   3.241 +        def format_help(self):
   3.242 +            # format the indented section
   3.243 +            if self.parent is not None:
   3.244 +                self.formatter._indent()
   3.245 +            join = self.formatter._join_parts
   3.246 +            for func, args in self.items:
   3.247 +                func(*args)
   3.248 +            item_help = join([func(*args) for func, args in self.items])
   3.249 +            if self.parent is not None:
   3.250 +                self.formatter._dedent()
   3.251 +
   3.252 +            # return nothing if the section was empty
   3.253 +            if not item_help:
   3.254 +                return ''
   3.255 +
   3.256 +            # add the heading if the section was non-empty
   3.257 +            if self.heading is not SUPPRESS and self.heading is not None:
   3.258 +                current_indent = self.formatter._current_indent
   3.259 +                heading = '%*s%s:\n' % (current_indent, '', self.heading)
   3.260 +            else:
   3.261 +                heading = ''
   3.262 +
   3.263 +            # join the section-initial newline, the heading and the help
   3.264 +            return join(['\n', heading, item_help, '\n'])
   3.265 +
   3.266 +    def _add_item(self, func, args):
   3.267 +        self._current_section.items.append((func, args))
   3.268 +
   3.269 +    # ========================
   3.270 +    # Message building methods
   3.271 +    # ========================
   3.272 +    def start_section(self, heading):
   3.273 +        self._indent()
   3.274 +        section = self._Section(self, self._current_section, heading)
   3.275 +        self._add_item(section.format_help, [])
   3.276 +        self._current_section = section
   3.277 +
   3.278 +    def end_section(self):
   3.279 +        self._current_section = self._current_section.parent
   3.280 +        self._dedent()
   3.281 +
   3.282 +    def add_text(self, text):
   3.283 +        if text is not SUPPRESS and text is not None:
   3.284 +            self._add_item(self._format_text, [text])
   3.285 +
   3.286 +    def add_usage(self, usage, actions, groups, prefix=None):
   3.287 +        if usage is not SUPPRESS:
   3.288 +            args = usage, actions, groups, prefix
   3.289 +            self._add_item(self._format_usage, args)
   3.290 +
   3.291 +    def add_argument(self, action):
   3.292 +        if action.help is not SUPPRESS:
   3.293 +
   3.294 +            # find all invocations
   3.295 +            get_invocation = self._format_action_invocation
   3.296 +            invocations = [get_invocation(action)]
   3.297 +            for subaction in self._iter_indented_subactions(action):
   3.298 +                invocations.append(get_invocation(subaction))
   3.299 +
   3.300 +            # update the maximum item length
   3.301 +            invocation_length = max([len(s) for s in invocations])
   3.302 +            action_length = invocation_length + self._current_indent
   3.303 +            self._action_max_length = max(self._action_max_length,
   3.304 +                                          action_length)
   3.305 +
   3.306 +            # add the item to the list
   3.307 +            self._add_item(self._format_action, [action])
   3.308 +
   3.309 +    def add_arguments(self, actions):
   3.310 +        for action in actions:
   3.311 +            self.add_argument(action)
   3.312 +
   3.313 +    # =======================
   3.314 +    # Help-formatting methods
   3.315 +    # =======================
   3.316 +    def format_help(self):
   3.317 +        help = self._root_section.format_help()
   3.318 +        if help:
   3.319 +            help = self._long_break_matcher.sub('\n\n', help)
   3.320 +            help = help.strip('\n') + '\n'
   3.321 +        return help
   3.322 +
   3.323 +    def _join_parts(self, part_strings):
   3.324 +        return ''.join([part
   3.325 +                        for part in part_strings
   3.326 +                        if part and part is not SUPPRESS])
   3.327 +
   3.328 +    def _format_usage(self, usage, actions, groups, prefix):
   3.329 +        if prefix is None:
   3.330 +            prefix = _('usage: ')
   3.331 +
   3.332 +        # if usage is specified, use that
   3.333 +        if usage is not None:
   3.334 +            usage = usage % dict(prog=self._prog)
   3.335 +
   3.336 +        # if no optionals or positionals are available, usage is just prog
   3.337 +        elif usage is None and not actions:
   3.338 +            usage = '%(prog)s' % dict(prog=self._prog)
   3.339 +
   3.340 +        # if optionals and positionals are available, calculate usage
   3.341 +        elif usage is None:
   3.342 +            prog = '%(prog)s' % dict(prog=self._prog)
   3.343 +
   3.344 +            # split optionals from positionals
   3.345 +            optionals = []
   3.346 +            positionals = []
   3.347 +            for action in actions:
   3.348 +                if action.option_strings:
   3.349 +                    optionals.append(action)
   3.350 +                else:
   3.351 +                    positionals.append(action)
   3.352 +
   3.353 +            # build full usage string
   3.354 +            format = self._format_actions_usage
   3.355 +            action_usage = format(optionals + positionals, groups)
   3.356 +            usage = ' '.join([s for s in [prog, action_usage] if s])
   3.357 +
   3.358 +            # wrap the usage parts if it's too long
   3.359 +            text_width = self._width - self._current_indent
   3.360 +            if len(prefix) + len(usage) > text_width:
   3.361 +
   3.362 +                # break usage into wrappable parts
   3.363 +                part_regexp = r'\(.*?\)+|\[.*?\]+|\S+'
   3.364 +                opt_usage = format(optionals, groups)
   3.365 +                pos_usage = format(positionals, groups)
   3.366 +                opt_parts = _re.findall(part_regexp, opt_usage)
   3.367 +                pos_parts = _re.findall(part_regexp, pos_usage)
   3.368 +                assert ' '.join(opt_parts) == opt_usage
   3.369 +                assert ' '.join(pos_parts) == pos_usage
   3.370 +
   3.371 +                # helper for wrapping lines
   3.372 +                def get_lines(parts, indent, prefix=None):
   3.373 +                    lines = []
   3.374 +                    line = []
   3.375 +                    if prefix is not None:
   3.376 +                        line_len = len(prefix) - 1
   3.377 +                    else:
   3.378 +                        line_len = len(indent) - 1
   3.379 +                    for part in parts:
   3.380 +                        if line_len + 1 + len(part) > text_width:
   3.381 +                            lines.append(indent + ' '.join(line))
   3.382 +                            line = []
   3.383 +                            line_len = len(indent) - 1
   3.384 +                        line.append(part)
   3.385 +                        line_len += len(part) + 1
   3.386 +                    if line:
   3.387 +                        lines.append(indent + ' '.join(line))
   3.388 +                    if prefix is not None:
   3.389 +                        lines[0] = lines[0][len(indent):]
   3.390 +                    return lines
   3.391 +
   3.392 +                # if prog is short, follow it with optionals or positionals
   3.393 +                if len(prefix) + len(prog) <= 0.75 * text_width:
   3.394 +                    indent = ' ' * (len(prefix) + len(prog) + 1)
   3.395 +                    if opt_parts:
   3.396 +                        lines = get_lines([prog] + opt_parts, indent, prefix)
   3.397 +                        lines.extend(get_lines(pos_parts, indent))
   3.398 +                    elif pos_parts:
   3.399 +                        lines = get_lines([prog] + pos_parts, indent, prefix)
   3.400 +                    else:
   3.401 +                        lines = [prog]
   3.402 +
   3.403 +                # if prog is long, put it on its own line
   3.404 +                else:
   3.405 +                    indent = ' ' * len(prefix)
   3.406 +                    parts = opt_parts + pos_parts
   3.407 +                    lines = get_lines(parts, indent)
   3.408 +                    if len(lines) > 1:
   3.409 +                        lines = []
   3.410 +                        lines.extend(get_lines(opt_parts, indent))
   3.411 +                        lines.extend(get_lines(pos_parts, indent))
   3.412 +                    lines = [prog] + lines
   3.413 +
   3.414 +                # join lines into usage
   3.415 +                usage = '\n'.join(lines)
   3.416 +
   3.417 +        # prefix with 'usage:'
   3.418 +        return '%s%s\n\n' % (prefix, usage)
   3.419 +
   3.420 +    def _format_actions_usage(self, actions, groups):
   3.421 +        # find group indices and identify actions in groups
   3.422 +        group_actions = _set()
   3.423 +        inserts = {}
   3.424 +        for group in groups:
   3.425 +            try:
   3.426 +                start = actions.index(group._group_actions[0])
   3.427 +            except ValueError:
   3.428 +                continue
   3.429 +            else:
   3.430 +                end = start + len(group._group_actions)
   3.431 +                if actions[start:end] == group._group_actions:
   3.432 +                    for action in group._group_actions:
   3.433 +                        group_actions.add(action)
   3.434 +                    if not group.required:
   3.435 +                        inserts[start] = '['
   3.436 +                        inserts[end] = ']'
   3.437 +                    else:
   3.438 +                        inserts[start] = '('
   3.439 +                        inserts[end] = ')'
   3.440 +                    for i in range(start + 1, end):
   3.441 +                        inserts[i] = '|'
   3.442 +
   3.443 +        # collect all actions format strings
   3.444 +        parts = []
   3.445 +        for i, action in enumerate(actions):
   3.446 +
   3.447 +            # suppressed arguments are marked with None
   3.448 +            # remove | separators for suppressed arguments
   3.449 +            if action.help is SUPPRESS:
   3.450 +                parts.append(None)
   3.451 +                if inserts.get(i) == '|':
   3.452 +                    inserts.pop(i)
   3.453 +                elif inserts.get(i + 1) == '|':
   3.454 +                    inserts.pop(i + 1)
   3.455 +
   3.456 +            # produce all arg strings
   3.457 +            elif not action.option_strings:
   3.458 +                part = self._format_args(action, action.dest)
   3.459 +
   3.460 +                # if it's in a group, strip the outer []
   3.461 +                if action in group_actions:
   3.462 +                    if part[0] == '[' and part[-1] == ']':
   3.463 +                        part = part[1:-1]
   3.464 +
   3.465 +                # add the action string to the list
   3.466 +                parts.append(part)
   3.467 +
   3.468 +            # produce the first way to invoke the option in brackets
   3.469 +            else:
   3.470 +                option_string = action.option_strings[0]
   3.471 +
   3.472 +                # if the Optional doesn't take a value, format is:
   3.473 +                #    -s or --long
   3.474 +                if action.nargs == 0:
   3.475 +                    part = '%s' % option_string
   3.476 +
   3.477 +                # if the Optional takes a value, format is:
   3.478 +                #    -s ARGS or --long ARGS
   3.479 +                else:
   3.480 +                    default = action.dest.upper()
   3.481 +                    args_string = self._format_args(action, default)
   3.482 +                    part = '%s %s' % (option_string, args_string)
   3.483 +
   3.484 +                # make it look optional if it's not required or in a group
   3.485 +                if not action.required and action not in group_actions:
   3.486 +                    part = '[%s]' % part
   3.487 +
   3.488 +                # add the action string to the list
   3.489 +                parts.append(part)
   3.490 +
   3.491 +        # insert things at the necessary indices
   3.492 +        for i in _sorted(inserts, reverse=True):
   3.493 +            parts[i:i] = [inserts[i]]
   3.494 +
   3.495 +        # join all the action items with spaces
   3.496 +        text = ' '.join([item for item in parts if item is not None])
   3.497 +
   3.498 +        # clean up separators for mutually exclusive groups
   3.499 +        open = r'[\[(]'
   3.500 +        close = r'[\])]'
   3.501 +        text = _re.sub(r'(%s) ' % open, r'\1', text)
   3.502 +        text = _re.sub(r' (%s)' % close, r'\1', text)
   3.503 +        text = _re.sub(r'%s *%s' % (open, close), r'', text)
   3.504 +        text = _re.sub(r'\(([^|]*)\)', r'\1', text)
   3.505 +        text = text.strip()
   3.506 +
   3.507 +        # return the text
   3.508 +        return text
   3.509 +
   3.510 +    def _format_text(self, text):
   3.511 +        if '%(prog)' in text:
   3.512 +            text = text % dict(prog=self._prog)
   3.513 +        text_width = self._width - self._current_indent
   3.514 +        indent = ' ' * self._current_indent
   3.515 +        return self._fill_text(text, text_width, indent) + '\n\n'
   3.516 +
   3.517 +    def _format_action(self, action):
   3.518 +        # determine the required width and the entry label
   3.519 +        help_position = min(self._action_max_length + 2,
   3.520 +                            self._max_help_position)
   3.521 +        help_width = self._width - help_position
   3.522 +        action_width = help_position - self._current_indent - 2
   3.523 +        action_header = self._format_action_invocation(action)
   3.524 +
   3.525 +        # ho nelp; start on same line and add a final newline
   3.526 +        if not action.help:
   3.527 +            tup = self._current_indent, '', action_header
   3.528 +            action_header = '%*s%s\n' % tup
   3.529 +
   3.530 +        # short action name; start on the same line and pad two spaces
   3.531 +        elif len(action_header) <= action_width:
   3.532 +            tup = self._current_indent, '', action_width, action_header
   3.533 +            action_header = '%*s%-*s  ' % tup
   3.534 +            indent_first = 0
   3.535 +
   3.536 +        # long action name; start on the next line
   3.537 +        else:
   3.538 +            tup = self._current_indent, '', action_header
   3.539 +            action_header = '%*s%s\n' % tup
   3.540 +            indent_first = help_position
   3.541 +
   3.542 +        # collect the pieces of the action help
   3.543 +        parts = [action_header]
   3.544 +
   3.545 +        # if there was help for the action, add lines of help text
   3.546 +        if action.help:
   3.547 +            help_text = self._expand_help(action)
   3.548 +            help_lines = self._split_lines(help_text, help_width)
   3.549 +            parts.append('%*s%s\n' % (indent_first, '', help_lines[0]))
   3.550 +            for line in help_lines[1:]:
   3.551 +                parts.append('%*s%s\n' % (help_position, '', line))
   3.552 +
   3.553 +        # or add a newline if the description doesn't end with one
   3.554 +        elif not action_header.endswith('\n'):
   3.555 +            parts.append('\n')
   3.556 +
   3.557 +        # if there are any sub-actions, add their help as well
   3.558 +        for subaction in self._iter_indented_subactions(action):
   3.559 +            parts.append(self._format_action(subaction))
   3.560 +
   3.561 +        # return a single string
   3.562 +        return self._join_parts(parts)
   3.563 +
   3.564 +    def _format_action_invocation(self, action):
   3.565 +        if not action.option_strings:
   3.566 +            metavar, = self._metavar_formatter(action, action.dest)(1)
   3.567 +            return metavar
   3.568 +
   3.569 +        else:
   3.570 +            parts = []
   3.571 +
   3.572 +            # if the Optional doesn't take a value, format is:
   3.573 +            #    -s, --long
   3.574 +            if action.nargs == 0:
   3.575 +                parts.extend(action.option_strings)
   3.576 +
   3.577 +            # if the Optional takes a value, format is:
   3.578 +            #    -s ARGS, --long ARGS
   3.579 +            else:
   3.580 +                default = action.dest.upper()
   3.581 +                args_string = self._format_args(action, default)
   3.582 +                for option_string in action.option_strings:
   3.583 +                    parts.append('%s %s' % (option_string, args_string))
   3.584 +
   3.585 +            return ', '.join(parts)
   3.586 +
   3.587 +    def _metavar_formatter(self, action, default_metavar):
   3.588 +        if action.metavar is not None:
   3.589 +            result = action.metavar
   3.590 +        elif action.choices is not None:
   3.591 +            choice_strs = [str(choice) for choice in action.choices]
   3.592 +            result = '{%s}' % ','.join(choice_strs)
   3.593 +        else:
   3.594 +            result = default_metavar
   3.595 +
   3.596 +        def format(tuple_size):
   3.597 +            if isinstance(result, tuple):
   3.598 +                return result
   3.599 +            else:
   3.600 +                return (result, ) * tuple_size
   3.601 +        return format
   3.602 +
   3.603 +    def _format_args(self, action, default_metavar):
   3.604 +        get_metavar = self._metavar_formatter(action, default_metavar)
   3.605 +        if action.nargs is None:
   3.606 +            result = '%s' % get_metavar(1)
   3.607 +        elif action.nargs == OPTIONAL:
   3.608 +            result = '[%s]' % get_metavar(1)
   3.609 +        elif action.nargs == ZERO_OR_MORE:
   3.610 +            result = '[%s [%s ...]]' % get_metavar(2)
   3.611 +        elif action.nargs == ONE_OR_MORE:
   3.612 +            result = '%s [%s ...]' % get_metavar(2)
   3.613 +        elif action.nargs == REMAINDER:
   3.614 +            result = '...'
   3.615 +        elif action.nargs == PARSER:
   3.616 +            result = '%s ...' % get_metavar(1)
   3.617 +        else:
   3.618 +            formats = ['%s' for _ in range(action.nargs)]
   3.619 +            result = ' '.join(formats) % get_metavar(action.nargs)
   3.620 +        return result
   3.621 +
   3.622 +    def _expand_help(self, action):
   3.623 +        params = dict(vars(action), prog=self._prog)
   3.624 +        for name in list(params):
   3.625 +            if params[name] is SUPPRESS:
   3.626 +                del params[name]
   3.627 +        for name in list(params):
   3.628 +            if hasattr(params[name], '__name__'):
   3.629 +                params[name] = params[name].__name__
   3.630 +        if params.get('choices') is not None:
   3.631 +            choices_str = ', '.join([str(c) for c in params['choices']])
   3.632 +            params['choices'] = choices_str
   3.633 +        return self._get_help_string(action) % params
   3.634 +
   3.635 +    def _iter_indented_subactions(self, action):
   3.636 +        try:
   3.637 +            get_subactions = action._get_subactions
   3.638 +        except AttributeError:
   3.639 +            pass
   3.640 +        else:
   3.641 +            self._indent()
   3.642 +            for subaction in get_subactions():
   3.643 +                yield subaction
   3.644 +            self._dedent()
   3.645 +
   3.646 +    def _split_lines(self, text, width):
   3.647 +        text = self._whitespace_matcher.sub(' ', text).strip()
   3.648 +        return _textwrap.wrap(text, width)
   3.649 +
   3.650 +    def _fill_text(self, text, width, indent):
   3.651 +        text = self._whitespace_matcher.sub(' ', text).strip()
   3.652 +        return _textwrap.fill(text, width, initial_indent=indent,
   3.653 +                                           subsequent_indent=indent)
   3.654 +
   3.655 +    def _get_help_string(self, action):
   3.656 +        return action.help
   3.657 +
   3.658 +
   3.659 +class RawDescriptionHelpFormatter(HelpFormatter):
   3.660 +    """Help message formatter which retains any formatting in descriptions.
   3.661 +
   3.662 +    Only the name of this class is considered a public API. All the methods
   3.663 +    provided by the class are considered an implementation detail.
   3.664 +    """
   3.665 +
   3.666 +    def _fill_text(self, text, width, indent):
   3.667 +        return ''.join([indent + line for line in text.splitlines(True)])
   3.668 +
   3.669 +
   3.670 +class RawTextHelpFormatter(RawDescriptionHelpFormatter):
   3.671 +    """Help message formatter which retains formatting of all help text.
   3.672 +
   3.673 +    Only the name of this class is considered a public API. All the methods
   3.674 +    provided by the class are considered an implementation detail.
   3.675 +    """
   3.676 +
   3.677 +    def _split_lines(self, text, width):
   3.678 +        return text.splitlines()
   3.679 +
   3.680 +
   3.681 +class ArgumentDefaultsHelpFormatter(HelpFormatter):
   3.682 +    """Help message formatter which adds default values to argument help.
   3.683 +
   3.684 +    Only the name of this class is considered a public API. All the methods
   3.685 +    provided by the class are considered an implementation detail.
   3.686 +    """
   3.687 +
   3.688 +    def _get_help_string(self, action):
   3.689 +        help = action.help
   3.690 +        if '%(default)' not in action.help:
   3.691 +            if action.default is not SUPPRESS:
   3.692 +                defaulting_nargs = [OPTIONAL, ZERO_OR_MORE]
   3.693 +                if action.option_strings or action.nargs in defaulting_nargs:
   3.694 +                    help += ' (default: %(default)s)'
   3.695 +        return help
   3.696 +
   3.697 +
   3.698 +# =====================
   3.699 +# Options and Arguments
   3.700 +# =====================
   3.701 +
   3.702 +def _get_action_name(argument):
   3.703 +    if argument is None:
   3.704 +        return None
   3.705 +    elif argument.option_strings:
   3.706 +        return  '/'.join(argument.option_strings)
   3.707 +    elif argument.metavar not in (None, SUPPRESS):
   3.708 +        return argument.metavar
   3.709 +    elif argument.dest not in (None, SUPPRESS):
   3.710 +        return argument.dest
   3.711 +    else:
   3.712 +        return None
   3.713 +
   3.714 +
   3.715 +class ArgumentError(Exception):
   3.716 +    """An error from creating or using an argument (optional or positional).
   3.717 +
   3.718 +    The string value of this exception is the message, augmented with
   3.719 +    information about the argument that caused it.
   3.720 +    """
   3.721 +
   3.722 +    def __init__(self, argument, message):
   3.723 +        self.argument_name = _get_action_name(argument)
   3.724 +        self.message = message
   3.725 +
   3.726 +    def __str__(self):
   3.727 +        if self.argument_name is None:
   3.728 +            format = '%(message)s'
   3.729 +        else:
   3.730 +            format = 'argument %(argument_name)s: %(message)s'
   3.731 +        return format % dict(message=self.message,
   3.732 +                             argument_name=self.argument_name)
   3.733 +
   3.734 +
   3.735 +class ArgumentTypeError(Exception):
   3.736 +    """An error from trying to convert a command line string to a type."""
   3.737 +    pass
   3.738 +
   3.739 +
   3.740 +# ==============
   3.741 +# Action classes
   3.742 +# ==============
   3.743 +
   3.744 +class Action(_AttributeHolder):
   3.745 +    """Information about how to convert command line strings to Python objects.
   3.746 +
   3.747 +    Action objects are used by an ArgumentParser to represent the information
   3.748 +    needed to parse a single argument from one or more strings from the
   3.749 +    command line. The keyword arguments to the Action constructor are also
   3.750 +    all attributes of Action instances.
   3.751 +
   3.752 +    Keyword Arguments:
   3.753 +
   3.754 +        - option_strings -- A list of command-line option strings which
   3.755 +            should be associated with this action.
   3.756 +
   3.757 +        - dest -- The name of the attribute to hold the created object(s)
   3.758 +
   3.759 +        - nargs -- The number of command-line arguments that should be
   3.760 +            consumed. By default, one argument will be consumed and a single
   3.761 +            value will be produced.  Other values include:
   3.762 +                - N (an integer) consumes N arguments (and produces a list)
   3.763 +                - '?' consumes zero or one arguments
   3.764 +                - '*' consumes zero or more arguments (and produces a list)
   3.765 +                - '+' consumes one or more arguments (and produces a list)
   3.766 +            Note that the difference between the default and nargs=1 is that
   3.767 +            with the default, a single value will be produced, while with
   3.768 +            nargs=1, a list containing a single value will be produced.
   3.769 +
   3.770 +        - const -- The value to be produced if the option is specified and the
   3.771 +            option uses an action that takes no values.
   3.772 +
   3.773 +        - default -- The value to be produced if the option is not specified.
   3.774 +
   3.775 +        - type -- The type which the command-line arguments should be converted
   3.776 +            to, should be one of 'string', 'int', 'float', 'complex' or a
   3.777 +            callable object that accepts a single string argument. If None,
   3.778 +            'string' is assumed.
   3.779 +
   3.780 +        - choices -- A container of values that should be allowed. If not None,
   3.781 +            after a command-line argument has been converted to the appropriate
   3.782 +            type, an exception will be raised if it is not a member of this
   3.783 +            collection.
   3.784 +
   3.785 +        - required -- True if the action must always be specified at the
   3.786 +            command line. This is only meaningful for optional command-line
   3.787 +            arguments.
   3.788 +
   3.789 +        - help -- The help string describing the argument.
   3.790 +
   3.791 +        - metavar -- The name to be used for the option's argument with the
   3.792 +            help string. If None, the 'dest' value will be used as the name.
   3.793 +    """
   3.794 +
   3.795 +    def __init__(self,
   3.796 +                 option_strings,
   3.797 +                 dest,
   3.798 +                 nargs=None,
   3.799 +                 const=None,
   3.800 +                 default=None,
   3.801 +                 type=None,
   3.802 +                 choices=None,
   3.803 +                 required=False,
   3.804 +                 help=None,
   3.805 +                 metavar=None):
   3.806 +        self.option_strings = option_strings
   3.807 +        self.dest = dest
   3.808 +        self.nargs = nargs
   3.809 +        self.const = const
   3.810 +        self.default = default
   3.811 +        self.type = type
   3.812 +        self.choices = choices
   3.813 +        self.required = required
   3.814 +        self.help = help
   3.815 +        self.metavar = metavar
   3.816 +
   3.817 +    def _get_kwargs(self):
   3.818 +        names = [
   3.819 +            'option_strings',
   3.820 +            'dest',
   3.821 +            'nargs',
   3.822 +            'const',
   3.823 +            'default',
   3.824 +            'type',
   3.825 +            'choices',
   3.826 +            'help',
   3.827 +            'metavar',
   3.828 +        ]
   3.829 +        return [(name, getattr(self, name)) for name in names]
   3.830 +
   3.831 +    def __call__(self, parser, namespace, values, option_string=None):
   3.832 +        raise NotImplementedError(_('.__call__() not defined'))
   3.833 +
   3.834 +
   3.835 +class _StoreAction(Action):
   3.836 +
   3.837 +    def __init__(self,
   3.838 +                 option_strings,
   3.839 +                 dest,
   3.840 +                 nargs=None,
   3.841 +                 const=None,
   3.842 +                 default=None,
   3.843 +                 type=None,
   3.844 +                 choices=None,
   3.845 +                 required=False,
   3.846 +                 help=None,
   3.847 +                 metavar=None):
   3.848 +        if nargs == 0:
   3.849 +            raise ValueError('nargs for store actions must be > 0; if you '
   3.850 +                             'have nothing to store, actions such as store '
   3.851 +                             'true or store const may be more appropriate')
   3.852 +        if const is not None and nargs != OPTIONAL:
   3.853 +            raise ValueError('nargs must be %r to supply const' % OPTIONAL)
   3.854 +        super(_StoreAction, self).__init__(
   3.855 +            option_strings=option_strings,
   3.856 +            dest=dest,
   3.857 +            nargs=nargs,
   3.858 +            const=const,
   3.859 +            default=default,
   3.860 +            type=type,
   3.861 +            choices=choices,
   3.862 +            required=required,
   3.863 +            help=help,
   3.864 +            metavar=metavar)
   3.865 +
   3.866 +    def __call__(self, parser, namespace, values, option_string=None):
   3.867 +        setattr(namespace, self.dest, values)
   3.868 +
   3.869 +
   3.870 +class _StoreConstAction(Action):
   3.871 +
   3.872 +    def __init__(self,
   3.873 +                 option_strings,
   3.874 +                 dest,
   3.875 +                 const,
   3.876 +                 default=None,
   3.877 +                 required=False,
   3.878 +                 help=None,
   3.879 +                 metavar=None):
   3.880 +        super(_StoreConstAction, self).__init__(
   3.881 +            option_strings=option_strings,
   3.882 +            dest=dest,
   3.883 +            nargs=0,
   3.884 +            const=const,
   3.885 +            default=default,
   3.886 +            required=required,
   3.887 +            help=help)
   3.888 +
   3.889 +    def __call__(self, parser, namespace, values, option_string=None):
   3.890 +        setattr(namespace, self.dest, self.const)
   3.891 +
   3.892 +
   3.893 +class _StoreTrueAction(_StoreConstAction):
   3.894 +
   3.895 +    def __init__(self,
   3.896 +                 option_strings,
   3.897 +                 dest,
   3.898 +                 default=False,
   3.899 +                 required=False,
   3.900 +                 help=None):
   3.901 +        super(_StoreTrueAction, self).__init__(
   3.902 +            option_strings=option_strings,
   3.903 +            dest=dest,
   3.904 +            const=True,
   3.905 +            default=default,
   3.906 +            required=required,
   3.907 +            help=help)
   3.908 +
   3.909 +
   3.910 +class _StoreFalseAction(_StoreConstAction):
   3.911 +
   3.912 +    def __init__(self,
   3.913 +                 option_strings,
   3.914 +                 dest,
   3.915 +                 default=True,
   3.916 +                 required=False,
   3.917 +                 help=None):
   3.918 +        super(_StoreFalseAction, self).__init__(
   3.919 +            option_strings=option_strings,
   3.920 +            dest=dest,
   3.921 +            const=False,
   3.922 +            default=default,
   3.923 +            required=required,
   3.924 +            help=help)
   3.925 +
   3.926 +
   3.927 +class _AppendAction(Action):
   3.928 +
   3.929 +    def __init__(self,
   3.930 +                 option_strings,
   3.931 +                 dest,
   3.932 +                 nargs=None,
   3.933 +                 const=None,
   3.934 +                 default=None,
   3.935 +                 type=None,
   3.936 +                 choices=None,
   3.937 +                 required=False,
   3.938 +                 help=None,
   3.939 +                 metavar=None):
   3.940 +        if nargs == 0:
   3.941 +            raise ValueError('nargs for append actions must be > 0; if arg '
   3.942 +                             'strings are not supplying the value to append, '
   3.943 +                             'the append const action may be more appropriate')
   3.944 +        if const is not None and nargs != OPTIONAL:
   3.945 +            raise ValueError('nargs must be %r to supply const' % OPTIONAL)
   3.946 +        super(_AppendAction, self).__init__(
   3.947 +            option_strings=option_strings,
   3.948 +            dest=dest,
   3.949 +            nargs=nargs,
   3.950 +            const=const,
   3.951 +            default=default,
   3.952 +            type=type,
   3.953 +            choices=choices,
   3.954 +            required=required,
   3.955 +            help=help,
   3.956 +            metavar=metavar)
   3.957 +
   3.958 +    def __call__(self, parser, namespace, values, option_string=None):
   3.959 +        items = _copy.copy(_ensure_value(namespace, self.dest, []))
   3.960 +        items.append(values)
   3.961 +        setattr(namespace, self.dest, items)
   3.962 +
   3.963 +
   3.964 +class _AppendConstAction(Action):
   3.965 +
   3.966 +    def __init__(self,
   3.967 +                 option_strings,
   3.968 +                 dest,
   3.969 +                 const,
   3.970 +                 default=None,
   3.971 +                 required=False,
   3.972 +                 help=None,
   3.973 +                 metavar=None):
   3.974 +        super(_AppendConstAction, self).__init__(
   3.975 +            option_strings=option_strings,
   3.976 +            dest=dest,
   3.977 +            nargs=0,
   3.978 +            const=const,
   3.979 +            default=default,
   3.980 +            required=required,
   3.981 +            help=help,
   3.982 +            metavar=metavar)
   3.983 +
   3.984 +    def __call__(self, parser, namespace, values, option_string=None):
   3.985 +        items = _copy.copy(_ensure_value(namespace, self.dest, []))
   3.986 +        items.append(self.const)
   3.987 +        setattr(namespace, self.dest, items)
   3.988 +
   3.989 +
   3.990 +class _CountAction(Action):
   3.991 +
   3.992 +    def __init__(self,
   3.993 +                 option_strings,
   3.994 +                 dest,
   3.995 +                 default=None,
   3.996 +                 required=False,
   3.997 +                 help=None):
   3.998 +        super(_CountAction, self).__init__(
   3.999 +            option_strings=option_strings,
  3.1000 +            dest=dest,
  3.1001 +            nargs=0,
  3.1002 +            default=default,
  3.1003 +            required=required,
  3.1004 +            help=help)
  3.1005 +
  3.1006 +    def __call__(self, parser, namespace, values, option_string=None):
  3.1007 +        new_count = _ensure_value(namespace, self.dest, 0) + 1
  3.1008 +        setattr(namespace, self.dest, new_count)
  3.1009 +
  3.1010 +
  3.1011 +class _HelpAction(Action):
  3.1012 +
  3.1013 +    def __init__(self,
  3.1014 +                 option_strings,
  3.1015 +                 dest=SUPPRESS,
  3.1016 +                 default=SUPPRESS,
  3.1017 +                 help=None):
  3.1018 +        super(_HelpAction, self).__init__(
  3.1019 +            option_strings=option_strings,
  3.1020 +            dest=dest,
  3.1021 +            default=default,
  3.1022 +            nargs=0,
  3.1023 +            help=help)
  3.1024 +
  3.1025 +    def __call__(self, parser, namespace, values, option_string=None):
  3.1026 +        parser.print_help()
  3.1027 +        parser.exit()
  3.1028 +
  3.1029 +
  3.1030 +class _VersionAction(Action):
  3.1031 +
  3.1032 +    def __init__(self,
  3.1033 +                 option_strings,
  3.1034 +                 version=None,
  3.1035 +                 dest=SUPPRESS,
  3.1036 +                 default=SUPPRESS,
  3.1037 +                 help=None):
  3.1038 +        super(_VersionAction, self).__init__(
  3.1039 +            option_strings=option_strings,
  3.1040 +            dest=dest,
  3.1041 +            default=default,
  3.1042 +            nargs=0,
  3.1043 +            help=help)
  3.1044 +        self.version = version
  3.1045 +
  3.1046 +    def __call__(self, parser, namespace, values, option_string=None):
  3.1047 +        version = self.version
  3.1048 +        if version is None:
  3.1049 +            version = parser.version
  3.1050 +        formatter = parser._get_formatter()
  3.1051 +        formatter.add_text(version)
  3.1052 +        parser.exit(message=formatter.format_help())
  3.1053 +
  3.1054 +
  3.1055 +class _SubParsersAction(Action):
  3.1056 +
  3.1057 +    class _ChoicesPseudoAction(Action):
  3.1058 +
  3.1059 +        def __init__(self, name, help):
  3.1060 +            sup = super(_SubParsersAction._ChoicesPseudoAction, self)
  3.1061 +            sup.__init__(option_strings=[], dest=name, help=help)
  3.1062 +
  3.1063 +    def __init__(self,
  3.1064 +                 option_strings,
  3.1065 +                 prog,
  3.1066 +                 parser_class,
  3.1067 +                 dest=SUPPRESS,
  3.1068 +                 help=None,
  3.1069 +                 metavar=None):
  3.1070 +
  3.1071 +        self._prog_prefix = prog
  3.1072 +        self._parser_class = parser_class
  3.1073 +        self._name_parser_map = {}
  3.1074 +        self._choices_actions = []
  3.1075 +
  3.1076 +        super(_SubParsersAction, self).__init__(
  3.1077 +            option_strings=option_strings,
  3.1078 +            dest=dest,
  3.1079 +            nargs=PARSER,
  3.1080 +            choices=self._name_parser_map,
  3.1081 +            help=help,
  3.1082 +            metavar=metavar)
  3.1083 +
  3.1084 +    def add_parser(self, name, **kwargs):
  3.1085 +        # set prog from the existing prefix
  3.1086 +        if kwargs.get('prog') is None:
  3.1087 +            kwargs['prog'] = '%s %s' % (self._prog_prefix, name)
  3.1088 +
  3.1089 +        # create a pseudo-action to hold the choice help
  3.1090 +        if 'help' in kwargs:
  3.1091 +            help = kwargs.pop('help')
  3.1092 +            choice_action = self._ChoicesPseudoAction(name, help)
  3.1093 +            self._choices_actions.append(choice_action)
  3.1094 +
  3.1095 +        # create the parser and add it to the map
  3.1096 +        parser = self._parser_class(**kwargs)
  3.1097 +        self._name_parser_map[name] = parser
  3.1098 +        return parser
  3.1099 +
  3.1100 +    def _get_subactions(self):
  3.1101 +        return self._choices_actions
  3.1102 +
  3.1103 +    def __call__(self, parser, namespace, values, option_string=None):
  3.1104 +        parser_name = values[0]
  3.1105 +        arg_strings = values[1:]
  3.1106 +
  3.1107 +        # set the parser name if requested
  3.1108 +        if self.dest is not SUPPRESS:
  3.1109 +            setattr(namespace, self.dest, parser_name)
  3.1110 +
  3.1111 +        # select the parser
  3.1112 +        try:
  3.1113 +            parser = self._name_parser_map[parser_name]
  3.1114 +        except KeyError:
  3.1115 +            tup = parser_name, ', '.join(self._name_parser_map)
  3.1116 +            msg = _('unknown parser %r (choices: %s)' % tup)
  3.1117 +            raise ArgumentError(self, msg)
  3.1118 +
  3.1119 +        # parse all the remaining options into the namespace
  3.1120 +        parser.parse_args(arg_strings, namespace)
  3.1121 +
  3.1122 +
  3.1123 +# ==============
  3.1124 +# Type classes
  3.1125 +# ==============
  3.1126 +
  3.1127 +class FileType(object):
  3.1128 +    """Factory for creating file object types
  3.1129 +
  3.1130 +    Instances of FileType are typically passed as type= arguments to the
  3.1131 +    ArgumentParser add_argument() method.
  3.1132 +
  3.1133 +    Keyword Arguments:
  3.1134 +        - mode -- A string indicating how the file is to be opened. Accepts the
  3.1135 +            same values as the builtin open() function.
  3.1136 +        - bufsize -- The file's desired buffer size. Accepts the same values as
  3.1137 +            the builtin open() function.
  3.1138 +    """
  3.1139 +
  3.1140 +    def __init__(self, mode='r', bufsize=None):
  3.1141 +        self._mode = mode
  3.1142 +        self._bufsize = bufsize
  3.1143 +
  3.1144 +    def __call__(self, string):
  3.1145 +        # the special argument "-" means sys.std{in,out}
  3.1146 +        if string == '-':
  3.1147 +            if 'r' in self._mode:
  3.1148 +                return _sys.stdin
  3.1149 +            elif 'w' in self._mode:
  3.1150 +                return _sys.stdout
  3.1151 +            else:
  3.1152 +                msg = _('argument "-" with mode %r' % self._mode)
  3.1153 +                raise ValueError(msg)
  3.1154 +
  3.1155 +        # all other arguments are used as file names
  3.1156 +        if self._bufsize:
  3.1157 +            return open(string, self._mode, self._bufsize)
  3.1158 +        else:
  3.1159 +            return open(string, self._mode)
  3.1160 +
  3.1161 +    def __repr__(self):
  3.1162 +        args = [self._mode, self._bufsize]
  3.1163 +        args_str = ', '.join([repr(arg) for arg in args if arg is not None])
  3.1164 +        return '%s(%s)' % (type(self).__name__, args_str)
  3.1165 +
  3.1166 +# ===========================
  3.1167 +# Optional and Positional Parsing
  3.1168 +# ===========================
  3.1169 +
  3.1170 +class Namespace(_AttributeHolder):
  3.1171 +    """Simple object for storing attributes.
  3.1172 +
  3.1173 +    Implements equality by attribute names and values, and provides a simple
  3.1174 +    string representation.
  3.1175 +    """
  3.1176 +
  3.1177 +    def __init__(self, **kwargs):
  3.1178 +        for name in kwargs:
  3.1179 +            setattr(self, name, kwargs[name])
  3.1180 +
  3.1181 +    def __eq__(self, other):
  3.1182 +        return vars(self) == vars(other)
  3.1183 +
  3.1184 +    def __ne__(self, other):
  3.1185 +        return not (self == other)
  3.1186 +
  3.1187 +    def __contains__(self, key):
  3.1188 +        return key in self.__dict__
  3.1189 +
  3.1190 +
  3.1191 +class _ActionsContainer(object):
  3.1192 +
  3.1193 +    def __init__(self,
  3.1194 +                 description,
  3.1195 +                 prefix_chars,
  3.1196 +                 argument_default,
  3.1197 +                 conflict_handler):
  3.1198 +        super(_ActionsContainer, self).__init__()
  3.1199 +
  3.1200 +        self.description = description
  3.1201 +        self.argument_default = argument_default
  3.1202 +        self.prefix_chars = prefix_chars
  3.1203 +        self.conflict_handler = conflict_handler
  3.1204 +
  3.1205 +        # set up registries
  3.1206 +        self._registries = {}
  3.1207 +
  3.1208 +        # register actions
  3.1209 +        self.register('action', None, _StoreAction)
  3.1210 +        self.register('action', 'store', _StoreAction)
  3.1211 +        self.register('action', 'store_const', _StoreConstAction)
  3.1212 +        self.register('action', 'store_true', _StoreTrueAction)
  3.1213 +        self.register('action', 'store_false', _StoreFalseAction)
  3.1214 +        self.register('action', 'append', _AppendAction)
  3.1215 +        self.register('action', 'append_const', _AppendConstAction)
  3.1216 +        self.register('action', 'count', _CountAction)
  3.1217 +        self.register('action', 'help', _HelpAction)
  3.1218 +        self.register('action', 'version', _VersionAction)
  3.1219 +        self.register('action', 'parsers', _SubParsersAction)
  3.1220 +
  3.1221 +        # raise an exception if the conflict handler is invalid
  3.1222 +        self._get_handler()
  3.1223 +
  3.1224 +        # action storage
  3.1225 +        self._actions = []
  3.1226 +        self._option_string_actions = {}
  3.1227 +
  3.1228 +        # groups
  3.1229 +        self._action_groups = []
  3.1230 +        self._mutually_exclusive_groups = []
  3.1231 +
  3.1232 +        # defaults storage
  3.1233 +        self._defaults = {}
  3.1234 +
  3.1235 +        # determines whether an "option" looks like a negative number
  3.1236 +        self._negative_number_matcher = _re.compile(r'^-\d+$|^-\d*\.\d+$')
  3.1237 +
  3.1238 +        # whether or not there are any optionals that look like negative
  3.1239 +        # numbers -- uses a list so it can be shared and edited
  3.1240 +        self._has_negative_number_optionals = []
  3.1241 +
  3.1242 +    # ====================
  3.1243 +    # Registration methods
  3.1244 +    # ====================
  3.1245 +    def register(self, registry_name, value, object):
  3.1246 +        registry = self._registries.setdefault(registry_name, {})
  3.1247 +        registry[value] = object
  3.1248 +
  3.1249 +    def _registry_get(self, registry_name, value, default=None):
  3.1250 +        return self._registries[registry_name].get(value, default)
  3.1251 +
  3.1252 +    # ==================================
  3.1253 +    # Namespace default accessor methods
  3.1254 +    # ==================================
  3.1255 +    def set_defaults(self, **kwargs):
  3.1256 +        self._defaults.update(kwargs)
  3.1257 +
  3.1258 +        # if these defaults match any existing arguments, replace
  3.1259 +        # the previous default on the object with the new one
  3.1260 +        for action in self._actions:
  3.1261 +            if action.dest in kwargs:
  3.1262 +                action.default = kwargs[action.dest]
  3.1263 +
  3.1264 +    def get_default(self, dest):
  3.1265 +        for action in self._actions:
  3.1266 +            if action.dest == dest and action.default is not None:
  3.1267 +                return action.default
  3.1268 +        return self._defaults.get(dest, None)
  3.1269 +
  3.1270 +
  3.1271 +    # =======================
  3.1272 +    # Adding argument actions
  3.1273 +    # =======================
  3.1274 +    def add_argument(self, *args, **kwargs):
  3.1275 +        """
  3.1276 +        add_argument(dest, ..., name=value, ...)
  3.1277 +        add_argument(option_string, option_string, ..., name=value, ...)
  3.1278 +        """
  3.1279 +
  3.1280 +        # if no positional args are supplied or only one is supplied and
  3.1281 +        # it doesn't look like an option string, parse a positional
  3.1282 +        # argument
  3.1283 +        chars = self.prefix_chars
  3.1284 +        if not args or len(args) == 1 and args[0][0] not in chars:
  3.1285 +            if args and 'dest' in kwargs:
  3.1286 +                raise ValueError('dest supplied twice for positional argument')
  3.1287 +            kwargs = self._get_positional_kwargs(*args, **kwargs)
  3.1288 +
  3.1289 +        # otherwise, we're adding an optional argument
  3.1290 +        else:
  3.1291 +            kwargs = self._get_optional_kwargs(*args, **kwargs)
  3.1292 +
  3.1293 +        # if no default was supplied, use the parser-level default
  3.1294 +        if 'default' not in kwargs:
  3.1295 +            dest = kwargs['dest']
  3.1296 +            if dest in self._defaults:
  3.1297 +                kwargs['default'] = self._defaults[dest]
  3.1298 +            elif self.argument_default is not None:
  3.1299 +                kwargs['default'] = self.argument_default
  3.1300 +
  3.1301 +        # create the action object, and add it to the parser
  3.1302 +        action_class = self._pop_action_class(kwargs)
  3.1303 +        if not _callable(action_class):
  3.1304 +            raise ValueError('unknown action "%s"' % action_class)
  3.1305 +        action = action_class(**kwargs)
  3.1306 +
  3.1307 +        # raise an error if the action type is not callable
  3.1308 +        type_func = self._registry_get('type', action.type, action.type)
  3.1309 +        if not _callable(type_func):
  3.1310 +            raise ValueError('%r is not callable' % type_func)
  3.1311 +
  3.1312 +        return self._add_action(action)
  3.1313 +
  3.1314 +    def add_argument_group(self, *args, **kwargs):
  3.1315 +        group = _ArgumentGroup(self, *args, **kwargs)
  3.1316 +        self._action_groups.append(group)
  3.1317 +        return group
  3.1318 +
  3.1319 +    def add_mutually_exclusive_group(self, **kwargs):
  3.1320 +        group = _MutuallyExclusiveGroup(self, **kwargs)
  3.1321 +        self._mutually_exclusive_groups.append(group)
  3.1322 +        return group
  3.1323 +
  3.1324 +    def _add_action(self, action):
  3.1325 +        # resolve any conflicts
  3.1326 +        self._check_conflict(action)
  3.1327 +
  3.1328 +        # add to actions list
  3.1329 +        self._actions.append(action)
  3.1330 +        action.container = self
  3.1331 +
  3.1332 +        # index the action by any option strings it has
  3.1333 +        for option_string in action.option_strings:
  3.1334 +            self._option_string_actions[option_string] = action
  3.1335 +
  3.1336 +        # set the flag if any option strings look like negative numbers
  3.1337 +        for option_string in action.option_strings:
  3.1338 +            if self._negative_number_matcher.match(option_string):
  3.1339 +                if not self._has_negative_number_optionals:
  3.1340 +                    self._has_negative_number_optionals.append(True)
  3.1341 +
  3.1342 +        # return the created action
  3.1343 +        return action
  3.1344 +
  3.1345 +    def _remove_action(self, action):
  3.1346 +        self._actions.remove(action)
  3.1347 +
  3.1348 +    def _add_container_actions(self, container):
  3.1349 +        # collect groups by titles
  3.1350 +        title_group_map = {}
  3.1351 +        for group in self._action_groups:
  3.1352 +            if group.title in title_group_map:
  3.1353 +                msg = _('cannot merge actions - two groups are named %r')
  3.1354 +                raise ValueError(msg % (group.title))
  3.1355 +            title_group_map[group.title] = group
  3.1356 +
  3.1357 +        # map each action to its group
  3.1358 +        group_map = {}
  3.1359 +        for group in container._action_groups:
  3.1360 +
  3.1361 +            # if a group with the title exists, use that, otherwise
  3.1362 +            # create a new group matching the container's group
  3.1363 +            if group.title not in title_group_map:
  3.1364 +                title_group_map[group.title] = self.add_argument_group(
  3.1365 +                    title=group.title,
  3.1366 +                    description=group.description,
  3.1367 +                    conflict_handler=group.conflict_handler)
  3.1368 +
  3.1369 +            # map the actions to their new group
  3.1370 +            for action in group._group_actions:
  3.1371 +                group_map[action] = title_group_map[group.title]
  3.1372 +
  3.1373 +        # add container's mutually exclusive groups
  3.1374 +        # NOTE: if add_mutually_exclusive_group ever gains title= and
  3.1375 +        # description= then this code will need to be expanded as above
  3.1376 +        for group in container._mutually_exclusive_groups:
  3.1377 +            mutex_group = self.add_mutually_exclusive_group(
  3.1378 +                required=group.required)
  3.1379 +
  3.1380 +            # map the actions to their new mutex group
  3.1381 +            for action in group._group_actions:
  3.1382 +                group_map[action] = mutex_group
  3.1383 +
  3.1384 +        # add all actions to this container or their group
  3.1385 +        for action in container._actions:
  3.1386 +            group_map.get(action, self)._add_action(action)
  3.1387 +
  3.1388 +    def _get_positional_kwargs(self, dest, **kwargs):
  3.1389 +        # make sure required is not specified
  3.1390 +        if 'required' in kwargs:
  3.1391 +            msg = _("'required' is an invalid argument for positionals")
  3.1392 +            raise TypeError(msg)
  3.1393 +
  3.1394 +        # mark positional arguments as required if at least one is
  3.1395 +        # always required
  3.1396 +        if kwargs.get('nargs') not in [OPTIONAL, ZERO_OR_MORE]:
  3.1397 +            kwargs['required'] = True
  3.1398 +        if kwargs.get('nargs') == ZERO_OR_MORE and 'default' not in kwargs:
  3.1399 +            kwargs['required'] = True
  3.1400 +
  3.1401 +        # return the keyword arguments with no option strings
  3.1402 +        return dict(kwargs, dest=dest, option_strings=[])
  3.1403 +
  3.1404 +    def _get_optional_kwargs(self, *args, **kwargs):
  3.1405 +        # determine short and long option strings
  3.1406 +        option_strings = []
  3.1407 +        long_option_strings = []
  3.1408 +        for option_string in args:
  3.1409 +            # error on strings that don't start with an appropriate prefix
  3.1410 +            if not option_string[0] in self.prefix_chars:
  3.1411 +                msg = _('invalid option string %r: '
  3.1412 +                        'must start with a character %r')
  3.1413 +                tup = option_string, self.prefix_chars
  3.1414 +                raise ValueError(msg % tup)
  3.1415 +
  3.1416 +            # strings starting with two prefix characters are long options
  3.1417 +            option_strings.append(option_string)
  3.1418 +            if option_string[0] in self.prefix_chars:
  3.1419 +                if len(option_string) > 1:
  3.1420 +                    if option_string[1] in self.prefix_chars:
  3.1421 +                        long_option_strings.append(option_string)
  3.1422 +
  3.1423 +        # infer destination, '--foo-bar' -> 'foo_bar' and '-x' -> 'x'
  3.1424 +        dest = kwargs.pop('dest', None)
  3.1425 +        if dest is None:
  3.1426 +            if long_option_strings:
  3.1427 +                dest_option_string = long_option_strings[0]
  3.1428 +            else:
  3.1429 +                dest_option_string = option_strings[0]
  3.1430 +            dest = dest_option_string.lstrip(self.prefix_chars)
  3.1431 +            if not dest:
  3.1432 +                msg = _('dest= is required for options like %r')
  3.1433 +                raise ValueError(msg % option_string)
  3.1434 +            dest = dest.replace('-', '_')
  3.1435 +
  3.1436 +        # return the updated keyword arguments
  3.1437 +        return dict(kwargs, dest=dest, option_strings=option_strings)
  3.1438 +
  3.1439 +    def _pop_action_class(self, kwargs, default=None):
  3.1440 +        action = kwargs.pop('action', default)
  3.1441 +        return self._registry_get('action', action, action)
  3.1442 +
  3.1443 +    def _get_handler(self):
  3.1444 +        # determine function from conflict handler string
  3.1445 +        handler_func_name = '_handle_conflict_%s' % self.conflict_handler
  3.1446 +        try:
  3.1447 +            return getattr(self, handler_func_name)
  3.1448 +        except AttributeError:
  3.1449 +            msg = _('invalid conflict_resolution value: %r')
  3.1450 +            raise ValueError(msg % self.conflict_handler)
  3.1451 +
  3.1452 +    def _check_conflict(self, action):
  3.1453 +
  3.1454 +        # find all options that conflict with this option
  3.1455 +        confl_optionals = []
  3.1456 +        for option_string in action.option_strings:
  3.1457 +            if option_string in self._option_string_actions:
  3.1458 +                confl_optional = self._option_string_actions[option_string]
  3.1459 +                confl_optionals.append((option_string, confl_optional))
  3.1460 +
  3.1461 +        # resolve any conflicts
  3.1462 +        if confl_optionals:
  3.1463 +            conflict_handler = self._get_handler()
  3.1464 +            conflict_handler(action, confl_optionals)
  3.1465 +
  3.1466 +    def _handle_conflict_error(self, action, conflicting_actions):
  3.1467 +        message = _('conflicting option string(s): %s')
  3.1468 +        conflict_string = ', '.join([option_string
  3.1469 +                                     for option_string, action
  3.1470 +                                     in conflicting_actions])
  3.1471 +        raise ArgumentError(action, message % conflict_string)
  3.1472 +
  3.1473 +    def _handle_conflict_resolve(self, action, conflicting_actions):
  3.1474 +
  3.1475 +        # remove all conflicting options
  3.1476 +        for option_string, action in conflicting_actions:
  3.1477 +
  3.1478 +            # remove the conflicting option
  3.1479 +            action.option_strings.remove(option_string)
  3.1480 +            self._option_string_actions.pop(option_string, None)
  3.1481 +
  3.1482 +            # if the option now has no option string, remove it from the
  3.1483 +            # container holding it
  3.1484 +            if not action.option_strings:
  3.1485 +                action.container._remove_action(action)
  3.1486 +
  3.1487 +
  3.1488 +class _ArgumentGroup(_ActionsContainer):
  3.1489 +
  3.1490 +    def __init__(self, container, title=None, description=None, **kwargs):
  3.1491 +        # add any missing keyword arguments by checking the container
  3.1492 +        update = kwargs.setdefault
  3.1493 +        update('conflict_handler', container.conflict_handler)
  3.1494 +        update('prefix_chars', container.prefix_chars)
  3.1495 +        update('argument_default', container.argument_default)
  3.1496 +        super_init = super(_ArgumentGroup, self).__init__
  3.1497 +        super_init(description=description, **kwargs)
  3.1498 +
  3.1499 +        # group attributes
  3.1500 +        self.title = title
  3.1501 +        self._group_actions = []
  3.1502 +
  3.1503 +        # share most attributes with the container
  3.1504 +        self._registries = container._registries
  3.1505 +        self._actions = container._actions
  3.1506 +        self._option_string_actions = container._option_string_actions
  3.1507 +        self._defaults = container._defaults
  3.1508 +        self._has_negative_number_optionals = \
  3.1509 +            container._has_negative_number_optionals
  3.1510 +
  3.1511 +    def _add_action(self, action):
  3.1512 +        action = super(_ArgumentGroup, self)._add_action(action)
  3.1513 +        self._group_actions.append(action)
  3.1514 +        return action
  3.1515 +
  3.1516 +    def _remove_action(self, action):
  3.1517 +        super(_ArgumentGroup, self)._remove_action(action)
  3.1518 +        self._group_actions.remove(action)
  3.1519 +
  3.1520 +
  3.1521 +class _MutuallyExclusiveGroup(_ArgumentGroup):
  3.1522 +
  3.1523 +    def __init__(self, container, required=False):
  3.1524 +        super(_MutuallyExclusiveGroup, self).__init__(container)
  3.1525 +        self.required = required
  3.1526 +        self._container = container
  3.1527 +
  3.1528 +    def _add_action(self, action):
  3.1529 +        if action.required:
  3.1530 +            msg = _('mutually exclusive arguments must be optional')
  3.1531 +            raise ValueError(msg)
  3.1532 +        action = self._container._add_action(action)
  3.1533 +        self._group_actions.append(action)
  3.1534 +        return action
  3.1535 +
  3.1536 +    def _remove_action(self, action):
  3.1537 +        self._container._remove_action(action)
  3.1538 +        self._group_actions.remove(action)
  3.1539 +
  3.1540 +
  3.1541 +class ArgumentParser(_AttributeHolder, _ActionsContainer):
  3.1542 +    """Object for parsing command line strings into Python objects.
  3.1543 +
  3.1544 +    Keyword Arguments:
  3.1545 +        - prog -- The name of the program (default: sys.argv[0])
  3.1546 +        - usage -- A usage message (default: auto-generated from arguments)
  3.1547 +        - description -- A description of what the program does
  3.1548 +        - epilog -- Text following the argument descriptions
  3.1549 +        - parents -- Parsers whose arguments should be copied into this one
  3.1550 +        - formatter_class -- HelpFormatter class for printing help messages
  3.1551 +        - prefix_chars -- Characters that prefix optional arguments
  3.1552 +        - fromfile_prefix_chars -- Characters that prefix files containing
  3.1553 +            additional arguments
  3.1554 +        - argument_default -- The default value for all arguments
  3.1555 +        - conflict_handler -- String indicating how to handle conflicts
  3.1556 +        - add_help -- Add a -h/-help option
  3.1557 +    """
  3.1558 +
  3.1559 +    def __init__(self,
  3.1560 +                 prog=None,
  3.1561 +                 usage=None,
  3.1562 +                 description=None,
  3.1563 +                 epilog=None,
  3.1564 +                 version=None,
  3.1565 +                 parents=[],
  3.1566 +                 formatter_class=HelpFormatter,
  3.1567 +                 prefix_chars='-',
  3.1568 +                 fromfile_prefix_chars=None,
  3.1569 +                 argument_default=None,
  3.1570 +                 conflict_handler='error',
  3.1571 +                 add_help=True):
  3.1572 +
  3.1573 +        if version is not None:
  3.1574 +            import warnings
  3.1575 +            warnings.warn(
  3.1576 +                """The "version" argument to ArgumentParser is deprecated. """
  3.1577 +                """Please use """
  3.1578 +                """"add_argument(..., action='version', version="N", ...)" """
  3.1579 +                """instead""", DeprecationWarning)
  3.1580 +
  3.1581 +        superinit = super(ArgumentParser, self).__init__
  3.1582 +        superinit(description=description,
  3.1583 +                  prefix_chars=prefix_chars,
  3.1584 +                  argument_default=argument_default,
  3.1585 +                  conflict_handler=conflict_handler)
  3.1586 +
  3.1587 +        # default setting for prog
  3.1588 +        if prog is None:
  3.1589 +            prog = _os.path.basename(_sys.argv[0])
  3.1590 +
  3.1591 +        self.prog = prog
  3.1592 +        self.usage = usage
  3.1593 +        self.epilog = epilog
  3.1594 +        self.version = version
  3.1595 +        self.formatter_class = formatter_class
  3.1596 +        self.fromfile_prefix_chars = fromfile_prefix_chars
  3.1597 +        self.add_help = add_help
  3.1598 +
  3.1599 +        add_group = self.add_argument_group
  3.1600 +        self._positionals = add_group(_('positional arguments'))
  3.1601 +        self._optionals = add_group(_('optional arguments'))
  3.1602 +        self._subparsers = None
  3.1603 +
  3.1604 +        # register types
  3.1605 +        def identity(string):
  3.1606 +            return string
  3.1607 +        self.register('type', None, identity)
  3.1608 +
  3.1609 +        # add help and version arguments if necessary
  3.1610 +        # (using explicit default to override global argument_default)
  3.1611 +        if self.add_help:
  3.1612 +            self.add_argument(
  3.1613 +                '-h', '--help', action='help', default=SUPPRESS,
  3.1614 +                help=_('show this help message and exit'))
  3.1615 +        if self.version:
  3.1616 +            self.add_argument(
  3.1617 +                '-v', '--version', action='version', default=SUPPRESS,
  3.1618 +                version=self.version,
  3.1619 +                help=_("show program's version number and exit"))
  3.1620 +
  3.1621 +        # add parent arguments and defaults
  3.1622 +        for parent in parents:
  3.1623 +            self._add_container_actions(parent)
  3.1624 +            try:
  3.1625 +                defaults = parent._defaults
  3.1626 +            except AttributeError:
  3.1627 +                pass
  3.1628 +            else:
  3.1629 +                self._defaults.update(defaults)
  3.1630 +
  3.1631 +    # =======================
  3.1632 +    # Pretty __repr__ methods
  3.1633 +    # =======================
  3.1634 +    def _get_kwargs(self):
  3.1635 +        names = [
  3.1636 +            'prog',
  3.1637 +            'usage',
  3.1638 +            'description',
  3.1639 +            'version',
  3.1640 +            'formatter_class',
  3.1641 +            'conflict_handler',
  3.1642 +            'add_help',
  3.1643 +        ]
  3.1644 +        return [(name, getattr(self, name)) for name in names]
  3.1645 +
  3.1646 +    # ==================================
  3.1647 +    # Optional/Positional adding methods
  3.1648 +    # ==================================
  3.1649 +    def add_subparsers(self, **kwargs):
  3.1650 +        if self._subparsers is not None:
  3.1651 +            self.error(_('cannot have multiple subparser arguments'))
  3.1652 +
  3.1653 +        # add the parser class to the arguments if it's not present
  3.1654 +        kwargs.setdefault('parser_class', type(self))
  3.1655 +
  3.1656 +        if 'title' in kwargs or 'description' in kwargs:
  3.1657 +            title = _(kwargs.pop('title', 'subcommands'))
  3.1658 +            description = _(kwargs.pop('description', None))
  3.1659 +            self._subparsers = self.add_argument_group(title, description)
  3.1660 +        else:
  3.1661 +            self._subparsers = self._positionals
  3.1662 +
  3.1663 +        # prog defaults to the usage message of this parser, skipping
  3.1664 +        # optional arguments and with no "usage:" prefix
  3.1665 +        if kwargs.get('prog') is None:
  3.1666 +            formatter = self._get_formatter()
  3.1667 +            positionals = self._get_positional_actions()
  3.1668 +            groups = self._mutually_exclusive_groups
  3.1669 +            formatter.add_usage(self.usage, positionals, groups, '')
  3.1670 +            kwargs['prog'] = formatter.format_help().strip()
  3.1671 +
  3.1672 +        # create the parsers action and add it to the positionals list
  3.1673 +        parsers_class = self._pop_action_class(kwargs, 'parsers')
  3.1674 +        action = parsers_class(option_strings=[], **kwargs)
  3.1675 +        self._subparsers._add_action(action)
  3.1676 +
  3.1677 +        # return the created parsers action
  3.1678 +        return action
  3.1679 +
  3.1680 +    def _add_action(self, action):
  3.1681 +        if action.option_strings:
  3.1682 +            self._optionals._add_action(action)
  3.1683 +        else:
  3.1684 +            self._positionals._add_action(action)
  3.1685 +        return action
  3.1686 +
  3.1687 +    def _get_optional_actions(self):
  3.1688 +        return [action
  3.1689 +                for action in self._actions
  3.1690 +                if action.option_strings]
  3.1691 +
  3.1692 +    def _get_positional_actions(self):
  3.1693 +        return [action
  3.1694 +                for action in self._actions
  3.1695 +                if not action.option_strings]
  3.1696 +
  3.1697 +    # =====================================
  3.1698 +    # Command line argument parsing methods
  3.1699 +    # =====================================
  3.1700 +    def parse_args(self, args=None, namespace=None):
  3.1701 +        args, argv = self.parse_known_args(args, namespace)
  3.1702 +        if argv:
  3.1703 +            msg = _('unrecognized arguments: %s')
  3.1704 +            self.error(msg % ' '.join(argv))
  3.1705 +        return args
  3.1706 +
  3.1707 +    def parse_known_args(self, args=None, namespace=None):
  3.1708 +        # args default to the system args
  3.1709 +        if args is None:
  3.1710 +            args = _sys.argv[1:]
  3.1711 +
  3.1712 +        # default Namespace built from parser defaults
  3.1713 +        if namespace is None:
  3.1714 +            namespace = Namespace()
  3.1715 +
  3.1716 +        # add any action defaults that aren't present
  3.1717 +        for action in self._actions:
  3.1718 +            if action.dest is not SUPPRESS:
  3.1719 +                if not hasattr(namespace, action.dest):
  3.1720 +                    if action.default is not SUPPRESS:
  3.1721 +                        default = action.default
  3.1722 +                        if isinstance(action.default, _basestring):
  3.1723 +                            default = self._get_value(action, default)
  3.1724 +                        setattr(namespace, action.dest, default)
  3.1725 +
  3.1726 +        # add any parser defaults that aren't present
  3.1727 +        for dest in self._defaults:
  3.1728 +            if not hasattr(namespace, dest):
  3.1729 +                setattr(namespace, dest, self._defaults[dest])
  3.1730 +
  3.1731 +        # parse the arguments and exit if there are any errors
  3.1732 +        try:
  3.1733 +            return self._parse_known_args(args, namespace)
  3.1734 +        except ArgumentError:
  3.1735 +            err = _sys.exc_info()[1]
  3.1736 +            self.error(str(err))
  3.1737 +
  3.1738 +    def _parse_known_args(self, arg_strings, namespace):
  3.1739 +        # replace arg strings that are file references
  3.1740 +        if self.fromfile_prefix_chars is not None:
  3.1741 +            arg_strings = self._read_args_from_files(arg_strings)
  3.1742 +
  3.1743 +        # map all mutually exclusive arguments to the other arguments
  3.1744 +        # they can't occur with
  3.1745 +        action_conflicts = {}
  3.1746 +        for mutex_group in self._mutually_exclusive_groups:
  3.1747 +            group_actions = mutex_group._group_actions
  3.1748 +            for i, mutex_action in enumerate(mutex_group._group_actions):
  3.1749 +                conflicts = action_conflicts.setdefault(mutex_action, [])
  3.1750 +                conflicts.extend(group_actions[:i])
  3.1751 +                conflicts.extend(group_actions[i + 1:])
  3.1752 +
  3.1753 +        # find all option indices, and determine the arg_string_pattern
  3.1754 +        # which has an 'O' if there is an option at an index,
  3.1755 +        # an 'A' if there is an argument, or a '-' if there is a '--'
  3.1756 +        option_string_indices = {}
  3.1757 +        arg_string_pattern_parts = []
  3.1758 +        arg_strings_iter = iter(arg_strings)
  3.1759 +        for i, arg_string in enumerate(arg_strings_iter):
  3.1760 +
  3.1761 +            # all args after -- are non-options
  3.1762 +            if arg_string == '--':
  3.1763 +                arg_string_pattern_parts.append('-')
  3.1764 +                for arg_string in arg_strings_iter:
  3.1765 +                    arg_string_pattern_parts.append('A')
  3.1766 +
  3.1767 +            # otherwise, add the arg to the arg strings
  3.1768 +            # and note the index if it was an option
  3.1769 +            else:
  3.1770 +                option_tuple = self._parse_optional(arg_string)
  3.1771 +                if option_tuple is None:
  3.1772 +                    pattern = 'A'
  3.1773 +                else:
  3.1774 +                    option_string_indices[i] = option_tuple
  3.1775 +                    pattern = 'O'
  3.1776 +                arg_string_pattern_parts.append(pattern)
  3.1777 +
  3.1778 +        # join the pieces together to form the pattern
  3.1779 +        arg_strings_pattern = ''.join(arg_string_pattern_parts)
  3.1780 +
  3.1781 +        # converts arg strings to the appropriate and then takes the action
  3.1782 +        seen_actions = _set()
  3.1783 +        seen_non_default_actions = _set()
  3.1784 +
  3.1785 +        def take_action(action, argument_strings, option_string=None):
  3.1786 +            seen_actions.add(action)
  3.1787 +            argument_values = self._get_values(action, argument_strings)
  3.1788 +
  3.1789 +            # error if this argument is not allowed with other previously
  3.1790 +            # seen arguments, assuming that actions that use the default
  3.1791 +            # value don't really count as "present"
  3.1792 +            if argument_values is not action.default:
  3.1793 +                seen_non_default_actions.add(action)
  3.1794 +                for conflict_action in action_conflicts.get(action, []):
  3.1795 +                    if conflict_action in seen_non_default_actions:
  3.1796 +                        msg = _('not allowed with argument %s')
  3.1797 +                        action_name = _get_action_name(conflict_action)
  3.1798 +                        raise ArgumentError(action, msg % action_name)
  3.1799 +
  3.1800 +            # take the action if we didn't receive a SUPPRESS value
  3.1801 +            # (e.g. from a default)
  3.1802 +            if argument_values is not SUPPRESS:
  3.1803 +                action(self, namespace, argument_values, option_string)
  3.1804 +
  3.1805 +        # function to convert arg_strings into an optional action
  3.1806 +        def consume_optional(start_index):
  3.1807 +
  3.1808 +            # get the optional identified at this index
  3.1809 +            option_tuple = option_string_indices[start_index]
  3.1810 +            action, option_string, explicit_arg = option_tuple
  3.1811 +
  3.1812 +            # identify additional optionals in the same arg string
  3.1813 +            # (e.g. -xyz is the same as -x -y -z if no args are required)
  3.1814 +            match_argument = self._match_argument
  3.1815 +            action_tuples = []
  3.1816 +            while True:
  3.1817 +
  3.1818 +                # if we found no optional action, skip it
  3.1819 +                if action is None:
  3.1820 +                    extras.append(arg_strings[start_index])
  3.1821 +                    return start_index + 1
  3.1822 +
  3.1823 +                # if there is an explicit argument, try to match the
  3.1824 +                # optional's string arguments to only this
  3.1825 +                if explicit_arg is not None:
  3.1826 +                    arg_count = match_argument(action, 'A')
  3.1827 +
  3.1828 +                    # if the action is a single-dash option and takes no
  3.1829 +                    # arguments, try to parse more single-dash options out
  3.1830 +                    # of the tail of the option string
  3.1831 +                    chars = self.prefix_chars
  3.1832 +                    if arg_count == 0 and option_string[1] not in chars:
  3.1833 +                        action_tuples.append((action, [], option_string))
  3.1834 +                        for char in self.prefix_chars:
  3.1835 +                            option_string = char + explicit_arg[0]
  3.1836 +                            explicit_arg = explicit_arg[1:] or None
  3.1837 +                            optionals_map = self._option_string_actions
  3.1838 +                            if option_string in optionals_map:
  3.1839 +                                action = optionals_map[option_string]
  3.1840 +                                break
  3.1841 +                        else:
  3.1842 +                            msg = _('ignored explicit argument %r')
  3.1843 +                            raise ArgumentError(action, msg % explicit_arg)
  3.1844 +
  3.1845 +                    # if the action expect exactly one argument, we've
  3.1846 +                    # successfully matched the option; exit the loop
  3.1847 +                    elif arg_count == 1:
  3.1848 +                        stop = start_index + 1
  3.1849 +                        args = [explicit_arg]
  3.1850 +                        action_tuples.append((action, args, option_string))
  3.1851 +                        break
  3.1852 +
  3.1853 +                    # error if a double-dash option did not use the
  3.1854 +                    # explicit argument
  3.1855 +                    else:
  3.1856 +                        msg = _('ignored explicit argument %r')
  3.1857 +                        raise ArgumentError(action, msg % explicit_arg)
  3.1858 +
  3.1859 +                # if there is no explicit argument, try to match the
  3.1860 +                # optional's string arguments with the following strings
  3.1861 +                # if successful, exit the loop
  3.1862 +                else:
  3.1863 +                    start = start_index + 1
  3.1864 +                    selected_patterns = arg_strings_pattern[start:]
  3.1865 +                    arg_count = match_argument(action, selected_patterns)
  3.1866 +                    stop = start + arg_count
  3.1867 +                    args = arg_strings[start:stop]
  3.1868 +                    action_tuples.append((action, args, option_string))
  3.1869 +                    break
  3.1870 +
  3.1871 +            # add the Optional to the list and return the index at which
  3.1872 +            # the Optional's string args stopped
  3.1873 +            assert action_tuples
  3.1874 +            for action, args, option_string in action_tuples:
  3.1875 +                take_action(action, args, option_string)
  3.1876 +            return stop
  3.1877 +
  3.1878 +        # the list of Positionals left to be parsed; this is modified
  3.1879 +        # by consume_positionals()
  3.1880 +        positionals = self._get_positional_actions()
  3.1881 +
  3.1882 +        # function to convert arg_strings into positional actions
  3.1883 +        def consume_positionals(start_index):
  3.1884 +            # match as many Positionals as possible
  3.1885 +            match_partial = self._match_arguments_partial
  3.1886 +            selected_pattern = arg_strings_pattern[start_index:]
  3.1887 +            arg_counts = match_partial(positionals, selected_pattern)
  3.1888 +
  3.1889 +            # slice off the appropriate arg strings for each Positional
  3.1890 +            # and add the Positional and its args to the list
  3.1891 +            for action, arg_count in zip(positionals, arg_counts):
  3.1892 +                args = arg_strings[start_index: start_index + arg_count]
  3.1893 +                start_index += arg_count
  3.1894 +                take_action(action, args)
  3.1895 +
  3.1896 +            # slice off the Positionals that we just parsed and return the
  3.1897 +            # index at which the Positionals' string args stopped
  3.1898 +            positionals[:] = positionals[len(arg_counts):]
  3.1899 +            return start_index
  3.1900 +
  3.1901 +        # consume Positionals and Optionals alternately, until we have
  3.1902 +        # passed the last option string
  3.1903 +        extras = []
  3.1904 +        start_index = 0
  3.1905 +        if option_string_indices:
  3.1906 +            max_option_string_index = max(option_string_indices)
  3.1907 +        else:
  3.1908 +            max_option_string_index = -1
  3.1909 +        while start_index <= max_option_string_index:
  3.1910 +
  3.1911 +            # consume any Positionals preceding the next option
  3.1912 +            next_option_string_index = min([
  3.1913 +                index
  3.1914 +                for index in option_string_indices
  3.1915 +                if index >= start_index])
  3.1916 +            if start_index != next_option_string_index:
  3.1917 +                positionals_end_index = consume_positionals(start_index)
  3.1918 +
  3.1919 +                # only try to parse the next optional if we didn't consume
  3.1920 +                # the option string during the positionals parsing
  3.1921 +                if positionals_end_index > start_index:
  3.1922 +                    start_index = positionals_end_index
  3.1923 +                    continue
  3.1924 +                else:
  3.1925 +                    start_index = positionals_end_index
  3.1926 +
  3.1927 +            # if we consumed all the positionals we could and we're not
  3.1928 +            # at the index of an option string, there were extra arguments
  3.1929 +            if start_index not in option_string_indices:
  3.1930 +                strings = arg_strings[start_index:next_option_string_index]
  3.1931 +                extras.extend(strings)
  3.1932 +                start_index = next_option_string_index
  3.1933 +
  3.1934 +            # consume the next optional and any arguments for it
  3.1935 +            start_index = consume_optional(start_index)
  3.1936 +
  3.1937 +        # consume any positionals following the last Optional
  3.1938 +        stop_index = consume_positionals(start_index)
  3.1939 +
  3.1940 +        # if we didn't consume all the argument strings, there were extras
  3.1941 +        extras.extend(arg_strings[stop_index:])
  3.1942 +
  3.1943 +        # if we didn't use all the Positional objects, there were too few
  3.1944 +        # arg strings supplied.
  3.1945 +        if positionals:
  3.1946 +            self.error(_('too few arguments'))
  3.1947 +
  3.1948 +        # make sure all required actions were present
  3.1949 +        for action in self._actions:
  3.1950 +            if action.required:
  3.1951 +                if action not in seen_actions:
  3.1952 +                    name = _get_action_name(action)
  3.1953 +                    self.error(_('argument %s is required') % name)
  3.1954 +
  3.1955 +        # make sure all required groups had one option present
  3.1956 +        for group in self._mutually_exclusive_groups:
  3.1957 +            if group.required:
  3.1958 +                for action in group._group_actions:
  3.1959 +                    if action in seen_non_default_actions:
  3.1960 +                        break
  3.1961 +
  3.1962 +                # if no actions were used, report the error
  3.1963 +                else:
  3.1964 +                    names = [_get_action_name(action)
  3.1965 +                             for action in group._group_actions
  3.1966 +                             if action.help is not SUPPRESS]
  3.1967 +                    msg = _('one of the arguments %s is required')
  3.1968 +                    self.error(msg % ' '.join(names))
  3.1969 +
  3.1970 +        # return the updated namespace and the extra arguments
  3.1971 +        return namespace, extras
  3.1972 +
  3.1973 +    def _read_args_from_files(self, arg_strings):
  3.1974 +        # expand arguments referencing files
  3.1975 +        new_arg_strings = []
  3.1976 +        for arg_string in arg_strings:
  3.1977 +
  3.1978 +            # for regular arguments, just add them back into the list
  3.1979 +            if arg_string[0] not in self.fromfile_prefix_chars:
  3.1980 +                new_arg_strings.append(arg_string)
  3.1981 +
  3.1982 +            # replace arguments referencing files with the file content
  3.1983 +            else:
  3.1984 +                try:
  3.1985 +                    args_file = open(arg_string[1:])
  3.1986 +                    try:
  3.1987 +                        arg_strings = []
  3.1988 +                        for arg_line in args_file.read().splitlines():
  3.1989 +                            for arg in self.convert_arg_line_to_args(arg_line):
  3.1990 +                                arg_strings.append(arg)
  3.1991 +                        arg_strings = self._read_args_from_files(arg_strings)
  3.1992 +                        new_arg_strings.extend(arg_strings)
  3.1993 +                    finally:
  3.1994 +                        args_file.close()
  3.1995 +                except IOError:
  3.1996 +                    err = _sys.exc_info()[1]
  3.1997 +                    self.error(str(err))
  3.1998 +
  3.1999 +        # return the modified argument list
  3.2000 +        return new_arg_strings
  3.2001 +
  3.2002 +    def convert_arg_line_to_args(self, arg_line):
  3.2003 +        return [arg_line]
  3.2004 +
  3.2005 +    def _match_argument(self, action, arg_strings_pattern):
  3.2006 +        # match the pattern for this action to the arg strings
  3.2007 +        nargs_pattern = self._get_nargs_pattern(action)
  3.2008 +        match = _re.match(nargs_pattern, arg_strings_pattern)
  3.2009 +
  3.2010 +        # raise an exception if we weren't able to find a match
  3.2011 +        if match is None:
  3.2012 +            nargs_errors = {
  3.2013 +                None: _('expected one argument'),
  3.2014 +                OPTIONAL: _('expected at most one argument'),
  3.2015 +                ONE_OR_MORE: _('expected at least one argument'),
  3.2016 +            }
  3.2017 +            default = _('expected %s argument(s)') % action.nargs
  3.2018 +            msg = nargs_errors.get(action.nargs, default)
  3.2019 +            raise ArgumentError(action, msg)
  3.2020 +
  3.2021 +        # return the number of arguments matched
  3.2022 +        return len(match.group(1))
  3.2023 +
  3.2024 +    def _match_arguments_partial(self, actions, arg_strings_pattern):
  3.2025 +        # progressively shorten the actions list by slicing off the
  3.2026 +        # final actions until we find a match
  3.2027 +        result = []
  3.2028 +        for i in range(len(actions), 0, -1):
  3.2029 +            actions_slice = actions[:i]
  3.2030 +            pattern = ''.join([self._get_nargs_pattern(action)
  3.2031 +                               for action in actions_slice])
  3.2032 +            match = _re.match(pattern, arg_strings_pattern)
  3.2033 +            if match is not None:
  3.2034 +                result.extend([len(string) for string in match.groups()])
  3.2035 +                break
  3.2036 +
  3.2037 +        # return the list of arg string counts
  3.2038 +        return result
  3.2039 +
  3.2040 +    def _parse_optional(self, arg_string):
  3.2041 +        # if it's an empty string, it was meant to be a positional
  3.2042 +        if not arg_string:
  3.2043 +            return None
  3.2044 +
  3.2045 +        # if it doesn't start with a prefix, it was meant to be positional
  3.2046 +        if not arg_string[0] in self.prefix_chars:
  3.2047 +            return None
  3.2048 +
  3.2049 +        # if the option string is present in the parser, return the action
  3.2050 +        if arg_string in self._option_string_actions:
  3.2051 +            action = self._option_string_actions[arg_string]
  3.2052 +            return action, arg_string, None
  3.2053 +
  3.2054 +        # if it's just a single character, it was meant to be positional
  3.2055 +        if len(arg_string) == 1:
  3.2056 +            return None
  3.2057 +
  3.2058 +        # if the option string before the "=" is present, return the action
  3.2059 +        if '=' in arg_string:
  3.2060 +            option_string, explicit_arg = arg_string.split('=', 1)
  3.2061 +            if option_string in self._option_string_actions:
  3.2062 +                action = self._option_string_actions[option_string]
  3.2063 +                return action, option_string, explicit_arg
  3.2064 +
  3.2065 +        # search through all possible prefixes of the option string
  3.2066 +        # and all actions in the parser for possible interpretations
  3.2067 +        option_tuples = self._get_option_tuples(arg_string)
  3.2068 +
  3.2069 +        # if multiple actions match, the option string was ambiguous
  3.2070 +        if len(option_tuples) > 1:
  3.2071 +            options = ', '.join([option_string
  3.2072 +                for action, option_string, explicit_arg in option_tuples])
  3.2073 +            tup = arg_string, options
  3.2074 +            self.error(_('ambiguous option: %s could match %s') % tup)
  3.2075 +
  3.2076 +        # if exactly one action matched, this segmentation is good,
  3.2077 +        # so return the parsed action
  3.2078 +        elif len(option_tuples) == 1:
  3.2079 +            option_tuple, = option_tuples
  3.2080 +            return option_tuple
  3.2081 +
  3.2082 +        # if it was not found as an option, but it looks like a negative
  3.2083 +        # number, it was meant to be positional
  3.2084 +        # unless there are negative-number-like options
  3.2085 +        if self._negative_number_matcher.match(arg_string):
  3.2086 +            if not self._has_negative_number_optionals:
  3.2087 +                return None
  3.2088 +
  3.2089 +        # if it contains a space, it was meant to be a positional
  3.2090 +        if ' ' in arg_string:
  3.2091 +            return None
  3.2092 +
  3.2093 +        # it was meant to be an optional but there is no such option
  3.2094 +        # in this parser (though it might be a valid option in a subparser)
  3.2095 +        return None, arg_string, None
  3.2096 +
  3.2097 +    def _get_option_tuples(self, option_string):
  3.2098 +        result = []
  3.2099 +
  3.2100 +        # option strings starting with two prefix characters are only
  3.2101 +        # split at the '='
  3.2102 +        chars = self.prefix_chars
  3.2103 +        if option_string[0] in chars and option_string[1] in chars:
  3.2104 +            if '=' in option_string:
  3.2105 +                option_prefix, explicit_arg = option_string.split('=', 1)
  3.2106 +            else:
  3.2107 +                option_prefix = option_string
  3.2108 +                explicit_arg = None
  3.2109 +            for option_string in self._option_string_actions:
  3.2110 +                if option_string.startswith(option_prefix):
  3.2111 +                    action = self._option_string_actions[option_string]
  3.2112 +                    tup = action, option_string, explicit_arg
  3.2113 +                    result.append(tup)
  3.2114 +
  3.2115 +        # single character options can be concatenated with their arguments
  3.2116 +        # but multiple character options always have to have their argument
  3.2117 +        # separate
  3.2118 +        elif option_string[0] in chars and option_string[1] not in chars:
  3.2119 +            option_prefix = option_string
  3.2120 +            explicit_arg = None
  3.2121 +            short_option_prefix = option_string[:2]
  3.2122 +            short_explicit_arg = option_string[2:]
  3.2123 +
  3.2124 +            for option_string in self._option_string_actions:
  3.2125 +                if option_string == short_option_prefix:
  3.2126 +                    action = self._option_string_actions[option_string]
  3.2127 +                    tup = action, option_string, short_explicit_arg
  3.2128 +                    result.append(tup)
  3.2129 +                elif option_string.startswith(option_prefix):
  3.2130 +                    action = self._option_string_actions[option_string]
  3.2131 +                    tup = action, option_string, explicit_arg
  3.2132 +                    result.append(tup)
  3.2133 +
  3.2134 +        # shouldn't ever get here
  3.2135 +        else:
  3.2136 +            self.error(_('unexpected option string: %s') % option_string)
  3.2137 +
  3.2138 +        # return the collected option tuples
  3.2139 +        return result
  3.2140 +
  3.2141 +    def _get_nargs_pattern(self, action):
  3.2142 +        # in all examples below, we have to allow for '--' args
  3.2143 +        # which are represented as '-' in the pattern
  3.2144 +        nargs = action.nargs
  3.2145 +
  3.2146 +        # the default (None) is assumed to be a single argument
  3.2147 +        if nargs is None:
  3.2148 +            nargs_pattern = '(-*A-*)'
  3.2149 +
  3.2150 +        # allow zero or one arguments
  3.2151 +        elif nargs == OPTIONAL:
  3.2152 +            nargs_pattern = '(-*A?-*)'
  3.2153 +
  3.2154 +        # allow zero or more arguments
  3.2155 +        elif nargs == ZERO_OR_MORE:
  3.2156 +            nargs_pattern = '(-*[A-]*)'
  3.2157 +
  3.2158 +        # allow one or more arguments
  3.2159 +        elif nargs == ONE_OR_MORE:
  3.2160 +            nargs_pattern = '(-*A[A-]*)'
  3.2161 +
  3.2162 +        # allow any number of options or arguments
  3.2163 +        elif nargs == REMAINDER:
  3.2164 +            nargs_pattern = '([-AO]*)'
  3.2165 +
  3.2166 +        # allow one argument followed by any number of options or arguments
  3.2167 +        elif nargs == PARSER:
  3.2168 +            nargs_pattern = '(-*A[-AO]*)'
  3.2169 +
  3.2170 +        # all others should be integers
  3.2171 +        else:
  3.2172 +            nargs_pattern = '(-*%s-*)' % '-*'.join('A' * nargs)
  3.2173 +
  3.2174 +        # if this is an optional action, -- is not allowed
  3.2175 +        if action.option_strings:
  3.2176 +            nargs_pattern = nargs_pattern.replace('-*', '')
  3.2177 +            nargs_pattern = nargs_pattern.replace('-', '')
  3.2178 +
  3.2179 +        # return the pattern
  3.2180 +        return nargs_pattern
  3.2181 +
  3.2182 +    # ========================
  3.2183 +    # Value conversion methods
  3.2184 +    # ========================
  3.2185 +    def _get_values(self, action, arg_strings):
  3.2186 +        # for everything but PARSER args, strip out '--'
  3.2187 +        if action.nargs not in [PARSER, REMAINDER]:
  3.2188 +            arg_strings = [s for s in arg_strings if s != '--']
  3.2189 +
  3.2190 +        # optional argument produces a default when not present
  3.2191 +        if not arg_strings and action.nargs == OPTIONAL:
  3.2192 +            if action.option_strings:
  3.2193 +                value = action.const
  3.2194 +            else:
  3.2195 +                value = action.default
  3.2196 +            if isinstance(value, _basestring):
  3.2197 +                value = self._get_value(action, value)
  3.2198 +                self._check_value(action, value)
  3.2199 +
  3.2200 +        # when nargs='*' on a positional, if there were no command-line
  3.2201 +        # args, use the default if it is anything other than None
  3.2202 +        elif (not arg_strings and action.nargs == ZERO_OR_MORE and
  3.2203 +              not action.option_strings):
  3.2204 +            if action.default is not None:
  3.2205 +                value = action.default
  3.2206 +            else:
  3.2207 +                value = arg_strings
  3.2208 +            self._check_value(action, value)
  3.2209 +
  3.2210 +        # single argument or optional argument produces a single value
  3.2211 +        elif len(arg_strings) == 1 and action.nargs in [None, OPTIONAL]:
  3.2212 +            arg_string, = arg_strings
  3.2213 +            value = self._get_value(action, arg_string)
  3.2214 +            self._check_value(action, value)
  3.2215 +
  3.2216 +        # REMAINDER arguments convert all values, checking none
  3.2217 +        elif action.nargs == REMAINDER:
  3.2218 +            value = [self._get_value(action, v) for v in arg_strings]
  3.2219 +
  3.2220 +        # PARSER arguments convert all values, but check only the first
  3.2221 +        elif action.nargs == PARSER:
  3.2222 +            value = [self._get_value(action, v) for v in arg_strings]
  3.2223 +            self._check_value(action, value[0])
  3.2224 +
  3.2225 +        # all other types of nargs produce a list
  3.2226 +        else:
  3.2227 +            value = [self._get_value(action, v) for v in arg_strings]
  3.2228 +            for v in value:
  3.2229 +                self._check_value(action, v)
  3.2230 +
  3.2231 +        # return the converted value
  3.2232 +        return value
  3.2233 +
  3.2234 +    def _get_value(self, action, arg_string):
  3.2235 +        type_func = self._registry_get('type', action.type, action.type)
  3.2236 +        if not _callable(type_func):
  3.2237 +            msg = _('%r is not callable')
  3.2238 +            raise ArgumentError(action, msg % type_func)
  3.2239 +
  3.2240 +        # convert the value to the appropriate type
  3.2241 +        try:
  3.2242 +            result = type_func(arg_string)
  3.2243 +
  3.2244 +        # ArgumentTypeErrors indicate errors
  3.2245 +        except ArgumentTypeError:
  3.2246 +            name = getattr(action.type, '__name__', repr(action.type))
  3.2247 +            msg = str(_sys.exc_info()[1])
  3.2248 +            raise ArgumentError(action, msg)
  3.2249 +
  3.2250 +        # TypeErrors or ValueErrors also indicate errors
  3.2251 +        except (TypeError, ValueError):
  3.2252 +            name = getattr(action.type, '__name__', repr(action.type))
  3.2253 +            msg = _('invalid %s value: %r')
  3.2254 +            raise ArgumentError(action, msg % (name, arg_string))
  3.2255 +
  3.2256 +        # return the converted value
  3.2257 +        return result
  3.2258 +
  3.2259 +    def _check_value(self, action, value):
  3.2260 +        # converted value must be one of the choices (if specified)
  3.2261 +        if action.choices is not None and value not in action.choices:
  3.2262 +            tup = value, ', '.join(map(repr, action.choices))
  3.2263 +            msg = _('invalid choice: %r (choose from %s)') % tup
  3.2264 +            raise ArgumentError(action, msg)
  3.2265 +
  3.2266 +    # =======================
  3.2267 +    # Help-formatting methods
  3.2268 +    # =======================
  3.2269 +    def format_usage(self):
  3.2270 +        formatter = self._get_formatter()
  3.2271 +        formatter.add_usage(self.usage, self._actions,
  3.2272 +                            self._mutually_exclusive_groups)
  3.2273 +        return formatter.format_help()
  3.2274 +
  3.2275 +    def format_help(self):
  3.2276 +        formatter = self._get_formatter()
  3.2277 +
  3.2278 +        # usage
  3.2279 +        formatter.add_usage(self.usage, self._actions,
  3.2280 +                            self._mutually_exclusive_groups)
  3.2281 +
  3.2282 +        # description
  3.2283 +        formatter.add_text(self.description)
  3.2284 +
  3.2285 +        # positionals, optionals and user-defined groups
  3.2286 +        for action_group in self._action_groups:
  3.2287 +            formatter.start_section(action_group.title)
  3.2288 +            formatter.add_text(action_group.description)
  3.2289 +            formatter.add_arguments(action_group._group_actions)
  3.2290 +            formatter.end_section()
  3.2291 +
  3.2292 +        # epilog
  3.2293 +        formatter.add_text(self.epilog)
  3.2294 +
  3.2295 +        # determine help from format above
  3.2296 +        return formatter.format_help()
  3.2297 +
  3.2298 +    def format_version(self):
  3.2299 +        import warnings
  3.2300 +        warnings.warn(
  3.2301 +            'The format_version method is deprecated -- the "version" '
  3.2302 +            'argument to ArgumentParser is no longer supported.',
  3.2303 +            DeprecationWarning)
  3.2304 +        formatter = self._get_formatter()
  3.2305 +        formatter.add_text(self.version)
  3.2306 +        return formatter.format_help()
  3.2307 +
  3.2308 +    def _get_formatter(self):
  3.2309 +        return self.formatter_class(prog=self.prog)
  3.2310 +
  3.2311 +    # =====================
  3.2312 +    # Help-printing methods
  3.2313 +    # =====================
  3.2314 +    def print_usage(self, file=None):
  3.2315 +        if file is None:
  3.2316 +            file = _sys.stdout
  3.2317 +        self._print_message(self.format_usage(), file)
  3.2318 +
  3.2319 +    def print_help(self, file=None):
  3.2320 +        if file is None:
  3.2321 +            file = _sys.stdout
  3.2322 +        self._print_message(self.format_help(), file)
  3.2323 +
  3.2324 +    def print_version(self, file=None):
  3.2325 +        import warnings
  3.2326 +        warnings.warn(
  3.2327 +            'The print_version method is deprecated -- the "version" '
  3.2328 +            'argument to ArgumentParser is no longer supported.',
  3.2329 +            DeprecationWarning)
  3.2330 +        self._print_message(self.format_version(), file)
  3.2331 +
  3.2332 +    def _print_message(self, message, file=None):
  3.2333 +        if message:
  3.2334 +            if file is None:
  3.2335 +                file = _sys.stderr
  3.2336 +            file.write(message)
  3.2337 +
  3.2338 +    # ===============
  3.2339 +    # Exiting methods
  3.2340 +    # ===============
  3.2341 +    def exit(self, status=0, message=None):
  3.2342 +        if message:
  3.2343 +            self._print_message(message, _sys.stderr)
  3.2344 +        _sys.exit(status)
  3.2345 +
  3.2346 +    def error(self, message):
  3.2347 +        """error(message: string)
  3.2348 +
  3.2349 +        Prints a usage message incorporating the message to stderr and
  3.2350 +        exits.
  3.2351 +
  3.2352 +        If you override this in a subclass, it should not return -- it
  3.2353 +        should either exit or raise an exception.
  3.2354 +        """
  3.2355 +        self.print_usage(_sys.stderr)
  3.2356 +        self.exit(2, _('%s: error: %s\n') % (self.prog, message))
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py	Mon Nov 26 12:04:32 2012 +0100
     4.3 @@ -0,0 +1,60 @@
     4.4 +#!/usr/bin/python
     4.5 +'''
     4.6 +Created on Jul 13, 2012
     4.7 +
     4.8 +@author: Daniel Kuehlwein
     4.9 +'''
    4.10 +
    4.11 +import sys
    4.12 +from argparse import ArgumentParser,RawDescriptionHelpFormatter
    4.13 +from matplotlib.pyplot import plot,figure,show,legend,xlabel,ylabel,axis,hist
    4.14 +from stats import Statistics
    4.15 +
    4.16 +parser = ArgumentParser(description='Compare Statistics.  \n\n\
    4.17 +Loads different statistics and displays a comparison. Requires the matplotlib module.\n\n\
    4.18 +-------- Example Usage ---------------\n\
    4.19 +./compareStats.py --statFiles ../tmp/natISANB.stats ../tmp/natATPNB.stats -b 30\n\n\
    4.20 +Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter)
    4.21 +parser.add_argument('--statFiles', default=None, nargs='+', 
    4.22 +                    help='The names of the saved statistic files.')
    4.23 +parser.add_argument('-b','--bins',default=50,help="Number of bins for the AUC histogram. Default=50.",type=int)
    4.24 +
    4.25 +def main(argv = sys.argv[1:]):
    4.26 +    args = parser.parse_args(argv)  
    4.27 +    if args.statFiles == None:
    4.28 +        print 'Filenames missing.'
    4.29 +        sys.exit(-1)
    4.30 +
    4.31 +    aucData = []
    4.32 +    aucLabels = []
    4.33 +    for statFile in args.statFiles:
    4.34 +        s = Statistics()
    4.35 +        s.load(statFile)
    4.36 +        avgRecall = [float(x)/s.problems for x in s.recallData]
    4.37 +        figure('Recall')
    4.38 +        plot(range(s.cutOff),avgRecall,label=statFile)
    4.39 +        legend(loc='lower right')
    4.40 +        ylabel('Average Recall')
    4.41 +        xlabel('Highest ranked premises')
    4.42 +        axis([0,s.cutOff,0.0,1.0])
    4.43 +        figure('100%Recall')
    4.44 +        plot(range(s.cutOff),s.recall100Data,label=statFile)
    4.45 +        legend(loc='lower right')
    4.46 +        ylabel('100%Recall')
    4.47 +        xlabel('Highest ranked premises')
    4.48 +        axis([0,s.cutOff,0,s.problems])
    4.49 +        aucData.append(s.aucData)
    4.50 +        aucLabels.append(statFile)
    4.51 +    figure('AUC Histogram')
    4.52 +    hist(aucData,bins=args.bins,label=aucLabels,histtype='bar')
    4.53 +    legend(loc='upper left')
    4.54 +    ylabel('Problems')
    4.55 +    xlabel('AUC')
    4.56 +        
    4.57 +    show()
    4.58 +
    4.59 +if __name__ == '__main__':
    4.60 +    #args = ['--statFiles','../tmp/natISANB.stats','../tmp/natATPNB.stats','-b','30']
    4.61 +    #sys.exit(main(args))
    4.62 +    sys.exit(main())
    4.63 +    
    4.64 \ No newline at end of file
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Mon Nov 26 12:04:32 2012 +0100
     5.3 @@ -0,0 +1,182 @@
     5.4 +'''
     5.5 +Created on Jul 12, 2012
     5.6 +
     5.7 +@author: daniel
     5.8 +'''
     5.9 +
    5.10 +from os.path import join
    5.11 +from Queue import Queue
    5.12 +from readData import create_accessible_dict,create_dependencies_dict,create_feature_dict
    5.13 +from cPickle import load,dump
    5.14 +
    5.15 +class Dictionaries(object):
    5.16 +    '''
    5.17 +    This class contains all info about name-> id mapping, etc.
    5.18 +    '''
    5.19 +    def __init__(self):
    5.20 +        '''
    5.21 +        Constructor
    5.22 +        '''
    5.23 +        self.nameIdDict = {}
    5.24 +        self.idNameDict = {}
    5.25 +        self.featureIdDict={}
    5.26 +        self.maxNameId = 0
    5.27 +        self.maxFeatureId = 0
    5.28 +        self.featureDict = {}
    5.29 +        self.dependenciesDict = {}
    5.30 +        self.accessibleDict = {}
    5.31 +        self.expandedAccessibles = {}
    5.32 +        self.changed = True
    5.33 +    
    5.34 +    """
    5.35 +    Init functions. Side Effect: nameIdDict, idNameDict, featureIdDict get filled!
    5.36 +    """    
    5.37 +    def init_featureDict(self,featureFile):
    5.38 +        self.featureDict,self.maxNameId,self.maxFeatureId = create_feature_dict(self.nameIdDict,self.idNameDict,self.maxNameId,self.featureIdDict,\
    5.39 +                                                                                self.maxFeatureId,featureFile)        
    5.40 +    def init_dependenciesDict(self,depFile):
    5.41 +        self.dependenciesDict = create_dependencies_dict(self.nameIdDict,depFile)
    5.42 +    def init_accessibleDict(self,accFile):
    5.43 +        self.accessibleDict,self.maxNameId = create_accessible_dict(self.nameIdDict,self.idNameDict,self.maxNameId,accFile)
    5.44 +    
    5.45 +    def init_all(self,inputFolder,featureFileName = 'mash_features',depFileName='mash_dependencies',accFileName = 'mash_accessibility'):
    5.46 +        featureFile = join(inputFolder,featureFileName)
    5.47 +        depFile = join(inputFolder,depFileName)
    5.48 +        accFile = join(inputFolder,accFileName)
    5.49 +        self.init_featureDict(featureFile)
    5.50 +        self.init_accessibleDict(accFile)
    5.51 +        self.init_dependenciesDict(depFile)
    5.52 +        self.expandedAccessibles = {}
    5.53 +        self.changed = True
    5.54 +        
    5.55 +    def get_name_id(self,name):
    5.56 +        """
    5.57 +        Return the Id for a name.
    5.58 +        If it doesn't exist yet, a new entry is created.
    5.59 +        """
    5.60 +        if self.nameIdDict.has_key(name):
    5.61 +            nameId = self.nameIdDict[name]
    5.62 +        else:
    5.63 +            self.nameIdDict[name] = self.maxNameId
    5.64 +            self.idNameDict[self.maxNameId] = name
    5.65 +            nameId = self.maxNameId
    5.66 +            self.maxNameId += 1 
    5.67 +            self.changed = True
    5.68 +        return nameId
    5.69 +
    5.70 +    def add_feature(self,featureName):
    5.71 +        if not self.featureIdDict.has_key(featureName):
    5.72 +            self.featureIdDict[featureName] = self.maxFeatureId
    5.73 +            self.maxFeatureId += 1
    5.74 +            self.changed = True 
    5.75 +            
    5.76 +    def expand_accessibles(self,acc):
    5.77 +        accessibles = set(acc)
    5.78 +        unexpandedQueue = Queue()
    5.79 +        for a in acc:
    5.80 +            if self.expandedAccessibles.has_key(a):
    5.81 +                accessibles = accessibles.union(self.expandedAccessibles[a])
    5.82 +            else:
    5.83 +                unexpandedQueue.put(a)
    5.84 +        while not unexpandedQueue.empty():
    5.85 +            nextUnExp = unexpandedQueue.get()
    5.86 +            nextUnExpAcc = self.accessibleDict[nextUnExp]            
    5.87 +            for a in nextUnExpAcc:
    5.88 +                if not a in accessibles:
    5.89 +                    accessibles = accessibles.union([a])
    5.90 +                    if self.expandedAccessibles.has_key(a):
    5.91 +                        accessibles = accessibles.union(self.expandedAccessibles[a])
    5.92 +                    else:
    5.93 +                        unexpandedQueue.put(a)                    
    5.94 +        return list(accessibles)
    5.95 +            
    5.96 +    def parse_fact(self,line):
    5.97 +        """
    5.98 +        Parses a single line, extracting accessibles, features, and dependencies.
    5.99 +        """
   5.100 +        assert line.startswith('! ')
   5.101 +        line = line[2:]
   5.102 +        
   5.103 +        # line = name:accessibles;features;dependencies
   5.104 +        line = line.split(':')
   5.105 +        name = line[0].strip()
   5.106 +        nameId = self.get_name_id(name)
   5.107 +    
   5.108 +        line = line[1].split(';')       
   5.109 +        # Accessible Ids
   5.110 +        unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
   5.111 +        self.accessibleDict[nameId] = unExpAcc
   5.112 +        # Feature Ids
   5.113 +        featureNames = [f.strip() for f in line[1].split()]
   5.114 +        for fn in featureNames:
   5.115 +            self.add_feature(fn)
   5.116 +        self.featureDict[nameId] = [self.featureIdDict[fn] for fn in featureNames]
   5.117 +        self.dependenciesDict[nameId] = [self.nameIdDict[d.strip()] for d in line[2].split()]
   5.118 +        self.changed = True
   5.119 +        return nameId
   5.120 +    
   5.121 +    def parse_overwrite(self,line):
   5.122 +        """
   5.123 +        Parses a single line, extracts the problemId and the Ids of the dependencies.
   5.124 +        """
   5.125 +        assert line.startswith('p ')
   5.126 +        line = line[2:]
   5.127 +        
   5.128 +        # line = name:dependencies
   5.129 +        line = line.split(':')
   5.130 +        name = line[0].strip()
   5.131 +        nameId = self.get_name_id(name)
   5.132 +    
   5.133 +        dependencies = [self.nameIdDict[d.strip()] for d in line[1].split()]
   5.134 +        self.changed = True
   5.135 +        return nameId,dependencies
   5.136 +    
   5.137 +    def parse_problem(self,line):
   5.138 +        """
   5.139 +        Parses a problem and returns the features and the accessibles. 
   5.140 +        """
   5.141 +        assert line.startswith('? ')
   5.142 +        line = line[2:]
   5.143 +        name = None
   5.144 +        
   5.145 +        # Check whether there is a problem name:
   5.146 +        tmp = line.split(':')
   5.147 +        if len(tmp) == 2:
   5.148 +            name = tmp[0].strip()
   5.149 +            line = tmp[1]
   5.150 +        
   5.151 +        # line = accessibles;features
   5.152 +        line = line.split(';')
   5.153 +        # Accessible Ids, expand and store the accessibles.
   5.154 +        unExpAcc = [self.nameIdDict[a.strip()] for a in line[0].split()]
   5.155 +        if len(self.expandedAccessibles.keys())>=100:
   5.156 +            self.expandedAccessibles = {}
   5.157 +            self.changed = True
   5.158 +        for accId in unExpAcc:
   5.159 +            if not self.expandedAccessibles.has_key(accId):
   5.160 +                accIdAcc = self.accessibleDict[accId]
   5.161 +                self.expandedAccessibles[accId] = self.expand_accessibles(accIdAcc)
   5.162 +                self.changed = True
   5.163 +        accessibles = self.expand_accessibles(unExpAcc)
   5.164 +        # Feature Ids
   5.165 +        featureNames = [f.strip() for f in line[1].split()]
   5.166 +        for fn in featureNames:
   5.167 +            self.add_feature(fn)
   5.168 +        features = [self.featureIdDict[fn] for fn in featureNames]
   5.169 +        return name,features,accessibles    
   5.170 +    
   5.171 +    def save(self,fileName):
   5.172 +        if self.changed:
   5.173 +            dictsStream = open(fileName, 'wb')
   5.174 +            dump((self.accessibleDict,self.dependenciesDict,self.expandedAccessibles,self.featureDict,\
   5.175 +                self.featureIdDict,self.idNameDict,self.maxFeatureId,self.maxNameId,self.nameIdDict),dictsStream)
   5.176 +            self.changed = False
   5.177 +            dictsStream.close()
   5.178 +    def load(self,fileName):
   5.179 +        dictsStream = open(fileName, 'rb')        
   5.180 +        self.accessibleDict,self.dependenciesDict,self.expandedAccessibles,self.featureDict,\
   5.181 +              self.featureIdDict,self.idNameDict,self.maxFeatureId,self.maxNameId,self.nameIdDict = load(dictsStream)
   5.182 +        self.changed = False
   5.183 +        dictsStream.close()
   5.184 +    
   5.185 +            
   5.186 \ No newline at end of file
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Mon Nov 26 12:04:32 2012 +0100
     6.3 @@ -0,0 +1,222 @@
     6.4 +#!/usr/bin/python
     6.5 +'''
     6.6 +MaSh - Machine Learning for Sledgehammer
     6.7 +
     6.8 +MaSh allows to use different machine learning algorithms to predict relevant fact for Sledgehammer.
     6.9 +
    6.10 +Created on July 12, 2012
    6.11 +
    6.12 +@author: Daniel Kuehlwein
    6.13 +'''
    6.14 +
    6.15 +import logging,datetime,string,os,sys
    6.16 +from argparse import ArgumentParser,RawDescriptionHelpFormatter
    6.17 +from time import time
    6.18 +from stats import Statistics
    6.19 +from dictionaries import Dictionaries
    6.20 +from naiveBayes import NBClassifier
    6.21 +from snow import SNoW
    6.22 +from predefined import Predefined
    6.23 +
    6.24 +# Set up command-line parser
    6.25 +parser = ArgumentParser(description='MaSh - Machine Learning for Sledgehammer.  \n\n\
    6.26 +MaSh allows to use different machine learning algorithms to predict relevant facts for Sledgehammer.\n\n\
    6.27 +--------------- Example Usage ---------------\n\
    6.28 +First initialize:\n./mash.py -l test.log -o ../tmp/ --init --inputDir ../data/Nat/ \n\
    6.29 +Then create predictions:\n./mash.py -i ../data/Nat/mash_commands -p ../tmp/test.pred -l test.log -o ../tmp/ --statistics\n\
    6.30 +\n\n\
    6.31 +Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter)
    6.32 +parser.add_argument('-i','--inputFile',help='File containing all problems to be solved.')
    6.33 +parser.add_argument('-o','--outputDir', default='../tmp/',help='Directory where all created files are stored. Default=../tmp/.')
    6.34 +parser.add_argument('-p','--predictions',default='../tmp/%s.predictions' % datetime.datetime.now(), 
    6.35 +                    help='File where the predictions stored. Default=../tmp/dateTime.predictions.')
    6.36 +parser.add_argument('--numberOfPredictions',default=200,help="Number of premises to write in the output. Default=200.",type=int)
    6.37 +
    6.38 +parser.add_argument('--init',default=False,action='store_true',help="Initialize Mash. Requires --inputDir to be defined. Default=False.")
    6.39 +parser.add_argument('--inputDir',default='../data/Nat/',\
    6.40 +                    help='Directory containing all the input data. MaSh expects the following files: mash_features,mash_dependencies,mash_accessibility')
    6.41 +parser.add_argument('--depFile', default='mash_dependencies',
    6.42 +                    help='Name of the file with the premise dependencies. The file must be in inputDir. Default = mash_dependencies')
    6.43 +parser.add_argument('--saveModel',default=False,action='store_true',help="Stores the learned Model at the end of a prediction run. Default=False.")
    6.44 +
    6.45 +parser.add_argument('--nb',default=False,action='store_true',help="Use Naive Bayes for learning. This is the default learning method.")
    6.46 +parser.add_argument('--snow',default=False,action='store_true',help="Use SNoW's naive bayes instead of Naive Bayes for learning.")
    6.47 +parser.add_argument('--predef',default=False,action='store_true',\
    6.48 +                    help="Use predefined predictions. Used only for comparison with the actual learning. Expects mash_meng_paulson_suggestions in inputDir.")
    6.49 +parser.add_argument('--statistics',default=False,action='store_true',help="Create and show statistics for the top CUTOFF predictions.\
    6.50 +                    WARNING: This will make the program a lot slower! Default=False.")
    6.51 +parser.add_argument('--saveStats',default=None,help="If defined, stores the statistics in the filename provided.")
    6.52 +parser.add_argument('--cutOff',default=500,help="Option for statistics. Only consider the first cutOff predictions. Default=500.",type=int)
    6.53 +parser.add_argument('-l','--log', default='../tmp/%s.log' % datetime.datetime.now(), help='Log file name. Default=../tmp/dateTime.log')
    6.54 +parser.add_argument('-q','--quiet',default=False,action='store_true',help="If enabled, only print warnings. Default=False.")
    6.55 +
    6.56 +def main(argv = sys.argv[1:]):        
    6.57 +    # Initializing command-line arguments
    6.58 +    args = parser.parse_args(argv)
    6.59 +
    6.60 +    # Set up logging 
    6.61 +    logging.basicConfig(level=logging.DEBUG,
    6.62 +                        format='%(asctime)s %(name)-12s %(levelname)-8s %(message)s',
    6.63 +                        datefmt='%d-%m %H:%M:%S',
    6.64 +                        filename=args.log,
    6.65 +                        filemode='w')
    6.66 +    console = logging.StreamHandler(sys.stdout)
    6.67 +    console.setLevel(logging.INFO)
    6.68 +    formatter = logging.Formatter('# %(message)s')
    6.69 +    console.setFormatter(formatter)
    6.70 +    logging.getLogger('').addHandler(console)
    6.71 +    logger = logging.getLogger('main.py')
    6.72 +    if args.quiet:
    6.73 +        logger.setLevel(logging.WARNING)
    6.74 +        console.setLevel(logging.WARNING)
    6.75 +    if not os.path.exists(args.outputDir):
    6.76 +        os.makedirs(args.outputDir)
    6.77 +
    6.78 +    logger.info('Using the following settings: %s',args)
    6.79 +    # Pick algorithm
    6.80 +    if args.nb:
    6.81 +        logger.info('Using Naive Bayes for learning.')        
    6.82 +        model = NBClassifier() 
    6.83 +        modelFile = os.path.join(args.outputDir,'NB.pickle')
    6.84 +    elif args.snow:
    6.85 +        logger.info('Using naive bayes (SNoW) for learning.')
    6.86 +        model = SNoW()
    6.87 +        modelFile = os.path.join(args.outputDir,'SNoW.pickle')
    6.88 +    elif args.predef:
    6.89 +        logger.info('Using predefined predictions.')
    6.90 +        predictionFile = os.path.join(args.inputDir,'mash_meng_paulson_suggestions') 
    6.91 +        model = Predefined(predictionFile)
    6.92 +        modelFile = os.path.join(args.outputDir,'isabelle.pickle')        
    6.93 +    else:
    6.94 +        logger.info('No algorithm specified. Using Naive Bayes.')        
    6.95 +        model = NBClassifier() 
    6.96 +        modelFile = os.path.join(args.outputDir,'NB.pickle')    
    6.97 +    dictsFile = os.path.join(args.outputDir,'dicts.pickle')    
    6.98 +    
    6.99 +    # Initializing model
   6.100 +    if args.init:        
   6.101 +        logger.info('Initializing Model.')
   6.102 +        startTime = time()
   6.103 +        
   6.104 +        # Load all data        
   6.105 +        dicts = Dictionaries()
   6.106 +        dicts.init_all(args.inputDir,depFileName=args.depFile)
   6.107 +        
   6.108 +        # Create Model
   6.109 +        trainData = dicts.featureDict.keys()
   6.110 +        if args.predef:
   6.111 +            dicts = model.initializeModel(trainData,dicts)
   6.112 +        else:
   6.113 +            model.initializeModel(trainData,dicts)
   6.114 +        
   6.115 +        model.save(modelFile)
   6.116 +        dicts.save(dictsFile)
   6.117 +
   6.118 +        logger.info('All Done. %s seconds needed.',round(time()-startTime,2))
   6.119 +        return 0
   6.120 +    # Create predictions and/or update model       
   6.121 +    else:
   6.122 +        lineCounter = 0
   6.123 +        dicts = Dictionaries()
   6.124 +        # Load Files
   6.125 +        if os.path.isfile(dictsFile):
   6.126 +            dicts.load(dictsFile)
   6.127 +        if os.path.isfile(modelFile):
   6.128 +            model.load(modelFile)
   6.129 +        
   6.130 +        # IO Streams
   6.131 +        OS = open(args.predictions,'a')
   6.132 +        IS = open(args.inputFile,'r')
   6.133 +        
   6.134 +        # Statistics
   6.135 +        if args.statistics:
   6.136 +            stats = Statistics(args.cutOff)
   6.137 +        
   6.138 +        predictions = None
   6.139 +        #Reading Input File
   6.140 +        for line in IS:
   6.141 + #           try:
   6.142 +            if True:
   6.143 +                if line.startswith('!'):
   6.144 +                    problemId = dicts.parse_fact(line)
   6.145 +                    # Statistics
   6.146 +                    if args.statistics:
   6.147 +                        acc = dicts.accessibleDict[problemId]
   6.148 +                        if args.predef:
   6.149 +                            predictions = model.predict[problemId]
   6.150 +                        else:
   6.151 +                            predictions,_predictionsValues = model.predict(dicts.featureDict[problemId],dicts.expand_accessibles(acc))        
   6.152 +                        stats.update(predictions,dicts.dependenciesDict[problemId])
   6.153 +                        if not stats.badPreds == []:
   6.154 +                            bp = string.join([str(dicts.idNameDict[x]) for x in stats.badPreds], ',')
   6.155 +                            logger.debug('Bad predictions: %s',bp)    
   6.156 +                    # Update Dependencies, p proves p
   6.157 +                    dicts.dependenciesDict[problemId] = [problemId]+dicts.dependenciesDict[problemId]
   6.158 +                    model.update(problemId,dicts.featureDict[problemId],dicts.dependenciesDict[problemId])
   6.159 +                elif line.startswith('p'):
   6.160 +                    # Overwrite old proof.
   6.161 +                    problemId,newDependencies = dicts.parse_overwrite(line)
   6.162 +                    newDependencies = [problemId]+newDependencies
   6.163 +                    model.overwrite(problemId,newDependencies,dicts)
   6.164 +                    dicts.dependenciesDict[problemId] = newDependencies
   6.165 +                elif line.startswith('?'):
   6.166 +                    startTime = time()
   6.167 +                    if args.predef:
   6.168 +                        continue
   6.169 +                    name,features,accessibles = dicts.parse_problem(line)
   6.170 +                    # Create predictions
   6.171 +                    logger.info('Starting computation for problem on line %s',lineCounter)                
   6.172 +                    predictions,predictionValues = model.predict(features,accessibles)        
   6.173 +                    assert len(predictions) == len(predictionValues)
   6.174 +                    logger.info('Done. %s seconds needed.',round(time()-startTime,2))
   6.175 +                    
   6.176 +                    # Output        
   6.177 +                    predictionNames = [str(dicts.idNameDict[p]) for p in predictions[:args.numberOfPredictions]]
   6.178 +                    predictionValues = [str(x) for x in predictionValues[:args.numberOfPredictions]]                    
   6.179 +                    predictionsStringList = ['%s=%s' % (predictionNames[i],predictionValues[i]) for i in range(len(predictionNames))]                
   6.180 +                    predictionsString = string.join(predictionsStringList,' ')
   6.181 +                    outString = '%s: %s' % (name,predictionsString)
   6.182 +                    OS.write('%s\n' % outString)
   6.183 +                    lineCounter += 1
   6.184 +                else:
   6.185 +                    logger.warning('Unspecified input format: \n%s',line)
   6.186 +                    sys.exit(-1)
   6.187 +            """
   6.188 +            except:
   6.189 +                logger.warning('An error occurred on line %s .',line)
   6.190 +                lineCounter += 1
   6.191 +                continue
   6.192 +            """    
   6.193 +        OS.close()
   6.194 +        IS.close()
   6.195 +        
   6.196 +        # Statistics
   6.197 +        if args.statistics:
   6.198 +            stats.printAvg()
   6.199 +        
   6.200 +        # Save
   6.201 +        if args.saveModel:
   6.202 +            model.save(modelFile)
   6.203 +        dicts.save(dictsFile)
   6.204 +        if not args.saveStats == None:
   6.205 +            statsFile = os.path.join(args.outputDir,args.saveStats)
   6.206 +            stats.save(statsFile)
   6.207 +    return 0
   6.208 +
   6.209 +if __name__ == '__main__':
   6.210 +    # Example:
   6.211 +    # Nat
   6.212 +    #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/','--predef']
   6.213 +    #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/natATPMP.stats']
   6.214 +    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/']    
   6.215 +    #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/natATPNB.stats','--cutOff','500']
   6.216 +    # BUG
   6.217 +    #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/List/','--isabelle']
   6.218 +    #args = ['-i', '../data/List/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--isabelle','-o','../tmp/','--statistics']
   6.219 +    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../bug/init','--init']
   6.220 +    #args = ['-i', '../bug/adds/mash_commands','-p','../tmp/testNB.pred','-l','testNB.log','--nb','-o','../tmp/']
   6.221 +    #startTime = time()
   6.222 +    #sys.exit(main(args))
   6.223 +    #print 'New ' + str(round(time()-startTime,2))    
   6.224 +    sys.exit(main())
   6.225 +    
   6.226 \ No newline at end of file
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/naiveBayes.py	Mon Nov 26 12:04:32 2012 +0100
     7.3 @@ -0,0 +1,130 @@
     7.4 +'''
     7.5 +Created on Jul 11, 2012
     7.6 +
     7.7 +@author: Daniel Kuehlwein
     7.8 +'''
     7.9 +
    7.10 +from cPickle import dump,load
    7.11 +from numpy import array,exp
    7.12 +from math import log
    7.13 +
    7.14 +class NBClassifier(object):
    7.15 +    '''
    7.16 +    An updateable naive Bayes classifier.
    7.17 +    '''
    7.18 +
    7.19 +    def __init__(self):
    7.20 +        '''
    7.21 +        Constructor
    7.22 +        '''
    7.23 +        self.counts = {}
    7.24 +    
    7.25 +    def initializeModel(self,trainData,dicts):
    7.26 +        """
    7.27 +        Build basic model from training data.
    7.28 +        """        
    7.29 +        for d in trainData:
    7.30 +            dPosCount = 0
    7.31 +            dFeatureCounts = {}            
    7.32 +            self.counts[d] = [dPosCount,dFeatureCounts]
    7.33 +        
    7.34 +        for key in dicts.dependenciesDict.keys():
    7.35 +            keyDeps = dicts.dependenciesDict[key]
    7.36 +            for dep in keyDeps:
    7.37 +                self.counts[dep][0] += 1
    7.38 +                depFeatures = dicts.featureDict[key]
    7.39 +                for f in depFeatures:
    7.40 +                    if self.counts[dep][1].has_key(f):
    7.41 +                        self.counts[dep][1][f] += 1
    7.42 +                    else:
    7.43 +                        self.counts[dep][1][f] = 1
    7.44 +
    7.45 +    
    7.46 +    def update(self,dataPoint,features,dependencies):
    7.47 +        """
    7.48 +        Updates the Model.
    7.49 +        """
    7.50 +        if not self.counts.has_key(dataPoint):
    7.51 +            dPosCount = 0
    7.52 +            dFeatureCounts = {}            
    7.53 +            self.counts[dataPoint] = [dPosCount,dFeatureCounts]
    7.54 +        for dep in dependencies:
    7.55 +            self.counts[dep][0] += 1
    7.56 +            for f in features:
    7.57 +                if self.counts[dep][1].has_key(f):
    7.58 +                    self.counts[dep][1][f] += 1
    7.59 +                else:
    7.60 +                    self.counts[dep][1][f] = 1
    7.61 + 
    7.62 +    def delete(self,dataPoint,features,dependencies):
    7.63 +        """
    7.64 +        Deletes a single datapoint from the model.
    7.65 +        """
    7.66 +        for dep in dependencies:
    7.67 +            self.counts[dep][0] -= 1
    7.68 +            for f in features:
    7.69 +                self.counts[dep][1][f] -= 1
    7.70 +
    7.71 +            
    7.72 +    def overwrite(self,problemId,newDependencies,dicts):
    7.73 +        """
    7.74 +        Deletes the old dependencies of problemId and replaces them with the new ones. Updates the model accordingly.
    7.75 +        """
    7.76 +        assert self.counts.has_key(problemId)
    7.77 +        oldDeps = dicts.dependenciesDict[problemId]
    7.78 +        features = dicts.featureDict[problemId]
    7.79 +        self.delete(problemId,features,oldDeps)
    7.80 +        self.update(problemId,features,newDependencies)
    7.81 +    
    7.82 +    def predict(self,features,accessibles):
    7.83 +        """
    7.84 +        For each accessible, predicts the probability of it being useful given the features.
    7.85 +        Returns a ranking of the accessibles.
    7.86 +        """
    7.87 +        predictions = []
    7.88 +        for a in accessibles:            
    7.89 +            posA = self.counts[a][0]
    7.90 +            fA = set(self.counts[a][1].keys())
    7.91 +            fWeightsA = self.counts[a][1]
    7.92 +            resultA = log(posA) 
    7.93 +            for f in features:
    7.94 +                if f in fA:
    7.95 +                    if fWeightsA[f] == 0:
    7.96 +                        resultA -= 15
    7.97 +                    else:
    7.98 +                        assert fWeightsA[f] <= posA
    7.99 +                        resultA += log(float(fWeightsA[f])/posA)
   7.100 +                else:
   7.101 +                    resultA -= 15
   7.102 +            predictions.append(resultA)
   7.103 +        expPredictions = array([exp(x) for x in predictions])
   7.104 +        predictions = array(predictions)
   7.105 +        perm = (-predictions).argsort()        
   7.106 +        return array(accessibles)[perm],expPredictions[perm] 
   7.107 +    
   7.108 +    def save(self,fileName):
   7.109 +        OStream = open(fileName, 'wb')
   7.110 +        dump(self.counts,OStream)        
   7.111 +        OStream.close()
   7.112 +        
   7.113 +    def load(self,fileName):
   7.114 +        OStream = open(fileName, 'rb')
   7.115 +        self.counts = load(OStream)      
   7.116 +        OStream.close()
   7.117 +
   7.118 +    
   7.119 +if __name__ == '__main__':
   7.120 +    featureDict = {0:[0,1,2],1:[3,2,1]}
   7.121 +    dependenciesDict = {0:[0],1:[0,1]}
   7.122 +    libDicts = (featureDict,dependenciesDict,{})
   7.123 +    c = NBClassifier()
   7.124 +    c.initializeModel([0,1],libDicts)
   7.125 +    c.update(2,[14,1,3],[0,2])
   7.126 +    print c.counts
   7.127 +    print c.predict([0,14],[0,1,2])
   7.128 +    c.storeModel('x')
   7.129 +    d = NBClassifier()
   7.130 +    d.loadModel('x')
   7.131 +    print c.counts
   7.132 +    print d.counts
   7.133 +    print 'Done'
   7.134 \ No newline at end of file
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py	Mon Nov 26 12:04:32 2012 +0100
     8.3 @@ -0,0 +1,60 @@
     8.4 +'''
     8.5 +Created on Jul 11, 2012
     8.6 +
     8.7 +@author: Daniel Kuehlwein
     8.8 +'''
     8.9 +
    8.10 +from cPickle import dump,load
    8.11 +
    8.12 +class Predefined(object):
    8.13 +    '''
    8.14 +    A classifier that uses the Meng-Paulson predictions.
    8.15 +    Only used to easily compare statistics between the old Sledgehammer algorithm and the new machine learning ones.
    8.16 +    '''
    8.17 +
    8.18 +    def __init__(self,mpPredictionFile):
    8.19 +        '''
    8.20 +        Constructor
    8.21 +        '''
    8.22 +        self.predictionFile = mpPredictionFile
    8.23 +    
    8.24 +    def initializeModel(self,_trainData,dicts):
    8.25 +        """
    8.26 +        Load predictions.
    8.27 +        """        
    8.28 +        self.predictions = {}
    8.29 +        IS = open(self.predictionFile,'r')
    8.30 +        for line in IS:
    8.31 +            line = line.split(':')
    8.32 +            name = line[0].strip()
    8.33 +            predId = dicts.get_name_id(name)
    8.34 +            line = line[1].split()
    8.35 +            preds = [dicts.get_name_id(x.strip())for x in line]
    8.36 +            self.predictions[predId] = preds
    8.37 +        IS.close()
    8.38 +        return dicts
    8.39 +    
    8.40 +    def update(self,dataPoint,features,dependencies):
    8.41 +        """
    8.42 +        Updates the Model.
    8.43 +        """
    8.44 +        # No Update needed since we assume that we got all predictions
    8.45 +        pass
    8.46 +            
    8.47 +    
    8.48 +    def predict(self,problemId):
    8.49 +        """
    8.50 +        Return the saved predictions.
    8.51 +        """
    8.52 +        return self.predictions[problemId] 
    8.53 +    
    8.54 +    def save(self,fileName):
    8.55 +        OStream = open(fileName, 'wb')
    8.56 +        dump((self.predictionFile,self.predictions),OStream)        
    8.57 +        OStream.close()
    8.58 +        
    8.59 +    def load(self,fileName):
    8.60 +        OStream = open(fileName, 'rb')
    8.61 +        self.predictionFile,self.predictions = load(OStream)      
    8.62 +        OStream.close()
    8.63 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py	Mon Nov 26 12:04:32 2012 +0100
     9.3 @@ -0,0 +1,79 @@
     9.4 +'''
     9.5 +All functions to read the Isabelle output.
     9.6 +
     9.7 +Created on July 9, 2012
     9.8 +
     9.9 +@author: Daniel Kuehlwein
    9.10 +'''
    9.11 +
    9.12 +import sys,logging
    9.13 +
    9.14 +def create_feature_dict(nameIdDict,idNameDict,maxNameId,featureIdDict,maxFeatureId,inputFile):
    9.15 +    logger = logging.getLogger('create_feature_dict')    
    9.16 +    featureDict = {}
    9.17 +    IS = open(inputFile,'r') 
    9.18 +    for line in IS:
    9.19 +        line = line.split(':')
    9.20 +        name = line[0]        
    9.21 +        # Name Id
    9.22 +        if nameIdDict.has_key(name):
    9.23 +            logger.warning('%s appears twice in the feature file. Aborting.',name)
    9.24 +            sys.exit(-1)
    9.25 +        else:
    9.26 +            nameIdDict[name] = maxNameId
    9.27 +            idNameDict[maxNameId] = name
    9.28 +            nameId = maxNameId
    9.29 +            maxNameId += 1            
    9.30 +        # Feature Ids
    9.31 +        featureNames = [f.strip() for f in line[1].split()]             
    9.32 +        for fn in featureNames:
    9.33 +            if not featureIdDict.has_key(fn):
    9.34 +                featureIdDict[fn] = maxFeatureId
    9.35 +                maxFeatureId += 1
    9.36 +        featureIds = [featureIdDict[fn] for fn in featureNames]
    9.37 +        # Store results
    9.38 +        featureDict[nameId] = featureIds
    9.39 +    IS.close()
    9.40 +    return featureDict,maxNameId,maxFeatureId
    9.41 +     
    9.42 +def create_dependencies_dict(nameIdDict,inputFile):
    9.43 +    logger = logging.getLogger('create_dependencies_dict')
    9.44 +    dependenciesDict = {}
    9.45 +    IS = open(inputFile,'r')
    9.46 +    for line in IS:
    9.47 +        line = line.split(':')
    9.48 +        name = line[0]        
    9.49 +        # Name Id
    9.50 +        if not nameIdDict.has_key(name):
    9.51 +            logger.warning('%s is missing in nameIdDict. Aborting.',name)
    9.52 +            sys.exit(-1)
    9.53 +
    9.54 +        nameId = nameIdDict[name]
    9.55 +        dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()]             
    9.56 +        # Store results, add p proves p
    9.57 +        dependenciesDict[nameId] = [nameId] + dependenciesIds
    9.58 +    IS.close()
    9.59 +    return dependenciesDict
    9.60 +
    9.61 +def create_accessible_dict(nameIdDict,idNameDict,maxNameId,inputFile):
    9.62 +    logger = logging.getLogger('create_accessible_dict')
    9.63 +    accessibleDict = {}
    9.64 +    IS = open(inputFile,'r')
    9.65 +    for line in IS:
    9.66 +        line = line.split(':')
    9.67 +        name = line[0]     
    9.68 +        # Name Id
    9.69 +        if not nameIdDict.has_key(name):
    9.70 +            logger.warning('%s is missing in nameIdDict. Adding it as theory.',name)
    9.71 +            nameIdDict[name] = maxNameId
    9.72 +            idNameDict[maxNameId] = name
    9.73 +            nameId = maxNameId
    9.74 +            maxNameId += 1  
    9.75 +        else:
    9.76 +            nameId = nameIdDict[name]
    9.77 +        accessibleStrings = line[1].split()
    9.78 +        accessibleDict[nameId] = [nameIdDict[a.strip()] for a in accessibleStrings]
    9.79 +    IS.close()
    9.80 +    return accessibleDict,maxNameId
    9.81 +        
    9.82 +    
    9.83 \ No newline at end of file
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/snow.py	Mon Nov 26 12:04:32 2012 +0100
    10.3 @@ -0,0 +1,97 @@
    10.4 +'''
    10.5 +THIS FILE IS NOT UP TO DATE!
    10.6 +NEEDS SOME FIXING BEFORE IT WILL WORK WITH THE MAIN ALGORITHM
    10.7 +
    10.8 +Created on Jul 12, 2012
    10.9 +
   10.10 +@author: daniel
   10.11 +'''
   10.12 +
   10.13 +import logging,shlex,subprocess,string
   10.14 +from cPickle import load,dump
   10.15 +
   10.16 +class SNoW(object):
   10.17 +    '''
   10.18 +    Calls the SNoW framework.
   10.19 +    '''
   10.20 +
   10.21 +    def __init__(self):
   10.22 +        '''
   10.23 +        Constructor
   10.24 +        '''
   10.25 +        self.logger = logging.getLogger('SNoW')
   10.26 +        self.SNoWTrainFile = '../tmp/snow.train'
   10.27 +        self.SNoWTestFile = '../snow.test'  
   10.28 +        self.SNoWNetFile = '../tmp/snow.net' 
   10.29 +    
   10.30 +    def initializeModel(self,trainData,dicts):
   10.31 +        """
   10.32 +        Build basic model from training data.
   10.33 +        """     
   10.34 +        # Prepare input files
   10.35 +        self.logger.debug('Creating IO Files')
   10.36 +        OS = open(self.SNoWTrainFile,'w')
   10.37 +        for nameId in trainData:
   10.38 +            features = [f+dicts.maxNameId for f in dicts.featureDict[nameId]]
   10.39 +            features = map(str,features)
   10.40 +            featureString = string.join(features,',')
   10.41 +            dependencies = dicts.dependenciesDict[nameId]
   10.42 +            dependencies = map(str,dependencies)
   10.43 +            dependenciesString = string.join(dependencies,',')
   10.44 +            snowString = string.join([featureString,dependenciesString],',')+':\n' 
   10.45 +            OS.write(snowString)
   10.46 +        OS.close()
   10.47 +
   10.48 +        # Build Model
   10.49 +        self.logger.debug('Building Model START.')
   10.50 +        snowTrainCommand = '../bin/snow -train -M+ -I %s -F %s -g- -B :0-%s' % (self.SNoWTrainFile,self.SNoWNetFile,dicts.maxNameId-1)    
   10.51 +        args = shlex.split(snowTrainCommand)
   10.52 +        p = subprocess.Popen(args,stdout=subprocess.PIPE,stderr=subprocess.STDOUT)    
   10.53 +        p.wait()
   10.54 +        self.logger.debug('Building Model END.')   
   10.55 +
   10.56 +    
   10.57 +    def update(self,dataPoint,features,dependencies,dicts):
   10.58 +        """
   10.59 +        Updates the Model.
   10.60 +        THIS IS NOT WORKING ATM< BUT WE DONT CARE
   10.61 +        """        
   10.62 +        self.logger.debug('Updating Model START') 
   10.63 +        trainData = dicts.featureDict.keys()       
   10.64 +        self.initializeModel(trainData,dicts)
   10.65 +        self.logger.debug('Updating Model END')
   10.66 +            
   10.67 +    
   10.68 +    def predict(self,features,accessibles,dicts):
   10.69 +        logger = logging.getLogger('predict_SNoW')
   10.70 +         
   10.71 +        OS = open(self.SNoWTestFile,'w')
   10.72 +        features = map(str,features)
   10.73 +        featureString = string.join(features, ',')
   10.74 +        snowString = featureString+':'
   10.75 +        OS.write(snowString)
   10.76 +        OS.close() 
   10.77 +        
   10.78 +        snowTestCommand = '../bin/snow -test -I %s -F %s -o allboth' % (self.SNoWTestFile,self.SNoWNetFile)
   10.79 +        args = shlex.split(snowTestCommand)
   10.80 +        p = subprocess.Popen(args,stdout=subprocess.PIPE,stderr=subprocess.STDOUT)    
   10.81 +        (lines, _stderrdata) = p.communicate()
   10.82 +        logger.debug('SNoW finished.')
   10.83 +        lines = lines.split('\n')    
   10.84 +        assert lines[9].startswith('Example ')
   10.85 +        assert lines[-4] == ''
   10.86 +        predictionsCon = []    
   10.87 +        for line in lines[10:-4]:
   10.88 +            premiseId = int(line.split()[0][:-1])
   10.89 +            predictionsCon.append(premiseId)
   10.90 +        return predictionsCon
   10.91 +    
   10.92 +    def save(self,fileName):
   10.93 +        OStream = open(fileName, 'wb')
   10.94 +        dump(self.counts,OStream)        
   10.95 +        OStream.close()
   10.96 +        
   10.97 +    def load(self,fileName):
   10.98 +        OStream = open(fileName, 'rb')
   10.99 +        self.counts = load(OStream)      
  10.100 +        OStream.close()
  10.101 \ No newline at end of file
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py	Mon Nov 26 12:04:32 2012 +0100
    11.3 @@ -0,0 +1,124 @@
    11.4 +'''
    11.5 +Created on Jul 9, 2012
    11.6 +
    11.7 +@author: Daniel Kuehlwein
    11.8 +'''
    11.9 +
   11.10 +import logging,string
   11.11 +from cPickle import load,dump
   11.12 +
   11.13 +class Statistics(object):
   11.14 +    '''
   11.15 +    Class for all the statistics
   11.16 +    '''
   11.17 +
   11.18 +    def __init__(self,cutOff=500):
   11.19 +        '''
   11.20 +        Constructor
   11.21 +        '''
   11.22 +        self.logger = logging.getLogger('Statistics')
   11.23 +        self.avgAUC = 0.0
   11.24 +        self.avgRecall100 = 0.0
   11.25 +        self.avgAvailable = 0.0
   11.26 +        self.avgDepNr = 0.0
   11.27 +        self.problems = 0.0
   11.28 +        self.cutOff = cutOff
   11.29 +        self.recallData = [0]*cutOff
   11.30 +        self.recall100Data = [0]*cutOff
   11.31 +        self.aucData = []
   11.32 +        
   11.33 +    def update(self,predictions,dependencies):
   11.34 +        """
   11.35 +        Evaluates AUC, dependencies, recall100 and number of available premises of a prediction.
   11.36 +        """
   11.37 +
   11.38 +        available = len(predictions)
   11.39 +        predictions = predictions[:self.cutOff]
   11.40 +        dependencies = set(dependencies)
   11.41 +        depNr = len(dependencies)
   11.42 +        aucSum = 0.    
   11.43 +        posResults = 0.        
   11.44 +        positives, negatives = 0, 0
   11.45 +        recall100 = 0.0
   11.46 +        badPreds = []
   11.47 +        depsFound = []
   11.48 +        for index,pId in enumerate(predictions):
   11.49 +            if pId in dependencies:        #positive
   11.50 +                posResults+=1
   11.51 +                positives+=1
   11.52 +                recall100 = index+1
   11.53 +                depsFound.append(pId)
   11.54 +                if index > 200:
   11.55 +                    badPreds.append(pId)
   11.56 +            else:            
   11.57 +                aucSum += posResults
   11.58 +                negatives+=1
   11.59 +            # Update Recall and Recall100 stats
   11.60 +            if depNr == positives:
   11.61 +                self.recall100Data[index] += 1
   11.62 +            if depNr == 0:
   11.63 +                self.recallData[index] += 1
   11.64 +            else:
   11.65 +                self.recallData[index] += float(positives)/depNr
   11.66 +    
   11.67 +        if not depNr == positives:
   11.68 +            depsFound = set(depsFound)
   11.69 +            missing = []
   11.70 +            for dep in dependencies:
   11.71 +                if not dep in depsFound:
   11.72 +                    missing.append(dep)
   11.73 +                    badPreds.append(dep)
   11.74 +                    recall100 = len(predictions)+1
   11.75 +                    positives+=1
   11.76 +            self.logger.debug('Dependencies missing for %s in accessibles! Estimating Statistics.',\
   11.77 +                              string.join([str(dep) for dep in missing],','))
   11.78 +    
   11.79 +        if positives == 0 or negatives == 0:
   11.80 +            auc = 1.0
   11.81 +        else:            
   11.82 +            auc = aucSum/(negatives*positives)
   11.83 +        
   11.84 +        self.aucData.append(auc)
   11.85 +        self.avgAUC += auc
   11.86 +        self.avgRecall100 += recall100
   11.87 +        self.problems += 1
   11.88 +        self.badPreds = badPreds
   11.89 +        self.avgAvailable += available 
   11.90 +        self.avgDepNr += depNr
   11.91 +        self.logger.info('AUC: %s \t Needed: %s \t Recall100: %s \t Available: %s \t cutOff:%s',\
   11.92 +                          round(100*auc,2),depNr,recall100,available,self.cutOff)        
   11.93 +        
   11.94 +    def printAvg(self):
   11.95 +        self.logger.info('Average results:')
   11.96 +        self.logger.info('avgAUC: %s \t avgDepNr: %s \t avgRecall100: %s \t cutOff:%s', \
   11.97 +                         round(100*self.avgAUC/self.problems,2),round(self.avgDepNr/self.problems,2),self.avgRecall100/self.problems,self.cutOff)
   11.98 +
   11.99 +        try:
  11.100 +            from matplotlib.pyplot import plot,figure,show,xlabel,ylabel,axis,hist
  11.101 +            avgRecall = [float(x)/self.problems for x in self.recallData]
  11.102 +            figure('Recall')
  11.103 +            plot(range(self.cutOff),avgRecall)
  11.104 +            ylabel('Average Recall')
  11.105 +            xlabel('Highest ranked premises')
  11.106 +            axis([0,self.cutOff,0.0,1.0])
  11.107 +            figure('100%Recall')
  11.108 +            plot(range(self.cutOff),self.recall100Data)
  11.109 +            ylabel('100%Recall')
  11.110 +            xlabel('Highest ranked premises')
  11.111 +            axis([0,self.cutOff,0,self.problems])
  11.112 +            figure('AUC Histogram')
  11.113 +            hist(self.aucData,bins=100)
  11.114 +            ylabel('Problems')
  11.115 +            xlabel('AUC')
  11.116 +            show()
  11.117 +        except:
  11.118 +            self.logger.warning('Matplotlib module missing. Skipping graphs.')
  11.119 +    
  11.120 +    def save(self,fileName):       
  11.121 +        oStream = open(fileName, 'wb')
  11.122 +        dump((self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData),oStream)
  11.123 +        oStream.close()
  11.124 +    def load(self,fileName):
  11.125 +        iStream = open(fileName, 'rb')        
  11.126 +        self.avgAUC,self.avgRecall100,self.avgAvailable,self.avgDepNr,self.problems,self.cutOff,self.recallData,self.recall100Data,self.aucData = load(iStream)
  11.127 +        iStream.close()
  11.128 \ No newline at end of file
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 26 11:46:19 2012 +0100
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Nov 26 12:04:32 2012 +0100
    12.3 @@ -101,7 +101,8 @@
    12.4  val relearn_isarN = "relearn_isar"
    12.5  val relearn_atpN = "relearn_atp"
    12.6  
    12.7 -fun mash_home () = getenv "MASH_HOME"
    12.8 +fun is_mash_enabled () = (getenv "MASH" = "yes")
    12.9 +fun mash_home () = getenv "ISABELLE_SLEDGEHAMMER_MASH"
   12.10  fun mash_model_dir () =
   12.11    getenv "ISABELLE_HOME_USER" ^ "/mash"
   12.12    |> tap (Isabelle_System.mkdir o Path.explode)
   12.13 @@ -446,9 +447,8 @@
   12.14        " --numberOfPredictions " ^ string_of_int max_suggs ^
   12.15        (if save then " --saveModel" else "")
   12.16      val command =
   12.17 -      mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
   12.18 +      mash_home () ^ "/src/mash.py --quiet --outputDir " ^ mash_model_dir () ^
   12.19        " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
   12.20 -
   12.21        |> tap (fn _ => trace_msg ctxt (fn () =>
   12.22               case try File.read (Path.explode err_file) of
   12.23                 NONE => "Done"
   12.24 @@ -623,7 +623,7 @@
   12.25  
   12.26  end
   12.27  
   12.28 -fun mash_could_suggest_facts () = mash_home () <> ""
   12.29 +fun mash_could_suggest_facts () = is_mash_enabled ()
   12.30  fun mash_can_suggest_facts ctxt = not (Graph.is_empty (#fact_G (mash_get ctxt)))
   12.31  
   12.32  fun num_keys keys = Graph.Keys.fold (K (Integer.add 1)) keys 0