module Recognize.Model.Connectives
(
success, unknown, failure, exists1, exists, existsF1, existsF, implication
, 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
success :: Monad m => Constraint m a
success = Constraint $ \_ -> return Success
unknown :: Monad m => Constraint m a
unknown = Constraint $ \_ -> return Unknown
failure :: Monad m => Constraint m a
failure = Constraint $ \_ -> return Failure
exists1 :: Attribute -> Constraint EvBuilder [Attribute]
exists1 = exists . (:[])
exists :: [Attribute] -> Constraint EvBuilder [Attribute]
exists hyps = implication hyps []
existsF1 :: Attribute -> Constraint EvBuilder [Attribute]
existsF1 = implication [] . (:[])
existsF :: [Attribute] -> Constraint EvBuilder [Attribute]
existsF = implication []
implication :: [Attribute]
-> [Attribute]
-> 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
negateConstraint :: Constraint EvBuilder [Attribute] -> Constraint EvBuilder [Attribute]
negateConstraint c = Constraint $ \xs -> fmap R.negate (getResult c xs)
(<||>) :: 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
(<?>>) :: 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
(<<?>) :: 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
(==>) :: 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
(<~>) :: Expr -> Expr -> Constraint EvBuilder a
e1 <~> e2 = Constraint $ \_ -> do
b <- compareExpr' e1 e2
if b then return Success
else return Failure
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
compareExpr :: Expr -> Expr -> EvBuilder Bool
compareExpr e1 e2 = do
e1Val <- normalizeIfNF <$> transformM getValueOf e1
e2Val <- normalizeIfNF <$> transformM getValueOf e2
compareExpr' (nfComAssoc e1Val) (nfComAssoc e2Val)
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