RationalRules.hs

-----------------------------------------------------------------------------
-- 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)
--
-----------------------------------------------------------------------------
--  $Id: RationalRules.hs 7527 2015-04-08 07:58:06Z bastiaan $

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

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
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 `mplus` 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) ->
      liftM (\c -> (c, b)) (f a b) `mplus`
      liftM (\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)