module Gen.Arith.Rules where

import Common.Arith
import Common.GuardedRewriting
import Test.QuickCheck
import Data.Maybe (isJust, fromJust, catMaybes)

type PropRule = Rule (Prop (Equation Expr))
type EqRule   = Rule (Equation Expr)
type ExprRule = Rule Expr


go = quickCheck $ forAll (sized propGen) (isSolved . solve rules)

rules :: [Prop (Equation Expr) -> Maybe (Prop (Equation Expr))]
rules = [ somewhereProp $ applyOne (map rewriteM propRules)
        , liftToProp $ applyOne (map rewriteM eqRules)
        , liftToProp $ liftToEq $ somewhereExpr $ applyOne (map rewriteM 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]


-- Rules
coverPlusLeft :: Rule (Equation Expr)
coverPlusLeft = synthesise $ \a b c -> 
  a :+: b :==: c +->
    a :==: c :-: b // hasVaria a && noVaria b

coverPlusRight = synthesise $ \a b c -> 
  a :+: b :==: c +->
    b :==: c :-: a // noVaria a && hasVaria b

coverMinLeft = synthesise $ \a b c ->
  a :-: b :==: c +-> 
    a :==: c :+: b // hasVaria a && noVaria b

coverMinRight = synthesise $ \a b c ->
  a :-: b :==: c +->
    b :==: a :-: c // noVaria a && hasVaria b
   
coverTimesLeft = synthesise $ \a b c -> 
  a :**: Const b :==: c +->
    a :==: c :/: Const b // hasVaria a && b /= 0
   
coverTimesRight = synthesise $ \a b c ->
  Const a :**: b :==: c +->
    b :==: c :/: Const a // a /= 0 && hasVaria b
   
coverDivLeft = synthesise $ \a b c ->
  a :/: Const b :==: c +->
    a :==: c :**: Const b // hasVaria a && b /= 0
   
coverDivRight = synthesise $ \a b c ->
  Const a :/: b :==: c +->
    b :==: Const a :/: c // hasVaria b -- and b should not be zero here!

coverPowerEven = synthesise $ \a n b -> let new = b :^: Const (1/n) in
  VarP (a :^: Const n :==: b) +->
    VarP (a :==: new) :\/: VarP (a :==: Const 0 :-: new)
      // hasVaria a && n > 0 && isEven n

coverPowerOdd = synthesise $ \a n b ->
  a :^: Const n :==: b +->
    a :==: b :^: Const (1/n) // hasVaria a && n > 0 && isOdd n

timesZeroLeft = synthesise $ \x ->
  Const 0 :**: x +->
    Const 0

timesZeroRight = synthesise $ \x -> 
  x :**: Const 0 +->
    Const 0

divisionByZero = synthesise $ \a b -> 
  VarP (a :==: b) +->
    F // hasDivisionByZero a || hasDivisionByZero b

--------------------------------------------------------
-- Rules for comparing the two sides of an equation
      
eqSame = synthesise $ \a b ->
  VarP (a :==: b) +->
    T // a == b

eqDifferent = synthesise $ \a b ->
  VarP (Const a :==: Const b) +->
    F // a /= b

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

andTrueLeft = synthesise $ \p ->
  T :/\: p +->
    p

andTrueRight = synthesise $ \p ->
  p :/\: T +->
    p

andFalseLeft = synthesise $ \p ->
  F :/\: p +->
    F

andFalseRight = synthesise $ \p ->
  p :/\: F +->
    F

orTrueLeft = synthesise $ \p ->
  T :\/: p +->
    T

orTrueRight = synthesise $ \p ->
  p :\/: T +->
    T

orFalseLeft = synthesise $ \p ->
  F :\/: p +->
    p

orFalseRight = synthesise $ \p ->
  p :\/: F +->
    p

notTrue = synthesise $ 
  Not T +->
    F

notFalse = synthesise $ 
  Not F +->
    T