{-# 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
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. 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
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' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Defn -> m (Defn, Perm AnyName)
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Defn -> m (Defn, Perm AnyName)
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
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' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
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
Alpha, Typeable Defn
Defn -> DataType
Defn -> Constr
(forall b. Data b => b -> b) -> Defn -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Subst Type)
instance Pretty Defn where
pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
Defn -> Sem r (Doc ann)
pretty (Defn Name ATerm
x [Type]
patTys Type
ty [Clause]
clauses) =
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat forall a b. (a -> b) -> a -> b
$
forall (r :: EffectRow) t ann.
Members '[Reader PA, LFresh] r =>
Name t -> Type -> Sem r (Doc ann)
prettyTyDecl Name ATerm
x (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
ty [Type]
patTys)
forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name ATerm
x,) 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 = forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (forall a b. (a -> b) -> [a] -> [b]
map APattern -> Pattern
erasePattern [APattern]
ps) (ATerm -> Term
erase ATerm
t)
where
([APattern]
ps, ATerm
t) = 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
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 forall a. Semigroup a => a -> a -> a
<> Map ModuleName ModuleInfo
is2)
([QName Term]
ns1 forall a. Semigroup a => a -> a -> a
<> [QName Term]
ns2)
(Ctx Term Docs
d2 forall a. Semigroup a => a -> a -> a
<> Ctx Term Docs
d1)
Ctx ATerm [ATerm]
p2
(TyCtx
ty2 forall a. Semigroup a => a -> a -> a
<> TyCtx
ty1)
(TyDefCtx
tyd2 forall a. Semigroup a => a -> a -> a
<> TyDefCtx
tyd1)
(Ctx ATerm Defn
tm2 forall a. Semigroup a => a -> a -> a
<> Ctx ATerm Defn
tm1)
([(ATerm, PolyType)]
tms1 forall a. Semigroup a => a -> a -> a
<> [(ATerm, PolyType)]
tms2)
(ExtSet
es1 forall a. Semigroup a => a -> a -> a
<> ExtSet
es2)
instance Monoid ModuleInfo where
mempty :: ModuleInfo
mempty = ModuleInfo
emptyModuleInfo
mappend :: ModuleInfo -> ModuleInfo -> ModuleInfo
mappend = forall a. Semigroup a => a -> a -> a
(<>)
withImports :: Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports :: forall a. Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports Getting a ModuleInfo a
l = forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting a ModuleInfo a
l forall a. Semigroup a => a -> a -> a
<> forall a s. Getting a s a -> s -> a
foldOf (Lens' ModuleInfo (Map ModuleName ModuleInfo)
miImports forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting a ModuleInfo a
l)
allTys :: ModuleInfo -> TyCtx
allTys :: ModuleInfo -> TyCtx
allTys = forall a. Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports Lens' ModuleInfo TyCtx
miTys
allTydefs :: ModuleInfo -> TyDefCtx
allTydefs :: ModuleInfo -> TyDefCtx
allTydefs = forall a. Monoid a => Getting a ModuleInfo a -> ModuleInfo -> a
withImports 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 forall k a. Map k a
M.empty [] forall a b. Ctx a b
emptyCtx forall a b. Ctx a b
emptyCtx forall a b. Ctx a b
emptyCtx forall k a. Map k a
M.empty forall a b. Ctx a b
emptyCtx [] 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 :: forall (r :: EffectRow).
Member (Embed IO) r =>
Resolver -> String -> Sem r (Maybe (String, ModuleProvenance))
resolveModule Resolver
resolver String
modname = do
String
datadir <- 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 = forall a b. (a -> b) -> [a] -> [b]
map (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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (String -> IO Bool
doesFileExist forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(String, ModuleProvenance)]
fps
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe a
listToMaybe [(String, ModuleProvenance)]
fexists