import Type.Proposition
import Data.List

derive :: Bool -> Sequent -> Derivation
derive mode s@(Sequent sx xd)
derive :: Sequent -> Derivation
derive s@(Sequent sx xd)
    | TTrue `elem` xd    = Axiom s "ax-tt"
    | FFalse `elem` sx   = Axiom s "ax-⊥"
    | compareList sx xd  = Axiom s "ax-id"
    | not $ allAtomTTrueFFalseOrNull sx = case sh of
        Not a      -> NormalDerivation s [derive mode (Sequent (tail sx) (a:xd))]                                       (if mode then "$ \neg -S$"       else "¬-S")
        And a b    -> NormalDerivation s [derive mode (Sequent (a:b:tail sx) xd)]                                       (if mode then "$ and -S$"         else "&-S")
        Or a b     -> NormalDerivation s [derive mode (Sequent (a:tail sx) xd), derive mode (Sequent (b:tail sx) xd)]   "∨-S"
        Imply a b  -> NormalDerivation s [derive mode (Sequent (tail sx) (a:xd)), derive mode (Sequent (b:tail sx) xd)] (if mode then "$ \rightarrow -S$" else "→-S")
        a@(Atom _) -> NormalDerivation s [derive mode (Sequent (tail sx ++ [a]) xd)]                                    "sc-S"
        Not a      -> NormalDerivation s [derive (Sequent (tail sx) (a:xd))]                                  $ Action LLeft Negate
        And a b    -> NormalDerivation s [derive (Sequent (a:b:tail sx) xd)]                                  $ Action LLeft Anded
        Or a b     -> NormalDerivation s [derive (Sequent (a:tail sx) xd), derive (Sequent (b:tail sx) xd)]   $ Action LLeft Ored
        Imply a b  -> NormalDerivation s [derive (Sequent (tail sx) (a:xd)), derive (Sequent (b:tail sx) xd)] $ Action LLeft Implied
        a@(Atom _) -> NormalDerivation s [derive (Sequent (tail sx ++ [a]) xd)]                               $ Action LLeft Swap
    | not $ allAtomTTrueFFalseOrNull xd = case dh of
        Not a      -> NormalDerivation s [derive mode (Sequent (a:sx) (tail xd))]                                       (if mode then "$ \neg -D$"       else "¬-D")
        And a b    -> NormalDerivation s [derive mode (Sequent sx (a:tail xd)), derive mode (Sequent sx (b:tail xd))]   (if mode then "$ and -D$"         else "&-D")
        Or a b     -> NormalDerivation s [derive mode (Sequent sx (a:b:tail xd))]                                       "∨-D"
        Imply a b  -> NormalDerivation s [derive mode (Sequent (a:sx) (b:tail xd))]                                     (if mode then "$ \rightarrow -D$" else "→-D")
        a@(Atom _) -> NormalDerivation s [derive mode (Sequent sx (tail xd ++ [a]))]                                    "sc-D"
        Not a      -> NormalDerivation s [derive (Sequent (a:sx) (tail xd))]                                  $ Action RRight Negate
        And a b    -> NormalDerivation s [derive (Sequent sx (a:tail xd)), derive (Sequent sx (b:tail xd))]   $ Action RRight Anded
        Or a b     -> NormalDerivation s [derive (Sequent sx (a:b:tail xd))]                                  $ Action RRight Ored
        Imply a b  -> NormalDerivation s [derive (Sequent (a:sx) (b:tail xd))]                                $ Action RRight Implied
        a@(Atom _) -> NormalDerivation s [derive (Sequent sx (tail xd ++ [a]))]                               $ Action RRight Swap
    | otherwise = NotDerivable s
    where
      sh = head sx