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

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

import           Language.Haskell.Liquid.GHC.GhcMonadLike as GhcMonadLike ( GhcMonadLike
                                                                          , lookupModSummary
                                                                          , askHscEnv
                                                                          )
import           Language.Haskell.Liquid.GHC.Plugin.Util  ( pluginAbort, deserialiseLiquidLib )
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           Optics
import qualified Outputable                              as O
import           GHC                                     hiding (lookupModule)
import           HscTypes
import           CoreMonad                                ( getDynFlags )
import           Finder                                   ( findExposedPackageModule
                                                          )

import           Data.Bifunctor
import           Data.Foldable
import           Data.Maybe

import           Control.Exception
import           Control.Monad.IO.Class
import           Control.Monad.Trans                      ( lift )
import           Control.Monad.Trans.Maybe

type SpecFinder m = GhcMonadLike m => Module -> MaybeT m 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
showList :: [SearchLocation] -> ShowS
$cshowList :: [SearchLocation] -> ShowS
show :: SearchLocation -> String
$cshow :: SearchLocation -> String
showsPrec :: Int -> SearchLocation -> ShowS
$cshowsPrec :: Int -> SearchLocation -> ShowS
Show

-- | Load any relevant spec in the input 'SpecEnv', by updating it. The update will happen only if necessary,
-- i.e. if the spec is not already present.
findRelevantSpecs :: forall m. GhcMonadLike m 
                  => ExternalPackageState
                  -> HomePackageTable
                  -> [Module]
                  -- ^ Any relevant module fetched during dependency-discovery.
                  -> m [SpecFinderResult]
findRelevantSpecs :: ExternalPackageState
-> HomePackageTable -> [Module] -> m [SpecFinderResult]
findRelevantSpecs ExternalPackageState
eps HomePackageTable
hpt [Module]
mods = do
  [SpecFinderResult]
res  <- ([SpecFinderResult] -> Module -> m [SpecFinderResult])
-> [SpecFinderResult] -> [Module] -> m [SpecFinderResult]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM [SpecFinderResult] -> Module -> m [SpecFinderResult]
loadRelevantSpec [SpecFinderResult]
forall a. Monoid a => a
mempty [Module]
mods
  [SpecFinderResult] -> m [SpecFinderResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [SpecFinderResult]
res
  where

    loadRelevantSpec :: [SpecFinderResult] -> Module -> m [SpecFinderResult]
    loadRelevantSpec :: [SpecFinderResult] -> Module -> m [SpecFinderResult]
loadRelevantSpec ![SpecFinderResult]
acc Module
currentModule = do
      Maybe SpecFinderResult
res <- MaybeT m SpecFinderResult -> m (Maybe SpecFinderResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m SpecFinderResult -> m (Maybe SpecFinderResult))
-> MaybeT m SpecFinderResult -> m (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ ExternalPackageState
-> HomePackageTable -> Module -> MaybeT m SpecFinderResult
forall (m :: * -> *).
ExternalPackageState -> HomePackageTable -> SpecFinder m
lookupInterfaceAnnotations ExternalPackageState
eps HomePackageTable
hpt Module
currentModule
      [SpecFinderResult] -> m [SpecFinderResult]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([SpecFinderResult] -> m [SpecFinderResult])
-> [SpecFinderResult] -> m [SpecFinderResult]
forall a b. (a -> b) -> a -> b
$ case Maybe SpecFinderResult
res of
        Maybe SpecFinderResult
Nothing         -> Module -> SpecFinderResult
SpecNotFound Module
currentModule SpecFinderResult -> [SpecFinderResult] -> [SpecFinderResult]
forall a. a -> [a] -> [a]
: [SpecFinderResult]
acc
        Just SpecFinderResult
specResult -> SpecFinderResult
specResult SpecFinderResult -> [SpecFinderResult] -> [SpecFinderResult]
forall a. a -> [a] -> [a]
: [SpecFinderResult]
acc

-- | If this module has a \"companion\" '.spec' file sitting next to it, this 'SpecFinder'
-- will try loading it.
findCompanionSpec :: GhcMonadLike m => Module -> m SpecFinderResult
findCompanionSpec :: Module -> m SpecFinderResult
findCompanionSpec Module
m = do
  Maybe SpecFinderResult
res <- MaybeT m SpecFinderResult -> m (Maybe SpecFinderResult)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT m SpecFinderResult -> m (Maybe SpecFinderResult))
-> MaybeT m SpecFinderResult -> m (Maybe SpecFinderResult)
forall a b. (a -> b) -> a -> b
$ Module -> MaybeT m SpecFinderResult
forall (m :: * -> *). SpecFinder m
lookupCompanionSpec Module
m
  case Maybe SpecFinderResult
res of
    Maybe SpecFinderResult
Nothing -> SpecFinderResult -> m SpecFinderResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> m SpecFinderResult)
-> SpecFinderResult -> m SpecFinderResult
forall a b. (a -> b) -> a -> b
$ Module -> SpecFinderResult
SpecNotFound Module
m
    Just SpecFinderResult
s  -> SpecFinderResult -> m SpecFinderResult
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 :: ExternalPackageState -> HomePackageTable -> SpecFinder m
lookupInterfaceAnnotations ExternalPackageState
eps HomePackageTable
hpt Module
thisModule = do
  LiquidLib
lib <- m (Maybe LiquidLib) -> MaybeT m LiquidLib
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe LiquidLib) -> MaybeT m LiquidLib)
-> m (Maybe LiquidLib) -> MaybeT m LiquidLib
forall a b. (a -> b) -> a -> b
$ Maybe LiquidLib -> m (Maybe LiquidLib)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe LiquidLib -> m (Maybe LiquidLib))
-> Maybe LiquidLib -> m (Maybe LiquidLib)
forall a b. (a -> b) -> a -> b
$ Module
-> ExternalPackageState -> HomePackageTable -> Maybe LiquidLib
deserialiseLiquidLib Module
thisModule ExternalPackageState
eps HomePackageTable
hpt
  SpecFinderResult -> MaybeT m SpecFinderResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> MaybeT m SpecFinderResult)
-> SpecFinderResult -> MaybeT m 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 :: SpecFinder m
lookupCompanionSpec :: Module -> MaybeT m SpecFinderResult
lookupCompanionSpec Module
thisModule = do

  ModSummary
modSummary <- m (Maybe ModSummary) -> MaybeT m ModSummary
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe ModSummary) -> MaybeT m ModSummary)
-> m (Maybe ModSummary) -> MaybeT m ModSummary
forall a b. (a -> b) -> a -> b
$ ModuleName -> m (Maybe ModSummary)
forall (m :: * -> *).
GhcMonadLike m =>
ModuleName -> m (Maybe ModSummary)
GhcMonadLike.lookupModSummary (Module -> ModuleName
moduleName Module
thisModule)
  String
file       <- m (Maybe String) -> MaybeT m String
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe String) -> MaybeT m String)
-> m (Maybe String) -> MaybeT m String
forall a b. (a -> b) -> a -> b
$ Maybe String -> m (Maybe String)
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 Error (ModName, BareSpec)
parsed     <- m (Maybe (Either Error (ModName, BareSpec)))
-> MaybeT m (Either Error (ModName, BareSpec))
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe (Either Error (ModName, BareSpec)))
 -> MaybeT m (Either Error (ModName, BareSpec)))
-> m (Maybe (Either Error (ModName, BareSpec)))
-> MaybeT m (Either Error (ModName, BareSpec))
forall a b. (a -> b) -> a -> b
$ do
    Either SomeException String
mbSpecContent <- IO (Either SomeException String) -> m (Either SomeException String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either SomeException String)
 -> m (Either SomeException String))
-> IO (Either SomeException String)
-> m (Either SomeException String)
forall a b. (a -> b) -> a -> b
$ 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 Error (ModName, BareSpec))
-> m (Maybe (Either Error (ModName, BareSpec)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Either Error (ModName, BareSpec))
forall a. Maybe a
Nothing
      Right String
raw -> Maybe (Either Error (ModName, BareSpec))
-> m (Maybe (Either Error (ModName, BareSpec)))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Either Error (ModName, BareSpec))
 -> m (Maybe (Either Error (ModName, BareSpec))))
-> Maybe (Either Error (ModName, BareSpec))
-> m (Maybe (Either Error (ModName, BareSpec)))
forall a b. (a -> b) -> a -> b
$ Either Error (ModName, BareSpec)
-> Maybe (Either Error (ModName, BareSpec))
forall a. a -> Maybe a
Just (Either Error (ModName, BareSpec)
 -> Maybe (Either Error (ModName, BareSpec)))
-> Either Error (ModName, BareSpec)
-> Maybe (Either Error (ModName, BareSpec))
forall a b. (a -> b) -> a -> b
$ String -> String -> Either Error (ModName, BareSpec)
specSpecificationP (ShowS
specFile String
file) String
raw

  case Either Error (ModName, BareSpec)
parsed of
    Left Error
parsingError -> do
      DynFlags
dynFlags <- m DynFlags -> MaybeT m DynFlags
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
      let errMsg :: SDoc
errMsg = String -> SDoc
O.text String
"Error when parsing " 
             SDoc -> SDoc -> SDoc
O.<+> String -> SDoc
O.text (ShowS
specFile String
file) SDoc -> SDoc -> SDoc
O.<+> String -> SDoc
O.text String
":"
             SDoc -> SDoc -> SDoc
O.<+> String -> SDoc
O.text (Error -> String
forall a. Show a => a -> String
show Error
parsingError)
      m SpecFinderResult -> MaybeT m SpecFinderResult
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m SpecFinderResult -> MaybeT m SpecFinderResult)
-> m SpecFinderResult -> MaybeT m SpecFinderResult
forall a b. (a -> b) -> a -> b
$ String -> m SpecFinderResult
forall (m :: * -> *) a. MonadIO m => String -> m a
pluginAbort (DynFlags -> SDoc -> String
O.showSDoc DynFlags
dynFlags SDoc
errMsg)
    Right (ModName
_, BareSpec
spec) -> do
      let bareSpec :: BareSpec
bareSpec = Optic' An_Iso NoIx BareSpec BareSpec -> BareSpec -> BareSpec
forall k (is :: IxList) s a.
Is k A_Getter =>
Optic' k is s a -> s -> a
view Optic' An_Iso NoIx BareSpec BareSpec
bareSpecIso BareSpec
spec
      SpecFinderResult -> MaybeT m SpecFinderResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SpecFinderResult -> MaybeT m SpecFinderResult)
-> SpecFinderResult -> MaybeT m 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 :: forall m. GhcMonadLike m => Config -> m [StableModule]
configToRedundantDependencies :: Config -> m [StableModule]
configToRedundantDependencies Config
cfg = do
  HscEnv
env <- m HscEnv
forall (m :: * -> *). HasHscEnv m => m HscEnv
askHscEnv
  [Maybe StableModule] -> [StableModule]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe StableModule] -> [StableModule])
-> m [Maybe StableModule] -> m [StableModule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Config -> Bool, ModuleName) -> m (Maybe StableModule))
-> [(Config -> Bool, ModuleName)] -> m [Maybe StableModule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (HscEnv -> (Bool, ModuleName) -> m (Maybe StableModule)
lookupModule HscEnv
env ((Bool, ModuleName) -> m (Maybe StableModule))
-> ((Config -> Bool, ModuleName) -> (Bool, ModuleName))
-> (Config -> Bool, ModuleName)
-> m (Maybe StableModule)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Config -> Bool) -> Bool)
-> (Config -> Bool, ModuleName) -> (Bool, ModuleName)
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 :: HscEnv -> (Bool, ModuleName) -> m (Maybe StableModule)
    lookupModule :: HscEnv -> (Bool, ModuleName) -> m (Maybe StableModule)
lookupModule HscEnv
env (Bool
fetchModule, ModuleName
modName)
      | Bool
fetchModule = IO (Maybe StableModule) -> m (Maybe StableModule)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe StableModule) -> m (Maybe StableModule))
-> IO (Maybe StableModule) -> m (Maybe StableModule)
forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> IO (Maybe StableModule)
lookupLiquidBaseModule HscEnv
env ModuleName
modName
      | Bool
otherwise   = Maybe StableModule -> m (Maybe StableModule)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe StableModule
forall a. Maybe a
Nothing

    lookupLiquidBaseModule :: HscEnv -> ModuleName -> IO (Maybe StableModule)
    lookupLiquidBaseModule :: HscEnv -> ModuleName -> IO (Maybe StableModule)
lookupLiquidBaseModule HscEnv
env ModuleName
mn = do
      FindResult
res <- IO FindResult -> IO FindResult
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FindResult -> IO FindResult) -> IO FindResult -> IO FindResult
forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> Maybe FastString -> IO FindResult
findExposedPackageModule HscEnv
env ModuleName
mn (FastString -> Maybe FastString
forall a. a -> Maybe a
Just FastString
"liquid-base")
      case FindResult
res of
        Found ModLocation
_ Module
mdl -> Maybe StableModule -> IO (Maybe StableModule)
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 (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")
  , (Bool -> Bool
not (Bool -> Bool) -> (Config -> Bool) -> Config -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config -> Bool
linear, String -> ModuleName
mkModuleName String
"Liquid.Prelude.NotReal")
  , (Config -> Bool
linear, String -> ModuleName
mkModuleName String
"Liquid.Prelude.Real")
  ]