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

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

import qualified Language.Haskell.Liquid.GHC.Plugin.Serialisation as Serialisation
import           Language.Haskell.Liquid.GHC.Plugin.Types
import           Language.Haskell.Liquid.UX.Config

import           Liquid.GHC.API         as GHC

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

import           Control.Monad.Trans.Maybe


type SpecFinder m = Module -> MaybeT IO SpecFinderResult

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

-- | 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
    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)
    mapM (loadRelevantSpec eps) mods
  where

    loadRelevantSpec :: ExternalPackageState -> Module -> TcM SpecFinderResult
    loadRelevantSpec :: ExternalPackageState
-> Module -> IOEnv (Env TcGblEnv TcLclEnv) SpecFinderResult
loadRelevantSpec ExternalPackageState
eps Module
currentModule = do
      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 -> NameCache -> SpecFinder Any
forall m.
ExternalPackageState
-> HomePackageTable -> NameCache -> SpecFinder Any
lookupInterfaceAnnotations ExternalPackageState
eps (HasDebugCallStack => UnitEnv -> HomePackageTable
UnitEnv -> HomePackageTable
ue_hpt (UnitEnv -> HomePackageTable) -> UnitEnv -> HomePackageTable
forall a b. (a -> b) -> a -> b
$ HscEnv -> UnitEnv
hsc_unit_env HscEnv
hscEnv) (HscEnv -> NameCache
hsc_NC HscEnv
hscEnv) Module
currentModule
      case res of
        Maybe SpecFinderResult
Nothing         -> do
          mAssm <- Module -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
forall {u}.
IsUnitId u =>
GenModule u
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
loadModuleLHAssumptionsIfAny Module
currentModule
          return $ fromMaybe (SpecNotFound currentModule) mAssm
        Just SpecFinderResult
specResult ->
          SpecFinderResult -> IOEnv (Env TcGblEnv TcLclEnv) SpecFinderResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return SpecFinderResult
specResult

    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
      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 res of
        Found ModLocation
_ Module
assumptionsMod -> do
          _ <- IfG (MaybeErr MissingInterfaceError ModIface)
-> TcRn (MaybeErr MissingInterfaceError ModIface)
forall a. IfG a -> TcRn a
initIfaceTcRn (IfG (MaybeErr MissingInterfaceError ModIface)
 -> TcRn (MaybeErr MissingInterfaceError ModIface))
-> IfG (MaybeErr MissingInterfaceError ModIface)
-> TcRn (MaybeErr MissingInterfaceError ModIface)
forall a b. (a -> b) -> a -> b
$ SDoc
-> Module
-> WhereFrom
-> IfG (MaybeErr MissingInterfaceError ModIface)
forall lcl.
SDoc
-> Module
-> WhereFrom
-> IfM lcl (MaybeErr MissingInterfaceError ModIface)
loadInterface SDoc
"liquidhaskell assumptions" Module
assumptionsMod WhereFrom
ImportBySystem
          -- read the EPS again
          eps2 <- liftIO $ readIORef (euc_eps $ ue_eps $ hsc_unit_env hscEnv)
          -- now look up the assumptions
          liftIO $ runMaybeT $ lookupInterfaceAnnotationsEPS eps2 (hsc_NC hscEnv) 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
$
                             IfaceMessageOpts -> MissingInterfaceError -> SDoc
missingInterfaceErrorDiagnostic (DynFlags -> DiagnosticOpts IfaceMessage
initIfaceMessageOpts (DynFlags -> DiagnosticOpts IfaceMessage)
-> DynFlags -> DiagnosticOpts IfaceMessage
forall a b. (a -> b) -> a -> b
$ HscEnv -> DynFlags
hsc_dflags HscEnv
hscEnv) (MissingInterfaceError -> SDoc) -> MissingInterfaceError -> SDoc
forall a b. (a -> b) -> a -> b
$
                             HscEnv -> ModuleName -> FindResult -> MissingInterfaceError
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) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
Data.Char.isAlphaNum (String -> String) -> String -> String
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"

-- | Load specs from an interface file.
lookupInterfaceAnnotations :: ExternalPackageState -> HomePackageTable -> NameCache -> SpecFinder m
lookupInterfaceAnnotations :: forall m.
ExternalPackageState
-> HomePackageTable -> NameCache -> SpecFinder Any
lookupInterfaceAnnotations ExternalPackageState
eps HomePackageTable
hpt NameCache
nameCache Module
thisModule = do
  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
$ Module
-> ExternalPackageState
-> HomePackageTable
-> NameCache
-> IO (Maybe LiquidLib)
Serialisation.deserialiseLiquidLib Module
thisModule ExternalPackageState
eps HomePackageTable
hpt NameCache
nameCache
  pure $ LibFound thisModule lib

lookupInterfaceAnnotationsEPS :: ExternalPackageState -> NameCache -> SpecFinder m
lookupInterfaceAnnotationsEPS :: forall m. ExternalPackageState -> NameCache -> SpecFinder Any
lookupInterfaceAnnotationsEPS ExternalPackageState
eps NameCache
nameCache Module
thisModule = do
  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
$ Module -> ExternalPackageState -> NameCache -> IO (Maybe LiquidLib)
Serialisation.deserialiseLiquidLibFromEPS Module
thisModule ExternalPackageState
eps NameCache
nameCache
  pure $ LibFound thisModule lib

-- | 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
      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 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")
  ]