{-# LANGUAGE CPP #-}

{-# LANGUAGE OverloadedStrings #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE GADTs #-}

{-# LANGUAGE NoMonomorphismRestriction #-}

{-# LANGUAGE RankNTypes #-}

{-# LANGUAGE TupleSections #-}

{-# LANGUAGE TypeSynonymInstances #-}

{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE ViewPatterns #-}

{-# LANGUAGE PatternSynonyms #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.

{-# OPTIONS_GHC -Wno-orphans #-}

-- | This module contains a wrappers and utility functions for

module Liquid.GHC.Misc where

import Data.String

import qualified Data.List as L

import Debug.Trace

import Prelude hiding (error)

import Liquid.GHC.API as Ghc hiding ( L

, sourceName

, showPpr

, showSDocDump

, panic

, showSDoc

)

import qualified Liquid.GHC.API as Ghc (GenLocated (L), showSDoc, panic, showSDocDump)

import Data.Char (isLower, isSpace, isUpper)

import Data.Maybe (isJust, fromMaybe, fromJust, maybeToList)

import Data.Hashable

import qualified Data.HashSet as S

import qualified Data.Map.Strict as OM

import Control.Monad.State (evalState, get, modify)

import qualified Data.Text.Encoding.Error as TE

import qualified Data.Text.Encoding as T

import qualified Data.Text as T

import Control.Arrow (second)

import Control.Monad ((>=>), foldM)

import qualified Text.PrettyPrint.HughesPJ as PJ

import Language.Fixpoint.Types hiding (L, panic, Loc (..), SrcSpan, Constant, SESearch (..))

import qualified Language.Fixpoint.Types as F

import Language.Fixpoint.Misc (safeHead, safeLast, errorstar) -- , safeLast, safeInit)

import Language.Haskell.Liquid.Misc (keyDiff)

import Control.DeepSeq

import Language.Haskell.Liquid.Types.Errors

isAnonBinder :: Ghc.TyConBinder -> Bool

isAnonBinder (Bndr _ (AnonTCB _)) = True

isAnonBinder (Bndr _ _) = False

mkAlive :: Var -> Id

mkAlive x

| isId x && isDeadOcc (idOccInfo x)

= setIdInfo x (setOccInfo (idInfo x) noOccInfo)

| otherwise

= x

-- | Encoding and Decoding Location --------------------------------------------

srcSpanTick :: Module -> SrcSpan -> CoreTickish

srcSpanTick m sp = ProfNote (AllCafsCC m sp) False True

tickSrcSpan :: CoreTickish -> SrcSpan

tickSrcSpan (ProfNote cc _ _) = cc_loc cc

tickSrcSpan (SourceNote ss _) = RealSrcSpan ss Nothing

tickSrcSpan _ = noSrcSpan

-- | Generic Helpers for Accessing GHC Innards ---------------------------------

stringTyVar :: String -> TyVar

stringTyVar s = mkTyVar name liftedTypeKind

where

name = mkInternalName (mkUnique 'x' 24) occ noSrcSpan

occ = mkTyVarOcc s

stringVar :: String -> Type -> Var

stringVar s t = mkLocalVar VanillaId name Many t vanillaIdInfo

where

name = mkInternalName (mkUnique 'x' 25) occ noSrcSpan

occ = mkVarOcc s

maybeAuxVar :: Symbol -> Maybe Var

maybeAuxVar s

| isMethod sym = Just sv

| otherwise = Nothing

where (_, uid) = splitModuleUnique s

sym = dropModuleNames s

sv = mkExportedLocalId VanillaId name anyTy

-- 'x' is chosen for no particular reason..

name = mkInternalName (mkUnique 'x' uid) occ noSrcSpan

occ = mkVarOcc (T.unpack (symbolText sym))

stringTyCon :: Char -> Int -> String -> TyCon

stringTyCon = stringTyConWithKind anyTy

stringTyConWithKind :: Kind -> Char -> Int -> String -> TyCon

stringTyConWithKind k c n s = Ghc.mkKindTyCon name [] k [] name

where

name = mkInternalName (mkUnique c n) occ noSrcSpan

occ = mkTcOcc s

hasBaseTypeVar :: Var -> Bool

hasBaseTypeVar = isBaseType . varType

isBaseType :: Type -> Bool

isBaseType (ForAllTy _ _) = False

isBaseType (FunTy { ft_arg = t1, ft_res = t2}) = isBaseType t1 && isBaseType t2

isBaseType (TyVarTy _) = True

isBaseType (TyConApp _ ts) = all isBaseType ts

isBaseType (AppTy t1 t2) = isBaseType t1 && isBaseType t2

isBaseType _ = False

isTmpVar :: Var -> Bool

isTmpVar = isTmpSymbol . dropModuleNamesAndUnique . symbol

isTmpSymbol :: Symbol -> Bool

isTmpSymbol x = any (`isPrefixOfSym` x) [anfPrefix, tempPrefix, "ds_"]

validTyVar :: String -> Bool

validTyVar s@(c:_) = isLower c && not (any isSpace s)

validTyVar _ = False

tvId :: TyVar -> String

tvId α = {- traceShow ("tvId: α = " ++ show α) $ -} showPpr α ++ show (varUnique α)

tidyCBs :: [CoreBind] -> [CoreBind]

tidyCBs = map unTick

unTick :: CoreBind -> CoreBind

unTick (NonRec b e) = NonRec b (unTickExpr e)

unTick (Rec bs) = Rec $ map (second unTickExpr) bs

unTickExpr :: CoreExpr -> CoreExpr

unTickExpr (App e a) = App (unTickExpr e) (unTickExpr a)

unTickExpr (Lam b e) = Lam b (unTickExpr e)

unTickExpr (Let b e) = Let (unTick b) (unTickExpr e)

unTickExpr (Case e b t as) = Case (unTickExpr e) b t (map unTickAlt as)

where unTickAlt (Alt a b' e') = Alt a b' (unTickExpr e')

unTickExpr (Cast e c) = Cast (unTickExpr e) c

unTickExpr (Tick _ e) = unTickExpr e

unTickExpr x = x

isFractionalClass :: Class -> Bool

isFractionalClass clas = classKey clas `elem` fractionalClassKeys

isOrdClass :: Class -> Bool

isOrdClass clas = classKey clas == ordClassKey

-- | Pretty Printers -----------------------------------------------------------

notracePpr :: Outputable a => String -> a -> a

notracePpr _ x = x

tracePpr :: Outputable a => String -> a -> a

tracePpr s x = trace ("\nTrace: [" ++ s ++ "] : " ++ showPpr x) x

pprShow :: Show a => a -> Ghc.SDoc

pprShow = text . show

toFixSDoc :: Fixpoint a => a -> PJ.Doc

toFixSDoc = PJ.text . PJ.render . toFix

sDocDoc :: Ghc.SDoc -> PJ.Doc

sDocDoc = PJ.text . showSDoc

pprDoc :: Outputable a => a -> PJ.Doc

pprDoc = sDocDoc . ppr

showPpr :: Outputable a => a -> String

showPpr = showSDoc . ppr

showSDoc :: Ghc.SDoc -> String

showSDoc = Ghc.renderWithContext ctx

where

style = Ghc.mkUserStyle myQualify Ghc.AllTheWay

ctx = Ghc.defaultSDocContext { sdocStyle = style }

myQualify :: Ghc.PrintUnqualified

myQualify = Ghc.neverQualify { Ghc.queryQualifyName = Ghc.alwaysQualifyNames }

showSDocDump :: Ghc.SDoc -> String

showSDocDump = Ghc.showSDocDump Ghc.defaultSDocContext

instance Outputable a => Outputable (S.HashSet a) where

ppr = ppr . S.toList

typeUniqueString :: Outputable a => a -> String

typeUniqueString = {- ("sort_" ++) . -} showSDocDump . ppr

-- | Manipulating Source Spans -------------------------------------------------

newtype Loc = L (Int, Int) deriving (Eq, Ord, Show)

instance Hashable Loc where

hashWithSalt i (L z) = hashWithSalt i z

instance Hashable SrcSpan where

hashWithSalt i (UnhelpfulSpan reason) = case reason of

UnhelpfulNoLocationInfo -> hashWithSalt i (uniq $ fsLit "UnhelpfulNoLocationInfo")

UnhelpfulWiredIn -> hashWithSalt i (uniq $ fsLit "UnhelpfulWiredIn")

UnhelpfulInteractive -> hashWithSalt i (uniq $ fsLit "UnhelpfulInteractive")

UnhelpfulGenerated -> hashWithSalt i (uniq $ fsLit "UnhelpfulGenerated")

UnhelpfulOther fs -> hashWithSalt i (uniq fs)

hashWithSalt i (RealSrcSpan s _) = hashWithSalt i (srcSpanStartLine s, srcSpanStartCol s, srcSpanEndCol s)

fSrcSpan :: (F.Loc a) => a -> SrcSpan

fSrcSpan = fSrcSpanSrcSpan . F.srcSpan

fSourcePos :: (F.Loc a) => a -> F.SourcePos

fSourcePos = F.sp_start . F.srcSpan

fSrcSpanSrcSpan :: F.SrcSpan -> SrcSpan

fSrcSpanSrcSpan (F.SS p p') = sourcePos2SrcSpan p p'

srcSpanFSrcSpan :: SrcSpan -> F.SrcSpan

srcSpanFSrcSpan sp = F.SS p p'

where

p = srcSpanSourcePos sp

p' = srcSpanSourcePosE sp

sourcePos2SrcSpan :: SourcePos -> SourcePos -> SrcSpan

sourcePos2SrcSpan p p' = RealSrcSpan (packRealSrcSpan f (unPos l) (unPos c) (unPos l') (unPos c')) Nothing

where

(f, l, c) = F.sourcePosElts p

(_, l', c') = F.sourcePosElts p'

sourcePosSrcSpan :: SourcePos -> SrcSpan

sourcePosSrcSpan p@(SourcePos file line col) = sourcePos2SrcSpan p (SourcePos file line (succPos col))

sourcePosSrcLoc :: SourcePos -> SrcLoc

sourcePosSrcLoc (SourcePos file line col) = mkSrcLoc (fsLit file) (unPos line) (unPos col)

srcSpanSourcePos :: SrcSpan -> SourcePos

srcSpanSourcePos (UnhelpfulSpan _) = dummyPos "<no source information>"

srcSpanSourcePos (RealSrcSpan s _) = realSrcSpanSourcePos s

srcSpanSourcePosE :: SrcSpan -> SourcePos

srcSpanSourcePosE (UnhelpfulSpan _) = dummyPos "<no source information>"

srcSpanSourcePosE (RealSrcSpan s _) = realSrcSpanSourcePosE s

srcSpanFilename :: SrcSpan -> String

srcSpanFilename = maybe "" unpackFS . srcSpanFileName_maybe

srcSpanStartLoc :: RealSrcSpan -> Loc

srcSpanStartLoc l = L (srcSpanStartLine l, srcSpanStartCol l)

srcSpanEndLoc :: RealSrcSpan -> Loc

srcSpanEndLoc l = L (srcSpanEndLine l, srcSpanEndCol l)

oneLine :: RealSrcSpan -> Bool

oneLine l = srcSpanStartLine l == srcSpanEndLine l

lineCol :: RealSrcSpan -> (Int, Int)

lineCol l = (srcSpanStartLine l, srcSpanStartCol l)

realSrcSpanSourcePos :: RealSrcSpan -> SourcePos

realSrcSpanSourcePos s = safeSourcePos file line col

where

file = unpackFS $ srcSpanFile s

line = srcSpanStartLine s

col = srcSpanStartCol s

realSrcSpanSourcePosE :: RealSrcSpan -> SourcePos

realSrcSpanSourcePosE s = safeSourcePos file line col

where

file = unpackFS $ srcSpanFile s

line = srcSpanEndLine s

col = srcSpanEndCol s

getSourcePos :: NamedThing a => a -> SourcePos

getSourcePos = srcSpanSourcePos . getSrcSpan

getSourcePosE :: NamedThing a => a -> SourcePos

getSourcePosE = srcSpanSourcePosE . getSrcSpan

locNamedThing :: NamedThing a => a -> F.Located a

locNamedThing x = F.Loc l lE x

where

l = getSourcePos x

lE = getSourcePosE x

instance F.Loc Var where

srcSpan v = SS (getSourcePos v) (getSourcePosE v)

namedLocSymbol :: (F.Symbolic a, NamedThing a) => a -> F.Located F.Symbol

namedLocSymbol d = F.symbol <$> locNamedThing d

varLocInfo :: (Type -> a) -> Var -> F.Located a

varLocInfo f x = f . varType <$> locNamedThing x

namedPanic :: (NamedThing a) => a -> String -> b

namedPanic x msg = panic (Just (getSrcSpan x)) msg

-- | Manipulating CoreExpr -----------------------------------------------------

collectArguments :: Int -> CoreExpr -> [Var]

collectArguments n e = if length xs > n then take n xs else xs

where

(vs', e') = collectValBinders' $ snd $ collectTyBinders e

vs = fst $ collectBinders $ ignoreLetBinds e'

xs = vs' ++ vs

collectValBinders' :: Ghc.Expr Var -> ([Var], Ghc.Expr Var)

collectValBinders' = go []

where

go tvs (Lam b e) | isTyVar b = go tvs e

go tvs (Lam b e) | isId b = go (b:tvs) e

go tvs (Tick _ e) = go tvs e

go tvs e = (reverse tvs, e)

ignoreLetBinds :: Ghc.Expr t -> Ghc.Expr t

ignoreLetBinds (Let (NonRec _ _) e')

= ignoreLetBinds e'

ignoreLetBinds e

= e

-- | Predicates on CoreExpr and DataCons ---------------------------------------

isExternalId :: Id -> Bool

isExternalId = isExternalName . getName

isTupleId :: Id -> Bool

isTupleId = maybe False Ghc.isTupleDataCon . idDataConM

idDataConM :: Id -> Maybe DataCon

idDataConM x = case idDetails x of

DataConWorkId d -> Just d

DataConWrapId d -> Just d

_ -> Nothing

isDataConId :: Id -> Bool

isDataConId = isJust . idDataConM

getDataConVarUnique :: Var -> Unique

getDataConVarUnique v

| isId v && isDataConId v = getUnique (idDataCon v)

| otherwise = getUnique v

isDictionaryExpression :: Ghc.Expr Id -> Maybe Id

isDictionaryExpression (Tick _ e) = isDictionaryExpression e

isDictionaryExpression (Var x) | isDictionary x = Just x

isDictionaryExpression _ = Nothing

realTcArity :: TyCon -> Arity

realTcArity = tyConArity

kindTCArity :: TyCon -> Arity

kindTCArity = go . tyConKind

where

go (FunTy { ft_res = res}) = 1 + go res

go _ = 0

kindArity :: Kind -> Arity

kindArity (ForAllTy _ res)

= 1 + kindArity res

kindArity _

= 0

uniqueHash :: Uniquable a => Int -> a -> Int

uniqueHash i = hashWithSalt i . getKey . getUnique

lookupRdrName :: HscEnv -> ModuleName -> RdrName -> IO (Maybe Name)

lookupRdrName hsc_env mod_name rdr_name = do

-- First find the package the module resides in by searching exposed packages and home modules

found_module <- findImportedModule hsc_env mod_name Nothing

case found_module of

Found _ mod' -> do

-- Find the exports of the module

(_, mb_iface) <- getModuleInterface hsc_env mod'

case mb_iface of

Just iface -> do

-- Try and find the required name in the exports

let decl_spec = ImpDeclSpec { is_mod = mod_name, is_as = mod_name

, is_qual = False, is_dloc = noSrcSpan }

provenance = Just $ ImpSpec decl_spec ImpAll

env = case mi_globals iface of

Nothing -> mkGlobalRdrEnv (gresFromAvails provenance (mi_exports iface))

Just e -> e

case lookupGRE_RdrName rdr_name env of

[] -> return Nothing

_ -> Ghc.panic "lookupRdrNameInModule"

Nothing -> throwCmdLineErrorS dflags $ Ghc.hsep [Ghc.ptext (sLit "Could not determine the exports of the module"), ppr mod_name]

err' -> throwCmdLineErrorS dflags $ cannotFindModule hsc_env mod_name err'

where dflags = hsc_dflags hsc_env

throwCmdLineErrorS dflags' = throwCmdLineError . Ghc.showSDoc dflags'

throwCmdLineError = throwGhcException . CmdLineError

ignoreInline :: ParsedModule -> ParsedModule

ignoreInline x = x {pm_parsed_source = go <$> pm_parsed_source x}

where

go y = y {hsmodDecls = filter go' (hsmodDecls y) }

go' :: LHsDecl GhcPs -> Bool

go' z

| SigD _ (InlineSig {}) <- unLoc z = False

| otherwise = True

-- | Symbol Conversions --------------------------------------------------------

symbolTyConWithKind :: Kind -> Char -> Int -> Symbol -> TyCon

symbolTyConWithKind k x i n = stringTyConWithKind k x i (symbolString n)

symbolTyCon :: Char -> Int -> Symbol -> TyCon

symbolTyCon x i n = stringTyCon x i (symbolString n)

symbolTyVar :: Symbol -> TyVar

symbolTyVar = stringTyVar . symbolString

localVarSymbol :: Var -> Symbol

localVarSymbol v

| us `isSuffixOfSym` vs = vs

| otherwise = suffixSymbol vs us

where

us = symbol $ showPpr $ getDataConVarUnique v

vs = exportedVarSymbol v

exportedVarSymbol :: Var -> Symbol

exportedVarSymbol x = notracepp msg . symbol . getName $ x

where

msg = "exportedVarSymbol: " ++ showPpr x

qualifiedNameSymbol :: Name -> Symbol

qualifiedNameSymbol n = symbol $ concatFS [modFS, occFS, uniqFS]

where

_msg = showSDoc (ppr n) -- getOccString n

modFS = case nameModule_maybe n of

Nothing -> fsLit ""

Just m -> concatFS [moduleNameFS (moduleName m), fsLit "."]

occFS = occNameFS (getOccName n)

uniqFS

| isSystemName n

= concatFS [fsLit "_", fsLit (showPpr (getUnique n))]

| otherwise

= fsLit ""

instance Symbolic FastString where

symbol = symbol . fastStringText

fastStringText :: FastString -> T.Text

fastStringText = T.decodeUtf8With TE.lenientDecode . bytesFS

tyConTyVarsDef :: TyCon -> [TyVar]

tyConTyVarsDef c

| noTyVars c = []

| otherwise = Ghc.tyConTyVars c

--where

-- none = tracepp ("tyConTyVarsDef: " ++ show c) (noTyVars c)

noTyVars :: TyCon -> Bool

noTyVars c = Ghc.isPrimTyCon c || isFunTyCon c || Ghc.isPromotedDataCon c

-- | Symbol Instances

instance Symbolic TyCon where

symbol = symbol . getName

instance Symbolic Class where

symbol = symbol . getName

instance Symbolic Name where

symbol = symbol . qualifiedNameSymbol

-- | [NOTE:REFLECT-IMPORTS] we **eschew** the `unique` suffix for exported vars,

instance Symbolic Var where -- TODO:reflect-datacons varSymbol

symbol v

| isExternalId v = exportedVarSymbol v

| otherwise = localVarSymbol v

instance Hashable Var where

hashWithSalt = uniqueHash

instance Hashable TyCon where

hashWithSalt = uniqueHash

instance Hashable Class where

hashWithSalt = uniqueHash

instance Hashable DataCon where

hashWithSalt = uniqueHash

instance Fixpoint Var where

toFix = pprDoc

instance Fixpoint Name where

toFix = pprDoc

instance Fixpoint Type where

toFix = pprDoc

instance Show Name where

show = symbolString . symbol

instance Show Var where

show = show . getName

instance Show Class where

show = show . getName

instance Show TyCon where

show = show . getName

instance NFData Class where

rnf t = seq t ()

instance NFData TyCon where

rnf t = seq t ()

instance NFData Type where

rnf t = seq t ()

instance NFData Var where

rnf t = seq t ()

-- | Manipulating Symbols ------------------------------------------------------

takeModuleUnique :: Symbol -> Symbol

takeModuleUnique = mungeNames tailName sepUnique "takeModuleUnique: "

where

tailName msg = symbol . safeLast msg

splitModuleUnique :: Symbol -> (Symbol, Int)

splitModuleUnique x = (dropModuleNamesAndUnique x, base62ToI (takeModuleUnique x))

base62ToI :: Symbol -> Int

base62ToI s = fromMaybe (errorstar "base62ToI Out Of Range") $ go (F.symbolText s)

where

digitToI :: OM.Map Char Int

digitToI = OM.fromList $ zip (['0'..'9'] ++ ['a'..'z'] ++ ['A'..'Z']) [0..]

f acc (flip OM.lookup digitToI -> x) = (acc * 62 +) <$> x

go = foldM f 0 . T.unpack

splitModuleName :: Symbol -> (Symbol, Symbol)

splitModuleName x = (takeModuleNames x, dropModuleNamesAndUnique x)

dropModuleNamesAndUnique :: Symbol -> Symbol

dropModuleNamesAndUnique = dropModuleUnique . dropModuleNames

dropModuleNames :: Symbol -> Symbol

dropModuleNames = dropModuleNamesCorrect

dropModuleNamesCorrect :: Symbol -> Symbol

dropModuleNamesCorrect = F.symbol . go . F.symbolText

where

go s = case T.uncons s of

Just (c,tl) -> if isUpper c && T.any (== '.') tl

then go $ snd $ fromJust $ T.uncons $ T.dropWhile (/= '.') s

else s

Nothing -> s

takeModuleNames :: Symbol -> Symbol

takeModuleNames = F.symbol . go [] . F.symbolText

where

go acc s = case T.uncons s of

Just (c,tl) -> if isUpper c && T.any (== '.') tl

then go (getModule' s:acc) $ snd $ fromJust $ T.uncons $ T.dropWhile (/= '.') s

else T.intercalate "." (reverse acc)

Nothing -> T.intercalate "." (reverse acc)

getModule' = T.takeWhile (/= '.')

dropModuleUnique :: Symbol -> Symbol

dropModuleUnique = mungeNames headName sepUnique "dropModuleUnique: "

where

headName msg = symbol . safeHead msg

cmpSymbol :: Symbol -> Symbol -> Bool

cmpSymbol coreSym logicSym

= (dropModuleUnique coreSym == dropModuleNamesAndUnique logicSym)

|| (dropModuleUnique coreSym == dropModuleUnique logicSym)

sepModNames :: T.Text

sepModNames = "."

sepUnique :: T.Text

sepUnique = "#"

mungeNames :: (String -> [T.Text] -> Symbol) -> T.Text -> String -> Symbol -> Symbol

mungeNames _ _ _ "" = ""

mungeNames f d msg s'@(symbolText -> s)

| s' == tupConName = tupConName

| otherwise = f (msg ++ T.unpack s) $ T.splitOn d $ stripParens s

qualifySymbol :: Symbol -> Symbol -> Symbol

qualifySymbol (symbolText -> m) x'@(symbolText -> x)

| isQualified x = x'

| isParened x = symbol (wrapParens (m `mappend` "." `mappend` stripParens x))

| otherwise = symbol (m `mappend` "." `mappend` x)

isQualifiedSym :: Symbol -> Bool

isQualifiedSym (symbolText -> x) = isQualified x

isQualified :: T.Text -> Bool

isQualified y = "." `T.isInfixOf` y

wrapParens :: (IsString a, Monoid a) => a -> a

wrapParens x = "(" `mappend` x `mappend` ")"

isParened :: T.Text -> Bool

isParened xs = xs /= stripParens xs

isDictionary :: Symbolic a => a -> Bool

isDictionary = isPrefixOfSym "$f" . dropModuleNames . symbol

isMethod :: Symbolic a => a -> Bool

isMethod = isPrefixOfSym "$c" . dropModuleNames . symbol

isInternal :: Symbolic a => a -> Bool

isInternal = isPrefixOfSym "$" . dropModuleNames . symbol

isWorker :: Symbolic a => a -> Bool

isWorker s = notracepp ("isWorkerSym: s = " ++ ss) $ "$W" `L.isInfixOf` ss

where

ss = symbolString (symbol s)

isSCSel :: Symbolic a => a -> Bool

isSCSel = isPrefixOfSym "$p" . dropModuleNames . symbol

stripParens :: T.Text -> T.Text

stripParens t = fromMaybe t (strip t)

where

strip = T.stripPrefix "(" >=> T.stripSuffix ")"

stripParensSym :: Symbol -> Symbol

stripParensSym (symbolText -> t) = symbol (stripParens t)

desugarModule :: TypecheckedModule -> Ghc DesugaredModule

desugarModule tcm = do

let ms = pm_mod_summary $ tm_parsed_module tcm

-- let ms = modSummary tcm

let (tcg, _) = tm_internals_ tcm

hsc_env <- getSession

let hsc_env_tmp = hsc_env { hsc_dflags = ms_hspp_opts ms }

guts <- liftIO $ hscDesugar{- WithLoc -} hsc_env_tmp ms tcg

return DesugaredModule { dm_typechecked_module = tcm, dm_core_module = guts }

-- | GHC Compatibility Layer ---------------------------------------------------

gHC_VERSION :: String

gHC_VERSION = show (__GLASGOW_HASKELL__ :: Int)

symbolFastString :: Symbol -> FastString

symbolFastString = mkFastStringByteString . T.encodeUtf8 . symbolText

lintCoreBindings :: [Var] -> CoreProgram -> (Bag SDoc, Bag SDoc)

lintCoreBindings = Ghc.lintCoreBindings (defaultDynFlags undefined (undefined ("LlvmTargets" :: String))) CoreDoNothing

synTyConRhs_maybe :: TyCon -> Maybe Type

synTyConRhs_maybe = Ghc.synTyConRhs_maybe

tcRnLookupRdrName :: HscEnv -> Ghc.LocatedN RdrName -> IO (Messages DecoratedSDoc, Maybe [Name])

tcRnLookupRdrName = Ghc.tcRnLookupRdrName

showCBs :: Bool -> [CoreBind] -> String

showCBs untidy

| untidy =

Ghc.renderWithContext ctx . ppr . tidyCBs

| otherwise = showPpr

where

ctx = Ghc.defaultSDocContext { sdocPprDebug = True }

ignoreCoreBinds :: S.HashSet Var -> [CoreBind] -> [CoreBind]

ignoreCoreBinds vs cbs

| S.null vs = cbs

| otherwise = concatMap go cbs

where

go :: CoreBind -> [CoreBind]

go b@(NonRec x _)

| S.member x vs = []

| otherwise = [b]

go (Rec xes) = [Rec (filter ((`notElem` vs) . fst) xes)]

findVarDef :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)

findVarDef sym cbs = case xCbs of

(NonRec v def : _ ) -> Just (v, def)

(Rec [(v, def)] : _ ) -> Just (v, def)

_ -> Nothing

where

xCbs = [ cb | cb <- concatMap unRec cbs, sym `elem` coreBindSymbols cb ]

unRec (Rec xes) = [NonRec x es | (x,es) <- xes]

unRec nonRec = [nonRec]

findVarDefMethod :: Symbol -> [CoreBind] -> Maybe (Var, CoreExpr)

findVarDefMethod sym cbs =

case rcbs of

(NonRec v def : _ ) -> Just (v, def)

(Rec [(v, def)] : _ ) -> Just (v, def)

_ -> Nothing

where

rcbs | isMethod sym = mCbs

| isDictionary (dropModuleNames sym) = dCbs

| otherwise = xCbs

xCbs = [ cb | cb <- concatMap unRec cbs, sym `elem` coreBindSymbols cb

]

mCbs = [ cb | cb <- concatMap unRec cbs, sym `elem` methodSymbols cb]

dCbs = [ cb | cb <- concatMap unRec cbs, sym `elem` dictionarySymbols cb]

unRec (Rec xes) = [NonRec x es | (x,es) <- xes]

unRec nonRec = [nonRec]

dictionarySymbols :: CoreBind -> [Symbol]

dictionarySymbols = filter isDictionary . map (dropModuleNames . symbol) . binders

methodSymbols :: CoreBind -> [Symbol]

methodSymbols = filter isMethod . map (dropModuleNames . symbol) . binders

coreBindSymbols :: CoreBind -> [Symbol]

coreBindSymbols = map (dropModuleNames . simplesymbol) . binders

simplesymbol :: (NamedThing t) => t -> Symbol

simplesymbol = symbol . getName

binders :: Bind a -> [a]

binders (NonRec z _) = [z]

binders (Rec xes) = fst <$> xes

expandVarType :: Var -> Type

expandVarType = expandTypeSynonyms . varType

-- | The following functions test if a `CoreExpr` or `CoreVar` can be

isEmbeddedDictExpr :: CoreExpr -> Bool

isEmbeddedDictExpr = isEmbeddedDictType . exprType

isEmbeddedDictVar :: Var -> Bool

isEmbeddedDictVar v = F.notracepp msg . isEmbeddedDictType . varType $ v

where

msg = "isGoodCaseBind v = " ++ show v

isEmbeddedDictType :: Type -> Bool

isEmbeddedDictType = anyF [isOrdPred, isNumericPred, isEqPred, isPrelEqPred]

isPrelEqPred :: Type -> Bool

isPrelEqPred ty = case tyConAppTyCon_maybe ty of

Just tyCon -> isPrelEqTyCon tyCon

_ -> False

isPrelEqTyCon :: TyCon -> Bool

isPrelEqTyCon tc = tc `hasKey` eqClassKey

isOrdPred :: Type -> Bool

isOrdPred ty = case tyConAppTyCon_maybe ty of

Just tyCon -> tyCon `hasKey` ordClassKey

_ -> False

isNumericPred :: Type -> Bool

isNumericPred ty = case tyConAppTyCon_maybe ty of

Just tyCon -> getUnique tyCon `elem` numericClassKeys

_ -> False

-- | The following functions test if a `CoreExpr` or `CoreVar` are just types

isPredExpr :: CoreExpr -> Bool

isPredExpr = isPredType . Ghc.exprType

isPredVar :: Var -> Bool

isPredVar v = F.notracepp msg . isPredType . varType $ v

where

msg = "isGoodCaseBind v = " ++ show v

isPredType :: Type -> Bool

isPredType = anyF [ isClassPred, isEqPred, isEqPrimPred ]

anyF :: [a -> Bool] -> a -> Bool

anyF ps x = or [ p x | p <- ps ]

-- | 'defaultDataCons t ds' returns the list of '(dc, types)' pairs,

defaultDataCons :: Type -> [AltCon] -> Maybe [(DataCon, [TyVar], [Type])]

defaultDataCons (TyConApp tc argτs) ds = do

allDs <- Ghc.tyConDataCons_maybe tc

let seenDs = [d | DataAlt d <- ds ]

let defDs = keyDiff showPpr allDs seenDs

return [ (d, Ghc.dataConExTyVars d, map irrelevantMult $ Ghc.dataConInstArgTys d argτs) | d <- defDs ]

defaultDataCons _ _ =

Nothing

isEvVar :: Id -> Bool

isEvVar x = isPredVar x || isTyVar x || isCoVar x

-- | Elaboration

elabRnExpr :: LHsExpr GhcPs -> TcRn CoreExpr

elabRnExpr rdr_expr = do

(rn_expr, _fvs) <- rnLExpr rdr_expr

failIfErrsM

-- Typecheck the expression

((tclvl, (tc_expr, res_ty)), lie)

<- captureTopConstraints $

pushTcLevelM $

tcInferRho rn_expr

-- Generalise

uniq <- newUnique

let { fresh_it = itName uniq (getLocA rdr_expr) }

((_qtvs, _dicts, evbs, _), residual)

<- captureConstraints $

simplifyInfer tclvl NoRestrictions

[] {- No sig vars -}

[(fresh_it, res_ty)]

lie

-- Ignore the dictionary bindings

evbs' <- simplifyInteractive residual

full_expr <- zonkTopLExpr (mkHsDictLet (EvBinds evbs') (mkHsDictLet evbs tc_expr))

initDsTc $ dsLExpr full_expr

newtype HashableType = HashableType {getHType :: Type}

instance Eq HashableType where

x == y = eqType (getHType x) (getHType y)

instance Ord HashableType where

compare x y = nonDetCmpType (getHType x) (getHType y)

instance Outputable HashableType where

ppr = ppr . getHType

-- | Superclass coherence

canonSelectorChains :: PredType -> OM.Map HashableType [Id]

canonSelectorChains t = foldr (OM.unionWith const) mempty (zs : xs)

where

(cls, ts) = Ghc.getClassPredTys t

scIdTys = classSCSelIds cls

ys = fmap (\d -> (d, piResultTys (idType d) (ts ++ [t]))) scIdTys

zs = OM.fromList $ fmap (\(x, y) -> (HashableType y, [x])) ys

xs = fmap (\(d, t') -> fmap (d :) (canonSelectorChains t')) ys

buildCoherenceOblig :: Class -> [[([Id], [Id])]]

buildCoherenceOblig cls = evalState (mapM f xs) OM.empty

where

(ts, _, selIds, _) = classBigSig cls

tts = mkTyVarTy <$> ts

t = mkClassPred cls tts

ys = fmap (\d -> (d, piResultTys (idType d) (tts ++ [t]))) selIds

xs = fmap (\(d, t') -> fmap (d:) (canonSelectorChains t')) ys

f tid = do

ctid' <- get

modify (flip (OM.unionWith const) tid)

pure . OM.elems $ OM.intersectionWith (,) ctid' (fmap tail tid)

coherenceObligToRef :: (F.Symbolic s) => s -> [Id] -> [Id] -> F.Reft

coherenceObligToRef d = coherenceObligToRefE (F.eVar $ F.symbol d)

coherenceObligToRefE :: F.Expr -> [Id] -> [Id] -> F.Reft

coherenceObligToRefE e rps0 rps1 = F.Reft (F.vv_, F.PAtom F.Eq lhs rhs)

where lhs = L.foldr EApp e ps0

rhs = L.foldr EApp (F.eVar F.vv_) ps1

ps0 = F.eVar . F.symbol <$> L.reverse rps0

ps1 = F.eVar . F.symbol <$> L.reverse rps1

data TcWiredIn = TcWiredIn {

tcWiredInName :: Name

, tcWiredInFixity :: Maybe (Int, FixityDirection)

, tcWiredInType :: LHsType GhcRn

}

-- | Run a computation in GHC's typechecking monad with wired in values locally bound in the typechecking environment.

withWiredIn :: TcM a -> TcM a

withWiredIn m = discardConstraints $ do

-- undef <- lookupUndef

wiredIns <- mkWiredIns

-- snd <$> tcValBinds Ghc.NotTopLevel (binds undef wiredIns) (sigs wiredIns) m

snd <$> tcValBinds Ghc.NotTopLevel [] (sigs wiredIns) m