{-|
Copyright  :  (C) 2015-2016, University of Twente,
                  2017     , QBayLogic B.V.
License    :  BSD2 (see the file LICENSE)
Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>
-}

{-# LANGUAGE CPP       #-}
{-# LANGUAGE MagicHash #-}

module GHC.TypeLits.Extra.Solver.Operations
  ( ExtraOp (..)
  , ExtraDefs (..)
  , Normalised (..)
  , NormaliseResult
  , mergeNormalised
  , reifyEOP
  , mergeMax
  , mergeMin
  , mergeDiv
  , mergeMod
  , mergeFLog
  , mergeCLog
  , mergeLog
  , mergeGCD
  , mergeLCM
  , mergeExp
  )
where

-- external

import Control.Monad.Trans.Writer.Strict
#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
import Data.Set                     as Set
#endif

import GHC.Base                     (isTrue#,(==#),(+#))
import GHC.Integer                  (smallInteger)
import GHC.Integer.Logarithms       (integerLogBase#)
import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural)

-- GHC API

#if MIN_VERSION_ghc(9,0,0)
import GHC.Builtin.Types.Literals (typeNatExpTyCon, typeNatSubTyCon)
import GHC.Core.TyCon (TyCon)
import GHC.Core.Type (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)
import GHC.Utils.Outputable (Outputable (..), (<+>), integer, text)
#else
import Outputable (Outputable (..), (<+>), integer, text)
import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon)
import TyCon      (TyCon)
import Type       (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)
#endif

-- | Indicates whether normalisation has occured

data Normalised = Normalised | Untouched
  deriving Normalised -> Normalised -> Bool
(Normalised -> Normalised -> Bool)
-> (Normalised -> Normalised -> Bool) -> Eq Normalised
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Normalised -> Normalised -> Bool
== :: Normalised -> Normalised -> Bool
$c/= :: Normalised -> Normalised -> Bool
/= :: Normalised -> Normalised -> Bool
Eq

instance Outputable Normalised where
  ppr :: Normalised -> SDoc
ppr Normalised
Normalised = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Normalised"
  ppr Normalised
Untouched  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Untouched"

mergeNormalised :: Normalised -> Normalised -> Normalised
mergeNormalised :: Normalised -> Normalised -> Normalised
mergeNormalised Normalised
Normalised Normalised
_ = Normalised
Normalised
mergeNormalised Normalised
_ Normalised
Normalised = Normalised
Normalised
mergeNormalised Normalised
_ Normalised
_          = Normalised
Untouched

-- | A normalise result contains the ExtraOp and a flag that indicates whether any expression

-- | was normalised within the ExtraOp.

type NormaliseResult = (ExtraOp, Normalised)

data ExtraOp
  = I    Integer
  | V    TyVar
  | C    CType
  | Max  ExtraOp ExtraOp
  | Min  ExtraOp ExtraOp
  | Div  ExtraOp ExtraOp
  | Mod  ExtraOp ExtraOp
  | FLog ExtraOp ExtraOp
  | CLog ExtraOp ExtraOp
  | Log  ExtraOp ExtraOp
  | GCD  ExtraOp ExtraOp
  | LCM  ExtraOp ExtraOp
  | Exp  ExtraOp ExtraOp
  deriving ExtraOp -> ExtraOp -> Bool
(ExtraOp -> ExtraOp -> Bool)
-> (ExtraOp -> ExtraOp -> Bool) -> Eq ExtraOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ExtraOp -> ExtraOp -> Bool
== :: ExtraOp -> ExtraOp -> Bool
$c/= :: ExtraOp -> ExtraOp -> Bool
/= :: ExtraOp -> ExtraOp -> Bool
Eq

instance Outputable ExtraOp where
  ppr :: ExtraOp -> SDoc
ppr (I Integer
i)      = Integer -> SDoc
forall doc. IsLine doc => Integer -> doc
integer Integer
i
  ppr (V TyVar
v)      = TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
v
  ppr (C CType
c)      = CType -> SDoc
forall a. Outputable a => a -> SDoc
ppr CType
c
  ppr (Max ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Max (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (Min ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Min (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (Div ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Div (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (Mod ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Mod (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (FLog ExtraOp
x ExtraOp
y) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"FLog (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (CLog ExtraOp
x ExtraOp
y) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"CLog (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (Log ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Log (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (GCD ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"GCD (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (LCM ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"GCD (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"
  ppr (Exp ExtraOp
x ExtraOp
y)  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Exp (" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"," SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
y SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
")"

data ExtraDefs = ExtraDefs
  { ExtraDefs -> TyCon
maxTyCon  :: TyCon
  , ExtraDefs -> TyCon
minTyCon  :: TyCon
  , ExtraDefs -> TyCon
divTyCon  :: TyCon
  , ExtraDefs -> TyCon
modTyCon  :: TyCon
  , ExtraDefs -> TyCon
flogTyCon :: TyCon
  , ExtraDefs -> TyCon
clogTyCon :: TyCon
  , ExtraDefs -> TyCon
logTyCon  :: TyCon
  , ExtraDefs -> TyCon
gcdTyCon  :: TyCon
  , ExtraDefs -> TyCon
lcmTyCon  :: TyCon
  , ExtraDefs -> TyCon
ordTyCon  :: TyCon
  , ExtraDefs -> TyCon
assertTC  :: TyCon
  }

reifyEOP :: ExtraDefs -> ExtraOp -> Type
reifyEOP :: ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
_ (I Integer
i) = Integer -> Type
mkNumLitTy Integer
i
reifyEOP ExtraDefs
_ (V TyVar
v) = TyVar -> Type
mkTyVarTy TyVar
v
reifyEOP ExtraDefs
_ (C (CType Type
c)) = Type
c
reifyEOP ExtraDefs
defs (Max ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
maxTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (Min ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
minTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (Div ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
divTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (Mod ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
modTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (CLog ExtraOp
x ExtraOp
y) = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
clogTyCon ExtraDefs
defs) [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (FLog ExtraOp
x ExtraOp
y) = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
flogTyCon ExtraDefs
defs) [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (Log ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
logTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (GCD ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
gcdTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (LCM ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp (ExtraDefs -> TyCon
lcmTyCon ExtraDefs
defs)  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]
reifyEOP ExtraDefs
defs (Exp ExtraOp
x ExtraOp
y)  = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon  [ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
                                                       ,ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y]

mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMax ExtraDefs
_ (I Integer
0) ExtraOp
y = (ExtraOp
y, Normalised
Normalised)
mergeMax ExtraDefs
_ ExtraOp
x (I Integer
0) = (ExtraOp
x, Normalised
Normalised)
mergeMax ExtraDefs
defs ExtraOp
x ExtraOp
y =
  let x' :: Type
x' = ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
      y' :: Type
y' = ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y
      z :: CoreSOP
z  = (CoreSOP, [(Type, Type)]) -> CoreSOP
forall a b. (a, b) -> a
fst (Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Type
y',Type
x'])))
#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
  in  case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
z) of
        Just (Bool
True , Set CType
cs) | Set CType -> Bool
forall a. Set a -> Bool
Set.null Set CType
cs -> (ExtraOp
y, Normalised
Normalised)
        Just (Bool
False, Set CType
cs) | Set CType -> Bool
forall a. Set a -> Bool
Set.null Set CType
cs -> (ExtraOp
x, Normalised
Normalised)
#else
  in  case isNatural z of
        Just True  -> (y, Normalised)
        Just False -> (x, Normalised)
#endif
        Maybe (Bool, Set CType)
_ -> (ExtraOp -> ExtraOp -> ExtraOp
Max ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMin ExtraDefs
defs ExtraOp
x ExtraOp
y =
  let x' :: Type
x' = ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
x
      y' :: Type
y' = ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
y
      z :: CoreSOP
z  = (CoreSOP, [(Type, Type)]) -> CoreSOP
forall a b. (a, b) -> a
fst (Writer [(Type, Type)] CoreSOP -> (CoreSOP, [(Type, Type)])
forall w a. Writer w a -> (a, w)
runWriter (Type -> Writer [(Type, Type)] CoreSOP
normaliseNat (TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Type
y',Type
x'])))
#if MIN_VERSION_ghc_typelits_natnormalise(0,7,0)
  in  case WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural CoreSOP
z) of
        Just (Bool
True, Set CType
cs) | Set CType -> Bool
forall a. Set a -> Bool
Set.null Set CType
cs -> (ExtraOp
x, Normalised
Normalised)
        Just (Bool
False,Set CType
cs) | Set CType -> Bool
forall a. Set a -> Bool
Set.null Set CType
cs -> (ExtraOp
y, Normalised
Normalised)
#else
  in  case isNatural z of
        Just True  -> (x, Normalised)
        Just False -> (y, Normalised)
#endif
        Maybe (Bool, Set CType)
_ -> (ExtraOp -> ExtraOp -> ExtraOp
Min ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeDiv :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeDiv ExtraOp
_     (I Integer
0)      = Maybe NormaliseResult
forall a. Maybe a
Nothing
mergeDiv (I Integer
i) (I Integer
j)      = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (Integer -> ExtraOp
I (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
div Integer
i Integer
j), Normalised
Normalised)
mergeDiv ExtraOp
x ExtraOp
y              = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp -> ExtraOp -> ExtraOp
Div ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeMod :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeMod ExtraOp
_     (I Integer
0)      = Maybe NormaliseResult
forall a. Maybe a
Nothing
mergeMod (I Integer
i) (I Integer
j)      = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (Integer -> ExtraOp
I (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod Integer
i Integer
j), Normalised
Normalised)
mergeMod ExtraOp
x ExtraOp
y              = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp -> ExtraOp -> ExtraOp
Mod ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeFLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeFLog (I Integer
i) ExtraOp
_         | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2  = Maybe NormaliseResult
forall a. Maybe a
Nothing
mergeFLog ExtraOp
i     (Exp ExtraOp
j ExtraOp
k) | ExtraOp
i ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
j = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp
k, Normalised
Normalised)
mergeFLog (I Integer
i) (I Integer
j)              = (Integer -> NormaliseResult)
-> Maybe Integer -> Maybe NormaliseResult
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Integer
r -> (Integer -> ExtraOp
I Integer
r, Normalised
Normalised)) (Integer -> Integer -> Maybe Integer
flogBase Integer
i Integer
j)
mergeFLog ExtraOp
x     ExtraOp
y                  = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp -> ExtraOp -> ExtraOp
FLog ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeCLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeCLog (I Integer
i) ExtraOp
_         | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2  = Maybe NormaliseResult
forall a. Maybe a
Nothing
mergeCLog ExtraOp
i     (Exp ExtraOp
j ExtraOp
k) | ExtraOp
i ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
j = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp
k, Normalised
Normalised)
mergeCLog (I Integer
i) (I Integer
j)              = (Integer -> NormaliseResult)
-> Maybe Integer -> Maybe NormaliseResult
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Integer
r -> (Integer -> ExtraOp
I Integer
r, Normalised
Normalised)) (Integer -> Integer -> Maybe Integer
clogBase Integer
i Integer
j)
mergeCLog ExtraOp
x     ExtraOp
y                  = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp -> ExtraOp -> ExtraOp
CLog ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeLog :: ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeLog (I Integer
i) ExtraOp
_          | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2   = Maybe NormaliseResult
forall a. Maybe a
Nothing
mergeLog ExtraOp
b     (Exp ExtraOp
b' ExtraOp
y) | ExtraOp
b ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
b' = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp
y, Normalised
Normalised)
mergeLog (I Integer
i) (I Integer
j)                = (Integer -> NormaliseResult)
-> Maybe Integer -> Maybe NormaliseResult
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Integer
r -> (Integer -> ExtraOp
I Integer
r, Normalised
Normalised)) (Integer -> Integer -> Maybe Integer
exactLogBase Integer
i Integer
j)
mergeLog ExtraOp
x     ExtraOp
y                    = NormaliseResult -> Maybe NormaliseResult
forall a. a -> Maybe a
Just (ExtraOp -> ExtraOp -> ExtraOp
Log ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult
mergeGCD :: ExtraOp -> ExtraOp -> NormaliseResult
mergeGCD (I Integer
i) (I Integer
j) = (Integer -> ExtraOp
I (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
gcd Integer
i Integer
j), Normalised
Normalised)
mergeGCD ExtraOp
x     ExtraOp
y     = (ExtraOp -> ExtraOp -> ExtraOp
GCD ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult
mergeLCM :: ExtraOp -> ExtraOp -> NormaliseResult
mergeLCM (I Integer
i) (I Integer
j) = (Integer -> ExtraOp
I (Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
lcm Integer
i Integer
j), Normalised
Normalised)
mergeLCM ExtraOp
x     ExtraOp
y     = (ExtraOp -> ExtraOp -> ExtraOp
LCM ExtraOp
x ExtraOp
y, Normalised
Untouched)

mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult
mergeExp :: ExtraOp -> ExtraOp -> NormaliseResult
mergeExp (I Integer
i) (I Integer
j)                = (Integer -> ExtraOp
I (Integer
iInteger -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
j), Normalised
Normalised)
mergeExp ExtraOp
b     (Log ExtraOp
b' ExtraOp
y) | ExtraOp
b ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
b' = (ExtraOp
y, Normalised
Normalised)
mergeExp ExtraOp
x     ExtraOp
y                    = (ExtraOp -> ExtraOp -> ExtraOp
Exp ExtraOp
x ExtraOp
y, Normalised
Untouched)

-- | \x y -> logBase x y, x > 1 && y > 0

flogBase :: Integer -> Integer -> Maybe Integer
flogBase :: Integer -> Integer -> Maybe Integer
flogBase Integer
x Integer
y | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int# -> Integer
smallInteger (Integer -> Integer -> Int#
integerLogBase# Integer
x Integer
y))
flogBase Integer
_ Integer
_         = Maybe Integer
forall a. Maybe a
Nothing

-- | \x y -> ceiling (logBase x y), x > 1 && y > 0

clogBase :: Integer -> Integer -> Maybe Integer
clogBase :: Integer -> Integer -> Maybe Integer
clogBase Integer
x Integer
y | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 =
  let z1 :: Int#
z1 = Integer -> Integer -> Int#
integerLogBase# Integer
x Integer
y
      z2 :: Int#
z2 = Integer -> Integer -> Int#
integerLogBase# Integer
x (Integer
yInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
  in  case Integer
y of
         Integer
1 -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
         Integer
_ | Int# -> Bool
isTrue# (Int#
z1 Int# -> Int# -> Int#
==# Int#
z2) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int# -> Integer
smallInteger (Int#
z1 Int# -> Int# -> Int#
+# Int#
1#))
           | Bool
otherwise           -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int# -> Integer
smallInteger Int#
z1)
clogBase Integer
_ Integer
_ = Maybe Integer
forall a. Maybe a
Nothing

-- | \x y -> logBase x y, x > 1 && y > 0, logBase x y == ceiling (logBase x y)

exactLogBase :: Integer -> Integer -> Maybe Integer
exactLogBase :: Integer -> Integer -> Maybe Integer
exactLogBase Integer
x Integer
y | Integer
y Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 =
  let z1 :: Int#
z1 = Integer -> Integer -> Int#
integerLogBase# Integer
x Integer
y
      z2 :: Int#
z2 = Integer -> Integer -> Int#
integerLogBase# Integer
x (Integer
yInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)
  in  case Integer
y of
        Integer
1 -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
        Integer
_ | Int# -> Bool
isTrue# (Int#
z1 Int# -> Int# -> Int#
==# Int#
z2) -> Maybe Integer
forall a. Maybe a
Nothing
          | Bool
otherwise           -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int# -> Integer
smallInteger Int#
z1)
exactLogBase Integer
_ Integer
_ = Maybe Integer
forall a. Maybe a
Nothing