{-# LANGUAGE RankNTypes #-}
-----------------------------------------------------------------------------
-- Copyright 2015, 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 7529 2015-04-08 09:55:03Z bastiaan $

module Domain.Logic.Proofs
   ( proofExercise, proofTopExercise, proofUnicodeExercise
   , topIsAnd, topIsAndCom
   ) where

import Control.Arrow
import Control.Monad
import Data.Foldable (toList)
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.Generator (equalLogicA)
import Domain.Logic.InverseRules hiding (inverseRules)
import Domain.Logic.Parser
import Domain.Logic.Rules
import Domain.Logic.Strategies
import Domain.Logic.Utils
import Domain.Math.Expr ()
import Ideas.Common.Library
import Ideas.Common.Traversal.Navigator
import Ideas.Common.Utils

-- Currently, we use the DWA strategy
proofExercise :: Exercise Proof
proofExercise = makeExercise
   { exerciseId     = describe "Prove two propositions equivalent" $
                         propositionalId # "proof"
   , status         = Experimental
   , parser         = -- maybe (Left "nee") Right . fromTerm . read
                      mapSecond makeProof . parseLogicProof False
   , prettyPrinter  = -- show . toTerm
                      showProof
   , equivalence    = withoutContext equivalentProofs
   , similarity     = withoutContext similarProofs
   , suitable       = predicate $ all (uncurry eqLogic) . subProofs
   , ready          = predicate $ all (uncurry equalLogicA) . subProofs
   , strategy       = {- cleanUpStrategyAfter (applyTop cleanUp) -}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
   }

proofTopExercise :: Exercise Proof
proofTopExercise = proofExercise
   { exerciseId    = describe "Prove two propositions equivalent (with top-level decomposition)" $
                        propositionalId # "proof.top"
   , parser        = mapSecond (ands . map makeProof) . parseLogicProofs
   , prettyPrinter = showSubProofs
   , equivalence   = withoutContext eqSubProofs
   , similarity    = withoutContext simSubProofs
   }

type Proof = Logic (SLogic, SLogic)

{-
cleanUp :: Proof -> Proof
cleanUp proof = makeProof (associateToRight lhs, associateToRight rhs)
 where
   (lhs, rhs) = proofPair proof -}

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

makeProof :: (SLogic, SLogic) -> Proof
makeProof pair =
   let p = Var pair in
   case apply (topIsOr <|> topIsAnd <|> topIsNot <|> topIsEquiv <|> topIsImpl) p of
      Just (Var eq1 :||:  Var eq2) -> makeProof eq1 :||:  makeProof eq2
      Just (Var eq1 :&&:  Var eq2) -> makeProof eq1 :&&:  makeProof eq2
      Just (Var eq1 :->:  Var eq2) -> makeProof eq1 :->:  makeProof eq2
      Just (Var eq1 :<->: Var eq2) -> makeProof eq1 :<->: makeProof eq2
      Just (Not (Var eq))          -> Not (makeProof eq)
      _ -> p

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

showSubProofs :: Proof -> String
showSubProofs = intercalate ", " . map (uncurry f) . subProofs
 where
   f p q = ppLogicPars p ++ " == " ++ ppLogicPars 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

eqSubProofs :: Proof -> Proof -> Bool
eqSubProofs proof1 proof2 =
   let ok = uncurry eqLogic
   in all ok (subProofs proof1) == all ok (subProofs proof2)

simSubProofs :: Proof -> Proof -> Bool
simSubProofs proof1 proof2 =
   let (xs1, xs2) = unzip (subProofs proof1)
       (ys1, ys2) = unzip (subProofs proof2)
       ok = uncurry equalLogicA
   in length xs1 == length ys1
   && all ok (zip xs1 ys1)
   && all ok (zip xs2 ys2)

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 towardsDNF
      |> commonLiteralSpecial
      |> useC distrAnd
      |> (use checkDNF <*> commonLiteral)
      )
      <*> use checkDNF <*> normStrategy

splitTop :: Strategy (Context Proof)
splitTop =  use topIsNot <|> use topIsEquiv <|> use topIsImpl
               -- only use commutativity if not already in desired order
           <|> (use topIsAnd |> use topIsAndCom)
           <|> (use topIsOr  |> use topIsOrCom)

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

ruleCommonLiteralSpecialInFront :: Rule Proof
ruleCommonLiteralSpecialInFront = siblingOf groupCommutativity $ 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

{- ------------------------------------------------------------------
In the strong-normalization strategy we do not check for common literals:
   |> somewhere (use checkDNF <*> commonLiteral)
Therefore, we also do not need simplification rules:
   |> somewhere (use ruleFalseAnd <|> use ruleTrueOr
                <|> use ruleFalseOr <|> use ruleTrueAnd)
   |> somewhere (use ruleComplAnd)
------------------------------------------------------------------ -}
normStrategy :: Strategy (Context Proof)
normStrategy = repeatS $
      somewhere splitTop
   |> somewhere (
         use ruleIdempOr   <|>
         use ruleIdempAnd  <|>
         use absorptionOrSubset <|>
         use ruleComplOr
      )
   |> somewhereDisjunct introduceVar

-- (p /\ q) \/ ... \/ (p /\ q /\ r)    ~> (p /\ q) \/ ...
--    (subset relatie tussen rijtjes: bijzonder geval is gelijke rijtjes)
absorptionOrSubset :: Rule SLogic
absorptionOrSubset = siblingOf groupAbsorption $ ruleList "absorpor-subset" $ \p -> do
   let xss = map conjunctions (disjunctions p)
       yss = nub $ filter (\xs -> all (ok xs) xss) xss
       ok xs ys = not (ys `isSubsetOf` xs) || xs == ys
   guard (length yss < length xss)
   return $ ors (map ands yss)

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

towardsDNF :: Strategy (Context SLogic)
towardsDNF = configureS (Reinsert `byName` specialGroupLiterals) $
   orRules <|> somewhereOr nnfStep

-- 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'..] ]
-}
--------------------------------------------------------------------

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 $
      -- if both sides have changed ...
      if as1++as2 /= as && bs1++bs2 /= bs
      then -- ... only keep the reordering on the left-hand side
         Var (to iso (as1++as2), rhs)
      else -- ... otherwise, decompose proof with "top" rule
         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)

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

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

topIsEquiv :: Rule Proof
topIsEquiv = minorRule "top-is-equiv" 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

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
            <*> introCompl
            <*> use ruleDistrAnd

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 = siblingOf groupTrueConjunction $ rewriteRule "IntroTrueLeft" $
   \x -> x  :~>  T :&&: x

introCompl :: Rule (Context Proof)
introCompl = siblingOf groupTrueComplement $ makeRule "IntroCompl" $ \cp -> do
   a <- missingVar 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 a (p :&&: q) = fmap (:&&: q) (introTautology a p)
   introTautology _ _ = Nothing

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

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

inverseRules :: [Rule (Context Proof)]
inverseRules = map use [invDefImpl, invDefEquiv, invDoubleNeg, invIdempOr, invIdempAnd,
   invTrueAnd, invNotTrue, invFalseOr, invNotFalse] ++
   [ invAbsorpOr, invAbsorpAnd, invTrueOr, invComplOr, invFalseAnd
   , invComplAnd, invDistrAnd, invDistrOr]

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

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

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

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

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

invTrueAnd :: Rule SLogic
invTrueAnd = siblingOf groupTrueConjunction $ rewriteRules "TrueZeroAnd.inv"
   [ \x -> x  :~>  T :&&: x
   , \x -> x  :~>  x :&&: T
   ]

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

invFalseOr :: Rule SLogic
invFalseOr = siblingOf groupFalseDisjunction $ rewriteRules "FalseZeroOr.inv"
   [ \x -> x  :~>  F :||: x
   , \x -> x  :~>  x :||: F
   ]

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

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

invAbsorpOr, invAbsorpAnd, invTrueOr, invComplOr, invFalseAnd,
   invComplAnd, invDistrAnd, invDistrOr :: Rule (Context Proof)
invAbsorpOr  = proofInvRule "AbsorpOr.inv" ruleAbsorpOr
invAbsorpAnd = proofInvRule "AbsorpAnd.inv" ruleAbsorpAnd
invTrueOr    = proofInvRule "TrueZeroOr.inv" ruleTrueOr
invComplOr   = proofInvRule "ComplOr.inv" ruleComplOr
invFalseAnd  = proofInvRule "FalseZeroAnd.inv" ruleFalseAnd
invComplAnd  = proofInvRule "ComplAnd.inv" ruleComplAnd
invDistrAnd  = proofInvRule "AndOverOr.inv" ruleDistrAnd -- see GeneralizedRules
invDistrOr   = proofInvRule "OrOverAnd.inv" ruleDistrOr  -- see GeneralizedRules

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

-- 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 = siblingOf groupCommutativity $ 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 = siblingOf groupDistribution $ 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)