{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE RankNTypes   #-}

module Language.Haskell.Liquid.GHC.Plugin.SpecFinder
    ( findRelevantSpecs
    , findCompanionSpec
    , SpecFinderResult(..)
    , SearchLocation(..)
    , configToRedundantDependencies
    ) where

import qualified Language.Haskell.Liquid.GHC.Plugin.Util as Util
import           Language.Haskell.Liquid.GHC.Plugin.Types
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.Specs     hiding (Spec)
import qualified Language.Haskell.Liquid.Misc            as Misc
import           Language.Haskell.Liquid.Parse            ( specSpecificationP )
import           Language.Fixpoint.Utils.Files            ( Ext(Spec), withExt )

import qualified Liquid.GHC.API         as O
import           Liquid.GHC.API         as GHC

import           Data.Bifunctor
import qualified Data.Char
import           Data.IORef
import           Data.Maybe

import           Control.Exception
import           Control.Monad                            ( foldM )
import           Control.Monad.Trans                      ( lift )
import           Control.Monad.Trans.Maybe

import           Text.Megaparsec.Error

type SpecFinder m = Module -> MaybeT IO SpecFinderResult

-- | The result of searching for a spec.
data SpecFinderResult = 
    SpecNotFound Module
  | SpecFound Module SearchLocation BareSpec
  | LibFound  Module SearchLocation LiquidLib

data SearchLocation =
    InterfaceLocation
  -- ^ The spec was loaded from the annotations of an interface.
  | DiskLocation
  -- ^ The spec was loaded from disk (e.g. 'Prelude.spec' or similar)
  deriving Int -> SearchLocation -> ShowS
[SearchLocation] -> ShowS
SearchLocation -> String
(Int -> SearchLocation -> ShowS)
-> (SearchLocation -> String)
-> ([SearchLocation] -> ShowS)
-> Show SearchLocation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SearchLocation -> ShowS
showsPrec :: Int -> SearchLocation -> ShowS
$cshow :: SearchLocation -> String
show :: SearchLocation -> String
$cshowList :: [SearchLocation] -> ShowS
showList :: [SearchLocation] -> ShowS
Show

-- | Load any relevant spec for the input list of 'Module's, by querying both the 'ExternalPackageState'
-- and the 'HomePackageTable'.
--
-- Specs come from the interface files of the given modules or their matching
-- _LHAssumptions modules. A module @M@ only matches with a module named
-- @M_LHAssumptions@.
--
-- Assumptions are taken from _LHAssumptions modules only if the interface
-- file of the matching module contains no spec.
findRelevantSpecs :: [String] -- ^ Package to exclude for loading LHAssumptions
                  -> HscEnv
                  -> [Module]
                  -- ^ Any relevant module fetched during dependency-discovery.
                  -> TcM [SpecFinderResult]
findRelevantSpecs :: [String] -> HscEnv -> [Module] -> TcM [SpecFinderResult]
findRelevantSpecs [String]
lhAssmPkgExcludes HscEnv
hscEnv [Module]
mods = do
    ExternalPackageState
eps <- IO ExternalPackageState
-> IOEnv (Env TcGblEnv TcLclEnv) ExternalPackageState
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ExternalPackageState
 -> IOEnv (Env TcGblEnv TcLclEnv) ExternalPackageState)
-> IO ExternalPackageState
-> IOEnv (Env TcGblEnv TcLclEnv) ExternalPackageState
forall a b. (a -> b) -> a -> b
$ IORef ExternalPackageState -> IO ExternalPackageState
forall a. IORef a -> IO a
readIORef (ExternalUnitCache -> IORef ExternalPackageState
euc_eps (ExternalUnitCache -> IORef ExternalPackageState)
-> ExternalUnitCache -> IORef ExternalPackageState
forall a b. (a -> b) -> a -> b
$ UnitEnv -> ExternalUnitCache
ue_eps (UnitEnv -> ExternalUnitCache) -> UnitEnv -> ExternalUnitCache
forall a b. (a -> b) -> a -> b
$ HscEnv -> UnitEnv
hsc_unit_env HscEnv
hscEnv)
    ([SpecFinderResult] -> Module -> TcM [SpecFinderResult])
-> [SpecFinderResult] -> [Module] -> TcM [SpecFinderResult]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ExternalPackageState
-> [SpecFinderResult] -> Module -> TcM [SpecFinderResult]
loadRelevantSpec ExternalPackageState
eps) [SpecFinderResult]
forall a. Monoid a => a
mempty [Module]
mods
  where

    loadRelevantSpec :: ExternalPackageState -> [SpecFinderResult] -> Module -> TcM [SpecFinderResult]
    loadRelevantSpec :: ExternalPackageState
-> [SpecFinderResult] -> Module -> TcM [SpecFinderResult]
loadRelevantSpec ExternalPackageState
eps ![SpecFinderResult]
acc Module
currentModule = do
      Maybe SpecFinderResult
res <- IO (Maybe SpecFinderResult)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe SpecFinderResult)
 -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult))
-> IO (Maybe SpecFinderResult)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult))
-> MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$
        ExternalPackageState -> HomePackageTable -> SpecFinder Any
forall m.
ExternalPackageState -> HomePackageTable -> SpecFinder Any
lookupInterfaceAnnotations ExternalPackageState
eps ((() :: Constraint) => UnitEnv -> HomePackageTable
UnitEnv -> HomePackageTable
ue_hpt (UnitEnv -> HomePackageTable) -> UnitEnv -> HomePackageTable
forall a b. (a -> b) -> a -> b
$ HscEnv -> UnitEnv
hsc_unit_env HscEnv
hscEnv) Module
currentModule
      case Maybe SpecFinderResult
res of
        Maybe SpecFinderResult
Nothing         -> do
          Maybe SpecFinderResult
mAssm <- Module -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall {u}.
IsUnitId u =>
GenModule u
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
loadModuleLHAssumptionsIfAny Module
currentModule
          [SpecFinderResult] -> TcM [SpecFinderResult]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SpecFinderResult] -> TcM [SpecFinderResult])
-> [SpecFinderResult] -> TcM [SpecFinderResult]
forall a b. (a -> b) -> a -> b
$ SpecFinderResult -> Maybe SpecFinderResult -> SpecFinderResult
forall a. a -> Maybe a -> a
fromMaybe (Module -> SpecFinderResult
SpecNotFound Module
currentModule) Maybe SpecFinderResult
mAssm SpecFinderResult -> [SpecFinderResult] -> [SpecFinderResult]
forall a. a -> [a] -> [a]
: [SpecFinderResult]
acc
        Just SpecFinderResult
specResult ->
          [SpecFinderResult] -> TcM [SpecFinderResult]
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SpecFinderResult
specResult SpecFinderResult -> [SpecFinderResult] -> [SpecFinderResult]
forall a. a -> [a] -> [a]
: [SpecFinderResult]
acc)

    loadModuleLHAssumptionsIfAny :: GenModule u
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
loadModuleLHAssumptionsIfAny GenModule u
m | GenModule u -> Bool
forall {u}. IsUnitId u => GenModule u -> Bool
isImportExcluded GenModule u
m = Maybe SpecFinderResult
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SpecFinderResult
forall a. Maybe a
Nothing
                                   | Bool
otherwise = do
      let assumptionsModName :: ModuleName
assumptionsModName = GenModule u -> ModuleName
forall {unit}. GenModule unit -> ModuleName
assumptionsModuleName GenModule u
m
      -- loadInterface might mutate the EPS if the module is
      -- not already loaded
      FindResult
res <- IO FindResult -> IOEnv (Env TcGblEnv TcLclEnv) FindResult
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FindResult -> IOEnv (Env TcGblEnv TcLclEnv) FindResult)
-> IO FindResult -> IOEnv (Env TcGblEnv TcLclEnv) FindResult
forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> PkgQual -> IO FindResult
findImportedModule HscEnv
hscEnv ModuleName
assumptionsModName PkgQual
NoPkgQual
      case FindResult
res of
        Found ModLocation
_ Module
assumptionsMod -> do
          MaybeErr SDoc ModIface
_ <- IfG (MaybeErr SDoc ModIface) -> TcRn (MaybeErr SDoc ModIface)
forall a. IfG a -> TcRn a
initIfaceTcRn (IfG (MaybeErr SDoc ModIface) -> TcRn (MaybeErr SDoc ModIface))
-> IfG (MaybeErr SDoc ModIface) -> TcRn (MaybeErr SDoc ModIface)
forall a b. (a -> b) -> a -> b
$ SDoc -> Module -> WhereFrom -> IfG (MaybeErr SDoc ModIface)
forall lcl.
SDoc -> Module -> WhereFrom -> IfM lcl (MaybeErr SDoc ModIface)
loadInterface SDoc
"liquidhaskell assumptions" Module
assumptionsMod WhereFrom
ImportBySystem
          -- read the EPS again
          ExternalPackageState
eps2 <- IO ExternalPackageState
-> IOEnv (Env TcGblEnv TcLclEnv) ExternalPackageState
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ExternalPackageState
 -> IOEnv (Env TcGblEnv TcLclEnv) ExternalPackageState)
-> IO ExternalPackageState
-> IOEnv (Env TcGblEnv TcLclEnv) ExternalPackageState
forall a b. (a -> b) -> a -> b
$ IORef ExternalPackageState -> IO ExternalPackageState
forall a. IORef a -> IO a
readIORef (ExternalUnitCache -> IORef ExternalPackageState
euc_eps (ExternalUnitCache -> IORef ExternalPackageState)
-> ExternalUnitCache -> IORef ExternalPackageState
forall a b. (a -> b) -> a -> b
$ UnitEnv -> ExternalUnitCache
ue_eps (UnitEnv -> ExternalUnitCache) -> UnitEnv -> ExternalUnitCache
forall a b. (a -> b) -> a -> b
$ HscEnv -> UnitEnv
hsc_unit_env HscEnv
hscEnv)
          -- now look up the assumptions
          IO (Maybe SpecFinderResult)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a. IO a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe SpecFinderResult)
 -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult))
-> IO (Maybe SpecFinderResult)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult))
-> MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ ExternalPackageState -> SpecFinder Any
forall m. ExternalPackageState -> SpecFinder Any
lookupInterfaceAnnotationsEPS ExternalPackageState
eps2 Module
assumptionsMod
        FoundMultiple{} -> TcRnMessage
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a. TcRnMessage -> TcM a
failWithTc (TcRnMessage
 -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult))
-> TcRnMessage
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ DiagnosticMessage -> TcRnMessage
forall a.
(Diagnostic a, Typeable a, DiagnosticOpts a ~ NoDiagnosticOpts) =>
a -> TcRnMessage
mkTcRnUnknownMessage (DiagnosticMessage -> TcRnMessage)
-> DiagnosticMessage -> TcRnMessage
forall a b. (a -> b) -> a -> b
$ [GhcHint] -> SDoc -> DiagnosticMessage
mkPlainError [] (SDoc -> DiagnosticMessage) -> SDoc -> DiagnosticMessage
forall a b. (a -> b) -> a -> b
$
                             HscEnv -> ModuleName -> FindResult -> SDoc
cannotFindModule HscEnv
hscEnv ModuleName
assumptionsModName FindResult
res
        FindResult
_ -> Maybe SpecFinderResult
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SpecFinderResult
forall a. Maybe a
Nothing

    isImportExcluded :: GenModule u -> Bool
isImportExcluded GenModule u
m =
      let s :: String
s = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
Data.Char.isAlphaNum ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ u -> String
forall u. IsUnitId u => u -> String
unitString (GenModule u -> u
forall unit. GenModule unit -> unit
moduleUnit GenModule u
m)
       in String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
s [String]
lhAssmPkgExcludes

    assumptionsModuleName :: GenModule unit -> ModuleName
assumptionsModuleName GenModule unit
m =
      FastString -> ModuleName
mkModuleNameFS (FastString -> ModuleName) -> FastString -> ModuleName
forall a b. (a -> b) -> a -> b
$ ModuleName -> FastString
moduleNameFS (GenModule unit -> ModuleName
forall {unit}. GenModule unit -> ModuleName
moduleName GenModule unit
m) FastString -> FastString -> FastString
forall a. Semigroup a => a -> a -> a
<> FastString
"_LHAssumptions"

-- | If this module has a \"companion\" '.spec' file sitting next to it, this 'SpecFinder'
-- will try loading it.
findCompanionSpec :: HscEnv -> Module -> IO SpecFinderResult
findCompanionSpec :: HscEnv -> Module -> IO SpecFinderResult
findCompanionSpec HscEnv
hscEnv Module
m = do
  Maybe SpecFinderResult
res <- MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult))
-> MaybeT IO SpecFinderResult -> IO (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ HscEnv -> SpecFinder Any
forall m. HscEnv -> SpecFinder Any
lookupCompanionSpec HscEnv
hscEnv Module
m
  case Maybe SpecFinderResult
res of
    Maybe SpecFinderResult
Nothing -> SpecFinderResult -> IO SpecFinderResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> IO SpecFinderResult)
-> SpecFinderResult -> IO SpecFinderResult
forall a b. (a -> b) -> a -> b
$ Module -> SpecFinderResult
SpecNotFound Module
m
    Just SpecFinderResult
s  -> SpecFinderResult -> IO SpecFinderResult
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SpecFinderResult
s

-- | Load a spec by trying to parse the relevant \".spec\" file from the filesystem.
lookupInterfaceAnnotations :: ExternalPackageState -> HomePackageTable -> SpecFinder m
lookupInterfaceAnnotations :: forall m.
ExternalPackageState -> HomePackageTable -> SpecFinder Any
lookupInterfaceAnnotations ExternalPackageState
eps HomePackageTable
hpt Module
thisModule = do
  LiquidLib
lib <- IO (Maybe LiquidLib) -> MaybeT IO LiquidLib
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe LiquidLib) -> MaybeT IO LiquidLib)
-> IO (Maybe LiquidLib) -> MaybeT IO LiquidLib
forall a b. (a -> b) -> a -> b
$ Maybe LiquidLib -> IO (Maybe LiquidLib)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe LiquidLib -> IO (Maybe LiquidLib))
-> Maybe LiquidLib -> IO (Maybe LiquidLib)
forall a b. (a -> b) -> a -> b
$ Module
-> ExternalPackageState -> HomePackageTable -> Maybe LiquidLib
Util.deserialiseLiquidLib Module
thisModule ExternalPackageState
eps HomePackageTable
hpt
  SpecFinderResult -> MaybeT IO SpecFinderResult
forall a. a -> MaybeT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> MaybeT IO SpecFinderResult)
-> SpecFinderResult -> MaybeT IO SpecFinderResult
forall a b. (a -> b) -> a -> b
$ Module -> SearchLocation -> LiquidLib -> SpecFinderResult
LibFound Module
thisModule SearchLocation
InterfaceLocation LiquidLib
lib

lookupInterfaceAnnotationsEPS :: ExternalPackageState -> SpecFinder m
lookupInterfaceAnnotationsEPS :: forall m. ExternalPackageState -> SpecFinder Any
lookupInterfaceAnnotationsEPS ExternalPackageState
eps Module
thisModule = do
  LiquidLib
lib <- IO (Maybe LiquidLib) -> MaybeT IO LiquidLib
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe LiquidLib) -> MaybeT IO LiquidLib)
-> IO (Maybe LiquidLib) -> MaybeT IO LiquidLib
forall a b. (a -> b) -> a -> b
$ Maybe LiquidLib -> IO (Maybe LiquidLib)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe LiquidLib -> IO (Maybe LiquidLib))
-> Maybe LiquidLib -> IO (Maybe LiquidLib)
forall a b. (a -> b) -> a -> b
$ Module -> ExternalPackageState -> Maybe LiquidLib
Util.deserialiseLiquidLibFromEPS Module
thisModule ExternalPackageState
eps
  SpecFinderResult -> MaybeT IO SpecFinderResult
forall a. a -> MaybeT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> MaybeT IO SpecFinderResult)
-> SpecFinderResult -> MaybeT IO SpecFinderResult
forall a b. (a -> b) -> a -> b
$ Module -> SearchLocation -> LiquidLib -> SpecFinderResult
LibFound Module
thisModule SearchLocation
InterfaceLocation LiquidLib
lib

-- | If this module has a \"companion\" '.spec' file sitting next to it, this 'SpecFinder'
-- will try loading it.
lookupCompanionSpec :: HscEnv -> SpecFinder m
lookupCompanionSpec :: forall m. HscEnv -> SpecFinder Any
lookupCompanionSpec HscEnv
hscEnv Module
thisModule = do

  ModSummary
modSummary <- IO (Maybe ModSummary) -> MaybeT IO ModSummary
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe ModSummary) -> MaybeT IO ModSummary)
-> IO (Maybe ModSummary) -> MaybeT IO ModSummary
forall a b. (a -> b) -> a -> b
$ Maybe ModSummary -> IO (Maybe ModSummary)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ModSummary -> IO (Maybe ModSummary))
-> Maybe ModSummary -> IO (Maybe ModSummary)
forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> Maybe ModSummary
lookupModSummary HscEnv
hscEnv (Module -> ModuleName
forall {unit}. GenModule unit -> ModuleName
moduleName Module
thisModule)
  String
file       <- IO (Maybe String) -> MaybeT IO String
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO (Maybe String) -> MaybeT IO String)
-> IO (Maybe String) -> MaybeT IO String
forall a b. (a -> b) -> a -> b
$ Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModLocation -> Maybe String
ml_hs_file (ModLocation -> Maybe String)
-> (ModSummary -> ModLocation) -> ModSummary -> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModSummary -> ModLocation
ms_location (ModSummary -> Maybe String) -> ModSummary -> Maybe String
forall a b. (a -> b) -> a -> b
$ ModSummary
modSummary)
  Either (ParseErrorBundle String Void) (ModName, BareSpec)
parsed     <- IO
  (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
-> MaybeT
     IO (Either (ParseErrorBundle String Void) (ModName, BareSpec))
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IO
   (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
 -> MaybeT
      IO (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
-> IO
     (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
-> MaybeT
     IO (Either (ParseErrorBundle String Void) (ModName, BareSpec))
forall a b. (a -> b) -> a -> b
$ do
    Either SomeException String
mbSpecContent <- IO String -> IO (Either SomeException String)
forall e a. Exception e => IO a -> IO (Either e a)
try (String -> IO String
Misc.sayReadFile (ShowS
specFile String
file))
    case Either SomeException String
mbSpecContent of
      Left (SomeException
_e :: SomeException) -> Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec))
-> IO
     (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec))
forall a. Maybe a
Nothing
      Right String
raw -> Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec))
-> IO
     (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec))
 -> IO
      (Maybe
         (Either (ParseErrorBundle String Void) (ModName, BareSpec))))
-> Maybe
     (Either (ParseErrorBundle String Void) (ModName, BareSpec))
-> IO
     (Maybe (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
forall a b. (a -> b) -> a -> b
$ Either (ParseErrorBundle String Void) (ModName, BareSpec)
-> Maybe
     (Either (ParseErrorBundle String Void) (ModName, BareSpec))
forall a. a -> Maybe a
Just (Either (ParseErrorBundle String Void) (ModName, BareSpec)
 -> Maybe
      (Either (ParseErrorBundle String Void) (ModName, BareSpec)))
-> Either (ParseErrorBundle String Void) (ModName, BareSpec)
-> Maybe
     (Either (ParseErrorBundle String Void) (ModName, BareSpec))
forall a b. (a -> b) -> a -> b
$ String
-> String
-> Either (ParseErrorBundle String Void) (ModName, BareSpec)
specSpecificationP (ShowS
specFile String
file) String
raw

  case Either (ParseErrorBundle String Void) (ModName, BareSpec)
parsed of
    Left ParseErrorBundle String Void
peb -> do
      let errMsg :: SDoc
errMsg = String -> SDoc
forall doc. IsLine doc => String -> doc
O.text String
"Error when parsing "
             SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
O.<+> String -> SDoc
forall doc. IsLine doc => String -> doc
O.text (ShowS
specFile String
file) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
O.<+> String -> SDoc
forall doc. IsLine doc => String -> doc
O.text String
":"
             SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
O.<+> String -> SDoc
forall doc. IsLine doc => String -> doc
O.text (ParseErrorBundle String Void -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
peb)
      IO SpecFinderResult -> MaybeT IO SpecFinderResult
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO SpecFinderResult -> MaybeT IO SpecFinderResult)
-> IO SpecFinderResult -> MaybeT IO SpecFinderResult
forall a b. (a -> b) -> a -> b
$ String -> IO SpecFinderResult
forall (m :: * -> *) a. MonadIO m => String -> m a
Util.pluginAbort (DynFlags -> SDoc -> String
O.showSDoc (HscEnv -> DynFlags
hsc_dflags HscEnv
hscEnv) SDoc
errMsg)
    Right (ModName
_, BareSpec
spec) -> do
      let bareSpec :: BareSpec
bareSpec = BareSpec -> BareSpec
toBareSpec BareSpec
spec
      SpecFinderResult -> MaybeT IO SpecFinderResult
forall a. a -> MaybeT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> MaybeT IO SpecFinderResult)
-> SpecFinderResult -> MaybeT IO SpecFinderResult
forall a b. (a -> b) -> a -> b
$ Module -> SearchLocation -> BareSpec -> SpecFinderResult
SpecFound Module
thisModule SearchLocation
DiskLocation BareSpec
bareSpec
  where
    specFile :: FilePath -> FilePath
    specFile :: ShowS
specFile String
fp = String -> Ext -> String
withExt String
fp Ext
Spec

-- | Returns a list of 'StableModule's which can be filtered out of the dependency list, because they are
-- selectively \"toggled\" on and off by the LiquidHaskell's configuration, which granularity can be
-- /per module/.
configToRedundantDependencies :: HscEnv -> Config -> IO [StableModule]
configToRedundantDependencies :: HscEnv -> Config -> IO [StableModule]
configToRedundantDependencies HscEnv
env Config
cfg = do
  [Maybe StableModule] -> [StableModule]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe StableModule] -> [StableModule])
-> IO [Maybe StableModule] -> IO [StableModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Config -> Bool, ModuleName) -> IO (Maybe StableModule))
-> [(Config -> Bool, ModuleName)] -> IO [Maybe StableModule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Bool, ModuleName) -> IO (Maybe StableModule)
lookupModule' ((Bool, ModuleName) -> IO (Maybe StableModule))
-> ((Config -> Bool, ModuleName) -> (Bool, ModuleName))
-> (Config -> Bool, ModuleName)
-> IO (Maybe StableModule)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Config -> Bool) -> Bool)
-> (Config -> Bool, ModuleName) -> (Bool, ModuleName)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ Config
cfg)) [(Config -> Bool, ModuleName)]
configSensitiveDependencies
  where
    lookupModule' :: (Bool, ModuleName) -> IO (Maybe StableModule)
    lookupModule' :: (Bool, ModuleName) -> IO (Maybe StableModule)
lookupModule' (Bool
fetchModule, ModuleName
modName)
      | Bool
fetchModule = ModuleName -> IO (Maybe StableModule)
lookupLiquidBaseModule ModuleName
modName
      | Bool
otherwise   = Maybe StableModule -> IO (Maybe StableModule)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe StableModule
forall a. Maybe a
Nothing

    lookupLiquidBaseModule :: ModuleName -> IO (Maybe StableModule)
    lookupLiquidBaseModule :: ModuleName -> IO (Maybe StableModule)
lookupLiquidBaseModule ModuleName
mn = do
      FindResult
res <- HscEnv -> ModuleName -> PkgQual -> IO FindResult
findImportedModule HscEnv
env ModuleName
mn (UnitEnv -> ModuleName -> Maybe FastString -> PkgQual
renamePkgQual (HscEnv -> UnitEnv
hsc_unit_env HscEnv
env) ModuleName
mn (FastString -> Maybe FastString
forall a. a -> Maybe a
Just FastString
"liquidhaskell"))
      case FindResult
res of
        Found ModLocation
_ Module
mdl -> Maybe StableModule -> IO (Maybe StableModule)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe StableModule -> IO (Maybe StableModule))
-> Maybe StableModule -> IO (Maybe StableModule)
forall a b. (a -> b) -> a -> b
$ StableModule -> Maybe StableModule
forall a. a -> Maybe a
Just (Module -> StableModule
toStableModule Module
mdl)
        FindResult
_           -> Maybe StableModule -> IO (Maybe StableModule)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe StableModule
forall a. Maybe a
Nothing

-- | Static associative map of the 'ModuleName' that needs to be filtered from the final 'TargetDependencies'
-- due to some particular configuration options.
--
-- Modify this map to add any extra special case. Remember that the semantic is not which module will be
-- /added/, but rather which one will be /removed/ from the final list of dependencies.
--
configSensitiveDependencies :: [(Config -> Bool, ModuleName)]
configSensitiveDependencies :: [(Config -> Bool, ModuleName)]
configSensitiveDependencies = [
    (Bool -> Bool
not (Bool -> Bool) -> (Config -> Bool) -> Config -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Bool
forall t. HasConfig t => t -> Bool
totalityCheck, String -> ModuleName
mkModuleName String
"Liquid.Prelude.Totality_LHAssumptions")
  , (Config -> Bool
linear, String -> ModuleName
mkModuleName String
"Liquid.Prelude.Real_LHAssumptions")
  ]