{-# LANGUAGE FlexibleInstances #-}
module Domain.Math.Power.Utils where
import Data.Foldable (toList)
import Data.Function (on)
import Data.List
import Data.Ratio
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.Rules
import Domain.Math.Numeric.Views
import Ideas.Common.Library hiding ((.*.), (./.))
import Ideas.Utils.Uniplate
exhaustiveStrategy :: IsTerm a => [Rule a] -> Strategy (Context a)
exhaustiveStrategy = exhaustiveSomewhere . map liftToContext
exhaustiveUse :: (IsTerm a, IsTerm b) => [Rule a] -> Strategy (Context b)
exhaustiveUse = exhaustiveSomewhere . map use
exhaustiveSomewhere :: IsStrategy f => [f (Context a)] -> Strategy (Context a)
exhaustiveSomewhere = repeatS . somewhere . alternatives
smartRule :: Rule Expr -> Rule Expr
smartRule = doAfter f
where
f (a :*: b) = a .*. b
f (a :/: b) = a ./. b
f (Negate a) = neg a
f (a :+: b) = a .+. b
f (a :-: b) = a .-. b
f e = e
mergeConstantsWith :: (Expr -> Bool) -> Expr -> Expr
mergeConstantsWith p = simplifyWith f productView
where
f (sign, xs) =
let (cs, ys) = partition p xs
c = simplify rationalView $ build productView (False, cs)
in if maybe False (> 1) (match rationalView c)
then (sign, c:ys)
else (sign, xs)
mergeConstants :: Expr -> Expr
mergeConstants = mergeConstantsWith (`belongsTo` rationalView)
plainNatView :: View Expr Integer
plainNatView = makeView f Nat
where
f (Nat n) = Just n
f _ = Nothing
myIntegerView :: View Expr Integer
myIntegerView = makeView f fromInteger
where
f (Nat n) = Just n
f (Negate (Nat n)) = Just $ negate n
f _ = Nothing
plainRationalView :: View Rational (Integer, Integer)
plainRationalView =
makeView (\x -> return (numerator x, denominator x)) (uncurry (%))
eqView :: View a b -> View (Equation a) (b, b)
eqView v = eqv >>> v *** v
where
eqv = makeView (\(lhs :==: rhs) -> Just (lhs, rhs)) (uncurry (:==:))
relationView :: View (Equation a) (Relation a)
relationView = makeView f g
where
f (x :==: y) = return $ x .==. y
g r | relationType r == EqualTo = leftHandSide r :==: rightHandSide r
| otherwise = error "Not an equality"
naturalRules :: [Rule Expr]
naturalRules =
[ calcPlusWith "nat" plainNatView, calcMinusWith "nat" plainNatView
, calcTimesWith "nat" plainNatView, calcDivisionWith "nat" plainNatView
, doubleNegate, negateZero , plusNegateLeft, plusNegateRight
, minusNegateRight, timesNegateLeft, timesNegateRight, divisionNegateLeft
, divisionNegateRight
]
rationalRules :: [Rule Expr]
rationalRules =
[ calcPlusWith "rational" rationalRelaxedForm
, calcMinusWith "rational" rationalRelaxedForm
, calcTimesWith "rational" rationalRelaxedForm
, calcDivisionWith "integer" integerNF
, doubleNegate, negateZero, divisionDenominator, divisionNumerator
, simplerFraction
]
coverUpRulesX :: [Rule (Equation Expr)]
coverUpRulesX = map (\r -> r cfg)
[ coverUpPlusWith, coverUpMinusLeftWith, coverUpMinusRightWith, coverUpNegateWith
, coverUpTimesWith, coverUpNumeratorWith, coverUpDenominatorWith, coverUpSqrtWith
]
where
cfg = configCoverUp { predicateCovered = elem "x" . vars
, predicateCombined = notElem "x" . vars
, coverLHS = False}
sortExpr :: Expr -> Expr
sortExpr = transform $ simplifyWith (sort . map sortProd) sumView
where sortProd = simplifyWith (fmap sort) productView
sortEquation :: Equation Expr -> Equation Expr
sortEquation (x :==: y) = if x < y then eq else flipSides eq
where eq = sortExpr x :==: sortExpr y
sortOrList :: OrList (Equation Expr) -> OrList (Equation Expr)
sortOrList = toOrList . sort . map sortEquation . toList
class SemEq a where
(===), (=/=) :: a -> a -> Bool
x =/= y = not (x === y)
infix 4 ===, =/=
instance SemEq a => SemEq (Equation a) where
(a :==: b) === (c :==: d) = a === c && b === d || a === d && b === c
instance SemEq Expr where
(===) = on (==) cleanUpExpr
instance SemEq a => SemEq (OrList a) where
a === b = let as = toList a ; bs = toList b
in length (intersectBy (===) as bs) == length as
takeRoot :: Integer -> Integer -> Maybe Integer
takeRoot n x
| n >= 0 && x >0 && a Prelude.^ x == n = Just a
| otherwise = Nothing
where
a = round (fromInteger n ** (1/fromInteger x) :: Double)
swap :: (a, b) -> (b, a)
swap (a, b) = (b, a)
split :: (Eq a) => (a -> a -> t) -> [a] -> [(t, [a])]
split op xs = f xs
where
f (y:ys) | not (null ys) = [(y `op` z, xs \\ [y, z]) | z <- ys] ++ f ys
| otherwise = []
f [] = []
toMaybe :: (a -> Bool) -> a -> Maybe a
toMaybe p x = if p x then Just x else Nothing
joinBy :: Eq a => (a -> a -> Bool) -> [a] -> [[a]]
joinBy _ [] = []
joinBy eq xs = ys : joinBy eq (xs \\ ys)
where
ys = dropUntil eq xs
dropUntil :: (a -> a -> Bool) -> [a] -> [a]
dropUntil _ [] = []
dropUntil _ [x] = [x]
dropUntil p (x:y:ys) | p x y = x : dropUntil p (y:ys)
| otherwise = [x]
holes :: [a] -> [(a, [a], a -> [a])]
holes xs = map f [0 .. length xs - 1]
where
f i = let (ys, z:zs) = splitAt i xs
in (z, ys ++ zs, \x -> ys ++ x:zs)
twoNonAdjacentHoles :: [a] -> [((a, a), a -> [a])]
twoNonAdjacentHoles xs = concatMap g pairs
where
pairs = [(x, y) | x <- [0 .. length xs - 1], y <- [x + 1 .. length xs - 1]]
g (x, y) = let (ys, z:zs) = splitAt x xs
(ps, q:qs) = splitAt (y - x - 1) zs
in if null ps
then [ ((z, q), \a -> ys ++ a:ps ++ qs) ]
else [ ((z, q), \a -> ys ++ a:ps ++ qs)
, ((z, q), \a -> ys ++ ps ++ a:qs) ]