#! /usr/bin/env python

# Copyright (c) 2012 United States Government as represented by
# the National Aeronautics and Space Administration.  No copyright
# is claimed in the United States under Title 17, U.S.Code. All Other
# Rights Reserved.
#
# The software in this package has been released as open-source software
# under the NASA Open Source Agreement.  See the accompanying file
# NASA_Open_Source_Agreement.pdf for a full description of the terms.


'''hypfind 1.2 -- shell command for submitting Hypatheon queries

Use hypfind to run queries against Hypatheon databases.
Results returned on standard output include entity names and
corresponding library, theory names (where applicable).

Usage: hypfind [-anpqusvh] [term ...]

Options:
  -a   --all        Don't filter out nonexistent paths from result.
  -n   --name       Return entity names only.
  -p   --path       Return non-prelude, absolute paths only.
  -q   --quote      Add quotes around results returned.
  -u   --unique     Remove duplicate lines from result.
  -s   --status     Print database status and exit.
  -v   --version    Print the version number and exit.
  -h   --help       Print this message.

Arguments:
  term ...          Search terms for submission to Hypatheon server.
  'name ...; refs ...; path ...; decl ...'      Fully qualified form.
'''

import os, sys, time

HYPATHEON = os.environ.get('HYPATHEON', '')
if not HYPATHEON:
        if sys.argv[0]:
            HYPATHEON = os.path.abspath(sys.argv[0] + '/../..')
            os.environ['HYPATHEON'] = HYPATHEON
        else:
            print 'The Hypatheon base directory was not found.'
            print 'Try setting the HYPATHEON environment variable.'
            sys.exit(1)

for dir in ('lib',):
    sys.path.insert(0, os.path.join(HYPATHEON, dir))

import getopt

from StringIO import StringIO
from traceback import print_exc

from app_globals import *

app_state['exec_mode'] = 'Shell-script'


def usage(code, msg=''):
    if code == 1: channel = sys.stdout
    else:         channel = sys.stderr
    print >> channel, __doc__  # docstring()
    if msg: print >> channel, msg
    sys.exit(code)

options = {}

def main():
    try:
        opts, args = getopt.getopt(
            sys.argv[1:],
            'anpqusvh',
            ['all', 'name', 'path', 'quote', 'unique',
             'status', 'help', 'version'])
    except getopt.GetoptError, msg:
        usage(2, msg)

    for opt, arg in opts:
        if opt in ('-h', '--help'):
            usage(1)
        elif opt in ('-v', '--version'):
            print 'hypfind (Hypatheon) %s' % app_version
            sys.exit(0)
        elif opt in ('-q', '--quote'):
            options['quote'] = 1
        elif opt in ('-u', '--unique'):
            options['unique'] = 1
        elif opt in ('-a', '--all'):
            options['all_paths'] = 1
        elif opt in ('-p', '--path'):
            options['abs_paths'] = 1
        elif opt in ('-n', '--name'):
            options['name_only'] = 1
        elif opt in ('-s', '--status'):
            from db_connect import getCollectionsStatus, open_db_connection
            try:
                open_db_connection()           # opens all databases
            except DatabaseError, e:
                pass           # old database files found; ignore for now
            show_status(getCollectionsStatus())
            sys.exit(0)

    if len(args) == 0:
        usage(1)
    query_and_display(args)    # now perform query

def show_status(status):
    ncols = len(status)
    if status:
        col_specs = '    %8s' * ncols
        row_specs = [ '    %-24s%s\n' % (label, col_specs)
                      for label in status_display_types ]
        status_msg = \
            ('Hypatheon database status for %s\n\n' % time.asctime()) + \
            ''.join([ spec % row for spec, row
                      in zip(row_specs, map(tuple, transpose_lists(status))) ])
    else:
        status_msg = 'Hypatheon Server is not running on %s.'
    print status_msg

def query_and_display(args):
    from db_connect    import query_type, open_db_connection
    from submit_query  import perform_query, rel_to_abs_paths
    from db_operations import get_declaration_name, get_proof_name, get_step_name
    try:
        open_db_connection()           # opens all databases
    except DatabaseError, e:
        pass           # old database files found; ignore for now

    queries = split_and_pad_terms(' '.join(args))
    q_type = query_type(queries)
    query_result = perform_query(queries, q_type)[2]
    if not query_result:            # empty result
        sys.exit(0)
    if q_type[0] == 'step':
        options['name_only'] = 1    # proof steps (cmds) don't have paths

    if 'abs_paths' in options:
        # absolute lib/thy paths will form the result
        if not (os.environ.get('PVSPATH') or
                os.environ.get('PVS_LIBRARY_PATH')):
            print 'PVSPATH and/or PVS_LIBRARY_PATH ' \
                  'is needed to find absolute paths.'
            sys.exit(4)
        query_result = rel_to_abs_paths(query_result)
        paths = [ r[1] for r in query_result
                  if not r[1].startswith('prelude') ]
        if 'all_paths' not in options:
            paths = filter(os.path.exists, paths)
        if not paths:
            sys.exit(0)

    elif 'name_only' not in options:
        # lib@thy paths are to be included as prefixes on each output line
        pairs = [ os.path.split(os.path.splitext(r[1])[0])
                  for r in query_result ]
        if q_type[0] == 'library':
            lib_thy = [ (p[1], '') for p in pairs ]
        else:
            lib_thy = [ (p[0], r[2]) for p, r in zip(pairs, query_result) ]
        max_lib = max([ len(p[0]) for p in lib_thy ])
        max_thy = max([ len(p[1]) for p in lib_thy ])
        lib_thy_format = '%%-%ds @ %%-%ds' % (max_lib, max_thy)
        paths = []
        for lib, thy in lib_thy:
            if thy: paths.append(lib_thy_format % (lib, thy))
            else:   paths.append(lib)

    if 'abs_paths' in options:
        output = sorted(paths)
    else:
        if q_type[0] == 'declaration':  get_fn = get_declaration_name
        elif q_type[0] == 'proof':      get_fn = get_proof_name
        elif q_type[0] == 'step':       get_fn = get_step_name
        else:                           get_fn = lambda n,c: ''
        if q_type[0] == 'module':
            entity_names = [ r[2] for r in query_result ]
        else:
            entity_names = [ get_fn(r[-1], r[4]) for r in query_result ]
        if 'name_only' in options:
            output = sorted(entity_names)
        else:
            output = [ '%s  %s' % (path, name)
                       for name, path in sorted(zip(entity_names, paths)) ]
    if 'unique' in options:
        output = list(set(output))
        output.sort()
    if 'quote' in options:
        output = [ '"%s"' % line for line in output ]
    for line in output:
        try:
            print line
        except UnicodeEncodeError:
            # need to handle non-ASCII characters
            print line.encode('utf-8')


connect_fail_msg = \
'''Connection failure: unable to establish a connection to the Hypatheon
database server.  Check the environment variable settings, then try the
query again.  If problems persist, try the query with the GUI client.
'''

database_error_msg = \
'''Database error: the Hypatheon database server encountered an error
while processing this query.  Check the environment variable settings,
then try the query again.  If problems persist, try the query with
the GUI client.
'''

try:
    exit_code = 0
    main()
except SystemExit:
    pass
except SearchTermError:
    exit_code = 1
    pass
except ConnectionFailure:
    exit_code = 2
    print >> sys.stderr, connect_fail_msg
except DatabaseError:
    exit_code = 3
    print >> sys.stderr, database_error_msg
except:
    exit_code = 10
    trace = StringIO()
    print_exc(10, trace)
    print >> sys.stderr, 'Unhandled exception:'
    print >> sys.stderr, trace.getvalue()

sys.exit(exit_code)
