```-----------------------------------------------------------------------------
-- 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)
--
-----------------------------------------------------------------------------

module Domain.Math.Polynomial.RationalRules
( divisionIsZero, divisionIsOne, sameDivisor, sameDividend
, crossMultiply, multiplyOneDiv, fractionPlus, cancelTermsDiv
, fractionScale, turnIntoFraction, checkSolution
) where

import Control.Applicative
import Control.Monad
import Data.Maybe
import Domain.Logic.Formula hiding (Var)
import Domain.Logic.Views
import Domain.Math.CleanUp
import Domain.Math.Data.OrList
import Domain.Math.Data.Relation
import Domain.Math.Equation.CoverUpRules
import Domain.Math.Expr
import Domain.Math.Numeric.Views
import Domain.Math.Polynomial.LeastCommonMultiple
import Domain.Math.Polynomial.Views
import Domain.Math.Power.Views
import Ideas.Common.Library hiding ((<>))
import qualified Domain.Logic.Formula as Logic

ratId :: Id
ratId = newId "algebra.equations.rational"

---------------------------------------------------------------
-- Rules for rational expressions and rational equations

-- a/b = 0  iff  a=0 (and b/=0)
divisionIsZero :: Rule (Context (Equation Expr))
divisionIsZero = makeRule (ratId, "division-zero") \$ \ceq -> do
lhs :==: rhs <- currentInContext ceq
guard (rhs == 0)
(a, b) <- match divView lhs
return \$ conditionNotZero b
\$ replaceInContext (a :==: 0) ceq

-- a/b = 1  iff  a=b (and b/=0)
divisionIsOne :: Rule (Context (Equation Expr))
divisionIsOne = makeRule (ratId, "division-one") \$ \ceq -> do
lhs :==: rhs <- currentInContext ceq
guard (rhs == 1)
(a, b) <- match divView lhs
return \$ conditionNotZero b
\$ replaceInContext (a :==: b) ceq

-- a/c = b/c  iff  a=b (and c/=0)
sameDivisor :: Rule (Context (Equation Expr))
sameDivisor = makeRule (ratId, "same-divisor") \$ \ceq -> do
lhs :==: rhs <- currentInContext ceq
(a, c1) <- match divView lhs
(b, c2) <- match divView rhs
guard (c1==c2)
return \$ conditionNotZero c1
\$ replaceInContext (a :==: b) ceq

-- a/b = a/c  iff  a=0 or b=c (and b/=0 and c/=0)
sameDividend :: Rule (Context (OrList (Equation Expr)))
sameDividend = makeRule (ratId, "same-dividend") \$ \cor -> do
oreq <- currentInContext cor
lhs :==: rhs <- getSingleton oreq
(a1, b) <- matchM divView lhs
(a2, c) <- matchM divView rhs
guard (a1==a2)
let new = singleton (a1 :==: 0) <> singleton (b :==: c)
return \$ conditionNotZero c
\$ conditionNotZero b
\$ replaceInContext new cor

-- a/b = c/d  iff  a*d = b*c   (and b/=0 and d/=0)
crossMultiply :: Rule (Context (Equation Expr))
crossMultiply = makeRule (ratId, "cross-multiply") \$ \ceq -> do
lhs :==: rhs <- currentInContext ceq
(a, b) <- match divView lhs
(c, d) <- match divView rhs
return \$ conditionNotZero d
\$ conditionNotZero b
\$ replaceInContext (a*d :==: b*c) ceq

-- a/b = c  iff  a = b*c  (and b/=0)
multiplyOneDiv :: Rule (Context (Equation Expr))
multiplyOneDiv = ruleList (ratId, "multiply-one-div") \$ \ceq -> do
lhs :==: rhs <- maybeToList (currentInContext ceq)
f (:==:) lhs rhs ceq <|> f (flip (:==:)) rhs lhs ceq
where
f eq ab c ceq = do
guard (not (c `belongsTo` divView))
(a, b) <- matchM divView ab
return \$ conditionNotZero b
\$ replaceInContext (a `eq` (b*c)) ceq

-- a/c + b/c = a+b/c   (also see Numeric.Rules)
fractionPlus :: Rule Expr -- also minus
fractionPlus = makeRule (ratId, "rational-plus") \$ \expr -> do
((a, b), (c, d)) <- match myView expr
guard (b == d)
return (build divView (a+c, b))
where
myView = plusView >>> (divView *** divView)

-- ab/ac  =>  b/c  (if a/=0)
-- Note that the common term can be squared (in one of the parts)
cancelTermsDiv :: Rule (Context Expr)
cancelTermsDiv = makeRule (ratId, "cancel-div") \$ \ce -> do
expr <- currentInContext ce
((b, xs), (c, ys)) <- match myView expr
let (ps, qs, rs) = rec (map f xs) (map f ys)
new = build myView ((b, map g ps), (c, map g qs))
guard (not (null rs))
return \$ conditionNotZero (build productView (False, map g rs))
\$ replaceInContext new ce
where
myView = divView >>> toView (productView *** productView)
powInt = powerView >>> second integerView
f a = fromMaybe (a, 1) (match powInt a)
g   = build powInt
rec ((_, 0):xs) ys = rec xs ys
rec (pair@(a, n):xs) ys =
case break ((==a) . fst) ys of
(ys1, (b, m):ys2)
| m == 0 ->
rec (pair:xs) (ys1++ys2)
| otherwise ->
let i = n `min` m
(ps,qs,rs) = rec ((a, n-i):xs) (ys1++(b,m-i):ys2)
in (ps, qs, (a,i):rs)
_ ->
let (ps,qs,rs) = rec xs ys
in (pair:ps, qs,rs)
rec xs ys = (xs, ys, [])

fractionScale :: Rule Expr
fractionScale = liftView myView \$
makeRule (ratId, "rational-scale") \$ \((a, e1), (b, e2)) -> do
guard (e1 /= e2)
let e3 = lcmExpr e1 e2
ma <- divisionExpr e3 e1
mb <- divisionExpr e3 e2
guard (ma /= 1 || mb /= 1)
return ((ma*a, e3), (mb*b, e3))
where
myView = plusView >>> (divView *** divView)

turnIntoFraction :: Rule Expr
turnIntoFraction = liftView plusView \$
makeRule (ratId, "to-rational") \$ \(a, b) ->
fmap (\c -> (c, b)) (f a b) <|>
fmap (\c -> (a, c)) (f b a)
where
f a b = do
guard (not (a `belongsTo` divView))
(_, e) <- match divView b
return \$ build divView (a*e, e)

-- A simple implementation that considers the condition stored in the context
checkSolution :: Rule (Context (OrList (Equation Expr)))
checkSolution = makeRule (ratId, "check-solution") \$ \cor -> do
oreq <- currentInContext cor
x :==: a <- getSingleton oreq
c  <- lookupClipboardG "condition" cor
xs <- match andView c
guard ((x ./=. a) `elem` xs)
return \$ replaceInContext false cor

---------------------------------------------------------------
-- Helper-code

condition :: Logic (Relation Expr) -> Context a -> Context a
condition p c
| new == T  = {- removeClipboardC "condition" -} c
| otherwise = addToClipboardG "condition" new c
where
mp  = lookupClipboardG "condition" c
new = maybe id (.&&.) mp p

conditionNotZero :: Expr -> Context a -> Context a
conditionNotZero expr = condition (f xs)
where
f  = pushNotWith (Logic.Var . notRelation) . Not
eq = expr :==: 0
xs = fmap (build equationView . fmap cleanUpExpr) \$
case match higherDegreeEquationsView (singleton eq) of
Just ys -> build orListView (coverUpOrs (build higherDegreeEquationsView ys))
Nothing -> Logic.Var (coverUp eq)```