Nicer truthtables

1 files changed, 91 insertions, 18 deletions

diff --git a/Logic.icl b/Logic.icl
index 7ebf98f..24ce94d 100644
--- a/Logic.icl
+++ b/Logic.icl
@@ -77,6 +77,88 @@ where
         | needs_parentheses_right (App2 e1 op e2) = "(" +++ toString e2 +++ ")"
         | otherwise = toString e2
 
+instance toString TruthTable
+where
+    toString t=:{exprs,options}
+        = row_b +++ join row_s [pad_right head len \\ head <- map toString exprs & len <- padlens] +++ row_e +++
+          line_b +++ join line_s [toString (repeatn len '-') \\ len <- padlens] +++ line_e +++
+          foldr (+++) "" [row_b +++ join row_s [pad_right (toStringOrEmpty val) len \\ val <- map (eval o substitute_all options`) exprs & len <- padlens] +++ row_e \\ options` <- options]
+        //= foldr (+++) "" (map toString padlens)
+    where
+        row_b = " "
+        row_e = " \n"
+        row_s = " | "
+        line_b = "-"
+        line_e = "-\n"
+        line_s = "-+-"
+        padlens = map ((max 5) o strlen o toString) exprs 
+        toStringOrEmpty :: [Bool] -> String
+        toStringOrEmpty [] = ""
+        toStringOrEmpty [b:bs] = toString b
+
+instance == Op1
+where
+    (==) Not Not = True
+
+instance < Op1
+where
+    (<) Not Not = False // this doesn't make much sense, but whatever
+
+instance == Op2
+where
+    (==) And And = True
+    (==) Or Or = True
+    (==) Impl Impl = True
+    (==) Equiv Equiv = True
+    (==) _ _ = False
+
+instance < Op2
+where
+    (<) op1 op2
+    | op1 == op2 = False
+    | otherwise = comp op1 op2
+    where
+        comp And And = False
+        comp And _ = True
+        comp _ And = False
+        comp Or Or = False
+        comp Or _ = True
+        comp _ Or = False
+        comp Impl Impl = False
+        comp Impl _ = True
+        comp Equiv Equiv = False
+
+instance == Expr
+where
+    (==) (B b1) (B b2) = b1 == b2
+    (==) (Atom a1) (Atom a2) = a1 == a2
+    (==) (App1 op e) (App1 op` e`) = op == op` && e == e`
+    (==) (App2 e1 op e2) (App2 e1` op` e2`) = e1 == e1` && op == op` && e2 == e2`
+    (==) _ _ = False
+
+instance < Expr
+where
+    (<) e1 e2
+    | e1 == e2 = False
+    | otherwise = comp e1 e2
+    where
+        comp (B False) _ = True
+        comp _ (B False) = False
+        comp (B _) _ = True
+        comp _ (B _) = False
+        comp (Atom a) (Atom b) = a < b
+        comp (Atom _) _ = True
+        comp _ (Atom _) = False
+        comp (App1 _ e) (App1 _ e`) = e < e`
+        comp (App1 _ _) _ = True
+        comp _ (App1 _ _) = False
+        comp (App2 e1 op e2) (App2 e1` op` e2`)
+        | e1 < e1` = True
+        | e1` < e1 = False
+        | e2 < e2` = True
+        | e2` < e2 = False
+        | otherwise = op < op`
+
 needs_parentheses :: Expr -> Bool
 needs_parentheses (App1 Not (B _)) = False
 needs_parentheses (App1 Not (Atom _)) = False
@@ -141,26 +223,17 @@ eval (App1 op e) = [apply1 op e` \\ e` <- eval e]
 eval (App2 e1 op e2) = [apply2 e1` op e2` \\ e1` <- eval e1 & e2` <- eval e2]
 eval _ = []
 
-instance toString TruthTable
-where
-    toString t=:{exprs,options}
-        = row_b +++ join row_s [pad_right head len \\ head <- map toString exprs & len <- padlens] +++ row_e +++
-          line_b +++ join line_s [toString (repeatn len '-') \\ len <- padlens] +++ line_e +++
-          foldr (+++) "" [row_b +++ join row_s [pad_right (toStringOrEmpty val) len \\ val <- map (eval o substitute_all options`) exprs & len <- padlens] +++ row_e \\ options` <- options]
-        //= foldr (+++) "" (map toString padlens)
-    where
-        row_b = " "
-        row_e = " \n"
-        row_s = " | "
-        line_b = "-"
-        line_e = "-\n"
-        line_s = "-+-"
-        padlens = map ((max 5) o strlen o toString) exprs 
-        toStringOrEmpty :: [Bool] -> String
-        toStringOrEmpty [] = ""
-        toStringOrEmpty [b:bs] = toString b
+subexprs :: Expr -> [Expr]
+subexprs (B _) = []
+subexprs (Atom _) = []
+subexprs (App1 op e) = removeDup (subexprs e ++ [e])
+subexprs (App2 e1 op e2) = removeDup (subexprs e1 ++ subexprs e2 ++ [e1,e2])
 
+sorted_subexprs :: (Expr -> [Expr])
+sorted_subexprs = sort o subexprs
 
+truthtable :: Expr -> TruthTable
+truthtable e = {exprs = sorted_subexprs e ++ [e], options = all_atom_options e}