#!/usr/bin/env python3

'''
Try parsing all files in given problem lists, and print out the ones that failed.
'''

import os
import sys
import multiprocessing as mp
import time
import datetime
import traceback
import queue
import ctypes

from collections import deque

from stringfuzz.constants import SMT_20_STRING, SMT_25_STRING, LANGUAGES
from stringfuzz.scanner import scan, ScanningError
from stringfuzz.parser import parse_file, parse_tokens, ParsingError
from stringfuzz.generator import generate, NotSupported

# constants
DEFAULT_NUM_WORKERS = 8
BATCH_SIZE          = 50
MAX_HISTORY         = 500
ESC                 = '\033'
BACK_ONE_LINE       = ESC + '[1A'
ERASE_LINE          = ESC + '[2K'
FRAME_DURATION      = 0.05 # in seconds
POISON_PILL         = None

SMT_25_PATTERNS = [
    'dumpCVC4',
    'smt25',
    '/cvc4/',
    'kaluza25',
]

# globals
io_lock = mp.Lock()

# helpers
def reset_cursor():
    return BACK_ONE_LINE + ERASE_LINE

def now():
    return datetime.datetime.now()

def sec2minsec(seconds):
    return (seconds // 60, seconds % 60)

def show_failure(message):
    with io_lock:
        print(reset_cursor() + message + '\n')

def show_progress(*args):
    with io_lock:
        print(*args, file=sys.stderr)

def is_smt25(file_path):
    return any(pattern in file_path for pattern in SMT_25_PATTERNS)

# functions
def consumer(q, num_done, i, crash):

    # run forever
    while True:

        # try to get a task
        batch = q.get()

        # stop running if got poison pill
        if batch is POISON_PILL:
            break

        # go through problem batch
        for problem_path in batch:

            try:
                parse_problem(problem_path)

            # on uncaught exceptions
            except Exception as e:

                # print stack trace
                with io_lock:
                    traceback.print_exc()

                # signal crash to parent process
                with crash.get_lock():
                    crash.value = 1

            # signal completion
            with num_done.get_lock():
                num_done.value += 1

def parse_problem(input_path):

    # get start time
    start_time = now()

    # figure out input language
    if is_smt25(input_path):
        language = SMT_25_STRING
    else:
        language = SMT_20_STRING

    # read in file
    with open(input_path, 'r') as file:
        text = file.read()

    # try to scan
    try:
        tokens = scan(text, language)
    except ScanningError as e:
        show_failure('{language:<5} failed scanning {problem}\n{error}'.format(
            path     = input_path,
            language = language,
            error    = e
        ))

    # if scanned, try to parse
    else:
        try:
            expressions = parse_tokens(tokens, language, text)
        except ParsingError as e:
            show_failure('{language:<5} failed parsing {path}\n{error}'.format(
                path     = input_path,
                language = language,
                error    = e
            ))

        # if parsed, try to generate
        else:
            for output_language in [SMT_25_STRING, SMT_20_STRING]:
                try:
                    translated = generate(expressions, output_language)
                except NotSupported as e:
                    show_failure('{language:<5} failed generating {path}\n{error}'.format(
                        path     = input_path,
                        language = language,
                        error    = e
                    ))

    # measure run time
    run_time = now() - start_time

def usage():
    print('Usage', sys.argv[0], 'problem_list [problem_list [...]]', file=sys.stderr)

def add_record(history, last_sample, current_sample):

    # create new record
    new_record = current_sample - last_sample

    # discard last record if needed
    if len(history) >= MAX_HISTORY:
        history.popleft()

    history.append(new_record)

def print_status(history, done_so_far, num_problems):

    # get rate
    history_size     = len(history)
    history_problems = sum(history)
    history_time     = history_size * FRAME_DURATION

    if history_problems > 0:
        sec_per_problem = history_time / history_problems
    else:
        sec_per_problem = FRAME_DURATION

    # calculate progress
    num_left           = num_problems - done_so_far
    percent_done       = (float(done_so_far) / float(num_problems)) * 100.0
    time_left          = int(float(sec_per_problem) * float(num_left))
    min_left, sec_left = sec2minsec(time_left)

    # format progress
    seconds_progress = '{:.0f}s'.format(sec_left)
    minutes_progress = '{:.0f}m'.format(min_left)
    time_progress    = seconds_progress

    if min_left > 0:
        time_progress = minutes_progress + ' ' + time_progress

    progress = '{} / {} ({:.2f}%) done; {} left ({:.6f} s per)'.format(
        done_so_far,
        num_problems,
        percent_done,
        time_progress,
        sec_per_problem
    )

    # show progress
    show_progress(reset_cursor() + progress)

def main():

    # record start time
    start_time = now()

    # get args
    list_paths = sys.argv[1:]

    # check args
    if len(list_paths) < 1:
        usage()
        exit(1)

    # read input lists
    problems = []
    for list_path in list_paths:
        with open(list_path, 'r') as list_file:
            problems += [line.strip() for line in list_file.readlines()]
    num_problems = len(problems)

    # create shared values
    num_done = mp.Value(ctypes.c_ulong, 0)
    crash    = mp.Value(ctypes.c_bool, 0)
    q        = mp.Queue()

    # populate queue
    for i in range(0, num_problems, BATCH_SIZE):
        batch = problems[i:i + BATCH_SIZE]
        q.put_nowait(batch)

    # calculate number of workers
    num_workers = os.cpu_count()
    if num_workers is None:
        num_workers = DEFAULT_NUM_WORKERS

    # add poison pills to the end of the queue
    for i in range(0, num_workers):
        q.put_nowait(POISON_PILL)

    # create workers
    workers = [mp.Process(target=consumer, args=(q, num_done, i, crash)) for i in range(num_workers)]

    # start workers
    for worker in workers:
        worker.start()

    # print newline to start update line
    show_progress('')

    # set up bookkeeping
    last_sample = num_done.value
    history     = deque()

    # run until done
    while num_done.value < num_problems:

        # sample number of done problems
        current_sample = num_done.value
        add_record(history, last_sample, current_sample)

        # print status
        print_status(history, current_sample, num_problems)

        # update bookkeeping
        last_sample = current_sample

        # sleep for a frame
        time.sleep(FRAME_DURATION)

        # check for crash condition
        if crash.value != 0:

            # terminate workers
            for worker in workers:
                worker.terminate()

            exit(1)

    # wait for the workers to finish
    for worker in workers:
        worker.join()

    # print final results
    end_time             = now()
    run_time             = end_time - start_time
    min_total, sec_total = sec2minsec(run_time.seconds)
    sec_per_problem      = run_time.seconds / num_done.value
    show_progress('finished in {}m {}s, {:.4f}s per run'.format(min_total, sec_total, sec_per_problem))

if __name__ == '__main__':
    main()
