"""

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"]) 

    s = Variable(["s"])

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

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

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

    formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])

    formula5 = Imp([And([Or([p, q]), r]), Not([s])])

    formula = formula5 # 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

    original = formula

    print "formula: \t\t\t%s [%i]" % (formula, formula.depth())

    formula = expand_imp_eq(formula)

    print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) 

    formula = de_morgan(formula)

    print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) 

    formula = reduce_iter(formula)

    print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) 

    formula = reduce_iter(dist_mod((formula)))

    print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) 

    formula = mcnf(formula)

    print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())

    cnf_formula = cnf(original)

    print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())

def values(fun, f):  

    return [fun(v) for v in f.values] 

def expand_imp_eq(formula):  

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

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

    if not isinstance(formula, Operator):   

        return formula

    if formula.id in expmap:

        return expmap[formula.id](values(expand_imp_eq, formula))   

    return formula.__class__(values(expand_imp_eq, formula))

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([Variable([a])]),

              NOT: lambda (a,): a}    

    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(de_morgan, formula))

def reduce_iter(formula):  

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

    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(reduce_iter, formula))

def dist_mod(formula):    

    distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),

               (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),

               (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))               

               and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),

               (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))

               and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}   

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

        return formula

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

    if ids in distmap:

        return distmap[ids](values(dist_mod, formula.values[0]))

    return formula.__class__(values(dist_mod, formula))    

def mcnf(formula):

    if formula.id == OR:

        conj_id = int(formula.values[1].id == AND) 

        return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]), 

                    Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);

    return formula

def cnf(formula):      

    def part(f):

        for v in f.values:

            if v.id != VARIABLE:

                sub_formulae.append(v)

                part(v)

    sub_formulae = [formula]

    part(formula)

    sub_formulae.reverse() 

    known = {}

    bicon = []

    for s in sub_formulae:       

        for i, v in enumerate(s.values):

            if v in known:

                s.values[i] = known[v]

        bicon.append(Eq([Variable(["x" + str(len(bicon))]), s]))

        known[s] = bicon[-1].values[0]    

    def conjunct(f):

        if len(bicon):

            return And([f, conjunct(bicon.pop())])

        return f

    return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))

""" The Parser - Do NOT look below this line! """ 

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 depth(self):       

        if self.arity == 0:

            return 0

        if self.id in (BOX, DIAMOND):

            return 1 + self.values[0].depth()

        if self.id == NOT:           

            return self.values[0].depth()

        return max(self.values[0].depth(), self.values[1].depth())

    def __eq__(self, other):

        return self.id == other.id and self.values == other.values # commutative types not considered yet

    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="Tries to parse simple modal logic syntax and reduces the formula. Edit your formula directly in the code file for best results.")

    parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") 

    return parser.parse_args()

EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""

if __name__ == "__main__":

    main()