{-# LANGUAGE RankNTypes #-}
-----------------------------------------------------------------------------
-- Copyright 2014, Open Universiteit Nederland. This file is distributed
-- under the terms of the GNU General Public License. For more information,
-- see the file "LICENSE.txt", which is included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- Exercise for the logic domain: to prove two propositions equivalent
--
-----------------------------------------------------------------------------
--  $Id: Proofs.hs 6548 2014-05-16 10:34:18Z bastiaan $

module Domain.Logic.Proofs
   ( proofExercise, proofUnicodeExercise
   , sortRuleOr, sortRuleAnd -- fix me
   ) where

import Control.Arrow
import Control.Monad
import Data.Foldable (toList)
import Data.Function (on)
import Data.List
import Data.Maybe
import Domain.Logic.BuggyRules
import Domain.Logic.Examples
import Domain.Logic.Exercises
import Domain.Logic.Formula
import Domain.Logic.GeneralizedRules
import Domain.Logic.Generator (equalLogicA)
import Domain.Logic.InverseRules
import Domain.Logic.Parser
import Domain.Logic.Rules
import Domain.Logic.Strategies (somewhereOr)
import Domain.Logic.Utils
import Domain.Math.Expr ()
import Ideas.Common.Library
import Ideas.Common.Traversal.Navigator
import Ideas.Common.Traversal.Utils
import Ideas.Common.Utils

{-
see :: Int -> IO ()
see n = do
   let a   = snd (examples proofExercise !! n)
       der = defaultDerivation proofExercise a
   printDerivation proofExercise a
   putStrLn $ ">> " ++ show (derivationLength der) ++ " steps\n"
-}

-- Currently, we use the DWA strategy
proofExercise :: Exercise Proof
proofExercise = makeExercise
   { exerciseId     = describe "Prove two propositions equivalent" $
                         propositionalId # "proof"
   , status         = Experimental
   , parser         = mapSecond makeProof . parseLogicProof False
   , prettyPrinter  = showProof
   , equivalence    = withoutContext equivalentProofs
   , similarity     = withoutContext similarProofs
   , suitable       = predicate $ all (uncurry eqLogic) . subProofs
   , ready          = predicate $ all (uncurry equalLogicA) . subProofs
   , strategy       = proofStrategy
   , extraRules     = map use extraLogicRules ++ inverseRules ++ map use buggyRules
   , navigation     = termNavigator
   , examples       = map (second makeProof) exampleProofs
   }

proofUnicodeExercise :: Exercise Proof
proofUnicodeExercise = proofExercise
   { exerciseId    = describe "Prove two propositions equivalent (unicode support)" $
                        propositionalId # "proof.unicode"
   , parser        = mapSecond makeProof . parseLogicProof True
   , prettyPrinter = showProofUnicode
   }

type Proof = Logic (SLogic, SLogic)

subProofs :: Proof -> [(SLogic, SLogic)]
subProofs = toList

makeProof :: (SLogic, SLogic) -> Proof
makeProof = Var

proofPair :: Proof -> (SLogic, SLogic)
proofPair x = (catLogic (fmap fst x), catLogic (fmap snd x))

showProof :: Proof -> String
showProof = uncurry f . proofPair
 where
   f p q = ppLogicPars p ++ " == " ++ ppLogicPars q

showProofUnicode :: Proof -> String
showProofUnicode = uncurry f . proofPair
 where
   f p q = ppLogicUnicodePars p ++ " == " ++ ppLogicUnicodePars q

equivalentProofs :: Proof -> Proof -> Bool
equivalentProofs proof1 proof2 =
   let (p1, q1) = proofPair proof1
       (p2, q2) = proofPair proof2
   in eqLogic p1 p2 && eqLogic q1 q2

similarProofs :: Proof -> Proof -> Bool
similarProofs proof1 proof2 =
   let (p1, q1) = proofPair proof1
       (p2, q2) = proofPair proof2
   in equalLogicA p1 p2 && equalLogicA q1 q2

proofStrategy :: LabeledStrategy (Context Proof)
proofStrategy = label "proof equivalent" $
   repeatS (
         somewhere splitTop
      -- disabled: first investigate how the common subexpressions should be
      -- communicated to the client
      -- |> somewhere commonExprAtom
      |> useC dnfStrategyDWA
      |> commonLiteralSpecial
      |> useC orToTop
      |> (use checkDNF <*> commonLiteral)
      )
      <*> use checkDNF <*> normStrategy
 where
   splitTop =  use topIsNot  <|> use topIsImpl
               -- only use commutativity if not already in desired order
           <|> (use topIsAnd |> use topIsAndCom)
           <|> (use topIsOr  |> use topIsOrCom)
           <|> use topIsEquiv

commonLiteralSpecial :: Strategy (Context Proof)
commonLiteralSpecial =
   repeat1 (somewhere (use ruleCommonLiteralSpecialInFront))
   <*>
   repeat1 (somewhere (use ruleInvDistrCommonLiteral))
   <*>
   repeatS (somewhere (use topIsAnd))

ruleCommonLiteralSpecialInFront :: Rule Proof
ruleCommonLiteralSpecialInFront = makeRule "command.common-literal-special" f
 where
   f (Var eq) =
      [ Var x | x <- maybeToList (findInFrontLeft eq) ] ++
      [ Var (swap x) | x <- maybeToList (findInFrontLeft (swap eq)) ]
   f _ = []

   findInFrontLeft eq@(p1 :&&: p2, q)
      | isAtomic p1 && isDNF p2 && all (`notElem` varsLogic p2) (varsLogic p1) && isDNF q = do
           lit <- listToMaybe (findCommonLiteral (p1, q))
           res <- inFrontLeft lit (swap eq)
           return (swap res)
   findInFrontLeft _ = Nothing

checkDNF :: Rule Proof
checkDNF = minor $ makeRule "is-dnf" $ \proof -> do
   guard $ and [ isDNF p && isDNF q | (p, q) <- subProofs proof ]
   Just proof

normStrategy :: Strategy (Context Proof)
normStrategy = repeatS $
      somewhere (use ruleFalseZeroAnd <|> use ruleTrueZeroOr)
   |> somewhere (use ruleComplAnd)
   |> somewhere (
         use ruleIdempOr   <|>
         use ruleIdempAnd  <|>
         use ruleAndOverOr <|>
         use ruleFalseZeroOr
      )
   |> oncetd (use sortRuleAnd)
   |> oncetd (use sortRuleOr)
   |> somewhereDisjunct introduceVar

sortRuleBy :: (b -> b -> Ordering) -> View a [b] -> Transformation a
sortRuleBy cmp v = makeTrans $ \p -> do
   xs <- match v p
   guard (not (sortedBy cmp xs))
   let ys = sortBy cmp xs
   return (build v ys)

sortRuleOr :: Rule SLogic
sortRuleOr = ruleTrans "CommOr.sort" $
   sortRuleBy compareVar $ disjunctions <-> ors

sortRuleAnd :: Rule SLogic
sortRuleAnd = ruleTrans "CommAnd.sort" $
   sortRuleBy compareVar $ conjunctions <-> ands

compareVar :: Ord a => Logic a -> Logic a -> Ordering
compareVar = compare `on` (\x -> (varsLogic x, x))

sortedBy :: (a -> a -> Ordering) -> [a] -> Bool
sortedBy cmp = rec
 where
   rec (x:y:zs) = cmp x y /= GT && rec (y:zs)
   rec _        = True

-----------------------------------------------------------------------------
-- To DNF, with priorities (the "DWA" approach)

dnfStrategyDWA :: Strategy (Context SLogic)
dnfStrategyDWA =
   toplevel <|> somewhereOr
      (  label "Simplify"                            simpler
      |> label "Sort and simplify"                   (sortAndSimplify |> deMorganAndSimplify)
      |> label "Eliminate implications/equivalences" eliminateImplEquiv
      |> label "Eliminate nots"                      eliminateNots
      )
 where
    toplevel = useRules
       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleIdempOr
       , ruleAbsorpOr, ruleComplOr
       ]
    simpler = somewhere $ useRules
       [ ruleFalseZeroOr, ruleTrueZeroOr, ruleTrueZeroAnd
       , ruleFalseZeroAnd, ruleNotTrue, ruleNotFalse
       , ruleNotNot, ruleIdempOr, ruleIdempAnd, ruleAbsorpOr, ruleAbsorpAnd
       , ruleComplOr, ruleComplAnd
       ]
    sortAndSimplify = somewhere $
           use ruleAbsorpOrNot
       <|> use sortForIdempOr
       <|> use sortForIdempAnd
       <|> use sortForComplOr
       <|> use sortForComplAnd
    deMorganAndSimplify = somewhere $
           deMorganOrNot <|> deMorganAndNot
    eliminateImplEquiv =
           somewhere (use ruleDefImpl)  -- preference: top-down!
        |> somewhere (use ruleDefEquiv) -- preference: bottom-up!

    eliminateNots = somewhere $ useRules
       [ generalRuleDeMorganAnd, generalRuleDeMorganOr
       , ruleDeMorganAnd, ruleDeMorganOr
       ]

orToTop :: LabeledStrategy (Context SLogic)
orToTop = label "Move ors to top" $ somewhere $ useRules
   [ generalRuleAndOverOr, ruleAndOverOr ]

useRules :: [Rule SLogic] -> Strategy (Context SLogic)
useRules = alternatives . map liftToContext

-- disabled for now

-- Find a common subexpression that can be treated as a box
{-
commonExprAtom :: Rule (Context Proof)
commonExprAtom = minor $ ruleTrans "commonExprAtom" $ makeTransLiftContext $ \proof ->
   case proof of
      Var (p, q) -> do
         sub <- substRef :? []
         let xs = filter (same <&&> complement isAtomic) (largestCommonSubExpr p q)
             same cse = eqLogic (substitute cse p) (substitute cse q)
             used = varsLogic p `union` varsLogic q `union` map (ShowString . fst) sub
             new  = head (logicVars \\ used)
             substitute a this
                | a == this = Var new
                | otherwise = descend (substitute a) this
         case xs of
            hd:_ -> do
               substRef := (show new, show hd):sub
               return (Var (substitute hd p, substitute hd q))
            _ -> fail "not applicable"
      _ -> fail "not applicable"

largestCommonSubExpr :: (Uniplate a, Ord a) => a -> a -> [a]
largestCommonSubExpr x = rec
 where
   uniX  = S.fromList (universe x)
   rec y | y `S.member` uniX = [y]
         | otherwise         = concatMap rec (children y)

substRef :: Ref [(String, String)]
substRef = makeRef "subst"

logicVars :: [ShowString]
logicVars = [ ShowString [c] | c <- ['a'..] ]
-}
--------------------------------------------------------------------

-- p \/ q \/ ~p  ~>  reorder p and ~p
sortForComplOr :: Rule SLogic
sortForComplOr = ruleMaybe "ComplOr.sort" $ \p -> do
   let xs = disjunctions p
       ys = sortBy compareVar xs
   guard (xs /= ys && any (\x -> Not x `elem` xs) xs)
   return (ors ys)

-- p /\ q /\ ~p  ~>  reorder p and ~p
sortForComplAnd :: Rule SLogic
sortForComplAnd = ruleMaybe "ComplAnd.sort" $ \p -> do
   let xs = conjunctions p
       ys = sortBy compareVar xs
   guard (xs /= ys && any (\x -> Not x `elem` xs) xs)
   return (ands ys)

-- p \/ q \/ p      ~> reorder p's
sortForIdempOr :: Rule SLogic
sortForIdempOr = ruleMaybe "IdempOr.sort" $ \p -> do
   let xs = disjunctions p
       ys = sortBy compareVar xs
   guard (xs /= ys && not (distinct xs))
   return (ors ys)

-- p /\ q /\ p      ~> reorder p's
sortForIdempAnd :: Rule SLogic
sortForIdempAnd = ruleMaybe "IdempAnd.sort" $ \p -> do
   let xs = conjunctions p
       ys = sortBy compareVar xs
   guard (xs /= ys && not (distinct xs))
   return (ands ys)

acTopRuleFor :: Bool -> (forall a . Isomorphism (Logic a) [Logic a])
             -> Transformation Proof
acTopRuleFor com iso = makeTrans $ \proof -> do
   (lhs, rhs) <- maybeToList (getSingleton proof)
   let as = from iso lhs
       bs = from iso rhs
       splitter = if com then divide else split
   (as1, as2, bs1, bs2) <- splitTwoLists splitter as bs
   let eqList xs ys = eqLogic (to iso xs) (to iso ys)
   guard (eqList as1 bs1 && eqList as2 bs2)
   return $ to iso
      [ Var (to iso as1, to iso bs1)
      , Var (to iso as2, to iso bs2)
      ]

splitTwoLists :: (forall t . [t] -> [([t], [t])])
              -> [a] -> [b] -> [([a], [a], [b], [b])]
splitTwoLists f as bs =
   [ (as1, as2, bs1, bs2)
   | (as1, as2) <- f as
   , not (null as1 || null as2)
   , (bs1, bs2) <- f bs
   , not (null bs1 || null bs2)
   ]

split :: [a] -> [([a], [a])] -- associative
split as = [ splitAt i as | i <- [1..length as-1] ]

divide :: [a] -> [([a], [a])] -- associative + commutative
divide = foldr op [([], [])]
 where
   op a xs = map addLeft xs ++ map addRight xs
    where
      addLeft  (ys, zs) = (a:ys, zs)
      addRight (ys, zs) = (ys, a:zs)

topIsAnd :: Rule Proof
topIsAnd = minor $ ruleTrans "top-is-and" $ acTopRuleFor False (collect andView)

topIsOr :: Rule Proof
topIsOr = minor $ ruleTrans "top-is-or" $ acTopRuleFor False (collect orView)

topIsEquiv :: Rule Proof
topIsEquiv = minor $ ruleTrans "top-is-equiv"  $ acTopRuleFor False (collect eqView)

topIsAndCom :: Rule Proof
topIsAndCom = ruleTrans "top-is-and.com" $ acTopRuleFor True (collect andView)

topIsOrCom :: Rule Proof
topIsOrCom = ruleTrans "top-is-or.com" $ acTopRuleFor True (collect orView)

--topIsEquivCom :: Rule Proof
--topIsEquivCom = ruleTrans "top-is-equiv.com"  $ acTopRuleFor True (collect eqView)

topIsImpl :: Rule Proof
topIsImpl = minorRule "top-is-impl" f
 where
   f (Var (p :->: q, r :->: s)) = do
      guard (eqLogic p r && eqLogic q s)
      return (Var (p, r) :->: Var (q, s))
   f _ = Nothing

topIsNot :: Rule Proof
topIsNot = minorRule "top-is-not" f
 where
   f (Var (Not p, Not q)) = Just (Not (Var (p, q)))
   f _ = Nothing

{- Strategie voor sterke(?) normalisatie

(prioritering)

1. p \/ q \/ ~p     ~> T           (propageren)
   p /\ q /\ p      ~> p /\ q
   p /\ q /\ ~p     ~> F           (propageren)

2. (p /\ q) \/ ... \/ (p /\ q /\ r)    ~> (p /\ q) \/ ...
         (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes)
   p \/ ... \/ (~p /\ q /\ r)  ~> p \/ ... \/ (q /\ r)
         (p is hier een losse variabele)
   ~p \/ ... \/ (p /\ q /\ r)  ~> ~p \/ ... \/ (q /\ r)
         (p is hier een losse variabele)

3. a) elimineren wat aan een kant helemaal niet voorkomt (zie regel hieronder)
   b) rijtjes sorteren
   c) rijtjes aanvullen

Twijfelachtige regel bij stap 3: samennemen in plaats van aanvullen:
   (p /\ q /\ r) \/ ... \/ (~p /\ q /\ r)   ~> q /\ r
          (p is hier een losse variable)
-}

-----------------------------------------------
-- Introduction of var

introduceVar :: Strategy (Context Proof)
introduceVar =  check missing
            <*> use introTrueLeft
            <*> layer [] introCompl

missing :: Context Proof -> Bool
missing = isJust . missingVar

localEqVars :: Context Proof -> [ShowString]
localEqVars cp =
   case currentTerm cp >>= fromTerm of
      Just (p, q) -> varsLogic p `union` varsLogic q
      Nothing     -> maybe [] localEqVars (up cp)

missingVar :: Context Proof -> Maybe ShowString
missingVar cp =
   case currentTerm cp >>= fromTerm of
      Just p  -> listToMaybe (localEqVars cp \\ varsLogic p)
      Nothing -> Nothing

introTrueLeft :: Rule SLogic
introTrueLeft = rewriteRule "IntroTrueLeft" $
   \x -> x  :~>  T :&&: x

introCompl :: Rule (Context Proof)
introCompl = makeRule "IntroCompl" $ \cp -> do
   a <- missingVar (safe up cp)
   let f = fromTerm >=> fmap toTerm . introTautology a
   changeTerm f cp
 where
   introTautology :: a -> Logic a -> Maybe (Logic a)
   introTautology a T = Just (Var a :||: Not (Var a))
   introTautology _ _ = Nothing

 {-
go = applyAll (somewhereDisjunct introduceVar) $ inContext proofExercise $
   makeProof (p :||: (Not p :&&: q), p :||: q)
 where
   p = Var (ShowString "p")
   q = Var (ShowString "q")

somewhereEq :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof)
somewhereEq s = traverse [once, topdown]
   (check isEq <*> layer [] s)
 where
   isEq :: Context Proof -> Bool
   isEq cp = fromMaybe False $ do
      t <- currentTerm cp
      case fromTerm t :: Maybe (SLogic, SLogic) of
         Just (p, q) -> return True
         _           -> return False -}

somewhereDisjunct :: IsStrategy f => f (Context Proof) -> Strategy (Context Proof)
somewhereDisjunct s = oncetd (check isEq <*> layer [] (somewhereOrG s))
 where
   isEq :: Context Proof -> Bool
   isEq cp = (isJust :: Maybe (SLogic, SLogic) -> Bool)
             (currentTerm cp >>= fromTerm :: Maybe (SLogic, SLogic))

somewhereOrG :: IsStrategy g => g (Context a) -> Strategy (Context a)
somewhereOrG s =
   let curIsOr a = case currentTerm a >>= (fromTerm :: Term -> Maybe SLogic) of
                      Just (_ :||: _) -> True
                      _               -> False
   in fix $ \this -> check (Prelude.not . curIsOr) <*> s
                 <|> check curIsOr <*> layer [] this

----------------------

ruleAbsorpOrNot :: Rule SLogic
ruleAbsorpOrNot = rewriteRules "DistrOrNot"
   [ -- not inside
     \x y -> x :||: (Not x :&&: y)  :~>  (x :||: Not x) :&&: (x :||: y)
   , \x y -> x :||: (y :&&: Not x)  :~>  (x :||: y) :&&: (x :||: Not x)
   , \x y -> (Not x :&&: y) :||: x  :~>  (Not x :||: x) :&&: (y :||: x)
   , \x y -> (y :&&: Not x) :||: x  :~>  (y :||: x) :&&: (Not x :||: x)
     -- not outside
   , \x y -> Not x :||: (x :&&: y)  :~>  (Not x :||: x) :&&: (Not x :||: y)
   , \x y -> Not x :||: (y :&&: x)  :~>  (Not x :||: y) :&&: (Not x :||: x)
   , \x y -> (x :&&: y) :||: Not x  :~>  (x :||: Not x) :&&: (y :||: Not x)
   , \x y -> (y :&&: x) :||: Not x  :~>  (y :||: Not x) :&&: (x :||: Not x)
   ]

-- specialization of De Morgan rules with a not inside (gives higher priority)
deMorganOrNot :: Strategy (Context SLogic)
deMorganOrNot = check p <*> (use ruleDeMorganOr <|> use generalRuleDeMorganOr)
 where
   p :: Context SLogic -> Bool
   p ctx = case currentInContext ctx of
              Just (Not x) ->
                 let ys = disjunctions x
                 in length ys > 1 && any isNot ys
              _ -> False

deMorganAndNot :: Strategy (Context SLogic)
deMorganAndNot = check p <*> (use ruleDeMorganAnd <|> use generalRuleDeMorganAnd)
 where
   p :: Context SLogic -> Bool
   p ctx = case currentInContext ctx of
              Just (Not x) ->
                 let ys = conjunctions x
                 in length ys > 1 && any isNot ys
              _ -> False

{-
ruleAbsorpAndNot :: Rule SLogic
ruleAbsorpAndNot = rewriteRules "AbsorpAndNot.distr"
   [ -- not inside
     \x y -> x :&&: (Not x :||: y)  :~>  (x :&&: Not x) :||: (x :&&: y)
   , \x y -> x :&&: (y :||: Not x)  :~>  (x :&&: y) :||: (x :&&: Not x)
   , \x y -> (Not x :||: y) :&&: x  :~>  (Not x :&&: x) :||: (y :&&: x)
   , \x y -> (y :||: Not x) :&&: x  :~>  (y :&&: x) :||: (Not x :&&: x)
     -- not outside
   , \x y -> Not x :&&: (x :||: y)  :~>  (Not x :||: x) :&&: (Not x :||: y)
   , \x y -> Not x :&&: (y :||: x)  :~>  (Not x :||: y) :&&: (Not x :||: x)
   , \x y -> (x :||: y) :&&: Not x  :~>  (x :||: Not x) :&&: (y :||: Not x)
   , \x y -> (y :||: x) :&&: Not x  :~>  (y :||: Not x) :&&: (x :||: Not x)
   ] -}

-----------------------------------------------------------------------------
-- Inverse rules

inverseRules :: [Rule (Context Proof)]
inverseRules = map use [invDefImpl, invDefEquiv, invNotNot, invIdempOr, invIdempAnd,
   invTrueZeroAnd, invNotTrue, invFalseZeroOr, invNotFalse] ++
   [ invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd
   , invComplAnd, invAndOverOr, invOrOverAnd]

invDefImpl :: Rule SLogic
invDefImpl = rewriteRule "DefImpl.inv" $
   \x y -> Not x :||: y  :~>  x :->: y

invDefEquiv :: Rule SLogic
invDefEquiv = rewriteRule "DefEquiv.inv" $
   \x y -> (x :&&: y) :||: (Not x :&&: Not y)  :~>  x :<->: y

invNotNot :: Rule SLogic
invNotNot = rewriteRule "NotNot.inv" $
   \x -> x  :~>  Not (Not x)

invIdempOr :: Rule SLogic
invIdempOr = rewriteRule "IdempOr.inv" $
   \x -> x  :~>  x :||: x

invIdempAnd :: Rule SLogic
invIdempAnd = rewriteRule "IdempAnd.inv" $
   \x -> x :~> x :&&: x

invTrueZeroAnd :: Rule SLogic
invTrueZeroAnd = rewriteRules "TrueZeroAnd.inv"
   [ \x -> x  :~>  T :&&: x
   , \x -> x  :~>  x :&&: T
   ]

invNotTrue :: Rule SLogic
invNotTrue = rewriteRule "NotTrue.inv" $
   F  :~>  Not T

invFalseZeroOr :: Rule SLogic
invFalseZeroOr = rewriteRules "FalseZeroOr.inv"
   [ \x -> x  :~>  F :||: x
   , \x -> x  :~>  x :||: F
   ]

invNotFalse :: Rule SLogic
invNotFalse = rewriteRule "NotFalse.inv" $
   T  :~> Not F

proofInvRule :: String -> Rule SLogic -> Rule (Context Proof)
proofInvRule = makeInvRuleWithUse (similarity proofExercise)

invAbsorpOr, invAbsorpAnd, invTrueZeroOr, invComplOr, invFalseZeroAnd,
   invComplAnd, invAndOverOr, invOrOverAnd :: Rule (Context Proof)
invAbsorpOr     = proofInvRule "AbsorpOr.inv" ruleAbsorpOr
invAbsorpAnd    = proofInvRule "AbsorpAnd.inv" ruleAbsorpAnd
invTrueZeroOr   = proofInvRule "TrueZeroOr.inv" ruleTrueZeroOr
invComplOr      = proofInvRule "ComplOr.inv" ruleComplOr
invFalseZeroAnd = proofInvRule "FalseZeroAnd.inv" ruleFalseZeroAnd
invComplAnd     = proofInvRule "ComplAnd.inv" ruleComplAnd
invAndOverOr    = proofInvRule "AndOverOr.inv" ruleAndOverOr -- see GeneralizedRules
invOrOverAnd    = proofInvRule "OrOverAnd.inv" ruleOrOverAnd -- see GeneralizedRules

-----------------------------------------------------------------------------
-- Heuristic

{-
vb :: Proof
vb = makeProof
     ( (p :&&: Not q :&&: Not r) :||: (Not p :&&: Not q)
     , (Not p :&&: Not q :&&: r) :||: (Not q :&&: Not r)
     )
 where
   (p, q, r) = (Var $ ShowString "p", Var $ ShowString "q", Var $ ShowString "r")
-}

-- Special case: all conjunctions, on both sides, have a common literal.
-- Move this literal to the front (on both sides). Then use inverse distribution
-- (and top-is-and if possible).
commonLiteral :: Strategy (Context Proof)
commonLiteral =
   repeatS (somewhere (use ruleCommonLiteralInFront))
   <*>
   repeat1 (somewhere (use ruleInvDistrCommonLiteral))
   <*>
   repeatS (somewhere (use topIsAnd))

findCommonLiteral :: Ord a => (Logic a, Logic a) -> [Logic a]
findCommonLiteral (p, q) = sort $
   intersectList (map conjunctions (disjunctions p ++ disjunctions q))

ruleCommonLiteralInFront :: Rule Proof
ruleCommonLiteralInFront = makeRule "command.common-literal" f
 where
   f (Var eq) =
      [ Var x | x <- maybeToList (findInFrontLeft eq) ] ++
      [ Var (swap x) | x <- maybeToList (findInFrontLeft (swap eq)) ]
   f _ = []

   findInFrontLeft eq = do
      lit <- listToMaybe (findCommonLiteral eq)
      inFrontLeft lit eq

inFrontLeft :: SLogic -> (SLogic, SLogic) -> Maybe (SLogic, SLogic)
inFrontLeft lit (p, q) = do
   let pss = map (toFront . conjunctions) (disjunctions p)
       toFront = uncurry (++) . partition (==lit)
       new = ors (map ands pss)
   guard (new /= p)
   Just (new, q)

ruleInvDistrCommonLiteral :: Rule Proof
ruleInvDistrCommonLiteral = makeRule "andoveror.inv.common-literal" f
 where
   f (Var eq) = [ Var x | x <- invDistr eq ] ++
                [ Var (swap x) | x <- invDistr (swap eq) ]
   f _ = []

   invDistr eq@(p, q) = do
      guard (not (null (findCommonLiteral eq)))
      new <- applyAll inverseAndOverOr p
      return (new, q)

intersectList :: Eq a => [[a]] -> [a]
intersectList [] = []
intersectList xs = foldr1 intersect xs

swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)