# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1305649939 -7200
# Node ID 811d4674e90650b2f2042a15825b3e2a0be3a8bf
# Parent  aa8691f59e8f45cf6618233026f9119c19cd19c8
Added iterated modalities reduction.

diff -r aa8691f59e8f -r 811d4674e906 sml.py
--- a/sml.py	Tue May 17 18:05:04 2011 +0200
+++ b/sml.py	Tue May 17 18:32:19 2011 +0200
@@ -13,7 +13,7 @@
     formula1 = Imp([Eq([p, q]), r])
     formula2 = Not([Or([p, q])])
     formula3 = Not([Not([p])])
-    formula =  formula1 # choose your formula here
+    formula = formula1 # choose your formula here
 
     args = parse_arguments()
     if (args.formula):
@@ -26,9 +26,10 @@
         tree = SyntaxTree(out, tree_nodes) 
         formula = tree.root
    
-    print "formula: \t\t", formula
-    print "expanded -> and <->: \t", expand_imp_eq(formula)
-    print "reduced ~: \t\t", reduce_not(expand_imp_eq(formula))
+    print "formula: \t\t\t", formula
+    print "expanded -> and <->: \t\t", expand_imp_eq(formula)
+    print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))
+    print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))
 
 def expand_imp_eq(formula):  
     map = {IMP: lambda (a, b): Or([Not([a]), b]),
@@ -40,21 +41,35 @@
         return formula
     return map[formula.id](values())   
 
-def reduce_not(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([a]),
               NOT: lambda (a,): a}
     def values():
-        return [reduce_not(v) for v in formula.values]
+        return [de_morgan(v) for v in formula.values]
     def negate(f):
          return negmap[f.id](f.values)
 
     if not isinstance(formula, Operator):
-        return formula   
+        return formula  
     if formula.id == NOT:
         return negate(formula.values[0])
     return formula.__class__(values())
+
+def reduce_iter(formula):  
+    redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
+    def values():
+        return [reduce_iter(v) for v in formula.values]
+
+    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())
  
 NOT = "~"
 AND = "&"