implementation module Logic

import StdEnv

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

instance toString Op1
where
    toString Not = "~"

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

instance toString Expr
where
    toString (B True) = toString 1
    toString (B False) = toString 0
    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

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