implementation module Logic

import StdEnv, StringUtils

isBool  :: Expr -> Bool
isBool (B _) = True
isBool _ = False

isAtom  :: Expr -> Bool
isAtom (Atom _) = True
isAtom _ = False

isApp1  :: Expr -> Bool
isApp1 (App1 _ _) = True
isApp1 _ = False

isApp2  :: Expr -> Bool
isApp2 (App2 _ _ _) = True
isApp2 _ = False

isApp   :: Expr -> Bool
isApp e = isApp1 e || isApp2 e

isNot   :: Expr -> Bool
isNot (App1 Not _) = True
isNot _ = False

isAnd   :: Expr -> Bool
isAnd (App2 _ And _) = True
isAnd _ = False

isOr    :: Expr -> Bool
isOr (App2 _ Or _) = True
isOr _ = False

isImpl  :: Expr -> Bool
isImpl (App2 _ Impl _) = True
isImpl _ = False

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 = "~"

instance toString Op2
where
    toString And = "&"
    toString Or = "|"
    toString Impl = "->"
    toString Equiv = "<->"

instance toString Expr
where
    toString (B b) = toString b
    toString (Atom a) = toString a
    toString (App1 op e)
    | needs_parentheses (App1 op e) = toString op +++ "(" +++ toString e +++ ")"
    | otherwise = toString op +++ toString e
    toString (App2 e1 op e2) = e1` +++ " " +++ toString op +++ " " +++ e2`
    where
        e1`
        | needs_parentheses_left (App2 e1 op e2) = "(" +++ toString e1 +++ ")"
        | otherwise = toString e1
        e2`
        | 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]
    where
        row_b = " "     // Row / Line begin, end, separator
        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

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
needs_parentheses (App1 Not (App1 Not _)) = False
needs_parentheses _ = True

needs_parentheses_left :: Expr -> Bool
needs_parentheses_left (App2 (B _) _ _) = False
needs_parentheses_left (App2 (Atom _) _ _) = False
needs_parentheses_left (App2 (App1 Not _) _ _) = False
needs_parentheses_left (App2 (App2 _ op1 _) op2 _) = binds_stronger op2 op1

needs_parentheses_right :: Expr -> Bool
needs_parentheses_right (App2 _ _ (B _)) = False
needs_parentheses_right (App2 _ _ (Atom _)) = False
needs_parentheses_right (App2 _ _ (App1 Not _)) = False
needs_parentheses_right (App2 _ op1 (App2 _ op2 _)) = not (binds_stronger op2 op1)

// Associativity rules
binds_stronger :: Op2 Op2 -> Bool
binds_stronger _ And = False        // And is left-associative
binds_stronger And _ = True
binds_stronger Or _ = True          // The rest is right-associative
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 _ = []

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}