module PM.Arith.Rules where

import Common.Arith
import Test.QuickCheck
import Data.Ratio

type Rule a   = a -> Maybe a
type PropRule = Rule (Prop (Equation Expr))
type EqRule   = Rule (Equation Expr)
type ExprRule = Rule Expr

rules :: [PropRule]
rules = [ somewhereProp $ applyOne propRules
        , liftToProp $ applyOne eqRules
        , liftToProp $ liftToEq $ somewhereExpr $ applyOne exprRules
        ]
 where
   propRules :: [PropRule]
   propRules = 
      [ coverPowerEven, divisionByZero
      , eqSame, eqDifferent
      , andTrueLeft, andTrueRight, andFalseLeft, andFalseRight
      , orTrueLeft, orTrueRight, orFalseLeft, orFalseRight
      , notTrue, notFalse
      ]

   eqRules :: [EqRule]
   eqRules = 
      [ coverPlusLeft, coverPlusRight, coverMinLeft, coverMinRight
      , coverTimesLeft, coverTimesRight, coverDivLeft, coverDivRight
      , coverPowerOdd
      ]

   exprRules :: [ExprRule]
   exprRules = [timesZeroLeft, timesZeroRight]
   
go = quickCheck $ forAll (sized propGen) (isSolved . solve rules)

-- Rules
coverPlusLeft :: EqRule
coverPlusLeft (a :+: b :==: c)
   | hasVaria a && noVaria b = 
        Just (a :==: c :-: b)
coverPlusLeft _ = Nothing

coverPlusRight :: EqRule
coverPlusRight (a :+: b :==: c)
   | noVaria a && hasVaria b =
        Just (b :==: c :-: a)
coverPlusRight _ = Nothing

coverMinLeft :: EqRule
coverMinLeft (a :-: b :==: c)
   | hasVaria a && noVaria b = 
        Just (a :==: c :+: b)
coverMinLeft _ = Nothing

coverMinRight :: EqRule
coverMinRight (a :-: b :==: c)
   | noVaria a && hasVaria b =
        Just (b :==: a :-: c)
coverMinRight _ = Nothing
   
coverTimesLeft :: EqRule
coverTimesLeft (a :**: Const b :==: c) 
   | hasVaria a && b /= 0 =
        Just (a :==: c :/: Const b)
coverTimesLeft _ = Nothing
   
coverTimesRight :: EqRule
coverTimesRight (Const a :**: b :==: c) 
   | a /= 0 && hasVaria b =
        Just (b :==: c :/: Const a)
coverTimesRight _ = Nothing
   
coverDivLeft :: EqRule
coverDivLeft (a :/: Const b :==: c) 
   | hasVaria a && b /= 0 =
        Just (a :==: c :**: Const b)
coverDivLeft _ = Nothing
   
coverDivRight :: EqRule
coverDivRight (Const a :/: b :==: c) 
   | hasVaria b =
        Just (b :==: Const a :/: c) -- and b should not be zero here!
coverDivRight _ = Nothing

coverPowerEven :: PropRule
coverPowerEven (VarP (a :^: Const n :==: b)) 
   | hasVaria a && n > 0 && isEven n =
        let new = b :^: Const (1/n) in
        Just (VarP (a :==: new) :\/: VarP (a :==: Const 0 :-: new))
coverPowerEven _ = Nothing

coverPowerOdd :: EqRule
coverPowerOdd (a :^: Const n :==: b)
   | hasVaria a && n > 0 && isOdd n =
        Just (a :==: b :^: Const (1/n))
coverPowerOdd _ = Nothing

timesZeroLeft :: ExprRule
timesZeroLeft (Const 0 :**: _) =
   Just (Const 0)
timesZeroLeft _ = Nothing

timesZeroRight :: ExprRule
timesZeroRight (_ :**: Const 0) =
   Just (Const 0)
timesZeroRight _ = Nothing

divisionByZero :: PropRule
divisionByZero (VarP (a :==: b)) 
   | hasDivisionByZero a || hasDivisionByZero b =
        Just F
divisionByZero _ = Nothing

--------------------------------------------------------
-- Rules for comparing the two sides of an equation
      
eqSame :: PropRule
eqSame (VarP (a :==: b)) | a == b = Just T
eqSame _ = Nothing 

eqDifferent :: PropRule
eqDifferent (VarP (Const a :==: Const b)) | a /= b = Just F
eqDifferent _ = Nothing 

----------------------------------
-- Propagating boolean constants

andTrueLeft :: PropRule 
andTrueLeft (T :/\: p) = Just p
andTrueLeft _ = Nothing

andTrueRight :: PropRule 
andTrueRight (p :/\: T) = Just p
andTrueRight _ = Nothing

andFalseLeft :: PropRule 
andFalseLeft (F :/\: _) = Just F
andFalseLeft _ = Nothing

andFalseRight :: PropRule 
andFalseRight (_ :/\: F) = Just F
andFalseRight _ = Nothing

orTrueLeft :: PropRule 
orTrueLeft (T :\/: _) = Just T
orTrueLeft _ = Nothing

orTrueRight :: PropRule 
orTrueRight (_ :\/: T) = Just T
orTrueRight _ = Nothing

orFalseLeft :: PropRule 
orFalseLeft (F :\/: p) = Just p
orFalseLeft _ = Nothing

orFalseRight :: PropRule 
orFalseRight (p :\/: F) = Just p
orFalseRight _ = Nothing

notTrue :: PropRule
notTrue (Not T) = Just F
notTrue _ = Nothing

notFalse :: PropRule
notFalse (Not F) = Just T
notFalse _ = Nothing