modal_logic: sml.py@fa6d6a2cefe4

     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 import re

     8 def main():

     9     # edit your formulae here

    10     p = Variable(["p"])

    11     q = Variable(["q"])

    12     r = Variable(["r"])

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

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

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

    16     formula =  formula1 # choose your formula here

    18     args = parse_arguments()

    19     if (args.formula):

    20         scanner = Scanner(TOKENS)

    21         parser = Parser(SYNTAX, scanner)

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

    23         if not accepted:

    24             print EXCUSE

    25             return

    26         tree = SyntaxTree(out, tree_nodes)

    27         formula = tree.root

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

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

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

    33 def expand_imp_eq(formula):

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

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

    37     def values():

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

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

    41         return formula

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

    44 def reduce_not(formula):

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

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

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

    48               NOT: lambda (a,): a}

    50     def values():

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

    53     def negate(f):

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

    56     if not isinstance(formula, Operator):

    57         return formula

    58     if formula.id == NOT:

    59         return negate(formula.values[0])

    60     return formula.__class__(values())

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

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

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

    69     def values():

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

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

    73         return formula

    74     elif formula.id not in map:

    75         return formula.__class__(values())

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

    78 NOT = "~"

    79 AND = "&"

    80 OR = "|"

    81 IMP = "->"

    82 EQ = "<->"

    83 BOX = "[]"

    84 DIAMOND = "<>"

    85 VARIABLE = "VAR"

    86 LB = "("

    87 RB = ")"

    89 class Operator(object):

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

    91         self.id = id

    92         self.arity = arity

    93         self.values = values

    94     def __str__(self):

    95         out = self.id

    96         if self.arity == 0:

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

    98         if self.arity == 1:

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

   100         elif self.arity  == 2:

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

   102         return out

   104 class Not(Operator):

   105     arity = 1

   106     def __init__(self, values):

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

   108     def __call__(self):

   109         pass

   111 class And(Operator):

   112     arity = 2

   113     def __init__(self, values):

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

   116 class Or(Operator):

   117     arity = 2

   118     def __init__(self, values):

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

   121 class Imp(Operator):

   122     arity = 2

   123     def __init__(self, values):

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

   126 class Eq(Operator):

   127     arity = 2

   128     def __init__(self, values):

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

   131 class Box(Operator):

   132     arity = 1

   133     def __init__(self, values):

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

   136 class Diamond(Operator):

   137     arity = 1

   138     def __init__(self, values):

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

   141 class Variable(Operator):

   142     arity = 0

   143     def __init__(self, values):

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

   146 class Lb(Operator):

   147     arity = -1

   148     def __init__(self, values):

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

   151 class Rb(Operator):

   152     arity = -1

   153     def __init__(self, values):

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

   156 class Formula(object):

   157     def __init__(self):

   158         pass

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

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

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

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

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

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

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

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

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

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

   171 class Scanner(object):

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

   173         self.tokens = tokens

   174         self.reset(source)

   175     def next(self):

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

   177             re.purge()

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

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

   180                 if m:

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

   182                     value = m.group(0)

   183                     return (token, value)

   184             self.i += 1

   185         return (None, None)

   186     def reset(self, source):

   187         self.i = 0

   188         self.source = source

   190 S = Formula

   191 A = "A"

   192 #0 S: (Variable,),

   193 #1 S: (Not, S),

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

   195 #3 S: (Box, S),

   196 #4 S: (Diamond, S),

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

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

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

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

   201 SYNTAX = ((Variable,),

   202           (Not, S),

   203           (Lb, A, Rb),

   204           (Box, S),

   205           (Diamond, S),

   206           (S, And, S),

   207           (S, Or, S),

   208           (S, Imp, S),

   209           (S, Eq, S))

   211 class Node(object):

   212     def __init__(self, parent, value):

   213         self.parent = parent

   214         self.value = value

   215         self.children = []

   216     def addChild(self, value):

   217         self.children.append(self, node)

   219 class Parser(object):

   220     def __init__(self, syntax, scanner):

   221         self.syntax = syntax

   222         self.scanner = scanner

   223     def parse(self, source):

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

   225                  (S, Not): 1,

   226                  (S, Lb): 2,

   227                  (S, Box): 3,

   228                  (S, Diamond): 4,

   229                  (A, S, And): 5,

   230                  (A, S, Or): 6,

   231                  (A, S, Imp): 7,

   232                  (A, S, Eq): 8,

   233                  (A, Variable, And): 5,

   234                  (A, Variable, Or): 6,

   235                  (A, Variable, Imp): 7,

   236                  (A, Variable, Eq): 8,

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

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

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

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

   241         stack = [S]

   242         tree_nodes = []

   243         tree = None

   244         out = []

   245         self.scanner.reset(source)

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

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

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

   249         accepted = True

   250         while token and len(stack):

   251             top = stack[-1]

   252             if top == token:

   253                 tree_nodes.append((token, value))

   254                 stack.pop()

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

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

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

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

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

   260             else:

   261                 action = None

   262                 if (top, token) in table:

   263                     action = table[(top, token)]

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

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

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

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

   268                 if action is None:

   269                     accepted = False

   270                     break

   272                 out.append(action)

   273                 stack.pop()

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

   275         accepted = accepted and not len(stack)

   276         return (accepted, out, tree_nodes)

   278 class SyntaxTree(object):

   279     def __init__(self, seq, tree_nodes):

   280         seq.reverse()

   281         tree_nodes.reverse()

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

   283     def compile(self, seq, tree_nodes):

   284         stack = []

   285         while len(seq):

   286             s = seq.pop()

   287             if s == 0:

   288                 c, v = tree_nodes.pop()

   289                 while c != Variable:

   290                     c, v = tree_nodes.pop()

   291                 stack.append(Variable(v))

   292             elif s == 1:

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

   294             elif s == 2:

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

   296             elif s == 3:

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

   298             elif s == 4:

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

   300             elif s == 5:

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

   302             elif s == 6:

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

   304             elif s == 7:

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

   306             elif s == 8:

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

   308         return stack

   310 from argparse import ArgumentParser

   312 def parse_arguments():

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

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

   315     return parser.parse_args()

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

   319 if __name__ == "__main__":

   320     main()

author	Eugen Sawin <sawine@me73.com>
	Tue, 17 May 2011 18:01:22 +0200
changeset 15	fa6d6a2cefe4
parent 14	719b6a84938f
child 16	559d9912dded
permissions	-rw-r--r--