-- | 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 OverloadedStrings          #-}
{-# LANGUAGE RecordWildCards            #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE TupleSections              #-}

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           Language.Haskell.Liquid.LHNameResolution (resolveLHNames)
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   (addTcRnUnknownMessages)

import           Language.Haskell.Liquid.GHC.Plugin.Types
import qualified Language.Haskell.Liquid.GHC.Plugin.Serialisation as Serialisation
import           Language.Haskell.Liquid.GHC.Plugin.SpecFinder
                                                         as SpecFinder

import           Language.Haskell.Liquid.GHC.Types       (MGIModGuts(..), miModGuts)
import           Language.Haskell.Liquid.Transforms.InlineAux (inlineAux)
import           Language.Haskell.Liquid.Transforms.Rewrite (rewriteBinds)

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

import           Data.Coerce
import           Data.Function                            ((&))
import qualified Data.List                               as L
import           Data.IORef
import qualified Data.Map                                as M
import           Data.Map                                 ( Map )


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.Errors
import           Language.Haskell.Liquid.Types.PrettyPrint
import           Language.Haskell.Liquid.Types.Specs
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Visitors
import           Language.Haskell.Liquid.Bare
import qualified Language.Haskell.Liquid.Bare.Resolve as Resolve
import           Language.Haskell.Liquid.UX.CmdLine
import           Language.Haskell.Liquid.UX.Config

-- | 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
(LiquidCheckException -> LiquidCheckException -> Bool)
-> (LiquidCheckException -> LiquidCheckException -> Bool)
-> Eq LiquidCheckException
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LiquidCheckException -> LiquidCheckException -> Bool
== :: LiquidCheckException -> LiquidCheckException -> Bool
$c/= :: LiquidCheckException -> LiquidCheckException -> Bool
/= :: LiquidCheckException -> LiquidCheckException -> Bool
Eq, Eq LiquidCheckException
Eq LiquidCheckException =>
(LiquidCheckException -> LiquidCheckException -> Ordering)
-> (LiquidCheckException -> LiquidCheckException -> Bool)
-> (LiquidCheckException -> LiquidCheckException -> Bool)
-> (LiquidCheckException -> LiquidCheckException -> Bool)
-> (LiquidCheckException -> LiquidCheckException -> Bool)
-> (LiquidCheckException
    -> LiquidCheckException -> LiquidCheckException)
-> (LiquidCheckException
    -> LiquidCheckException -> LiquidCheckException)
-> Ord 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
$ccompare :: LiquidCheckException -> LiquidCheckException -> Ordering
compare :: LiquidCheckException -> LiquidCheckException -> Ordering
$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
>= :: LiquidCheckException -> LiquidCheckException -> Bool
$cmax :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
max :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
$cmin :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
min :: LiquidCheckException
-> LiquidCheckException -> LiquidCheckException
Ord, Int -> LiquidCheckException -> ShowS
[LiquidCheckException] -> ShowS
LiquidCheckException -> [Char]
(Int -> LiquidCheckException -> ShowS)
-> (LiquidCheckException -> [Char])
-> ([LiquidCheckException] -> ShowS)
-> Show LiquidCheckException
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LiquidCheckException -> ShowS
showsPrec :: Int -> LiquidCheckException -> ShowS
$cshow :: LiquidCheckException -> [Char]
show :: LiquidCheckException -> [Char]
$cshowList :: [LiquidCheckException] -> ShowS
showList :: [LiquidCheckException] -> ShowS
Show)

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

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

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

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

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

plugin :: GHC.Plugin
plugin :: Plugin
plugin = Plugin
GHC.defaultPlugin {
    driverPlugin          = lhDynFlags
  , parsedResultAction    = parsePlugin
  , typeCheckResultAction = typecheckPlugin
  , pluginRecompile       = purePlugin
  }
  where
    liquidPlugin :: (MonadIO m) => [CommandLineOption] -> a -> (Config -> m a) -> m a
    liquidPlugin :: forall (m :: * -> *) a.
MonadIO m =>
[[Char]] -> a -> (Config -> m a) -> m a
liquidPlugin [[Char]]
opts a
def Config -> m a
go = do
        cfg <- IO Config -> m Config
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Config -> m Config) -> IO Config -> m Config
forall a b. (a -> b) -> a -> b
$ [[Char]] -> IO Config
LH.getOpts [[Char]]
opts
        if skipModule cfg then return def else go cfg

    parsePlugin :: [CommandLineOption] -> ModSummary -> ParsedResult -> Hsc ParsedResult
    parsePlugin :: [[Char]] -> ModSummary -> ParsedResult -> Hsc ParsedResult
parsePlugin [[Char]]
opts ModSummary
ms ParsedResult
parsedResult = [[Char]]
-> ParsedResult -> (Config -> Hsc ParsedResult) -> Hsc ParsedResult
forall (m :: * -> *) a.
MonadIO m =>
[[Char]] -> a -> (Config -> m a) -> m a
liquidPlugin [[Char]]
opts ParsedResult
parsedResult ((Config -> Hsc ParsedResult) -> Hsc ParsedResult)
-> (Config -> Hsc ParsedResult) -> Hsc ParsedResult
forall a b. (a -> b) -> a -> b
$ \Config
cfg ->
      Config -> ModSummary -> ParsedResult -> Hsc ParsedResult
parsedHook Config
cfg ModSummary
ms ParsedResult
parsedResult

    typecheckPlugin :: [CommandLineOption] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
    typecheckPlugin :: [[Char]] -> ModSummary -> TcGblEnv -> TcM TcGblEnv
typecheckPlugin [[Char]]
opts ModSummary
summary TcGblEnv
gblEnv = [[Char]] -> TcGblEnv -> (Config -> TcM TcGblEnv) -> TcM TcGblEnv
forall (m :: * -> *) a.
MonadIO m =>
[[Char]] -> a -> (Config -> m a) -> m a
liquidPlugin [[Char]]
opts TcGblEnv
gblEnv ((Config -> TcM TcGblEnv) -> TcM TcGblEnv)
-> (Config -> TcM TcGblEnv) -> TcM TcGblEnv
forall a b. (a -> b) -> a -> b
$ \Config
cfg ->
      Config -> ModSummary -> TcGblEnv -> TcM TcGblEnv
typecheckPluginGo Config
cfg 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.
    typecheckPluginGo :: Config -> ModSummary -> TcGblEnv -> TcM TcGblEnv
typecheckPluginGo Config
cfg ModSummary
summary TcGblEnv
gblEnv = do
      logger <- IOEnv (Env TcGblEnv TcLclEnv) Logger
forall (m :: * -> *). HasLogger m => m Logger
getLogger
      dynFlags <- getDynFlags
      withTiming logger (text "LiquidHaskell" <+> brackets (ppr $ ms_mod_name summary)) (const ()) $ do
        if gopt Opt_Haddock dynFlags
          then do
            -- Warn the user
            let msg     = [Doc] -> Doc
PJ.vcat [ [Char] -> Doc
PJ.text [Char]
"LH can't be run with Haddock."
                                  , Int -> Doc -> Doc
PJ.nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
PJ.text [Char]
"Documentation will still be created."
                                  ]
            let srcLoc  = FastString -> Int -> Int -> SrcLoc
mkSrcLoc ([Char] -> FastString
mkFastString ([Char] -> FastString) -> [Char] -> FastString
forall a b. (a -> b) -> a -> b
$ ModSummary -> [Char]
ms_hspp_file ModSummary
summary) Int
1 Int
1
            let warning = SrcSpan -> Doc -> Warning
mkWarning (SrcLoc -> SrcLoc -> SrcSpan
mkSrcSpan SrcLoc
srcLoc SrcLoc
srcLoc) Doc
msg
            liftIO $ printWarning logger warning
            pure gblEnv
          else do
            newGblEnv <- typecheckHook cfg summary gblEnv
            case newGblEnv of
              -- Exit with success if all expected errors were found
              Left (ErrorsOccurred []) -> TcGblEnv -> TcM TcGblEnv
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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
                [Char] -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
defaultFilterReporter (ModSummary -> [Char]
LH.modSummaryHsFile ModSummary
summary) [Filter]
errorFilters
                TcM TcGblEnv
forall env a. IOEnv env a
failM
              Right TcGblEnv
newGblEnv' ->
                TcGblEnv -> TcM TcGblEnv
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TcGblEnv
newGblEnv'

--------------------------------------------------------------------------------
-- | Inter-phase communication -------------------------------------------------
--------------------------------------------------------------------------------
--
-- Since we have no good way of passing extra data between different
-- phases of our plugin, we resort to leaving breadcrumbs in horrible
-- global mutable state.
--
-- Each module gets a mutable breadcrumb during compilation.
--
-- The @parseResultAction@ sets the breadcumb to @Parsed mod@.
--
-- The @typeCheckResultAction@ clears the breadcrumb on entry.
--
-- If the @typeCheckResultAction@ does not find the breadcrumb, it skips the
-- module, assuming that it has been verified already. This could happen if
-- the plugin is activated more than once on the same module (by passing
-- multiple times @-fplugin=LiquidHaskell@ to GHC).

{- HLINT ignore Breadcrumb "Use newtype instead of data" -}
  -- It's basically an accidental detail that we only have one type of
  -- breadcrumb at the moment. We don't want to use a `newtype` to
  -- avoid communicating the false intention that a breadcrumb "is" a
  -- list of `SpecComment`s.
data Breadcrumb
  = Parsed ![SpecComment]

breadcrumbsRef :: IORef (Map Module Breadcrumb)
breadcrumbsRef :: IORef (Map Module Breadcrumb)
breadcrumbsRef = IO (IORef (Map Module Breadcrumb)) -> IORef (Map Module Breadcrumb)
forall a. IO a -> a
unsafePerformIO (IO (IORef (Map Module Breadcrumb))
 -> IORef (Map Module Breadcrumb))
-> IO (IORef (Map Module Breadcrumb))
-> IORef (Map Module Breadcrumb)
forall a b. (a -> b) -> a -> b
$ Map Module Breadcrumb -> IO (IORef (Map Module Breadcrumb))
forall a. a -> IO (IORef a)
newIORef Map Module Breadcrumb
forall a. Monoid a => a
mempty
{-# NOINLINE breadcrumbsRef #-}

{- HLINT ignore swapBreadcrumb "Use tuple-section" -}
swapBreadcrumb :: (MonadIO m) => Module -> Maybe Breadcrumb -> m (Maybe Breadcrumb)
swapBreadcrumb :: forall (m :: * -> *).
MonadIO m =>
Module -> Maybe Breadcrumb -> m (Maybe Breadcrumb)
swapBreadcrumb Module
mod0 Maybe Breadcrumb
new = IO (Maybe Breadcrumb) -> m (Maybe Breadcrumb)
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe Breadcrumb) -> m (Maybe Breadcrumb))
-> IO (Maybe Breadcrumb) -> m (Maybe Breadcrumb)
forall a b. (a -> b) -> a -> b
$ IORef (Map Module Breadcrumb)
-> (Map Module Breadcrumb
    -> (Map Module Breadcrumb, Maybe Breadcrumb))
-> IO (Maybe Breadcrumb)
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Map Module Breadcrumb)
breadcrumbsRef ((Map Module Breadcrumb
  -> (Map Module Breadcrumb, Maybe Breadcrumb))
 -> IO (Maybe Breadcrumb))
-> (Map Module Breadcrumb
    -> (Map Module Breadcrumb, Maybe Breadcrumb))
-> IO (Maybe Breadcrumb)
forall a b. (a -> b) -> a -> b
$ \Map Module Breadcrumb
breadcrumbs ->
  let (Maybe Breadcrumb
old, Map Module Breadcrumb
breadcrumbs') = (Maybe Breadcrumb -> (Maybe Breadcrumb, Maybe Breadcrumb))
-> Module
-> Map Module Breadcrumb
-> (Maybe Breadcrumb, Map Module Breadcrumb)
forall (f :: * -> *) k a.
(Functor f, Ord k) =>
(Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
M.alterF (\Maybe Breadcrumb
old1 -> (Maybe Breadcrumb
old1, Maybe Breadcrumb
new)) Module
mod0 Map Module Breadcrumb
breadcrumbs
  in (Map Module Breadcrumb
breadcrumbs', Maybe Breadcrumb
old)

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

lhDynFlags :: [CommandLineOption] -> HscEnv -> IO HscEnv
lhDynFlags :: [[Char]] -> HscEnv -> IO HscEnv
lhDynFlags [[Char]]
_ HscEnv
hscEnv =
    HscEnv -> IO HscEnv
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return HscEnv
hscEnv
      { hsc_dflags =
          hsc_dflags hscEnv
           -- Ignore-interface-pragmas need to be unset to have access to
           -- the RHS unfoldings in the `Ghc.Var`s which is
           -- needed as part of the reflection of foreign functions in the logic
           --
           -- This needs to be active before the plugin runs, so pragmas are
           -- read at the time the interface files are loaded.
           `gopt_unset` Opt_IgnoreInterfacePragmas
           -- 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.
           `gopt_set` Opt_KeepRawTokenStream
      }

--------------------------------------------------------------------------------
-- | Desugarer setting tweaks --------------------------------------------------
--------------------------------------------------------------------------------

-- | LiquidHaskell requires the desugarer to keep source note ticks
-- and to export everything.
--
-- TODO: We shouldn't rely on exports to find out what's in a ModGuts
-- https://github.com/ucsd-progsys/liquidhaskell/pull/2388#issuecomment-2411418479
desugarerDynFlags :: DynFlags -> DynFlags
desugarerDynFlags :: DynFlags -> DynFlags
desugarerDynFlags DynFlags
df = ((DynFlags -> GeneralFlag -> DynFlags)
-> DynFlags -> [GeneralFlag] -> DynFlags
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl DynFlags -> GeneralFlag -> DynFlags
gopt_unset DynFlags
df [GeneralFlag]
disabledOpts)
    { debugLevel   = 1                  -- To keep source note ticks
    , backend      = interpreterBackend -- To export everything
    }
  where
    disabledOpts :: [GeneralFlag]
disabledOpts =
      [ GeneralFlag
Opt_EnableRewriteRules -- Prevent the simple optimizer from firing rewrite rules
                               -- during desugaring. See tests/reflect/pos/T2405.hs for
                               -- a discussion of an example where this is unwanted.
      ]


--------------------------------------------------------------------------------
-- | Parsing phase -------------------------------------------------------------
--------------------------------------------------------------------------------

-- | We hook at this stage of the pipeline to extract the
-- specs. Comments are preserved during parsing because we turn on
-- 'Opt_KeepRawTokenStream'. So we can get the /LH/ specs from
-- there.
parsedHook :: Config -> ModSummary -> ParsedResult -> Hsc ParsedResult
parsedHook :: Config -> ModSummary -> ParsedResult -> Hsc ParsedResult
parsedHook Config
_cfg ModSummary
ms ParsedResult
parsedResult = do
    -- TODO: we should parse the specs here so we can fail early
    -- (before going through the whole GHC typechecker) if they don't
    -- parse. Alas, LH.filterReportError is TcRn-specific.
    let specComments :: [SpecComment]
specComments = ((Maybe RealSrcLoc, [Char]) -> SpecComment)
-> [(Maybe RealSrcLoc, [Char])] -> [SpecComment]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe RealSrcLoc, [Char]) -> SpecComment
mkSpecComment ([(Maybe RealSrcLoc, [Char])] -> [SpecComment])
-> [(Maybe RealSrcLoc, [Char])] -> [SpecComment]
forall a b. (a -> b) -> a -> b
$ HsParsedModule -> [(Maybe RealSrcLoc, [Char])]
LH.extractSpecComments (ParsedResult -> HsParsedModule
parsedResultModule ParsedResult
parsedResult)

    -- See 'Breadcrumb' for more information.
    _oldBreadcrumb <- Module -> Maybe Breadcrumb -> Hsc (Maybe Breadcrumb)
forall (m :: * -> *).
MonadIO m =>
Module -> Maybe Breadcrumb -> m (Maybe Breadcrumb)
swapBreadcrumb Module
thisModule (Maybe Breadcrumb -> Hsc (Maybe Breadcrumb))
-> Maybe Breadcrumb -> Hsc (Maybe Breadcrumb)
forall a b. (a -> b) -> a -> b
$ Breadcrumb -> Maybe Breadcrumb
forall a. a -> Maybe a
Just ([SpecComment] -> Breadcrumb
Parsed [SpecComment]
specComments)

    return parsedResult
  where
    thisModule :: Module
thisModule = ModSummary -> Module
ms_mod ModSummary
ms

--------------------------------------------------------------------------------
-- | 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 desugaring a postprocessed version of the typechecked module, so we are
--    really independent from the \"normal\" compilation pipeline.
--
typecheckHook  :: Config -> ModSummary -> TcGblEnv -> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook :: Config
-> ModSummary
-> TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook Config
cfg0 ModSummary
ms TcGblEnv
tcGblEnv = Module
-> Maybe Breadcrumb
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe Breadcrumb)
forall (m :: * -> *).
MonadIO m =>
Module -> Maybe Breadcrumb -> m (Maybe Breadcrumb)
swapBreadcrumb Module
thisModule Maybe Breadcrumb
forall a. Maybe a
Nothing IOEnv (Env TcGblEnv TcLclEnv) (Maybe Breadcrumb)
-> (Maybe Breadcrumb -> TcM (Either LiquidCheckException TcGblEnv))
-> TcM (Either LiquidCheckException TcGblEnv)
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) a
-> (a -> IOEnv (Env TcGblEnv TcLclEnv) b)
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Just (Parsed [SpecComment]
specComments) ->
    Config
-> ModSummary
-> TcGblEnv
-> [SpecComment]
-> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook' Config
cfg0 ModSummary
ms TcGblEnv
tcGblEnv [SpecComment]
specComments
  Maybe Breadcrumb
Nothing ->
    -- The module has been verified by an earlier call to the plugin.
    -- This could happen if multiple @-fplugin=LiquidHaskell@ flags are passed to GHC.
    -- See 'Breadcrumb' for more information.
    Either LiquidCheckException TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either LiquidCheckException TcGblEnv
 -> TcM (Either LiquidCheckException TcGblEnv))
-> Either LiquidCheckException TcGblEnv
-> TcM (Either LiquidCheckException TcGblEnv)
forall a b. (a -> b) -> a -> b
$ TcGblEnv -> Either LiquidCheckException TcGblEnv
forall a b. b -> Either a b
Right TcGblEnv
tcGblEnv
  where
    thisModule :: Module
thisModule = ModSummary -> Module
ms_mod ModSummary
ms

typecheckHook' :: Config -> ModSummary -> TcGblEnv -> [SpecComment] -> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook' :: Config
-> ModSummary
-> TcGblEnv
-> [SpecComment]
-> TcM (Either LiquidCheckException TcGblEnv)
typecheckHook' Config
cfg ModSummary
ms TcGblEnv
tcGblEnv [SpecComment]
specComments = do
  [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *). MonadIO m => [Char] -> m ()
debugLog ([Char] -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"We are in module: " [Char] -> ShowS
forall a. Semigroup a => a -> a -> a
<> StableModule -> [Char]
forall a. Show a => a -> [Char]
show (Module -> StableModule
toStableModule Module
thisModule)

  case [(SourcePos, [Char])] -> Either [Error] [BPspec]
parseSpecComments ([SpecComment] -> [(SourcePos, [Char])]
forall a b. Coercible a b => a -> b
coerce [SpecComment]
specComments) of
    Left [Error]
errors ->
      [Char]
-> TcM (Either LiquidCheckException TcGblEnv)
-> TcM (Either LiquidCheckException TcGblEnv)
-> [Filter]
-> Tidy
-> [Error]
-> TcM (Either LiquidCheckException TcGblEnv)
forall e' a.
(Show e', PPrint e') =>
[Char]
-> TcRn a -> TcRn a -> [Filter] -> Tidy -> [TError e'] -> TcRn a
LH.filterReportErrors [Char]
thisFile TcM (Either LiquidCheckException TcGblEnv)
forall env a. IOEnv env a
GHC.failM TcM (Either LiquidCheckException TcGblEnv)
forall {b}.
IOEnv (Env TcGblEnv TcLclEnv) (Either LiquidCheckException b)
continue (Config -> [Filter]
getFilters Config
cfg) Tidy
Full [Error]
errors
    Right [BPspec]
specs ->
      Config
-> ModSummary
-> TcGblEnv
-> [BPspec]
-> TcM (Either LiquidCheckException TcGblEnv)
liquidCheckModule Config
cfg ModSummary
ms TcGblEnv
tcGblEnv [BPspec]
specs
  where
    thisModule :: Module
thisModule = ModSummary -> Module
ms_mod ModSummary
ms
    thisFile :: [Char]
thisFile = ModSummary -> [Char]
LH.modSummaryHsFile ModSummary
ms

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

liquidCheckModule :: Config -> ModSummary -> TcGblEnv -> [BPspec] -> TcM (Either LiquidCheckException TcGblEnv)
liquidCheckModule :: Config
-> ModSummary
-> TcGblEnv
-> [BPspec]
-> TcM (Either LiquidCheckException TcGblEnv)
liquidCheckModule Config
cfg0 ModSummary
ms TcGblEnv
tcg [BPspec]
specs = do
  Config
-> [Char]
-> [Located [Char]]
-> (Config -> TcM (Either LiquidCheckException TcGblEnv))
-> TcM (Either LiquidCheckException TcGblEnv)
forall (m :: * -> *) a.
MonadIO m =>
Config -> [Char] -> [Located [Char]] -> (Config -> m a) -> m a
withPragmas Config
cfg0 [Char]
thisFile [Located [Char]]
pragmas ((Config -> TcM (Either LiquidCheckException TcGblEnv))
 -> TcM (Either LiquidCheckException TcGblEnv))
-> (Config -> TcM (Either LiquidCheckException TcGblEnv))
-> TcM (Either LiquidCheckException TcGblEnv)
forall a b. (a -> b) -> a -> b
$ \Config
cfg -> do
    pipelineData <- do
      env <- TcRnIf TcGblEnv TcLclEnv HscEnv
forall gbl lcl. TcRnIf gbl lcl HscEnv
getTopEnv
      session <- Session <$> liftIO (newIORef env)
      liftIO $ flip reflectGhc session $ mkPipelineData ms tcg specs
    liquidLib <- setGblEnv tcg $ liquidHaskellCheckWithConfig cfg pipelineData ms
    traverse (serialiseSpec tcg) liquidLib
  where
    thisFile :: [Char]
thisFile = ModSummary -> [Char]
LH.modSummaryHsFile ModSummary
ms
    pragmas :: [Located [Char]]
pragmas = [ Located [Char]
s | Pragma Located [Char]
s <- [BPspec]
specs ]

mkPipelineData :: (GhcMonad m) => ModSummary -> TcGblEnv -> [BPspec] -> m PipelineData
mkPipelineData :: forall (m :: * -> *).
GhcMonad m =>
ModSummary -> TcGblEnv -> [BPspec] -> m PipelineData
mkPipelineData ModSummary
ms TcGblEnv
tcg0 [BPspec]
specs = do
    let tcg :: TcGblEnv
tcg = TcGblEnv -> TcGblEnv
addNoInlinePragmasToBinds TcGblEnv
tcg0

    unoptimisedGuts <- (HscEnv -> m ModGuts) -> m ModGuts
forall (m :: * -> *) a. GhcMonad m => (HscEnv -> m a) -> m a
withSession ((HscEnv -> m ModGuts) -> m ModGuts)
-> (HscEnv -> m ModGuts) -> m ModGuts
forall a b. (a -> b) -> a -> b
$ \HscEnv
hsc_env ->
        let lcl_hsc_env :: HscEnv
lcl_hsc_env = (DynFlags -> DynFlags) -> HscEnv -> HscEnv
hscUpdateFlags (DynFlags -> DynFlags
noWarnings (DynFlags -> DynFlags)
-> (DynFlags -> DynFlags) -> DynFlags -> DynFlags
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DynFlags -> DynFlags
desugarerDynFlags) HscEnv
hsc_env in
        IO ModGuts -> m ModGuts
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ModGuts -> m ModGuts) -> IO ModGuts -> m ModGuts
forall a b. (a -> b) -> a -> b
$ HscEnv -> ModSummary -> TcGblEnv -> IO ModGuts
hscDesugar HscEnv
lcl_hsc_env ModSummary
ms TcGblEnv
tcg

    return $ PipelineData unoptimisedGuts specs
  where
    noWarnings :: DynFlags -> DynFlags
noWarnings DynFlags
dflags = DynFlags
dflags { warningFlags = mempty }

serialiseSpec :: TcGblEnv -> LiquidLib -> TcM TcGblEnv
serialiseSpec :: TcGblEnv -> LiquidLib -> TcM TcGblEnv
serialiseSpec 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"
  -- ---

  serialisedSpec <- IO Annotation -> IOEnv (Env TcGblEnv TcLclEnv) Annotation
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Annotation -> IOEnv (Env TcGblEnv TcLclEnv) Annotation)
-> IO Annotation -> IOEnv (Env TcGblEnv TcLclEnv) Annotation
forall a b. (a -> b) -> a -> b
$ LiquidLib -> Module -> IO Annotation
Serialisation.serialiseLiquidLib LiquidLib
liquidLib Module
thisModule
  debugLog $ "Serialised annotation ==> " ++ (O.showSDocUnsafe . O.ppr $ serialisedSpec)

  -- liftIO $ putStrLn "liquidHaskellCheck 10"

  pure $ tcGblEnv { tcg_anns = serialisedSpec : tcg_anns tcGblEnv }
  where
    thisModule :: Module
thisModule = TcGblEnv -> Module
tcg_mod TcGblEnv
tcGblEnv

processInputSpec
  :: Config
  -> PipelineData
  -> ModSummary
  -> BareSpecParsed
  -> TcM (Either LiquidCheckException LiquidLib)
processInputSpec :: Config
-> PipelineData
-> ModSummary
-> BareSpecParsed
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
processInputSpec Config
cfg PipelineData
pipelineData ModSummary
modSummary BareSpecParsed
inputSpec = do
  tcg <- TcM TcGblEnv
forall gbl lcl. TcRnIf gbl lcl gbl
getGblEnv
  debugLog $ " Input spec: \n" ++ show (fromBareSpecParsed inputSpec)
  debugLog $ "Direct ===> \n" ++ unlines (renderModule <$> directImports tcg)

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

  let lhContext = LiquidHaskellContext {
        lhGlobalCfg :: Config
lhGlobalCfg       = Config
cfg
      , lhInputSpec :: BareSpecParsed
lhInputSpec       = BareSpecParsed
inputSpec
      , lhModuleSummary :: ModSummary
lhModuleSummary   = ModSummary
modSummary
      , lhModuleGuts :: ModGuts
lhModuleGuts      = PipelineData -> ModGuts
pdUnoptimisedCore PipelineData
pipelineData
      , lhRelevantModules :: [Module]
lhRelevantModules = TcGblEnv -> [Module]
directImports TcGblEnv
tcg
      }

  -- liftIO $ putStrLn ("liquidHaskellCheck 6: " ++ show isIg)
  if isIgnore inputSpec
    then pure $ Left (ErrorsOccurred [])
    else checkLiquidHaskellContext lhContext

liquidHaskellCheckWithConfig
  :: Config -> PipelineData -> ModSummary -> TcM (Either LiquidCheckException LiquidLib)
liquidHaskellCheckWithConfig :: Config
-> PipelineData
-> ModSummary
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
liquidHaskellCheckWithConfig Config
cfg PipelineData
pipelineData ModSummary
modSummary = do
  -- Parse the spec comments stored in the pipeline data.
  let inputSpec :: BareSpecParsed
inputSpec = (ModName, BareSpecParsed) -> BareSpecParsed
forall a b. (a, b) -> b
snd ((ModName, BareSpecParsed) -> BareSpecParsed)
-> (ModName, BareSpecParsed) -> BareSpecParsed
forall a b. (a -> b) -> a -> b
$
        ModuleName -> [BPspec] -> (ModName, BareSpecParsed)
hsSpecificationP (Module -> ModuleName
forall unit. GenModule unit -> ModuleName
moduleName Module
thisModule) (PipelineData -> [BPspec]
pdSpecComments PipelineData
pipelineData)

  Config
-> PipelineData
-> ModSummary
-> BareSpecParsed
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
processInputSpec Config
cfg PipelineData
pipelineData ModSummary
modSummary BareSpecParsed
inputSpec
    TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
-> (UserError
    -> TcRnIf
         TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib))
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall e a.
(HasCallStack, Exception e) =>
IOEnv (Env TcGblEnv TcLclEnv) a
-> (e -> IOEnv (Env TcGblEnv TcLclEnv) a)
-> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\(UserError
e :: UserError) -> [UserError]
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall e a.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException a)
reportErrs [UserError
e])
    TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
-> (Error
    -> TcRnIf
         TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib))
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall e a.
(HasCallStack, Exception e) =>
IOEnv (Env TcGblEnv TcLclEnv) a
-> (e -> IOEnv (Env TcGblEnv TcLclEnv) a)
-> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\(Error
e :: Error) -> [Error]
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall e a.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException a)
reportErrs [Error
e])
    TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
-> ([Error]
    -> TcRnIf
         TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib))
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall e a.
(HasCallStack, Exception e) =>
IOEnv (Env TcGblEnv TcLclEnv) a
-> (e -> IOEnv (Env TcGblEnv TcLclEnv) a)
-> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) e a.
(MonadCatch m, HasCallStack, Exception e) =>
m a -> (e -> m a) -> m a
`Ex.catch` (\([Error]
es :: [Error]) -> [Error]
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall e a.
(Show e, PPrint e) =>
[TError e] -> TcM (Either LiquidCheckException a)
reportErrs [Error]
es)

  where
    thisFile :: [Char]
thisFile = ModSummary -> [Char]
LH.modSummaryHsFile ModSummary
modSummary
    thisModule :: Module
thisModule = ModSummary -> Module
ms_mod ModSummary
modSummary

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

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

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

      let bareSpec = LiquidHaskellContext -> BareSpecParsed
lhInputSpec LiquidHaskellContext
lhContext
          file = ModSummary -> [Char]
LH.modSummaryHsFile (ModSummary -> [Char]) -> ModSummary -> [Char]
forall a b. (a -> b) -> a -> b
$ LiquidHaskellContext -> ModSummary
lhModuleSummary LiquidHaskellContext
lhContext

      withPragmas (lhGlobalCfg lhContext) file (Ms.pragmas bareSpec) $ \Config
moduleCfg ->  do
        let filters :: [Filter]
filters = Config -> [Filter]
getFilters Config
moduleCfg
        -- Report the outcome of the checking
        (OutputResult -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> Config
-> [[Char]]
-> Output Doc
-> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *).
MonadIO m =>
(OutputResult -> m ()) -> Config -> [[Char]] -> Output Doc -> m ()
LH.reportResult ([Char]
-> [Filter] -> OutputResult -> IOEnv (Env TcGblEnv TcLclEnv) ()
errorLogger [Char]
file [Filter]
filters) Config
moduleCfg [TargetSrc -> [Char]
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 Output Doc -> ErrorResult
forall a. Output a -> ErrorResult
o_result Output Doc
out of
          F.Safe Stats
_ -> Either LiquidCheckException LiquidLib
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either LiquidCheckException LiquidLib
 -> TcRnIf
      TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib))
-> Either LiquidCheckException LiquidLib
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall a b. (a -> b) -> a -> b
$ LiquidLib -> Either LiquidCheckException LiquidLib
forall a b. b -> Either a b
Right LiquidLib
pmrClientLib
          ErrorResult
_ | Config -> Bool
json Config
moduleCfg -> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall env a. IOEnv env a
failM
            | Bool
otherwise -> Either LiquidCheckException LiquidLib
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either LiquidCheckException LiquidLib
 -> TcRnIf
      TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib))
-> Either LiquidCheckException LiquidLib
-> TcRnIf TcGblEnv TcLclEnv (Either LiquidCheckException LiquidLib)
forall a b. (a -> b) -> a -> b
$ LiquidCheckException -> Either LiquidCheckException LiquidLib
forall a b. a -> Either a b
Left (LiquidCheckException -> Either LiquidCheckException LiquidLib)
-> LiquidCheckException -> Either LiquidCheckException LiquidLib
forall a b. (a -> b) -> a -> b
$ [Filter] -> LiquidCheckException
ErrorsOccurred []

errorLogger :: FilePath -> [Filter] -> OutputResult -> TcM ()
errorLogger :: [Char]
-> [Filter] -> OutputResult -> IOEnv (Env TcGblEnv TcLclEnv) ()
errorLogger [Char]
file [Filter]
filters OutputResult
outputResult = do
  FilterReportErrorsArgs
  (IOEnv (Env TcGblEnv TcLclEnv)) Filter Any (SrcSpan, Doc) ()
-> [(SrcSpan, Doc)] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *) filter msg e a.
(Monad m, Ord filter) =>
FilterReportErrorsArgs m filter msg e a -> [e] -> m a
LH.filterReportErrorsWith
    FilterReportErrorsArgs { errorReporter :: [(SrcSpan, Doc)] -> IOEnv (Env TcGblEnv TcLclEnv) ()
errorReporter = \[(SrcSpan, Doc)]
errs ->
                               [(SrcSpan, Doc)] -> IOEnv (Env TcGblEnv TcLclEnv) ()
LH.addTcRnUnknownMessages [(SrcSpan
sp, Doc
e) | (SrcSpan
sp, Doc
e) <- [(SrcSpan, Doc)]
errs]
                           , filterReporter :: [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
filterReporter = [Char] -> [Filter] -> IOEnv (Env TcGblEnv TcLclEnv) ()
LH.defaultFilterReporter [Char]
file
                           , failure :: IOEnv (Env TcGblEnv TcLclEnv) ()
failure = IOEnv (Env TcGblEnv TcLclEnv) ()
forall env a. IOEnv env a
GHC.failM
                           , continue :: IOEnv (Env TcGblEnv TcLclEnv) ()
continue = () -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                           , matchingFilters :: (SrcSpan, Doc) -> [Filter]
matchingFilters = ((SrcSpan, Doc) -> [Char])
-> [Filter] -> (SrcSpan, Doc) -> [Filter]
forall e. (e -> [Char]) -> [Filter] -> e -> [Filter]
LH.reduceFilters (\(SrcSpan
src, Doc
doc) -> Doc -> [Char]
PJ.render Doc
doc [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" at " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SrcSpan -> [Char]
forall a. Outputable a => a -> [Char]
LH.showPpr SrcSpan
src) [Filter]
filters
                           , filters :: [Filter]
filters = [Filter]
filters
                           }
    (OutputResult -> [(SrcSpan, Doc)]
LH.orMessages OutputResult
outputResult)

isIgnore :: Spec lname ty -> Bool
isIgnore :: forall lname ty. Spec lname ty -> Bool
isIgnore Spec lname ty
sp = (Located [Char] -> Bool) -> [Located [Char]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"--skip-module") ([Char] -> Bool)
-> (Located [Char] -> [Char]) -> Located [Char] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located [Char] -> [Char]
forall a. Located a -> a
F.val) (Spec lname ty -> [Located [Char]]
forall lname ty. Spec lname ty -> [Located [Char]]
pragmas Spec lname ty
sp)

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

loadDependencies :: Config -> [Module] -> TcM TargetDependencies
loadDependencies :: Config -> [Module] -> TcM TargetDependencies
loadDependencies Config
currentModuleConfig [Module]
mods = do
  hscEnv    <- Env TcGblEnv TcLclEnv -> HscEnv
forall gbl lcl. Env gbl lcl -> HscEnv
env_top (Env TcGblEnv TcLclEnv -> HscEnv)
-> IOEnv (Env TcGblEnv TcLclEnv) (Env TcGblEnv TcLclEnv)
-> TcRnIf TcGblEnv TcLclEnv HscEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env TcGblEnv TcLclEnv) (Env TcGblEnv TcLclEnv)
forall env. IOEnv env env
getEnv
  results   <- SpecFinder.findRelevantSpecs
                 (excludeAutomaticAssumptionsFor currentModuleConfig) hscEnv mods
  let deps = HashMap StableModule LiftedSpec -> TargetDependencies
TargetDependencies (HashMap StableModule LiftedSpec -> TargetDependencies)
-> HashMap StableModule LiftedSpec -> TargetDependencies
forall a b. (a -> b) -> a -> b
$ (HashMap StableModule LiftedSpec
 -> SpecFinderResult -> HashMap StableModule LiftedSpec)
-> HashMap StableModule LiftedSpec
-> [SpecFinderResult]
-> HashMap StableModule LiftedSpec
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HashMap StableModule LiftedSpec
-> SpecFinderResult -> HashMap StableModule LiftedSpec
processResult HashMap StableModule LiftedSpec
forall a. Monoid a => a
mempty ([SpecFinderResult] -> [SpecFinderResult]
forall a. [a] -> [a]
reverse [SpecFinderResult]
results)
  redundant <- liftIO $ configToRedundantDependencies hscEnv currentModuleConfig

  debugLog $ "Redundant dependencies ==> " ++ show redundant

  pure $ foldl' (flip dropDependency) deps redundant
  where
    processResult
      :: HM.HashMap StableModule LiftedSpec
      -> SpecFinderResult
      -> HM.HashMap StableModule LiftedSpec
    processResult :: HashMap StableModule LiftedSpec
-> SpecFinderResult -> HashMap StableModule LiftedSpec
processResult HashMap StableModule LiftedSpec
acc (SpecNotFound Module
_mdl) = HashMap StableModule LiftedSpec
acc
    processResult HashMap StableModule LiftedSpec
acc (LibFound Module
originalModule LiquidLib
lib) =
      StableModule
-> LiftedSpec
-> HashMap StableModule LiftedSpec
-> HashMap StableModule LiftedSpec
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)
        (HashMap StableModule LiftedSpec
acc HashMap StableModule LiftedSpec
-> HashMap StableModule LiftedSpec
-> HashMap StableModule LiftedSpec
forall a. Semigroup a => a -> a -> a
<> TargetDependencies -> HashMap StableModule LiftedSpec
getDependencies (LiquidLib -> TargetDependencies
libDeps LiquidLib
lib))

data LiquidHaskellContext = LiquidHaskellContext {
    LiquidHaskellContext -> Config
lhGlobalCfg        :: Config
  , LiquidHaskellContext -> BareSpecParsed
lhInputSpec        :: BareSpecParsed
  , LiquidHaskellContext -> ModSummary
lhModuleSummary    :: ModSummary
  , LiquidHaskellContext -> ModGuts
lhModuleGuts       :: ModGuts
  , LiquidHaskellContext -> [Module]
lhRelevantModules  :: [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.
  }

processModule :: LiquidHaskellContext -> TcM (Either LiquidCheckException ProcessModuleResult)
processModule :: LiquidHaskellContext
-> TcM (Either LiquidCheckException ProcessModuleResult)
processModule LiquidHaskellContext{[Module]
ModGuts
ModSummary
Config
BareSpecParsed
lhGlobalCfg :: LiquidHaskellContext -> Config
lhInputSpec :: LiquidHaskellContext -> BareSpecParsed
lhModuleSummary :: LiquidHaskellContext -> ModSummary
lhModuleGuts :: LiquidHaskellContext -> ModGuts
lhRelevantModules :: LiquidHaskellContext -> [Module]
lhGlobalCfg :: Config
lhInputSpec :: BareSpecParsed
lhModuleSummary :: ModSummary
lhModuleGuts :: ModGuts
lhRelevantModules :: [Module]
..} = do
  let modGuts0 :: ModGuts
modGuts0   = ModGuts
lhModuleGuts
      thisModule :: Module
thisModule = ModGuts -> Module
mg_module ModGuts
modGuts0

  [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *). MonadIO m => [Char] -> m ()
debugLog ([Char]
"Module ==> " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Module -> [Char]
renderModule Module
thisModule)

  let bareSpec0 :: BareSpecParsed
bareSpec0       = BareSpecParsed
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 :: [Char]
file            = ModSummary -> [Char]
LH.modSummaryHsFile ModSummary
lhModuleSummary

  _                   <- IO () -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> IO () -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [Located [Char]] -> IO ()
LH.checkFilePragmas ([Located [Char]] -> IO ()) -> [Located [Char]] -> IO ()
forall a b. (a -> b) -> a -> b
$ BareSpecParsed -> [Located [Char]]
forall lname ty. Spec lname ty -> [Located [Char]]
Ms.pragmas BareSpecParsed
bareSpec0

  withPragmas lhGlobalCfg file (Ms.pragmas bareSpec0) $ \Config
moduleCfg -> do
    dependencies <- Config -> [Module] -> TcM TargetDependencies
loadDependencies Config
moduleCfg [Module]
lhRelevantModules

    debugLog $ "Found " <> show (HM.size $ getDependencies dependencies) <> " dependencies:"
    when debugLogs $
      forM_ (HM.keys . getDependencies $ dependencies) $ debugLog . moduleStableString . unStableModule

    debugLog $ "mg_exports => " ++ O.showSDocUnsafe (O.ppr $ mg_exports modGuts0)
    debugLog $ "mg_tcs => " ++ O.showSDocUnsafe (O.ppr $ mg_tcs modGuts0)

    hscEnv <- getTopEnv
    let preNormalizedCore = Config -> ModGuts -> [CoreBind]
preNormalizeCore Config
moduleCfg ModGuts
modGuts0
        modGuts = ModGuts
modGuts0 { mg_binds = preNormalizedCore }
    targetSrc  <- liftIO $ makeTargetSrc moduleCfg file modGuts hscEnv
    logger <- getLogger

    -- 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.

    tcg <- getGblEnv
    let localVars = [CoreBind] -> LocalVars
Resolve.makeLocalVars [CoreBind]
preNormalizedCore
        eBareSpec = Config
-> Module
-> LocalVars
-> ImportedMods
-> GlobalRdrEnv
-> BareSpecParsed
-> TargetDependencies
-> Either [Error] (BareSpec, LogicNameEnv, LogicMap)
resolveLHNames
          Config
moduleCfg
          Module
thisModule
          LocalVars
localVars
          (ImportAvails -> ImportedMods
imp_mods (ImportAvails -> ImportedMods) -> ImportAvails -> ImportedMods
forall a b. (a -> b) -> a -> b
$ TcGblEnv -> ImportAvails
tcg_imports TcGblEnv
tcg)
          (TcGblEnv -> GlobalRdrEnv
tcg_rdr_env TcGblEnv
tcg)
          BareSpecParsed
bareSpec0
          TargetDependencies
dependencies
    result <-
      case eBareSpec of
        Left [Error]
errors -> Either Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Either
        Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)
 -> IOEnv
      (Env TcGblEnv TcLclEnv)
      (Either
         Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)))
-> Either
     Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Either
        Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec))
forall a b. (a -> b) -> a -> b
$ Diagnostics
-> Either
     Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)
forall a b. a -> Either a b
Left (Diagnostics
 -> Either
      Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec))
-> Diagnostics
-> Either
     Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)
forall a b. (a -> b) -> a -> b
$ [Warning] -> [Error] -> Diagnostics
mkDiagnostics [] [Error]
errors
        Right (BareSpec
bareSpec, LogicNameEnv
lnameEnv, LogicMap
lmap') ->
          (([Warning], TargetSpec, LiftedSpec)
 -> (([Warning], TargetSpec, LiftedSpec), BareSpec))
-> Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
-> Either
     Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec)
forall a b.
(a -> b) -> Either Diagnostics a -> Either Diagnostics b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,BareSpec
bareSpec) (Either Diagnostics ([Warning], TargetSpec, LiftedSpec)
 -> Either
      Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Either
        Diagnostics (([Warning], TargetSpec, LiftedSpec), BareSpec))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
            Config
-> LocalVars
-> LogicNameEnv
-> LogicMap
-> TargetSrc
-> BareSpec
-> TargetDependencies
-> IOEnv
     (Env TcGblEnv TcLclEnv)
     (Either Diagnostics ([Warning], TargetSpec, LiftedSpec))
makeTargetSpec
              Config
moduleCfg
              LocalVars
localVars
              LogicNameEnv
lnameEnv
              LogicMap
lmap'
              TargetSrc
targetSrc
              BareSpec
bareSpec
              TargetDependencies
dependencies

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

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

        [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *). MonadIO m => [Char] -> m ()
debugLog ([Char] -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"bareSpec ==> "   [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ BareSpec -> [Char]
forall a. Show a => a -> [Char]
show BareSpec
bareSpec
        [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall (m :: * -> *). MonadIO m => [Char] -> m ()
debugLog ([Char] -> IOEnv (Env TcGblEnv TcLclEnv) ())
-> [Char] -> IOEnv (Env TcGblEnv TcLclEnv) ()
forall a b. (a -> b) -> a -> b
$ [Char]
"liftedSpec ==> " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ LiftedSpec -> [Char]
forall a. Show a => a -> [Char]
show LiftedSpec
liftedSpec

        let clientLib :: LiquidLib
clientLib  = LiftedSpec -> LiquidLib
mkLiquidLib LiftedSpec
liftedSpec LiquidLib -> (LiquidLib -> LiquidLib) -> LiquidLib
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
            }

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

makeTargetSrc :: Config
              -> FilePath
              -> ModGuts
              -> HscEnv
              -> IO TargetSrc
makeTargetSrc :: Config -> [Char] -> ModGuts -> HscEnv -> IO TargetSrc
makeTargetSrc Config
cfg [Char]
file ModGuts
modGuts HscEnv
hscEnv = do
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
dumpPreNormalizedCore Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> IO ()
putStrLn [Char]
"\n*************** Pre-normalized CoreBinds *****************\n"
    [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
L.intersperse [Char]
"" ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ (CoreBind -> [Char]) -> [CoreBind] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (DynFlags -> CoreBind -> [Char]
forall a. Outputable a => DynFlags -> a -> [Char]
GHC.showPpr (HscEnv -> DynFlags
GHC.hsc_dflags HscEnv
hscEnv)) (ModGuts -> [CoreBind]
mg_binds ModGuts
modGuts)
  coreBinds <- Config -> HscEnv -> ModGuts -> IO [CoreBind]
anormalize Config
cfg HscEnv
hscEnv ModGuts
modGuts

  let allTcs      = MGIModGuts -> [TyCon]
mgi_tcs MGIModGuts
mgiModGuts

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

  debugLog $ "_gsTcs   => " ++ show allTcs
  debugLog $ "_gsFiTcs => " ++ show fiTcs
  debugLog $ "_gsFiDcs => " ++ show fiDcs
  debugLog $ "dataCons => " ++ show dataCons
  debugLog $ "coreBinds => " ++ (O.showSDocUnsafe . O.ppr $ coreBinds)
  debugLog $ "impVars => " ++ (O.showSDocUnsafe . O.ppr $ impVars)
  debugLog $ "useVars  => " ++ (O.showSDocUnsafe . O.ppr $ readVars coreBinds)
  debugLog $ "derVars  => " ++ (O.showSDocUnsafe . O.ppr $ HS.fromList (LH.derivedVars cfg mgiModGuts))
  debugLog $ "gsExports => " ++ show (mgi_exports  mgiModGuts)
  debugLog $ "gsTcs     => " ++ (O.showSDocUnsafe . O.ppr $ allTcs)
  debugLog $ "gsCls     => " ++ (O.showSDocUnsafe . O.ppr $ mgi_cls_inst mgiModGuts)
  debugLog $ "gsFiTcs   => " ++ (O.showSDocUnsafe . O.ppr $ fiTcs)
  debugLog $ "gsFiDcs   => " ++ show fiDcs
  debugLog $ "gsPrimTcs => " ++ (O.showSDocUnsafe . O.ppr $ GHC.primTyCons)
  return $ TargetSrc
    { giTarget    = file
    , giTargetMod = ModName Target (moduleName (mg_module modGuts))
    , giCbs       = coreBinds
    , giImpVars   = impVars
    , giDefVars   = L.nub $ dataCons ++ letVars coreBinds
    , giUseVars   = readVars coreBinds
    , giDerVars   = HS.fromList (LH.derivedVars cfg mgiModGuts)
    , gsExports   = mgi_exports  mgiModGuts
    , gsTcs       = allTcs
    , gsCls       = mgi_cls_inst mgiModGuts
    , gsFiTcs     = fiTcs
    , gsFiDcs     = fiDcs
    , gsPrimTcs   = GHC.primTyCons
    }
  where
    mgiModGuts :: MGIModGuts
    mgiModGuts :: MGIModGuts
mgiModGuts = Maybe [ClsInst] -> ModGuts -> MGIModGuts
miModGuts Maybe [ClsInst]
deriv ModGuts
modGuts
      where
        deriv :: Maybe [ClsInst]
deriv   = [ClsInst] -> Maybe [ClsInst]
forall a. a -> Maybe a
Just ([ClsInst] -> Maybe [ClsInst]) -> [ClsInst] -> Maybe [ClsInst]
forall a b. (a -> b) -> a -> b
$ InstEnv -> [ClsInst]
instEnvElts (InstEnv -> [ClsInst]) -> InstEnv -> [ClsInst]
forall a b. (a -> b) -> a -> b
$ ModGuts -> InstEnv
mg_inst_env ModGuts
modGuts

preNormalizeCore :: Config -> ModGuts -> [CoreBind]
preNormalizeCore :: Config -> ModGuts -> [CoreBind]
preNormalizeCore Config
cfg ModGuts
modGuts = Config -> [CoreBind] -> [CoreBind]
rewriteBinds Config
cfg [CoreBind]
inl_cbs
  where
    inl_cbs :: [CoreBind]
inl_cbs  = Config -> Module -> [CoreBind] -> [CoreBind]
inlineAux Config
cfg (ModGuts -> Module
mg_module ModGuts
modGuts) (ModGuts -> [CoreBind]
mg_binds ModGuts
modGuts)

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