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

---
 .gitignore      |  1 +
 Logic.dcl       | 14 +++++++++
 Logic.icl       | 92 +++++++++++++++++++++++++++++++++++++++++++++++++++++++--
 LogicParser.icl | 23 ++++++++++++---
 LogicTest.icl   |  9 +++++-
 StringUtils.dcl | 11 +++++++
 StringUtils.icl | 25 ++++++++++++++++
 7 files changed, 167 insertions(+), 8 deletions(-)
 create mode 100644 StringUtils.dcl
 create mode 100644 StringUtils.icl

diff --git a/.gitignore b/.gitignore
index 6e882c9..262031c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 Clean System Files
+*.swp
diff --git a/Logic.dcl b/Logic.dcl
index 46228dc..90d579b 100644
--- a/Logic.dcl
+++ b/Logic.dcl
@@ -20,6 +20,11 @@ import StdEnv
 // All Chars may be used, but typically only [a-zA-Z] are used
 :: AtomName :== Char
 
+// Possibility for an atom to be true or false
+:: AtomOption :== (AtomName,Bool)
+
+:: TruthTable = {exprs :: [Expr], options :: [[AtomOption]]}
+
 isBool  :: Expr -> Bool
 isAtom  :: Expr -> Bool
 isApp1  :: Expr -> Bool
@@ -38,3 +43,12 @@ instance toString Expr
 
 binds_stronger :: Op2 Op2 -> Bool           // True iff arg1 stronger binds than arg2
 
+all_atoms :: Expr -> [AtomName]             // All the atomic expressions in an expressions
+all_atom_options :: Expr -> [[AtomOption]]  // All AtomOptions for all atomic expressions in an expression
+
+substitute :: AtomOption Expr -> Expr       // Substitute all atomic expressions with some name with some constant
+substitute_all :: [AtomOption] Expr -> Expr // Same, for multiple options
+eval :: Expr -> [Bool]                      // Evaluate to a simpler form
+
+instance toString TruthTable
+
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
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
 
diff --git a/LogicParser.icl b/LogicParser.icl
index ef81237..69adc8a 100644
--- a/LogicParser.icl
+++ b/LogicParser.icl
@@ -1,7 +1,8 @@
-module LogicParser
+module LogicTest
 
 import Logic
 
+// Some random examples
 e1 = Atom 'p'
 e2 = Atom 'q'
 e3 = App1 Not e1
@@ -9,10 +10,24 @@ e4 = App2 e1 And e2
 e5 = App2 e3 Or e2
 e6 = App2 e3 Impl e3
 e7 = App2 e4 Equiv e5
-
 e8 = App2 (App2 (Atom 'p') And (Atom 'q')) Impl (Atom 'q')
 e9 = App2 (Atom 'p') And (App2 (Atom 'q') Impl (Atom 'q'))
 
-exprs = [e1,e2,e3,e4,e5,e6,e7,e8,e9]
+exprs_rand = [e1,e2,e3,e4,e5,e6,e7,e8,e9]
+
+// To test associativity rules
+e10 = App2 (App2 (Atom 'p') And (Atom 'q')) And (Atom 'r')
+e11 = App2 (Atom 'p') And (App2 (Atom 'q') And (Atom 'r'))
+
+e12 = App2 (App2 (Atom 'p') Or (Atom 'q')) Or (Atom 'r')
+e13 = App2 (Atom 'p') Or (App2 (Atom 'q') Or (Atom 'r'))
+
+e14 = App2 (App2 (Atom 'p') Impl (Atom 'q')) Impl (Atom 'r')
+e15 = App2 (Atom 'p') Impl (App2 (Atom 'q') Impl (Atom 'r'))
+
+e16 = App2 (App2 (Atom 'p') Equiv (Atom 'q')) Equiv (Atom 'r')
+e17 = App2 (Atom 'p') Equiv (App2 (Atom 'q') Equiv (Atom 'r'))
+
+exprs_assoc = [e10,e11,e12,e13,e14,e15,e16,e17]
 
-Start = map toString exprs
+Start = map toString exprs_assoc
diff --git a/LogicTest.icl b/LogicTest.icl
index 69adc8a..4122b92 100644
--- a/LogicTest.icl
+++ b/LogicTest.icl
@@ -30,4 +30,11 @@ e17 = App2 (Atom 'p') Equiv (App2 (Atom 'q') Equiv (Atom 'r'))
 
 exprs_assoc = [e10,e11,e12,e13,e14,e15,e16,e17]
 
-Start = map toString exprs_assoc
+//Start = map all_atom_options exprs_rand
+//Start = toString (all_atom_options e4)
+//Start = substitute ('q',True) e8
+
+table = { exprs = exprs_rand ++ exprs_assoc,
+          options = all_atom_options e4 }
+
+Start = toString table
diff --git a/StringUtils.dcl b/StringUtils.dcl
new file mode 100644
index 0000000..b473246
--- /dev/null
+++ b/StringUtils.dcl
@@ -0,0 +1,11 @@
+definition module StringUtils
+
+import StdEnv
+
+strlen :: String -> Int
+
+pad_right :: String Int -> String
+pad_left :: String Int -> String
+
+join :: String [String] -> String
+
diff --git a/StringUtils.icl b/StringUtils.icl
new file mode 100644
index 0000000..1c57a69
--- /dev/null
+++ b/StringUtils.icl
@@ -0,0 +1,25 @@
+implementation module StringUtils
+
+import StdEnv
+
+strlen :: String -> Int
+strlen s = length s`
+where
+    s` :: [Char]
+    s` = fromString s
+
+pad_right :: String Int -> String
+pad_right s l
+| strlen s >= l = s
+| otherwise = s +++ toString (repeatn (l - strlen s) ' ')
+
+pad_left :: String Int -> String
+pad_left s l
+| strlen s >= l = s
+| otherwise = toString (repeatn (l - strlen s) ' ') +++ s
+
+join :: String [String] -> String
+join glue [] = ""
+join glue [s] = s
+join glue [s:ss] = s +++ glue +++ join glue ss
+
-- 
cgit v1.2.3