{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE UndecidableInstances #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Module
-- Copyright   :  (c) 2019 disco team (see LICENSE)
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- The 'ModuleInfo' record representing a disco module, and functions
-- to resolve the location of a module on disk.
-----------------------------------------------------------------------------

module Disco.Module where

import           Data.Data                               (Data)
import           GHC.Generics                            (Generic)

import           Control.Lens                            (Getting, foldOf,
                                                          makeLenses, view)
import           Control.Monad                           (filterM)
import           Control.Monad.IO.Class                  (MonadIO (..))
import           Data.Bifunctor                          (first)
import           Data.Map                                (Map)
import qualified Data.Map                                as M
import           Data.Maybe                              (listToMaybe)
import qualified Data.Set                                as S
import           System.Directory                        (doesFileExist)
import           System.FilePath                         (replaceExtension,
                                                          (</>))

import           Unbound.Generics.LocallyNameless        (Alpha, Bind, Name,
                                                          Subst, bind)
import           Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

import           Polysemy

import           Disco.AST.Surface
import           Disco.AST.Typed
import           Disco.Context
import           Disco.Extensions
import           Disco.Names
import           Disco.Pretty                            hiding ((<>))
import           Disco.Typecheck.Erase                   (erase, erasePattern)
import           Disco.Typecheck.Util                    (TyCtx)
import           Disco.Types

import           Paths_disco

------------------------------------------------------------
-- ModuleInfo and related types
------------------------------------------------------------

-- | When loading a module, we could be loading it from code entered
-- at the REPL, or from a standalone file.  The two modes have
-- slightly different behavior.
data LoadingMode = REPL | Standalone

-- | A definition consists of a name being defined, the types of any
--   pattern arguments (each clause must have the same number of
--   patterns), the type of the body of each clause, and a list of
--   clauses.  For example,
--
--   @
--   f x (0,z) = 3*x + z > 5
--   f x (y,z) = z == 9
--   @
--
--   might look like @Defn f [Z, Z*Z] B [clause 1 ..., clause 2 ...]@
data Defn = Defn (Name ATerm) [Type] Type [Clause]
  deriving (Int -> Defn -> ShowS
[Defn] -> ShowS
Defn -> String
(Int -> Defn -> ShowS)
-> (Defn -> String) -> ([Defn] -> ShowS) -> Show Defn
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Defn] -> ShowS
$cshowList :: [Defn] -> ShowS
show :: Defn -> String
$cshow :: Defn -> String
showsPrec :: Int -> Defn -> ShowS
$cshowsPrec :: Int -> Defn -> ShowS
Show, (forall x. Defn -> Rep Defn x)
-> (forall x. Rep Defn x -> Defn) -> Generic Defn
forall x. Rep Defn x -> Defn
forall x. Defn -> Rep Defn x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Defn x -> Defn
$cfrom :: forall x. Defn -> Rep Defn x
Generic, Show Defn
Show Defn
-> (AlphaCtx -> Defn -> Defn -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn)
-> (AlphaCtx -> NamePatFind -> Defn -> Defn)
-> (AlphaCtx -> NthPatFind -> Defn -> Defn)
-> (Defn -> DisjointSet AnyName)
-> (Defn -> All)
-> (Defn -> Bool)
-> (Defn -> NthPatFind)
-> (Defn -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> Defn -> Defn)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> Defn -> m (Defn, Perm AnyName))
-> (AlphaCtx -> Defn -> Defn -> Ordering)
-> Alpha Defn
AlphaCtx -> NthPatFind -> Defn -> Defn
AlphaCtx -> NamePatFind -> Defn -> Defn
AlphaCtx -> Perm AnyName -> Defn -> Defn
AlphaCtx -> Defn -> Defn -> Bool
AlphaCtx -> Defn -> Defn -> Ordering
Defn -> Bool
Defn -> All
Defn -> DisjointSet AnyName
Defn -> NthPatFind
Defn -> NamePatFind
forall a.
Show a
-> (AlphaCtx -> a -> a -> Bool)
-> (forall (f :: * -> *).
    (Contravariant f, Applicative f) =>
    AlphaCtx -> (AnyName -> f AnyName) -> a -> f a)
-> (AlphaCtx -> NamePatFind -> a -> a)
-> (AlphaCtx -> NthPatFind -> a -> a)
-> (a -> DisjointSet AnyName)
-> (a -> All)
-> (a -> Bool)
-> (a -> NthPatFind)
-> (a -> NamePatFind)
-> (AlphaCtx -> Perm AnyName -> a -> a)
-> (forall (m :: * -> *) b.
    LFresh m =>
    AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b)
-> (forall (m :: * -> *).
    Fresh m =>
    AlphaCtx -> a -> m (a, Perm AnyName))
-> (AlphaCtx -> a -> a -> Ordering)
-> Alpha a
forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn
forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Defn -> m (Defn, Perm AnyName)
forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b
acompare' :: AlphaCtx -> Defn -> Defn -> Ordering
$cacompare' :: AlphaCtx -> Defn -> Defn -> Ordering
freshen' :: AlphaCtx -> Defn -> m (Defn, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Defn -> m (Defn, Perm AnyName)
lfreshen' :: AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b
swaps' :: AlphaCtx -> Perm AnyName -> Defn -> Defn
$cswaps' :: AlphaCtx -> Perm AnyName -> Defn -> Defn
namePatFind :: Defn -> NamePatFind
$cnamePatFind :: Defn -> NamePatFind
nthPatFind :: Defn -> NthPatFind
$cnthPatFind :: Defn -> NthPatFind
isEmbed :: Defn -> Bool
$cisEmbed :: Defn -> Bool
isTerm :: Defn -> All
$cisTerm :: Defn -> All
isPat :: Defn -> DisjointSet AnyName
$cisPat :: Defn -> DisjointSet AnyName
open :: AlphaCtx -> NthPatFind -> Defn -> Defn
$copen :: AlphaCtx -> NthPatFind -> Defn -> Defn
close :: AlphaCtx -> NamePatFind -> Defn -> Defn
$cclose :: AlphaCtx -> NamePatFind -> Defn -> Defn
fvAny' :: AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn
aeq' :: AlphaCtx -> Defn -> Defn -> Bool
$caeq' :: AlphaCtx -> Defn -> Defn -> Bool
$cp1Alpha :: Show Defn
Alpha, Typeable Defn
DataType
Constr
Typeable Defn
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Defn -> c Defn)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Defn)
-> (Defn -> Constr)
-> (Defn -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Defn))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn))
-> ((forall b. Data b => b -> b) -> Defn -> Defn)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r)
-> (forall u. (forall d. Data d => d -> u) -> Defn -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Defn -> m Defn)
-> Data Defn
Defn -> DataType
Defn -> Constr
(forall b. Data b => b -> b) -> Defn -> Defn
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
forall u. (forall d. Data d => d -> u) -> Defn -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
$cDefn :: Constr
$tDefn :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Defn -> m Defn
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapMp :: (forall d. Data d => d -> m d) -> Defn -> m Defn
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapM :: (forall d. Data d => d -> m d) -> Defn -> m Defn
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapQi :: Int -> (forall d. Data d => d -> u) -> Defn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
gmapQ :: (forall d. Data d => d -> u) -> Defn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
$cgmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Defn)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn)
dataTypeOf :: Defn -> DataType
$cdataTypeOf :: Defn -> DataType
toConstr :: Defn -> Constr
$ctoConstr :: Defn -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
$cp1Data :: Typeable Defn
Data, Subst Type)

instance Pretty Defn where
  pretty :: Defn -> Sem r Doc
pretty (Defn Name ATerm
x [Type]
patTys Type
ty [Clause]
clauses) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ([Sem r Doc] -> Sem r Doc) -> [Sem r Doc] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
    Name ATerm -> Type -> Sem r Doc
forall (r :: EffectRow) t.
Members '[Reader PA, LFresh] r =>
Name t -> Type -> Sem r Doc
prettyTyDecl Name ATerm
x ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
ty [Type]
patTys)
    Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
:
    (Clause -> Sem r Doc) -> [Clause] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Name ATerm, Bind [Pattern] Term) -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty ((Name ATerm, Bind [Pattern] Term) -> Sem r Doc)
-> (Clause -> (Name ATerm, Bind [Pattern] Term))
-> Clause
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name ATerm
x,) (Bind [Pattern] Term -> (Name ATerm, Bind [Pattern] Term))
-> (Clause -> Bind [Pattern] Term)
-> Clause
-> (Name ATerm, Bind [Pattern] Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bind [Pattern] Term
eraseClause) [Clause]
clauses

-- | A clause in a definition consists of a list of patterns (the LHS
--   of the =) and a term (the RHS).  For example, given the concrete
--   syntax @f n (x,y) = n*x + y@, the corresponding 'Clause' would be
--   something like @[n, (x,y)] (n*x + y)@.
type Clause = Bind [APattern] ATerm

eraseClause :: Clause -> Bind [Pattern] Term
eraseClause :: Clause -> Bind [Pattern] Term
eraseClause Clause
b = [Pattern] -> Term -> Bind [Pattern] Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ((APattern -> Pattern) -> [APattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Pattern
erasePattern [APattern]
ps) (ATerm -> Term
erase ATerm
t)
  where ([APattern]
ps, ATerm
t) = Clause -> ([APattern], ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind Clause
b

-- | Type checking a module yields a value of type ModuleInfo which contains
--   mapping from terms to their relavent documenation, a mapping from terms to
--   properties, and a mapping from terms to their types.
data ModuleInfo = ModuleInfo
  { ModuleInfo -> ModuleName
_miName     :: ModuleName
  , ModuleInfo -> Map ModuleName ModuleInfo
_miImports  :: Map ModuleName ModuleInfo

  -- List of names declared by the module, in the order they occur
  , ModuleInfo -> [QName Term]
_miNames    :: [QName Term]
  , ModuleInfo -> Ctx Term Docs
_miDocs     :: Ctx Term Docs
  , ModuleInfo -> Ctx ATerm [ATerm]
_miProps    :: Ctx ATerm [AProperty]
  , ModuleInfo -> TyCtx
_miTys      :: TyCtx
  , ModuleInfo -> TyDefCtx
_miTydefs   :: TyDefCtx
  , ModuleInfo -> Ctx ATerm Defn
_miTermdefs :: Ctx ATerm Defn
  , ModuleInfo -> [(ATerm, PolyType)]
_miTerms    :: [(ATerm, PolyType)]
  , ModuleInfo -> ExtSet
_miExts     :: ExtSet
  }
  deriving (Int -> ModuleInfo -> ShowS
[ModuleInfo] -> ShowS
ModuleInfo -> String
(Int -> ModuleInfo -> ShowS)
-> (ModuleInfo -> String)
-> ([ModuleInfo] -> ShowS)
-> Show ModuleInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModuleInfo] -> ShowS
$cshowList :: [ModuleInfo] -> ShowS
show :: ModuleInfo -> String
$cshow :: ModuleInfo -> String
showsPrec :: Int -> ModuleInfo -> ShowS
$cshowsPrec :: Int -> ModuleInfo -> ShowS
Show)

makeLenses ''ModuleInfo

instance Semigroup ModuleInfo where
  -- | Two ModuleInfos
  --   are merged by joining their doc, type, type definition, and term
  --   contexts. The property context of the new module is the one
  --   obtained from the second module. The name of the new module is
  --   taken from the first. Definitions from later modules override
  --   earlier ones.  Note that this function should really only be used
  --   for the special top-level REPL module.
  ModuleInfo ModuleName
n1 Map ModuleName ModuleInfo
is1 [QName Term]
ns1 Ctx Term Docs
d1 Ctx ATerm [ATerm]
_ TyCtx
ty1 TyDefCtx
tyd1 Ctx ATerm Defn
tm1 [(ATerm, PolyType)]
tms1 ExtSet
es1
    <> :: ModuleInfo -> ModuleInfo -> ModuleInfo
<> ModuleInfo ModuleName
_  Map ModuleName ModuleInfo
is2 [QName Term]
ns2 Ctx Term Docs
d2 Ctx ATerm [ATerm]
p2 TyCtx
ty2 TyDefCtx
tyd2 Ctx ATerm Defn
tm2 [(ATerm, PolyType)]
tms2 ExtSet
es2
    = ModuleName
-> Map ModuleName ModuleInfo
-> [QName Term]
-> Ctx Term Docs
-> Ctx ATerm [ATerm]
-> TyCtx
-> TyDefCtx
-> Ctx ATerm Defn
-> [(ATerm, PolyType)]
-> ExtSet
-> ModuleInfo
ModuleInfo
        ModuleName
n1
        (Map ModuleName ModuleInfo
is1 Map ModuleName ModuleInfo
-> Map ModuleName ModuleInfo -> Map ModuleName ModuleInfo
forall a. Semigroup a => a -> a -> a
<> Map ModuleName ModuleInfo
is2)
        ([QName Term]
ns1 [QName Term] -> [QName Term] -> [QName Term]
forall a. Semigroup a => a -> a -> a
<> [QName Term]
ns2)
        (Ctx Term Docs
d2 Ctx Term Docs -> Ctx Term Docs -> Ctx Term Docs
forall a. Semigroup a => a -> a -> a
<> Ctx Term Docs
d1)
        Ctx ATerm [ATerm]
p2
        (TyCtx
ty2 TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> TyCtx
ty1)
        (TyDefCtx
tyd2 TyDefCtx -> TyDefCtx -> TyDefCtx
forall a. Semigroup a => a -> a -> a
<> TyDefCtx
tyd1)
        (Ctx ATerm Defn
tm2 Ctx ATerm Defn -> Ctx ATerm Defn -> Ctx ATerm Defn
forall a. Semigroup a => a -> a -> a
<> Ctx ATerm Defn
tm1)
        ([(ATerm, PolyType)]
tms1 [(ATerm, PolyType)] -> [(ATerm, PolyType)] -> [(ATerm, PolyType)]
forall a. Semigroup a => a -> a -> a
<> [(ATerm, PolyType)]
tms2)
        (ExtSet
es1 ExtSet -> ExtSet -> ExtSet
forall a. Semigroup a => a -> a -> a
<> ExtSet
es2)

instance Monoid ModuleInfo where
  mempty :: ModuleInfo
mempty = ModuleInfo
emptyModuleInfo
  mappend :: ModuleInfo -> ModuleInfo -> ModuleInfo
mappend = ModuleInfo -> ModuleInfo -> ModuleInfo
forall a. Semigroup a => a -> a -> a
(<>)

-- | Get something from a module and its direct imports.
withImports :: Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports :: Getting a ModuleInfo a -> ModuleInfo -> a
withImports Getting a ModuleInfo a
l = Getting a ModuleInfo a -> ModuleInfo -> a
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting a ModuleInfo a
l (ModuleInfo -> a) -> (ModuleInfo -> a) -> ModuleInfo -> a
forall a. Semigroup a => a -> a -> a
<> Getting a ModuleInfo a -> ModuleInfo -> a
forall a s. Getting a s a -> s -> a
foldOf ((Map ModuleName ModuleInfo -> Const a (Map ModuleName ModuleInfo))
-> ModuleInfo -> Const a ModuleInfo
Lens' ModuleInfo (Map ModuleName ModuleInfo)
miImports ((Map ModuleName ModuleInfo -> Const a (Map ModuleName ModuleInfo))
 -> ModuleInfo -> Const a ModuleInfo)
-> ((a -> Const a a)
    -> Map ModuleName ModuleInfo
    -> Const a (Map ModuleName ModuleInfo))
-> Getting a ModuleInfo a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Const a ModuleInfo)
-> Map ModuleName ModuleInfo -> Const a (Map ModuleName ModuleInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ModuleInfo -> Const a ModuleInfo)
 -> Map ModuleName ModuleInfo
 -> Const a (Map ModuleName ModuleInfo))
-> Getting a ModuleInfo a
-> (a -> Const a a)
-> Map ModuleName ModuleInfo
-> Const a (Map ModuleName ModuleInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting a ModuleInfo a
l)

-- | Get the types of all names bound in a module and its direct imports.
allTys :: ModuleInfo -> TyCtx
allTys :: ModuleInfo -> TyCtx
allTys = Getting TyCtx ModuleInfo TyCtx -> ModuleInfo -> TyCtx
forall a. Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports Getting TyCtx ModuleInfo TyCtx
Lens' ModuleInfo TyCtx
miTys

-- | Get all type definitions from a module and its direct imports.
allTydefs :: ModuleInfo -> TyDefCtx
allTydefs :: ModuleInfo -> TyDefCtx
allTydefs = Getting TyDefCtx ModuleInfo TyDefCtx -> ModuleInfo -> TyDefCtx
forall a. Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports Getting TyDefCtx ModuleInfo TyDefCtx
Lens' ModuleInfo TyDefCtx
miTydefs

-- | The empty module info record.
emptyModuleInfo :: ModuleInfo
emptyModuleInfo :: ModuleInfo
emptyModuleInfo = ModuleName
-> Map ModuleName ModuleInfo
-> [QName Term]
-> Ctx Term Docs
-> Ctx ATerm [ATerm]
-> TyCtx
-> TyDefCtx
-> Ctx ATerm Defn
-> [(ATerm, PolyType)]
-> ExtSet
-> ModuleInfo
ModuleInfo ModuleName
REPLModule Map ModuleName ModuleInfo
forall k a. Map k a
M.empty [] Ctx Term Docs
forall a b. Ctx a b
emptyCtx Ctx ATerm [ATerm]
forall a b. Ctx a b
emptyCtx TyCtx
forall a b. Ctx a b
emptyCtx TyDefCtx
forall k a. Map k a
M.empty Ctx ATerm Defn
forall a b. Ctx a b
emptyCtx [] ExtSet
forall a. Set a
S.empty

------------------------------------------------------------
-- Module resolution
------------------------------------------------------------

-- | A data type indicating where we should look for Disco modules to
--   be loaded.
data Resolver
  = -- | Load only from the stdlib               (standard lib modules)
    FromStdlib
  | -- | Load only from a specific directory     (:load)
    FromDir FilePath
  | -- | Load from current working dir or stdlib (import at REPL)
    FromCwdOrStdlib
  | -- | Load from specific dir or stdlib        (import in file)
    FromDirOrStdlib FilePath

-- | Add the possibility of loading imports from the stdlib.  For
--   example, this is what we want to do after a user loads a specific
--   file using `:load` (for which we will NOT look in the stdlib),
--   but then we need to recursively load modules which it imports
--   (which may either be in the stdlib, or the same directory as the
--   `:load`ed module).
withStdlib :: Resolver -> Resolver
withStdlib :: Resolver -> Resolver
withStdlib (FromDir String
fp) = String -> Resolver
FromDirOrStdlib String
fp
withStdlib Resolver
r            = Resolver
r

-- | Given a module resolution mode and a raw module name, relavent
--   directories are searched for the file containing the provided
--   module name.  Returns Nothing if no module with the given name
--   could be found.
resolveModule :: Member (Embed IO) r => Resolver -> String -> Sem r (Maybe (FilePath, ModuleProvenance))
resolveModule :: Resolver -> String -> Sem r (Maybe (String, ModuleProvenance))
resolveModule Resolver
resolver String
modname = do
  String
datadir <- IO String -> Sem r String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getDataDir
  let searchPath :: [(String, ModuleProvenance)]
searchPath =
        case Resolver
resolver of
          Resolver
FromStdlib          -> [(String
datadir, ModuleProvenance
Stdlib)]
          FromDir String
dir         -> [(String
dir, String -> ModuleProvenance
Dir String
dir)]
          Resolver
FromCwdOrStdlib     -> [(String
datadir, ModuleProvenance
Stdlib), (String
".", String -> ModuleProvenance
Dir String
".")]
          FromDirOrStdlib String
dir -> [(String
datadir, ModuleProvenance
Stdlib), (String
dir, String -> ModuleProvenance
Dir String
dir)]
  let fps :: [(String, ModuleProvenance)]
fps = ((String, ModuleProvenance) -> (String, ModuleProvenance))
-> [(String, ModuleProvenance)] -> [(String, ModuleProvenance)]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS -> (String, ModuleProvenance) -> (String, ModuleProvenance)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (String -> ShowS
</> String -> ShowS
replaceExtension String
modname String
"disco")) [(String, ModuleProvenance)]
searchPath
  [(String, ModuleProvenance)]
fexists <- IO [(String, ModuleProvenance)]
-> Sem r [(String, ModuleProvenance)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(String, ModuleProvenance)]
 -> Sem r [(String, ModuleProvenance)])
-> IO [(String, ModuleProvenance)]
-> Sem r [(String, ModuleProvenance)]
forall a b. (a -> b) -> a -> b
$ ((String, ModuleProvenance) -> IO Bool)
-> [(String, ModuleProvenance)] -> IO [(String, ModuleProvenance)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (String -> IO Bool
doesFileExist (String -> IO Bool)
-> ((String, ModuleProvenance) -> String)
-> (String, ModuleProvenance)
-> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, ModuleProvenance) -> String
forall a b. (a, b) -> a
fst) [(String, ModuleProvenance)]
fps
  Maybe (String, ModuleProvenance)
-> Sem r (Maybe (String, ModuleProvenance))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, ModuleProvenance)
 -> Sem r (Maybe (String, ModuleProvenance)))
-> Maybe (String, ModuleProvenance)
-> Sem r (Maybe (String, ModuleProvenance))
forall a b. (a -> b) -> a -> b
$ [(String, ModuleProvenance)] -> Maybe (String, ModuleProvenance)
forall a. [a] -> Maybe a
listToMaybe [(String, ModuleProvenance)]
fexists