{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE RecordWildCards #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
#if __GLASGOW_HASKELL__ < 801
#define nonDetCmpType cmpType
#endif
module GHC.TypeLits.Normalise.Unify
(
CType (..)
, CoreSOP
, normaliseNat
, normaliseNatEverywhere
, normaliseSimplifyNat
, reifySOP
, UnifyItem (..)
, CoreUnify
, substsSOP
, substsSubst
, UnifyResult (..)
, unifyNats
, unifiers
, fvSOP
, subtractIneq
, solveIneq
, ineqToSubst
, subtractionToPred
, instantSolveIneq
, solvedInEqSmallestConstraint
, isNatural
)
where
import Control.Arrow (first, second)
import Control.Monad.Trans.Writer.Strict
import Data.Function (on)
import Data.List ((\\), intersect, nub)
import Data.Maybe (fromMaybe, mapMaybe, isJust)
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Base (isTrue#,(==#))
import GHC.Integer (smallInteger)
import GHC.Integer.Logarithms (integerLogBase#)
#if MIN_VERSION_ghc(9,0,0)
import GHC.Builtin.Types (boolTy, promotedTrueDataCon)
import GHC.Builtin.Types.Literals
(typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon, typeNatSubTyCon)
#if MIN_VERSION_ghc(9,2,0)
import GHC.Builtin.Types (naturalTy, promotedFalseDataCon)
import GHC.Builtin.Types.Literals (typeNatCmpTyCon)
#else
import GHC.Builtin.Types (typeNatKind)
import GHC.Builtin.Types.Literals (typeNatLeqTyCon)
#endif
import GHC.Core.Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)
import GHC.Core.TyCon (TyCon)
#if MIN_VERSION_ghc(9,6,0)
import GHC.Core.Type
(PredType, TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy, typeKind)
import GHC.Core.TyCo.Compare
(eqType, nonDetCmpType)
#else
import GHC.Core.Type
(PredType, TyVar, coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy, nonDetCmpType, typeKind)
#endif
import GHC.Core.TyCo.Rep (Kind, Type (..), TyLit (..))
import GHC.Tc.Plugin (TcPluginM, tcPluginTrace)
import GHC.Tc.Types.Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)
import GHC.Types.Unique.Set
(UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets, unitUniqSet)
import GHC.Utils.Outputable (Outputable (..), (<+>), ($$), text)
#else
import Outputable (Outputable (..), (<+>), ($$), text)
import TcPluginM (TcPluginM, tcPluginTrace)
import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,
typeNatSubTyCon, typeNatLeqTyCon)
import TyCon (TyCon)
import Type (TyVar,
coreView, eqType, mkNumLitTy, mkTyConApp, mkTyVarTy,
nonDetCmpType, PredType, typeKind)
import TyCoRep (Kind, Type (..), TyLit (..))
import TysWiredIn (boolTy, promotedTrueDataCon, typeNatKind)
import UniqSet (UniqSet, unionManyUniqSets, emptyUniqSet, unionUniqSets,
unitUniqSet)
#if MIN_VERSION_ghc(8,10,0)
import Constraint (Ct, ctEvidence, ctEvId, ctEvPred, isGiven)
import Predicate (EqRel (NomEq), Pred (EqPred), classifyPredType, mkPrimEqPred)
#else
import TcRnMonad (Ct, ctEvidence, isGiven)
import TcRnTypes (ctEvPred)
import Type (EqRel (NomEq), PredTree (EqPred), classifyPredType, mkPrimEqPred)
#endif
#endif
import GHC.TypeLits.Normalise.SOP
import GHC.TypeLits (Nat)
#if MIN_VERSION_ghc(9,2,0)
typeNatKind :: Type
typeNatKind :: Type
typeNatKind = Type
naturalTy
#endif
newtype CType = CType { CType -> Type
unCType :: Type }
deriving CType -> SDoc
(CType -> SDoc) -> Outputable CType
forall a. (a -> SDoc) -> Outputable a
$cppr :: CType -> SDoc
ppr :: CType -> SDoc
Outputable
instance Eq CType where
(CType Type
ty1) == :: CType -> CType -> Bool
== (CType Type
ty2) = Type -> Type -> Bool
eqType Type
ty1 Type
ty2
instance Ord CType where
compare :: CType -> CType -> Ordering
compare (CType Type
ty1) (CType Type
ty2) = Type -> Type -> Ordering
nonDetCmpType Type
ty1 Type
ty2
type CoreSOP = SOP TyVar CType
type CoreProduct = Product TyVar CType
type CoreSymbol = Symbol TyVar CType
normaliseNat :: Type -> Writer [(Type,Type)] CoreSOP
normaliseNat :: Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
ty | Just Type
ty1 <- Type -> Maybe Type
coreView Type
ty = Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
ty1
normaliseNat (TyVarTy TyVar
v) = SOP TyVar CType -> Writer [(Type, Type)] (SOP TyVar CType)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [TyVar -> Symbol TyVar CType
forall v c. v -> Symbol v c
V TyVar
v]])
normaliseNat (LitTy (NumTyLit Integer
i)) = SOP TyVar CType -> Writer [(Type, Type)] (SOP TyVar CType)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
i]])
normaliseNat (TyConApp TyCon
tc [Type
x,Type
y])
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatAddTyCon = SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
x WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
forall a b.
WriterT [(Type, Type)] Identity (a -> b)
-> WriterT [(Type, Type)] Identity a
-> WriterT [(Type, Type)] Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
y
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatSubTyCon = do
[(Type, Type)] -> WriterT [(Type, Type)] Identity ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [(Type
x,Type
y)]
SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
x
WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
forall a b.
WriterT [(Type, Type)] Identity (a -> b)
-> WriterT [(Type, Type)] Identity a
-> WriterT [(Type, Type)] Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]]) (SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
y)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatMulTyCon = SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
x WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
forall a b.
WriterT [(Type, Type)] Identity (a -> b)
-> WriterT [(Type, Type)] Identity a
-> WriterT [(Type, Type)] Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
y
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
typeNatExpTyCon = SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
normaliseExp (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
x WriterT
[(Type, Type)] Identity (SOP TyVar CType -> SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
-> Writer [(Type, Type)] (SOP TyVar CType)
forall a b.
WriterT [(Type, Type)] Identity (a -> b)
-> WriterT [(Type, Type)] Identity a
-> WriterT [(Type, Type)] Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
y
normaliseNat Type
t = SOP TyVar CType -> Writer [(Type, Type)] (SOP TyVar CType)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [CType -> Symbol TyVar CType
forall v c. c -> Symbol v c
C (Type -> CType
CType Type
t)]])
maybeRunWriter
:: Monoid a
=> Writer a (Maybe b)
-> Writer a (Maybe b)
maybeRunWriter :: forall a b. Monoid a => Writer a (Maybe b) -> Writer a (Maybe b)
maybeRunWriter Writer a (Maybe b)
w =
case Writer a (Maybe b) -> (Maybe b, a)
forall w a. Writer w a -> (a, w)
runWriter Writer a (Maybe b)
w of
(Maybe b
Nothing, a
_) -> Maybe b -> Writer a (Maybe b)
forall a. a -> WriterT a Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
forall a. Maybe a
Nothing
(Maybe b
b, a
a) -> a -> WriterT a Identity ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell a
a WriterT a Identity () -> Writer a (Maybe b) -> Writer a (Maybe b)
forall a b.
WriterT a Identity a
-> WriterT a Identity b -> WriterT a Identity b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe b -> Writer a (Maybe b)
forall a. a -> WriterT a Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe b
b
normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere :: Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere Type
ty0
| TyConApp TyCon
tc [Type]
_fields <- Type
ty0
, TyCon
tc TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCon]
knownTyCons = do
Maybe Type
ty1M <- Writer [(Type, Type)] (Maybe Type)
-> Writer [(Type, Type)] (Maybe Type)
forall a b. Monoid a => Writer a (Maybe b) -> Writer a (Maybe b)
maybeRunWriter (Type -> Writer [(Type, Type)] (Maybe Type)
go Type
ty0)
let ty1 :: Type
ty1 = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
ty0 Maybe Type
ty1M
Type
ty2 <- Type -> Writer [(Type, Type)] Type
normaliseSimplifyNat Type
ty1
Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if Type
ty2 Type -> Type -> Bool
`eqType` Type
ty1 then Maybe Type
ty1M else Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty2)
| Bool
otherwise = Type -> Writer [(Type, Type)] (Maybe Type)
go Type
ty0
where
knownTyCons :: [TyCon]
knownTyCons :: [TyCon]
knownTyCons = [TyCon
typeNatExpTyCon, TyCon
typeNatMulTyCon, TyCon
typeNatSubTyCon, TyCon
typeNatAddTyCon]
go :: Type -> Writer [(Type, Type)] (Maybe Type)
go :: Type -> Writer [(Type, Type)] (Maybe Type)
go (TyConApp TyCon
tc_ [Type]
fields0_) = do
[Maybe Type]
fields1_ <- (Type -> Writer [(Type, Type)] (Maybe Type))
-> [Type] -> WriterT [(Type, Type)] Identity [Maybe Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Writer [(Type, Type)] (Maybe Type)
-> Writer [(Type, Type)] (Maybe Type)
forall a b. Monoid a => Writer a (Maybe b) -> Writer a (Maybe b)
maybeRunWriter (Writer [(Type, Type)] (Maybe Type)
-> Writer [(Type, Type)] (Maybe Type))
-> (Type -> Writer [(Type, Type)] (Maybe Type))
-> Type
-> Writer [(Type, Type)] (Maybe Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Writer [(Type, Type)] (Maybe Type)
cont) [Type]
fields0_
if (Maybe Type -> Bool) -> [Maybe Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Type]
fields1_ then
Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> Maybe Type
forall a. a -> Maybe a
Just (TyCon -> [Type] -> Type
TyConApp TyCon
tc_ ((Type -> Maybe Type -> Type) -> [Type] -> [Maybe Type] -> [Type]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe [Type]
fields0_ [Maybe Type]
fields1_)))
else
Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing
where
cont :: Type -> Writer [(Type, Type)] (Maybe Type)
cont = if TyCon
tc_ TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCon]
knownTyCons then Type -> Writer [(Type, Type)] (Maybe Type)
go else Type -> Writer [(Type, Type)] (Maybe Type)
normaliseNatEverywhere
go Type
_ = Maybe Type -> Writer [(Type, Type)] (Maybe Type)
forall a. a -> WriterT [(Type, Type)] Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Type
forall a. Maybe a
Nothing
normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type
normaliseSimplifyNat :: Type -> Writer [(Type, Type)] Type
normaliseSimplifyNat Type
ty
| (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty Type -> Type -> Bool
`eqType` Type
typeNatKind = do
SOP TyVar CType
ty' <- Type -> Writer [(Type, Type)] (SOP TyVar CType)
normaliseNat Type
ty
Type -> Writer [(Type, Type)] Type
forall a. a -> WriterT [(Type, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Writer [(Type, Type)] Type)
-> Type -> Writer [(Type, Type)] Type
forall a b. (a -> b) -> a -> b
$ SOP TyVar CType -> Type
reifySOP (SOP TyVar CType -> Type) -> SOP TyVar CType -> Type
forall a b. (a -> b) -> a -> b
$ SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c
simplifySOP SOP TyVar CType
ty'
| Bool
otherwise = Type -> Writer [(Type, Type)] Type
forall a. a -> WriterT [(Type, Type)] Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
ty
reifySOP :: CoreSOP -> Type
reifySOP :: SOP TyVar CType -> Type
reifySOP = [Either (Product TyVar CType) (Product TyVar CType)] -> Type
combineP ([Either (Product TyVar CType) (Product TyVar CType)] -> Type)
-> (SOP TyVar CType
-> [Either (Product TyVar CType) (Product TyVar CType)])
-> SOP TyVar CType
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product TyVar CType
-> Either (Product TyVar CType) (Product TyVar CType))
-> [Product TyVar CType]
-> [Either (Product TyVar CType) (Product TyVar CType)]
forall a b. (a -> b) -> [a] -> [b]
map Product TyVar CType
-> Either (Product TyVar CType) (Product TyVar CType)
negateP ([Product TyVar CType]
-> [Either (Product TyVar CType) (Product TyVar CType)])
-> (SOP TyVar CType -> [Product TyVar CType])
-> SOP TyVar CType
-> [Either (Product TyVar CType) (Product TyVar CType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP TyVar CType -> [Product TyVar CType]
forall v c. SOP v c -> [Product v c]
unS
where
negateP :: CoreProduct -> Either CoreProduct CoreProduct
negateP :: Product TyVar CType
-> Either (Product TyVar CType) (Product TyVar CType)
negateP (P ((I Integer
i):ps :: [Symbol TyVar CType]
ps@(Symbol TyVar CType
_:[Symbol TyVar CType]
_))) | Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (-Integer
1) = Product TyVar CType
-> Either (Product TyVar CType) (Product TyVar CType)
forall a b. a -> Either a b
Left ([Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps)
negateP (P ((I Integer
i):[Symbol TyVar CType]
ps)) | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0 = Product TyVar CType
-> Either (Product TyVar CType) (Product TyVar CType)
forall a b. a -> Either a b
Left ([Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P ((Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
abs Integer
i))Symbol TyVar CType -> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. a -> [a] -> [a]
:[Symbol TyVar CType]
ps))
negateP Product TyVar CType
ps = Product TyVar CType
-> Either (Product TyVar CType) (Product TyVar CType)
forall a b. b -> Either a b
Right Product TyVar CType
ps
combineP :: [Either CoreProduct CoreProduct] -> Type
combineP :: [Either (Product TyVar CType) (Product TyVar CType)] -> Type
combineP [] = Integer -> Type
mkNumLitTy Integer
0
combineP [Either (Product TyVar CType) (Product TyVar CType)
p] = (Product TyVar CType -> Type)
-> (Product TyVar CType -> Type)
-> Either (Product TyVar CType) (Product TyVar CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Product TyVar CType
p' -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon
[Integer -> Type
mkNumLitTy Integer
0, Product TyVar CType -> Type
reifyProduct Product TyVar CType
p'])
Product TyVar CType -> Type
reifyProduct Either (Product TyVar CType) (Product TyVar CType)
p
combineP [Either (Product TyVar CType) (Product TyVar CType)
p1,Either (Product TyVar CType) (Product TyVar CType)
p2] = (Product TyVar CType -> Type)
-> (Product TyVar CType -> Type)
-> Either (Product TyVar CType) (Product TyVar CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
(\Product TyVar CType
x -> (Product TyVar CType -> Type)
-> (Product TyVar CType -> Type)
-> Either (Product TyVar CType) (Product TyVar CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
(\Product TyVar CType
y -> let r :: Type
r = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Product TyVar CType -> Type
reifyProduct Product TyVar CType
x
,Product TyVar CType -> Type
reifyProduct Product TyVar CType
y]
in TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Integer -> Type
mkNumLitTy Integer
0, Type
r])
(\Product TyVar CType
y -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Product TyVar CType -> Type
reifyProduct Product TyVar CType
y, Product TyVar CType -> Type
reifyProduct Product TyVar CType
x])
Either (Product TyVar CType) (Product TyVar CType)
p2)
(\Product TyVar CType
x -> (Product TyVar CType -> Type)
-> (Product TyVar CType -> Type)
-> Either (Product TyVar CType) (Product TyVar CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
(\Product TyVar CType
y -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon [Product TyVar CType -> Type
reifyProduct Product TyVar CType
x, Product TyVar CType -> Type
reifyProduct Product TyVar CType
y])
(\Product TyVar CType
y -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon [Product TyVar CType -> Type
reifyProduct Product TyVar CType
x, Product TyVar CType -> Type
reifyProduct Product TyVar CType
y])
Either (Product TyVar CType) (Product TyVar CType)
p2)
Either (Product TyVar CType) (Product TyVar CType)
p1
combineP (Either (Product TyVar CType) (Product TyVar CType)
p:[Either (Product TyVar CType) (Product TyVar CType)]
ps) = let es :: Type
es = [Either (Product TyVar CType) (Product TyVar CType)] -> Type
combineP [Either (Product TyVar CType) (Product TyVar CType)]
ps
in (Product TyVar CType -> Type)
-> (Product TyVar CType -> Type)
-> Either (Product TyVar CType) (Product TyVar CType)
-> Type
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\Product TyVar CType
x -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatSubTyCon
[Type
es, Product TyVar CType -> Type
reifyProduct Product TyVar CType
x])
(\Product TyVar CType
x -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatAddTyCon
[Product TyVar CType -> Type
reifyProduct Product TyVar CType
x, Type
es])
Either (Product TyVar CType) (Product TyVar CType)
p
reifyProduct :: CoreProduct -> Type
reifyProduct :: Product TyVar CType -> Type
reifyProduct (P [Symbol TyVar CType]
ps) =
let ps' :: [Type]
ps' = (Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> Type)
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> Type
reifySymbol ((Symbol TyVar CType
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])])
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Symbol TyVar CType]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol TyVar CType
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
mergeExp [] [Symbol TyVar CType]
ps)
in (Type -> Type -> Type) -> [Type] -> Type
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\Type
t1 Type
t2 -> TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatMulTyCon [Type
t1,Type
t2]) [Type]
ps'
where
mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])]
-> [Either CoreSymbol (CoreSOP,[CoreProduct])]
mergeExp :: Symbol TyVar CType
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
mergeExp (E SOP TyVar CType
s Product TyVar CType
p) [] = [(SOP TyVar CType, [Product TyVar CType])
-> Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
forall a b. b -> Either a b
Right (SOP TyVar CType
s,[Product TyVar CType
p])]
mergeExp (E SOP TyVar CType
s1 Product TyVar CType
p1) (Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
y:[Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
ys)
| Right (SOP TyVar CType
s2,[Product TyVar CType]
p2) <- Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
y
, SOP TyVar CType
s1 SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
s2
= (SOP TyVar CType, [Product TyVar CType])
-> Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
forall a b. b -> Either a b
Right (SOP TyVar CType
s1,(Product TyVar CType
p1Product TyVar CType
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. a -> [a] -> [a]
:[Product TyVar CType]
p2)) Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
forall a. a -> [a] -> [a]
: [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
ys
| Bool
otherwise
= (SOP TyVar CType, [Product TyVar CType])
-> Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
forall a b. b -> Either a b
Right (SOP TyVar CType
s1,[Product TyVar CType
p1]) Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
forall a. a -> [a] -> [a]
: Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
y Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
forall a. a -> [a] -> [a]
: [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
ys
mergeExp Symbol TyVar CType
x [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
ys = Symbol TyVar CType
-> Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
forall a b. a -> Either a b
Left Symbol TyVar CType
x Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
-> [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
forall a. a -> [a] -> [a]
: [Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])]
ys
reifySymbol :: Either CoreSymbol (CoreSOP,[CoreProduct]) -> Type
reifySymbol :: Either
(Symbol TyVar CType) (SOP TyVar CType, [Product TyVar CType])
-> Type
reifySymbol (Left (I Integer
i) ) = Integer -> Type
mkNumLitTy Integer
i
reifySymbol (Left (C CType
c) ) = CType -> Type
unCType CType
c
reifySymbol (Left (V TyVar
v) ) = TyVar -> Type
mkTyVarTy TyVar
v
reifySymbol (Left (E SOP TyVar CType
s Product TyVar CType
p)) = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon [SOP TyVar CType -> Type
reifySOP SOP TyVar CType
s,Product TyVar CType -> Type
reifyProduct Product TyVar CType
p]
reifySymbol (Right (SOP TyVar CType
s1,[Product TyVar CType]
s2)) = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatExpTyCon
[SOP TyVar CType -> Type
reifySOP SOP TyVar CType
s1
,SOP TyVar CType -> Type
reifySOP ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
s2)
]
subtractIneq
:: (CoreSOP, CoreSOP, Bool)
-> CoreSOP
subtractIneq :: Ineq -> SOP TyVar CType
subtractIneq (SOP TyVar CType
x,SOP TyVar CType
y,Bool
isLE)
| Bool
isLE
= SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd SOP TyVar CType
y (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]]) SOP TyVar CType
x)
| Bool
otherwise
= SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd SOP TyVar CType
x (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]]) (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd SOP TyVar CType
y ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
1]])))
sopToIneq
:: CoreSOP
-> Maybe Ineq
sopToIneq :: SOP TyVar CType -> Maybe Ineq
sopToIneq (S [P ((I Integer
i):[Symbol TyVar CType]
l),Product TyVar CType
r])
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
= Ineq -> Maybe Ineq
forall a. a -> Maybe a
Just (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
l]),[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
r],Bool
True)
sopToIneq (S [Product TyVar CType
r,P ((I Integer
i:[Symbol TyVar CType]
l))])
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
= Ineq -> Maybe Ineq
forall a. a -> Maybe a
Just (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
l]),[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
r],Bool
True)
sopToIneq SOP TyVar CType
_ = Maybe Ineq
forall a. Maybe a
Nothing
ineqToSubst
:: Ineq
-> Maybe CoreUnify
ineqToSubst :: Ineq -> Maybe CoreUnify
ineqToSubst (SOP TyVar CType
x,S [P [V TyVar
v]],Bool
True)
= CoreUnify -> Maybe CoreUnify
forall a. a -> Maybe a
Just (TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
v SOP TyVar CType
x)
ineqToSubst Ineq
_
= Maybe CoreUnify
forall a. Maybe a
Nothing
subtractionToPred
:: TyCon
-> (Type,Type)
-> (PredType, Kind)
subtractionToPred :: TyCon -> (Type, Type) -> (Type, Type)
subtractionToPred TyCon
ordCond (Type
x,Type
y) =
#if MIN_VERSION_ghc(9,2,0)
let cmpNat :: Type
cmpNat = TyCon -> [Type] -> Type
mkTyConApp TyCon
typeNatCmpTyCon [Type
y,Type
x]
trueTc :: Type
trueTc = TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedTrueDataCon []
falseTc :: Type
falseTc = TyCon -> [Type] -> Type
mkTyConApp TyCon
promotedFalseDataCon []
ordCmp :: Type
ordCmp = TyCon -> [Type] -> Type
mkTyConApp TyCon
ordCond
[Type
boolTy,Type
cmpNat,Type
trueTc,Type
trueTc,Type
falseTc]
predTy :: Type
predTy = Type -> Type -> Type
mkPrimEqPred Type
ordCmp Type
trueTc
in (Type
predTy,Type
boolTy)
#else
(mkPrimEqPred (mkTyConApp ordCond [y,x])
(mkTyConApp promotedTrueDataCon [])
,boolTy)
#endif
type CoreUnify = UnifyItem TyVar CType
data UnifyItem v c = SubstItem { forall v c. UnifyItem v c -> v
siVar :: v
, forall v c. UnifyItem v c -> SOP v c
siSOP :: SOP v c
}
| UnifyItem { forall v c. UnifyItem v c -> SOP v c
siLHS :: SOP v c
, forall v c. UnifyItem v c -> SOP v c
siRHS :: SOP v c
}
deriving UnifyItem v c -> UnifyItem v c -> Bool
(UnifyItem v c -> UnifyItem v c -> Bool)
-> (UnifyItem v c -> UnifyItem v c -> Bool) -> Eq (UnifyItem v c)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v c. (Eq v, Eq c) => UnifyItem v c -> UnifyItem v c -> Bool
$c== :: forall v c. (Eq v, Eq c) => UnifyItem v c -> UnifyItem v c -> Bool
== :: UnifyItem v c -> UnifyItem v c -> Bool
$c/= :: forall v c. (Eq v, Eq c) => UnifyItem v c -> UnifyItem v c -> Bool
/= :: UnifyItem v c -> UnifyItem v c -> Bool
Eq
instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) where
ppr :: UnifyItem v c -> SDoc
ppr (SubstItem {v
SOP v c
siVar :: forall v c. UnifyItem v c -> v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: v
siSOP :: SOP v c
..}) = v -> SDoc
forall a. Outputable a => a -> SDoc
ppr v
siVar 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
<+> SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siSOP
ppr (UnifyItem {SOP v c
siLHS :: forall v c. UnifyItem v c -> SOP v c
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: SOP v c
siRHS :: SOP v c
..}) = SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siLHS 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
<+> SOP v c -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP v c
siRHS
substsSOP :: (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP :: forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [] SOP v c
u = SOP v c
u
substsSOP ((SubstItem {v
SOP v c
siVar :: forall v c. UnifyItem v c -> v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: v
siSOP :: SOP v c
..}):[UnifyItem v c]
s) SOP v c
u = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s (v -> SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP v
siVar SOP v c
siSOP SOP v c
u)
substsSOP ((UnifyItem {}):[UnifyItem v c]
s) SOP v c
u = [UnifyItem v c] -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => [UnifyItem v c] -> SOP v c -> SOP v c
substsSOP [UnifyItem v c]
s SOP v c
u
substSOP :: (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP :: forall v c. (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP v
tv SOP v c
e = (SOP v c -> SOP v c -> SOP v c) -> [SOP v c] -> SOP v c
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd ([SOP v c] -> SOP v c)
-> (SOP v c -> [SOP v c]) -> SOP v c -> SOP v c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product v c -> SOP v c) -> [Product v c] -> [SOP v c]
forall a b. (a -> b) -> [a] -> [b]
map (v -> SOP v c -> Product v c -> SOP v c
forall v c.
(Ord v, Ord c) =>
v -> SOP v c -> Product v c -> SOP v c
substProduct v
tv SOP v c
e) ([Product v c] -> [SOP v c])
-> (SOP v c -> [Product v c]) -> SOP v c -> [SOP v c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP v c -> [Product v c]
forall v c. SOP v c -> [Product v c]
unS
substProduct :: (Ord v, Ord c) => v -> SOP v c -> Product v c -> SOP v c
substProduct :: forall v c.
(Ord v, Ord c) =>
v -> SOP v c -> Product v c -> SOP v c
substProduct v
tv SOP v c
e = (SOP v c -> SOP v c -> SOP v c) -> [SOP v c] -> SOP v c
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul ([SOP v c] -> SOP v c)
-> (Product v c -> [SOP v c]) -> Product v c -> SOP v c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol v c -> SOP v c) -> [Symbol v c] -> [SOP v c]
forall a b. (a -> b) -> [a] -> [b]
map (v -> SOP v c -> Symbol v c -> SOP v c
forall v c. (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c
substSymbol v
tv SOP v c
e) ([Symbol v c] -> [SOP v c])
-> (Product v c -> [Symbol v c]) -> Product v c -> [SOP v c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product v c -> [Symbol v c]
forall v c. Product v c -> [Symbol v c]
unP
substSymbol :: (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c
substSymbol :: forall v c. (Ord v, Ord c) => v -> SOP v c -> Symbol v c -> SOP v c
substSymbol v
_ SOP v c
_ s :: Symbol v c
s@(I Integer
_) = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [Symbol v c
s]]
substSymbol v
_ SOP v c
_ s :: Symbol v c
s@(C c
_) = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [Symbol v c
s]]
substSymbol v
tv SOP v c
e (V v
tv')
| v
tv v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
tv' = SOP v c
e
| Bool
otherwise = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [v -> Symbol v c
forall v c. v -> Symbol v c
V v
tv']]
substSymbol v
tv SOP v c
e (E SOP v c
s Product v c
p) = SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
normaliseExp (v -> SOP v c -> SOP v c -> SOP v c
forall v c. (Ord v, Ord c) => v -> SOP v c -> SOP v c -> SOP v c
substSOP v
tv SOP v c
e SOP v c
s) (v -> SOP v c -> Product v c -> SOP v c
forall v c.
(Ord v, Ord c) =>
v -> SOP v c -> Product v c -> SOP v c
substProduct v
tv SOP v c
e Product v c
p)
substsSubst :: (Ord v, Ord c) => [UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst :: forall v c.
(Ord v, Ord c) =>
[UnifyItem v c] -> [UnifyItem v c] -> [UnifyItem v c]
substsSubst [UnifyItem v c]
s = (UnifyItem v c -> UnifyItem v c)
-> [UnifyItem v c] -> [UnifyItem v c]
forall a b. (a -> b) -> [a] -> [b]
map UnifyItem v c -> UnifyItem v c
subt
where
subt :: UnifyItem v c -> UnifyItem v c
subt si :: UnifyItem v c
si@(SubstItem {v
SOP v c
siVar :: forall v c. UnifyItem v c -> v
siSOP :: forall v c. UnifyItem v c -> SOP v c
siVar :: v
siSOP :: SOP v c
..}) = UnifyItem v c
si {siSOP = substsSOP s siSOP}
subt si :: UnifyItem v c
si@(UnifyItem {SOP v c
siLHS :: forall v c. UnifyItem v c -> SOP v c
siRHS :: forall v c. UnifyItem v c -> SOP v c
siLHS :: SOP v c
siRHS :: SOP v c
..}) = UnifyItem v c
si {siLHS = substsSOP s siLHS, siRHS = substsSOP s siRHS}
{-# INLINEABLE substsSubst #-}
data UnifyResult
= Win
| Lose
| Draw [CoreUnify]
instance Outputable UnifyResult where
ppr :: UnifyResult -> SDoc
ppr UnifyResult
Win = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Win"
ppr (Draw [CoreUnify]
subst) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Draw" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [CoreUnify] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CoreUnify]
subst
ppr UnifyResult
Lose = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Lose"
unifyNats :: Ct -> CoreSOP -> CoreSOP -> TcPluginM UnifyResult
unifyNats :: Ct -> SOP TyVar CType -> SOP TyVar CType -> TcPluginM UnifyResult
unifyNats Ct
ct SOP TyVar CType
u SOP TyVar CType
v = do
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"unifyNats" (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SOP TyVar CType -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP TyVar CType
u SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ SOP TyVar CType -> SDoc
forall a. Outputable a => a -> SDoc
ppr SOP TyVar CType
v)
UnifyResult -> TcPluginM UnifyResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ct -> SOP TyVar CType -> SOP TyVar CType -> UnifyResult
unifyNats' Ct
ct SOP TyVar CType
u SOP TyVar CType
v)
unifyNats' :: Ct -> CoreSOP -> CoreSOP -> UnifyResult
unifyNats' :: Ct -> SOP TyVar CType -> SOP TyVar CType -> UnifyResult
unifyNats' Ct
ct SOP TyVar CType
u SOP TyVar CType
v
= if SOP TyVar CType -> SOP TyVar CType -> Bool
eqFV SOP TyVar CType
u SOP TyVar CType
v
then if SOP TyVar CType -> Bool
containsConstants SOP TyVar CType
u Bool -> Bool -> Bool
|| SOP TyVar CType -> Bool
containsConstants SOP TyVar CType
v
then if SOP TyVar CType
u SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
v
then UnifyResult
Win
else [CoreUnify] -> UnifyResult
Draw ((CoreUnify -> Bool) -> [CoreUnify] -> [CoreUnify]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreUnify -> Bool
diffFromConstraint (Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers Ct
ct SOP TyVar CType
u SOP TyVar CType
v))
else if SOP TyVar CType
u SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
v
then UnifyResult
Win
else UnifyResult
Lose
else [CoreUnify] -> UnifyResult
Draw ((CoreUnify -> Bool) -> [CoreUnify] -> [CoreUnify]
forall a. (a -> Bool) -> [a] -> [a]
filter CoreUnify -> Bool
diffFromConstraint (Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers Ct
ct SOP TyVar CType
u SOP TyVar CType
v))
where
diffFromConstraint :: CoreUnify -> Bool
diffFromConstraint (UnifyItem SOP TyVar CType
x SOP TyVar CType
y) = Bool -> Bool
not (SOP TyVar CType
x SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
u Bool -> Bool -> Bool
&& SOP TyVar CType
y SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
v)
diffFromConstraint CoreUnify
_ = Bool
True
unifiers :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers :: Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers Ct
ct u :: SOP TyVar CType
u@(S [P [V TyVar
x]]) SOP TyVar CType
v
= case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq Type
t1 Type
_
| Type -> CType
CType (SOP TyVar CType -> Type
reifySOP SOP TyVar CType
u) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t1 Bool -> Bool -> Bool
|| CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) -> [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
x SOP TyVar CType
v]
Pred
_ -> []
unifiers Ct
ct SOP TyVar CType
u v :: SOP TyVar CType
v@(S [P [V TyVar
x]])
= case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq Type
_ Type
t2
| Type -> CType
CType (SOP TyVar CType -> Type
reifySOP SOP TyVar CType
v) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t2 Bool -> Bool -> Bool
|| CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) -> [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
x SOP TyVar CType
u]
Pred
_ -> []
unifiers Ct
ct u :: SOP TyVar CType
u@(S [P [C CType
_]]) SOP TyVar CType
v
= case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq Type
t1 Type
t2
| Type -> CType
CType (SOP TyVar CType -> Type
reifySOP SOP TyVar CType
u) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t1 Bool -> Bool -> Bool
|| Type -> CType
CType (SOP TyVar CType -> Type
reifySOP SOP TyVar CType
v) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t2 -> [SOP TyVar CType -> SOP TyVar CType -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem SOP TyVar CType
u SOP TyVar CType
v]
Pred
_ -> []
unifiers Ct
ct SOP TyVar CType
u v :: SOP TyVar CType
v@(S [P [C CType
_]])
= case Type -> Pred
classifyPredType (Type -> Pred) -> Type -> Pred
forall a b. (a -> b) -> a -> b
$ CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> CtEvidence -> Type
forall a b. (a -> b) -> a -> b
$ Ct -> CtEvidence
ctEvidence Ct
ct of
EqPred EqRel
NomEq Type
t1 Type
t2
| Type -> CType
CType (SOP TyVar CType -> Type
reifySOP SOP TyVar CType
u) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t1 Bool -> Bool -> Bool
|| Type -> CType
CType (SOP TyVar CType -> Type
reifySOP SOP TyVar CType
v) CType -> CType -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> CType
CType Type
t2 -> [SOP TyVar CType -> SOP TyVar CType -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem SOP TyVar CType
u SOP TyVar CType
v]
Pred
_ -> []
unifiers Ct
ct SOP TyVar CType
u SOP TyVar CType
v = Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct SOP TyVar CType
u SOP TyVar CType
v
unifiers' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers' :: Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
_ct (S [P [V TyVar
x]]) (S []) = [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
x ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
0]])]
unifiers' Ct
_ct (S []) (S [P [V TyVar
x]]) = [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
x ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
0]])]
unifiers' Ct
_ct (S [P [V TyVar
x]]) SOP TyVar CType
s = [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
x SOP TyVar CType
s]
unifiers' Ct
_ct SOP TyVar CType
s (S [P [V TyVar
x]]) = [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
x SOP TyVar CType
s]
unifiers' Ct
_ct s1 :: SOP TyVar CType
s1@(S [P [C CType
_]]) SOP TyVar CType
s2 = [SOP TyVar CType -> SOP TyVar CType -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem SOP TyVar CType
s1 SOP TyVar CType
s2]
unifiers' Ct
_ct SOP TyVar CType
s1 s2 :: SOP TyVar CType
s2@(S [P [C CType
_]]) = [SOP TyVar CType -> SOP TyVar CType -> CoreUnify
forall v c. SOP v c -> SOP v c -> UnifyItem v c
UnifyItem SOP TyVar CType
s1 SOP TyVar CType
s2]
unifiers' Ct
ct (S [P [E SOP TyVar CType
s1 Product TyVar CType
p1]]) (S [P [E SOP TyVar CType
s2 Product TyVar CType
p2]])
| SOP TyVar CType
s1 SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
s2 = Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p1]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p2])
unifiers' Ct
ct (S [P [E (S [P [Symbol TyVar CType]
s1]) Product TyVar CType
p1]]) (S [P [Symbol TyVar CType]
p2])
| (Symbol TyVar CType -> Bool) -> [Symbol TyVar CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol TyVar CType -> [Symbol TyVar CType] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol TyVar CType]
p2) [Symbol TyVar CType]
s1
= let base :: [Symbol TyVar CType]
base = [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Symbol TyVar CType]
s1 [Symbol TyVar CType]
p2
diff :: [Symbol TyVar CType]
diff = [Symbol TyVar CType]
p2 [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
s1
in Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
diff]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [SOP TyVar CType -> Product TyVar CType -> Symbol TyVar CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
base]) ([Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]),SOP TyVar CType -> Product TyVar CType -> Symbol TyVar CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
base]) Product TyVar CType
p1]])
unifiers' Ct
ct (S [P [Symbol TyVar CType]
p2]) (S [P [E (S [P [Symbol TyVar CType]
s1]) Product TyVar CType
p1]])
| (Symbol TyVar CType -> Bool) -> [Symbol TyVar CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol TyVar CType -> [Symbol TyVar CType] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol TyVar CType]
p2) [Symbol TyVar CType]
s1
= let base :: [Symbol TyVar CType]
base = [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Symbol TyVar CType]
s1 [Symbol TyVar CType]
p2
diff :: [Symbol TyVar CType]
diff = [Symbol TyVar CType]
p2 [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
s1
in Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [SOP TyVar CType -> Product TyVar CType -> Symbol TyVar CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
base]) ([Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (-Integer
1)]),SOP TyVar CType -> Product TyVar CType -> Symbol TyVar CType
forall v c. SOP v c -> Product v c -> Symbol v c
E ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
base]) Product TyVar CType
p1]]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
diff])
unifiers' Ct
ct (S [P [E (S [P [I Integer
i]]) Product TyVar CType
p]]) (S [P [I Integer
j]])
= case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
Just Integer
k -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
k]])
Maybe Integer
Nothing -> []
unifiers' Ct
ct (S [P [I Integer
j]]) (S [P [E (S [P [I Integer
i]]) Product TyVar CType
p]])
= case Integer -> Integer -> Maybe Integer
integerLogBase Integer
i Integer
j of
Just Integer
k -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
k]])
Maybe Integer
Nothing -> []
unifiers' Ct
ct (S [P [E SOP TyVar CType
s1 Product TyVar CType
p1]]) (S [Product TyVar CType
p2]) = case Product TyVar CType
-> Maybe ([SOP TyVar CType], [Product TyVar CType])
collectBases Product TyVar CType
p2 of
Just (SOP TyVar CType
b:[SOP TyVar CType]
bs,[Product TyVar CType]
ps) | (SOP TyVar CType -> Bool) -> [SOP TyVar CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
s1) (SOP TyVar CType
bSOP TyVar CType -> [SOP TyVar CType] -> [SOP TyVar CType]
forall a. a -> [a] -> [a]
:[SOP TyVar CType]
bs) ->
Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p1]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps)
Maybe ([SOP TyVar CType], [Product TyVar CType])
_ -> []
unifiers' Ct
ct (S [Product TyVar CType
p2]) (S [P [E SOP TyVar CType
s1 Product TyVar CType
p1]]) = case Product TyVar CType
-> Maybe ([SOP TyVar CType], [Product TyVar CType])
collectBases Product TyVar CType
p2 of
Just (SOP TyVar CType
b:[SOP TyVar CType]
bs,[Product TyVar CType]
ps) | (SOP TyVar CType -> Bool) -> [SOP TyVar CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
s1) (SOP TyVar CType
bSOP TyVar CType -> [SOP TyVar CType] -> [SOP TyVar CType]
forall a. a -> [a] -> [a]
:[SOP TyVar CType]
bs) ->
Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p1])
Maybe ([SOP TyVar CType], [Product TyVar CType])
_ -> []
unifiers' Ct
ct (S [P ((I Integer
i):[Symbol TyVar CType]
ps)]) (S [P [I Integer
j]]) =
case Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i of
Just Integer
k -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
k]])
Maybe Integer
_ -> []
unifiers' Ct
ct (S [P [I Integer
j]]) (S [P ((I Integer
i):[Symbol TyVar CType]
ps)]) =
case Integer -> Integer -> Maybe Integer
safeDiv Integer
j Integer
i of
Just Integer
k -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
k]])
Maybe Integer
_ -> []
unifiers' Ct
ct (S [P [Symbol TyVar CType]
ps1]) (S [P [Symbol TyVar CType]
ps2])
| [Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
psx = []
| Bool
otherwise = Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps1'']) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps2''])
where
ps1' :: [Symbol TyVar CType]
ps1' = [Symbol TyVar CType]
ps1 [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
psx
ps2' :: [Symbol TyVar CType]
ps2' = [Symbol TyVar CType]
ps2 [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
psx
ps1'' :: [Symbol TyVar CType]
ps1'' | [Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
ps1' = [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
1]
| Bool
otherwise = [Symbol TyVar CType]
ps1'
ps2'' :: [Symbol TyVar CType]
ps2'' | [Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
ps2' = [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
1]
| Bool
otherwise = [Symbol TyVar CType]
ps2'
psx :: [Symbol TyVar CType]
psx = [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Symbol TyVar CType]
ps1 [Symbol TyVar CType]
ps2
unifiers' Ct
ct (S ((P [I Integer
i]):[Product TyVar CType]
ps1)) (S ((P [I Integer
j]):[Product TyVar CType]
ps2))
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
j = Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps1) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S (([Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer
jInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
i)])Product TyVar CType
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. a -> [a] -> [a]
:[Product TyVar CType]
ps2))
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
j = Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S (([Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
j)])Product TyVar CType
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. a -> [a] -> [a]
:[Product TyVar CType]
ps1)) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps2)
unifiers' Ct
ct s1 :: SOP TyVar CType
s1@(S [Product TyVar CType]
ps1) s2 :: SOP TyVar CType
s2@(S [Product TyVar CType]
ps2) = case SOP TyVar CType -> Maybe Ineq
sopToIneq SOP TyVar CType
k1 of
Just (SOP TyVar CType
s1',SOP TyVar CType
s2',Bool
_)
| SOP TyVar CType
s1' SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
/= SOP TyVar CType
s1 Bool -> Bool -> Bool
|| SOP TyVar CType
s2' SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
/= SOP TyVar CType
s1
, Bool
-> ((Bool, Set CType) -> Bool) -> Maybe (Bool, Set CType) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&) ((Bool, Bool) -> Bool)
-> ((Bool, Set CType) -> (Bool, Bool)) -> (Bool, Set CType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set CType -> Bool) -> (Bool, Set CType) -> (Bool, Bool)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Set CType -> Bool
forall a. Set a -> Bool
Set.null) (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural SOP TyVar CType
s1'))
, Bool
-> ((Bool, Set CType) -> Bool) -> Maybe (Bool, Set CType) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True ((Bool -> Bool -> Bool) -> (Bool, Bool) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Bool -> Bool -> Bool
(&&) ((Bool, Bool) -> Bool)
-> ((Bool, Set CType) -> (Bool, Bool)) -> (Bool, Set CType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set CType -> Bool) -> (Bool, Set CType) -> (Bool, Bool)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Set CType -> Bool
forall a. Set a -> Bool
Set.null) (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural SOP TyVar CType
s2'))
-> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct SOP TyVar CType
s1' SOP TyVar CType
s2'
Maybe Ineq
_ | [Product TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product TyVar CType]
psx
, [Product TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product TyVar CType]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Product TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product TyVar CType]
ps2
-> case [CoreUnify] -> [CoreUnify]
forall a. Eq a => [a] -> [a]
nub ([[CoreUnify]] -> [CoreUnify]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Product TyVar CType -> Product TyVar CType -> [CoreUnify])
-> [Product TyVar CType] -> [Product TyVar CType] -> [[CoreUnify]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Product TyVar CType
x Product TyVar CType
y -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
x]) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
y])) [Product TyVar CType]
ps1 [Product TyVar CType]
ps2)) of
[] -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers'' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps1) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps2)
[CoreUnify
k] | [Product TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product TyVar CType]
ps1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Product TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Product TyVar CType]
ps2 -> [CoreUnify
k]
[CoreUnify]
_ -> []
| [Product TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product TyVar CType]
psx
, CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct)
-> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers'' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps1) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps2)
| [Product TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product TyVar CType]
psx
-> []
Maybe Ineq
_ -> Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers' Ct
ct ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps1'') ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps2'')
where
k1 :: SOP TyVar CType
k1 = Ineq -> SOP TyVar CType
subtractIneq (SOP TyVar CType
s1,SOP TyVar CType
s2,Bool
True)
ps1' :: [Product TyVar CType]
ps1' = [Product TyVar CType]
ps1 [Product TyVar CType]
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product TyVar CType]
psx
ps2' :: [Product TyVar CType]
ps2' = [Product TyVar CType]
ps2 [Product TyVar CType]
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product TyVar CType]
psx
ps1'' :: [Product TyVar CType]
ps1'' | [Product TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product TyVar CType]
ps1' = [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
0]]
| Bool
otherwise = [Product TyVar CType]
ps1'
ps2'' :: [Product TyVar CType]
ps2'' | [Product TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product TyVar CType]
ps2' = [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
0]]
| Bool
otherwise = [Product TyVar CType]
ps2'
psx :: [Product TyVar CType]
psx = [Product TyVar CType]
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
intersect [Product TyVar CType]
ps1 [Product TyVar CType]
ps2
unifiers'' :: Ct -> CoreSOP -> CoreSOP -> [CoreUnify]
unifiers'' :: Ct -> SOP TyVar CType -> SOP TyVar CType -> [CoreUnify]
unifiers'' Ct
ct (S [P [I Integer
i],P [V TyVar
v]]) SOP TyVar CType
s2
| CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
v (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd SOP TyVar CType
s2 ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]))]
unifiers'' Ct
ct SOP TyVar CType
s1 (S [P [I Integer
i],P [V TyVar
v]])
| CtEvidence -> Bool
isGiven (Ct -> CtEvidence
ctEvidence Ct
ct) = [TyVar -> SOP TyVar CType -> CoreUnify
forall v c. v -> SOP v c -> UnifyItem v c
SubstItem TyVar
v (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd SOP TyVar CType
s1 ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I (Integer -> Integer
forall a. Num a => a -> a
negate Integer
i)]]))]
unifiers'' Ct
_ SOP TyVar CType
_ SOP TyVar CType
_ = []
collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])
collectBases :: Product TyVar CType
-> Maybe ([SOP TyVar CType], [Product TyVar CType])
collectBases = ([(SOP TyVar CType, Product TyVar CType)]
-> ([SOP TyVar CType], [Product TyVar CType]))
-> Maybe [(SOP TyVar CType, Product TyVar CType)]
-> Maybe ([SOP TyVar CType], [Product TyVar CType])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(SOP TyVar CType, Product TyVar CType)]
-> ([SOP TyVar CType], [Product TyVar CType])
forall a b. [(a, b)] -> ([a], [b])
unzip (Maybe [(SOP TyVar CType, Product TyVar CType)]
-> Maybe ([SOP TyVar CType], [Product TyVar CType]))
-> (Product TyVar CType
-> Maybe [(SOP TyVar CType, Product TyVar CType)])
-> Product TyVar CType
-> Maybe ([SOP TyVar CType], [Product TyVar CType])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol TyVar CType
-> Maybe (SOP TyVar CType, Product TyVar CType))
-> [Symbol TyVar CType]
-> Maybe [(SOP TyVar CType, Product TyVar CType)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Symbol TyVar CType -> Maybe (SOP TyVar CType, Product TyVar CType)
forall {v} {c}. Symbol v c -> Maybe (SOP v c, Product v c)
go ([Symbol TyVar CType]
-> Maybe [(SOP TyVar CType, Product TyVar CType)])
-> (Product TyVar CType -> [Symbol TyVar CType])
-> Product TyVar CType
-> Maybe [(SOP TyVar CType, Product TyVar CType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product TyVar CType -> [Symbol TyVar CType]
forall v c. Product v c -> [Symbol v c]
unP
where
go :: Symbol v c -> Maybe (SOP v c, Product v c)
go (E SOP v c
s1 Product v c
p1) = (SOP v c, Product v c) -> Maybe (SOP v c, Product v c)
forall a. a -> Maybe a
Just (SOP v c
s1,Product v c
p1)
go Symbol v c
_ = Maybe (SOP v c, Product v c)
forall a. Maybe a
Nothing
fvSOP :: CoreSOP -> UniqSet TyVar
fvSOP :: SOP TyVar CType -> UniqSet TyVar
fvSOP = [UniqSet TyVar] -> UniqSet TyVar
forall a. [UniqSet a] -> UniqSet a
unionManyUniqSets ([UniqSet TyVar] -> UniqSet TyVar)
-> (SOP TyVar CType -> [UniqSet TyVar])
-> SOP TyVar CType
-> UniqSet TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Product TyVar CType -> UniqSet TyVar)
-> [Product TyVar CType] -> [UniqSet TyVar]
forall a b. (a -> b) -> [a] -> [b]
map Product TyVar CType -> UniqSet TyVar
fvProduct ([Product TyVar CType] -> [UniqSet TyVar])
-> (SOP TyVar CType -> [Product TyVar CType])
-> SOP TyVar CType
-> [UniqSet TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP TyVar CType -> [Product TyVar CType]
forall v c. SOP v c -> [Product v c]
unS
fvProduct :: CoreProduct -> UniqSet TyVar
fvProduct :: Product TyVar CType -> UniqSet TyVar
fvProduct = [UniqSet TyVar] -> UniqSet TyVar
forall a. [UniqSet a] -> UniqSet a
unionManyUniqSets ([UniqSet TyVar] -> UniqSet TyVar)
-> (Product TyVar CType -> [UniqSet TyVar])
-> Product TyVar CType
-> UniqSet TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol TyVar CType -> UniqSet TyVar)
-> [Symbol TyVar CType] -> [UniqSet TyVar]
forall a b. (a -> b) -> [a] -> [b]
map Symbol TyVar CType -> UniqSet TyVar
fvSymbol ([Symbol TyVar CType] -> [UniqSet TyVar])
-> (Product TyVar CType -> [Symbol TyVar CType])
-> Product TyVar CType
-> [UniqSet TyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product TyVar CType -> [Symbol TyVar CType]
forall v c. Product v c -> [Symbol v c]
unP
fvSymbol :: CoreSymbol -> UniqSet TyVar
fvSymbol :: Symbol TyVar CType -> UniqSet TyVar
fvSymbol (I Integer
_) = UniqSet TyVar
forall a. UniqSet a
emptyUniqSet
fvSymbol (C CType
_) = UniqSet TyVar
forall a. UniqSet a
emptyUniqSet
fvSymbol (V TyVar
v) = TyVar -> UniqSet TyVar
forall a. Uniquable a => a -> UniqSet a
unitUniqSet TyVar
v
fvSymbol (E SOP TyVar CType
s Product TyVar CType
p) = SOP TyVar CType -> UniqSet TyVar
fvSOP SOP TyVar CType
s UniqSet TyVar -> UniqSet TyVar -> UniqSet TyVar
forall a. UniqSet a -> UniqSet a -> UniqSet a
`unionUniqSets` Product TyVar CType -> UniqSet TyVar
fvProduct Product TyVar CType
p
eqFV :: CoreSOP -> CoreSOP -> Bool
eqFV :: SOP TyVar CType -> SOP TyVar CType -> Bool
eqFV = UniqSet TyVar -> UniqSet TyVar -> Bool
forall a. Eq a => a -> a -> Bool
(==) (UniqSet TyVar -> UniqSet TyVar -> Bool)
-> (SOP TyVar CType -> UniqSet TyVar)
-> SOP TyVar CType
-> SOP TyVar CType
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` SOP TyVar CType -> UniqSet TyVar
fvSOP
containsConstants :: CoreSOP -> Bool
containsConstants :: SOP TyVar CType -> Bool
containsConstants =
(Product TyVar CType -> Bool) -> [Product TyVar CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Symbol TyVar CType -> Bool) -> [Symbol TyVar CType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol TyVar CType -> Bool
symbolContainsConstant ([Symbol TyVar CType] -> Bool)
-> (Product TyVar CType -> [Symbol TyVar CType])
-> Product TyVar CType
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Product TyVar CType -> [Symbol TyVar CType]
forall v c. Product v c -> [Symbol v c]
unP) ([Product TyVar CType] -> Bool)
-> (SOP TyVar CType -> [Product TyVar CType])
-> SOP TyVar CType
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SOP TyVar CType -> [Product TyVar CType]
forall v c. SOP v c -> [Product v c]
unS
where
symbolContainsConstant :: Symbol TyVar CType -> Bool
symbolContainsConstant Symbol TyVar CType
c = case Symbol TyVar CType
c of
C {} -> Bool
True
E SOP TyVar CType
s Product TyVar CType
p -> SOP TyVar CType -> Bool
containsConstants SOP TyVar CType
s Bool -> Bool -> Bool
|| SOP TyVar CType -> Bool
containsConstants ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p])
Symbol TyVar CType
_ -> Bool
False
safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv :: Integer -> Integer -> Maybe Integer
safeDiv Integer
i Integer
j
| Integer
j Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
| Bool
otherwise = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
i Integer
j of
(Integer
k,Integer
0) -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
k
(Integer, Integer)
_ -> Maybe Integer
forall a. Maybe a
Nothing
integerLogBase :: Integer -> Integer -> Maybe Integer
integerLogBase :: Integer -> Integer -> Maybe Integer
integerLogBase Integer
x Integer
y | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1 Bool -> Bool -> Bool
&& 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 if Int# -> Bool
isTrue# (Int#
z1 Int# -> Int# -> Int#
==# Int#
z2)
then Maybe Integer
forall a. Maybe a
Nothing
else Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Int# -> Integer
smallInteger Int#
z1)
integerLogBase Integer
_ Integer
_ = Maybe Integer
forall a. Maybe a
Nothing
isNatural :: CoreSOP -> WriterT (Set CType) Maybe Bool
isNatural :: SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural (S []) = Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isNatural (S [P []]) = Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
isNatural (S [P (I Integer
i:[Symbol TyVar CType]
ps)])
| Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps])
| Bool
otherwise = Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
isNatural (S [P (V TyVar
_:[Symbol TyVar CType]
ps)]) = SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps])
isNatural (S [P (E SOP TyVar CType
s Product TyVar CType
p:[Symbol TyVar CType]
ps)]) = do
Bool
sN <- SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural SOP TyVar CType
s
Bool
pN <- SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p])
if Bool
sN Bool -> Bool -> Bool
&& Bool
pN
then SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps])
else Maybe (Bool, Set CType) -> WriterT (Set CType) Maybe Bool
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT Maybe (Bool, Set CType)
forall a. Maybe a
Nothing
isNatural (S [P (C CType
c:[Symbol TyVar CType]
ps)]) = do
Set CType -> WriterT (Set CType) Maybe ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell (CType -> Set CType
forall a. a -> Set a
Set.singleton CType
c)
SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ps])
isNatural (S (Product TyVar CType
p:[Product TyVar CType]
ps)) = do
Bool
pN <- SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p])
Bool
pK <- SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
ps)
case (Bool
pN,Bool
pK) of
(Bool
True,Bool
True) -> Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
(Bool
False,Bool
False) -> Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
(Bool, Bool)
_ -> Maybe (Bool, Set CType) -> WriterT (Set CType) Maybe Bool
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT Maybe (Bool, Set CType)
forall a. Maybe a
Nothing
solveIneq
:: Word
-> Ineq
-> Ineq
-> WriterT (Set CType) Maybe Bool
solveIneq :: Word -> Ineq -> Ineq -> WriterT (Set CType) Maybe Bool
solveIneq Word
0 Ineq
_ Ineq
_ = WriterT (Set CType) Maybe Bool
forall a. WriterT (Set CType) Maybe a
noRewrite
solveIneq Word
k want :: Ineq
want@(SOP TyVar CType
_,SOP TyVar CType
_,Bool
True) have :: Ineq
have@(SOP TyVar CType
_,SOP TyVar CType
_,Bool
True)
| Ineq
want Ineq -> Ineq -> Bool
forall a. Eq a => a -> a -> Bool
== Ineq
have
= Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
| Bool
otherwise
= do
let
new :: [([(Ineq, Ineq)], Set CType)]
new = ((Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)])
-> Maybe ([(Ineq, Ineq)], Set CType))
-> [Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]]
-> [([(Ineq, Ineq)], Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
f -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
-> Maybe ([(Ineq, Ineq)], Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
f Ineq
want Ineq
have)) [Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]]
ineqRules
solved :: [([(Bool, Set CType)], Set CType)]
solved = (([(Ineq, Ineq)], Set CType) -> ([(Bool, Set CType)], Set CType))
-> [([(Ineq, Ineq)], Set CType)]
-> [([(Bool, Set CType)], Set CType)]
forall a b. (a -> b) -> [a] -> [b]
map (([(Ineq, Ineq)] -> [(Bool, Set CType)])
-> ([(Ineq, Ineq)], Set CType) -> ([(Bool, Set CType)], Set CType)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (((Ineq, Ineq) -> Maybe (Bool, Set CType))
-> [(Ineq, Ineq)] -> [(Bool, Set CType)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT (Set CType) Maybe Bool -> Maybe (Bool, Set CType))
-> ((Ineq, Ineq) -> WriterT (Set CType) Maybe Bool)
-> (Ineq, Ineq)
-> Maybe (Bool, Set CType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ineq -> Ineq -> WriterT (Set CType) Maybe Bool)
-> (Ineq, Ineq) -> WriterT (Set CType) Maybe Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Word -> Ineq -> Ineq -> WriterT (Set CType) Maybe Bool
solveIneq (Word
kWord -> Word -> Word
forall a. Num a => a -> a -> a
-Word
1))))) [([(Ineq, Ineq)], Set CType)]
new
solved1 :: [((Bool, Set CType), Set CType)]
solved1 = (([(Bool, Set CType)], Set CType)
-> ((Bool, Set CType), Set CType))
-> [([(Bool, Set CType)], Set CType)]
-> [((Bool, Set CType), Set CType)]
forall a b. (a -> b) -> [a] -> [b]
map (([(Bool, Set CType)] -> (Bool, Set CType))
-> ([(Bool, Set CType)], Set CType)
-> ((Bool, Set CType), Set CType)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint) [([(Bool, Set CType)], Set CType)]
solved
solved2 :: [(Bool, Set CType)]
solved2 = (((Bool, Set CType), Set CType) -> (Bool, Set CType))
-> [((Bool, Set CType), Set CType)] -> [(Bool, Set CType)]
forall a b. (a -> b) -> [a] -> [b]
map (\((Bool
b,Set CType
s1),Set CType
s2) -> (Bool
b,Set CType -> Set CType -> Set CType
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set CType
s1 Set CType
s2)) [((Bool, Set CType), Set CType)]
solved1
solved3 :: (Bool, Set CType)
solved3 = [(Bool, Set CType)] -> (Bool, Set CType)
forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint [(Bool, Set CType)]
solved2
if [([(Bool, Set CType)], Set CType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([(Bool, Set CType)], Set CType)]
solved then
WriterT (Set CType) Maybe Bool
forall a. WriterT (Set CType) Maybe a
noRewrite
else do
Maybe (Bool, Set CType) -> WriterT (Set CType) Maybe Bool
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT ((Bool, Set CType) -> Maybe (Bool, Set CType)
forall a. a -> Maybe a
Just (Bool, Set CType)
solved3)
solveIneq Word
_ Ineq
_ Ineq
_ = Bool -> WriterT (Set CType) Maybe Bool
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
solvedInEqSmallestConstraint :: [(Bool,Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint :: forall a. [(Bool, Set a)] -> (Bool, Set a)
solvedInEqSmallestConstraint = (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
forall {a}. (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
False, Set a
forall a. Set a
Set.empty)
where
go :: (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool, Set a)
bs [] = (Bool, Set a)
bs
go (Bool
b,Set a
s) ((Bool
b1,Set a
s1):[(Bool, Set a)]
solved)
| Bool -> Bool
not Bool
b Bool -> Bool -> Bool
&& Bool
b1
= (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
b1,Set a
s1) [(Bool, Set a)]
solved
| Bool
b Bool -> Bool -> Bool
&& Bool
b1
, Set a -> Int
forall a. Set a -> Int
Set.size Set a
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Set a -> Int
forall a. Set a -> Int
Set.size Set a
s1
= (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
b1,Set a
s1) [(Bool, Set a)]
solved
| Bool
otherwise
= (Bool, Set a) -> [(Bool, Set a)] -> (Bool, Set a)
go (Bool
b,Set a
s) [(Bool, Set a)]
solved
instantSolveIneq
:: Word
-> Ineq
-> WriterT (Set CType) Maybe Bool
instantSolveIneq :: Word -> Ineq -> WriterT (Set CType) Maybe Bool
instantSolveIneq Word
k Ineq
u = Word -> Ineq -> Ineq -> WriterT (Set CType) Maybe Bool
solveIneq Word
k Ineq
u (SOP TyVar CType
forall {v} {c}. SOP v c
one,SOP TyVar CType
forall {v} {c}. SOP v c
one,Bool
True)
where
one :: SOP v c
one = [Product v c] -> SOP v c
forall v c. [Product v c] -> SOP v c
S [[Symbol v c] -> Product v c
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol v c
forall v c. Integer -> Symbol v c
I Integer
1]]
type Ineq = (CoreSOP, CoreSOP, Bool)
type IneqRule = Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq,Ineq)]
noRewrite :: WriterT (Set CType) Maybe a
noRewrite :: forall a. WriterT (Set CType) Maybe a
noRewrite = Maybe (a, Set CType) -> WriterT (Set CType) Maybe a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT Maybe (a, Set CType)
forall a. Maybe a
Nothing
ineqRules
:: [IneqRule]
ineqRules :: [Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]]
ineqRules =
[ Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
leTrans
, Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
plusMonotone
, Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
timesMonotone
, Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
powMonotone
, Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
pow2MonotoneSpecial
, Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
haveSmaller
, Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
haveBigger
]
leTrans :: IneqRule
leTrans :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
leTrans want :: Ineq
want@(SOP TyVar CType
a,SOP TyVar CType
b,Bool
le) (SOP TyVar CType
x,SOP TyVar CType
y,Bool
_)
| S [P [I Integer
a']] <- SOP TyVar CType
a
, S [P [I Integer
x']] <- SOP TyVar CType
x
, Integer
x' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
a'
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType
a,SOP TyVar CType
y,Bool
le))]
| S [P [I Integer
b']] <- SOP TyVar CType
b
, S [P [I Integer
y']] <- SOP TyVar CType
y
, Integer
y' Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
b'
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType
x,SOP TyVar CType
b,Bool
le))]
leTrans Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
plusMonotone :: IneqRule
plusMonotone :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
plusMonotone Ineq
want Ineq
have
| Just Ineq
want' <- SOP TyVar CType -> Maybe Ineq
sopToIneq (Ineq -> SOP TyVar CType
subtractIneq Ineq
want)
, Ineq
want' Ineq -> Ineq -> Bool
forall a. Eq a => a -> a -> Bool
/= Ineq
want
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want',Ineq
have)]
| Just Ineq
have' <- SOP TyVar CType -> Maybe Ineq
sopToIneq (Ineq -> SOP TyVar CType
subtractIneq Ineq
have)
, Ineq
have' Ineq -> Ineq -> Bool
forall a. Eq a => a -> a -> Bool
/= Ineq
have
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,Ineq
have')]
plusMonotone Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
haveSmaller :: IneqRule
haveSmaller :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
haveSmaller Ineq
want Ineq
have
| (S (Product TyVar CType
x:Product TyVar CType
y:[Product TyVar CType]
ys),SOP TyVar CType
us,Bool
True) <- Ineq
have
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S (Product TyVar CType
xProduct TyVar CType
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. a -> [a] -> [a]
:[Product TyVar CType]
ys),SOP TyVar CType
us,Bool
True))
,(Ineq
want,([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S (Product TyVar CType
yProduct TyVar CType
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. a -> [a] -> [a]
:[Product TyVar CType]
ys),SOP TyVar CType
us,Bool
True))
]
| (S [P [I Integer
1]], S [P (I Integer
_:p :: [Symbol TyVar CType]
p@(Symbol TyVar CType
_:[Symbol TyVar CType]
_))],Bool
True) <- Ineq
have
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
1]],[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
p],Bool
True))]
haveSmaller Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
haveBigger :: IneqRule
haveBigger :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
haveBigger Ineq
want Ineq
have
| (SOP TyVar CType
_ ,S [Product TyVar CType]
vs,Bool
True) <- Ineq
want
, (SOP TyVar CType
as,S [Product TyVar CType]
bs,Bool
True) <- Ineq
have
, let vs' :: [Product TyVar CType]
vs' = [Product TyVar CType]
vs [Product TyVar CType]
-> [Product TyVar CType] -> [Product TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Product TyVar CType]
bs
, Bool -> Bool
not ([Product TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Product TyVar CType]
vs')
= do
Bool
b <- SOP TyVar CType -> WriterT (Set CType) Maybe Bool
isNatural ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
vs')
if Bool
b then
[(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType
as,SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPAdd ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
bs) ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType]
vs'),Bool
True))]
else
WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
haveBigger Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
timesMonotone :: IneqRule
timesMonotone :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
timesMonotone want :: Ineq
want@(SOP TyVar CType
a,SOP TyVar CType
b,Bool
le) have :: Ineq
have@(SOP TyVar CType
x,SOP TyVar CType
y,Bool
_)
| S [P a' :: [Symbol TyVar CType]
a'@(Symbol TyVar CType
_:Symbol TyVar CType
_:[Symbol TyVar CType]
_)] <- SOP TyVar CType
a
, S [P [Symbol TyVar CType]
x'] <- SOP TyVar CType
x
, S [P [Symbol TyVar CType]
y'] <- SOP TyVar CType
y
, let ax :: [Symbol TyVar CType]
ax = [Symbol TyVar CType]
a' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
x'
, let ay :: [Symbol TyVar CType]
ay = [Symbol TyVar CType]
a' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
y'
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
ax)
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
ay)
, let az :: SOP TyVar CType
az = if [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
ax Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
ay then [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ax] else [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ay]
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
az SOP TyVar CType
x, SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
az SOP TyVar CType
y,Bool
le))]
| S [P b' :: [Symbol TyVar CType]
b'@(Symbol TyVar CType
_:Symbol TyVar CType
_:[Symbol TyVar CType]
_)] <- SOP TyVar CType
b
, S [P [Symbol TyVar CType]
x'] <- SOP TyVar CType
x
, S [P [Symbol TyVar CType]
y'] <- SOP TyVar CType
y
, let bx :: [Symbol TyVar CType]
bx = [Symbol TyVar CType]
b' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
x'
, let by :: [Symbol TyVar CType]
by = [Symbol TyVar CType]
b' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
y'
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
bx)
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
by)
, let bz :: SOP TyVar CType
bz = if [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
bx Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
by then [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
bx] else [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
by]
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
bz SOP TyVar CType
x, SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
bz SOP TyVar CType
y,Bool
le))]
| S [P x' :: [Symbol TyVar CType]
x'@(Symbol TyVar CType
_:Symbol TyVar CType
_:[Symbol TyVar CType]
_)] <- SOP TyVar CType
x
, S [P [Symbol TyVar CType]
a'] <- SOP TyVar CType
a
, S [P [Symbol TyVar CType]
b'] <- SOP TyVar CType
b
, let xa :: [Symbol TyVar CType]
xa = [Symbol TyVar CType]
x' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
a'
, let xb :: [Symbol TyVar CType]
xb = [Symbol TyVar CType]
x' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
b'
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
xa)
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
xb)
, let xz :: SOP TyVar CType
xz = if [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
xa Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
xb then [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
xa] else [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
xb]
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
xz SOP TyVar CType
a, SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
xz SOP TyVar CType
b,Bool
le),Ineq
have)]
| S [P y' :: [Symbol TyVar CType]
y'@(Symbol TyVar CType
_:Symbol TyVar CType
_:[Symbol TyVar CType]
_)] <- SOP TyVar CType
y
, S [P [Symbol TyVar CType]
a'] <- SOP TyVar CType
a
, S [P [Symbol TyVar CType]
b'] <- SOP TyVar CType
b
, let ya :: [Symbol TyVar CType]
ya = [Symbol TyVar CType]
y' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
a'
, let yb :: [Symbol TyVar CType]
yb = [Symbol TyVar CType]
y' [Symbol TyVar CType]
-> [Symbol TyVar CType] -> [Symbol TyVar CType]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Symbol TyVar CType]
b'
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
ya)
, Bool -> Bool
not ([Symbol TyVar CType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol TyVar CType]
yb)
, let yz :: SOP TyVar CType
yz = if [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
ya Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Symbol TyVar CType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol TyVar CType]
yb then [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
ya] else [Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Symbol TyVar CType]
yb]
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
yz SOP TyVar CType
a, SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
yz SOP TyVar CType
b,Bool
le),Ineq
have)]
timesMonotone Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
powMonotone :: IneqRule
powMonotone :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
powMonotone Ineq
want (SOP TyVar CType
x, S [P [E SOP TyVar CType
yS Product TyVar CType
yP]],Bool
le)
= case SOP TyVar CType
x of
S [P [E SOP TyVar CType
xS Product TyVar CType
xP]]
| SOP TyVar CType
xS SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
yS
-> [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
xP],[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
yP],Bool
le))]
| Product TyVar CType
xP Product TyVar CType -> Product TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== Product TyVar CType
yP
-> [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType
xS,SOP TyVar CType
yS,Bool
le))]
SOP TyVar CType
_ | SOP TyVar CType
x SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
yS
-> [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
1]],[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
yP],Bool
le))]
SOP TyVar CType
_ -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
powMonotone (SOP TyVar CType
a,S [P [E SOP TyVar CType
bS Product TyVar CType
bP]],Bool
le) Ineq
have
= case SOP TyVar CType
a of
S [P [E SOP TyVar CType
aS Product TyVar CType
aP]]
| SOP TyVar CType
aS SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
bS
-> [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
aP],[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
bP],Bool
le),Ineq
have)]
| Product TyVar CType
aP Product TyVar CType -> Product TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== Product TyVar CType
bP
-> [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((SOP TyVar CType
aS,SOP TyVar CType
bS,Bool
le),Ineq
have)]
SOP TyVar CType
_ | SOP TyVar CType
a SOP TyVar CType -> SOP TyVar CType -> Bool
forall a. Eq a => a -> a -> Bool
== SOP TyVar CType
bS
-> [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
1]],[Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
bP],Bool
le),Ineq
have)]
SOP TyVar CType
_ -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
powMonotone Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
pow2MonotoneSpecial :: IneqRule
pow2MonotoneSpecial :: Ineq -> Ineq -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
pow2MonotoneSpecial (SOP TyVar CType
a,SOP TyVar CType
b,Bool
le) Ineq
have
| Just SOP TyVar CType
a' <- Integer -> SOP TyVar CType -> Maybe (SOP TyVar CType)
facSOP Integer
2 SOP TyVar CType
a
, Just SOP TyVar CType
b' <- Integer -> SOP TyVar CType -> Maybe (SOP TyVar CType)
facSOP Integer
2 SOP TyVar CType
b
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [((SOP TyVar CType
a',SOP TyVar CType
b',Bool
le),Ineq
have)]
pow2MonotoneSpecial Ineq
want (SOP TyVar CType
x,SOP TyVar CType
y,Bool
le)
| Just SOP TyVar CType
x' <- Integer -> SOP TyVar CType -> Maybe (SOP TyVar CType)
facSOP Integer
2 SOP TyVar CType
x
, Just SOP TyVar CType
y' <- Integer -> SOP TyVar CType -> Maybe (SOP TyVar CType)
facSOP Integer
2 SOP TyVar CType
y
= [(Ineq, Ineq)] -> WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. a -> WriterT (Set CType) Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Ineq
want,(SOP TyVar CType
x',SOP TyVar CType
y',Bool
le))]
pow2MonotoneSpecial Ineq
_ Ineq
_ = WriterT (Set CType) Maybe [(Ineq, Ineq)]
forall a. WriterT (Set CType) Maybe a
noRewrite
facSOP
:: Integer
-> CoreSOP
-> Maybe CoreSOP
facSOP :: Integer -> SOP TyVar CType -> Maybe (SOP TyVar CType)
facSOP Integer
n (S [P [Symbol TyVar CType]
ps]) = ([SOP TyVar CType] -> SOP TyVar CType)
-> Maybe [SOP TyVar CType] -> Maybe (SOP TyVar CType)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S ([Product TyVar CType] -> SOP TyVar CType)
-> ([SOP TyVar CType] -> [Product TyVar CType])
-> [SOP TyVar CType]
-> SOP TyVar CType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Product TyVar CType]] -> [Product TyVar CType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Product TyVar CType]] -> [Product TyVar CType])
-> ([SOP TyVar CType] -> [[Product TyVar CType]])
-> [SOP TyVar CType]
-> [Product TyVar CType]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SOP TyVar CType -> [Product TyVar CType])
-> [SOP TyVar CType] -> [[Product TyVar CType]]
forall a b. (a -> b) -> [a] -> [b]
map SOP TyVar CType -> [Product TyVar CType]
forall v c. SOP v c -> [Product v c]
unS) ((Symbol TyVar CType -> Maybe (SOP TyVar CType))
-> [Symbol TyVar CType] -> Maybe [SOP TyVar CType]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Integer -> Symbol TyVar CType -> Maybe (SOP TyVar CType)
facSymbol Integer
n) [Symbol TyVar CType]
ps)
facSOP Integer
_ SOP TyVar CType
_ = Maybe (SOP TyVar CType)
forall a. Maybe a
Nothing
facSymbol
:: Integer
-> CoreSymbol
-> Maybe CoreSOP
facSymbol :: Integer -> Symbol TyVar CType -> Maybe (SOP TyVar CType)
facSymbol Integer
n (I Integer
i)
| Just Integer
j <- Integer -> Integer -> Maybe Integer
integerLogBase Integer
n Integer
i
= SOP TyVar CType -> Maybe (SOP TyVar CType)
forall a. a -> Maybe a
Just ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [[Symbol TyVar CType] -> Product TyVar CType
forall v c. [Symbol v c] -> Product v c
P [Integer -> Symbol TyVar CType
forall v c. Integer -> Symbol v c
I Integer
j]])
facSymbol Integer
n (E SOP TyVar CType
s Product TyVar CType
p)
| Just SOP TyVar CType
s' <- Integer -> SOP TyVar CType -> Maybe (SOP TyVar CType)
facSOP Integer
n SOP TyVar CType
s
= SOP TyVar CType -> Maybe (SOP TyVar CType)
forall a. a -> Maybe a
Just (SOP TyVar CType -> SOP TyVar CType -> SOP TyVar CType
forall v c. (Ord v, Ord c) => SOP v c -> SOP v c -> SOP v c
mergeSOPMul SOP TyVar CType
s' ([Product TyVar CType] -> SOP TyVar CType
forall v c. [Product v c] -> SOP v c
S [Product TyVar CType
p]))
facSymbol Integer
_ Symbol TyVar CType
_ = Maybe (SOP TyVar CType)
forall a. Maybe a
Nothing