-----------------------------------------------------------------------------
-- Copyright 2019, Advise-Me project team. This file is distributed under 
-- the terms of the Apache License 2.0. For more information, see the files
-- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution.
-----------------------------------------------------------------------------
-- |
-- Maintainer  :  bastiaan.heeren@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- This module defines functions and operators for constructing and combining constraints.
--
-----------------------------------------------------------------------------

module Recognize.Model.Connectives
   ( -- * Constructing constraints
     success, unknown, failure, exists1, exists, existsF1, existsF, implication
     -- * Combinators
   , negateConstraint
   , (<||>), (<?>>), (<<?>), (==>), (<~>)
   ) where

import Control.Monad
import Data.Maybe
import Domain.Math.Data.Relation
import Domain.Math.Expr
import Ideas.Common.Rewriting.Term
import Ideas.Utils.Uniplate
import Recognize.Data.Attribute
import Recognize.Expr.Normalform
import Recognize.Expr.Symbols
import Recognize.Expr.Functions
import Recognize.Model.Constraint
import Recognize.Model.EvidenceBuilder
import Recognize.Model.Result            as R
import Util.Monad
import qualified Data.List.NonEmpty as N

-- | Constraint with an always succesful predicate
success :: Monad m => Constraint m a
success = Constraint $ \_ -> return Success

-- | Constraint whose predicate is always unknown
unknown :: Monad m => Constraint m a
unknown = Constraint $ \_ -> return Unknown

-- | Constraint whose predicate is always failure
failure :: Monad m => Constraint m a
failure = Constraint $ \_ -> return Failure

-- | If the attribute is present the constraint holds
--
-- otherwise we do not know
exists1 :: Attribute -> Constraint EvBuilder [Attribute]
exists1 = exists . (:[])

-- | If all attributes are present the constraint holds
--
-- otherwise we do not know
exists :: [Attribute] -> Constraint EvBuilder [Attribute]
exists hyps = implication hyps []

-- | If the attribute is present the constraint holds
--
-- otherwise it does not
existsF1 :: Attribute -> Constraint EvBuilder [Attribute]
existsF1 = implication [] . (:[])

-- | If all attributes are present the constraint holds
--
-- otherwise it does not
existsF :: [Attribute] -> Constraint EvBuilder [Attribute]
existsF = implication []

-- | If all hypotheses are present and all conclusions are present then the constraint holds
--
-- If all hypotheses are present, but not all conclusions are present then the constraint does not hold
--
-- If not all hypotheses are present then we do not know
implication :: [Attribute] -- ^ Hypotheses
            -> [Attribute] -- ^ Conclusions
            -> Constraint EvBuilder [Attribute]
implication hyps concs = Constraint $ \xs -> do
  ht <- hypsTrue xs
  ct <- concsTrue xs
  detResult (ht,ct)
  where
    detResult (ht,ct) =
      case (ht,ct) of
        (True,True) -> return Success
        (True,_) -> return Failure
        _ -> return Unknown
    hypsTrue xs  = allM (`elemM` xs) hyps
    concsTrue xs = allM (`elemM` xs) concs
    elemM x = anyM $ \y -> do
      vs <- getVariables
      b  <- compareAttribute x y
      unless b $ putVariables vs
      return b

-- | Negate the results of the predicate within a constraint.
negateConstraint :: Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute]
negateConstraint c = Constraint $ \xs -> fmap R.negate (getResult c xs)

-- Or for constraints
(<||>) :: Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute]
c1 <||> c2 = Constraint $ \xs -> do
  r1 <- getResult c1 xs
  case r1 of
    Success -> return Success
    Failure -> getResult c2 xs
    Unknown -> do
      r2 <- getResult c2 xs
      case r2 of
        Success -> return Success
        _ -> return Unknown

-- | If the first constraint is unknown then we return the result of the second constraint
(<?>>) :: Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute]
c1 <?>> c2 = Constraint $ \xs -> do
  r1 <- getResult c1 xs
  case r1 of
    Unknown -> getResult c2 xs
    _ -> return r1

-- | If the second constraint is unknown then we return the result of the first constraint
(<<?>) :: Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute]
c1 <<?> c2 = Constraint $ \xs -> do
  r2 <- getResult c2 xs
  case r2 of
    Unknown -> getResult c1 xs
    _ -> return r2

-- | Implication over constraints
--
-- If the first constraint holds then the result of this operation is equal to that of the second constraint
--
-- otherwise we do not know whether this constraint holds
(==>) :: Constraint EvBuilder [Attribute]  -> Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute]
c1 ==> c2 = Constraint $ \xs -> do
  r1 <- getResult c1 xs
  case r1 of
    Success -> getResult c2 xs
    _ -> return Unknown

-- | Equality constraint between two expressions
-- Does not consume any input
(<~>) :: Expr -> Expr -> Constraint EvBuilder a
e1 <~> e2 = Constraint $ \_ -> do
  b <- compareExpr' e1 e2
  if b then return Success
       else return Failure


-- | Compares two attributes for equality
compareAttribute :: Attribute -> Attribute -> EvBuilder Bool
compareAttribute (ARule r1 b1 a1) (ARule r2 b2 a2) = do
  lb1b2 <- zipWithM compareExpr lb1 lb2
  a1a2 <- compareExpr a1 a2
  return $ and lb1b2 && a1a2 && r1 == r2 && length lb1 == length lb2
  where
    lb1 = N.toList b1
    lb2 = N.toList b2
compareAttribute (ARuleR r1 b1 a1) (ARuleR r2 b2 a2) = do
  lb1b2 <- compareExpr (leftHandSide  b1) (leftHandSide  b2)
  rb1b2 <- compareExpr (rightHandSide b1) (rightHandSide b2)
  la1a2 <- compareExpr (leftHandSide  a1) (leftHandSide  a2)
  ra1a2 <- compareExpr (rightHandSide a1) (rightHandSide a2)
  let b1b2rel = relationType b1 == relationType b2
      a1a2rel = relationType a1 == relationType a2
  return $ r1 == r2 && lb1b2 && rb1b2 && la1a2 && ra1a2 && b1b2rel && a1a2rel
compareAttribute (InvalidEquation b1 a1) (InvalidEquation b2 a2) = do
  b <- compareExpr b1 b2
  a <- compareExpr a1 a2
  return (b && a)
compareAttribute (UnequalRelations b1 a1) (UnequalRelations b2 a2) = do
  lb1b2 <- compareExpr (leftHandSide b1) (leftHandSide  b2)
  rb1b2 <- compareExpr (rightHandSide b1) (rightHandSide b2)
  la1a2 <- compareExpr (leftHandSide  a1) (leftHandSide  a2)
  ra1a2 <- compareExpr (rightHandSide a1) (rightHandSide a2)
  return $ lb1b2 && rb1b2 && la1a2 && ra1a2
compareAttribute (MatchedBy a1 b1) (MatchedBy a2 b2) = do
  b <- compareExpr b1 b2
  a <- compareExpr a1 a2
  return (a && b)
compareAttribute (LabelE l1 e1) (LabelE l2 e2) = do
  b <- compareExpr e1 e2
  return (l1 == l2 && b)
compareAttribute (FinalAnswer e1) (FinalAnswer e2) =
  compareExpr e1 e2
compareAttribute (AtomMixedUp a1 b1) (AtomMixedUp a2 b2) = do
  a <- compareExpr a1 a2
  b <- compareExpr b1 b2
  return (a && b)
compareAttribute a1 a2 = return $ a1 == a2

-- Substitute any possible named wildcards with their respective values and then compare
-- For other expressions their expressions themselves are used
compareExpr :: Expr -> Expr -> EvBuilder Bool
compareExpr e1 e2 = do
  e1Val <- normalizeIfNF <$> transformM getValueOf e1
  e2Val <- normalizeIfNF <$> transformM getValueOf e2
  compareExpr' (nfComAssoc e1Val) (nfComAssoc e2Val)

-- | Compares two expressions for equality. Takes into account variables and wildcards.
compareExpr' :: Expr -> Expr -> EvBuilder Bool
compareExpr' (Number d1) (Number d2) = return (d1 == d2)
compareExpr' (Var v1) (Var v2) = return (v1 == v2)
compareExpr' (Nat n1) (Nat n2) = return (n1 == n2)
compareExpr' (Nat _) (Sym s [])
  | isWildcardSymbol s = return True
  | otherwise = return False
compareExpr' e1@(Nat _) (Sym s [Var n])
  | isNamedWildcardSymbol s = updateVar n e1 >> return True
  | otherwise = return False
compareExpr' (Sym s [Var n]) e2@(Nat _)
  | isNamedWildcardSymbol s = updateVar n e2 >> return True
  | otherwise = return False
compareExpr' (Sym s []) (Nat _)
  | isWildcardSymbol s = return True
  | otherwise = return False
compareExpr' (Var _) (Sym s [])
  | isWildcardSymbol s = return True
  | otherwise = return False
compareExpr' e1@(Var _) (Sym s [Var n])
  | isNamedWildcardSymbol s = updateVar n e1 >> return True
  | otherwise = return False
compareExpr' (Sym s [Var n]) e2@(Var _)
  | isNamedWildcardSymbol s = updateVar n e2 >> return True
  | otherwise = return False
compareExpr' (Sym s []) (Var _)
  | isWildcardSymbol s = return True
  | otherwise = return False
compareExpr' e1 e2 =
  let (s1, es1) = fromMaybe (wildcardSymbol, []) (getFunction e1)
      (s2, es2) = fromMaybe (wildcardSymbol, []) (getFunction e2)
  in
    if isWildcardSymbol s1 && s1 == s2 then return (e1 == e2)
     else case (getFunction e1, getFunction e2) of
      (Just (s,[Var n]),_)
        | isNamedWildcardSymbol s -> updateVar n e2 >> return True
      (_,Just (s,[Var n]))
        | isNamedWildcardSymbol s -> updateVar n e1 >> return True
      (Just (s,_),_)
        | isWildcardSymbol s -> return True
      (_,Just (s,_))
        | isWildcardSymbol s -> return True
      (Just (s,[Nat p, e]),_)
        | s == approxSymbol -> compareExpr' (nf4 (fromIntegral p) e) (nf4 (fromIntegral p) e2)
      (_,Just (s,[Nat p, e]))
        | s == approxSymbol -> compareExpr' (nf4 (fromIntegral p) e1) (nf4 (fromIntegral p) e)
      (_,_) ->
        if s1 == s2 then do
          es1es2 <- zipWithM compareExpr' es1 es2
          return $ and es1es2
         else return False