{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
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
data LoadingMode = REPL | Standalone
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
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
data ModuleInfo = ModuleInfo
{ ModuleInfo -> ModuleName
_miName :: ModuleName
, ModuleInfo -> Map ModuleName ModuleInfo
_miImports :: Map ModuleName ModuleInfo
, 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
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
(<>)
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)
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
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
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
data Resolver
=
FromStdlib
|
FromDir FilePath
|
FromCwdOrStdlib
|
FromDirOrStdlib FilePath
withStdlib :: Resolver -> Resolver
withStdlib :: Resolver -> Resolver
withStdlib (FromDir String
fp) = String -> Resolver
FromDirOrStdlib String
fp
withStdlib Resolver
r = Resolver
r
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