{-# LANGUAGE CPP #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DerivingVia #-}
{-# OPTIONS_GHC -Wno-x-partial -Wno-incomplete-uni-patterns -Wno-unused-imports #-}
module Stock.Ord where
import GHC.Plugins hiding (TcPlugin)
import GHC.Tc.Plugin
import GHC.Tc.Types
import GHC.Tc.Types.Constraint
#if MIN_VERSION_ghc(9,12,0)
import GHC.Tc.Types.CtLoc (CtLoc)
#else
import GHC.Tc.Types.Constraint (CtLoc)
#endif
import GHC.Tc.Types.Evidence
import GHC.Tc.Utils.Monad (addErrTc)
import GHC.Tc.Errors.Types (mkTcRnUnknownMessage)
import GHC.Types.Error (mkPlainError, noHints)
import GHC.Core.Class (Class, className, classMethods, classOpItems, classTyCon)
import GHC.Core.Predicate (classifyPredType, Pred(ClassPred), mkClassPred)
import GHC.Builtin.Types.Prim (intPrimTy)
import GHC.Builtin.PrimOps (PrimOp(TagToEnumOp))
import GHC.Builtin.PrimOps.Ids (primOpId)
import GHC.Builtin.Names ( eqClassName, ordClassName, appendName
, enumClassName, mapName, numClassName
, enumFromToName, enumFromThenToName
, eqStringName
, genClassName, repTyConName, u1TyConName, k1TyConName
, prodTyConName, sumTyConName
, monoidClassName, foldableClassName, functorClassName
, semigroupClassName )
import Stock.Compat ( gHC_INTERNAL_SHOW, gHC_INTERNAL_READ
, gHC_INTERNAL_LIST, gHC_INTERNAL_GENERICS )
import GHC.Core.Reduction (mkReduction)
import GHC.Core.TyCo.Rep (UnivCoProvenance(PluginProv))
import GHC.Rename.Fixity (lookupFixityRn)
import GHC.Types.Fixity (Fixity(..), defaultFixity)
import GHC.Core.TyCo.Compare (eqType)
import GHC.Core.Multiplicity (scaledThing)
import GHC.Core.SimpleOpt (defaultSimpleOpts)
import GHC.Core.Unfold.Make (mkInlineUnfoldingWithArity)
import GHC.Core.InstEnv (classInstances, is_dfun, is_tys)
import GHC.Runtime.Loader (getValueSafely)
import Stock.Derive
import Data.Maybe (catMaybes, fromJust, isJust, fromMaybe)
import qualified Data.Monoid as Mon (Alt(..))
import Stock.Trans (MaybeT(..))
import Control.Monad (forM, zipWithM, unless, guard)
import Data.IORef (IORef, newIORef, readIORef, modifyIORef')
import Stock.Internal
import Stock.Eq
buildCompare :: CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
-> TcPluginM (CoreExpr, [Ct])
buildCompare :: CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (CoreExpr, [Ct])
buildCompare CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons = do
Class
ordCls <- Name -> TcPluginM Class
tcLookupClass Name
ordClassName
let ordTy :: Type
ordTy = TyCon -> Type
mkTyConTy TyCon
orderingTyCon
[DataCon
ltC, DataCon
eqC, DataCon
gtC] = TyCon -> [DataCon]
tyConDataCons TyCon
orderingTyCon
ltE :: Expr b
ltE = Id -> Expr b
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId DataCon
ltC); eqE :: Expr b
eqE = Id -> Expr b
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId DataCon
eqC); gtE :: Expr b
gtE = Id -> Expr b
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId DataCon
gtC)
cmpSel :: Id
cmpSel = String -> Class -> Id
classMethod String
"compare" Class
ordCls
scrut :: Id -> Expr b
scrut Id
v = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast (Id -> Expr b
forall b. Id -> Expr b
Var Id
v) Coercion
co
indexed :: [(Int, (DataCon, [Coercion]))]
indexed = [Int] -> [(DataCon, [Coercion])] -> [(Int, (DataCon, [Coercion]))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [(DataCon, [Coercion])]
dcons
realFts :: DataCon -> [Type]
realFts DataCon
dc = Type -> DataCon -> [Type]
fieldTysAt Type
innerTy DataCon
dc
lexCmp :: [(Coercion, Id, Id)] -> TcPluginM (CoreExpr, [Ct])
lexCmp [] = (CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr
forall {b}. Expr b
eqE, [])
lexCmp ((Coercion
fco, Id
x, Id
y) : [(Coercion, Id, Id)]
more) = do
let ft :: Type
ft = Coercion -> Type
coercionRKind Coercion
fco
CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
ordCls [Type
ft])
(CoreExpr
restE, [Ct]
ws) <- [(Coercion, Id, Id)] -> TcPluginM (CoreExpr, [Ct])
lexCmp [(Coercion, Id, Id)]
more
Id
scr <- Type -> String -> TcPluginM Id
freshId Type
ordTy String
"o"
let cmp :: CoreExpr
cmp = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
cmpSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev, CoreExpr -> Coercion -> CoreExpr
castInto (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x) Coercion
fco, CoreExpr -> Coercion -> CoreExpr
castInto (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
y) Coercion
fco]
e :: CoreExpr
e = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
cmp Id
scr Type
ordTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
ltC) [] CoreExpr
forall {b}. Expr b
ltE
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
eqC) [] CoreExpr
restE
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
gtC) [] CoreExpr
forall {b}. Expr b
gtE ]
(CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr
e, CtEvidence -> Ct
mkNonCanonical CtEvidence
ev Ct -> [Ct] -> [Ct]
forall a. a -> [a] -> [a]
: [Ct]
ws)
Id
aId <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"a"
Id
bId <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"b"
([Alt Id]
outerAlts, [[Ct]]
wss) <- ([(Alt Id, [Ct])] -> ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Alt Id, [Ct])] -> ([Alt Id], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip (TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [(Int, (DataCon, [Coercion]))]
-> ((Int, (DataCon, [Coercion])) -> TcPluginM (Alt Id, [Ct]))
-> TcPluginM [(Alt Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, (DataCon, [Coercion]))]
indexed \(Int
i, (DataCon
dci, [Coercion]
cosI)) -> do
[Id]
xs <- (Int -> Type -> TcPluginM Id) -> [Int] -> [Type] -> TcPluginM [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM Id
freshId Type
ft (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] (DataCon -> [Type]
realFts DataCon
dci)
([Alt Id]
innerAlts, [[Ct]]
iwss) <- ([(Alt Id, [Ct])] -> ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Alt Id, [Ct])] -> ([Alt Id], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip (TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [(Int, (DataCon, [Coercion]))]
-> ((Int, (DataCon, [Coercion])) -> TcPluginM (Alt Id, [Ct]))
-> TcPluginM [(Alt Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, (DataCon, [Coercion]))]
indexed \(Int
j, (DataCon
dcj, [Coercion]
_)) -> do
[Id]
ys <- (Int -> Type -> TcPluginM Id) -> [Int] -> [Type] -> TcPluginM [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM Id
freshId Type
ft (String
"y" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] (DataCon -> [Type]
realFts DataCon
dcj)
(CoreExpr
body, [Ct]
ws) <- if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j
then [(Coercion, Id, Id)] -> TcPluginM (CoreExpr, [Ct])
lexCmp ([Coercion] -> [Id] -> [Id] -> [(Coercion, Id, Id)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Coercion]
cosI [Id]
xs [Id]
ys)
else (CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j then CoreExpr
forall {b}. Expr b
ltE else CoreExpr
forall {b}. Expr b
gtE, [])
(Alt Id, [Ct]) -> TcPluginM (Alt Id, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dcj) [Id]
ys CoreExpr
body, [Ct]
ws)
Id
innerBndr <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"cb"
(Alt Id, [Ct]) -> TcPluginM (Alt Id, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dci) [Id]
xs (CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
scrut Id
bId) Id
innerBndr Type
ordTy [Alt Id]
innerAlts), [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ct]]
iwss)
Id
outerBndr <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"ca"
let cmpImpl :: CoreExpr
cmpImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
aId, Id
bId] (CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
scrut Id
aId) Id
outerBndr Type
ordTy [Alt Id]
outerAlts)
(CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr
cmpImpl, [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ct]]
wss)
buildRel :: Class -> Class -> CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
-> Bool -> Bool -> TcPluginM (CoreExpr, [Ct])
buildRel :: Class
-> Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> Bool
-> Bool
-> TcPluginM (CoreExpr, [Ct])
buildRel Class
ordCls Class
eqCls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons Bool
asc Bool
refl = do
let boolE :: Bool -> Expr b
boolE Bool
b = Id -> Expr b
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId (if Bool
b then DataCon
trueDataCon else DataCon
falseDataCon))
ltName :: String
ltName = if Bool
asc then String
"<" else String
">"
lastName :: String
lastName | Bool
asc Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
refl = String
"<" | Bool
asc = String
"<=" | Bool -> Bool
not Bool
refl = String
">" | Bool
otherwise = String
">="
scrut :: Id -> Expr b
scrut Id
v = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast (Id -> Expr b
forall b. Id -> Expr b
Var Id
v) Coercion
co
realFts :: DataCon -> [Type]
realFts DataCon
dc = Type -> DataCon -> [Type]
fieldTysAt Type
innerTy DataCon
dc
indexed :: [(Int, (DataCon, [Coercion]))]
indexed = [Int] -> [(DataCon, [Coercion])] -> [(Int, (DataCon, [Coercion]))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [(DataCon, [Coercion])]
dcons
fieldRel :: String -> Coercion -> Id -> Id -> TcPluginM (CoreExpr, [Ct])
fieldRel String
nm Coercion
fco Id
x Id
y = do
let ft :: Type
ft = Coercion -> Type
coercionRKind Coercion
fco
CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
ordCls [Type
ft])
(CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var (String -> Class -> Id
classMethod String
nm Class
ordCls))
[Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev, CoreExpr -> Coercion -> CoreExpr
castInto (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x) Coercion
fco, CoreExpr -> Coercion -> CoreExpr
castInto (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
y) Coercion
fco]
, [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev] )
fieldEq :: Coercion -> Id -> Id -> TcPluginM (CoreExpr, [Ct])
fieldEq Coercion
fco Id
x Id
y = do
let ft :: Type
ft = Coercion -> Type
coercionRKind Coercion
fco
CtEvidence
ev <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
eqCls [Type
ft])
(CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var (String -> Class -> Id
classMethod String
"==" Class
eqCls))
[Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ev, CoreExpr -> Coercion -> CoreExpr
castInto (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
x) Coercion
fco, CoreExpr -> Coercion -> CoreExpr
castInto (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
y) Coercion
fco]
, [CtEvidence -> Ct
mkNonCanonical CtEvidence
ev] )
orE :: CoreExpr -> CoreExpr -> TcPluginM CoreExpr
orE CoreExpr
p CoreExpr
q = do Id
s <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"o"
CoreExpr -> TcPluginM CoreExpr
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
p Id
s Type
boolTy [ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] CoreExpr
q
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) [] (Bool -> CoreExpr
forall {b}. Bool -> Expr b
boolE Bool
True) ])
andE2 :: CoreExpr -> CoreExpr -> TcPluginM CoreExpr
andE2 CoreExpr
p CoreExpr
q = do Id
s <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"n"
CoreExpr -> TcPluginM CoreExpr
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
p Id
s Type
boolTy [ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] (Bool -> CoreExpr
forall {b}. Bool -> Expr b
boolE Bool
False)
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) [] CoreExpr
q ])
lexRel :: [(Coercion, Id, Id)] -> TcPluginM (CoreExpr, [Ct])
lexRel [] = (CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> CoreExpr
forall {b}. Bool -> Expr b
boolE Bool
refl, [])
lexRel [(Coercion
fco, Id
x, Id
y)] = String -> Coercion -> Id -> Id -> TcPluginM (CoreExpr, [Ct])
fieldRel String
lastName Coercion
fco Id
x Id
y
lexRel ((Coercion
fco, Id
x, Id
y) : [(Coercion, Id, Id)]
more) = do
(CoreExpr
ltE, [Ct]
w1) <- String -> Coercion -> Id -> Id -> TcPluginM (CoreExpr, [Ct])
fieldRel String
ltName Coercion
fco Id
x Id
y
(CoreExpr
eqE, [Ct]
w2) <- Coercion -> Id -> Id -> TcPluginM (CoreExpr, [Ct])
fieldEq Coercion
fco Id
x Id
y
(CoreExpr
rest, [Ct]
w3) <- [(Coercion, Id, Id)] -> TcPluginM (CoreExpr, [Ct])
lexRel [(Coercion, Id, Id)]
more
CoreExpr
ae <- CoreExpr -> CoreExpr -> TcPluginM CoreExpr
andE2 CoreExpr
eqE CoreExpr
rest
CoreExpr
oe <- CoreExpr -> CoreExpr -> TcPluginM CoreExpr
orE CoreExpr
ltE CoreExpr
ae
(CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr
oe, [Ct]
w1 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
w2 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
w3)
Id
aId <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"a" ; Id
bId <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"b"
([Alt Id]
outerAlts, [[Ct]]
wss) <- ([(Alt Id, [Ct])] -> ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Alt Id, [Ct])] -> ([Alt Id], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip (TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [(Int, (DataCon, [Coercion]))]
-> ((Int, (DataCon, [Coercion])) -> TcPluginM (Alt Id, [Ct]))
-> TcPluginM [(Alt Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, (DataCon, [Coercion]))]
indexed \(Int
i, (DataCon
dci, [Coercion]
cosI)) -> do
[Id]
xs <- (Int -> Type -> TcPluginM Id) -> [Int] -> [Type] -> TcPluginM [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM Id
freshId Type
ft (String
"x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] (DataCon -> [Type]
realFts DataCon
dci)
([Alt Id]
innerAlts, [[Ct]]
iwss) <- ([(Alt Id, [Ct])] -> ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> TcPluginM a -> TcPluginM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Alt Id, [Ct])] -> ([Alt Id], [[Ct]])
forall a b. [(a, b)] -> ([a], [b])
unzip (TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]]))
-> TcPluginM [(Alt Id, [Ct])] -> TcPluginM ([Alt Id], [[Ct]])
forall a b. (a -> b) -> a -> b
$ [(Int, (DataCon, [Coercion]))]
-> ((Int, (DataCon, [Coercion])) -> TcPluginM (Alt Id, [Ct]))
-> TcPluginM [(Alt Id, [Ct])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, (DataCon, [Coercion]))]
indexed \(Int
j, (DataCon
dcj, [Coercion]
_)) -> do
[Id]
ys <- (Int -> Type -> TcPluginM Id) -> [Int] -> [Type] -> TcPluginM [Id]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\Int
n Type
ft -> Type -> String -> TcPluginM Id
freshId Type
ft (String
"y" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)) [Int
0 :: Int ..] (DataCon -> [Type]
realFts DataCon
dcj)
(CoreExpr
body, [Ct]
ws) <- if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j then [(Coercion, Id, Id)] -> TcPluginM (CoreExpr, [Ct])
lexRel ([Coercion] -> [Id] -> [Id] -> [(Coercion, Id, Id)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Coercion]
cosI [Id]
xs [Id]
ys)
else (CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> CoreExpr
forall {b}. Bool -> Expr b
boolE (if Bool
asc then Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j else Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
j), [])
(Alt Id, [Ct]) -> TcPluginM (Alt Id, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dcj) [Id]
ys CoreExpr
body, [Ct]
ws)
Id
cb <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"cb"
(Alt Id, [Ct]) -> TcPluginM (Alt Id, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dci) [Id]
xs (CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
scrut Id
bId) Id
cb Type
boolTy [Alt Id]
innerAlts), [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ct]]
iwss)
Id
cb2 <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"ca"
(CoreExpr, [Ct]) -> TcPluginM (CoreExpr, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
aId, Id
bId] (CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
scrut Id
aId) Id
cb2 Type
boolTy [Alt Id]
outerAlts), [[Ct]] -> [Ct]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Ct]]
wss)
synthOrd :: Class -> CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthOrd :: Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthOrd Class
ordCls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons = do
(CoreExpr
cmpImpl, [Ct]
cmpWs) <- CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (CoreExpr, [Ct])
buildCompare CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons
Class
eqCls <- Name -> TcPluginM Class
tcLookupClass Name
eqClassName
(EvTerm
eqDict0, [Ct]
eqWs) <- Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthEq Class
eqCls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons
let eqDict :: CoreExpr
eqDict = EvTerm -> CoreExpr
unwrapEv EvTerm
eqDict0
let overridden :: Bool
overridden = (Coercion -> Bool) -> [Coercion] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (Coercion -> Bool) -> Coercion -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Bool
isReflCo) (((DataCon, [Coercion]) -> [Coercion])
-> [(DataCon, [Coercion])] -> [Coercion]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (DataCon, [Coercion]) -> [Coercion]
forall a b. (a, b) -> b
snd [(DataCon, [Coercion])]
dcons)
small :: Bool
small = [(DataCon, [Coercion])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(DataCon, [Coercion])]
dcons Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
3 Bool -> Bool -> Bool
|| ((DataCon, [Coercion]) -> Bool) -> [(DataCon, [Coercion])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ([Coercion] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Coercion] -> Bool)
-> ((DataCon, [Coercion]) -> [Coercion])
-> (DataCon, [Coercion])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon, [Coercion]) -> [Coercion]
forall a b. (a, b) -> b
snd) [(DataCon, [Coercion])]
dcons
idxOf :: String -> Int
idxOf String
nm = [Int] -> Int
forall a. HasCallStack => [a] -> a
head [ Int
i | (Int
i, Id
m) <- [Int] -> [Id] -> [(Int, Id)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] (Class -> [Id]
classMethods Class
ordCls)
, OccName -> String
occNameString (Id -> OccName
forall name. HasOccName name => name -> OccName
occName Id
m) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm ]
([(Int, CoreExpr)]
relOverrides, [Ct]
relWs) <-
if Bool -> Bool
not Bool
small then ([(Int, CoreExpr)], [Ct]) -> TcPluginM ([(Int, CoreExpr)], [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])
else do
let mk :: Bool -> Bool -> TcPluginM (CoreExpr, [Ct])
mk Bool
asc Bool
refl = Class
-> Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> Bool
-> Bool
-> TcPluginM (CoreExpr, [Ct])
buildRel Class
ordCls Class
eqCls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons Bool
asc Bool
refl
(CoreExpr
ltI, [Ct]
w1) <- Bool -> Bool -> TcPluginM (CoreExpr, [Ct])
mk Bool
True Bool
False ; (CoreExpr
leI, [Ct]
w2) <- Bool -> Bool -> TcPluginM (CoreExpr, [Ct])
mk Bool
True Bool
True
(CoreExpr
gtI, [Ct]
w3) <- Bool -> Bool -> TcPluginM (CoreExpr, [Ct])
mk Bool
False Bool
False ; (CoreExpr
geI, [Ct]
w4) <- Bool -> Bool -> TcPluginM (CoreExpr, [Ct])
mk Bool
False Bool
True
([(Int, CoreExpr)], [Ct]) -> TcPluginM ([(Int, CoreExpr)], [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( [(String -> Int
idxOf String
"<", CoreExpr
ltI), (String -> Int
idxOf String
"<=", CoreExpr
leI), (String -> Int
idxOf String
">", CoreExpr
gtI), (String -> Int
idxOf String
">=", CoreExpr
geI)]
, [Ct]
w1 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
w2 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
w3 [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
w4 )
if Bool
overridden
then do
CoreExpr
dict <- Class
-> Type -> [CoreExpr] -> [(Int, CoreExpr)] -> TcPluginM CoreExpr
recDictWith Class
ordCls Type
wrappedTy [CoreExpr
eqDict] ([(Int
0, CoreExpr
cmpImpl)] [(Int, CoreExpr)] -> [(Int, CoreExpr)] -> [(Int, CoreExpr)]
forall a. [a] -> [a] -> [a]
++ [(Int, CoreExpr)]
relOverrides)
(EvTerm, [Ct]) -> TcPluginM (EvTerm, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> EvTerm
EvExpr CoreExpr
dict, [Ct]
cmpWs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqWs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
relWs)
else do
let cmpTy :: Type
cmpTy = HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
wrappedTy (HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
wrappedTy (TyCon -> Type
mkTyConTy TyCon
orderingTyCon))
cmpUnf :: Unfolding
cmpUnf = SimpleOpts -> UnfoldingSource -> Int -> CoreExpr -> Unfolding
mkInlineUnfoldingWithArity SimpleOpts
defaultSimpleOpts UnfoldingSource
StableSystemSrc Int
2 CoreExpr
cmpImpl
Id
cmpId0 <- Type -> String -> TcPluginM Id
freshId Type
cmpTy String
"vvCompare"
let cmpId :: Id
cmpId = Id
cmpId0 Id -> Unfolding -> Id
`setIdUnfolding` Unfolding
cmpUnf
CoreExpr
dictInner <- Class
-> Type -> [CoreExpr] -> [(Int, CoreExpr)] -> TcPluginM CoreExpr
recDictWith Class
ordCls Type
wrappedTy [CoreExpr
eqDict] ([(Int
0, Id -> CoreExpr
forall b. Id -> Expr b
Var Id
cmpId)] [(Int, CoreExpr)] -> [(Int, CoreExpr)] -> [(Int, CoreExpr)]
forall a. [a] -> [a] -> [a]
++ [(Int, CoreExpr)]
relOverrides)
let dict :: CoreExpr
dict = Bind Id -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let (Id -> CoreExpr -> Bind Id
forall b. b -> Expr b -> Bind b
NonRec Id
cmpId CoreExpr
cmpImpl) CoreExpr
dictInner
(EvTerm, [Ct]) -> TcPluginM (EvTerm, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> EvTerm
EvExpr CoreExpr
dict, [Ct]
cmpWs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
eqWs [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
relWs)