modal_logic: smm.py@7e81bfff0521

     1 """

     2 Name:

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

     5 """

     6 from os import path

     7 import os

     8 import re

     9 import token

    11 def main():

    12     args = parse_arguments()

    13     scanner = Scanner(TOKENS)

    14     parser = Parser(SYNTAX, scanner)

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

    16     #tree = SyntaxTree(out, tree_nodes)

    17     #print tree.root

    18     p = Variable(["p"])

    19     q = Variable(["q"])

    20     r = Variable(["r"])

    21     formula = Imp([Eq([p, q]), r])

    22     formula = Not([Or([p, q])])

    23     formula = Not([Not([p])])

    24     print formula

    25     print "reduced"

    26     print reduce(formula)

    29 def reduce(formula):

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

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

    32            NOT: lambda (a,): not isinstance(a, Not) and a.__class__([Not([v]) for v in a.values]) or Not(a.values),

    33            AND: lambda (a, b): And([a, b]),

    34            OR: lambda (a, b): Or([a, b])}

    35     def values():

    36         return [reduce(v) for v in formula.values]

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

    39         print "skipped"

    40         return formula

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

    45 NOT = "~"

    46 AND = "&"

    47 OR = "|"

    48 IMP = "->"

    49 EQ = "<->"

    50 BOX = "[]"

    51 DIAMOND = "<>"

    52 VARIABLE = "p"

    53 LB = "("

    54 RB = ")"

    56 class Operator(object):

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

    58         self.id = id

    59         self.arity = arity

    60         self.values = values

    61     def __str__(self):

    62         out = self.id

    63         if self.arity == 0:

    64             out = str(self.values[0])

    65         if self.arity == 1:

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

    67         elif self.arity  == 2:

    68             #print self.id

    69             #print self.values

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

    71         return out

    73 class Not(Operator):

    74     arity = 1

    75     def __init__(self, values):

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

    77     def __call__(self):

    78         pass

    80 class And(Operator):

    81     arity = 2

    82     def __init__(self, values):

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

    85 class Or(Operator):

    86     arity = 2

    87     def __init__(self, values):

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

    90 class Imp(Operator):

    91     arity = 2

    92     def __init__(self, values):

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

    95 class Eq(Operator):

    96     arity = 2

    97     def __init__(self, values):

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

   100 class Box(Operator):

   101     arity = 1

   102     def __init__(self, values):

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

   105 class Diamond(Operator):

   106     arity = 1

   107     def __init__(self, values):

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

   110 class Variable(Operator):

   111     arity = 0

   112     def __init__(self, values):

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

   115 class Lb(Operator):

   116     arity = -1

   117     def __init__(self, values):

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

   120 class Rb(Operator):

   121     arity = -1

   122     def __init__(self, values):

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

   125 class Formula(object):

   126     def __init__(self):

   127         pass

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

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

   131           re.compile("~"): Not,

   132           re.compile("&"): And,

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

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

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

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

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

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

   140 class Scanner(object):

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

   142         self.tokens = tokens

   143         self.reset(source)

   144     def next(self):

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

   146             re.purge()

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

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

   149                 if m:

   150                     self.i += m.end(0)

   151                     value = m.group(0)

   152                     return (token, value)

   153             self.i += 1

   154         return (None, None)

   155     def reset(self, source):

   156         self.i = 0

   157         self.source = source

   159 S = Formula

   160 A = "A"

   161 #0 S: (Variable,),

   162 #1 S: (Not, S),

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

   164 #3 S: (Box, S),

   165 #4 S: (Diamond, S),

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

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

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

   169 #8 A: (S, Eq, S)

   170 SYNTAX = ((Variable,),

   171           (Not, S),

   172           (Lb, A, Rb),

   173           (Box, S),

   174           (Diamond, S),

   175           (S, And, S),

   176           (S, Or, S),

   177           (S, Imp, S),

   178           (S, Eq, S))

   180 class Node(object):

   181     def __init__(self, parent, value):

   182         self.parent = parent

   183         self.value = value

   184         self.children = []

   185     def addChild(self, value):

   186         self.children.append(self, node)

   188 class Parser(object):

   189     def __init__(self, syntax, scanner):

   190         self.syntax = syntax

   191         self.scanner = scanner

   192     def parse(self, source):

   193         table = {(S, Variable): 0,

   194                  (S, Not): 1,

   195                  (S, Lb): 2,

   196                  (S, Box): 3,

   197                  (S, Diamond): 4,

   198                  (A, S, And): 5,

   199                  (A, S, Or): 6,

   200                  (A, S, Imp): 7,

   201                  (A, S, Eq): 8,

   202                  (A, Variable, And): 5,

   203                  (A, Variable, Or): 6,

   204                  (A, Variable, Imp): 7,

   205                  (A, Variable, Eq): 8,

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

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

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

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

   210         stack = [S]

   211         tree_nodes = []

   212         tree = None

   213         out = []

   214         self.scanner.reset(source)

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

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

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

   218         accepted = True

   219         while token and len(stack):

   220             top = stack[-1]

   221             if top == token:

   222                 tree_nodes.append((token, value))

   223                 stack.pop()

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

   225                 (token, value) = (lookahead, la_value)

   226                 (lookahead, la_value) = (lookahead2, la2_value)

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

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

   229             else:

   230                 action = None

   231                 if (top, token) in table:

   232                     action = table[(top, token)]

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

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

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

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

   237                 if action is None:

   238                     accepted = False

   239                     break

   241                 out.append(action)

   242                 stack.pop()

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

   244         accepted = accepted and not len(stack)

   245         return (accepted, out, tree_nodes)

   247 class SyntaxTree(object):

   248     def __init__(self, seq, tree_nodes):

   249         seq.reverse()

   250         tree_nodes.reverse()

   251         print tree_nodes

   252         print seq

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

   254         print self.root

   255     def compile(self, seq, tree_nodes):

   256         stack = []

   257         waiting = []

   258         print seq

   259         while len(seq):

   260             s = seq.pop()

   261             if s == 0:

   262                 c, v = tree_nodes.pop()

   263                 while c != Variable:

   264                     c, v = tree_nodes.pop()

   265                 stack.append(Variable(v))

   266             elif s == 1:

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

   268             elif s == 2:

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

   270             elif s == 3:

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

   272             elif s == 4:

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

   274             elif s == 5:

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

   276             elif s == 6:

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

   278             elif s == 7:

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

   280             elif s == 8:

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

   282         print stack

   283         return stack

   285     def compile_(self, tree_nodes):

   286         table = []

   287         unfinished = []

   288         node = None

   289         print tree_nodes

   290         for n, v in (tree_nodes):

   291             print

   292             print n

   293             if n.arity >= 0:

   294                 if len(table) < n.arity:

   295                     print "appending unfinished ", n

   296                     unfinished.append(n)

   297                 else:

   298                     args = table[:n.arity]

   299                     if n.arity == 0:

   300                         args = [v]

   301                     table = table[n.arity:]

   302                     node = n(args)

   303                     table.append(node)

   304                 if len(unfinished) and unfinished[-1].arity <= len(table):

   305                     n = unfinished[-1]

   306                     print "finishing ", n

   307                     args = table[:n.arity]

   308                     table = table[n.arity:]

   309                     node = n(args)

   310                     table.append(node)

   311                     unfinished.pop()

   312         return table[0]

   314 from argparse import ArgumentParser

   316 def parse_arguments():

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

   318     parser.add_argument("formula", help="your formula")

   319     return parser.parse_args()

   321 if __name__ == "__main__":

   322     main()

author	Eugen Sawin <sawine@me73.com>
	Tue, 17 May 2011 13:52:38 +0200
changeset 9	7e81bfff0521
parent 8	09cc70d6f115
child 10	c7ca4a177c90
permissions	-rw-r--r--