{-|
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 #-}

module GHC.TypeLits.Extra.Solver.Unify
  ( ExtraDefs (..)
  , UnifyResult (..)
  , normaliseNat
  , unifyExtra
  )
where

-- external
import Control.Monad.Trans.Class    (lift)
import Control.Monad.Trans.Maybe    (MaybeT (..))
import Control.Monad.Trans.Writer.Strict (runWriter)
import Data.Function                (on)
import GHC.TypeLits.Normalise.Unify (CType (..))
import qualified GHC.TypeLits.Normalise.Unify as Normalise

-- GHC API
import Outputable (Outputable (..), ($$), text)
import TcPluginM  (TcPluginM, matchFam, tcPluginTrace)
import TcRnMonad  (Ct)
import TcTypeNats (typeNatExpTyCon)
import Type       (TyVar, coreView)
import TyCoRep    (Type (..), TyLit (..))
import UniqSet    (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)

-- internal
import GHC.TypeLits.Extra.Solver.Operations

normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat defs :: ExtraDefs
defs ty :: Type
ty | Just ty1 :: Type
ty1 <- Type -> Maybe Type
coreView Type
ty = ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
ty1
normaliseNat _ (TyVarTy v :: Var
v)          = ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var -> ExtraOp
V Var
v)
normaliseNat _ (LitTy (NumTyLit i :: Integer
i)) = ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> ExtraOp
I Integer
i)
normaliseNat defs :: ExtraDefs
defs (TyConApp tc :: TyCon
tc [x :: Type
x,y :: Type
y])
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
maxTyCon ExtraDefs
defs = ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp
mergeMax ExtraDefs
defs (ExtraOp -> ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> ExtraOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                                        MaybeT TcPluginM (ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
minTyCon ExtraDefs
defs = ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp
mergeMin ExtraDefs
defs (ExtraOp -> ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> ExtraOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                                        MaybeT TcPluginM (ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
divTyCon ExtraDefs
defs = do ExtraOp
x' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                             ExtraOp
y' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
                             TcPluginM (Maybe ExtraOp) -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe ExtraOp -> TcPluginM (Maybe ExtraOp)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe ExtraOp
mergeDiv ExtraOp
x' ExtraOp
y'))
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
modTyCon ExtraDefs
defs = do ExtraOp
x' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                             ExtraOp
y' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
                             TcPluginM (Maybe ExtraOp) -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe ExtraOp -> TcPluginM (Maybe ExtraOp)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe ExtraOp
mergeMod ExtraOp
x' ExtraOp
y'))
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
flogTyCon ExtraDefs
defs = do ExtraOp
x' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                              ExtraOp
y' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
                              TcPluginM (Maybe ExtraOp) -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe ExtraOp -> TcPluginM (Maybe ExtraOp)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe ExtraOp
mergeFLog ExtraOp
x' ExtraOp
y'))
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
clogTyCon ExtraDefs
defs = do ExtraOp
x' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                              ExtraOp
y' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
                              TcPluginM (Maybe ExtraOp) -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe ExtraOp -> TcPluginM (Maybe ExtraOp)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe ExtraOp
mergeCLog ExtraOp
x' ExtraOp
y'))
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
logTyCon ExtraDefs
defs = do ExtraOp
x' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                             ExtraOp
y' <- ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
                             TcPluginM (Maybe ExtraOp) -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe ExtraOp -> TcPluginM (Maybe ExtraOp)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe ExtraOp
mergeLog ExtraOp
x' ExtraOp
y'))
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
gcdTyCon ExtraDefs
defs = ExtraOp -> ExtraOp -> ExtraOp
mergeGCD (ExtraOp -> ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> ExtraOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                                   MaybeT TcPluginM (ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
lcmTyCon ExtraDefs
defs = ExtraOp -> ExtraOp -> ExtraOp
mergeLCM (ExtraOp -> ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> ExtraOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                                   MaybeT TcPluginM (ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y
  | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatExpTyCon = ExtraOp -> ExtraOp -> ExtraOp
mergeExp (ExtraOp -> ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp
-> MaybeT TcPluginM (ExtraOp -> ExtraOp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
x
                                     MaybeT TcPluginM (ExtraOp -> ExtraOp)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM ExtraOp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
y

normaliseNat defs :: ExtraDefs
defs (TyConApp tc :: TyCon
tc tys :: [Type]
tys) = do
  [Type]
tys'   <- (Type -> MaybeT TcPluginM Type)
-> [Type] -> MaybeT TcPluginM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((ExtraOp -> Type)
-> MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs) (MaybeT TcPluginM ExtraOp -> MaybeT TcPluginM Type)
-> (Type -> MaybeT TcPluginM ExtraOp)
-> Type
-> MaybeT TcPluginM Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs) [Type]
tys
  Maybe (TcCoercion, Type)
tyM    <- TcPluginM (Maybe (TcCoercion, Type))
-> MaybeT TcPluginM (Maybe (TcCoercion, Type))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, Type))
matchFam TyCon
tc [Type]
tys')
  case Maybe (TcCoercion, Type)
tyM of
    Just (_,ty :: Type
ty) -> ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp
normaliseNat ExtraDefs
defs Type
ty
    _ -> let q :: CoreSOP
q = (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
Normalise.normaliseNat (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys)))
         in  ExtraOp -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. Monad m => a -> m a
return (CType -> ExtraOp
C (Type -> CType
CType (CoreSOP -> Type
Normalise.reifySOP CoreSOP
q)))

normaliseNat _ t :: Type
t = ExtraOp -> MaybeT TcPluginM ExtraOp
forall (m :: * -> *) a. Monad m => a -> m a
return (CType -> ExtraOp
C (Type -> CType
CType Type
t))

-- | Result of comparing two 'SOP' terms, returning a potential substitution
-- list under which the two terms are equal.
data UnifyResult
  = Win  -- ^ Two terms are equal
  | Lose -- ^ Two terms are /not/ equal
  | Draw -- ^ We don't know if the two terms are equal

instance Outputable UnifyResult where
  ppr :: UnifyResult -> SDoc
ppr Win  = String -> SDoc
text "Win"
  ppr Lose = String -> SDoc
text "Lose"
  ppr Draw = String -> SDoc
text "Draw"

unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
unifyExtra ct :: Ct
ct u :: ExtraOp
u v :: ExtraOp
v = do
  String -> SDoc -> TcPluginM ()
tcPluginTrace "unifyExtra" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
u SDoc -> SDoc -> SDoc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
v)
  UnifyResult -> TcPluginM UnifyResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> UnifyResult
unifyExtra' ExtraOp
u ExtraOp
v)

unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult
unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult
unifyExtra' u :: ExtraOp
u v :: ExtraOp
v
  | ExtraOp -> ExtraOp -> Bool
eqFV ExtraOp
u ExtraOp
v
  = ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
u ExtraOp
v
  | Bool
otherwise
  = UnifyResult
Draw
  where
    go :: ExtraOp -> ExtraOp -> UnifyResult
go a :: ExtraOp
a b :: ExtraOp
b | ExtraOp
a ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
b = UnifyResult
Win
    -- The following operations commute
    go (Max a :: ExtraOp
a b :: ExtraOp
b) (Max x :: ExtraOp
x y :: ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    go (Min a :: ExtraOp
a b :: ExtraOp
b) (Min x :: ExtraOp
x y :: ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    go (GCD a :: ExtraOp
a b :: ExtraOp
b) (GCD x :: ExtraOp
x y :: ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    go (LCM a :: ExtraOp
a b :: ExtraOp
b) (LCM x :: ExtraOp
x y :: ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    -- If there are operations contained in the type which this solver does
    -- not understand, then the result is a Draw
    go a :: ExtraOp
a b :: ExtraOp
b = if ExtraOp -> Bool
containsConstants ExtraOp
a Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
b then UnifyResult
Draw else UnifyResult
Lose

    commuteResult :: UnifyResult -> UnifyResult -> UnifyResult
commuteResult Win  Win  = UnifyResult
Win
    commuteResult Lose _    = UnifyResult
Lose
    commuteResult _    Lose = UnifyResult
Lose
    commuteResult _    _    = UnifyResult
Draw

fvOP :: ExtraOp -> UniqSet TyVar
fvOP :: ExtraOp -> UniqSet Var
fvOP (I _)      = UniqSet Var
forall a. UniqSet a
emptyUniqSet
fvOP (V v :: Var
v)      = Var -> UniqSet Var
forall a. Uniquable a => a -> UniqSet a
unitUniqSet Var
v
fvOP (C _)      = UniqSet Var
forall a. UniqSet a
emptyUniqSet
fvOP (Max x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (Min x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (Div x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (Mod x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (FLog x :: ExtraOp
x y :: ExtraOp
y) = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (CLog x :: ExtraOp
x y :: ExtraOp
y) = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (Log x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (GCD x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (LCM x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y
fvOP (Exp x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> UniqSet Var
fvOP ExtraOp
x UniqSet Var -> UniqSet Var -> UniqSet Var
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` ExtraOp -> UniqSet Var
fvOP ExtraOp
y

eqFV :: ExtraOp -> ExtraOp -> Bool
eqFV :: ExtraOp -> ExtraOp -> Bool
eqFV = UniqSet Var -> UniqSet Var -> Bool
forall a. Eq a => a -> a -> Bool
(==) (UniqSet Var -> UniqSet Var -> Bool)
-> (ExtraOp -> UniqSet Var) -> ExtraOp -> ExtraOp -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` ExtraOp -> UniqSet Var
fvOP

containsConstants :: ExtraOp -> Bool
containsConstants :: ExtraOp -> Bool
containsConstants (I _) = Bool
False
containsConstants (V _) = Bool
False
containsConstants (C _) = Bool
True
containsConstants (Max x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (Min x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (Div x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (Mod x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (FLog x :: ExtraOp
x y :: ExtraOp
y) = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (CLog x :: ExtraOp
x y :: ExtraOp
y) = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (Log x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (GCD x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (LCM x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y
containsConstants (Exp x :: ExtraOp
x y :: ExtraOp
y)  = ExtraOp -> Bool
containsConstants ExtraOp
x Bool -> Bool -> Bool
|| ExtraOp -> Bool
containsConstants ExtraOp
y