# -*- Python -*-

# Configuration file for the 'lit' test runner.

import os
import sys
import re
import platform

import lit.util
import lit.formats

# name: The name of this test suite.
config.name = 'Dafny'

config.test_format = lit.formats.ShTest(execute_external=False)

# suffixes: A list of file extensions to treat as test files. This is overriden
# by individual lit.local.cfg files in the test subdirectories.
config.suffixes = ['.dfy']

# excludes: A list of directories to exclude from the testsuite. The 'Inputs'
# subdirectories contain auxiliary inputs for various tests in their parent
# directories.
config.excludes = ['Inputs']

# test_source_root: The root path where tests are located.
config.test_source_root = os.path.dirname(os.path.abspath(__file__))

# test_exec_root: The root path where tests should be run.
config.test_exec_root = config.test_source_root

# Propagate 'HOME' through the environment.
if 'HOME' in os.environ:
    config.environment['HOME'] = os.environ['HOME']

# Propagate 'INCLUDE' through the environment.
if 'INCLUDE' in os.environ:
    config.environment['INCLUDE'] = os.environ['INCLUDE']

# Propagate 'LIB' through the environment.
if 'LIB' in os.environ:
    config.environment['LIB'] = os.environ['LIB']

# Propagate the temp directory. Windows requires this because it uses \Windows\
# if none of these are present.
if 'TMP' in os.environ:
    config.environment['TMP'] = os.environ['TMP']
if 'TEMP' in os.environ:
    config.environment['TEMP'] = os.environ['TEMP']

# Propagate PYTHON_EXECUTABLE into the environment
config.environment['PYTHON_EXECUTABLE'] = getattr(config, 'python_executable', '')

# Check that the object root is known.
if config.test_exec_root is None:
    lit_config.fatal('Could not determine execution root for tests!')

"""
   Function for quoting filepaths
   so that if they contain spaces
   lit's shell interpreter will
   treat the path as a single argument
"""
def quotePath(path):
    if ' ' in path:
        return '"{path}"'.format(path=path)
    else:
        return path

### Add Dafny specific substitutions

# Find Dafny.exe
up = os.path.dirname
repositoryRoot = up(
                     up( os.path.abspath(__file__) )
                   )
lit_config.note('Repository root is {}'.format(repositoryRoot))

binaryDir = os.path.join( repositoryRoot, 'Binaries')
dafnyExecutable = os.path.join( binaryDir, 'Dafny.exe')
serverExecutable = os.path.join( binaryDir, 'DafnyServer.exe')

if not os.path.exists(dafnyExecutable):
    lit_config.fatal('Could not find Dafny.exe at {}'.format(dafnyExecutable))

if not os.path.exists(serverExecutable):
    lit_config.warning('Could not find DafnyServer.exe at {}'.format(serverExecutable))
else:
    config.suffixes.append('.transcript')

dafnyExecutable = quotePath(dafnyExecutable)

if os.name == 'posix':
    dafnyExecutable = 'mono ' + dafnyExecutable
    serverExecutable = 'mono ' + serverExecutable
    if lit.util.which('mono') == None:
        lit_config.fatal('Cannot find mono. Make sure it is your PATH')

# Expected output does not contain logo
dafnyExecutable += ' -nologo -countVerificationErrors:0'

# We do not want absolute or relative paths in error messages, just the basename of the file
dafnyExecutable += ' -useBaseNameForFileName'

# Allow user to provide extra arguments to Dafny
dafnyParams = lit_config.params.get('dafny_params','')
if len(dafnyParams) > 0:
    dafnyExecutable = dafnyExecutable + ' ' + dafnyParams

# Inform user what executable is being used
lit_config.note('Using Dafny: {}\n'.format(dafnyExecutable))

config.substitutions.append( ('%dafny', dafnyExecutable) )
config.substitutions.append( ('%server', serverExecutable) )

# Sanity check: Check solver executable is available
# FIXME: Should this check be removed entirely?
if os.name != 'nt':
    solvers = ['z3.exe','cvc4.exe']
    solverFound = False
    for solver in solvers:
        if os.path.exists( os.path.join(binaryDir, solver)):
            solverFound = True

    if not solverFound:
        lit_config.fatal('Could not find solver in "{binaryDir}". Tried looking for {solvers}'.format(
                           binaryDir=binaryDir,
                           solvers=solvers
                           )
                        )
else:
    lit_config.warning('Skipping solver sanity check on Windows')

# Add diff tool substitution
commonDiffFlags=' --unified=3 --strip-trailing-cr'
diffExecutable = None
if os.name == 'posix':
    diffExecutable = 'diff' + commonDiffFlags
elif os.name == 'nt':
    pydiff = quotePath( os.path.join(config.test_source_root, 'pydiff.py') )
    diffExecutable = sys.executable + ' ' + pydiff + commonDiffFlags
else:
    lit_config.fatal('Unsupported platform')
lit_config.note("Using diff tool '{}'".format(diffExecutable))

config.substitutions.append( ('%diff', diffExecutable ))

# Detect the OutputCheck tool
outputCheckPath = lit.util.which('OutputCheck')
if outputCheckPath == None:
    lit_config.fatal('The OutputCheck tool is not in your PATH. Please install it.')

config.substitutions.append( ('%OutputCheck', outputCheckPath + ' --dump-file-to-check') )