modal_logic: smm.py@3d2eea446705

     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 NOT = "~"

    12 AND = "&"

    13 OR = "|"

    14 IMP = "->"

    15 EQ = "<->"

    16 BOX = "[]"

    17 DIAMOND = "<>"

    18 VARIABLE = "p"

    19 LB = "("

    20 RB = ")"

    22 class Operator(object):

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

    24         self.id = id

    25         self.arity = arity

    26         self.values = values

    27     def __str__(self):

    28         out = self.id

    29         if self.arity == 0:

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

    31         if self.arity == 1:

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

    33         elif self.arity  == 2:

    34             #print self.id

    35             #print self.values

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

    37         return out

    39 class Not(Operator):

    40     arity = 1

    41     def __init__(self, values):

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

    43     def __call__(self):

    44         pass

    46 class And(Operator):

    47     arity = 2

    48     def __init__(self, values):

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

    51 class Or(Operator):

    52     arity = 2

    53     def __init__(self, values):

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

    56 class Imp(Operator):

    57     arity = 2

    58     def __init__(self, values):

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

    61 class Eq(Operator):

    62     arity = 2

    63     def __init__(self, values):

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

    66 class Box(Operator):

    67     arity = 1

    68     def __init__(self, values):

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

    71 class Diamond(Operator):

    72     arity = 1

    73     def __init__(self, values):

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

    76 class Variable(Operator):

    77     arity = 0

    78     def __init__(self, values):

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

    81 class Lb(Operator):

    82     arity = -1

    83     def __init__(self, values):

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

    86 class Rb(Operator):

    87     arity = -1

    88     def __init__(self, values):

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

    91 class Formula(object):

    92     def __init__(self):

    93         pass

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

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

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

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

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

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

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

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

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

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

   106 class Scanner(object):

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

   108         self.tokens = tokens

   109         self.reset(source)

   110     def next(self):

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

   112             re.purge()

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

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

   115                 if m:

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

   117                     value = m.group(0)

   118                     return (token, value)

   119             self.i += 1

   120         return (None, None)

   121     def reset(self, source):

   122         self.i = 0

   123         self.source = source

   125 S = Formula

   126 A = "A"

   127 #0 S: (Variable,),

   128 #1 S: (Not, S),

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

   130 #3 S: (Box, S),

   131 #4 S: (Diamond, S),

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

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

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

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

   136 SYNTAX = ((Variable,),

   137           (Not, S),

   138           (Lb, A, Rb),

   139           (Box, S),

   140           (Diamond, S),

   141           (S, And, S),

   142           (S, Or, S),

   143           (S, Imp, S),

   144           (S, Eq, S))

   146 class Node(object):

   147     def __init__(self, parent, value):

   148         self.parent = parent

   149         self.value = value

   150         self.children = []

   151     def addChild(self, value):

   152         self.children.append(self, node)

   154 class Parser(object):

   155     def __init__(self, syntax, scanner):

   156         self.syntax = syntax

   157         self.scanner = scanner

   158     def parse(self, source):

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

   160                  (S, Not): 1,

   161                  (S, Lb): 2,

   162                  (S, Box): 3,

   163                  (S, Diamond): 4,

   164                  (A, S, And): 5,

   165                  (A, S, Or): 6,

   166                  (A, S, Imp): 7,

   167                  (A, S, Eq): 8,

   168                  (A, Variable, And): 5,

   169                  (A, Variable, Or): 6,

   170                  (A, Variable, Imp): 7,

   171                  (A, Variable, Eq): 8,

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

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

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

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

   176         stack = [S]

   177         tree_nodes = []

   178         tree = None

   179         out = []

   180         self.scanner.reset(source)

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

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

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

   184         accepted = True

   185         while token and len(stack):

   186             top = stack[-1]

   187             if top == token:

   188                 tree_nodes.append((token, value))

   189                 stack.pop()

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

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

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

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

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

   195             else:

   196                 action = None

   197                 if (top, token) in table:

   198                     action = table[(top, token)]

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

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

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

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

   203                 if action is None:

   204                     accepted = False

   205                     break

   207                 out.append(action)

   208                 stack.pop()

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

   210         accepted = accepted and not len(stack)

   211         return (accepted, out, tree_nodes)

   213 class SyntaxTree(object):

   214     def __init__(self, seq, tree_nodes):

   215         seq.reverse()

   216         tree_nodes.reverse()

   217         print tree_nodes

   218         print seq

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

   220         print self.root

   221     def compile(self, seq, tree_nodes):

   222         stack = []

   223         waiting = []

   224         print seq

   225         while len(seq):

   226             s = seq.pop()

   227             if s == 0:

   228                 c, v = tree_nodes.pop()

   229                 while c != Variable:

   230                     c, v = tree_nodes.pop()

   231                 stack.append(Variable(v))

   232             elif s == 1:

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

   234             elif s == 2:

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

   236             elif s == 3:

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

   238             elif s == 4:

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

   240             elif s == 5:

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

   242             elif s == 6:

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

   244             elif s == 7:

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

   246             elif s == 8:

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

   248         print stack

   249         return stack

   251     def compile_(self, tree_nodes):

   252         table = []

   253         unfinished = []

   254         node = None

   255         print tree_nodes

   256         for n, v in (tree_nodes):

   257             print

   258             print n

   259             if n.arity >= 0:

   260                 if len(table) < n.arity:

   261                     print "appending unfinished ", n

   262                     unfinished.append(n)

   263                 else:

   264                     args = table[:n.arity]

   265                     if n.arity == 0:

   266                         args = [v]

   267                     table = table[n.arity:]

   268                     node = n(args)

   269                     table.append(node)

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

   271                     n = unfinished[-1]

   272                     print "finishing ", n

   273                     args = table[:n.arity]

   274                     table = table[n.arity:]

   275                     node = n(args)

   276                     table.append(node)

   277                     unfinished.pop()

   278         return table[0]

   281 def main():

   282     args = parse_arguments()

   283     scanner = Scanner(TOKENS)

   284     parser = Parser(SYNTAX, scanner)

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

   286     tree = SyntaxTree(out, tree_nodes)

   287     #print tree.root

   289 from argparse import ArgumentParser

   291 def parse_arguments():

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

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

   294     return parser.parse_args()

   296 if __name__ == "__main__":

   297     main()

author	Eugen Sawin <sawine@me73.com>
	Tue, 17 May 2011 02:19:11 +0200
changeset 6	3d2eea446705
parent 5	ca2d1c23da5f
child 7	cafa7d4b888d
permissions	-rw-r--r--