-- | This module provides a GHC 'Plugin' that allows LiquidHaskell to be hooked directly into GHC's
-- compilation pipeline, facilitating its usage and adoption.

{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE ViewPatterns               #-}

module Language.Haskell.Liquid.GHC.Plugin (

  plugin

  ) where

import qualified Liquid.GHC.API         as O
import           Liquid.GHC.API         as GHC hiding (Type)
import qualified Text.PrettyPrint.HughesPJ               as PJ
import qualified Language.Fixpoint.Types                 as F
import qualified  Language.Haskell.Liquid.GHC.Misc        as LH
import qualified Language.Haskell.Liquid.UX.CmdLine      as LH
import qualified Language.Haskell.Liquid.GHC.Interface   as LH
import qualified Language.Haskell.Liquid.Liquid          as LH
import qualified Language.Haskell.Liquid.Types.PrettyPrint as LH ( filterReportErrors
                                                                 , filterReportErrorsWith
                                                                 , defaultFilterReporter
                                                                 , reduceFilters )
import qualified Language.Haskell.Liquid.GHC.Logging     as LH   (fromPJDoc)

import           Language.Haskell.Liquid.GHC.Plugin.Types
import           Language.Haskell.Liquid.GHC.Plugin.Util as Util
import           Language.Haskell.Liquid.GHC.Plugin.SpecFinder
                                                         as SpecFinder

import           Language.Haskell.Liquid.GHC.Types       (MGIModGuts(..), miModGuts)
import           GHC.LanguageExtensions

import           Control.Monad
import qualified Control.Monad.Catch as Ex
import           Control.Monad.IO.Class (MonadIO)

import           Data.Coerce
import           Data.Function                            ((&))
import           Data.Kind                                ( Type )
import           Data.List                               as L
                                                   hiding ( intersperse )
import           Data.IORef
import qualified Data.Set                                as S
import           Data.Set                                 ( Set )


import qualified Data.HashSet                            as HS
import qualified Data.HashMap.Strict                     as HM

import           System.IO.Unsafe                         ( unsafePerformIO )
import           Language.Fixpoint.Types           hiding ( errs
                                                          , panic
                                                          , Error
                                                          , Result
                                                          , Expr
                                                          )

import qualified Language.Haskell.Liquid.Measure         as Ms
import           Language.Haskell.Liquid.Parse
import           Language.Haskell.Liquid.Transforms.ANF
import           Language.Haskell.Liquid.Types     hiding ( getConfig )
import           Language.Haskell.Liquid.Bare
import           Language.Haskell.Liquid.UX.CmdLine

-- | Represents an abnormal but non-fatal state of the plugin. Because it is not
-- meant to escape the plugin, it is not thrown in IO but instead carried around
-- in an `Either`'s `Left` case and handled at the top level of the plugin
-- function.
newtype LiquidCheckException = ErrorsOccurred [Filter] -- Unmatched expected errors
  deriving (LiquidCheckException -> LiquidCheckException -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LiquidCheckException -> LiquidCheckException -> Bool
$c/= :: LiquidCheckException -> LiquidCheckException -> Bool
== :: LiquidCheckException -> LiquidCheckException -> Bool
$c== :: LiquidCheckException -> LiquidCheckException -> Bool
Eq, Eq LiquidCheckException
LiquidCheckException -> LiquidCheckException -> Bool
LiquidCheckException -> LiquidCheckException -> Ordering
LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
$cmin :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
max :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
$cmax :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
>= :: LiquidCheckException -> LiquidCheckException -> Bool
$c>= :: LiquidCheckException -> LiquidCheckException -> Bool
> :: LiquidCheckException -> LiquidCheckException -> Bool
$c> :: LiquidCheckException -> LiquidCheckException -> Bool
<= :: LiquidCheckException -> LiquidCheckException -> Bool
$c<= :: LiquidCheckException -> LiquidCheckException -> Bool
< :: LiquidCheckException -> LiquidCheckException -> Bool
$c< :: LiquidCheckException -> LiquidCheckException -> Bool
compare :: LiquidCheckException -> LiquidCheckException -> Ordering
$ccompare :: LiquidCheckException -> LiquidCheckException -> Ordering
Ord, Int -> LiquidCheckException -> ShowS
[LiquidCheckException] -> ShowS
LiquidCheckException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LiquidCheckException] -> ShowS
$cshowList :: [LiquidCheckException] -> ShowS
show :: LiquidCheckException -> String
$cshow :: LiquidCheckException -> String
showsPrec :: Int -> LiquidCheckException -> ShowS
$cshowsPrec :: Int -> LiquidCheckException -> ShowS
Show)

---------------------------------------------------------------------------------
-- | State and configuration management -----------------------------------------
---------------------------------------------------------------------------------

-- | A reference to cache the LH's 'Config' and produce it only /once/, during the dynFlags hook.
cfgRef :: IORef Config
cfgRef :: IORef Config
cfgRef = forall a. IO a -> a
unsafePerformIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef Config
defConfig
{-# NOINLINE cfgRef #-}

-- | Set to 'True' to enable debug logging.
debugLogs :: Bool
debugLogs :: Bool
debugLogs = Bool
False

---------------------------------------------------------------------------------
-- | Useful functions -----------------------------------------------------------
---------------------------------------------------------------------------------

-- | Reads the 'Config' out of a 'IORef'.
getConfig :: IO Config
getConfig :: IO Config
getConfig = forall a. IORef a -> IO a
readIORef IORef Config
cfgRef

-- | Combinator which conditionally print on the screen based on the value of 'debugLogs'.
debugLog :: MonadIO m => String -> m ()
debugLog :: forall (m :: * -> *). MonadIO m => String -> m ()
debugLog String
msg = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugLogs forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO ()
putStrLn String
msg)

---------------------------------------------------------------------------------
-- | The Plugin entrypoint ------------------------------------------------------
---------------------------------------------------------------------------------

plugin :: GHC.Plugin
plugin :: Plugin
plugin = Plugin
GHC.defaultPlugin {
    typeCheckResultAction :: [String] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
typeCheckResultAction = [String] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
liquidPlugin
  , driverPlugin :: [String] -> HscEnv -> IO HscEnv
driverPlugin          = [String] -> HscEnv -> IO HscEnv
customDynFlags
  , pluginRecompile :: [String] -> IO PluginRecompile
pluginRecompile       = [String] -> IO PluginRecompile
purePlugin
  }
  where
    liquidPlugin :: [CommandLineOption] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
    liquidPlugin :: [String] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
liquidPlugin [String]
_ ModSummary
summary TcGblEnv
gblEnv = do
      Config
cfg <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Config
getConfig
      if Config -> Bool
skipModule Config
cfg then forall (m :: * -> *) a. Monad m => a -> m a
return TcGblEnv
gblEnv
      else ModSummary -> TcGblEnv -> TcM TcGblEnv
liquidPluginGo ModSummary
summary TcGblEnv
gblEnv

    -- Unfortunately, we can't make Haddock run the LH plugin, because the former
    -- does mangle the '.hi' files, causing annotations to not be persisted in the
    -- 'ExternalPackageState' and/or 'HomePackageTable'. For this reason we disable
    -- the plugin altogether if the module is being compiled with Haddock.
    -- See also: https://github.com/ucsd-progsys/liquidhaskell/issues/1727
    -- for a post-mortem.
    liquidPluginGo :: ModSummary -> TcGblEnv -> TcM TcGblEnv
liquidPluginGo ModSummary
summary TcGblEnv
gblEnv = do
      Logger
logger <- forall (m :: * -> *). HasLogger m => m Logger
getLogger
      DynFlags
dynFlags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
      forall (m :: * -> *) a.
MonadIO m =>
Logger -> DynFlags -> SDoc -> (a -> ()) -> m a -> m a
withTiming Logger
logger DynFlags
dynFlags (String -> SDoc
text String
"LiquidHaskell" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
brackets (forall a. Outputable a => a -> SDoc
ppr forall a b. (a -> b) -> a -> b
$ ModSummary -> ModuleName
ms_mod_name ModSummary
summary)) (forall a b. a -> b -> a
const ()) forall a b. (a -> b) -> a -> b
$ do
        if GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_Haddock DynFlags
dynFlags
          then do
            -- Warn the user
            let msg :: Doc
msg     = [Doc] -> Doc
PJ.vcat [ String -> Doc
PJ.text String
"LH can't be run with Haddock."
                                  , Int -> Doc -> Doc
PJ.nest Int
4 forall a b. (a -> b) -> a -> b
$ String -> Doc
PJ.text String
"Documentation will still be created."
                                  ]
            let srcLoc :: SrcLoc
srcLoc  = FastString -> Int -> Int -> SrcLoc
mkSrcLoc (String -> FastString
mkFastString forall a b. (a -> b) -> a -> b
$ ModSummary -> String
ms_hspp_file ModSummary
summary) Int
1 Int
1
            let warning :: Warning
warning = SrcSpan -> Doc -> Warning
mkWarning (SrcLoc -> SrcLoc -> SrcSpan
mkSrcSpan SrcLoc
srcLoc SrcLoc
srcLoc) Doc
msg
            forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Logger -> DynFlags -> Warning -> IO ()
printWarning Logger
logger DynFlags
dynFlags Warning
warning
            forall (f :: * -> *) a. Applicative f => a -> f a
pure TcGblEnv
gblEnv
          else do
            Either LiquidCheckException TcGblEnv
newGblEnv <- ModSummary
-> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook ModSummary
summary TcGblEnv
gblEnv
            case Either LiquidCheckException TcGblEnv
newGblEnv of
              -- Exit with success if all expected errors were found
              Left (ErrorsOccurred []) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TcGblEnv
gblEnv
              -- Exit with error if there were unmatched expected errors
              Left (ErrorsOccurred [Filter]
errorFilters) -> do
                String -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
defaultFilterReporter (ModSummary -> String
LH.modSummaryHsFile ModSummary
summary) [Filter]
errorFilters
                forall env a. IOEnv env a
failM
              Right TcGblEnv
newGblEnv' ->
                forall (f :: * -> *) a. Applicative f => a -> f a
pure TcGblEnv
newGblEnv'

--------------------------------------------------------------------------------
-- | GHC Configuration & Setup -------------------------------------------------
--------------------------------------------------------------------------------

-- | Overrides the default 'DynFlags' options. Specifically, we need the GHC
-- lexer not to throw away block comments, as this is where the LH spec comments
-- would live. This is why we set the 'Opt_KeepRawTokenStream' option.
customDynFlags :: [CommandLineOption] -> HscEnv -> IO HscEnv
customDynFlags :: [String] -> HscEnv -> IO HscEnv
customDynFlags [String]
opts HscEnv
hscEnv = do
  Config
cfg <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [String] -> IO Config
LH.getOpts [String]
opts
  forall a. IORef a -> a -> IO ()
writeIORef IORef Config
cfgRef Config
cfg
  forall (m :: * -> *) a. Monad m => a -> m a
return (HscEnv
hscEnv { hsc_dflags :: DynFlags
hsc_dflags = DynFlags -> DynFlags
configureDynFlags (HscEnv -> DynFlags
hsc_dflags HscEnv
hscEnv) })
  where
    configureDynFlags :: DynFlags -> DynFlags
    configureDynFlags :: DynFlags -> DynFlags
configureDynFlags DynFlags
df =
      DynFlags
df DynFlags -> GeneralFlag -> DynFlags
`gopt_set` GeneralFlag
Opt_ImplicitImportQualified
         DynFlags -> GeneralFlag -> DynFlags
`gopt_set` GeneralFlag
Opt_PIC
         DynFlags -> GeneralFlag -> DynFlags
`gopt_set` GeneralFlag
Opt_DeferTypedHoles
         DynFlags -> GeneralFlag -> DynFlags
`gopt_set` GeneralFlag
Opt_KeepRawTokenStream
         DynFlags -> Extension -> DynFlags
`xopt_set` Extension
MagicHash
         DynFlags -> Extension -> DynFlags
`xopt_set` Extension
DeriveGeneric
         DynFlags -> Extension -> DynFlags
`xopt_set` Extension
StandaloneDeriving

--------------------------------------------------------------------------------
-- | \"Unoptimising\" things ----------------------------------------------------
--------------------------------------------------------------------------------

-- | LiquidHaskell requires the unoptimised core binds in order to work correctly, but at the same time the
-- user can invoke GHC with /any/ optimisation flag turned out. This is why we grab the core binds by
-- desugaring the module during /parsing/ (before that's already too late) and we cache the core binds for
-- the rest of the program execution.
class Unoptimise a where
  type UnoptimisedTarget a :: Type
  unoptimise :: a -> UnoptimisedTarget a

instance Unoptimise DynFlags where
  type UnoptimisedTarget DynFlags = DynFlags
  unoptimise :: DynFlags -> UnoptimisedTarget DynFlags
unoptimise DynFlags
df = Int -> DynFlags -> DynFlags
updOptLevel Int
0 DynFlags
df
    { debugLevel :: Int
debugLevel   = Int
1
    , ghcLink :: GhcLink
ghcLink      = GhcLink
LinkInMemory
    , backend :: Backend
backend      = Backend
Interpreter
    , ghcMode :: GhcMode
ghcMode      = GhcMode
CompManager
    }

instance Unoptimise ModSummary where
  type UnoptimisedTarget ModSummary = ModSummary
  unoptimise :: ModSummary -> UnoptimisedTarget ModSummary
unoptimise ModSummary
modSummary = ModSummary
modSummary { ms_hspp_opts :: DynFlags
ms_hspp_opts = forall a. Unoptimise a => a -> UnoptimisedTarget a
unoptimise (ModSummary -> DynFlags
ms_hspp_opts ModSummary
modSummary) }

instance Unoptimise (DynFlags, HscEnv) where
  type UnoptimisedTarget (DynFlags, HscEnv) = HscEnv
  unoptimise :: (DynFlags, HscEnv) -> UnoptimisedTarget (DynFlags, HscEnv)
unoptimise (forall a. Unoptimise a => a -> UnoptimisedTarget a
unoptimise -> UnoptimisedTarget DynFlags
df, HscEnv
env) = HscEnv
env { hsc_dflags :: DynFlags
hsc_dflags = UnoptimisedTarget DynFlags
df }

--------------------------------------------------------------------------------
-- | Typechecking phase --------------------------------------------------------
--------------------------------------------------------------------------------

-- | We hook at this stage of the pipeline in order to call \"liquidhaskell\". This
-- might seems counterintuitive as LH works on a desugared module. However, there
-- are a bunch of reasons why we do this:
--
-- 1. Tools like \"ghcide\" works by running the compilation pipeline up until
--    this stage, which means that we won't be able to report errors and warnings
--    if we call /LH/ any later than here;
--
-- 2. Although /LH/ works on \"Core\", it requires the _unoptimised_ \"Core\" that we
--    grab from parsing (again) the module by using the GHC API, so we are really
--    independent from the \"normal\" compilation pipeline.
--
typecheckHook :: ModSummary -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook :: ModSummary
-> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook (forall a. Unoptimise a => a -> UnoptimisedTarget a
unoptimise -> UnoptimisedTarget ModSummary
modSummary) TcGblEnv
tcGblEnv = do
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"We are in module: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (Module -> StableModule
toStableModule Module
thisModule)

  HscEnv
env             <- forall gbl lcl. Env gbl lcl -> HscEnv
env_top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall env. IOEnv env env
getEnv
  ParsedModule
parsed          <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ModSummary -> IO ParsedModule
parseModuleIO HscEnv
env (ModSummary -> ModSummary
LH.keepRawTokenStream UnoptimisedTarget ModSummary
modSummary)
  let comments :: [(Maybe RealSrcLoc, String)]
comments    = ParsedModule -> [(Maybe RealSrcLoc, String)]
LH.extractSpecComments ParsedModule
parsed
  -- The LH plugin itself calls the type checker (see following line). This
  -- would lead to a loop if we didn't remove the plugin when calling the type
  -- checker.
  TypecheckedModuleLH
typechecked     <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ParsedModule -> IO TypecheckedModuleLH
typecheckModuleIO (HscEnv -> HscEnv
dropPlugins HscEnv
env) (ParsedModule -> ParsedModule
LH.ignoreInline ParsedModule
parsed)
  [(Name, Maybe TyThing)]
resolvedNames   <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ModSummary -> TcGblEnv -> IO [(Name, Maybe TyThing)]
LH.lookupTyThings HscEnv
env UnoptimisedTarget ModSummary
modSummary TcGblEnv
tcGblEnv
  [TyCon]
availTyCons     <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [TyCon]
LH.availableTyCons HscEnv
env UnoptimisedTarget ModSummary
modSummary TcGblEnv
tcGblEnv (TcGblEnv -> [AvailInfo]
tcg_exports TcGblEnv
tcGblEnv)
  [Id]
availVars       <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ModSummary -> TcGblEnv -> [AvailInfo] -> IO [Id]
LH.availableVars HscEnv
env UnoptimisedTarget ModSummary
modSummary TcGblEnv
tcGblEnv (TcGblEnv -> [AvailInfo]
tcg_exports TcGblEnv
tcGblEnv)

  ModGuts
unoptimisedGuts <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ModSummary -> TypecheckedModuleLH -> IO ModGuts
desugarModuleIO HscEnv
env UnoptimisedTarget ModSummary
modSummary TypecheckedModuleLH
typechecked

  let tcData :: TcData
tcData = [LImportDecl GhcRn]
-> [(Name, Maybe TyThing)] -> [TyCon] -> [Id] -> TcData
mkTcData (TcGblEnv -> [LImportDecl GhcRn]
tcg_rn_imports TcGblEnv
tcGblEnv) [(Name, Maybe TyThing)]
resolvedNames [TyCon]
availTyCons [Id]
availVars
  let pipelineData :: PipelineData
pipelineData = ModGuts -> TcData -> [SpecComment] -> PipelineData
PipelineData ModGuts
unoptimisedGuts TcData
tcData (forall a b. (a -> b) -> [a] -> [b]
map (Maybe RealSrcLoc, String) -> SpecComment
mkSpecComment [(Maybe RealSrcLoc, String)]
comments)

  PipelineData
-> ModSummary
-> TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
liquidHaskellCheck PipelineData
pipelineData UnoptimisedTarget ModSummary
modSummary TcGblEnv
tcGblEnv

  where
    thisModule :: Module
    thisModule :: Module
thisModule = TcGblEnv -> Module
tcg_mod TcGblEnv
tcGblEnv

    dropPlugins :: HscEnv -> HscEnv
dropPlugins HscEnv
hsc_env = HscEnv
hsc_env { hsc_plugins :: [LoadedPlugin]
hsc_plugins = [], hsc_static_plugins :: [StaticPlugin]
hsc_static_plugins = [] }

serialiseSpec :: Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv
serialiseSpec :: Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv
serialiseSpec Module
thisModule TcGblEnv
tcGblEnv LiquidLib
liquidLib = do
  -- ---
  -- -- CAN WE 'IGNORE' THE BELOW? TODO:IGNORE -- issue use `emptyLiquidLib` instead of pmrClientLib
  -- ProcessModuleResult{..} <- processModule lhContext

  -- liftIO $ putStrLn "liquidHaskellCheck 7"

  -- -- Call into the existing Liquid interface
  -- out <- liftIO $ LH.checkTargetInfo pmrTargetInfo

  -- liftIO $ putStrLn "liquidHaskellCheck 8"

  -- -- Report the outcome of the checking
  -- LH.reportResult errorLogger cfg [giTarget (giSrc pmrTargetInfo)] out
  -- case o_result out of
  --   Safe _stats -> pure ()
  --   _           -> failM

  -- liftIO $ putStrLn "liquidHaskellCheck 9"
  -- ---

  let serialisedSpec :: Annotation
serialisedSpec = LiquidLib -> Module -> Annotation
Util.serialiseLiquidLib LiquidLib
liquidLib Module
thisModule
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"Serialised annotation ==> " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ Annotation
serialisedSpec)

  -- liftIO $ putStrLn "liquidHaskellCheck 10"

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TcGblEnv
tcGblEnv { tcg_anns :: [Annotation]
tcg_anns = Annotation
serialisedSpec forall a. a -> [a] -> [a]
: TcGblEnv -> [Annotation]
tcg_anns TcGblEnv
tcGblEnv }

processInputSpec :: Config -> PipelineData -> ModSummary -> TcGblEnv -> BareSpec -> TcM (Either LiquidCheckException TcGblEnv)
processInputSpec :: Config
-> PipelineData
-> ModSummary
-> TcGblEnv
-> BareSpec
-> TcM (Either LiquidCheckException TcGblEnv)
processInputSpec Config
cfg PipelineData
pipelineData ModSummary
modSummary TcGblEnv
tcGblEnv BareSpec
inputSpec = do
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
" Input spec: \n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BareSpec
inputSpec
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"Relevant ===> \n" forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines (Module -> String
renderModule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Set a -> [a]
S.toList (ModGuts -> Set Module
relevantModules ModGuts
modGuts))

  LogicMap
logicMap :: LogicMap <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO LogicMap
LH.makeLogicMap

  -- debugLog $ "Logic map:\n" ++ show logicMap

  let lhContext :: LiquidHaskellContext
lhContext = LiquidHaskellContext {
        lhGlobalCfg :: Config
lhGlobalCfg       = Config
cfg
      , lhInputSpec :: BareSpec
lhInputSpec       = BareSpec
inputSpec
      , lhModuleLogicMap :: LogicMap
lhModuleLogicMap  = LogicMap
logicMap
      , lhModuleSummary :: ModSummary
lhModuleSummary   = ModSummary
modSummary
      , lhModuleTcData :: TcData
lhModuleTcData    = PipelineData -> TcData
pdTcData PipelineData
pipelineData
      , lhModuleGuts :: ModGuts
lhModuleGuts      = PipelineData -> ModGuts
pdUnoptimisedCore PipelineData
pipelineData
      , lhRelevantModules :: Set Module
lhRelevantModules = ModGuts -> Set Module
relevantModules ModGuts
modGuts
      }

  -- liftIO $ putStrLn ("liquidHaskellCheck 6: " ++ show isIg)
  if BareSpec -> Bool
isIgnore BareSpec
inputSpec
    then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Filter] -> LiquidCheckException
ErrorsOccurred [])
    else do
      Either LiquidCheckException LiquidLib
liquidLib' <- LiquidHaskellContext -> TcM (Either LiquidCheckException LiquidLib)
checkLiquidHaskellContext LiquidHaskellContext
lhContext
      forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Module -> TcGblEnv -> LiquidLib -> TcM TcGblEnv
serialiseSpec Module
thisModule TcGblEnv
tcGblEnv) Either LiquidCheckException LiquidLib
liquidLib'

  where
    thisModule :: Module
    thisModule :: Module
thisModule = TcGblEnv -> Module
tcg_mod TcGblEnv
tcGblEnv

    modGuts :: ModGuts
    modGuts :: ModGuts
modGuts = PipelineData -> ModGuts
pdUnoptimisedCore PipelineData
pipelineData

liquidHaskellCheckWithConfig :: Config -> PipelineData -> ModSummary -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv)
liquidHaskellCheckWithConfig :: Config
-> PipelineData
-> ModSummary
-> TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
liquidHaskellCheckWithConfig Config
globalCfg PipelineData
pipelineData ModSummary
modSummary TcGblEnv
tcGblEnv = do
  -- The 'specQuotes' contain stuff we need from imported modules, extracted
  -- from the annotations in their interface files.
  let specQuotes :: [BPspec]
      specQuotes :: [BPspec]
specQuotes = forall a. (a -> Module) -> (a -> [Annotation]) -> a -> [BPspec]
LH.extractSpecQuotes' TcGblEnv -> Module
tcg_mod TcGblEnv -> [Annotation]
tcg_anns TcGblEnv
tcGblEnv

  -- Here, we are calling Liquid Haskell's parser, acting on the unparsed
  -- spec comments stored in the pipeline data, supported by the specQuotes
  -- obtained from the imported modules.
  Either LiquidCheckException BareSpec
inputSpec' :: Either LiquidCheckException BareSpec <-
    String
-> Module
-> [SpecComment]
-> [BPspec]
-> TcM (Either LiquidCheckException BareSpec)
getLiquidSpec String
thisFile Module
thisModule (PipelineData -> [SpecComment]
pdSpecComments PipelineData
pipelineData) [BPspec]
specQuotes

  case Either LiquidCheckException BareSpec
inputSpec' of
    Left LiquidCheckException
e -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left LiquidCheckException
e
    Right BareSpec
inputSpec ->
      forall (m :: * -> *) a.
MonadIO m =>
Config -> String -> [Located String] -> (Config -> m a) -> m a
withPragmas Config
globalCfg String
thisFile (forall ty bndr. Spec ty bndr -> [Located String]
Ms.pragmas forall a b. (a -> b) -> a -> b
$ BareSpec -> Spec LocBareType LocSymbol
fromBareSpec BareSpec
inputSpec) forall a b. (a -> b) -> a -> b
$ \Config
moduleCfg -> do
        Config
-> PipelineData
-> ModSummary
-> TcGblEnv
-> BareSpec
-> TcM (Either LiquidCheckException TcGblEnv)
processInputSpec Config
moduleCfg PipelineData
pipelineData ModSummary
modSummary TcGblEnv
tcGblEnv BareSpec
inputSpec
          forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\(UserError
e :: UserError) -> forall e.
(Show e, PPrint e) =>
Config -> [TError e] -> TcM (Either LiquidCheckException TcGblEnv)
reportErrs Config
moduleCfg [UserError
e])
          forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\(Error
e :: Error) -> forall e.
(Show e, PPrint e) =>
Config -> [TError e] -> TcM (Either LiquidCheckException TcGblEnv)
reportErrs Config
moduleCfg [Error
e])
          forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\([Error]
es :: [Error]) -> forall e.
(Show e, PPrint e) =>
Config -> [TError e] -> TcM (Either LiquidCheckException TcGblEnv)
reportErrs Config
moduleCfg [Error]
es)

  where
    thisFile :: FilePath
    thisFile :: String
thisFile = ModSummary -> String
LH.modSummaryHsFile ModSummary
modSummary

    continue :: TcM (Either LiquidCheckException TcGblEnv)
    continue :: TcM (Either LiquidCheckException TcGblEnv)
continue = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Filter] -> LiquidCheckException
ErrorsOccurred [])

    reportErrs :: (Show e, F.PPrint e) => Config -> [TError e] -> TcM (Either LiquidCheckException TcGblEnv)
    reportErrs :: forall e.
(Show e, PPrint e) =>
Config -> [TError e] -> TcM (Either LiquidCheckException TcGblEnv)
reportErrs Config
cfg = forall e' a.
(Show e', PPrint e') =>
String
-> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a
LH.filterReportErrors String
thisFile forall env a. IOEnv env a
GHC.failM TcM (Either LiquidCheckException TcGblEnv)
continue (Config -> [Filter]
getFilters Config
cfg) Tidy
Full

    thisModule :: Module
    thisModule :: Module
thisModule = TcGblEnv -> Module
tcg_mod TcGblEnv
tcGblEnv

-- | Partially calls into LiquidHaskell's GHC API.
liquidHaskellCheck :: PipelineData -> ModSummary -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv)
liquidHaskellCheck :: PipelineData
-> ModSummary
-> TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
liquidHaskellCheck PipelineData
pipelineData ModSummary
modSummary TcGblEnv
tcGblEnv = do
  Config
cfg <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Config
getConfig
  Config
-> PipelineData
-> ModSummary
-> TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
liquidHaskellCheckWithConfig Config
cfg PipelineData
pipelineData ModSummary
modSummary TcGblEnv
tcGblEnv

checkLiquidHaskellContext :: LiquidHaskellContext -> TcM (Either LiquidCheckException LiquidLib)
checkLiquidHaskellContext :: LiquidHaskellContext -> TcM (Either LiquidCheckException LiquidLib)
checkLiquidHaskellContext LiquidHaskellContext
lhContext = do
  Either LiquidCheckException ProcessModuleResult
pmr <- LiquidHaskellContext
-> TcM (Either LiquidCheckException ProcessModuleResult)
processModule LiquidHaskellContext
lhContext
  case Either LiquidCheckException ProcessModuleResult
pmr of
    Left LiquidCheckException
e -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left LiquidCheckException
e
    Right ProcessModuleResult{TargetInfo
LiquidLib
pmrTargetInfo :: ProcessModuleResult -> TargetInfo
pmrClientLib :: ProcessModuleResult -> LiquidLib
pmrTargetInfo :: TargetInfo
pmrClientLib :: LiquidLib
..} -> do
      -- Call into the existing Liquid interface
      Output Doc
out <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ TargetInfo -> IO (Output Doc)
LH.checkTargetInfo TargetInfo
pmrTargetInfo

      let bareSpec :: BareSpec
bareSpec = LiquidHaskellContext -> BareSpec
lhInputSpec LiquidHaskellContext
lhContext
          file :: String
file = ModSummary -> String
LH.modSummaryHsFile forall a b. (a -> b) -> a -> b
$ LiquidHaskellContext -> ModSummary
lhModuleSummary LiquidHaskellContext
lhContext

      forall (m :: * -> *) a.
MonadIO m =>
Config -> String -> [Located String] -> (Config -> m a) -> m a
withPragmas (LiquidHaskellContext -> Config
lhGlobalCfg LiquidHaskellContext
lhContext) String
file (forall ty bndr. Spec ty bndr -> [Located String]
Ms.pragmas forall a b. (a -> b) -> a -> b
$ BareSpec -> Spec LocBareType LocSymbol
fromBareSpec BareSpec
bareSpec) forall a b. (a -> b) -> a -> b
$ \Config
moduleCfg ->  do
        let filters :: [Filter]
filters = Config -> [Filter]
getFilters Config
moduleCfg
        -- Report the outcome of the checking
        forall (m :: * -> *).
MonadIO m =>
(OutputResult -> m ()) -> Config -> [String] -> Output Doc -> m ()
LH.reportResult (String
-> [Filter] -> OutputResult -> IOEnv (Env TcGblEnv TcLclEnv) ()
errorLogger String
file [Filter]
filters) Config
moduleCfg [TargetSrc -> String
giTarget (TargetInfo -> TargetSrc
giSrc TargetInfo
pmrTargetInfo)] Output Doc
out
        -- If there are unmatched filters or errors, and we are not reporting with
        -- json, we don't make it to this part of the code because errorLogger
        -- will throw an exception.
        --
        -- F.Crash is also handled by reportResult and errorLogger
        case forall a. Output a -> ErrorResult
o_result Output Doc
out of
          F.Safe Stats
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right LiquidLib
pmrClientLib
          ErrorResult
_ | Config -> Bool
json Config
moduleCfg -> forall env a. IOEnv env a
failM
            | Bool
otherwise -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ [Filter] -> LiquidCheckException
ErrorsOccurred []

errorLogger :: FilePath -> [Filter] -> OutputResult -> TcM ()
errorLogger :: String
-> [Filter] -> OutputResult -> IOEnv (Env TcGblEnv TcLclEnv) ()
errorLogger String
file [Filter]
filters OutputResult
outputResult = do
  forall (m :: * -> *) filter msg e a.
(Monad m, Ord filter) =>
FilterReportErrorsArgs m filter msg e a -> [e] -> m a
LH.filterReportErrorsWith
    FilterReportErrorsArgs { msgReporter :: [MsgEnvelope DecoratedSDoc] -> IOEnv (Env TcGblEnv TcLclEnv) ()
msgReporter = [MsgEnvelope DecoratedSDoc] -> IOEnv (Env TcGblEnv TcLclEnv) ()
GHC.reportErrors
                           , filterReporter :: [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
filterReporter = String -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
LH.defaultFilterReporter String
file
                           , failure :: IOEnv (Env TcGblEnv TcLclEnv) ()
failure = forall env a. IOEnv env a
GHC.failM
                           , continue :: IOEnv (Env TcGblEnv TcLclEnv) ()
continue = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                           , pprinter :: (SrcSpan, Doc)
-> IOEnv (Env TcGblEnv TcLclEnv) (MsgEnvelope DecoratedSDoc)
pprinter = \(SrcSpan
spn, Doc
e) -> SrcSpan
-> SDoc
-> SDoc
-> IOEnv (Env TcGblEnv TcLclEnv) (MsgEnvelope DecoratedSDoc)
mkLongErrAt SrcSpan
spn (Doc -> SDoc
LH.fromPJDoc Doc
e) SDoc
O.empty
                           , matchingFilters :: (SrcSpan, Doc) -> [Filter]
matchingFilters = forall e. (e -> String) -> [Filter] -> e -> [Filter]
LH.reduceFilters (\(SrcSpan
src, Doc
doc) -> Doc -> String
PJ.render Doc
doc forall a. [a] -> [a] -> [a]
++ String
" at " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> String
LH.showPpr SrcSpan
src) [Filter]
filters
                           , filters :: [Filter]
filters = [Filter]
filters
                           }
    (OutputResult -> [(SrcSpan, Doc)]
LH.orMessages OutputResult
outputResult)

isIgnore :: BareSpec -> Bool
isIgnore :: BareSpec -> Bool
isIgnore (MkBareSpec Spec LocBareType LocSymbol
sp) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((forall a. Eq a => a -> a -> Bool
== String
"--skip-module") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
F.val) (forall ty bndr. Spec ty bndr -> [Located String]
pragmas Spec LocBareType LocSymbol
sp)

--------------------------------------------------------------------------------
-- | Working with bare & lifted specs ------------------------------------------
--------------------------------------------------------------------------------

loadDependencies :: Config
                 -- ^ The 'Config' associated to the /current/ module being compiled.
                 -> Module
                 -> [Module]
                 -> TcM TargetDependencies
loadDependencies :: Config -> Module -> [Module] -> TcM TargetDependencies
loadDependencies Config
currentModuleConfig Module
thisModule [Module]
mods = do
  HscEnv
hscEnv    <- forall gbl lcl. Env gbl lcl -> HscEnv
env_top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall env. IOEnv env env
getEnv
  [SpecFinderResult]
results   <- [String] -> HscEnv -> [Module] -> TcM [SpecFinderResult]
SpecFinder.findRelevantSpecs
                 (Config -> [String]
excludeAutomaticAssumptionsFor Config
currentModuleConfig) HscEnv
hscEnv [Module]
mods
  TargetDependencies
deps      <- forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM TargetDependencies -> SpecFinderResult -> TcM TargetDependencies
processResult forall a. Monoid a => a
mempty (forall a. [a] -> [a]
reverse [SpecFinderResult]
results)
  [StableModule]
redundant <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> Config -> IO [StableModule]
configToRedundantDependencies HscEnv
hscEnv Config
currentModuleConfig

  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"Redundant dependencies ==> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [StableModule]
redundant

  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip StableModule -> TargetDependencies -> TargetDependencies
dropDependency) TargetDependencies
deps [StableModule]
redundant
  where
    processResult :: TargetDependencies -> SpecFinderResult -> TcM TargetDependencies
    processResult :: TargetDependencies -> SpecFinderResult -> TcM TargetDependencies
processResult !TargetDependencies
acc (SpecNotFound Module
mdl) = do
      forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"[T:" forall a. [a] -> [a] -> [a]
++ Module -> String
renderModule Module
thisModule
              forall a. [a] -> [a] -> [a]
++ String
"] Spec not found for " forall a. [a] -> [a] -> [a]
++ Module -> String
renderModule Module
mdl
      forall (f :: * -> *) a. Applicative f => a -> f a
pure TargetDependencies
acc
    processResult TargetDependencies
_ (SpecFound Module
originalModule SearchLocation
location BareSpec
_) = do
      DynFlags
dynFlags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
      forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"[T:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall unit. GenModule unit -> ModuleName
moduleName Module
thisModule)
              forall a. [a] -> [a] -> [a]
++ String
"] Spec found for " forall a. [a] -> [a] -> [a]
++ Module -> String
renderModule Module
originalModule forall a. [a] -> [a] -> [a]
++ String
", at location " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SearchLocation
location
      forall (m :: * -> *) a. MonadIO m => String -> m a
Util.pluginAbort (DynFlags -> SDoc -> String
O.showSDoc DynFlags
dynFlags forall a b. (a -> b) -> a -> b
$ String -> SDoc
O.text String
"A BareSpec was returned as a dependency, this is not allowed, in " SDoc -> SDoc -> SDoc
O.<+> forall a. Outputable a => a -> SDoc
O.ppr Module
thisModule)
    processResult !TargetDependencies
acc (LibFound Module
originalModule SearchLocation
location LiquidLib
lib) = do
      forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"[T:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall unit. GenModule unit -> ModuleName
moduleName Module
thisModule)
              forall a. [a] -> [a] -> [a]
++ String
"] Lib found for " forall a. [a] -> [a] -> [a]
++ Module -> String
renderModule Module
originalModule forall a. [a] -> [a] -> [a]
++ String
", at location " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SearchLocation
location
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ TargetDependencies {
          getDependencies :: HashMap StableModule LiftedSpec
getDependencies = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HM.insert (Module -> StableModule
toStableModule Module
originalModule) (LiquidLib -> LiftedSpec
libTarget LiquidLib
lib) (TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies forall a b. (a -> b) -> a -> b
$ TargetDependencies
acc forall a. Semigroup a => a -> a -> a
<> LiquidLib -> TargetDependencies
libDeps LiquidLib
lib)
        }

data LiquidHaskellContext = LiquidHaskellContext {
    LiquidHaskellContext -> Config
lhGlobalCfg        :: Config
  , LiquidHaskellContext -> BareSpec
lhInputSpec        :: BareSpec
  , LiquidHaskellContext -> LogicMap
lhModuleLogicMap   :: LogicMap
  , LiquidHaskellContext -> ModSummary
lhModuleSummary    :: ModSummary
  , LiquidHaskellContext -> TcData
lhModuleTcData     :: TcData
  , LiquidHaskellContext -> ModGuts
lhModuleGuts       :: ModGuts
  , LiquidHaskellContext -> Set Module
lhRelevantModules  :: Set Module
  }

--------------------------------------------------------------------------------
-- | Per-Module Pipeline -------------------------------------------------------
--------------------------------------------------------------------------------

data ProcessModuleResult = ProcessModuleResult {
    ProcessModuleResult -> LiquidLib
pmrClientLib  :: LiquidLib
  -- ^ The \"client library\" we will serialise on disk into an interface's 'Annotation'.
  , ProcessModuleResult -> TargetInfo
pmrTargetInfo :: TargetInfo
  -- ^ The 'GhcInfo' for the current 'Module' that LiquidHaskell will process.
  }

-- | Parse the spec comments from one module, supported by the
-- spec quotes from the imported module. Also looks for
-- "companion specs" for the current module and merges them in
-- if it finds one.
getLiquidSpec :: FilePath -> Module -> [SpecComment] -> [BPspec] -> TcM (Either LiquidCheckException BareSpec)
getLiquidSpec :: String
-> Module
-> [SpecComment]
-> [BPspec]
-> TcM (Either LiquidCheckException BareSpec)
getLiquidSpec String
thisFile Module
thisModule [SpecComment]
specComments [BPspec]
specQuotes = do
  Config
globalCfg <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO Config
getConfig
  let commSpecE :: Either [Error] (ModName, Spec LocBareType LocSymbol)
      commSpecE :: Either [Error] (ModName, Spec LocBareType LocSymbol)
commSpecE = ModuleName
-> [(SourcePos, String)]
-> [BPspec]
-> Either [Error] (ModName, Spec LocBareType LocSymbol)
hsSpecificationP (forall unit. GenModule unit -> ModuleName
moduleName Module
thisModule) (coerce :: forall a b. Coercible a b => a -> b
coerce [SpecComment]
specComments) [BPspec]
specQuotes
  case Either [Error] (ModName, Spec LocBareType LocSymbol)
commSpecE of
    Left [Error]
errors ->
      forall e' a.
(Show e', PPrint e') =>
String
-> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a
LH.filterReportErrors String
thisFile forall env a. IOEnv env a
GHC.failM forall {b}.
IOEnv (Env TcGblEnv TcLclEnv) (Either LiquidCheckException b)
continue (Config -> [Filter]
getFilters Config
globalCfg) Tidy
Full [Error]
errors
    Right (Spec LocBareType LocSymbol -> BareSpec
toBareSpec forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd -> BareSpec
commSpec) -> do
      HscEnv
env    <- forall gbl lcl. Env gbl lcl -> HscEnv
env_top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall env. IOEnv env env
getEnv
      SpecFinderResult
res <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> Module -> IO SpecFinderResult
SpecFinder.findCompanionSpec HscEnv
env Module
thisModule
      case SpecFinderResult
res of
        SpecFound Module
_ SearchLocation
_ BareSpec
companionSpec -> do
          forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"Companion spec found for " forall a. [a] -> [a] -> [a]
++ Module -> String
renderModule Module
thisModule
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ BareSpec
commSpec forall a. Semigroup a => a -> a -> a
<> BareSpec
companionSpec
        SpecFinderResult
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right BareSpec
commSpec
  where
    continue :: IOEnv (Env TcGblEnv TcLclEnv) (Either LiquidCheckException b)
continue = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Filter] -> LiquidCheckException
ErrorsOccurred [])

processModule :: LiquidHaskellContext -> TcM (Either LiquidCheckException ProcessModuleResult)
processModule :: LiquidHaskellContext
-> TcM (Either LiquidCheckException ProcessModuleResult)
processModule LiquidHaskellContext{Set Module
ModGuts
ModSummary
Config
LogicMap
BareSpec
TcData
lhRelevantModules :: Set Module
lhModuleGuts :: ModGuts
lhModuleTcData :: TcData
lhModuleSummary :: ModSummary
lhModuleLogicMap :: LogicMap
lhInputSpec :: BareSpec
lhGlobalCfg :: Config
lhRelevantModules :: LiquidHaskellContext -> Set Module
lhModuleGuts :: LiquidHaskellContext -> ModGuts
lhModuleTcData :: LiquidHaskellContext -> TcData
lhModuleSummary :: LiquidHaskellContext -> ModSummary
lhModuleLogicMap :: LiquidHaskellContext -> LogicMap
lhInputSpec :: LiquidHaskellContext -> BareSpec
lhGlobalCfg :: LiquidHaskellContext -> Config
..} = do
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog (String
"Module ==> " forall a. [a] -> [a] -> [a]
++ Module -> String
renderModule Module
thisModule)
  HscEnv
hscEnv              <- forall gbl lcl. Env gbl lcl -> HscEnv
env_top forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall env. IOEnv env env
getEnv

  let bareSpec :: BareSpec
bareSpec        = BareSpec
lhInputSpec
  -- /NOTE/: For the Plugin to work correctly, we shouldn't call 'canonicalizePath', because otherwise
  -- this won't trigger the \"external name resolution\" as part of 'Language.Haskell.Liquid.Bare.Resolve'
  -- (cfr. 'allowExtResolution').
  let file :: String
file            = ModSummary -> String
LH.modSummaryHsFile ModSummary
lhModuleSummary

  ()
_                   <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Located String] -> IO ()
LH.checkFilePragmas forall a b. (a -> b) -> a -> b
$ forall ty bndr. Spec ty bndr -> [Located String]
Ms.pragmas (BareSpec -> Spec LocBareType LocSymbol
fromBareSpec BareSpec
bareSpec)

  forall (m :: * -> *) a.
MonadIO m =>
Config -> String -> [Located String] -> (Config -> m a) -> m a
withPragmas Config
lhGlobalCfg String
file (forall ty bndr. Spec ty bndr -> [Located String]
Ms.pragmas forall a b. (a -> b) -> a -> b
$ BareSpec -> Spec LocBareType LocSymbol
fromBareSpec BareSpec
bareSpec) forall a b. (a -> b) -> a -> b
$ \Config
moduleCfg -> do
    TargetDependencies
dependencies       <- Config -> Module -> [Module] -> TcM TargetDependencies
loadDependencies Config
moduleCfg
                                           Module
thisModule
                                           (forall a. Set a -> [a]
S.toList Set Module
lhRelevantModules)

    forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"Found " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall k v. HashMap k v -> Int
HM.size forall a b. (a -> b) -> a -> b
$ TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies TargetDependencies
dependencies) forall a. Semigroup a => a -> a -> a
<> String
" dependencies:"
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debugLogs forall a b. (a -> b) -> a -> b
$
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k v. HashMap k v -> [k]
HM.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies forall a b. (a -> b) -> a -> b
$ TargetDependencies
dependencies) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall b c a. (b -> c) -> (a -> b) -> a -> c
. Module -> String
moduleStableString forall b c a. (b -> c) -> (a -> b) -> a -> c
. StableModule -> Module
unStableModule

    forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"mg_exports => " forall a. [a] -> [a] -> [a]
++ SDoc -> String
O.showSDocUnsafe (forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ ModGuts -> [AvailInfo]
mg_exports ModGuts
modGuts)
    forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"mg_tcs => " forall a. [a] -> [a] -> [a]
++ SDoc -> String
O.showSDocUnsafe (forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ ModGuts -> [TyCon]
mg_tcs ModGuts
modGuts)

    TargetSrc
targetSrc  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Config -> String -> TcData -> ModGuts -> HscEnv -> IO TargetSrc
makeTargetSrc Config
moduleCfg String
file TcData
lhModuleTcData ModGuts
modGuts HscEnv
hscEnv
    Logger
logger <- forall (m :: * -> *). HasLogger m => m Logger
getLogger
    DynFlags
dynFlags <- forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags

    -- See https://github.com/ucsd-progsys/liquidhaskell/issues/1711
    -- Due to the fact the internals can throw exceptions from pure code at any point, we need to
    -- call 'evaluate' to force any exception and catch it, if we can.


    Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
result <-
      Config
-> LogicMap
-> TargetSrc
-> BareSpec
-> TargetDependencies
-> TcRn (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec Config
moduleCfg LogicMap
lhModuleLogicMap TargetSrc
targetSrc BareSpec
bareSpec TargetDependencies
dependencies

    let continue :: IOEnv (Env TcGblEnv TcLclEnv) (Either LiquidCheckException b)
continue = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left ([Filter] -> LiquidCheckException
ErrorsOccurred [])
        reportErrs :: (Show e, F.PPrint e) => [TError e] -> TcRn (Either LiquidCheckException ProcessModuleResult)
        reportErrs :: forall e.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException ProcessModuleResult)
reportErrs = forall e' a.
(Show e', PPrint e') =>
String
-> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a
LH.filterReportErrors String
file forall env a. IOEnv env a
GHC.failM forall {b}.
IOEnv (Env TcGblEnv TcLclEnv) (Either LiquidCheckException b)
continue (Config -> [Filter]
getFilters Config
moduleCfg) Tidy
Full

    (case Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
result of
      -- Print warnings and errors, aborting the compilation.
      Left Diagnostics
diagnostics -> do
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Logger -> DynFlags -> Warning -> IO ()
printWarning Logger
logger DynFlags
dynFlags)    (Diagnostics -> [Warning]
allWarnings Diagnostics
diagnostics)
        forall e.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException ProcessModuleResult)
reportErrs forall a b. (a -> b) -> a -> b
$ Diagnostics -> [Error]
allErrors Diagnostics
diagnostics
      Right ([Warning]
warnings, TargetSpec
targetSpec, LiftedSpec
liftedSpec) -> do
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Logger -> DynFlags -> Warning -> IO ()
printWarning Logger
logger DynFlags
dynFlags) [Warning]
warnings
        let targetInfo :: TargetInfo
targetInfo = TargetSrc -> TargetSpec -> TargetInfo
TargetInfo TargetSrc
targetSrc TargetSpec
targetSpec

        forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"bareSpec ==> "   forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show BareSpec
bareSpec
        forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"liftedSpec ==> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LiftedSpec
liftedSpec

        let clientLib :: LiquidLib
clientLib  = LiftedSpec -> LiquidLib
mkLiquidLib LiftedSpec
liftedSpec forall a b. a -> (a -> b) -> b
& TargetDependencies -> LiquidLib -> LiquidLib
addLibDependencies TargetDependencies
dependencies

        let result' :: ProcessModuleResult
result' = ProcessModuleResult {
              pmrClientLib :: LiquidLib
pmrClientLib  = LiquidLib
clientLib
            , pmrTargetInfo :: TargetInfo
pmrTargetInfo = TargetInfo
targetInfo
            }

        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right ProcessModuleResult
result')
      forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\(UserError
e :: UserError) -> forall e.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException ProcessModuleResult)
reportErrs [UserError
e])
      forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\(Error
e :: Error) -> forall e.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException ProcessModuleResult)
reportErrs [Error
e])
      forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\([Error]
es :: [Error]) -> forall e.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException ProcessModuleResult)
reportErrs [Error]
es)

  where
    modGuts :: ModGuts
modGuts    = ModGuts
lhModuleGuts
    thisModule :: Module
thisModule = ModGuts -> Module
mg_module ModGuts
modGuts

makeTargetSrc :: Config
              -> FilePath
              -> TcData
              -> ModGuts
              -> HscEnv
              -> IO TargetSrc
makeTargetSrc :: Config -> String -> TcData -> ModGuts -> HscEnv -> IO TargetSrc
makeTargetSrc Config
cfg String
file TcData
tcData ModGuts
modGuts HscEnv
hscEnv = do
  [CoreBind]
coreBinds      <- Config -> HscEnv -> ModGuts -> IO [CoreBind]
anormalize Config
cfg HscEnv
hscEnv ModGuts
modGuts

  -- The type constructors for a module are the (nubbed) union of the ones defined and
  -- the ones exported. This covers the case of \"wrapper modules\" that simply re-exports
  -- everything from the imported modules.
  let availTcs :: [TyCon]
availTcs    = TcData -> [TyCon]
tcAvailableTyCons TcData
tcData
  let allTcs :: [TyCon]
allTcs      = forall a. Eq a => [a] -> [a]
L.nub (MGIModGuts -> [TyCon]
mgi_tcs MGIModGuts
mgiModGuts forall a. [a] -> [a] -> [a]
++ [TyCon]
availTcs)

  let dataCons :: [Id]
dataCons       = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a -> b) -> [a] -> [b]
map DataCon -> Id
dataConWorkId forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
tyConDataCons) [TyCon]
allTcs
  let ([TyCon]
fiTcs, [(Symbol, DataCon)]
fiDcs) = [FamInst] -> ([TyCon], [(Symbol, DataCon)])
LH.makeFamInstEnv (ModGuts -> [FamInst]
getFamInstances ModGuts
modGuts)
  let things :: [(Name, Maybe TyThing)]
things         = TcData -> [(Name, Maybe TyThing)]
tcResolvedNames TcData
tcData
  let impVars :: [Id]
impVars        = [CoreBind] -> [Id]
LH.importVars [CoreBind]
coreBinds forall a. [a] -> [a] -> [a]
++ Maybe [ClsInst] -> [Id]
LH.classCons (MGIModGuts -> Maybe [ClsInst]
mgi_cls_inst MGIModGuts
mgiModGuts)

  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"_gsTcs   => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [TyCon]
allTcs
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"_gsFiTcs => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [TyCon]
fiTcs
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"_gsFiDcs => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Symbol, DataCon)]
fiDcs
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"dataCons => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [Id]
dataCons
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"coreBinds => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ [CoreBind]
coreBinds)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"impVars => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ [Id]
impVars)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"defVars  => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ [Id]
dataCons forall a. [a] -> [a] -> [a]
++ forall a. CBVisitable a => a -> [Id]
letVars [CoreBind]
coreBinds forall a. [a] -> [a] -> [a]
++ TcData -> [Id]
tcAvailableVars TcData
tcData)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"useVars  => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ forall a. CBVisitable a => a -> [Id]
readVars [CoreBind]
coreBinds)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"derVars  => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList (Config -> MGIModGuts -> [Id]
LH.derivedVars Config
cfg MGIModGuts
mgiModGuts))
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"gsExports => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (MGIModGuts -> HashSet StableName
mgi_exports  MGIModGuts
mgiModGuts)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"gsTcs     => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ [TyCon]
allTcs)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"gsCls     => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ MGIModGuts -> Maybe [ClsInst]
mgi_cls_inst MGIModGuts
mgiModGuts)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"gsFiTcs   => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ [TyCon]
fiTcs)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"gsFiDcs   => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [(Symbol, DataCon)]
fiDcs
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"gsPrimTcs => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ [TyCon]
GHC.primTyCons)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"things   => " forall a. [a] -> [a] -> [a]
++ (SDoc -> String
O.showSDocUnsafe forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SDoc] -> SDoc
O.vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Outputable a => a -> SDoc
O.ppr forall a b. (a -> b) -> a -> b
$ [(Name, Maybe TyThing)]
things)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"allImports => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (TcData -> HashSet Symbol
tcAllImports TcData
tcData)
  forall (m :: * -> *). MonadIO m => String -> m ()
debugLog forall a b. (a -> b) -> a -> b
$ String
"qualImports => " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (TcData -> QImports
tcQualifiedImports TcData
tcData)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TargetSrc
    { giTarget :: String
giTarget    = String
file
    , giTargetMod :: ModName
giTargetMod = ModType -> ModuleName -> ModName
ModName ModType
Target (forall unit. GenModule unit -> ModuleName
moduleName (ModGuts -> Module
mg_module ModGuts
modGuts))
    , giCbs :: [CoreBind]
giCbs       = [CoreBind]
coreBinds
    , giImpVars :: [Id]
giImpVars   = [Id]
impVars
    , giDefVars :: [Id]
giDefVars   = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ [Id]
dataCons forall a. [a] -> [a] -> [a]
++ forall a. CBVisitable a => a -> [Id]
letVars [CoreBind]
coreBinds forall a. [a] -> [a] -> [a]
++ TcData -> [Id]
tcAvailableVars TcData
tcData
    , giUseVars :: [Id]
giUseVars   = forall a. CBVisitable a => a -> [Id]
readVars [CoreBind]
coreBinds
    , giDerVars :: HashSet Id
giDerVars   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList (Config -> MGIModGuts -> [Id]
LH.derivedVars Config
cfg MGIModGuts
mgiModGuts)
    , gsExports :: HashSet StableName
gsExports   = MGIModGuts -> HashSet StableName
mgi_exports  MGIModGuts
mgiModGuts
    , gsTcs :: [TyCon]
gsTcs       = [TyCon]
allTcs
    , gsCls :: Maybe [ClsInst]
gsCls       = MGIModGuts -> Maybe [ClsInst]
mgi_cls_inst MGIModGuts
mgiModGuts
    , gsFiTcs :: [TyCon]
gsFiTcs     = [TyCon]
fiTcs
    , gsFiDcs :: [(Symbol, DataCon)]
gsFiDcs     = [(Symbol, DataCon)]
fiDcs
    , gsPrimTcs :: [TyCon]
gsPrimTcs   = [TyCon]
GHC.primTyCons
    , gsQualImps :: QImports
gsQualImps  = TcData -> QImports
tcQualifiedImports TcData
tcData
    , gsAllImps :: HashSet Symbol
gsAllImps   = TcData -> HashSet Symbol
tcAllImports       TcData
tcData
    , gsTyThings :: [TyThing]
gsTyThings  = [ TyThing
t | (Name
_, Just TyThing
t) <- [(Name, Maybe TyThing)]
things ]
    }
  where
    mgiModGuts :: MGIModGuts
    mgiModGuts :: MGIModGuts
mgiModGuts = Maybe [ClsInst] -> ModGuts -> MGIModGuts
miModGuts Maybe [ClsInst]
deriv ModGuts
modGuts
      where
        deriv :: Maybe [ClsInst]
deriv   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ InstEnv -> [ClsInst]
instEnvElts forall a b. (a -> b) -> a -> b
$ ModGuts -> InstEnv
mg_inst_env ModGuts
modGuts

getFamInstances :: ModGuts -> [FamInst]
getFamInstances :: ModGuts -> [FamInst]
getFamInstances ModGuts
guts = FamInstEnv -> [FamInst]
famInstEnvElts (ModGuts -> FamInstEnv
mg_fam_inst_env ModGuts
guts)