module HR where
import Prop
import Tactics

--  Rules following Huth and Ryan
--  This is approximately Gentzen's NK cast as sequents

type Rule a = Sequent a -> Maybe [Sequent a]

andI :: Rule a
andI (Sequent gamma (AndP p q)) = Just [Sequent gamma  p, 
                                        Sequent gamma  q]
andI _ = Nothing

andE1 :: Prop a -> Rule a
andE1 psi (Sequent gamma  phi) = Just [Sequent gamma (AndP phi psi)]

andE2 :: Prop a -> Rule a
andE2 psi (Sequent gamma  phi) = Just [Sequent gamma (AndP psi phi)]

orI1 :: Rule a
orI1 (Sequent gamma (OrP p _)) = Just [Sequent gamma p]
orI1 _ = Nothing

orI2 :: Rule a
orI2 (Sequent gamma (OrP _ q)) = Just [Sequent gamma q]
orI2 _ = Nothing

orE :: Prop a -> Rule a
orE r@(OrP p q) (Sequent gamma x) = Just [Sequent gamma r, 
                                          Sequent (p:gamma) x, 
                                          Sequent (q:gamma) x]
orE _ _ = Nothing

impliesI :: Rule a
impliesI (Sequent gamma (ImpliesP p q)) = Just [Sequent (p:gamma) q]
impliesI _                              = Nothing

impliesE :: Prop a -> Rule a
impliesE psi (Sequent gamma phi) = return [Sequent gamma (ImpliesP psi phi),
                                           Sequent gamma  psi]

notI :: Rule a
notI (Sequent gamma (NotP p)) = Just [Sequent (p:gamma) AbsurdP]
notI _ = Nothing

notE :: Prop a -> Rule a
notE psi (Sequent gamma AbsurdP) = Just [Sequent gamma  psi, 
                                         Sequent gamma  (NotP psi)]
notE _ _ = Nothing

absurdE :: Rule a
absurdE (Sequent gamma phi) = Just [Sequent gamma  AbsurdP]

notNotI :: Rule a
notNotI (Sequent gamma (NotP (NotP p))) = Just [(Sequent gamma  p)]
notNotI _ = Nothing

notNotE :: Rule a
notNotE (Sequent gamma p) = Just [(Sequent gamma  (NotP (NotP p)))]

truthI :: Rule a
truthI (Sequent gamma TruthP) = Just []
truthI _ = Nothing

hyp :: (Eq a) => Int -> Rule a
hyp n (Sequent gamma phi) = if phi == gamma !! (n-1) then Just [] else Nothing

-- A more user friendly rule that uses a search tactical to hide the index into the list:

hypothesis :: (Eq a) => Rule a
hypothesis = tryL hyp

-- Sequent type specific tacticals:

tryL :: (Int -> Rule a) -> Rule a
tryL r (Sequent hs g) = (oneOf $ map (\i -> r i) [1..length hs]) (Sequent hs g)

-- A very very naive tactic to assist -> elimination
--  Please improve!

helpfulImplies (Sequent [] phi) = []
helpfulImplies (Sequent ((ImpliesP p q):gamma) phi)
                | q == phi   = p:(helpfulImplies (Sequent gamma phi))
helpfulImplies (Sequent (_:gamma) phi) = helpfulImplies (Sequent gamma phi)

impliesESimple s = case helpfulImplies s of
                       (phi:_) -> impliesE phi s
                       [] -> Nothing


fixup (Just t:ts) = t:(fixup ts)
fixup (Nothing:ts) = fixup ts
fixup [] = []