{-# LANGUAGE CPP #-}
module GHC.TypeLits.Extra.Solver.Unify
( ExtraDefs (..)
, UnifyResult (..)
, NormaliseResult
, normaliseNat
, unifyExtra
)
where
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Maybe (MaybeT (..))
import Data.Maybe (catMaybes)
import Data.Function (on)
import GHC.TypeLits.Normalise.Unify (CType (..))
#if MIN_VERSION_ghc(9,0,0)
import GHC.Builtin.Types.Literals (typeNatExpTyCon)
import GHC.Core.TyCo.Rep (Type (..), TyLit (..))
import GHC.Core.Type (TyVar, coreView)
import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)
import GHC.Tc.Types.Constraint (Ct)
import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
import GHC.Utils.Outputable (Outputable (..), ($$), text)
#else
import Outputable (Outputable (..), ($$), text)
import TcPluginM (TcPluginM, tcPluginTrace)
import TcTypeNats (typeNatExpTyCon)
import Type (TyVar, coreView)
import TyCoRep (Type (..), TyLit (..))
import UniqSet (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
#if MIN_VERSION_ghc(8,10,0)
import Constraint (Ct)
#else
import TcRnMonad (Ct)
#endif
#endif
import GHC.TypeLits.Extra.Solver.Operations
mergeNormResWith
:: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith :: (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith f :: ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult
f x :: MaybeT TcPluginM NormaliseResult
x y :: MaybeT TcPluginM NormaliseResult
y = do
(x' :: ExtraOp
x', n1 :: Normalised
n1) <- MaybeT TcPluginM NormaliseResult
x
(y' :: ExtraOp
y', n2 :: Normalised
n2) <- MaybeT TcPluginM NormaliseResult
y
(res :: ExtraOp
res, n3 :: Normalised
n3) <- ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult
f ExtraOp
x' ExtraOp
y'
NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExtraOp
res, Normalised
n1 Normalised -> Normalised -> Normalised
`mergeNormalised` Normalised
n2 Normalised -> Normalised -> Normalised
`mergeNormalised` Normalised
n3)
normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat defs :: ExtraDefs
defs ty :: Type
ty | Just ty1 :: Type
ty1 <- Type -> Maybe Type
coreView Type
ty = ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
ty1
normaliseNat _ (TyVarTy v :: Var
v) = NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var -> ExtraOp
V Var
v, Normalised
Untouched)
normaliseNat _ (LitTy (NumTyLit i :: Integer
i)) = NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> ExtraOp
I Integer
i, Normalised
Untouched)
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 = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMax ExtraDefs
defs ExtraOp
x' ExtraOp
y'))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
minTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMin ExtraDefs
defs ExtraOp
x' ExtraOp
y'))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
divTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeDiv ExtraOp
x' ExtraOp
y')))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
modTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeMod ExtraOp
x' ExtraOp
y')))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
flogTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeFLog ExtraOp
x' ExtraOp
y')))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
clogTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeCLog ExtraOp
x' ExtraOp
y')))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
logTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeLog ExtraOp
x' ExtraOp
y')))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
gcdTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> NormaliseResult
mergeGCD ExtraOp
x' ExtraOp
y'))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
lcmTyCon ExtraDefs
defs = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> NormaliseResult
mergeLCM ExtraOp
x' ExtraOp
y'))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatExpTyCon = (ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\x' :: ExtraOp
x' y' :: ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> NormaliseResult
mergeExp ExtraOp
x' ExtraOp
y'))
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
x)
(ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
y)
normaliseNat defs :: ExtraDefs
defs (TyConApp tc :: TyCon
tc tys :: [Type]
tys) = do
let mergeExtraOp :: [(Maybe NormaliseResult, Type)] -> [Type]
mergeExtraOp [] = []
mergeExtraOp ((Just (op :: ExtraOp
op, Normalised), _):xs :: [(Maybe NormaliseResult, Type)]
xs) = ExtraDefs -> ExtraOp -> Type
reifyEOP ExtraDefs
defs ExtraOp
opType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[(Maybe NormaliseResult, Type)] -> [Type]
mergeExtraOp [(Maybe NormaliseResult, Type)]
xs
mergeExtraOp ((_, ty :: Type
ty):xs :: [(Maybe NormaliseResult, Type)]
xs) = Type
tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[(Maybe NormaliseResult, Type)] -> [Type]
mergeExtraOp [(Maybe NormaliseResult, Type)]
xs
[Maybe NormaliseResult]
normResults <- TcPluginM [Maybe NormaliseResult]
-> MaybeT TcPluginM [Maybe NormaliseResult]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ([TcPluginM (Maybe NormaliseResult)]
-> TcPluginM [Maybe NormaliseResult]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence (MaybeT TcPluginM NormaliseResult
-> TcPluginM (Maybe NormaliseResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT TcPluginM NormaliseResult
-> TcPluginM (Maybe NormaliseResult))
-> (Type -> MaybeT TcPluginM NormaliseResult)
-> Type
-> TcPluginM (Maybe NormaliseResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs (Type -> TcPluginM (Maybe NormaliseResult))
-> [Type] -> [TcPluginM (Maybe NormaliseResult)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
tys))
let anyNormalised :: Normalised
anyNormalised = (Normalised -> Normalised -> Normalised)
-> Normalised -> [Normalised] -> Normalised
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Normalised -> Normalised -> Normalised
mergeNormalised Normalised
Untouched (NormaliseResult -> Normalised
forall a b. (a, b) -> b
snd (NormaliseResult -> Normalised)
-> [NormaliseResult] -> [Normalised]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Maybe NormaliseResult] -> [NormaliseResult]
forall a. [Maybe a] -> [a]
catMaybes [Maybe NormaliseResult]
normResults)
let tys' :: [Type]
tys' = [(Maybe NormaliseResult, Type)] -> [Type]
mergeExtraOp ([Maybe NormaliseResult]
-> [Type] -> [(Maybe NormaliseResult, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe NormaliseResult]
normResults [Type]
tys)
NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CType -> ExtraOp
C (Type -> CType
CType (TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys')), Normalised
anyNormalised)
normaliseNat _ t :: Type
t = NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. Monad m => a -> m a
return (CType -> ExtraOp
C (Type -> CType
CType Type
t), Normalised
Untouched)
data UnifyResult
= Win
| Lose
| Draw
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
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
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
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)
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