liquidhaskell-0.8.6.0: src/Language/Haskell/Liquid/GHC/Interface.hs
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
module Language.Haskell.Liquid.GHC.Interface (
-- * Determine the build-order for target files
realTargets
-- * Extract all information needed for verification
, getGhcInfos
, runLiquidGhc
-- * Printer
, pprintCBs
-- * predicates
-- , isExportedVar
-- , exportedVars
) where
import Prelude hiding (error)
import qualified Outputable as O
import GHC hiding (Target, Located, desugarModule)
import qualified GHC
import GHC.Paths (libdir)
import GHC.Serialized
import qualified Language.Haskell.Liquid.GHC.API as Ghc
import Annotations
import Class
import CoreMonad
import CoreSyn
import DataCon
import Digraph
import DriverPhases
import DriverPipeline
import DynFlags
import Finder
import HscTypes hiding (Target)
import IdInfo
import InstEnv
import Module
import Panic (throwGhcExceptionIO)
-- import Serialized
import TcRnTypes
import Var
-- import NameSet
import FastString
import FamInstEnv
import FamInst
import qualified TysPrim
import GHC.LanguageExtensions
import Control.Exception
import Control.Monad
import Data.Bifunctor
import Data.Data
import Data.List hiding (intersperse)
import Data.Maybe
import Data.Generics.Aliases (mkT)
import Data.Generics.Schemes (everywhere)
import qualified Data.HashSet as S
import qualified Data.Map as M
import System.Console.CmdArgs.Verbosity hiding (Loud)
import System.Directory
import System.FilePath
import System.IO.Temp
import Text.Parsec.Pos
import Text.PrettyPrint.HughesPJ hiding (first, (<>))
import Language.Fixpoint.Types hiding (panic, Error, Result, Expr)
import qualified Language.Fixpoint.Misc as Misc
import Language.Haskell.Liquid.Bare
import Language.Haskell.Liquid.GHC.Misc
import Language.Haskell.Liquid.GHC.Play
import Language.Haskell.Liquid.WiredIn (isDerivedInstance)
import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Haskell.Liquid.Misc as Misc
import Language.Haskell.Liquid.Parse
import Language.Haskell.Liquid.Transforms.ANF
import Language.Haskell.Liquid.Types hiding (Spec)
-- import Language.Haskell.Liquid.Types.PrettyPrint
-- import Language.Haskell.Liquid.Types.Visitors
import Language.Haskell.Liquid.UX.CmdLine
import Language.Haskell.Liquid.UX.Config (totalityCheck)
import Language.Haskell.Liquid.UX.QuasiQuoter
import Language.Haskell.Liquid.UX.Tidy
import Language.Fixpoint.Utils.Files
import qualified Debug.Trace as Debug
--------------------------------------------------------------------------------
{- | @realTargets mE cfg targets@ uses `Interface.configureGhcTargets` to
return a list of files
[i1, i2, ... ] ++ [f1, f2, ...]
1. Where each file only (transitively imports) PRECEDIING ones;
2. `f1..` are a permutation of the original `targets`;
3. `i1..` either don't have "fresh" .bspec files.
-}
--------------------------------------------------------------------------------
realTargets :: Maybe HscEnv -> Config -> [FilePath] -> IO [FilePath]
realTargets mbEnv cfg tgtFs
| noCheckImports cfg = return tgtFs
| otherwise = do
incDir <- Misc.getIncludeDir
allFs <- orderTargets mbEnv cfg tgtFs
let srcFs = filter (not . Misc.isIncludeFile incDir) allFs
realFs <- filterM check srcFs
dir <- getCurrentDirectory
return (makeRelative dir <$> realFs)
where
check f = not <$> skipTarget tgts f
tgts = S.fromList tgtFs
orderTargets :: Maybe HscEnv -> Config -> [FilePath] -> IO [FilePath]
orderTargets mbEnv cfg tgtFiles = runLiquidGhc mbEnv cfg $ do
homeModules <- configureGhcTargets tgtFiles
return (modSummaryHsFile <$> mgModSummaries homeModules)
skipTarget :: S.HashSet FilePath -> FilePath -> IO Bool
skipTarget tgts f
| S.member f tgts = return False -- Always check target file
| otherwise = hasFreshBinSpec f -- But skip an import with fresh .bspec
hasFreshBinSpec :: FilePath -> IO Bool
hasFreshBinSpec srcF = do
let specF = extFileName BinSpec srcF
srcMb <- Misc.lastModified srcF
specMb <- Misc.lastModified specF
case (srcMb, specMb) of
(Just srcT, Just specT) -> return (srcT < specT)
_ -> return False
--------------------------------------------------------------------------------
-- | GHC Interface Pipeline ----------------------------------------------------
--------------------------------------------------------------------------------
getGhcInfos :: Maybe HscEnv -> Config -> [FilePath] -> IO ([GhcInfo], HscEnv)
getGhcInfos hscEnv cfg tgtFiles' = do
tgtFiles <- mapM canonicalizePath tgtFiles'
_ <- mapM checkFilePresent tgtFiles
_ <- mapM_ createTempDirectoryIfMissing tgtFiles
logicMap <- liftIO makeLogicMap
runLiquidGhc hscEnv cfg (getGhcInfos' cfg logicMap tgtFiles)
checkFilePresent :: FilePath -> IO ()
checkFilePresent f = do
b <- doesFileExist f
unless b $ panic Nothing ("Cannot find file: " ++ f)
getGhcInfos' :: Config -> LogicMap -> [FilePath] -> Ghc ([GhcInfo], HscEnv)
getGhcInfos' cfg logicMap tgtFiles = do
_ <- compileCFiles cfg
homeModules <- configureGhcTargets tgtFiles
depGraph <- buildDepGraph homeModules
ghcInfos <- processModules cfg logicMap tgtFiles depGraph homeModules
hscEnv <- getSession
return (ghcInfos, hscEnv)
createTempDirectoryIfMissing :: FilePath -> IO ()
createTempDirectoryIfMissing tgtFile = Misc.tryIgnore "create temp directory" $
createDirectoryIfMissing False $ tempDirectory tgtFile
--------------------------------------------------------------------------------
-- | GHC Configuration & Setup -------------------------------------------------
--------------------------------------------------------------------------------
runLiquidGhc :: Maybe HscEnv -> Config -> Ghc a -> IO a
runLiquidGhc hscEnv cfg act =
withSystemTempDirectory "liquid" $ \tmp ->
runGhc (Just libdir) $ do
maybe (return ()) setSession hscEnv
df <- configureDynFlags cfg tmp
prettyPrintGhcErrors df act
updateIncludePaths :: DynFlags -> [FilePath] -> IncludeSpecs
updateIncludePaths df ps = addGlobalInclude (includePaths df) ps
configureDynFlags :: Config -> FilePath -> Ghc DynFlags
configureDynFlags cfg tmp = do
df <- getSessionDynFlags
(df',_,_) <- parseDynamicFlags df $ map noLoc $ ghcOptions cfg
loud <- liftIO isLoud
let df'' = df' { importPaths = nub $ idirs cfg ++ importPaths df'
, libraryPaths = nub $ idirs cfg ++ libraryPaths df'
, includePaths = updateIncludePaths df' (idirs cfg) -- addGlobalInclude (includePaths df') (idirs cfg)
, packageFlags = ExposePackage ""
(PackageArg "ghc-prim")
(ModRenaming True [])
: (packageFlags df')
, debugLevel = 1 -- insert SourceNotes
-- , profAuto = ProfAutoCalls
, ghcLink = LinkInMemory
, hscTarget = HscInterpreted
, ghcMode = CompManager
-- prevent GHC from printing anything, unless in Loud mode
, log_action = if loud
then defaultLogAction
else \_ _ _ _ _ _ -> return ()
-- redirect .hi/.o/etc files to temp directory
, objectDir = Just tmp
, hiDir = Just tmp
, stubDir = Just tmp
} `gopt_set` Opt_ImplicitImportQualified
`gopt_set` Opt_PIC
`gopt_set` Opt_DeferTypedHoles
`xopt_set` MagicHash
`xopt_set` DeriveGeneric
`xopt_set` StandaloneDeriving
_ <- setSessionDynFlags df''
return df''
configureGhcTargets :: [FilePath] -> Ghc ModuleGraph
configureGhcTargets tgtFiles = do
targets <- mapM (`guessTarget` Nothing) tgtFiles
_ <- setTargets targets
moduleGraph <- depanal [] False -- see [NOTE:DROP-BOOT-FILES]
let homeModules = filter (not . isBootSummary) $
flattenSCCs $ topSortModuleGraph False moduleGraph Nothing
let homeNames = moduleName . ms_mod <$> homeModules
_ <- setTargetModules homeNames
liftIO $ whenLoud $ print ("Module Dependencies", homeNames)
return $ mkModuleGraph homeModules
setTargetModules :: [ModuleName] -> Ghc ()
setTargetModules modNames = setTargets $ mkTarget <$> modNames
where
mkTarget modName = GHC.Target (TargetModule modName) True Nothing
compileCFiles :: Config -> Ghc ()
compileCFiles cfg = do
df <- getSessionDynFlags
_ <- setSessionDynFlags $
df { includePaths = updateIncludePaths df (idirs cfg)
, importPaths = nub $ idirs cfg ++ importPaths df
, libraryPaths = nub $ idirs cfg ++ libraryPaths df }
hsc <- getSession
os <- mapM (\x -> liftIO $ compileFile hsc StopLn (x,Nothing)) (nub $ cFiles cfg)
df <- getSessionDynFlags
void $ setSessionDynFlags $ df { ldInputs = nub $ map (FileOption "") os ++ ldInputs df }
{- | [NOTE:DROP-BOOT-FILES] Drop hs-boot files from the graph.
We do it manually rather than using the flag to topSortModuleGraph
because otherwise the order of mutually recursive modules depends
on the modulename, e.g. given
Bar.hs --> Foo.hs --> Bar.hs-boot
we'll get
[Bar.hs, Foo.hs]
which is backwards..
-}
--------------------------------------------------------------------------------
-- Home Module Dependency Graph ------------------------------------------------
--------------------------------------------------------------------------------
type DepGraph = Graph DepGraphNode
type DepGraphNode = Node Module ()
reachableModules :: DepGraph -> Module -> [Module]
reachableModules depGraph mod =
node_key <$> tail (reachableG depGraph (DigraphNode () mod []))
buildDepGraph :: ModuleGraph -> Ghc DepGraph
buildDepGraph homeModules =
graphFromEdgedVerticesOrd <$> mapM mkDepGraphNode (mgModSummaries homeModules)
mkDepGraphNode :: ModSummary -> Ghc DepGraphNode
mkDepGraphNode modSummary =
DigraphNode () (ms_mod modSummary) <$> (filterM isHomeModule =<< modSummaryImports modSummary)
isHomeModule :: Module -> Ghc Bool
isHomeModule mod = do
homePkg <- thisPackage <$> getSessionDynFlags
return $ moduleUnitId mod == homePkg
modSummaryImports :: ModSummary -> Ghc [Module]
modSummaryImports modSummary =
mapM (importDeclModule (ms_mod modSummary))
(ms_textual_imps modSummary)
importDeclModule :: Module -> (Maybe FastString, GHC.Located ModuleName) -> Ghc Module
importDeclModule fromMod (pkgQual, locModName) = do
hscEnv <- getSession
let modName = unLoc locModName
result <- liftIO $ findImportedModule hscEnv modName pkgQual
case result of
Finder.Found _ mod -> return mod
_ -> do
dflags <- getSessionDynFlags
liftIO $ throwGhcExceptionIO $ ProgramError $
O.showPpr dflags (moduleName fromMod) ++ ": " ++
O.showSDoc dflags (cannotFindModule dflags modName result)
--------------------------------------------------------------------------------
-- | Extract Ids ---------------------------------------------------------------
--------------------------------------------------------------------------------
classCons :: Maybe [ClsInst] -> [Id]
classCons Nothing = []
classCons (Just cs) = concatMap (dataConImplicitIds . head . tyConDataCons . classTyCon . is_cls) cs
derivedVars :: Config -> MGIModGuts -> [Var]
derivedVars cfg mg = concatMap (dFunIdVars cbs . is_dfun) derInsts
where
derInsts
| checkDer = insts
| otherwise = filter isDerivedInstance insts
insts = mgClsInstances mg
checkDer = checkDerived cfg
cbs = mgi_binds mg
mgClsInstances :: MGIModGuts -> [ClsInst]
mgClsInstances = fromMaybe [] . mgi_cls_inst
dFunIdVars :: CoreProgram -> DFunId -> [Id]
dFunIdVars cbs fd = notracepp msg $ concatMap bindersOf cbs' ++ deps
where
msg = "DERIVED-VARS-OF: " ++ showpp fd
cbs' = filter f cbs
f (NonRec x _) = eqFd x
f (Rec xes) = any eqFd (fst <$> xes)
eqFd x = varName x == varName fd
deps = concatMap unfoldDep unfolds
unfolds = unfoldingInfo . idInfo <$> concatMap bindersOf cbs'
unfoldDep :: Unfolding -> [Id]
unfoldDep (DFunUnfolding _ _ e) = concatMap exprDep e
unfoldDep CoreUnfolding {uf_tmpl = e} = exprDep e
unfoldDep _ = []
exprDep :: CoreExpr -> [Id]
exprDep = freeVars S.empty
importVars :: CoreProgram -> [Id]
importVars = freeVars S.empty
_definedVars :: CoreProgram -> [Id]
_definedVars = concatMap defs
where
defs (NonRec x _) = [x]
defs (Rec xes) = map fst xes
--------------------------------------------------------------------------------
-- | Per-Module Pipeline -------------------------------------------------------
--------------------------------------------------------------------------------
type SpecEnv = ModuleEnv (ModName, Ms.BareSpec)
processModules :: Config -> LogicMap -> [FilePath] -> DepGraph -> ModuleGraph -> Ghc [GhcInfo]
processModules cfg logicMap tgtFiles depGraph homeModules = do
-- DO NOT DELETE: liftIO $ putStrLn $ "Process Modules: TargetFiles = " ++ show tgtFiles
catMaybes . snd <$> Misc.mapAccumM go emptyModuleEnv (mgModSummaries homeModules)
where
go = processModule cfg logicMap (S.fromList tgtFiles) depGraph
processModule :: Config -> LogicMap -> S.HashSet FilePath -> DepGraph -> SpecEnv -> ModSummary
-> Ghc (SpecEnv, Maybe GhcInfo)
processModule cfg logicMap tgtFiles depGraph specEnv modSummary = do
let mod = ms_mod modSummary
-- DO-NOT-DELETE _ <- liftIO $ whenLoud $ putStrLn $ "Process Module: " ++ showPpr (moduleName mod)
file <- liftIO $ canonicalizePath $ modSummaryHsFile modSummary
let isTarget = file `S.member` tgtFiles
_ <- loadDependenciesOf $ moduleName mod
parsed <- parseModule $ keepRawTokenStream modSummary
let specComments = extractSpecComments parsed
typechecked <- typecheckModule $ ignoreInline parsed
let specQuotes = extractSpecQuotes typechecked
_ <- loadModule' typechecked
(modName, commSpec) <- either throw return $ hsSpecificationP (moduleName mod) specComments specQuotes
liftedSpec <- liftIO $ if isTarget || null specComments then return Nothing else loadLiftedSpec cfg file
let bareSpec = updLiftedSpec commSpec liftedSpec
_ <- checkFilePragmas $ Ms.pragmas bareSpec
let specEnv' = extendModuleEnv specEnv mod (modName, noTerm bareSpec)
(specEnv', ) <$> if isTarget
then Just <$> processTargetModule cfg logicMap depGraph specEnv file typechecked bareSpec
else return Nothing
updLiftedSpec :: Ms.BareSpec -> Maybe Ms.BareSpec -> Ms.BareSpec
updLiftedSpec s1 Nothing = s1
updLiftedSpec s1 (Just s2) = (clear s1) `mappend` s2
where
clear s = s { sigs = [], aliases = [], ealiases = [], qualifiers = [], dataDecls = [] }
keepRawTokenStream :: ModSummary -> ModSummary
keepRawTokenStream modSummary = modSummary
{ ms_hspp_opts = ms_hspp_opts modSummary `gopt_set` Opt_KeepRawTokenStream }
loadDependenciesOf :: ModuleName -> Ghc ()
loadDependenciesOf modName = do
loadResult <- load $ LoadDependenciesOf modName
when (failed loadResult) $ liftIO $ throwGhcExceptionIO $ ProgramError $
"Failed to load dependencies of module " ++ showPpr modName
loadModule' :: TypecheckedModule -> Ghc TypecheckedModule
loadModule' tm = loadModule tm'
where
pm = tm_parsed_module tm
ms = pm_mod_summary pm
df = ms_hspp_opts ms
df' = df { hscTarget = HscNothing, ghcLink = NoLink }
ms' = ms { ms_hspp_opts = df' }
pm' = pm { pm_mod_summary = ms' }
tm' = tm { tm_parsed_module = pm' }
processTargetModule :: Config -> LogicMap -> DepGraph -> SpecEnv -> FilePath -> TypecheckedModule -> Ms.BareSpec
-> Ghc GhcInfo
processTargetModule cfg0 logicMap depGraph specEnv file typechecked bareSpec = do
cfg <- liftIO $ withPragmas cfg0 file (Ms.pragmas bareSpec)
let modSum = pm_mod_summary (tm_parsed_module typechecked)
ghcSrc <- makeGhcSrc cfg file typechecked modSum
bareSpecs <- makeBareSpecs cfg depGraph specEnv modSum bareSpec
let ghcSpec = makeGhcSpec cfg ghcSrc logicMap bareSpecs
_ <- liftIO $ saveLiftedSpec ghcSrc ghcSpec
return $ GI ghcSrc ghcSpec
---------------------------------------------------------------------------------------
-- | @makeGhcSrc@ builds all the source-related information needed for consgen
---------------------------------------------------------------------------------------
makeGhcSrc :: Config -> FilePath -> TypecheckedModule -> ModSummary -> Ghc GhcSrc
makeGhcSrc cfg file typechecked modSum = do
desugared <- desugarModule typechecked
let modGuts = makeMGIModGuts desugared
let modGuts' = dm_core_module desugared
hscEnv <- getSession
-- _ <- liftIO $ whenLoud $ dumpRdrEnv hscEnv modGuts
-- _ <- liftIO $ whenLoud $ dumpTypeEnv typechecked
coreBinds <- liftIO $ anormalize cfg hscEnv modGuts'
_ <- liftIO $ whenNormal $ Misc.donePhase Misc.Loud "A-Normalization"
let dataCons = concatMap (map dataConWorkId . tyConDataCons) (mgi_tcs modGuts)
-- let defVs = definedVars coreBinds
(fiTcs, fiDcs) <- liftIO $ makeFamInstEnv hscEnv
things <- lookupTyThings hscEnv typechecked modGuts
-- _ <- liftIO $ print (showpp things)
let impVars = importVars coreBinds ++ classCons (mgi_cls_inst modGuts)
incDir <- liftIO $ Misc.getIncludeDir
return $ Src
{ giIncDir = incDir
, giTarget = file
, giTargetMod = ModName Target (moduleName (ms_mod modSum))
, giCbs = coreBinds
, giImpVars = impVars
, giDefVars = dataCons ++ (letVars coreBinds)
, giUseVars = readVars coreBinds
, giDerVars = S.fromList (derivedVars cfg modGuts)
, gsExports = mgi_exports modGuts
, gsTcs = mgi_tcs modGuts
, gsCls = mgi_cls_inst modGuts
, gsFiTcs = fiTcs
, gsFiDcs = fiDcs
, gsPrimTcs = TysPrim.primTyCons
, gsQualImps = qualifiedImports typechecked
, gsAllImps = allImports typechecked
, gsTyThings = {- impThings impVars -} [ t | (_, Just t) <- things ]
}
_impThings :: [Var] -> [TyThing] -> [TyThing]
_impThings vars = filter ok
where
vs = S.fromList vars
ok (AnId x) = S.member x vs
ok _ = True
allImports :: TypecheckedModule -> S.HashSet Symbol
allImports tm = case tm_renamed_source tm of
Nothing -> Debug.trace "WARNING: Missing RenamedSource" mempty
Just (_,imps,_,_) -> S.fromList (symbol . unLoc . ideclName . unLoc <$> imps)
qualifiedImports :: TypecheckedModule -> QImports
qualifiedImports tm = case tm_renamed_source tm of
Nothing -> Debug.trace "WARNING: Missing RenamedSource" (qImports mempty)
Just (_,imps,_,_) -> qImports [ (qn, n) | i <- imps
, let decl = unLoc i
, let m = unLoc (ideclName decl)
, qm <- maybeToList (unLoc <$> ideclAs decl)
, let [n,qn] = symbol <$> [m, qm]
]
qImports :: [(Symbol, Symbol)] -> QImports
qImports qns = QImports
{ qiNames = Misc.group qns
, qiModules = S.fromList (snd <$> qns)
}
---------------------------------------------------------------------------------------
-- | @lookupTyThings@ grabs all the @Name@s and associated @TyThing@ known to GHC
-- for this module; we will use this to create our name-resolution environment
-- (see `Bare.Resolve`)
---------------------------------------------------------------------------------------
lookupTyThings :: HscEnv -> TypecheckedModule -> MGIModGuts -> Ghc [(Name, Maybe TyThing)]
lookupTyThings hscEnv tcm mg =
forM (mgNames mg) $ \n -> do
tt1 <- lookupName n
tt2 <- liftIO $ Ghc.hscTcRcLookupName hscEnv n
tt3 <- modInfoLookupName mi n
tt4 <- lookupGlobalName n
return (n, Misc.firstMaybes [tt1, tt2, tt3, tt4])
where
mi = tm_checked_module_info tcm
-- lookupName :: GhcMonad m => Name -> m (Maybe TyThing)
-- hscTcRcLookupName :: HscEnv -> Name -> IO (Maybe TyThing)
-- modInfoLookupName :: GhcMonad m => ModuleInfo -> Name -> m (Maybe TyThing)
-- lookupGlobalName :: GhcMonad m => Name -> m (Maybe TyThing)
_dumpTypeEnv :: TypecheckedModule -> IO ()
_dumpTypeEnv tm = do
print "DUMP-TYPE-ENV"
print (showpp <$> tcmTyThings tm)
tcmTyThings :: TypecheckedModule -> Maybe [Name]
tcmTyThings
= id
-- typeEnvElts
-- . tcg_type_env . fst
-- . md_types . snd
-- . tm_internals_
. modInfoTopLevelScope
. tm_checked_module_info
_dumpRdrEnv :: HscEnv -> MGIModGuts -> IO ()
_dumpRdrEnv _hscEnv modGuts = do
print "DUMP-RDR-ENV"
print (mgNames modGuts)
-- print (hscNames hscEnv)
-- print (mgDeps modGuts)
where
_mgDeps = Ghc.dep_mods . mgi_deps
_hscNames = fmap showPpr . Ghc.ic_tythings . Ghc.hsc_IC
mgNames :: MGIModGuts -> [Ghc.Name]
mgNames = fmap Ghc.gre_name . Ghc.globalRdrEnvElts . mgi_rdr_env
---------------------------------------------------------------------------------------
-- | @makeBareSpecs@ loads BareSpec for target and imported modules
---------------------------------------------------------------------------------------
makeBareSpecs :: Config -> DepGraph -> SpecEnv -> ModSummary -> Ms.BareSpec
-> Ghc [(ModName, Ms.BareSpec)]
makeBareSpecs cfg depGraph specEnv modSum tgtSpec = do
let paths = nub $ idirs cfg ++ importPaths (ms_hspp_opts modSum)
_ <- liftIO $ whenLoud $ putStrLn $ "paths = " ++ show paths
let reachable = reachableModules depGraph (ms_mod modSum)
specSpecs <- findAndParseSpecFiles cfg paths modSum reachable
let homeSpecs = cachedBareSpecs specEnv reachable
let impSpecs = specSpecs ++ homeSpecs
let tgtMod = ModName Target (moduleName (ms_mod modSum))
return $ (tgtMod, tgtSpec) : impSpecs
modSummaryHsFile :: ModSummary -> FilePath
modSummaryHsFile modSummary =
fromMaybe
(panic Nothing $
"modSummaryHsFile: missing .hs file for " ++
showPpr (ms_mod modSummary))
(ml_hs_file $ ms_location modSummary)
cachedBareSpecs :: SpecEnv -> [Module] -> [(ModName, Ms.BareSpec)]
cachedBareSpecs specEnv mods = lookupBareSpec <$> mods
where
lookupBareSpec m = fromMaybe (err m) (lookupModuleEnv specEnv m)
err m = impossible Nothing ("lookupBareSpec: missing module " ++ showPpr m)
checkFilePragmas :: [Located String] -> Ghc ()
checkFilePragmas = Misc.applyNonNull (return ()) throw . mapMaybe err
where
err pragma
| check (val pragma) = Just (ErrFilePragma $ fSrcSpan pragma :: Error)
| otherwise = Nothing
check pragma = any (`isPrefixOf` pragma) bad
bad =
[ "-i", "--idirs"
, "-g", "--ghc-option"
, "--c-files", "--cfiles"
]
--------------------------------------------------------------------------------
-- | Family instance information
--------------------------------------------------------------------------------
makeFamInstEnv :: HscEnv -> IO ([GHC.TyCon], [(Symbol, DataCon)])
makeFamInstEnv env = do
famInsts <- getFamInstances env
let fiTcs = [ tc | FamInst { fi_flavor = DataFamilyInst tc } <- famInsts ]
let fiDcs = [ (symbol d, d) | tc <- fiTcs, d <- tyConDataCons tc ]
return (fiTcs, fiDcs)
getFamInstances :: HscEnv -> IO [FamInst]
getFamInstances env = do
(_, Just (pkg_fie, home_fie)) <- runTcInteractive env tcGetFamInstEnvs
return $ famInstEnvElts home_fie ++ famInstEnvElts pkg_fie
--------------------------------------------------------------------------------
-- | Extract Specifications from GHC -------------------------------------------
--------------------------------------------------------------------------------
extractSpecComments :: ParsedModule -> [(SourcePos, String)]
extractSpecComments = mapMaybe extractSpecComment
. concat
. M.elems
. snd
. pm_annotations
-- | 'extractSpecComment' pulls out the specification part from a full comment
-- string, i.e. if the string is of the form:
-- 1. '{-@ S @-}' then it returns the substring 'S',
-- 2. '{-@ ... -}' then it throws a malformed SPECIFICATION ERROR, and
-- 3. Otherwise it is just treated as a plain comment so we return Nothing.
extractSpecComment :: GHC.Located AnnotationComment -> Maybe (SourcePos, String)
extractSpecComment (GHC.L sp (AnnBlockComment text))
| isPrefixOf "{-@" text && isSuffixOf "@-}" text -- valid specification
= Just (offsetPos, take (length text - 6) $ drop 3 text)
| isPrefixOf "{-@" text -- invalid specification
= uError $ ErrParseAnn sp "A valid specification must have a closing '@-}'."
where
offsetPos = incSourceColumn (srcSpanSourcePos sp) 3
extractSpecComment _ = Nothing
extractSpecQuotes :: TypecheckedModule -> [BPspec]
extractSpecQuotes typechecked = mapMaybe extractSpecQuote anns
where
anns = map ann_value $
filter (isOurModTarget . ann_target) $
tcg_anns $ fst $ tm_internals_ typechecked
isOurModTarget (ModuleTarget mod1) = mod1 == mod
isOurModTarget _ = False
mod = ms_mod $ pm_mod_summary $ tm_parsed_module typechecked
extractSpecQuote :: AnnPayload -> Maybe BPspec
extractSpecQuote payload =
case fromSerialized deserializeWithData payload of
Nothing -> Nothing
Just qt -> Just $ refreshSymbols $ liquidQuoteSpec qt
refreshSymbols :: Data a => a -> a
refreshSymbols = everywhere (mkT refreshSymbol)
refreshSymbol :: Symbol -> Symbol
refreshSymbol = symbol . symbolText
--------------------------------------------------------------------------------
-- | Finding & Parsing Files ---------------------------------------------------
--------------------------------------------------------------------------------
-- | Handle Spec Files ---------------------------------------------------------
findAndParseSpecFiles :: Config
-> [FilePath]
-> ModSummary
-> [Module]
-> Ghc [(ModName, Ms.BareSpec)]
findAndParseSpecFiles cfg paths modSummary reachable = do
impSumms <- mapM getModSummary (moduleName <$> reachable)
imps'' <- nub . concat <$> mapM modSummaryImports (modSummary : impSumms)
imps' <- filterM ((not <$>) . isHomeModule) imps''
let imps = m2s <$> imps'
fs' <- moduleFiles Spec paths imps
-- liftIO $ whenLoud $ print ("moduleFiles-imps'': " ++ show (m2s <$> imps''))
-- liftIO $ whenLoud $ print ("moduleFiles-imps' : " ++ show (m2s <$> imps'))
-- liftIO $ whenLoud $ print ("moduleFiles-imps : " ++ show imps)
-- liftIO $ whenLoud $ print ("moduleFiles-Paths : " ++ show paths)
-- liftIO $ whenLoud $ print ("moduleFiles-Specs : " ++ show fs')
patSpec <- getPatSpec paths $ totalityCheck cfg
rlSpec <- getRealSpec paths $ not (linear cfg)
let fs = patSpec ++ rlSpec ++ fs'
transParseSpecs paths mempty mempty fs
where
m2s = moduleNameString . moduleName
getPatSpec :: [FilePath] -> Bool -> Ghc [FilePath]
getPatSpec paths totalitycheck
| totalitycheck = moduleFiles Spec paths [patErrorName]
| otherwise = return []
where
patErrorName = "PatErr"
getRealSpec :: [FilePath] -> Bool -> Ghc [FilePath]
getRealSpec paths freal
| freal = moduleFiles Spec paths [realSpecName]
| otherwise = moduleFiles Spec paths [notRealSpecName]
where
realSpecName = "Real"
notRealSpecName = "NotReal"
transParseSpecs :: [FilePath]
-> S.HashSet FilePath
-> [(ModName, Ms.BareSpec)]
-> [FilePath]
-> Ghc [(ModName, Ms.BareSpec)]
transParseSpecs _ _ specs [] = return specs
transParseSpecs paths seenFiles specs newFiles = do
-- liftIO $ print ("TRANS-PARSE-SPECS", seenFiles, newFiles)
newSpecs <- liftIO $ mapM parseSpecFile newFiles
impFiles <- moduleFiles Spec paths $ specsImports newSpecs
let seenFiles' = seenFiles `S.union` S.fromList newFiles
let specs' = specs ++ map (second noTerm) newSpecs
let newFiles' = filter (not . (`S.member` seenFiles')) impFiles
transParseSpecs paths seenFiles' specs' newFiles'
where
specsImports ss = nub $ concatMap (map symbolString . Ms.imports . snd) ss
noTerm :: Ms.BareSpec -> Ms.BareSpec
noTerm spec = spec { Ms.decr = mempty, Ms.lazy = mempty, Ms.termexprs = mempty }
parseSpecFile :: FilePath -> IO (ModName, Ms.BareSpec)
parseSpecFile file = either throw return . specSpecificationP file =<< Misc.sayReadFile file
-- Find Hquals Files -----------------------------------------------------------
_moduleHquals :: MGIModGuts
-> [FilePath]
-> FilePath
-> [String]
-> [FilePath]
-> Ghc [FilePath]
_moduleHquals mgi paths target imps incs = do
hqs <- specIncludes Hquals paths incs
hqs' <- moduleFiles Hquals paths (mgi_namestring mgi : imps)
hqs'' <- liftIO $ filterM doesFileExist [extFileName Hquals target]
return $ Misc.sortNub $ hqs'' ++ hqs ++ hqs'
-- Find Files for Modules ------------------------------------------------------
moduleFiles :: Ext -> [FilePath] -> [String] -> Ghc [FilePath]
moduleFiles ext paths names = catMaybes <$> mapM (moduleFile ext paths) names
moduleFile :: Ext -> [FilePath] -> String -> Ghc (Maybe FilePath)
moduleFile ext paths name
| ext `elem` [Hs, LHs] = do
graph <- mgModSummaries <$> getModuleGraph
case find (\m -> not (isBootSummary m) &&
name == moduleNameString (ms_mod_name m)) graph of
Nothing -> liftIO $ getFileInDirs (extModuleName name ext) paths
Just ms -> return $ normalise <$> ml_hs_file (ms_location ms)
| otherwise = liftIO $ getFileInDirs (extModuleName name ext) paths
specIncludes :: Ext -> [FilePath] -> [FilePath] -> Ghc [FilePath]
specIncludes ext paths reqs = do
let libFile = extFileNameR ext $ symbolString preludeName
let incFiles = catMaybes $ reqFile ext <$> reqs
liftIO $ forM (libFile : incFiles) $ \f -> do
mfile <- getFileInDirs f paths
case mfile of
Just file -> return file
Nothing -> panic Nothing $ "cannot find " ++ f ++ " in " ++ show paths
reqFile :: Ext -> FilePath -> Maybe FilePath
reqFile ext s
| isExtFile ext s = Just s
| otherwise = Nothing
--------------------------------------------------------------------------------
-- Assemble Information for Spec Extraction ------------------------------------
--------------------------------------------------------------------------------
makeMGIModGuts :: DesugaredModule -> MGIModGuts
makeMGIModGuts desugared = miModGuts deriv modGuts
where
modGuts = coreModule desugared
deriv = Just $ instEnvElts $ mg_inst_env modGuts
makeLogicMap :: IO LogicMap
makeLogicMap = do
lg <- Misc.getCoreToLogicPath
lspec <- Misc.sayReadFile lg
case parseSymbolToLogic lg lspec of
Left e -> throw e
Right lm -> return (lm <> listLMap)
listLMap :: LogicMap -- TODO-REBARE: move to wiredIn
listLMap = toLogicMap [ (dummyLoc nilName , [] , hNil)
, (dummyLoc consName, [x, xs], hCons (EVar <$> [x, xs])) ]
where
x = "x"
xs = "xs"
hNil = mkEApp (dcSym Ghc.nilDataCon ) []
hCons = mkEApp (dcSym Ghc.consDataCon)
dcSym = dummyLoc . dropModuleUnique . symbol
--------------------------------------------------------------------------------
-- | Pretty Printing -----------------------------------------------------------
--------------------------------------------------------------------------------
instance PPrint GhcSpec where
pprintTidy k spec = vcat
[ "******* Target Variables ********************"
, pprintTidy k $ gsTgtVars (gsVars spec)
, "******* Type Signatures *********************"
, pprintLongList k (gsTySigs (gsSig spec))
, "******* Assumed Type Signatures *************"
, pprintLongList k (gsAsmSigs (gsSig spec))
, "******* DataCon Specifications (Measure) ****"
, pprintLongList k (gsCtors (gsData spec))
, "******* Measure Specifications **************"
, pprintLongList k (gsMeas (gsData spec)) ]
instance PPrint GhcInfo where
pprintTidy k info = vcat
[ -- "*************** Imports *********************"
-- , intersperse comma $ text <$> imports info
-- , "*************** Includes ********************"
-- , intersperse comma $ text <$> includes info
"*************** Imported Variables **********"
, pprDoc $ giImpVars (giSrc info)
, "*************** Defined Variables ***********"
, pprDoc $ giDefVars (giSrc info)
, "*************** Specification ***************"
, pprintTidy k $ giSpec info
, "*************** Core Bindings ***************"
, pprintCBs $ giCbs (giSrc info) ]
-- RJ: the silly guards below are to silence the unused-var checker
pprintCBs :: [CoreBind] -> Doc
pprintCBs
| otherwise = pprintCBsTidy
| otherwise = pprintCBsVerbose
where
pprintCBsTidy = pprDoc . tidyCBs
pprintCBsVerbose = text . O.showSDocDebug unsafeGlobalDynFlags . O.ppr . tidyCBs
instance Show GhcInfo where
show = showpp
instance PPrint TargetVars where
pprintTidy _ AllVars = text "All Variables"
pprintTidy k (Only vs) = text "Only Variables: " <+> pprintTidy k vs
------------------------------------------------------------------------
-- Dealing with Errors ---------------------------------------------------
------------------------------------------------------------------------
instance Result SourceError where
result = (`Crash` "Invalid Source") . sourceErrors ""