{-|
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 (..)
  , 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 API

#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

-- internal

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 ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult
f MaybeT TcPluginM NormaliseResult
x MaybeT TcPluginM NormaliseResult
y = do
  (ExtraOp
x', Normalised
n1) <- MaybeT TcPluginM NormaliseResult
x
  (ExtraOp
y', Normalised
n2) <- MaybeT TcPluginM NormaliseResult
y
  (ExtraOp
res, Normalised
n3) <- ExtraOp -> ExtraOp -> MaybeT TcPluginM NormaliseResult
f ExtraOp
x' ExtraOp
y'
  NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM 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 NormaliseResult
normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
ty | Just Type
ty1 <- Type -> Maybe Type
coreView Type
ty = ExtraDefs -> Type -> MaybeT TcPluginM NormaliseResult
normaliseNat ExtraDefs
defs Type
ty1
normaliseNat ExtraDefs
_ (TyVarTy TyVar
v)          = NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyVar -> ExtraOp
V TyVar
v, Normalised
Untouched)
normaliseNat ExtraDefs
_ (LitTy (NumTyLit Integer
i)) = NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> ExtraOp
I Integer
i, Normalised
Untouched)
normaliseNat ExtraDefs
defs (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 NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
-> MaybeT TcPluginM NormaliseResult
mergeNormResWith (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall a. a -> TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall a. a -> TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall a. a -> TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall a. a -> TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> TcPluginM (Maybe NormaliseResult)
-> MaybeT TcPluginM NormaliseResult
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe NormaliseResult -> TcPluginM (Maybe NormaliseResult)
forall a. a -> TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
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 (\ExtraOp
x' ExtraOp
y' -> NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM a
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 ExtraDefs
defs (TyConApp TyCon
tc [Type]
tys) = do
  let mergeExtraOp :: [(Maybe NormaliseResult, Type)] -> [Type]
mergeExtraOp [] = []
      mergeExtraOp ((Just (ExtraOp
op, Normalised
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 [Maybe NormaliseResult]
-> MaybeT TcPluginM [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 (Maybe NormaliseResult)]
-> TcPluginM [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 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 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 NormaliseResult
forall a. a -> MaybeT TcPluginM 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)

normaliseNat ExtraDefs
_ Type
t = NormaliseResult -> MaybeT TcPluginM NormaliseResult
forall a. a -> MaybeT TcPluginM 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 UnifyResult
unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult
unifyExtra Ct
ct ExtraOp
u ExtraOp
v = do
  String -> SDoc -> TcPluginM ()
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 UnifyResult
forall a. a -> TcPluginM 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