diff -r 42bc914ee673 -r 1f97011ea795 sml.py
--- a/sml.py	Tue May 17 19:11:34 2011 +0200
+++ b/sml.py	Wed May 18 03:23:35 2011 +0200
@@ -13,7 +13,8 @@
     formula1 = Imp([Eq([p, q]), r])
     formula2 = Not([Or([p, q])])
     formula3 = Not([Not([p])])
-    formula = formula1 # choose your formula here
+    formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
+    formula = formula4 # choose your formula here
 
     args = parse_arguments()
     if (args.formula):
@@ -26,31 +27,38 @@
         tree = SyntaxTree(out, tree_nodes) 
         formula = tree.root
    
-    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)))
-    print "distributed modalities+: \t", reduce_iter(dist(reduce_iter(de_morgan(expand_imp_eq(formula)))))
+    print "formula: \t\t\t%s (%i)" % (formula, formula.depth())
+    formula = expand_imp_eq(formula)
+    print "expanded -> and <->: \t\t%s (%i)" % (formula, formula.depth()) 
+    formula = de_morgan(formula)
+    print "reduced ~: \t\t\t%s (%i)" % (formula, formula.depth()) 
+    formula = reduce_iter(formula)
+    print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth()) 
+    formula = reduce_iter(dist_mod((formula)))
+    print "distributed modalities+: \t%s (%i)" % (formula, formula.depth()) 
+    formula = None
 
 def values(fun, f):  
     return [fun(v) for v in f.values] 
 
 def expand_imp_eq(formula):  
-    map = {IMP: lambda (a, b): Or([Not([a]), b]),
-           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}   
-    if not isinstance(formula, Operator) or formula.id not in map:       
+    expmap = {IMP: lambda (a, b): Or([Not([a]), b]),
+              EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}   
+    if not isinstance(formula, Operator):   
         return formula
-    return map[formula.id](values(expand_imp_eq, formula))   
+    if formula.id in expmap:
+        return expmap[formula.id](values(expand_imp_eq, formula))   
+    return formula.__class__(values(expand_imp_eq, formula))
 
-def de_morgan(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]),
+              VARIABLE: lambda (a,): Not([Variable([a])]),
               NOT: lambda (a,): a}    
     def negate(f):
-         return negmap[f.id](f.values)
+        return negmap[f.id](f.values)
     if not isinstance(formula, Operator):
         return formula  
     if formula.id == NOT:
@@ -66,7 +74,7 @@
         return reduce_iter(formula.values[0])
     return formula.__class__(values(reduce_iter, formula))
 
-def dist(formula):    
+def dist_mod(formula):    
     distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
                (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
                (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))               
@@ -77,8 +85,8 @@
         return formula
     ids = (formula.id, formula.values[0].id)
     if ids in distmap:
-        return distmap[ids](formula.values[0].values)
-    return formula.__class__(values(dist, formula))        
+        return distmap[ids](values(dist_mod, formula.values[0]))
+    return formula.__class__(values(dist_mod, formula))        
  
 NOT = "~"
 AND = "&"
@@ -96,10 +104,18 @@
         self.id = id         
         self.arity = arity
         self.values = values
+    def depth(self):       
+        if self.arity == 0:
+            return 0
+        if self.id in (BOX, DIAMOND):
+            return 1 + self.values[0].depth()
+        if self.id == NOT:           
+            return self.values[0].depth()
+        return max(self.values[0].depth(), self.values[1].depth())
     def __str__(self):
         out = self.id
         if self.arity == 0:
-            out = str(self.values[0])
+            out = str(self.values[0])           
         if self.arity == 1:
             out = self.id + str(self.values[0])
         elif self.arity  == 2:          
@@ -319,7 +335,7 @@
     parser.add_argument("-f", "--formula", help="your formula") 
     return parser.parse_args()
  
-EXCUSE = """The formula was not accepted by me, because I don't like you and the rest of the world. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
+EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
 
 if __name__ == "__main__":
     main()