liquidhaskell-boot-0.9.14.1: src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Haskell.Liquid.Transforms.CoreToLogic
( coreToDef
, coreToFun
, coreToLogic
, mkLit, mkI, mkS
, runToLogic
, runToLogicWithBoolBinds
, logicType
, inlineSpecType
, measureSpecType
, weakenResult
, normalizeCoreExpr
) where
import Data.Bifunctor (first)
import Data.ByteString (ByteString)
import Prelude hiding (error)
import Language.Haskell.Liquid.GHC.TypeRep () -- needed for Eq 'Type'
import Liquid.GHC.API hiding (Expr, Located, get, panic)
import qualified Liquid.GHC.API as Ghc
import qualified Liquid.GHC.API as C
import qualified Data.List as L
import Data.Maybe (listToMaybe)
import qualified Data.Text as T
import qualified Data.Char
import qualified Text.Printf as Printf
import Data.Text.Encoding
import Data.Text.Encoding.Error
import Control.Monad.Except
import Control.Monad.Identity
import qualified Language.Haskell.Liquid.Misc as Misc
import Language.Fixpoint.Types hiding (panic, Error, R, simplify, isBool)
import qualified Language.Fixpoint.Types as F
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import Language.Haskell.Liquid.Bare.Types
import Language.Haskell.Liquid.Bare.DataType
import Language.Haskell.Liquid.Bare.Misc (simpleSymbolVar)
import Language.Haskell.Liquid.GHC.Play
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.Names
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.RType
import Language.Haskell.Liquid.Types.RTypeOp
import Language.Haskell.Liquid.Types.Types
import qualified Data.HashMap.Strict as M
import Control.Monad.Reader
import Language.Haskell.Liquid.UX.Config
import Data.Ratio
import GHC.Base ((+#), (-#), (*#))
logicType :: (IsReft r) => Bool -> Type -> RRType r
logicType allowTC τ = fromRTypeRep $ t { ty_binds = bs, ty_info = is, ty_args = as, ty_refts = rs}
where
t = toRTypeRep $ ofType τ
(bs, is, as, rs) = Misc.unzip4 $ dropWhile (isErasable' . Misc.thd4) $ Misc.zip4 (ty_binds t) (ty_info t) (ty_args t) (ty_refts t)
isErasable' = if allowTC then isEmbeddedClass else isClassType
{- | [NOTE:inlineSpecType type]: the refinement depends on whether the result type is a Bool or not:
CASE1: measure f@logic :: X -> Bool <=> f@haskell :: x:X -> {v:Bool | v <=> (f@logic x)}
CASE2: measure f@logic :: X -> Y <=> f@haskell :: x:X -> {v:Y | v = (f@logic x)}
-}
-- formerly: strengthenResult
inlineSpecType :: Bool -> Var -> SpecType
inlineSpecType allowTC v = fromRTypeRep $ rep {ty_res = res `strengthen` r , ty_binds = xs}
where
r = MkUReft (mkReft (mkEApp f (mkA <$> vxs))) mempty
rep = toRTypeRep t
res = ty_res rep
xs = intSymbol (symbol ("x" :: String)) <$> [1..length $ ty_binds rep]
vxs = dropWhile (isErasable' . snd) $ zip xs (ty_args rep)
isErasable' = if allowTC then isEmbeddedClass else isClassType
f = dummyLoc (symbol v)
t = ofType (GM.expandVarType v) :: SpecType
mkA = EVar . fst
mkReft :: Expr -> Reft
mkReft = if isBool res then propReft else exprReft
-- | Refine types of measures: keep going until you find the last data con!
-- this code is a hack! we refine the last data constructor,
-- it got complicated to support both
-- 1. multi parameter measures (see tests/pos/HasElem.hs)
-- 2. measures returning functions (fromReader :: Reader r a -> (r -> a) )
-- TODO: SIMPLIFY by dropping support for multi parameter measures
-- formerly: strengthenResult'
measureSpecType :: Bool -> Var -> SpecType
measureSpecType allowTC v = go mkT [] [(1::Int)..] st
where
mkReft :: Expr -> Reft
mkReft | boolRes = propReft
| otherwise = exprReft
mkT xs = MkUReft (mkReft $ mkEApp locSym (EVar <$> reverse xs)) mempty
locSym = dummyLoc (symbol v)
st = ofType (GM.expandVarType v) :: SpecType
boolRes = isBool $ ty_res $ toRTypeRep st
go f args i (RAllT a t r) = RAllT a (go f args i t) r
go f args i (RAllP p t) = RAllP p $ go f args i t
go f args i (RFun x ii t1 t2 r)
| (if allowTC then isEmbeddedClass else isClassType) t1 = RFun x ii t1 (go f args i t2) r
go f args i t@(RFun _ ii t1 t2 r)
| hasRApps t = RFun x' ii t1 (go f (x':args) (tail i) t2) r
where x' = intSymbol (symbol ("x" :: String)) (head i)
go f args _ t = t `strengthen` f args
hasRApps (RFun _ _ t1 t2 _) = hasRApps t1 || hasRApps t2
hasRApps RApp {} = True
hasRApps _ = False
-- | 'weakenResult foo t' drops the singleton constraint `v = foo x y`
-- that is added, e.g. for measures in /strengthenResult'.
-- This should only be used _when_ checking the body of 'foo'
-- where the output, is, by definition, equal to the singleton.
weakenResult :: Bool -> Var -> SpecType -> SpecType
weakenResult allowTC v t = F.notracepp msg t'
where
msg = "weakenResult v =" ++ GM.showPpr v ++ " t = " ++ showpp t
t' = fromRTypeRep $ rep { ty_res = mapExprReft weaken (ty_res rep) }
rep = toRTypeRep t
weaken x = pAnd . filter ((Just vE /=) . isSingletonExpr x) . conjuncts
vE = mkEApp vF xs
xs = EVar . fst <$> dropWhile ((if allowTC then isEmbeddedClass else isClassType) . snd) xts
xts = zip (ty_binds rep) (ty_args rep)
vF = dummyLoc (symbol v)
type LogicM = ExceptT Error (ReaderT LState Identity)
data LState = LState
{ lsSymMap :: LogicMap
, lsError :: String -> Error
, lsEmb :: TCEmb TyCon
, lsBools :: [Var]
, lsDCMap :: DataConMap
, lsConfig :: Config
}
throw :: String -> LogicM a
throw str = do
fmkError <- reader lsError
throwError $ fmkError str
getState :: LogicM LState
getState = ask
runToLogic
:: TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error)
-> LogicM t -> Either Error t
runToLogic = runToLogicWithBoolBinds []
runToLogicWithBoolBinds
:: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error)
-> LogicM t -> Either Error t
runToLogicWithBoolBinds xs tce lmap dm cfg ferror m
= runReader (runExceptT m) $ LState
{ lsSymMap = lmap
, lsError = ferror
, lsEmb = tce
, lsBools = xs
, lsDCMap = dm
, lsConfig = cfg
}
coreAltToDef :: (IsReft r) => Located LHName -> Var -> [Var] -> Var -> Type -> [C.CoreAlt]
-> LogicM [Def (Located (RRType r)) DataCon]
coreAltToDef locSym z zs y t alts
| not (null litAlts) = measureFail locSym "Cannot lift definition with literal alternatives"
| otherwise = do
d1s <- F.notracepp "coreAltDefs-1" <$> mapM (mkAlt locSym cc myArgs z) dataAlts
d2s <- F.notracepp "coreAltDefs-2" <$> mkDef locSym cc myArgs z defAlts defExpr
return (d1s ++ d2s)
where
myArgs = reverse zs
cc = if eqType t boolTy then P else E
defAlts = GM.defaultDataCons (GM.expandVarType y) ((\(Alt c _ _) -> c) <$> alts)
defExpr = listToMaybe [ e | (Alt C.DEFAULT _ e) <- alts ]
dataAlts = [ a | a@(Alt (C.DataAlt _) _ _) <- alts ]
litAlts = [ a | a@(Alt (C.LitAlt _) _ _) <- alts ]
-- mkAlt :: LocSymbol -> (Expr -> Body) -> [Var] -> Var -> (C.AltCon, [Var], C.CoreExpr)
mkAlt x ctor _args dx (Alt (C.DataAlt d) xs e)
= do
allowTC <- reader (typeclass . lsConfig)
let xs' = filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) xs
Def x {- (toArgs id args) -} d (Just $ varRType dx) (toArgs Just xs')
. ctor
. (`subst1` (F.symbol dx, F.mkEApp (GM.namedLocSymbol d) (F.eVar <$> xs')))
<$> coreToLg e
mkAlt _ _ _ _ alt
= throw $ "Bad alternative" ++ GM.showPpr alt
mkDef x ctor _args dx (Just dtss) (Just e) = do
eDef <- ctor <$> coreToLg e
-- let ys = toArgs id args
let dxt = Just (varRType dx)
return [ Def x {- ys -} d dxt (defArgs x ts) eDef | (d, _, ts) <- dtss ]
mkDef _ _ _ _ _ _ =
return []
toArgs :: IsReft r => (Located (RRType r) -> b) -> [Var] -> [(Symbol, b)]
toArgs f args = [(symbol x, f $ varRType x) | x <- args]
defArgs :: IsReft r => Located LHName -> [Type] -> [(Symbol, Maybe (Located (RRType r)))]
defArgs x = zipWith (\i t -> (defArg i, defRTyp t)) [0..]
where
defArg = tempSymbol (lhNameToResolvedSymbol $ val x)
defRTyp = Just . F.atLoc x . ofType
coreToDef :: IsReft r => Located LHName -> Var -> C.CoreExpr
-> LogicM [Def (Located (RRType r)) DataCon]
coreToDef locSym _ s = do
allowTC <- reader $ typeclass . lsConfig
go [] $ inlinePreds $ simplifyCoreExpr allowTC s
where
go args (C.Lam x e) = go (x:args) e
go args (C.Tick _ e) = go args e
go (z:zs) (C.Case _ y t alts) = coreAltToDef locSym z zs y t alts
go (z:zs) e
| Just t <- isMeasureArg z = coreAltToDef locSym z zs z t [Alt C.DEFAULT [] e]
go _ _ = measureFail locSym "Does not have a case-of at the top-level"
inlinePreds = inlineCoreExpr (eqType boolTy . GM.expandVarType)
measureFail :: Located LHName -> String -> a
measureFail x msg = panic sp e
where
sp = Just (GM.fSrcSpan x)
e = Printf.printf "Cannot create measure '%s': %s" (F.showpp x) msg
-- | 'isMeasureArg x' returns 'Just t' if 'x' is a valid argument for a measure.
isMeasureArg :: Var -> Maybe Type
isMeasureArg x
| Just tc <- tcMb
, Ghc.isAlgTyCon tc = F.notracepp "isMeasureArg" $ Just t
| otherwise = Nothing
where
t = GM.expandVarType x
tcMb = tyConAppTyCon_maybe t
varRType :: (IsReft r) => Var -> Located (RRType r)
varRType = GM.varLocInfo ofType
coreToFun :: LocSymbol -> Var -> C.CoreExpr -> LogicM ([Var], Either Expr Expr)
coreToFun _ _v s = do
allowTC <- reader $ typeclass . lsConfig
go [] $ normalizeCoreExpr allowTC s
where
go acc (C.Lam x e) | isTyVar x = go acc e
go acc (C.Lam x e) = do
allowTC <- reader $ typeclass . lsConfig
let isE = if allowTC then GM.isEmbeddedDictVar else isErasable
if isE x then go acc e else go (x:acc) e
go acc (C.Tick _ e) = go acc e
go acc e = (reverse acc,) . Right <$> coreToLg e
instance Show C.CoreExpr where
show = GM.showPpr
coreToLogic :: C.CoreExpr -> LogicM Expr
coreToLogic cb = do
allowTC <- reader $ typeclass . lsConfig
coreToLg $ normalizeCoreExpr allowTC cb
coreToLg :: C.CoreExpr -> LogicM Expr
coreToLg (C.Let (C.NonRec x (C.Coercion c)) e)
= coreToLg (C.substExpr (C.extendCvSubst C.emptySubst x c) e)
coreToLg (C.Let b e)
= subst1 <$> coreToLg e <*> makesub b
coreToLg (C.Tick _ e) = coreToLg e
coreToLg (C.App (C.Var v) e)
| ignoreVar v = coreToLg e
coreToLg (C.Var x)
| x == falseDataConId = return PFalse
| x == trueDataConId = return PTrue
| otherwise = eVarWithMap x . lsSymMap <$> getState
coreToLg e@(C.App _ _) = toPredApp e
coreToLg (C.Case e b _ alts)
| eqType (GM.expandVarType b) boolTy = checkBoolAlts alts >>= coreToIte e
-- coreToLg (C.Lam x e) = do p <- coreToLg e
-- tce <- lsEmb <$> getState
-- return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
coreToLg (C.Case e b _ alts) = do p <- coreToLg e
casesToLg b p alts
coreToLg (C.Lit l) = case mkLit l of
Nothing -> throw $ "Bad Literal in measure definition" ++ GM.showPpr l
Just i -> return i
coreToLg (C.Cast e c) = do (s, t) <- coerceToLg c
e' <- coreToLg e
return (ECoerc s t e')
-- elaboration reuses coretologic
-- TODO: fix this
coreToLg (C.Lam x e) = do p <- coreToLg e
tce <- lsEmb <$> getState
return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
coreToLg e = throw ("Cannot transform to Logic:\t" ++ GM.showPpr e)
coerceToLg :: Coercion -> LogicM (Sort, Sort)
coerceToLg = typeEqToLg . coercionTypeEq
coercionTypeEq :: Coercion -> (Type, Type)
coercionTypeEq co
| Ghc.Pair s t <- -- GM.tracePpr ("coercion-type-eq-1: " ++ GM.showPpr co) $
coercionKind co
= (s, t)
typeEqToLg :: (Type, Type) -> LogicM (Sort, Sort)
typeEqToLg (s, t) = do
tce <- reader lsEmb
let tx = typeSort tce . expandTypeSynonyms
return $ F.notracepp "TYPE-EQ-TO-LOGIC" (tx s, tx t)
checkBoolAlts :: [C.CoreAlt] -> LogicM (C.CoreExpr, C.CoreExpr)
checkBoolAlts [Alt (C.DataAlt false) [] efalse, Alt (C.DataAlt true) [] etrue]
| false == falseDataCon, true == trueDataCon
= return (efalse, etrue)
checkBoolAlts [Alt (C.DataAlt true) [] etrue, Alt (C.DataAlt false) [] efalse]
| false == falseDataCon, true == trueDataCon
= return (efalse, etrue)
checkBoolAlts alts
= throw ("checkBoolAlts failed on " ++ GM.showPpr alts)
-- @casesToLg v e alts@ transforms a case expression with scrutinee @e@ and
-- alternatives @alts@ into a logic expression. The variable @v@ is the binder
-- for the scrutinee in the case alternatives.
casesToLg :: Var -> Expr -> [C.CoreAlt] -> LogicM Expr
casesToLg v e alts = mapM (altToLg e) normAlts >>= go
where
normAlts = normalizeAlts alts
go :: [(C.AltCon, Expr)] -> LogicM Expr
go [(_,p)] = return (p `subst1` su)
go ((d,p):dps) = do c <- checkDataAlt d e
e' <- go dps
return (EIte c p e' `subst1` su)
go [] = panic (Just (getSrcSpan v)) $ "Unexpected empty cases in casesToLg: " ++ show e
su = (symbol v, e)
checkDataAlt :: C.AltCon -> Expr -> LogicM Expr
checkDataAlt (C.DataAlt d) e = return $ EApp (EVar (makeDataConChecker d)) e
checkDataAlt C.DEFAULT _ = return PTrue
checkDataAlt (C.LitAlt l) e
| Just le <- mkLit l = return (EEq le e)
| otherwise = throw $ "Oops, not yet handled: checkDataAlt on Lit: " ++ GM.showPpr l
-- | 'altsDefault' reorders the CoreAlt to ensure that 'DEFAULT' is at the end.
normalizeAlts :: [C.CoreAlt] -> [C.CoreAlt]
normalizeAlts alts = ctorAlts ++ defAlts
where
(defAlts, ctorAlts) = L.partition isDefault alts
isDefault (Alt c _ _) = c == C.DEFAULT
altToLg :: Expr -> C.CoreAlt -> LogicM (C.AltCon, Expr)
altToLg de (Alt a@(C.DataAlt d) xs e) = do
p <- coreToLg e
dm <- reader lsDCMap
allowTC <- reader (typeclass . lsConfig)
let su = mkSubst $ concat [ dataConProj dm de d x i | (x, i) <- zip (filter (not . if allowTC then GM.isEmbeddedDictVar else GM.isEvVar) xs) [1..]]
return (a, subst su p)
altToLg _ (Alt a _ e)
= (a, ) <$> coreToLg e
dataConProj :: DataConMap -> Expr -> DataCon -> Var -> Int -> [(Symbol, Expr)]
dataConProj dm de d x i = [(symbol x, t), (GM.simplesymbol x, t)]
where
t | primDataCon d = de
| otherwise = EApp (EVar $ makeDataConSelector (Just dm) d i) de
primDataCon :: DataCon -> Bool
primDataCon d = d == intDataCon
coreToIte :: C.CoreExpr -> (C.CoreExpr, C.CoreExpr) -> LogicM Expr
coreToIte e (efalse, etrue)
= do p <- coreToLg e
e1 <- coreToLg efalse
e2 <- coreToLg etrue
return $ EIte p e2 e1
toPredApp :: C.CoreExpr -> LogicM Expr
toPredApp p = do
allowTC <- reader (typeclass . lsConfig)
go . first opSym . splitArgs allowTC $ p
where
opSym = tomaybesymbol
go (Just f, [e1, e2])
| Just rel <- M.lookup f brels
= PAtom rel <$> coreToLg e1 <*> coreToLg e2
go (Just f, [e])
| f == symbol (show 'not)
= PNot <$> coreToLg e
go (Just f, [e1, e2])
| f == symbol (show '(||))
= POr <$> mapM coreToLg [e1, e2]
| f == symbol (show '(&&))
= PAnd <$> mapM coreToLg [e1, e2]
| f == symbol ("Language.Haskell.Liquid.Prelude.==>" :: String)
= PImp <$> coreToLg e1 <*> coreToLg e2
| f == symbol ("Language.Haskell.Liquid.Prelude.<=>" :: String)
= PIff <$> coreToLg e1 <*> coreToLg e2
| f == symbol (show 'const)
= coreToLg e1
go (Just f, [es])
| f == symbol (show 'or)
= POr . deList <$> coreToLg es
| f == symbol (show 'and)
= PAnd . deList <$> coreToLg es
go (_, _)
= toLogicApp p
deList :: Expr -> [Expr]
deList (EApp (EApp (EVar cons) e) es)
| cons == symbol (show '(:))
= e:deList es
deList (EVar nil)
| nil == symbol (show '[])
= []
deList e
= [e]
toLogicApp :: C.CoreExpr -> LogicM Expr
toLogicApp e = do
allowTC <- reader (typeclass . lsConfig)
let (f, es) = splitArgs allowTC e
case f of
C.Var _ -> do args <- mapM coreToLg es
lmap <- lsSymMap <$> getState
def <- (`mkEApp` args) <$> tosymbol f
(\x -> makeApp def lmap x args) <$> tosymbol' f
_ -> do fe <- coreToLg f
args <- mapM coreToLg es
return $ foldl EApp fe args
makeApp :: Expr -> LogicMap -> Located Symbol-> [Expr] -> Expr
makeApp _ _ f [e]
| val f == symbol (show 'negate)
= ENeg e
| val f == symbol (show 'fromInteger)
, ECon c <- e
= ECon c
| (modName, sym) <- GM.splitModuleName (val f)
, symbol ("Ghci" :: String) `isPrefixOfSym` modName
, sym == "len"
= EApp (EVar sym) e
makeApp _ _ f [e1, e2]
| Just op <- M.lookup (val f) bops
= EBin op e1 e2
-- Hack for typeclass support. (overriden == without Eq constraint defined at Ghci)
| (modName, sym) <- GM.splitModuleName (val f)
, symbol ("Ghci" :: String) `isPrefixOfSym` modName
, Just op <- M.lookup (mappendSym (symbol ("GHC.Internal.Num." :: String)) sym) bops
= EBin op e1 e2
makeApp def lmap f es =
eAppWithMap lmap (val f) es def
-- where msg = "makeApp f = " ++ show f ++ " es = " ++ show es ++ " def = " ++ show def
eVarWithMap :: Id -> LogicMap -> Expr
eVarWithMap x lmap = do
eAppWithMap lmap (symbol x) [] (EVar $ symbol x)
brels :: M.HashMap Symbol Brel
brels = M.fromList [ (symbol (show '(==)), Eq)
, (symbol (show '(/=)), Ne)
, (symbol (show '(>=)), Ge)
, (symbol (show '(>)) , Gt)
, (symbol (show '(<=)), Le)
, (symbol (show '(<)) , Lt)
]
-- bops is a map between GHC function names/symbols and binary operators
-- from the logic. We want GHC functions like +, -, etc. to map to the
-- corresponding operators. There are actually multiple sources for +, -,
-- they can come from GHC.Prim, GHC.Internal.Num, GHC.Internal.Real or
-- be an instance of Num for Int.
bops :: M.HashMap Symbol Bop
bops = M.fromList [ (symbol (show '(+)), Plus)
, (numIntSymbol "+", Plus)
, (symbol (show '(+#)), Plus)
, (symbol (show '(-)), Minus)
, (numIntSymbol "-", Minus)
, (symbol (show '(-#)), Minus)
, (symbol (show '(*)), Times)
, (numIntSymbol "*", Times)
, (symbol (show '(*#)), Times)
, (symbol (show '(/)), Div)
, (symbol (show '(%)), Mod)
]
where
numIntSymbol :: String -> Symbol
numIntSymbol = symbol . (++) "GHC.Internal.Num.$fNumInt_$c"
splitArgs :: Bool -> C.Expr t -> (C.Expr t, [C.Arg t])
splitArgs allowTC exprt = (exprt', reverse args)
where
(exprt', args) = go exprt
go (C.App (C.Var i) e) | ignoreVar i = go e
go (C.App f (C.Var v)) | if allowTC then GM.isEmbeddedDictVar v else isErasable v = go f
go (C.App f e) = (f', e:es) where (f', es) = go f
go f = (f, [])
tomaybesymbol :: C.CoreExpr -> Maybe Symbol
tomaybesymbol (C.Var x) = Just $ symbol x
tomaybesymbol _ = Nothing
tosymbol :: C.CoreExpr -> LogicM (Located Symbol)
tosymbol e
= case tomaybesymbol e of
Just x -> return $ dummyLoc x
_ -> throw ("Bad Measure Definition:\n" ++ GM.showPpr e ++ "\t cannot be applied")
tosymbol' :: C.CoreExpr -> LogicM (Located Symbol)
tosymbol' (C.Var x) = return $ dummyLoc $ symbol x
tosymbol' e = throw ("Bad Measure Definition:\n" ++ GM.showPpr e ++ "\t cannot be applied")
makesub :: C.CoreBind -> LogicM (Symbol, Expr)
makesub (C.NonRec x e) = (symbol x,) <$> coreToLg e
makesub _ = throw "Cannot make Logical Substitution of Recursive Definitions"
mkLit :: Literal -> Maybe Expr
mkLit (LitNumber _ n) = mkI n
-- mkLit (MachInt64 n) = mkI n
-- mkLit (MachWord n) = mkI n
-- mkLit (MachWord64 n) = mkI n
-- mkLit (LitInteger n _) = mkI n
mkLit (LitFloat n) = mkR n
mkLit (LitDouble n) = mkR n
mkLit (LitString s) = Just (mkS s)
mkLit (LitChar c) = mkC c
mkLit _ = Nothing -- ELit sym sort
mkI :: Integer -> Maybe Expr
mkI = Just . ECon . I
mkR :: Rational -> Maybe Expr
mkR = Just . ECon . F.R . fromRational
mkS :: ByteString -> Expr
mkS = ESym . SL . decodeUtf8With lenientDecode
mkC :: Char -> Maybe Expr
mkC = Just . ECon . (`F.L` F.charSort) . repr
where
repr = T.pack . show . Data.Char.ord
ignoreVar :: Id -> Bool
ignoreVar i = simpleSymbolVar i `elem` ["I#", "D#"]
-- | Tries to determine if a 'CoreAlt' maps to one of the 'Integer' type constructors.
isBangInteger :: [C.CoreAlt] -> Bool
isBangInteger [Alt (C.DataAlt s) _ _, Alt (C.DataAlt jp) _ _, Alt (C.DataAlt jn) _ _]
= s == Ghc.integerISDataCon
&& jp == Ghc.integerIPDataCon
&& jn == Ghc.integerINDataCon
isBangInteger _ = False
isErasable :: Id -> Bool
isErasable v = F.notracepp msg $ isGhcSplId v && not (isDCId v)
where
msg = "isErasable: " ++ GM.showPpr (v, Ghc.idDetails v)
isGhcSplId :: Id -> Bool
isGhcSplId v = isPrefixOfSym (symbol ("$" :: String)) (simpleSymbolVar v)
isDCId :: Id -> Bool
isDCId v = case Ghc.idDetails v of
DataConWorkId _ -> True
DataConWrapId _ -> True
_ -> False
isANF :: Id -> Bool
isANF v = isPrefixOfSym (symbol ("lq_anf" :: String)) (simpleSymbolVar v)
isDead :: Id -> Bool
isDead = isDeadOcc . occInfo . Ghc.idInfo
-- | 'normalizeCoreExpr allowTC e' simplifies the Core expression 'e' by:
-- 1. inlining predicates (i.e. applications of measures that return Bool)
-- 2. inlining ANF variables (i.e. variables that are introduced by the ANF transformation)
-- 3. simplifying the expression by removing dead binders and applications of
-- type arguments and dictionaries.
--
-- The 'allowTC' flag controls whether type class dictionaries are considered erasable
-- and will be removed from the expression.
--
normalizeCoreExpr :: Bool -> CoreExpr -> CoreExpr
normalizeCoreExpr allowTC = inline_preds . inline_anf . simplifyCoreExpr allowTC
where
inline_preds = inlineCoreExpr (eqType boolTy . GM.expandVarType)
inline_anf = inlineCoreExpr isANF
-- | 'simplifyCoreExpr allowTC e' simplifies the Core expression 'e' by removing
-- applications of type arguments and dictionaries, and by removing dead
-- binders.
--
-- The 'allowTC' flag controls whether type class dictionaries are considered
-- erasable.
--
-- If 'allowTC' is 'True', then type class dictionaries are considered erasable
-- and will be removed from the expression. If 'allowTC' is 'False', then type
-- class dictionaries are not considered erasable and will not be removed.
--
-- This function is used in 'normalizeCoreExpr' to simplify the Core expression
-- before inlining predicates and ANF variables.
--
-- The 'simplifyCoreExpr' function recursively traverses the Core expression and
-- applies the following simplifications:
-- 1. It removes applications of type arguments (i.e. 'C.App e1 (C.Type _)').
-- 2. It removes applications of variables that are considered erasable
-- (i.e. 'C.App e1 (C.Var v)' where 'v' is erasable).
-- 3. It removes applications of lambda expressions where the binder is dead
-- (i.e. 'C.App (C.Lam x e) _' where 'x' is dead).
-- 4. It removes lambda expressions where the binder is a type variable
-- (i.e. 'C.Lam x e' where 'x' is a type variable).
-- 5. It removes lambda expressions where the binder is considered erasable
-- (i.e. 'C.Lam x e' where 'x' is erasable).
-- 6. It removes non-recursive let bindings where the binder is considered
-- erasable (i.e. 'C.Let (C.NonRec x eb) e' where 'x' is erasable).
-- 7. It removes recursive let bindings where all binders are considered
-- erasable (i.e. 'C.Let (C.Rec xes) e' where all 'x' in 'xes' are
-- erasable).
-- 8. It simplifies case expressions that match on a boolean by checking if
-- the alternatives correspond to 'True' and 'False' and then substituting
-- the scrutinee with the appropriate alternative.
-- 9. It simplifies case expressions by removing alternatives that correspond
-- to pattern match errors (i.e. 'isPatErrorAlt').
-- 10. It recursively simplifies applications, casts, ticks, coercions, and
-- type expressions.
--
simplifyCoreExpr :: Bool -> CoreExpr -> CoreExpr
simplifyCoreExpr allowTC = go
where
isDictOrErasable = if allowTC then GM.isEmbeddedDictVar else isErasable
go :: CoreExpr -> CoreExpr
go e@(C.Var _)
= e
go e@(C.Lit _)
= e
go (C.App e1 (C.Type _))
= go e1
go (C.App e1 (C.Var v))
| isDictOrErasable v
= go e1
go (C.App (C.Lam x e) _)
| isDead x
= go e
go (C.App e1 e2)
= C.App (go e1) (go e2)
go (C.Lam x e)
| isTyVar x
= go e
go (C.Lam x e)
| isDictOrErasable x
= go e
go (C.Lam x e)
= C.Lam x (go e)
go (C.Let (C.NonRec x eb) e)
| isDictOrErasable x
= go e
| otherwise
= C.Let (C.NonRec x (go eb)) (go e)
go (C.Let (C.Rec xes) e)
| all (isDictOrErasable . fst) xes
= go e
| otherwise
= C.Let (C.Rec (map (fmap go) xes)) (go e)
go (C.Case e x _t alts@[Alt _ _ ee,_,_])
| isBangInteger alts
= sub (M.singleton x (go e)) (go ee)
go (C.Case e x t alts)
= C.Case (go e) x t $
filter
(not . isPatErrorAlt)
[ Alt c xs (go ealt) | Alt c xs ealt <- alts ]
go (C.Cast e c)
= C.Cast (go e) c
go (C.Tick _ e)
= go e
go (C.Coercion c)
= C.Coercion c
go (C.Type t)
= C.Type t
inlineCoreExpr :: (Id -> Bool) -> CoreExpr -> CoreExpr
inlineCoreExpr p (C.Let (C.NonRec x ex) e)
| p x = sub (M.singleton x (inlineCoreExpr p ex)) (inlineCoreExpr p e)
| otherwise = C.Let (C.NonRec x (inlineCoreExpr p ex)) (inlineCoreExpr p e)
inlineCoreExpr p (C.Let (C.Rec xes) e) = C.Let (C.Rec (map (fmap (inlineCoreExpr p)) xes)) (inlineCoreExpr p e)
inlineCoreExpr p (C.App e1 e2) = C.App (inlineCoreExpr p e1) (inlineCoreExpr p e2)
inlineCoreExpr p (C.Lam x e) = C.Lam x (inlineCoreExpr p e)
inlineCoreExpr p (C.Case e x t alts) =
C.Case (inlineCoreExpr p e) x t
[ Alt c xs (inlineCoreExpr p ealt) | Alt c xs ealt <- alts ]
inlineCoreExpr p (C.Cast e c) = C.Cast (inlineCoreExpr p e) c
inlineCoreExpr p (C.Tick t e) = C.Tick t (inlineCoreExpr p e)
inlineCoreExpr _ (C.Var x) = C.Var x
inlineCoreExpr _ (C.Lit l) = C.Lit l
inlineCoreExpr _ (C.Coercion c) = C.Coercion c
inlineCoreExpr _ (C.Type t) = C.Type t