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

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

-- external
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 (..))

-- ghc-tcplugin-api
import GHC.TcPlugin.API

-- GHC API
import GHC.Builtin.Types.Literals (typeNatExpTyCon)
import GHC.Core.TyCo.Rep (Type (..), TyLit (..))
import GHC.Core.Type (coreView)
import GHC.Types.Unique.Set (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)
import GHC.Utils.Outputable (($$), text)

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

mergeNormResWith
  :: (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
  -> MaybeT (TcPluginM 'Solve) NormaliseResult
  -> MaybeT (TcPluginM 'Solve) NormaliseResult
  -> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith :: (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult
f MaybeT (TcPluginM 'Solve) NormaliseResult
x MaybeT (TcPluginM 'Solve) NormaliseResult
y = do
  (ExtraOp
x', Normalised
n1) <- MaybeT (TcPluginM 'Solve) NormaliseResult
x
  (ExtraOp
y', Normalised
n2) <- MaybeT (TcPluginM 'Solve) NormaliseResult
y
  (ExtraOp
res, Normalised
n3) <- ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult
f ExtraOp
x' ExtraOp
y'
  NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
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 'Solve) NormaliseResult
normaliseNat :: ExtraDefs -> Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
normaliseNat ExtraDefs
defs = Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go
 where
  go :: Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
  go :: Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
ty | Just Type
ty1 <- Type -> Maybe Type
coreView Type
ty = Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
ty1
  go (TyVarTy TyVar
v)          = NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar -> ExtraOp
V TyVar
v, Normalised
Untouched)
  go (LitTy (NumTyLit Integer
i)) = NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> ExtraOp
I Integer
i, Normalised
Untouched)
  go (TyConApp TyCon
tc [Type
x,Type
y])
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
maxTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMax ExtraDefs
defs ExtraOp
x' ExtraOp
y'))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
minTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraDefs -> ExtraOp -> ExtraOp -> NormaliseResult
mergeMin ExtraDefs
defs ExtraOp
x' ExtraOp
y'))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
divTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> TcPluginM 'Solve (Maybe NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM 'Solve (Maybe NormaliseResult)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeDiv ExtraOp
x' ExtraOp
y')))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
modTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> TcPluginM 'Solve (Maybe NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM 'Solve (Maybe NormaliseResult)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeMod ExtraOp
x' ExtraOp
y')))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
flogTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> TcPluginM 'Solve (Maybe NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM 'Solve (Maybe NormaliseResult)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeFLog ExtraOp
x' ExtraOp
y')))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
clogTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> TcPluginM 'Solve (Maybe NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM 'Solve (Maybe NormaliseResult)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeCLog ExtraOp
x' ExtraOp
y')))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
logTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> TcPluginM 'Solve (Maybe NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM 'Solve (Maybe NormaliseResult)
forall a. a -> TcPluginM 'Solve a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> Maybe NormaliseResult
mergeLog ExtraOp
x' ExtraOp
y')))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
gcdTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> NormaliseResult
mergeGCD ExtraOp
x' ExtraOp
y'))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraDefs -> TyCon
lcmTyCon ExtraDefs
defs
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> NormaliseResult
mergeLCM ExtraOp
x' ExtraOp
y'))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)
    | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatExpTyCon
    = (ExtraOp -> ExtraOp -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
-> MaybeT (TcPluginM 'Solve) NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtraOp -> ExtraOp -> NormaliseResult
mergeExp ExtraOp
x' ExtraOp
y'))
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
x)
                       (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go Type
y)

  go (TyConApp TyCon
tc [Type]
tys) = do
    let mergeExtraOp :: [(Maybe NormaliseResult, Type)] -> [Type]
mergeExtraOp [] = []
        mergeExtraOp ((Just (ExtraOp
op, Normalised []), Type
_):[(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 ((Maybe NormaliseResult
_, Type
ty):[(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 'Solve [Maybe NormaliseResult]
-> MaybeT (TcPluginM 'Solve) [Maybe NormaliseResult]
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ([TcPluginM 'Solve (Maybe NormaliseResult)]
-> TcPluginM 'Solve [Maybe NormaliseResult]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (MaybeT (TcPluginM 'Solve) NormaliseResult
-> TcPluginM 'Solve (Maybe NormaliseResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (TcPluginM 'Solve) NormaliseResult
 -> TcPluginM 'Solve (Maybe NormaliseResult))
-> (Type -> MaybeT (TcPluginM 'Solve) NormaliseResult)
-> Type
-> TcPluginM 'Solve (Maybe NormaliseResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> MaybeT (TcPluginM 'Solve) NormaliseResult
go (Type -> TcPluginM 'Solve (Maybe NormaliseResult))
-> [Type] -> [TcPluginM 'Solve (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 a b. (a -> b -> b) -> b -> [a] -> b
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 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
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)

  go Type
t = NormaliseResult -> MaybeT (TcPluginM 'Solve) NormaliseResult
forall a. a -> MaybeT (TcPluginM 'Solve) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CType -> ExtraOp
C (Type -> CType
CType Type
t), Normalised
Untouched)

-- | 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 UnifyResult
Win  = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Win"
  ppr UnifyResult
Lose = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Lose"
  ppr UnifyResult
Draw = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Draw"

unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM 'Solve UnifyResult
unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM 'Solve UnifyResult
unifyExtra Ct
ct ExtraOp
u ExtraOp
v = do
  String -> SDoc -> TcPluginM 'Solve ()
forall (m :: * -> *). MonadTcPlugin m => String -> SDoc -> m ()
tcPluginTrace String
"unifyExtra" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
u SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ ExtraOp -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExtraOp
v)
  UnifyResult -> TcPluginM 'Solve UnifyResult
forall a. a -> TcPluginM 'Solve a
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' ExtraOp
u 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 ExtraOp
a ExtraOp
b | ExtraOp
a ExtraOp -> ExtraOp -> Bool
forall a. Eq a => a -> a -> Bool
== ExtraOp
b = UnifyResult
Win
    -- The following operations commute
    go (Max ExtraOp
a ExtraOp
b) (Max ExtraOp
x ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    go (Min ExtraOp
a ExtraOp
b) (Min ExtraOp
x ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    go (GCD ExtraOp
a ExtraOp
b) (GCD ExtraOp
x ExtraOp
y) = UnifyResult -> UnifyResult -> UnifyResult
commuteResult (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
a ExtraOp
y) (ExtraOp -> ExtraOp -> UnifyResult
go ExtraOp
b ExtraOp
x)
    go (LCM ExtraOp
a ExtraOp
b) (LCM ExtraOp
x 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 ExtraOp
a 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 UnifyResult
Win  UnifyResult
Win  = UnifyResult
Win
    commuteResult UnifyResult
Lose UnifyResult
_    = UnifyResult
Lose
    commuteResult UnifyResult
_    UnifyResult
Lose = UnifyResult
Lose
    commuteResult UnifyResult
_    UnifyResult
_    = UnifyResult
Draw

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

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

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