# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1305652294 -7200
# Node ID 42bc914ee673b79d7020620e5eb332e6264b938b
# Parent  811d4674e90650b2f2042a15825b3e2a0be3a8bf
Added modality distribution.

diff -r 811d4674e906 -r 42bc914ee673 sml.py
--- a/sml.py	Tue May 17 18:32:19 2011 +0200
+++ b/sml.py	Tue May 17 19:11:34 2011 +0200
@@ -30,16 +30,17 @@
     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)))))
+
+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])])])}
-    def values():       
-        return [expand_imp_eq(v) for v in formula.values] 
-
+           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}   
     if not isinstance(formula, Operator) or formula.id not in map:       
         return formula
-    return map[formula.id](values())   
+    return map[formula.id](values(expand_imp_eq, formula))   
 
 def de_morgan(formula):  
     negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
@@ -47,29 +48,37 @@
               BOX: lambda (a,): Diamond([negate(a)]),
               DIAMOND: lambda (a,): Box([negate(a)]),
               VARIABLE: lambda (a,): Not([a]),
-              NOT: lambda (a,): a}
-    def values():
-        return [de_morgan(v) for v in formula.values]
+              NOT: lambda (a,): a}    
     def negate(f):
          return negmap[f.id](f.values)
-
     if not isinstance(formula, Operator):
         return formula  
     if formula.id == NOT:
         return negate(formula.values[0])
-    return formula.__class__(values())
+    return formula.__class__(values(de_morgan, formula))
 
 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())
+    return formula.__class__(values(reduce_iter, formula))
+
+def dist(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))               
+               and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
+               (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
+               and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}   
+    if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
+        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))        
  
 NOT = "~"
 AND = "&"
@@ -310,7 +319,7 @@
     parser.add_argument("-f", "--formula", help="your formula") 
     return parser.parse_args()
  
-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."""
+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"""
 
 if __name__ == "__main__":
     main()