modal_logic: sml.py@719b6a84938f

     1 """

     2 Name: sml - Simple Modal Logic Lib.

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

     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     p = Variable(["p"])

    13     q = Variable(["q"])

    14     r = Variable(["r"])

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

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

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

    18     formula =  formula1

    20     args = parse_arguments()

    21     if (args.formula):

    22         scanner = Scanner(TOKENS)

    23         parser = Parser(SYNTAX, scanner)

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

    25         if not accepted:

    26             print EXCUSE

    27             return

    28         tree = SyntaxTree(out, tree_nodes)

    29         formula = tree.root

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

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

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

    35 def expand_imp_eq(formula):

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

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

    39     def values():

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

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

    43         return formula

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

    46 def reduce_not(formula):

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

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

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

    50               NOT: lambda (a,): a}

    52     def values():

    53         return [reduce_not(v) for v in formula.values]

    55     def negate(f):

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

    58     if not isinstance(formula, Operator):

    59         return formula

    60     if formula.id == NOT:

    61         return negate(formula.values[0])

    62     return formula.__class__(values())

    67     map = {NOT: lambda (a,): not isinstance(a, Not)

    68            and not isinstance(a.values[0], Not)

    69            and a.__class__([Not([reduce2(v)]) for v in a.values]) or a.values[0]}

    71     def values():

    72         return [reduce2(v) for v in formula.values]

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

    75         return formula

    76     elif formula.id not in map:

    77         return formula.__class__(values())

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

    80 NOT = "~"

    81 AND = "&"

    82 OR = "|"

    83 IMP = "->"

    84 EQ = "<->"

    85 BOX = "[]"

    86 DIAMOND = "<>"

    87 VARIABLE = "VAR"

    88 LB = "("

    89 RB = ")"

    91 class Operator(object):

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

    93         self.id = id

    94         self.arity = arity

    95         self.values = values

    96     def __str__(self):

    97         out = self.id

    98         if self.arity == 0:

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

   100         if self.arity == 1:

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

   102         elif self.arity  == 2:

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

   104         return out

   106 class Not(Operator):

   107     arity = 1

   108     def __init__(self, values):

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

   110     def __call__(self):

   111         pass

   113 class And(Operator):

   114     arity = 2

   115     def __init__(self, values):

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

   118 class Or(Operator):

   119     arity = 2

   120     def __init__(self, values):

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

   123 class Imp(Operator):

   124     arity = 2

   125     def __init__(self, values):

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

   128 class Eq(Operator):

   129     arity = 2

   130     def __init__(self, values):

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

   133 class Box(Operator):

   134     arity = 1

   135     def __init__(self, values):

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

   138 class Diamond(Operator):

   139     arity = 1

   140     def __init__(self, values):

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

   143 class Variable(Operator):

   144     arity = 0

   145     def __init__(self, values):

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

   148 class Lb(Operator):

   149     arity = -1

   150     def __init__(self, values):

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

   153 class Rb(Operator):

   154     arity = -1

   155     def __init__(self, values):

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

   158 class Formula(object):

   159     def __init__(self):

   160         pass

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

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

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

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

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

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

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

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

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

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

   173 class Scanner(object):

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

   175         self.tokens = tokens

   176         self.reset(source)

   177     def next(self):

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

   179             re.purge()

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

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

   182                 if m:

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

   184                     value = m.group(0)

   185                     return (token, value)

   186             self.i += 1

   187         return (None, None)

   188     def reset(self, source):

   189         self.i = 0

   190         self.source = source

   192 S = Formula

   193 A = "A"

   194 #0 S: (Variable,),

   195 #1 S: (Not, S),

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

   197 #3 S: (Box, S),

   198 #4 S: (Diamond, S),

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

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

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

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

   203 SYNTAX = ((Variable,),

   204           (Not, S),

   205           (Lb, A, Rb),

   206           (Box, S),

   207           (Diamond, S),

   208           (S, And, S),

   209           (S, Or, S),

   210           (S, Imp, S),

   211           (S, Eq, S))

   213 class Node(object):

   214     def __init__(self, parent, value):

   215         self.parent = parent

   216         self.value = value

   217         self.children = []

   218     def addChild(self, value):

   219         self.children.append(self, node)

   221 class Parser(object):

   222     def __init__(self, syntax, scanner):

   223         self.syntax = syntax

   224         self.scanner = scanner

   225     def parse(self, source):

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

   227                  (S, Not): 1,

   228                  (S, Lb): 2,

   229                  (S, Box): 3,

   230                  (S, Diamond): 4,

   231                  (A, S, And): 5,

   232                  (A, S, Or): 6,

   233                  (A, S, Imp): 7,

   234                  (A, S, Eq): 8,

   235                  (A, Variable, And): 5,

   236                  (A, Variable, Or): 6,

   237                  (A, Variable, Imp): 7,

   238                  (A, Variable, Eq): 8,

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

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

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

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

   243         stack = [S]

   244         tree_nodes = []

   245         tree = None

   246         out = []

   247         self.scanner.reset(source)

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

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

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

   251         accepted = True

   252         while token and len(stack):

   253             top = stack[-1]

   254             if top == token:

   255                 tree_nodes.append((token, value))

   256                 stack.pop()

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

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

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

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

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

   262             else:

   263                 action = None

   264                 if (top, token) in table:

   265                     action = table[(top, token)]

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

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

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

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

   270                 if action is None:

   271                     accepted = False

   272                     break

   274                 out.append(action)

   275                 stack.pop()

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

   277         accepted = accepted and not len(stack)

   278         return (accepted, out, tree_nodes)

   280 class SyntaxTree(object):

   281     def __init__(self, seq, tree_nodes):

   282         seq.reverse()

   283         tree_nodes.reverse()

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

   285     def compile(self, seq, tree_nodes):

   286         stack = []

   287         while len(seq):

   288             s = seq.pop()

   289             if s == 0:

   290                 c, v = tree_nodes.pop()

   291                 while c != Variable:

   292                     c, v = tree_nodes.pop()

   293                 stack.append(Variable(v))

   294             elif s == 1:

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

   296             elif s == 2:

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

   298             elif s == 3:

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

   300             elif s == 4:

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

   302             elif s == 5:

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

   304             elif s == 6:

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

   306             elif s == 7:

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

   308             elif s == 8:

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

   310         return stack

   312 from argparse import ArgumentParser

   314 def parse_arguments():

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

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

   317     return parser.parse_args()

   319 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."""

   321 if __name__ == "__main__":

   322     main()

author	Eugen Sawin <sawine@me73.com>
	Tue, 17 May 2011 18:00:34 +0200
changeset 14	719b6a84938f
parent 13	7e15db592010
child 15	fa6d6a2cefe4
permissions	-rw-r--r--