{-# 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
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 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef (HscEnv -> IORef ExternalPackageState
hsc_EPS HscEnv
hscEnv)
    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) 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$
        forall m. ExternalPackageState -> HomePackageTable -> SpecFinder m
lookupInterfaceAnnotations ExternalPackageState
eps (HscEnv -> HomePackageTable
hsc_HPT HscEnv
hscEnv) Module
currentModule
      case Maybe SpecFinderResult
res of
        Maybe SpecFinderResult
Nothing         -> do
          Maybe SpecFinderResult
mAssm <- forall {u}.
IsUnitId u =>
GenModule u
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
loadModuleLHAssumptionsIfAny Module
currentModule
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe (Module -> SpecFinderResult
SpecNotFound Module
currentModule) Maybe SpecFinderResult
mAssm forall a. a -> [a] -> [a]
: [SpecFinderResult]
acc
        Just SpecFinderResult
specResult ->
          forall (m :: * -> *) a. Monad m => a -> m a
return (SpecFinderResult
specResult forall a. a -> [a] -> [a]
: [SpecFinderResult]
acc)

    loadModuleLHAssumptionsIfAny :: GenModule u
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe SpecFinderResult)
loadModuleLHAssumptionsIfAny GenModule u
m | forall {u}. IsUnitId u => GenModule u -> Bool
isImportExcluded GenModule u
m = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                                   | Bool
otherwise = do
      let assModName :: ModuleName
assModName = forall {unit}. GenModule unit -> ModuleName
assumptionsModuleName GenModule u
m
      -- loadInterface might mutate the EPS if the module is
      -- not already loaded
      FindResult
res <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> Maybe FastString -> IO FindResult
findImportedModule HscEnv
hscEnv ModuleName
assModName forall a. Maybe a
Nothing
      case FindResult
res of
        Found ModLocation
_ Module
assMod -> do
          MaybeErr SDoc ModIface
_ <- forall a. IfG a -> TcRn a
initIfaceTcRn forall a b. (a -> b) -> a -> b
$ forall lcl.
SDoc -> Module -> WhereFrom -> IfM lcl (MaybeErr SDoc ModIface)
loadInterface SDoc
"liquidhaskell assumptions" Module
assMod WhereFrom
ImportBySystem
          -- read the EPS again
          ExternalPackageState
eps2 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef (HscEnv -> IORef ExternalPackageState
hsc_EPS HscEnv
hscEnv)
          -- now look up the assumptions
          forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ forall m. ExternalPackageState -> SpecFinder m
lookupInterfaceAnnotationsEPS ExternalPackageState
eps2 Module
assMod
        FoundMultiple{} -> forall a. SDoc -> TcM a
failWithTc forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> FindResult -> SDoc
cannotFindModule HscEnv
hscEnv ModuleName
assModName FindResult
res
        FindResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

    isImportExcluded :: GenModule u -> Bool
isImportExcluded GenModule u
m =
      let s :: String
s = forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
Data.Char.isAlphaNum forall a b. (a -> b) -> a -> b
$ forall u. IsUnitId u => u -> String
unitString (forall unit. GenModule unit -> unit
moduleUnit GenModule u
m)
       in 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 forall a b. (a -> b) -> a -> b
$ ModuleName -> FastString
moduleNameFS (forall {unit}. GenModule unit -> ModuleName
moduleName GenModule unit
m) 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 <- forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall a b. (a -> b) -> a -> b
$ forall m. HscEnv -> SpecFinder m
lookupCompanionSpec HscEnv
hscEnv Module
m
  case Maybe SpecFinderResult
res of
    Maybe SpecFinderResult
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Module -> SpecFinderResult
SpecNotFound Module
m
    Just SpecFinderResult
s  -> 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 m
lookupInterfaceAnnotations ExternalPackageState
eps HomePackageTable
hpt Module
thisModule = do
  LiquidLib
lib <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Module
-> ExternalPackageState -> HomePackageTable -> Maybe LiquidLib
Util.deserialiseLiquidLib Module
thisModule ExternalPackageState
eps HomePackageTable
hpt
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 m
lookupInterfaceAnnotationsEPS ExternalPackageState
eps Module
thisModule = do
  LiquidLib
lib <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Module -> ExternalPackageState -> Maybe LiquidLib
Util.deserialiseLiquidLibFromEPS Module
thisModule ExternalPackageState
eps
  forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 m
lookupCompanionSpec HscEnv
hscEnv Module
thisModule = do

  ModSummary
modSummary <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ HscEnv -> ModuleName -> Maybe ModSummary
lookupModSummary HscEnv
hscEnv (forall {unit}. GenModule unit -> ModuleName
moduleName Module
thisModule)
  String
file       <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure (ModLocation -> Maybe String
ml_hs_file forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModSummary -> ModLocation
ms_location forall a b. (a -> b) -> a -> b
$ ModSummary
modSummary)
  Either (ParseErrorBundle String Void) (ModName, BareSpec)
parsed     <- forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ do
    Either SomeException String
mbSpecContent <- 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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
      Right String
raw -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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
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 (forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
peb)
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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
      forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
  forall a. [Maybe a] -> [a]
catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Bool, ModuleName) -> IO (Maybe StableModule)
lookupModule' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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   = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

    lookupLiquidBaseModule :: ModuleName -> IO (Maybe StableModule)
    lookupLiquidBaseModule :: ModuleName -> IO (Maybe StableModule)
lookupLiquidBaseModule ModuleName
mn = do
      FindResult
res <- HscEnv -> ModuleName -> Maybe FastString -> IO FindResult
findExposedPackageModule HscEnv
env ModuleName
mn (forall a. a -> Maybe a
Just FastString
"liquidhaskell")
      case FindResult
res of
        Found ModLocation
_ Module
mdl -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Module -> StableModule
toStableModule Module
mdl)
        FindResult
_           -> forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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")
  ]