{-# 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
newtype LiquidCheckException = ErrorsOccurred [Filter]
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)
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 #-}
debugLogs :: Bool
debugLogs :: Bool
debugLogs = Bool
False
getConfig :: IO Config
getConfig :: IO Config
getConfig = forall a. IORef a -> IO a
readIORef IORef Config
cfgRef
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)
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
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
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
Left (ErrorsOccurred []) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TcGblEnv
gblEnv
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'
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
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 }
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
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
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)
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
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
}
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
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
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
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
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
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
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)
loadDependencies :: Config
-> 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
}
data ProcessModuleResult = ProcessModuleResult {
ProcessModuleResult -> LiquidLib
pmrClientLib :: LiquidLib
, ProcessModuleResult -> TargetInfo
pmrTargetInfo :: TargetInfo
}
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
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
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
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
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)