#!/usr/bin/env python3
#
# CLI interface wrapper for libMATA

import argparse
import os
import subprocess
import sys
import tempfile


MATA_CODE_NAME = 'mata-code'
GDB_COMMAND = os.path.expandvars('$GDB')

# operations of the CLI, mapping name to the number of expected arguments and a
# corresponding operation in libMATA
CLI_OPERATIONS_DEF = {
    'load' : {'arity': 1},
    'isect': {'arity': 2, 'mata-name': 'isect'},
    'union': {'arity': 2, 'mata-name': 'union'},
    'empty': {'arity': 1, 'mata-name': 'is_empty'},
    'univ' : {'arity': 1, 'mata-name': 'is_univ'},
    'incl' : {'arity': 2, 'mata-name': 'is_incl'},
    'eq'   : {'arity': 2, 'mata-name': 'is_equiv'}
}

CLI_OPERATIONS = CLI_OPERATIONS_DEF.keys()

###########################################
def find_mata_path():
    '''find_mata_path() -> string

Finds the path to the mata-code executable.
'''
    dirname, filename = os.path.split(sys.argv[0])
    mata_code_dirname = os.path.join(dirname, '..' , 'build', 'cli')
    mata_path = os.path.join(mata_code_dirname, MATA_CODE_NAME)
    os.path.isfile(mata_path)
    return mata_path


###########################################
def get_mata_version():
    '''get_mata_version() -> string

Retrieves the version of libMATA.
'''
    result = ''
    result += call_mata_code(['-v'])
    return result


###########################################
def is_binary_op(operation):
    '''is_binary_op(operation) -> bool

Checks whether the passed string denotes a binary operation
'''
    assert operation in CLI_OPERATIONS_DEF
    return True if CLI_OPERATIONS_DEF[operation]['arity'] == 2 else False


###########################################
def call_mata_code(params=None, input=None, gdb=False, debug=1):
    '''call_mata_code([params], input=None, gdb=False, debug=1) -> str

Calls mata-code with the given 'params' and 'input'.  If 'gdb' is provided,
then mata-code is run within $GDB.  The 'debug' flag specifies the verbosity.
Input is fed into mata-code on STDIN.  The string from STDOUT is returned.
'''
    command = [MATA_PATH, '-d', str(debug)]
    if params:
        command += params

    if not gdb:
        compl_proc = subprocess.run(
            command,
            input=input,
            stdout=subprocess.PIPE,
            universal_newlines=True,
            check=True)
        return compl_proc.stdout
    else:
        assert gdb
        tmp = tempfile.NamedTemporaryFile(mode='w+t',delete=False)
        tmp.write(input)
        tmp.close()
        command = command + [tmp.name]
        command = [GDB_COMMAND, '--args'] + command
        os.execvp(GDB_COMMAND, [GDB_COMMAND] + command)
        # exec removes the python script


###########################################
def create_code_str(cmds):
    '''create_code_str(cmds) -> string

Creates a @CODE string in the .vtf format using 'cmds' as the commands to execute.
'''
    header = \
        '# Generated by libMATA CLI interface\n' \
        '\n' \
        '@CODE\n'
    return header + cmds


###########################################
def errprint(str):
    '''errprint(str) -> ()

Prints onto stderr.
'''
    print('error: ' + str, file=sys.stderr)


###########################################
def check_num_params(expected, provided):
    '''check_num_params(expected, provided) -> ()

Raises an exception if 'expected' != 'provided'.
'''
    if expected != provided:
        raise Exception('Number of provided parameters (' + str(provided) + \
            ') does not match the number of expected (' + str(expected) + ')')

###########################################
def run_main(args):
    '''run_main(args) -> ()

Runs the main program according to the arguments obtained from the parser.
'''
    # check the number of arguments is OK from below (i.e. that at least the
    # number is not less than should be
    assert args.oper in CLI_OPERATIONS_DEF
    check_num_params(CLI_OPERATIONS_DEF[args.oper]['arity'], len(args.inputs))

    # load the arguments
    cmds = ''
    cmds += 'a1 = (load_file "{0}")\n'.format(args.inputs[0])
    if (is_binary_op(args.oper)):
        cmds += 'a2 = (load_file "{0}")\n'.format(args.inputs[1])

    # according to the operation
    if args.oper == 'load':
        cmds += 'res = a1\n'
    elif not is_binary_op(args.oper):
        cmds += 'res = (' + CLI_OPERATIONS_DEF[args.oper]['mata-name'] + ' a1)\n'
    else:
        cmds += 'res = (' + CLI_OPERATIONS_DEF[args.oper]['mata-name'] + ' a1 a2)\n'

    assert cmds
    cmds += '(print res)\n';
    code_str = create_code_str(cmds)

    if not args.file:
        res = call_mata_code(input=code_str, gdb=args.gdb, debug=args.debug)
        print(res)
    else:
        print(code_str)


###########################################
if __name__ == '__main__':
    try:
        MATA_PATH = find_mata_path()
        mata_version_str = get_mata_version()

        parser = argparse.ArgumentParser(description='User interface to libMATA')
        parser.add_argument('oper', metavar='op', choices=CLI_OPERATIONS,
            help='operation to be performed (one of {' + ', '.join(CLI_OPERATIONS) + '})')
        parser.add_argument('inputs', metavar='AUT', nargs='*',
            help='files with input automata in the .vtf format')

        parser.add_argument('-v', '--version', action='version', version=mata_version_str)
        parser.add_argument('-f', '--file', action='store_true',
            help='only output a @CODE file in the ' + '.vtf format, do not run ' +
            MATA_CODE_NAME)
        parser.add_argument('--gdb', action='store_true',
            help='run ' + MATA_CODE_NAME + ' in $GDB')
        parser.add_argument('-d', '--debug', type=int, metavar='N', default=1,
            help='set debug verbosity to N (default: %(default)s)')

        args = parser.parse_args()

        run_main(args)
    except Exception as ex:
        errprint(str(ex))
