"""

Name: sml - Simple Modal Logic Lib.

Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.

Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>

"""

import re

def main():

    # edit your formulae here

    p = Variable(["p"])

    q = Variable(["q"])

    r = Variable(["r"])

    formula1 = Imp([Eq([p, q]), r])

    formula2 = Not([Or([p, q])])

    formula3 = Not([Not([p])])

    formula = formula1 # choose your formula here

    args = parse_arguments()

    if (args.formula):

        scanner = Scanner(TOKENS)

        parser = Parser(SYNTAX, scanner)

        (accepted, out, tree_nodes) = parser.parse(args.formula)

        if not accepted:

            print EXCUSE 

            return

        tree = SyntaxTree(out, tree_nodes) 

        formula = tree.root

    print "formula: \t\t\t", formula

    print "expanded -> and <->: \t\t", expand_imp_eq(formula)

    print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))

    print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))

def expand_imp_eq(formula):  

    map = {IMP: lambda (a, b): Or([Not([a]), b]),

           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}

    def values():       

        return [expand_imp_eq(v) for v in formula.values] 

    if not isinstance(formula, Operator) or formula.id not in map:       

        return formula

    return map[formula.id](values())   

def de_morgan(formula):  

    negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),

              OR: lambda (a, b): And([negate(a), negate(b)]),

              BOX: lambda (a,): Diamond([negate(a)]),

              DIAMOND: lambda (a,): Box([negate(a)]),

              VARIABLE: lambda (a,): Not([a]),

              NOT: lambda (a,): a}

    def values():

        return [de_morgan(v) for v in formula.values]

    def negate(f):

         return negmap[f.id](f.values)

    if not isinstance(formula, Operator):

        return formula  

    if formula.id == NOT:

        return negate(formula.values[0])

    return formula.__class__(values())

def reduce_iter(formula):  

    redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))

    def values():

        return [reduce_iter(v) for v in formula.values]

    if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):

        return formula

    ids = (formula.id, formula.values[0].id)

    if ids in redset:

        return reduce_iter(formula.values[0])

    return formula.__class__(values())

NOT = "~"

AND = "&"

OR = "|"

IMP = "->"

EQ = "<->"

BOX = "[]"

DIAMOND = "<>"

VARIABLE = "VAR"

LB = "("

RB = ")"

class Operator(object):

    def __init__(self, id, arity, values):

        self.id = id         

        self.arity = arity

        self.values = values

    def __str__(self):

        out = self.id

        if self.arity == 0:

            out = str(self.values[0])

        if self.arity == 1:

            out = self.id + str(self.values[0])

        elif self.arity  == 2:          

            out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"

        return out

class Not(Operator):

    arity = 1

    def __init__(self, values):

        Operator.__init__(self, NOT, Not.arity, values)       

    def __call__(self):

        pass

class And(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, AND, And.arity, values)

class Or(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, OR, Or.arity, values)       

class Imp(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, IMP, Imp.arity, values)

class Eq(Operator):

    arity = 2

    def __init__(self, values):

        Operator.__init__(self, EQ, Eq.arity, values)

class Box(Operator):

    arity = 1

    def __init__(self, values):

        Operator.__init__(self, BOX, Box.arity, values)

class Diamond(Operator):

    arity = 1

    def __init__(self, values):

        Operator.__init__(self, DIAMOND, Diamond.arity, values)

class Variable(Operator):

    arity = 0

    def __init__(self, values):

        Operator.__init__(self, VARIABLE, Variable.arity, values)   

class Lb(Operator):

    arity = -1

    def __init__(self, values):

        Operator.__init__(self, LB, Lb.arity, values)

class Rb(Operator):

    arity = -1

    def __init__(self, values):

        Operator.__init__(self, RB, Rb.arity, values)

class Formula(object):

    def __init__(self):

        pass 

TOKENS = {re.compile("\("): Lb,

          re.compile("\)"): Rb,

          re.compile("~"): Not,

          re.compile("&"): And,

          re.compile("\|"): Or,

          re.compile("->"): Imp,

          re.compile("<->"): Eq,

          re.compile("\[\]"): Box,

          re.compile("<>"): Diamond,

          re.compile("[a-z]+"): Variable}

class Scanner(object):

    def __init__(self, tokens, source=None):

        self.tokens = tokens

        self.reset(source)

    def next(self):         

        while self.i < len(self.source):

            re.purge()

            for p, token in self.tokens.iteritems():

                m = p.match(self.source[self.i:])               

                if m:                  

                    self.i += m.end(0)

                    value = m.group(0)  

                    return (token, value)

            self.i += 1

        return (None, None)

    def reset(self, source):

        self.i = 0

        self.source = source

S = Formula

A = "A"

#0 S: (Variable,),

#1 S: (Not, S),

#2 S: (Lb, A, Rb),

#3 S: (Box, S),

#4 S: (Diamond, S),

#5 A: (S, And, S),

#6 A: (S, Or, S),

#7 A: (S, Imp, S),

#8 A: (S, Eq, S)

SYNTAX = ((Variable,),

          (Not, S),

          (Lb, A, Rb),

          (Box, S),

          (Diamond, S),

          (S, And, S),

          (S, Or, S),

          (S, Imp, S),

          (S, Eq, S))

class Node(object):

    def __init__(self, parent, value):

        self.parent = parent

        self.value = value

        self.children = []

    def addChild(self, value):

        self.children.append(self, node)

class Parser(object):

    def __init__(self, syntax, scanner):

        self.syntax = syntax

        self.scanner = scanner

    def parse(self, source):

        table = {(S, Variable): 0,

                 (S, Not): 1,

                 (S, Lb): 2,

                 (S, Box): 3,

                 (S, Diamond): 4,

                 (A, S, And): 5,

                 (A, S, Or): 6,

                 (A, S, Imp): 7,

                 (A, S, Eq): 8,

                 (A, Variable, And): 5,

                 (A, Variable, Or): 6,

                 (A, Variable, Imp): 7,

                 (A, Variable, Eq): 8,

                 (A, Not, Variable, And): 5,

                 (A, Not, Variable, Or): 6,

                 (A, Not, Variable, Imp): 7,

                 (A, Not, Variable, Eq): 8}

        stack = [S]

        tree_nodes = []

        tree = None

        out = []

        self.scanner.reset(source)

        (token, value) = self.scanner.next()

        (lookahead, la_value) = self.scanner.next()

        (lookahead2, la2_value) = self.scanner.next()

        accepted = True 

        while token and len(stack): 

            top = stack[-1]               

            if top == token:

                tree_nodes.append((token, value))

                stack.pop()

                #tree_nodes.append((stack.pop(), value))

                (token, value) = (lookahead, la_value)

                (lookahead, la_value) = (lookahead2, la2_value)

                #(lookahead, _) = self.scanner.next()

                (lookahead2, la2_value) = self.scanner.next()

            else:

                action = None

                if (top, token) in table:

                    action = table[(top, token)]

                elif (top, token, lookahead) in table:

                    action = table[(top, token, lookahead)]  

                elif (top, token, lookahead, lookahead2) in table:

                    action = table[(top, token, lookahead, lookahead2)]    

                if action is None:

                    accepted = False

                    break

                out.append(action)

                stack.pop()

                stack.extend(reversed(self.syntax[action]))

        accepted = accepted and not len(stack)

        return (accepted, out, tree_nodes) 

class SyntaxTree(object):

    def __init__(self, seq, tree_nodes):

        seq.reverse()

        tree_nodes.reverse()      

        self.root = self.compile(seq, tree_nodes)[0]       

    def compile(self, seq, tree_nodes):

        stack = []     

        while len(seq):           

            s = seq.pop()

            if s == 0:

                c, v = tree_nodes.pop()

                while c != Variable:

                    c, v = tree_nodes.pop()

                stack.append(Variable(v))

            elif s == 1:

                stack.append(Not(self.compile(seq, tree_nodes)))

            elif s == 2:

                stack.extend(self.compile(seq, tree_nodes))

            elif s == 3:

                stack.append(Box(self.compile(seq, tree_nodes)))

            elif s == 4:

                stack.append(Diamond(self.compile(seq, tree_nodes)))

            elif s == 5:

                stack.append(And(self.compile(seq, tree_nodes)))

            elif s == 6:

                stack.append(Or(self.compile(seq, tree_nodes)))

            elif s == 7:

                stack.append(Imp(self.compile(seq, tree_nodes)))

            elif s == 8:

                stack.append(Eq(self.compile(seq, tree_nodes)))       

        return stack   

from argparse import ArgumentParser

def parse_arguments():

    parser = ArgumentParser(description="Parses simple modal logic syntax.")

    parser.add_argument("-f", "--formula", help="your formula") 

    return parser.parse_args()

EXCUSE = """The formula was not accepted by the parser, because the parser doesn't like you or the rest of the world. It seems to have some real issues with formulae with inner nesting and generally suffers from its hasty implementation. The parser would like to thank you for your coorporation by providing the formula within the code file itself. Thank you."""

if __name__ == "__main__":

    main()