# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1305648034 -7200
# Node ID 719b6a84938f325fba5cfcf9e48bbf4dc49abaf4
# Parent  7e15db5920104dc6adb7c9e208f56bc9f39f6f53
Fix negation.

diff -r 7e15db592010 -r 719b6a84938f sml.py
--- a/sml.py	Tue May 17 16:11:11 2011 +0200
+++ b/sml.py	Tue May 17 18:00:34 2011 +0200
@@ -15,7 +15,7 @@
     formula1 = Imp([Eq([p, q]), r])
     formula2 = Not([Or([p, q])])
     formula3 = Not([Not([p])])
-    use = formula1
+    formula =  formula1
 
     args = parse_arguments()
     if (args.formula):
@@ -28,25 +28,54 @@
         tree = SyntaxTree(out, tree_nodes) 
         formula = tree.root
    
-    print formula
-    print "reduced"
-    print reduce(formula)
-    print reduce(formula)
+    print "formula: \t\t", formula
+    print "expanded -> and <->: \t", expand_imp_eq(formula)
+    print "reduced ~: \t\t", reduce_not(expand_imp_eq(formula))
 
-def reduce(formula):  
+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])])]),
-           NOT: lambda (a,): not isinstance(a, Not) 
-           and not isinstance(a.values[0], Not) 
-           and a.__class__([Not([v]) for v in a.values]) or a.values[0],
-           AND: lambda (a, b): And([a, b]), 
-           OR: lambda (a, b): Or([a, b])}
+           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
+
     def values():       
-        return [reduce(v) for v in formula.values] 
+        return [expand_imp_eq(v) for v in formula.values] 
 
     if not isinstance(formula, Operator) or formula.id not in map:       
         return formula
-    return map[formula.id](values())    
+    return map[formula.id](values())   
+
+def reduce_not(formula):  
+    negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
+              OR: lambda (a, b): And([negate(a), negate(b)]),
+              VARIABLE: lambda (a,): Not([a]),
+              NOT: lambda (a,): a}
+
+    def values():
+        return [reduce_not(v) for v in formula.values]
+
+    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())
+
+
+
+
+    map = {NOT: lambda (a,): not isinstance(a, Not) 
+           and not isinstance(a.values[0], Not) 
+           and a.__class__([Not([reduce2(v)]) for v in a.values]) or a.values[0]}
+
+    def values(): 
+        return [reduce2(v) for v in formula.values] 
+
+    if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
+        return formula 
+    elif formula.id not in map: 
+        return formula.__class__(values())
+    return map[formula.id](values())   
  
 NOT = "~"
 AND = "&"
@@ -55,7 +84,7 @@
 EQ = "<->"
 BOX = "[]"
 DIAMOND = "<>"
-VARIABLE = "p"
+VARIABLE = "VAR"
 LB = "("
 RB = ")"