{-# LANGUAGE CPP #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DerivingVia #-}
{-# OPTIONS_GHC -Wno-x-partial -Wno-incomplete-uni-patterns -Wno-unused-imports #-}
module Stock.Enum 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.Core.Make (mkRuntimeErrorApp, pAT_ERROR_ID)
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.Ord
synthEnum :: Class -> CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthEnum :: Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthEnum Class
cls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons0 = do
Class
ordCls <- Name -> TcPluginM Class
tcLookupClass Name
ordClassName
Id
mapId <- Name -> TcPluginM Id
tcLookupId Name
mapName
Id
eftId <- Name -> TcPluginM Id
tcLookupId Name
enumFromToName
Id
efttId <- Name -> TcPluginM Id
tcLookupId Name
enumFromThenToName
let dcons :: [DataCon]
dcons = ((DataCon, [Coercion]) -> DataCon)
-> [(DataCon, [Coercion])] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map (DataCon, [Coercion]) -> DataCon
forall a b. (a, b) -> a
fst [(DataCon, [Coercion])]
dcons0
tagToEnumId :: Id
tagToEnumId = PrimOp -> Id
primOpId PrimOp
TagToEnumOp
geSel :: Id
geSel = String -> Class -> Id
classMethod String
">=" Class
ordCls
maxTag :: CoreExpr
maxTag = Integer -> CoreExpr
mkUncheckedIntExpr (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral ([DataCon] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DataCon]
dcons Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
toWrapped :: Expr b -> Expr b
toWrapped Expr b
e = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast Expr b
e (Coercion -> Coercion
mkSymCo Coercion
co)
fromInner :: Id -> Expr b
fromInner 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
CtEvidence
enumIntEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
cls [Type
intTy])
CtEvidence
ordIntEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
ordCls [Type
intTy])
let enumIntDict :: CoreExpr
enumIntDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
enumIntEv
ordIntDict :: CoreExpr
ordIntDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ordIntEv
Id
fv <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"v"
Id
fcb <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"cb"
let fromEnumImpl :: CoreExpr
fromEnumImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
fv] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
fromInner Id
fv) Id
fcb Type
intTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [] (Integer -> CoreExpr
mkUncheckedIntExpr (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i))
| (Int
i, DataCon
dc) <- [Int] -> [DataCon] -> [(Int, DataCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [DataCon]
dcons ]
Id
ti <- Type -> String -> TcPluginM Id
freshId Type
intTy String
"i"
Id
tcb <- Type -> String -> TcPluginM Id
freshId Type
intTy String
"ib"
Id
tip <- Type -> String -> TcPluginM Id
freshId Type
intPrimTy String
"i#"
Id
bLo <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"blo"
Id
bHi <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"bhi"
let leSel :: Id
leSel = String -> Class -> Id
classMethod String
"<=" Class
ordCls
okCon :: CoreExpr
okCon = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ti) Id
tcb Type
wrappedTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
intDataCon) [Id
tip]
(CoreExpr -> CoreExpr
forall {b}. Expr b -> Expr b
toWrapped (CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
tagToEnumId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
innerTy, Id -> CoreExpr
forall b. Id -> Expr b
Var Id
tip])) ]
errOut :: CoreExpr
errOut = Id -> Type -> String -> CoreExpr
mkRuntimeErrorApp Id
pAT_ERROR_ID Type
wrappedTy
String
"toEnum: argument out of range (derived via Stock)"
toEnumImpl :: CoreExpr
toEnumImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
ti] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
geSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
ordIntDict, Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ti, Integer -> CoreExpr
mkUncheckedIntExpr Integer
0]) Id
bLo Type
wrappedTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] CoreExpr
errOut
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) []
(CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
leSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
ordIntDict, Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ti, CoreExpr
maxTag]) Id
bHi Type
wrappedTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] CoreExpr
errOut
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) [] CoreExpr
okCon ]) ]
Id
ex <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"x"
let mapToCon :: CoreExpr -> CoreExpr
mapToCon CoreExpr
es = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
mapId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
wrappedTy, CoreExpr
toEnumImpl, CoreExpr
es]
enumFromImpl :: CoreExpr
enumFromImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
ex] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
mapToCon (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
eftId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
enumIntDict, CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps CoreExpr
fromEnumImpl [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ex], CoreExpr
maxTag]
Id
etx <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"x"
Id
ety <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"y"
Id
lbn <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"b"
let fx :: CoreExpr
fx = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps CoreExpr
fromEnumImpl [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
etx]
fy :: CoreExpr
fy = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps CoreExpr
fromEnumImpl [Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ety]
lim :: CoreExpr
lim = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
geSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
ordIntDict, CoreExpr
fy, CoreExpr
fx]) Id
lbn Type
intTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] (Integer -> CoreExpr
mkUncheckedIntExpr Integer
0)
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) [] CoreExpr
maxTag ]
enumFromThenImpl :: CoreExpr
enumFromThenImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
etx, Id
ety] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
mapToCon (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$
CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
efttId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
enumIntDict, CoreExpr
fx, CoreExpr
fy, CoreExpr
lim]
Id
dmSucc <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
0
Id
dmPred <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
1
Id
dmEFT <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
6
Id
dmEFTT <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
7
CoreExpr
dict <- Class -> Type -> (Id -> TcPluginM [CoreExpr]) -> TcPluginM CoreExpr
recClassDict Class
cls Type
wrappedTy \Id
dvar ->
let useDef :: Id -> Expr b
useDef Id
dm = Expr b -> [Expr b] -> Expr b
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Expr b
forall b. Id -> Expr b
Var Id
dm) [Type -> Expr b
forall b. Type -> Expr b
Type Type
wrappedTy, Id -> Expr b
forall b. Id -> Expr b
Var Id
dvar]
in [CoreExpr] -> TcPluginM [CoreExpr]
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmSucc, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmPred
, CoreExpr
toEnumImpl, CoreExpr
fromEnumImpl
, CoreExpr
enumFromImpl, CoreExpr
enumFromThenImpl
, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmEFT, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmEFTT ]
(EvTerm, [Ct]) -> TcPluginM (EvTerm, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> EvTerm
EvExpr CoreExpr
dict, [CtEvidence -> Ct
mkNonCanonical CtEvidence
enumIntEv, CtEvidence -> Ct
mkNonCanonical CtEvidence
ordIntEv])
synthIx :: Class -> CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthIx :: Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthIx Class
cls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons0 = do
Class
ordCls <- Name -> TcPluginM Class
tcLookupClass Name
ordClassName
Class
numCls <- Name -> TcPluginM Class
tcLookupClass Name
numClassName
Class
enumCls <- Name -> TcPluginM Class
tcLookupClass Name
enumClassName
Id
mapId <- Name -> TcPluginM Id
tcLookupId Name
mapName
Id
eftId <- Name -> TcPluginM Id
tcLookupId Name
enumFromToName
let dcons :: [DataCon]
dcons = ((DataCon, [Coercion]) -> DataCon)
-> [(DataCon, [Coercion])] -> [DataCon]
forall a b. (a -> b) -> [a] -> [b]
map (DataCon, [Coercion]) -> DataCon
forall a b. (a, b) -> a
fst [(DataCon, [Coercion])]
dcons0
tagToEnumId :: Id
tagToEnumId = PrimOp -> Id
primOpId PrimOp
TagToEnumOp
leSel :: Id
leSel = String -> Class -> Id
classMethod String
"<=" Class
ordCls
subSel :: Id
subSel = String -> Class -> Id
classMethod String
"-" Class
numCls
pairTy :: Type
pairTy = [Type] -> Type
mkBoxedTupleTy [Type
wrappedTy, Type
wrappedTy]
tupCon :: DataCon
tupCon = Boxity -> Int -> DataCon
tupleDataCon Boxity
Boxed Int
2
toWrapped :: Expr b -> Expr b
toWrapped Expr b
e = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast Expr b
e (Coercion -> Coercion
mkSymCo Coercion
co)
fromInner :: Id -> Expr b
fromInner 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
CtEvidence
enumIntEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
enumCls [Type
intTy])
CtEvidence
ordIntEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
ordCls [Type
intTy])
CtEvidence
numIntEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
numCls [Type
intTy])
let enumIntDict :: CoreExpr
enumIntDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
enumIntEv
ordIntDict :: CoreExpr
ordIntDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
ordIntEv
numIntDict :: CoreExpr
numIntDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
numIntEv
Id
fv <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"v"; Id
fcb <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"cb"
let fromEnumImpl :: CoreExpr
fromEnumImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
fv] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
fromInner Id
fv) Id
fcb Type
intTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [] (Integer -> CoreExpr
mkUncheckedIntExpr (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i))
| (Int
i, DataCon
dc) <- [Int] -> [DataCon] -> [(Int, DataCon)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] [DataCon]
dcons ]
tagOf :: CoreExpr -> CoreExpr
tagOf CoreExpr
e = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps CoreExpr
fromEnumImpl [CoreExpr
e]
Id
ti <- Type -> String -> TcPluginM Id
freshId Type
intTy String
"i"; Id
tcb <- Type -> String -> TcPluginM Id
freshId Type
intTy String
"ib"; Id
tip <- Type -> String -> TcPluginM Id
freshId Type
intPrimTy String
"i#"
let toEnumImpl :: CoreExpr
toEnumImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
ti] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ti) Id
tcb Type
wrappedTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
intDataCon) [Id
tip]
(CoreExpr -> CoreExpr
forall {b}. Expr b -> Expr b
toWrapped (CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
tagToEnumId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
innerTy, Id -> CoreExpr
forall b. Id -> Expr b
Var Id
tip])) ]
Id
rlu <- Type -> String -> TcPluginM Id
freshId Type
pairTy String
"lu"; Id
rcb <- Type -> String -> TcPluginM Id
freshId Type
pairTy String
"cb"
Id
rl <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"l"; Id
ru <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"u"
let rangeImpl :: CoreExpr
rangeImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
rlu] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
rlu) Id
rcb (Type -> Type
mkListTy Type
wrappedTy)
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
tupCon) [Id
rl, Id
ru]
(CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
mapId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
wrappedTy, CoreExpr
toEnumImpl,
CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
eftId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
enumIntDict, CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
rl), CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ru)]]) ]
Id
ulu <- Type -> String -> TcPluginM Id
freshId Type
pairTy String
"lu"; Id
ucb <- Type -> String -> TcPluginM Id
freshId Type
pairTy String
"cb"
Id
ul <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"l"; Id
uu <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"u"; Id
ui <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"i"
let unsafeIndexImpl :: CoreExpr
unsafeIndexImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
ulu, Id
ui] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ulu) Id
ucb Type
intTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
tupCon) [Id
ul, Id
uu]
(CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
subSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
numIntDict, CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ui), CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ul)]) ]
Id
ilu <- Type -> String -> TcPluginM Id
freshId Type
pairTy String
"lu"; Id
icb <- Type -> String -> TcPluginM Id
freshId Type
pairTy String
"cb"
Id
il <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"l"; Id
iu <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"u"; Id
ii <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"i"
Id
ib <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"b"
let le :: CoreExpr -> CoreExpr -> CoreExpr
le CoreExpr
a CoreExpr
b = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
leSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
ordIntDict, CoreExpr
a, CoreExpr
b]
inRangeImpl :: CoreExpr
inRangeImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
ilu, Id
ii] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ilu) Id
icb Type
boolTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
tupCon) [Id
il, Id
iu]
(CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> CoreExpr -> CoreExpr
le (CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
il)) (CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ii))) Id
ib Type
boolTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] (Id -> CoreExpr
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId DataCon
falseDataCon))
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) [] (CoreExpr -> CoreExpr -> CoreExpr
le (CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
ii)) (CoreExpr -> CoreExpr
tagOf (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
iu))) ]) ]
CoreExpr
ordSuper <- EvTerm -> CoreExpr
unwrapEv (EvTerm -> CoreExpr)
-> ((EvTerm, [Ct]) -> EvTerm) -> (EvTerm, [Ct]) -> CoreExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EvTerm, [Ct]) -> EvTerm
forall a b. (a, b) -> a
fst ((EvTerm, [Ct]) -> CoreExpr)
-> TcPluginM (EvTerm, [Ct]) -> TcPluginM CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthOrd Class
ordCls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons0
Id
dmIndex <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
1
Id
dmRSize <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
4
Id
dmURSize <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
5
CoreExpr
dict <- Class -> Type -> (Id -> TcPluginM [CoreExpr]) -> TcPluginM CoreExpr
recClassDict Class
cls Type
wrappedTy \Id
dvar ->
let useDef :: Id -> Expr b
useDef Id
dm = Expr b -> [Expr b] -> Expr b
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Expr b
forall b. Id -> Expr b
Var Id
dm) [Type -> Expr b
forall b. Type -> Expr b
Type Type
wrappedTy, Id -> Expr b
forall b. Id -> Expr b
Var Id
dvar]
in [CoreExpr] -> TcPluginM [CoreExpr]
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ CoreExpr
ordSuper
, CoreExpr
rangeImpl, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmIndex, CoreExpr
unsafeIndexImpl, CoreExpr
inRangeImpl
, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmRSize, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmURSize ]
(EvTerm, [Ct]) -> TcPluginM (EvTerm, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> EvTerm
EvExpr CoreExpr
dict, (CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical [CtEvidence
enumIntEv, CtEvidence
ordIntEv, CtEvidence
numIntEv])
synthIxProduct :: Class -> CtLoc -> Type -> Type -> Coercion -> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthIxProduct :: Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthIxProduct Class
cls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons0 = do
Class
ordCls <- Name -> TcPluginM Class
tcLookupClass Name
ordClassName
Class
numCls <- Name -> TcPluginM Class
tcLookupClass Name
numClassName
Id
mapId <- Name -> TcPluginM Id
tcLookupId Name
mapName
Id
concatMapId <- Module -> OccName -> TcPluginM Name
lookupOrig Module
gHC_INTERNAL_LIST (String -> OccName
mkVarOcc String
"concatMap") TcPluginM Name -> (Name -> TcPluginM Id) -> TcPluginM Id
forall a b. TcPluginM a -> (a -> TcPluginM b) -> TcPluginM b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name -> TcPluginM Id
tcLookupId
let dc :: DataCon
dc = (DataCon, [Coercion]) -> DataCon
forall a b. (a, b) -> a
fst ([(DataCon, [Coercion])] -> (DataCon, [Coercion])
forall a. HasCallStack => [a] -> a
head [(DataCon, [Coercion])]
dcons0)
fts :: [Type]
fts = Type -> DataCon -> [Type]
fieldTysAt Type
innerTy DataCon
dc
rangeSel :: Id
rangeSel = String -> Class -> Id
classMethod String
"range" Class
cls
uIndexSel :: Id
uIndexSel = String -> Class -> Id
classMethod String
"unsafeIndex" Class
cls
inRangeSel :: Id
inRangeSel = String -> Class -> Id
classMethod String
"inRange" Class
cls
uRSizeSel :: Id
uRSizeSel = String -> Class -> Id
classMethod String
"unsafeRangeSize" Class
cls
mulSel :: Id
mulSel = String -> Class -> Id
classMethod String
"*" Class
numCls
addSel :: Id
addSel = String -> Class -> Id
classMethod String
"+" Class
numCls
pairW :: Type
pairW = [Type] -> Type
mkBoxedTupleTy [Type
wrappedTy, Type
wrappedTy]
tup2 :: DataCon
tup2 = Boxity -> Int -> DataCon
tupleDataCon Boxity
Boxed Int
2
listW :: Type
listW = Type -> Type
mkListTy Type
wrappedTy
toWrapped :: Expr b -> Expr b
toWrapped Expr b
e = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast Expr b
e (Coercion -> Coercion
mkSymCo Coercion
co)
fromInner :: Expr b -> Expr b
fromInner Expr b
e = Expr b -> Coercion -> Expr b
forall b. Expr b -> Coercion -> Expr b
Cast Expr b
e Coercion
co
conApp :: [CoreExpr] -> CoreExpr
conApp [CoreExpr]
args = CoreExpr -> CoreExpr
forall {b}. Expr b -> Expr b
toWrapped (Type -> DataCon -> [CoreExpr] -> CoreExpr
conAppAt Type
innerTy DataCon
dc [CoreExpr]
args)
[CtEvidence]
fieldEvs <- (Type -> TcPluginM CtEvidence) -> [Type] -> TcPluginM [CtEvidence]
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 (\Type
ft -> CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
cls [Type
ft])) [Type]
fts
CtEvidence
numIntEv <- CtLoc -> Type -> TcPluginM CtEvidence
newWanted CtLoc
loc (Class -> [Type] -> Type
mkClassPred Class
numCls [Type
intTy])
let dicts :: [CoreExpr]
dicts = (CtEvidence -> CoreExpr) -> [CtEvidence] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr [CtEvidence]
fieldEvs
numIntDict :: CoreExpr
numIntDict = HasDebugCallStack => CtEvidence -> CoreExpr
CtEvidence -> CoreExpr
ctEvExpr CtEvidence
numIntEv
pairOf :: Type -> CoreExpr -> CoreExpr -> CoreExpr
pairOf Type
ft CoreExpr
l CoreExpr
u = DataCon -> [CoreExpr] -> CoreExpr
mkCoreConApps DataCon
tup2 [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, CoreExpr
l, CoreExpr
u]
rangeFE :: Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
rangeFE Type
ft CoreExpr
d CoreExpr
l CoreExpr
u = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
rangeSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, CoreExpr
d, Type -> CoreExpr -> CoreExpr -> CoreExpr
pairOf Type
ft CoreExpr
l CoreExpr
u]
uIdxFE :: Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
uIdxFE Type
ft CoreExpr
d CoreExpr
l CoreExpr
u CoreExpr
i = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
uIndexSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, CoreExpr
d, Type -> CoreExpr -> CoreExpr -> CoreExpr
pairOf Type
ft CoreExpr
l CoreExpr
u, CoreExpr
i]
inRngFE :: Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
inRngFE Type
ft CoreExpr
d CoreExpr
l CoreExpr
u CoreExpr
i = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
inRangeSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, CoreExpr
d, Type -> CoreExpr -> CoreExpr -> CoreExpr
pairOf Type
ft CoreExpr
l CoreExpr
u, CoreExpr
i]
uRSzFE :: Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
uRSzFE Type
ft CoreExpr
d CoreExpr
l CoreExpr
u = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
uRSizeSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, CoreExpr
d, Type -> CoreExpr -> CoreExpr -> CoreExpr
pairOf Type
ft CoreExpr
l CoreExpr
u]
mul :: CoreExpr -> CoreExpr -> CoreExpr
mul CoreExpr
a CoreExpr
b = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
mulSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
numIntDict, CoreExpr
a, CoreExpr
b]
add :: CoreExpr -> CoreExpr -> CoreExpr
add CoreExpr
a CoreExpr
b = CoreExpr -> [CoreExpr] -> CoreExpr
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
addSel) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
intTy, CoreExpr
numIntDict, CoreExpr
a, CoreExpr
b]
let destr :: Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
v [Id]
binders Type
resTy CoreExpr
body = do
Id
cb <- Type -> String -> TcPluginM Id
freshId Type
innerTy String
"cb"
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 -> CoreExpr
forall {b}. Expr b -> Expr b
fromInner (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
v)) Id
cb Type
resTy [AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
dc) [Id]
binders CoreExpr
body])
Id
luR <- Type -> String -> TcPluginM Id
freshId Type
pairW String
"lu"; Id
lcb <- Type -> String -> TcPluginM Id
freshId Type
pairW String
"lcb"
Id
loR <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"lo"; Id
hiR <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"hi"
[Id]
lsR <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"l") [Type]
fts; [Id]
usR <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"u") [Type]
fts
let mkRange :: [(Type, CoreExpr, Id, Id)] -> [Id] -> TcPluginM CoreExpr
mkRange [] [Id]
chosen = CoreExpr -> TcPluginM CoreExpr
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
wrappedTy [[CoreExpr] -> CoreExpr
conApp ((Id -> CoreExpr) -> [Id] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Id -> CoreExpr
forall b. Id -> Expr b
Var [Id]
chosen)])
mkRange [(Type
ft, CoreExpr
d, Id
l, Id
u)] [Id]
chosen = do
Id
x <- Type -> String -> TcPluginM Id
freshId Type
ft String
"x"
CoreExpr -> TcPluginM CoreExpr
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 Id
mapId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
wrappedTy
, Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Id
x ([CoreExpr] -> CoreExpr
conApp ((Id -> CoreExpr) -> [Id] -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Id -> CoreExpr
forall b. Id -> Expr b
Var ([Id]
chosen [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
x]))), Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
rangeFE Type
ft CoreExpr
d (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
l) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
u)])
mkRange ((Type
ft, CoreExpr
d, Id
l, Id
u) : [(Type, CoreExpr, Id, Id)]
r) [Id]
chosen = do
Id
x <- Type -> String -> TcPluginM Id
freshId Type
ft String
"x"
CoreExpr
bd <- [(Type, CoreExpr, Id, Id)] -> [Id] -> TcPluginM CoreExpr
mkRange [(Type, CoreExpr, Id, Id)]
r ([Id]
chosen [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
x])
CoreExpr -> TcPluginM CoreExpr
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 Id
concatMapId) [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
ft, Type -> CoreExpr
forall b. Type -> Expr b
Type Type
wrappedTy, Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Id
x CoreExpr
bd, Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
rangeFE Type
ft CoreExpr
d (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
l) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
u)])
CoreExpr
rangeInner <- [(Type, CoreExpr, Id, Id)] -> [Id] -> TcPluginM CoreExpr
mkRange ([Type] -> [CoreExpr] -> [Id] -> [Id] -> [(Type, CoreExpr, Id, Id)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 [Type]
fts [CoreExpr]
dicts [Id]
lsR [Id]
usR) []
CoreExpr
rangeUs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
hiR [Id]
usR Type
listW CoreExpr
rangeInner
CoreExpr
rangeLs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
loR [Id]
lsR Type
listW CoreExpr
rangeUs
let rangeImpl :: CoreExpr
rangeImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
luR] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
luR) Id
lcb Type
listW
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
tup2) [Id
loR, Id
hiR] CoreExpr
rangeLs ]
Id
luI <- Type -> String -> TcPluginM Id
freshId Type
pairW String
"lu"; Id
icb <- Type -> String -> TcPluginM Id
freshId Type
pairW String
"icb"; Id
iV <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"i"
Id
loI <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"lo"; Id
hiI <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"hi"
[Id]
lsI <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"l") [Type]
fts; [Id]
usI <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"u") [Type]
fts; [Id]
isI <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"i") [Type]
fts
let idxBody :: CoreExpr
idxBody = (CoreExpr -> (Type, CoreExpr, Id, Id, Id) -> CoreExpr)
-> CoreExpr -> [(Type, CoreExpr, Id, Id, Id)] -> CoreExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\CoreExpr
acc (Type
ft, CoreExpr
d, Id
l, Id
u, Id
i) -> CoreExpr -> CoreExpr -> CoreExpr
add (CoreExpr -> CoreExpr -> CoreExpr
mul CoreExpr
acc (Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
uRSzFE Type
ft CoreExpr
d (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
l) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
u)))
(Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
uIdxFE Type
ft CoreExpr
d (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
l) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
u) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
i)))
(Integer -> CoreExpr
mkUncheckedIntExpr Integer
0) ([Type]
-> [CoreExpr]
-> [Id]
-> [Id]
-> [Id]
-> [(Type, CoreExpr, Id, Id, Id)]
zipWith5q [Type]
fts [CoreExpr]
dicts [Id]
lsI [Id]
usI [Id]
isI)
CoreExpr
idxIs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
iV [Id]
isI Type
intTy CoreExpr
idxBody
CoreExpr
idxUs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
hiI [Id]
usI Type
intTy CoreExpr
idxIs
CoreExpr
idxLs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
loI [Id]
lsI Type
intTy CoreExpr
idxUs
let uIndexImpl :: CoreExpr
uIndexImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
luI, Id
iV] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
luI) Id
icb Type
intTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
tup2) [Id
loI, Id
hiI] CoreExpr
idxLs ]
Id
luN <- Type -> String -> TcPluginM Id
freshId Type
pairW String
"lu"; Id
ncb <- Type -> String -> TcPluginM Id
freshId Type
pairW String
"ncb"; Id
nV <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"i"
Id
loN <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"lo"; Id
hiN <- Type -> String -> TcPluginM Id
freshId Type
wrappedTy String
"hi"
[Id]
lsN <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"l") [Type]
fts; [Id]
usN <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"u") [Type]
fts; [Id]
isN <- (Type -> TcPluginM Id) -> [Type] -> TcPluginM [Id]
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 (Type -> String -> TcPluginM Id
`freshId` String
"i") [Type]
fts
let conj :: [(Type, CoreExpr, Id, Id, Id)] -> TcPluginM CoreExpr
conj [] = CoreExpr -> TcPluginM CoreExpr
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> CoreExpr
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId DataCon
trueDataCon))
conj ((Type
ft, CoreExpr
d, Id
l, Id
u, Id
i) : [(Type, CoreExpr, Id, Id, Id)]
more) = do
Id
b <- Type -> String -> TcPluginM Id
freshId Type
boolTy String
"b"
CoreExpr
rest <- [(Type, CoreExpr, Id, Id, Id)] -> TcPluginM CoreExpr
conj [(Type, CoreExpr, Id, Id, Id)]
more
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 (Type -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr -> CoreExpr
inRngFE Type
ft CoreExpr
d (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
l) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
u) (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
i)) Id
b Type
boolTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
falseDataCon) [] (Id -> CoreExpr
forall b. Id -> Expr b
Var (DataCon -> Id
dataConWorkId DataCon
falseDataCon))
, AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
trueDataCon) [] CoreExpr
rest ])
CoreExpr
inRBody <- [(Type, CoreExpr, Id, Id, Id)] -> TcPluginM CoreExpr
conj ([Type]
-> [CoreExpr]
-> [Id]
-> [Id]
-> [Id]
-> [(Type, CoreExpr, Id, Id, Id)]
zipWith5q [Type]
fts [CoreExpr]
dicts [Id]
lsN [Id]
usN [Id]
isN)
CoreExpr
inRIs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
nV [Id]
isN Type
boolTy CoreExpr
inRBody
CoreExpr
inRUs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
hiN [Id]
usN Type
boolTy CoreExpr
inRIs
CoreExpr
inRLs <- Id -> [Id] -> Type -> CoreExpr -> TcPluginM CoreExpr
destr Id
loN [Id]
lsN Type
boolTy CoreExpr
inRUs
let inRangeImpl :: CoreExpr
inRangeImpl = [Id] -> CoreExpr -> CoreExpr
forall b. [b] -> Expr b -> Expr b
mkLams [Id
luN, Id
nV] (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (Id -> CoreExpr
forall b. Id -> Expr b
Var Id
luN) Id
ncb Type
boolTy
[ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt (DataCon -> AltCon
DataAlt DataCon
tup2) [Id
loN, Id
hiN] CoreExpr
inRLs ]
(EvTerm
ordEv, [Ct]
ordWs) <- Class
-> CtLoc
-> Type
-> Type
-> Coercion
-> [(DataCon, [Coercion])]
-> TcPluginM (EvTerm, [Ct])
synthOrd Class
ordCls CtLoc
loc Type
wrappedTy Type
innerTy Coercion
co [(DataCon, [Coercion])]
dcons0
let ordSuper :: CoreExpr
ordSuper = EvTerm -> CoreExpr
unwrapEv EvTerm
ordEv
Id
dmIndex <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
1
Id
dmRSize <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
4
Id
dmURSize <- Class -> Int -> TcPluginM Id
defMethId Class
cls Int
5
CoreExpr
dict <- Class -> Type -> (Id -> TcPluginM [CoreExpr]) -> TcPluginM CoreExpr
recClassDict Class
cls Type
wrappedTy \Id
dvar ->
let useDef :: Id -> Expr b
useDef Id
dm = Expr b -> [Expr b] -> Expr b
forall b. Expr b -> [Expr b] -> Expr b
mkApps (Id -> Expr b
forall b. Id -> Expr b
Var Id
dm) [Type -> Expr b
forall b. Type -> Expr b
Type Type
wrappedTy, Id -> Expr b
forall b. Id -> Expr b
Var Id
dvar]
in [CoreExpr] -> TcPluginM [CoreExpr]
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [ CoreExpr
ordSuper, CoreExpr
rangeImpl, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmIndex, CoreExpr
uIndexImpl, CoreExpr
inRangeImpl
, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmRSize, Id -> CoreExpr
forall b. Id -> Expr b
useDef Id
dmURSize ]
(EvTerm, [Ct]) -> TcPluginM (EvTerm, [Ct])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CoreExpr -> EvTerm
EvExpr CoreExpr
dict, (CtEvidence -> Ct) -> [CtEvidence] -> [Ct]
forall a b. (a -> b) -> [a] -> [b]
map CtEvidence -> Ct
mkNonCanonical ([CtEvidence]
fieldEvs [CtEvidence] -> [CtEvidence] -> [CtEvidence]
forall a. [a] -> [a] -> [a]
++ [CtEvidence
numIntEv]) [Ct] -> [Ct] -> [Ct]
forall a. [a] -> [a] -> [a]
++ [Ct]
ordWs)
zip4 :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 :: forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 (a
a:[a]
as) (b
b:[b]
bs) (c
c:[c]
cs) (d
d:[d]
ds) = (a
a,b
b,c
c,d
d) (a, b, c, d) -> [(a, b, c, d)] -> [(a, b, c, d)]
forall a. a -> [a] -> [a]
: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
forall a b c d. [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]
zip4 [a]
as [b]
bs [c]
cs [d]
ds
zip4 [a]
_ [b]
_ [c]
_ [d]
_ = []
zipWith5q :: [Type] -> [CoreExpr] -> [Id] -> [Id] -> [Id] -> [(Type, CoreExpr, Id, Id, Id)]
zipWith5q :: [Type]
-> [CoreExpr]
-> [Id]
-> [Id]
-> [Id]
-> [(Type, CoreExpr, Id, Id, Id)]
zipWith5q (Type
a:[Type]
as) (CoreExpr
b:[CoreExpr]
bs) (Id
c:[Id]
cs) (Id
d:[Id]
ds) (Id
e:[Id]
es) = (Type
a,CoreExpr
b,Id
c,Id
d,Id
e) (Type, CoreExpr, Id, Id, Id)
-> [(Type, CoreExpr, Id, Id, Id)] -> [(Type, CoreExpr, Id, Id, Id)]
forall a. a -> [a] -> [a]
: [Type]
-> [CoreExpr]
-> [Id]
-> [Id]
-> [Id]
-> [(Type, CoreExpr, Id, Id, Id)]
zipWith5q [Type]
as [CoreExpr]
bs [Id]
cs [Id]
ds [Id]
es
zipWith5q [Type]
_ [CoreExpr]
_ [Id]
_ [Id]
_ [Id]
_ = []