\section{Propositional Formulae}

%include lhs2Tex.fmt

Imports of functions from the hierarchical libraries:

\begin{code}
import Data.List (nub)
import Data.Maybe (fromJust)
\end{code}

The datatype for simple propositional logic formulae
is unchanged from the solution for 1.7;
it uses |String| to represent propositional variables,
but only strings containing identifiers should be used.

\begin{code}
type Variable = Char
data Prop
  = Var Variable
  | Negation Prop
  | BinOp Op Prop Prop
  deriving (Eq, Ord) -- |Eq| will be needed for |nub| in |subProps| below.
\end{code}

To allow more generalised treatment of the binary operators,
we included only a single alternative for all of them,
and provide a separate datatype to contain just the binary operators:

\begin{code}
data Op = And | Or | Implies | Equiv
  deriving (Eq, Ord)
\end{code}

Code below is follow the sequence of the assignment 1.8
\begin{code}
deVar :: Prop -> Bool
deVar a = case a of 
      Var _ -> True
      _ -> False

deNeg :: Prop -> Bool
deNeg a = case a of 
      Negation _ -> True
      _ -> False

deCon :: Prop -> Bool
deCon a = case a of 
      BinOp And _ _ -> True
      _ -> False

deDis :: Prop -> Bool
deDis a = case a of 
      BinOp Or _ _ -> True
      _ -> False

deImp :: Prop -> Bool
deImp a = case a of 
      BinOp Implies _ _ -> True
      _ -> False

deEqu :: Prop -> Bool
deEqu a = case a of 
      BinOp Equiv _ _ -> True
      _ -> False

nestDepth :: Prop -> Int
nestDepth a = case a of
          Var _ -> 0
          Negation x -> 1 + (nestDepth x)
          BinOp _ x y -> 1 + max (nestDepth x) (nestDepth y)

subProps :: Prop -> [Prop]
subProps p@(Var _) = [p]
subProps p@(Negation q) = p : subProps q
subProps p@(BinOp _ q r) = p : nub (subProps q ++ subProps r)
\end{code}

Below is the code for Question 1.9
For the truth table, we need first to figure out which variables are in the propositional formula.
After get the variables in the propostional formula, we need to delete the duplicate by using |nub|.

\begin{code}
listVar :: Prop -> [Variable]
listVar (Var p) = [p]
listVar (Negation q) = listVar q
listVar (BinOp _ q r) = (listVar q ++ listVar r)
delDup :: Prop -> [Variable]
delDup = nub . listVar
\end{code}

Then using list comprehension to get the combination of all the variable's boolean value first.

\begin{code}
table :: [Variable] -> [[(Variable,Bool)]]
table [] = [[]]
table (varChar:folist) = [ (varChar,p):after | p <- [True,False],after <- table folist] 
\end{code}

Before generating the real truthtable, we need to give the rule for getting boolean result of And,Or....

\begin{code}
getBool :: Prop -> [(Variable,Bool)] -> Bool
getBool (Var p) ta = fromJust (lookup p ta)
getBool (Negation p) ta = not (getBool p ta)
getBool (BinOp And p q) ta = (getBool p ta) && (getBool q ta)
getBool (BinOp Or p q) ta = (getBool p ta) || (getBool q ta)
getBool (BinOp Implies p q) ta = not (getBool p ta) || (getBool q ta) 
getBool (BinOp Equiv p q) ta = (not (getBool p ta) || (getBool q ta)) && (not (getBool q ta) || (getBool p ta)) 
\end{code}

Now, we can get the real truthTable we need.
\begin{code}
truthTable :: Prop -> [([(Variable,Bool)],Bool)]
truthTable prop = [(bs, getBool prop bs) | bs <- table (delDup prop)]
\end{code}

Although we can get the truthtable now, we need to print it out in an arranged form.

\begin{code}
rangeTable :: [([(Variable,Bool)],Bool)] -> String
rangeTable [] = "\n"
rangeTable (x:xs) = (show x) ++ "\n" ++ (rangeTable xs)
 
realTable :: Prop -> IO ()
realTable prop = putStrLn ("The formule is " ++ (show prop) ++ "\n" ++ (rangeTable (truthTable prop)))
\end{code}

\section{Convenience Functions for Formula Construction}

To make  formula construction in programs and in GHCi easier,
we define infix operators for the binary junctors,
let them all associate to the right,
and impose the same precedence ordering as Z:

\begin{code}
lnot p = Negation p
p &&& q = BinOp And p q
p ||| q = BinOp Or p q
p ==> q = BinOp Implies p q
p <=> q = BinOp Equiv p q

infixr 7 &&&
infixr 6 |||
infixr 5 <=>
infixr 4 ==>
\end{code}

Another step that helps with example formula construction
is providing simple names for the some frequently-used propositional
variables:

\begin{code}
p = Var 'p'
q = Var 'q'
r = Var 'r'
s = Var 's'
\end{code}

With all this, defining example propositions becomes easy:

\begin{code}
prop1 = (p ==> q) ==> ((q ==> r) ==> (p ==> r))
prop2 = lnot p ==> (p ==> (p ==> q))
prop3= ((p ==> lnot q) ==> lnot p) ==> q
prop4= (lnot q &&& (p ==> r)) &&& (r ==> q)
prop5= lnot (q ||| r <=> s) ==> lnot (p ==> r) ||| s &&& (r ==> p)
\end{code}

\section{|Show| --- Conversion to Strings}

The choice of operator symbols can be encapsulated in the
function |showOp| that is completely independent of the |Prop| context:

\begin{code}
showOp :: Op -> String
showOp And      = "&"
showOp Or       = "|"
showOp Implies  = "=>"
showOp Equiv    = "<=>"

instance Show Op where show = showOp
\end{code}

Code for the Assignment 1.8 (f)
I just change this part of code to produce a minimum precences, I will change the truthtable part
in the weekend. Thank u for ur feedback
\begin{code}
showMinProp :: Int -> Prop -> String
showMinProp _ (Var s) = show s
showMinProp _ (Negation p) = "~" ++ showMinProp 9 p
showMinProp preNo (BinOp op p q) =
     let a = case op of 
               And -> 7
               Or  -> 6
               Implies -> 5
               Equiv   -> 4
     in (if preNo > a then paren else id)
        (showMinProp a p ++ space (showOp op) ++ showMinProp a q)

space s = " " ++ s ++ " "
paren s = "(" ++ s ++ ")"

instance Show Prop where show = showMinProp 0
\end{code}

\begin{verbatim}
<prop>             ::= <implies> "==>" <prop> | <implies>
<implies>          ::= <equiv> "==>" <implies> | <equiv>
<equiv>            ::= <or> "<=>" <equiv> | <or>
<or>               ::= <and> "|||" <or> | <and>
<and>              ::= <lnot> "&&&" <and> | <nega>
<nega>             ::= "lnot" <nega> | <var>
<var>              ::= "p" | "q" | "r" | "s" | "(" <prop> ")"
\end{verbatim}

\begin{code}
parseProp    :: String -> (Prop,String)
parseImplies :: String -> (Prop,String)
parseEquiv   :: String -> (Prop,String)
parseOr      :: String -> (Prop,String)
parseAnd     :: String -> (Prop,String)
parseNega    :: String -> (Prop,String)
parseVar     :: String -> (Prop,String)

parseProp cs = let (i,cs') = parseImplies cs in case cs' of
          "==>" : cs'' -> let (p,cs''') = parseProp cs'' in (BinOp Implies i p, cs''')
          _  -> (i,cs')     

parseImplies cs = let (e,cs') = parseEquiv cs in case cs' of
		  "<=>" : cs'' -> let (i,cs''') = parseImplies cs'' in (BinOp Equiv e i, cs''')
          _  -> (e,cs')

parseEquiv cs = let (o,cs') = parseOr cs in case cs' of
          "|||" : cs'' -> let (e,cs''') = parseEquiv cs'' in (BinOp Or o e, cs''')
          _  -> (o,cs')

parseOr cs = let (a,cs') = parseAnd cs in case cs' of
          "&&&" : cs'' -> let (o,cs''') = parseOr cs'' in (BinOp And a o, cs''')
          _  -> (a,cs')

parseAnd cs = let (n,cs') = parseNega cs in case cs' of
          "lnot" : cs'' -> let (a,cs''') = parseAnd cs'' in (lnot a, cs''')
          _  -> (n,cs')

parseNega cs = let (v,cs') = parseVar cs in case cs' of
          'p' : cs'' -> let (n,cs''') = parseNega cs'' in (Var n, cs''')
          'q' : cs'' -> let (n,cs''') = parseNega cs'' in (Var n, cs''')
          'r' : cs'' -> let (n,cs''') = parseNega cs'' in (Var n, cs''')
          's' : cs'' -> let (n,cs''') = parseNega cs'' in (Var n, cs''')
          _  -> (v,cs')

parseVar ('(':cs) = let (e,cs') = parseProp cs in case cs' of
                        ')' : cs'' -> (e,cs'')
                        _   -> error "closing parenthesis expected"

parseVar (c:cs) = let (ident,cs') = parseRest [c] cs
                  in (Var ident,cs')

parseRest :: String -> String -> (String,String)
parseRest s cs = (s,cs)           

\end{code}