From 537bb5e2bae76e0df0d9e07a40dbe6b299be6aad Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 3 Jul 2015 12:43:24 +0200
Subject: Truth tables

---
 Logic.icl | 92 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 89 insertions(+), 3 deletions(-)

(limited to 'Logic.icl')

diff --git a/Logic.icl b/Logic.icl
index 5d5fc26..7ebf98f 100644
--- a/Logic.icl
+++ b/Logic.icl
@@ -1,6 +1,6 @@
 implementation module Logic
 
-import StdEnv
+import StdEnv, StringUtils
 
 isBool  :: Expr -> Bool
 isBool (B _) = True
@@ -41,6 +41,15 @@ isEquiv :: Expr -> Bool
 isEquiv (App2 _ Equiv _) = True
 isEquiv _ = False
 
+apply1 :: Op1 Bool -> Bool
+apply1 Not b = not b
+
+apply2 :: Bool Op2 Bool -> Bool
+apply2 x And y = x && y
+apply2 x Or y = x || y
+apply2 x Impl y = y || not x
+apply2 x Equiv y = x == y
+
 instance toString Op1
 where
     toString Not = "~"
@@ -54,8 +63,7 @@ where
 
 instance toString Expr
 where
-    toString (B True) = toString 1
-    toString (B False) = toString 0
+    toString (B b) = toString b
     toString (Atom a) = toString a
     toString (App1 op e)
     | needs_parentheses (App1 op e) = toString op +++ "(" +++ toString e +++ ")"
@@ -96,4 +104,82 @@ binds_stronger _ Or = False
 binds_stronger Impl _ = True
 binds_stronger _ Impl = False
 binds_stronger Equiv Equiv = True
+
+all_atoms :: Expr -> [AtomName]
+all_atoms (Atom a) = [a]
+all_atoms (B _) = []
+all_atoms (App1 _ e) = all_atoms e
+all_atoms (App2 e1 _ e2) = removeDup (all_atoms e1 ++ all_atoms e2)
+
+all_atom_options :: Expr -> [[AtomOption]]
+all_atom_options e = [opt \\ opt <- all_options (all_atoms e) []]
+where
+    all_options :: [AtomName] [AtomOption] -> [[AtomOption]]
+    all_options [] opts = [opts]
+    all_options [a:as] opts = all_options as (opts ++ [(a,False)]) ++ all_options as (opts ++ [(a,True)])
+
+substitute :: AtomOption Expr -> Expr
+substitute (a,b) (Atom a`)
+| a == a` = B b
+| otherwise = Atom a`
+substitute (a,b) (App1 op e) = App1 op (substitute (a,b) e)
+substitute (a,b) (App2 e1 op e2) = App2 (substitute (a,b) e1) op (substitute (a,b) e2)
+substitute _ e = e
+
+substitute_all :: [AtomOption] Expr -> Expr
+substitute_all opts e = foldr substitute e opts
+
+contains_atoms :: Expr -> Bool
+contains_atoms (B _) = False
+contains_atoms (Atom _) = True
+contains_atoms (App1 _ e) = contains_atoms e
+contains_atoms (App2 e1 _ e2) = contains_atoms e1 || contains_atoms e2
+
+eval :: Expr -> [Bool]
+eval (B b) = [b]
+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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 
-- 
cgit v1.2.3