#!/usr/bin/env python3

function_lookup_table = {
                        "s": 1,
                        "+": 2,
                        "*": 2
                      }

predicate_lookup_table = {
                            "==": 2,
                            "!=": 2,
                            "<<": 2,
                            "<=": 2,
                            ">>": 2,
                            ">=": 2,
                         }

logical_relators = {"and", "or", "-->", "<->"} # Assuming right associativity

unary_operator = {"not"}

quantifiers = ["for-all", "there-exists"]

def indexErrorWrapper(func):
    def inner(string):
        try:
            return func(string)
        except IndexError:
            return (False, '', string)
    return inner

@indexErrorWrapper
def ConstParse(string):
    if string[0] == '0':
        return (True, [string[0]], string[1:])
    else:
        return (False, '', string)

@indexErrorWrapper
def VariableParse(string):
    if string[0].isalpha():
        return (True, [string[0]], string[1:])
    else:
        return (False, '', string)

def ArbitraryFunctionParse(string, lookup_table, identifier_size):
    parsed_function = []
    if string[:identifier_size] in lookup_table:
        degree = lookup_table[string[:identifier_size]]
        parsed_function.append(string[:identifier_size])
        if string[identifier_size] == '(':
            current_string = string[identifier_size + 1:]
            for term in range(degree):
                result, output, rest = TermParse(current_string)
                if not result:
                    return (False, '', string)

                if term != degree - 1:
                    if not rest.startswith(","):
                        return (False, '', string)
                    current_string = rest[1:]

                else:
                    current_string = rest

                parsed_function.append(output)
            if current_string[0] == ")":
                return (True, parsed_function, current_string[1:])
            else:
                return (False, '', string)
        else:
            return (False, '', string)
    else:
        return (False, '', string)

FunctionParse = indexErrorWrapper(lambda string: ArbitraryFunctionParse(string, function_lookup_table, 1))

def orParser(parsers):
    def composedParser(string):
        for parser in parsers:
            result, output, rest = parser(string)
            if result:
                return (result, output, rest)
        return (False, '', string)
    return composedParser

TermParse = orParser([FunctionParse, VariableParse, ConstParse])

PredicateParse = indexErrorWrapper(lambda string: ArbitraryFunctionParse(string, predicate_lookup_table, 2))

def QuantifierParse(string):
    for quantifier in quantifiers:
        if string.startswith(quantifier):
            current_string = string[len(quantifier):]
            if not current_string[0] == "(":
                return (False, '', string)
            current_string = current_string[1:]
            result, output_left, current_string = VariableParse(current_string)
            if not result:
                return (False, '', string)
            if not current_string[0] == ",":
                return (False, '', string)
            current_string = current_string[1:]
            result, output_right, current_string = FormulaParse(current_string)
            if not result:
                return (False, '', string)
            if current_string[0] == ")":
                return (True, [quantifier, output_left, output_right], current_string[1:])
            else:
                return (False, '', string)
    else:
        return (False, '', string)

def UnaryParse(string):
    for unary in unary_operator:
        if string.startswith(unary + " "):
            current_string = string[len(unary) + 1:]
            result, output, current_string = FormulaParse(current_string)
            if result:
                return (True, [unary, output], current_string)
            else:
                return (False, '', string)
    return (False, '', string)

@indexErrorWrapper
def FormulaParse(string):
    preFormula = orParser([UnaryParse, PredicateParse, QuantifierParse])
    result = True
    current_string = string
    parsed_output = []
    result1, output1, current_string1 = preFormula(current_string)
    if result1:
        for logical_relator in logical_relators:
            if current_string1.startswith(" " + logical_relator + " "):
                current_string = current_string1[len(logical_relator)+2:]
                result2, output2, current_string = FormulaParse(current_string)
                if not result2:
                    return (False, '', string)
                else:
                    return (True, [logical_relator, output1, output2], current_string)
        return (result1, output1, current_string1)
    else:
        return (False, '', string)

def eolParse(string):
    if string != "":
        return (False, "", string)
    else:
        return (True, "", "")

def takeFirst(parsers):
    def combinedParser(string):
        assert len(parsers) > 0, "At least one parser should be provided"
        result, output, current_string = parsers[0](string)
        if result:
            for parser in parsers[1:]:
                result,_,current_string = parser(current_string)
                if not result:
                    return (False, "", string)
            return (True, output, current_string)
        else:
            return (False, "", string)
    return combinedParser

AxiomParse = indexErrorWrapper(takeFirst([FormulaParse, eolParse]))
