Utils.hs

{-# LANGUAGE FlexibleInstances #-}
-----------------------------------------------------------------------------
-- 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  :  alex.gerdes@ou.nl
-- Stability   :  provisional
-- Portability :  portable (depends on ghc)
--
-- some of these help functions may have a broader scope and could be
-- moved to other parts of the framework (eg. Common)
--
-----------------------------------------------------------------------------
--  $Id: Utils.hs 7527 2015-04-08 07:58:06Z bastiaan $

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
import Ideas.Common.Utils.Uniplate

-- | Strategy functions -------------------------------------------------------

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

-- | Rule functions -----------------------------------------------------------

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)

-- | View functions -----------------------------------------------------------

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"

-- | Rule collections ---------------------------------------------------------

naturalRules :: [Rule Expr]
naturalRules =
   [ calcPlusWith "nat" plainNatView, calcMinusWith "nat" plainNatView
   , calcTimesWith "nat" plainNatView, calcDivisionWith "nat" plainNatView
   , doubleNegate, negateZero , plusNegateLeft, plusNegateRight
--   , minusNegateLeft
   , 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}

-- | Common functions ---------------------------------------------------------

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

-- Semantic equivalence
class SemEq a where
    (===), (=/=) :: a -> a -> Bool
    x =/= y = not (x === y)
--    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

-- y = root n x
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)
{-
| n == 0    = [0]
             | n == 1    = if x > 0 && odd x then [1] else [1, -1]
             | n == (-1) = [-1 | x > 0 && odd x]
             | x == 1    = [n]
             | x > 0     = maybe [] roots $ lookup x $ map swap $ PF.allPowers (abs n)
             | otherwise = []
  where
    roots r | n > 0 && even x = [r, negate r]
            | n > 0 && odd  x = [r]
            | n < 0 && odd  x = [negate r]
            | otherwise       = [] -}

-- prop_takeRoot n = traceShow n f
--   where
--     f n x | x > 0 = n `elem` (takeRoot (n Prelude.^ x) x)
--           | otherwise = True

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