{-# LANGUAGE CPP #-}
{-# LANGUAGE NamedFieldPuns #-}
module Data.SBV.Plugin.Analyze (analyzeBind) where
import GhcPlugins
import TyCoRep
import Control.Monad.Reader
import System.Exit
import Data.IORef
import Data.Char (isAlpha, isAlphaNum, toLower, isUpper)
import Data.List (intercalate, partition, nub, nubBy, sort, sortBy, isPrefixOf)
import Data.Maybe (listToMaybe, fromMaybe)
import Data.Ord (comparing)
import qualified Data.Map as M
import qualified Data.SBV as S hiding (proveWith, proveWithAny)
import qualified Data.SBV.Dynamic as S
import qualified Data.SBV.Internals as S
import qualified Control.Exception as C
import Data.SBV.Plugin.Common
import Data.SBV.Plugin.Data
analyzeBind :: Config -> CoreBind -> CoreM ()
analyzeBind cfg@Config{sbvAnnotation, cfgEnv} = go
where go (NonRec b e) = condProve (b, e)
go (Rec binds) = mapM_ condProve binds
condProve (b, e)
| not $ null (sbvAnnotation b)
= mapM_ workAnnotated (sbvAnnotation b)
| TyCoRep.TyConApp tc _ <- varType b
, getOccString (tyConName tc) == "Proved"
= liftIO $ prove cfg [] b e
| True
= return ()
where workAnnotated (SBV opts)
| Just s <- hasSkip opts
= liftIO $ putStrLn $ "[SBV] " ++ showSpan (flags cfgEnv) (pickSpan [varSpan b]) ++ " Skipping " ++ show (showSDoc (flags cfgEnv) (ppr b)) ++ ": " ++ s
| Uninterpret `elem` opts
= return ()
| True
= liftIO $ prove cfg opts b e
hasSkip opts = listToMaybe [s | Skip s <- opts]
prove :: Config -> [SBVOption] -> Var -> CoreExpr -> IO ()
prove cfg@Config{isGHCi} opts b e = do
success <- safely $ proveIt cfg opts b e
unless (success || isGHCi || IgnoreFailure `elem` opts) $ do
putStrLn $ "[SBV] Failed. (Use option '" ++ show IgnoreFailure ++ "' to continue.)"
exitFailure
safely :: IO Bool -> IO Bool
safely a = a `C.catch` bad
where bad :: C.SomeException -> IO Bool
bad e = do print e
return False
proveIt :: Config -> [SBVOption] -> Var -> CoreExpr -> IO Bool
proveIt cfg@Config{cfgEnv, sbvAnnotation} opts topBind topExpr = do
solverConfigs <- pickSolvers opts
let verbose = Verbose `elem` opts
qCheck = QuickCheck `elem` opts
runProver prop
| qCheck = Left `fmap` S.svQuickCheck prop
| True = Right `fmap` S.proveWithAny [s{S.verbose = verbose} | s <- solverConfigs] prop
topLoc = varSpan topBind
loc = "[SBV] " ++ showSpan (flags cfgEnv) topLoc
slvrTag = ", using " ++ tag ++ "."
where tag = case map (S.name . S.solver) solverConfigs of
[] -> "no solvers"
[x] -> show x
[x, y] -> show x ++ " and " ++ show y
xs -> intercalate ", " (map show (init xs)) ++ ", and " ++ show (last xs)
putStrLn $ "\n" ++ loc ++ (if qCheck then " QuickChecking " else " Proving ") ++ show (sh topBind) ++ slvrTag
(finalResult, finalUninterps) <- do
finalResult <- runProver (res cfgEnv topLoc)
finalUninterps <- readIORef (rUninterpreted cfgEnv)
return (finalResult, finalUninterps)
case finalResult of
Right (solver, _, sres@(S.ThmResult smtRes)) -> do
let success = case smtRes of
S.Unsatisfiable{} -> True
S.Satisfiable{} -> False
S.Unknown{} -> False
S.ProofError{} -> False
S.SatExtField{} -> False
putStr $ "[" ++ show solver ++ "] "
print sres
let ok t = not . any (eqType t)
eq (a, b) (c, d) = a == c && b `eqType` d
unintVals = filter ((`ok` uninteresting cfgEnv) . snd) $ nubBy eq $ sortBy (comparing fst) [vt | (vt, (False, _, _)) <- finalUninterps]
unless (success || null unintVals) $ do
let plu | length finalUninterps > 1 = "s:"
| True = ":"
shUI (e, t) = (showSDoc (flags cfgEnv) (ppr (getSrcSpan e)), sh e, sh t)
ls = map shUI unintVals
len1 = maximum (0 : [length s | (s, _, _) <- ls])
len2 = maximum (0 : [length s | (_, s, _) <- ls])
pad n s = take n (s ++ repeat ' ')
put (a, b, c) = putStrLn $ " [" ++ pad len1 a ++ "] " ++ pad len2 b ++ " :: " ++ c
putStrLn $ "[SBV] Counter-example might be bogus due to uninterpreted constant" ++ plu
mapM_ put ls
return success
Left success -> return success
where debug = Debug `elem` opts
cantHandle :: String -> [String] -> Eval a
cantHandle w es = do Env{flags, curLoc} <- ask
let marker = "[SBV] " ++ showSpan flags (pickSpan curLoc)
tag s = marker ++ " " ++ s
tab s = replicate (length marker) ' ' ++ " " ++ s
msg = concatMap ("\n" ++) $ tag ("Skipping proof. " ++ w ++ ":") : map tab es
#if MIN_VERSION_base(4,9,0)
errorWithoutStackTrace msg
#else
error msg
#endif
res initEnv topLoc = do
v <- runReaderT (symEval topExpr) initEnv { curLoc = [topLoc]
, mbListSize = listToMaybe [n | ListSize n <- opts]
, bailOut = cantHandle
}
case v of
Base r -> return r
r -> error $ "Impossible happened. Final result reduced to a non-base value: " ++ showSDocUnsafe (ppr r)
tbd :: String -> [String] -> Eval Val
tbd w ws = do Env{bailOut} <- ask
bailOut w ws
sh o = showSDoc (flags cfgEnv) (ppr o)
symEval :: CoreExpr -> Eval Val
symEval e = do let (bs, body) = collectBinders (pushLetLambda e)
curEnv@Env{bailOut} <- ask
bodyType <- getType (pickSpan (curLoc curEnv)) (exprType body)
let (extraArgs, finalType) = walk bodyType []
where walk (KFun d c) sofar = walk c (d:sofar)
walk k sofar = (reverse sofar, k)
case finalType of
KBase S.KBool -> do
argKs <- mapM (\b -> getType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs
let mkVar ((b, k), mbN) = do sv <- local (\env -> env{curLoc = varSpan b : curLoc env})
$ mkSym cfg (Just b) (Just (idType b)) k (mbN `mplus` Just (sh b))
return ((b, k), sv)
bArgs <- mapM mkVar (zip argKs (concat [map Just ns | Names ns <- opts] ++ repeat Nothing))
bRes <- local (\env -> env{envMap = foldr (uncurry M.insert) (envMap env) bArgs}) (go body)
let feed [] sres = return sres
feed (k:ks) (Func _ f) = do sv <- mkSym cfg Nothing Nothing k Nothing
f sv >>= feed ks
feed ks v = error $ "Impossible! Left with extra args to apply on a non-function: " ++ sh (ks, v)
feed extraArgs bRes
_ -> bailOut "Non-boolean property declaration" (concat [ ["Found : " ++ sh (exprType e)]
, ["Returning: " ++ sh (exprType body) | not (null bs)]
, ["Expected : Bool" ++ if null bs then "" else " result"]
])
where
pushLetLambda (Let b (Lam x bd)) = Lam x (pushLetLambda (Let b bd))
pushLetLambda o = o
isUninterpretedBinding :: Var -> Bool
isUninterpretedBinding v = any (Uninterpret `elem`) [opt | SBV opt <- sbvAnnotation v]
go :: CoreExpr -> Eval Val
go (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t : curLoc envMap}) $ go e
go e = tgo (exprType e) e
debugTrace s w
| debug = trace ("--> " ++ s) w
| True = w
tgo :: Type -> CoreExpr -> Eval Val
tgo t e | debugTrace (sh (e, t)) False = undefined
tgo t (Var v) = do Env{envMap, coreMap} <- ask
k <- getType (getSrcSpan v) t
case (v, k) `M.lookup` envMap of
Just b -> return b
Nothing -> case v `M.lookup` coreMap of
Just (l, b) -> if isUninterpretedBinding v
then uninterpret False t v
else local (\env -> env{curLoc = l : curLoc env}) $ go b
Nothing -> debugTrace ("Uninterpreting: " ++ sh (v, k, nub $ sort $ map (fst . fst) (M.toList envMap)))
$ uninterpret False t v
tgo t e@(Lit l) = do Env{machWordSize} <- ask
case l of
MachChar{} -> unint
MachStr{} -> unint
MachNullAddr -> unint
MachLabel{} -> unint
MachInt i -> return $ Base $ S.svInteger (S.KBounded True machWordSize) i
MachInt64 i -> return $ Base $ S.svInteger (S.KBounded True 64 ) i
MachWord i -> return $ Base $ S.svInteger (S.KBounded False machWordSize) i
MachWord64 i -> return $ Base $ S.svInteger (S.KBounded False 64 ) i
MachFloat f -> return $ Base $ S.svFloat (fromRational f)
MachDouble d -> return $ Base $ S.svDouble (fromRational d)
LitInteger i it -> do k <- getType noSrcSpan it
case k of
KBase b -> return $ Base $ S.svInteger b i
_ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k)
where unint = do Env{flags} <- ask
k <- getType noSrcSpan t
nm <- mkValidName (showSDoc flags (ppr e))
case k of
KBase b -> return $ Base $ S.svUninterpreted b nm Nothing []
_ -> error $ "Impossible: The type for literal resulted in non base kind: " ++ sh (e, k)
tgo tFun orig@App{} = do
reduced <- betaReduce orig
Env{specials} <- ask
let getVar (Var v) = Just v
getVar (Tick _ e) = getVar e
getVar _ = Nothing
isEq (App (App ev (Type _)) dict) | Just v <- getVar ev, isReallyADictionary dict, Just f <- isEquality specials v = Just f
isEq _ = Nothing
isTup (Var v) = isTuple specials v
isTup (App f (Type _)) = isTup f
isTup (Tick _ e) = isTup e
isTup _ = Nothing
isLst (Var v) = isList specials v
isLst (App f (Type _)) = isLst f
isLst (Tick _ e) = isLst e
isLst _ = Nothing
isSpecial e = isEq e `mplus` isTup e `mplus` isLst e
case isSpecial reduced of
Just f -> debugTrace ("Special located: " ++ sh (orig, f)) $ return f
Nothing -> case reduced of
App (App (App (App (Var v) (Type t1)) (Type t2)) dict1) dict2 | isReallyADictionary dict1 && isReallyADictionary dict2 -> do
Env{envMap} <- ask
let vSpan = getSrcSpan v
k1 <- getType vSpan t1
k2 <- getType vSpan t2
let kExp = KFun k1 (KFun k1 k2)
case (v, kExp) `M.lookup` envMap of
Just b -> debugTrace ("Located exp(^): " ++ sh (reduced, kExp)) $ return b
_ -> do Env{coreMap} <- ask
case v `M.lookup` coreMap of
Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App (App (App e (Type t1)) (Type t2)) dict1) dict2)
Nothing -> tgo tFun (Var v)
App (App (App (Var v) (Type t1)) (Type t2)) dict | isReallyADictionary dict -> do
Env{envMap} <- ask
let vSpan = getSrcSpan v
k1 <- getType vSpan t1
k2 <- getType vSpan t2
let kSplit = KFun k1 (KTup [k2, k2])
kJoin = KFun k1 (KFun k1 k2)
case ((v, kSplit) `M.lookup` envMap, (v, kJoin) `M.lookup` envMap) of
(Just b, _) -> debugTrace ("Located split: " ++ sh (reduced, kSplit)) $ return b
(_, Just b) -> debugTrace ("Located join: " ++ sh (reduced, kJoin)) $ return b
_ -> do Env{coreMap} <- ask
case v `M.lookup` coreMap of
Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App (App e (Type t1)) (Type t2)) dict)
Nothing -> tgo tFun (Var v)
App (App (Var v) (Type t)) dict | isReallyADictionary dict -> do
Env{envMap} <- ask
k <- getType (getSrcSpan v) t
case (v, k) `M.lookup` envMap of
Just b -> return b
Nothing -> do Env{coreMap} <- ask
case v `M.lookup` coreMap of
Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App (App e (Type t)) dict)
Nothing -> tgo tFun (Var v)
App (Var v) (Type t) -> do
Env{coreMap} <- ask
case v `M.lookup` coreMap of
Just (l, e) -> local (\env -> env{curLoc = l : curLoc env}) $ tgo tFun (App e (Type t))
Nothing -> tgo tFun (Var v)
App (Let (Rec bs) f) a -> go (Let (Rec bs) (App f a))
App f e -> do
func <- go f
arg <- go e
case (func, arg) of
(Func _ sf, sv) -> sf sv
_ -> error $ "[SBV] Impossible happened. Got an application with mismatched types: " ++ sh [(f, func), (e, arg)]
e -> go e
tgo _ (Lam b body) = do
k <- getType (getSrcSpan b) (varType b)
Env{envMap} <- ask
return $ Func (Just (sh b)) $ \s -> local (\env -> env{envMap = M.insert (b, k) s envMap}) (go body)
tgo _ (Let (NonRec b e) body) = local (\env -> env{coreMap = M.insert b (varSpan b, e) (coreMap env)}) (go body)
tgo _ (Let (Rec bs) body) = local (\env -> env{coreMap = foldr (\(b, e) m -> M.insert b (varSpan b, e) m) (coreMap env) bs}) (go body)
tgo _ e@(Case ce cBinder caseType alts)
= do sce <- go ce
let caseTooComplicated w [] = tbd ("Unsupported case-expression (" ++ w ++ ")") [sh e]
caseTooComplicated w xs = tbd ("Unsupported case-expression (" ++ w ++ ")") $ [sh e, "While Analyzing:"] ++ xs
isDefault (DEFAULT, _, _) = True
isDefault _ = False
(defs, nonDefs) = partition isDefault alts
walk [] = caseTooComplicated "with-non-exhaustive-match" []
walk ((p, bs, rhs) : rest) =
do
let eLoc = case (rhs, bs) of
(Tick t _, _ ) -> tickSpan t
(Var v, _ ) -> varSpan v
(_, b:_) -> varSpan b
_ -> varSpan cBinder
mr <- match eLoc sce p bs
case mr of
Just (m, bs') -> do let result = local (\env -> env{curLoc = eLoc : curLoc env, envMap = foldr (uncurry M.insert) (envMap env) bs'}) $ go rhs
if null rest
then result
else choose (caseTooComplicated "with-complicated-alternatives-during-merging") m result (walk rest)
Nothing -> caseTooComplicated "with-complicated-match" ["MATCH " ++ sh (ce, p), " --> " ++ sh rhs]
k <- getType (getSrcSpan cBinder) caseType
local (\env -> env{envMap = M.insert (cBinder, k) sce (envMap env)}) $ walk (nonDefs ++ defs)
where choose bailOut t tb fb = case S.svAsBool t of
Nothing -> do stb <- tb
sfb <- fb
iteVal bailOut t stb sfb
Just True -> tb
Just False -> fb
match :: SrcSpan -> Val -> AltCon -> [Var] -> Eval (Maybe (S.SVal, [((Var, SKind), Val)]))
match sp a c bs = case c of
DEFAULT -> return $ Just (S.svTrue, [])
LitAlt l -> do b <- go (Lit l)
return $ Just (a `eqVal` b, [])
DataAlt dc -> do Env{envMap, destMap} <- ask
k <- getType sp (dataConRepType dc)
let wid = dataConWorkId dc
case (wid, k) `M.lookup` envMap of
Just (Base b) -> return $ Just (a `eqVal` Base b, [])
_ -> case wid `M.lookup` destMap of
Nothing -> return Nothing
Just f -> do bts <- mapM (\b -> getType (getSrcSpan b) (varType b) >>= \bt -> return (b, bt)) bs
return $ Just (f a bts)
tgo t (Cast e c)
= debugTrace ("Going thru a Cast: " ++ sh c) $ tgo t e
tgo _ (Tick t e) = local (\envMap -> envMap{curLoc = tickSpan t : curLoc envMap}) $ go e
tgo _ (Type t)
= do Env{curLoc} <- ask
k <- getType (pickSpan curLoc) t
return (Typ k)
tgo _ e@Coercion{}
= tbd "Unsupported coercion-expression" [sh e]
isBetaReducable (Type _) = True
isBetaReducable e = isReallyADictionary e
betaReduce :: CoreExpr -> Eval CoreExpr
betaReduce orig@(App f a) = do
rf <- betaReduce f
if not (isBetaReducable a)
then return (App rf a)
else do let chaseVars :: CoreExpr -> Eval CoreExpr
chaseVars (Var x) = do Env{coreMap} <- ask
case x `M.lookup` coreMap of
Nothing -> return (Var x)
Just (_, b) -> chaseVars b
chaseVars (Tick _ x) = chaseVars x
chaseVars x = return x
func <- chaseVars rf
case func of
Lam x b -> do reduced <- betaReduce $ substExpr (ppr "SBV.betaReduce") (extendSubstList emptySubst [(x, a)]) b
() <- debugTrace ("Beta reduce:\n" ++ sh (orig, reduced)) $ return ()
return reduced
_ -> return (App rf a)
betaReduce e = return e
isReallyADictionary :: CoreExpr -> Bool
isReallyADictionary (App f _) = isReallyADictionary f
isReallyADictionary (Var v) = "$" `isPrefixOf` unpackFS (occNameFS (occName (varName v)))
isReallyADictionary _ = False
mkSym :: Config -> Maybe Var -> Maybe Type -> SKind -> Maybe String -> Eval Val
mkSym Config{cfgEnv} mbBind mbBType = sym
where sh o = showSDoc (flags cfgEnv) (ppr o)
tinfo k = case mbBType of
Nothing -> "Kind: " ++ sh k
Just t -> "Type: " ++ sh t
sym (KBase k) nm = do v <- lift $ ask >>= liftIO . S.svMkSymVar Nothing k nm
return (Base v)
sym (KTup ks) nm = do let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. length ks]
vs <- zipWithM sym ks ns
return $ Tup vs
sym (KLst ks) nm = do Env{mbListSize, bailOut} <- ask
ls <- case mbListSize of
Just i -> return i
Nothing -> bailOut "List-argument found, with no size info"
[ "Name: " ++ fromMaybe "anonymous" nm
, tinfo (KLst ks)
, "Hint: Use the \"ListSize\" annotation"
]
let ns = map (\i -> (++ ("_" ++ show i)) `fmap` nm) [1 .. ls]
vs <- zipWithM sym (replicate ls ks) ns
return (Lst vs)
sym k@KFun{} nm = case mbBind of
Just v -> uninterpret True (varType v) v
_ -> do Env{bailOut} <- ask
bailOut "Unsupported unnamed higher-order symbolic input"
[ "Name: " ++ fromMaybe "<anonymous>" nm
, tinfo k
, "Hint: Name all higher-order inputs explicitly"
]
uninterpret :: Bool -> Type -> Var -> Eval Val
uninterpret isInput t var = do
Env{rUninterpreted, flags} <- ask
prevUninterpreted <- liftIO $ readIORef rUninterpreted
case [r | ((v, t'), r) <- prevUninterpreted, var == v && t `eqType` t'] of
(_, _, val):_ -> return val
[] -> do let (tvs, t') = splitForAllTys t
(args, res) = splitFunTys t'
sp = getSrcSpan var
argKs <- mapM (getType sp) args
resK <- getType sp res
nm <- mkValidName $ showSDoc flags (ppr var)
body <- walk argKs (nm, resK) []
let fVal = wrap tvs body
liftIO $ modifyIORef rUninterpreted (((var, t), (isInput, nm, fVal)) :)
return fVal
where walk :: [SKind] -> (String, SKind) -> [Val] -> Eval Val
walk [] (nm, k) args = do Env{mbListSize, bailOut} <- ask
let mkArg :: Val -> [S.SVal]
mkArg (Base v) = [v]
mkArg (Tup vs) = concatMap mkArg vs
mkArg (Lst vs) = concatMap mkArg vs
mkArg sk = error $ "Not yet supported uninterpreted function with a higher-order argument: " ++ showSDocUnsafe (ppr sk)
bArgs = concatMap mkArg (reverse args)
mkRes :: String -> SKind -> Eval [S.SVal]
mkRes n (KBase b) = return [S.svUninterpreted b n Nothing bArgs]
mkRes n (KTup bs) = concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ]] bs
mkRes n (KLst b) = do ls <- case mbListSize of
Just i -> return i
Nothing -> bailOut "List-argument found in uninterpreted function, with no size info"
["Hint: Use the \"ListSize\" annotation"]
concat `fmap` zipWithM mkRes [n ++ "_" ++ show i | i <- [(1 :: Int) .. ls]] (repeat b)
mkRes n sk@KFun{} = bailOut "Not yet supported uninterpreted function with a higher-order result"
[ "Name: " ++ n
, "Kind: " ++ showSDocUnsafe (ppr sk)
]
res <- mkRes nm k
case map Base res of
[x] -> return x
xs -> return $ Tup xs
walk (_:ks) nmk args = return $ Func Nothing $ \a -> walk ks nmk (a:args)
wrap [] f = f
wrap (_:ts) f = Func Nothing $ \(Typ _) -> return (wrap ts f)
mkValidName :: String -> Eval String
mkValidName name =
do Env{rUsedNames} <- ask
usedNames <- liftIO $ readIORef rUsedNames
let unm = unSMT $ genSym usedNames name
liftIO $ modifyIORef rUsedNames (unm :)
return $ escape unm
where genSym bad nm
| nm `elem` bad = head [nm' | i <- [(0::Int) ..], let nm' = nm ++ "_" ++ show i, nm' `notElem` bad]
| True = nm
unSMT nm
| map toLower nm `elem` S.smtLibReservedNames
= if not (null nm) && isUpper (head nm)
then "sbv" ++ nm
else "sbv_" ++ nm
| True
= nm
escape nm | isAlpha (head nm) && all isGood (tail nm) = nm
| True = "|" ++ map tr nm ++ "|"
isGood c = isAlphaNum c || c == '_'
tr '|' = '_'
tr '\\' = '_'
tr c = c
getType :: SrcSpan -> Type -> Eval SKind
getType sp typ = do let (tvs, typ') = splitForAllTys typ
(args, res) = splitFunTys typ'
argKs <- mapM (getType sp) args
resK <- getComposite res
return $ wrap tvs $ foldr KFun resK argKs
where wrap ts f = foldr (KFun . mkUserSort) f ts
mkUserSort v = KBase (S.KUserSort (show (occNameFS (occName (varName v)))) (Left "sbvPlugin"))
getComposite :: Type -> Eval SKind
getComposite t = case splitTyConApp_maybe t of
Just (k, ts) | isTupleTyCon k -> KTup `fmap` mapM (getType sp) ts
Just (k, [a]) | listTyCon == k -> KLst `fmap` getType sp a
_ -> KBase `fmap` getBaseType t
getBaseType :: Type -> Eval S.Kind
getBaseType bt = do
Env{tcMap} <- ask
case grabTCs (splitTyConApp_maybe bt) of
Just k -> case k `M.lookup` tcMap of
Just knd -> return knd
Nothing -> unknown
_ -> unknown
where
grabTCs Nothing = Nothing
grabTCs (Just (top, ts)) = do as <- walk ts []
return $ TCKey (top, as)
walk [] sofar = Just $ reverse sofar
walk (a:as) sofar = case splitTyConApp_maybe a of
Just (ac, []) -> walk as (ac:sofar)
_ -> Nothing
unknown = do Env{flags, rUITypes} <- ask
uiTypes <- liftIO $ readIORef rUITypes
case [k | (bt', k) <- uiTypes, bt `eqType` bt'] of
k:_ -> return k
[] -> do nm <- mkValidName $ showSDoc flags (ppr bt)
let k = S.KUserSort nm $ Left $ "originating from sbvPlugin: " ++ showSDoc flags (ppr sp)
liftIO $ modifyIORef rUITypes ((bt, k) :)
return k
{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}