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

-- |
-- Module      :  Disco.Module
-- Copyright   :  (c) 2019 disco team (see LICENSE)
-- Maintainer  :  [email protected]
--
-- 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 Control.Lens (
  Getting,
  foldOf,
  makeLenses,
  view,
 )
import Control.Monad (filterM)
import Control.Monad.IO.Class (MonadIO (..))
import Data.Bifunctor (first)
import Data.Data (Data)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import qualified Data.Map as M
import Data.Maybe (listToMaybe)
import qualified Data.Set as S
import GHC.Generics (Generic)
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 (NonEmpty 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
$cshowsPrec :: Int -> Defn -> ShowS
showsPrec :: Int -> Defn -> ShowS
$cshow :: Defn -> String
show :: Defn -> String
$cshowList :: [Defn] -> ShowS
showList :: [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
$cfrom :: forall x. Defn -> Rep Defn x
from :: forall x. Defn -> Rep Defn x
$cto :: forall x. Rep Defn x -> Defn
to :: forall x. Rep Defn x -> Defn
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 -> Perm AnyName -> Defn -> Defn
AlphaCtx -> NamePatFind -> Defn -> Defn
AlphaCtx -> NthPatFind -> Defn -> Defn
AlphaCtx -> Defn -> Defn -> Bool
AlphaCtx -> Defn -> Defn -> Ordering
Defn -> Bool
Defn -> All
Defn -> NamePatFind
Defn -> NthPatFind
Defn -> DisjointSet AnyName
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
$caeq' :: AlphaCtx -> Defn -> Defn -> Bool
aeq' :: AlphaCtx -> Defn -> Defn -> Bool
$cfvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn
fvAny' :: forall (f :: * -> *).
(Contravariant f, Applicative f) =>
AlphaCtx -> (AnyName -> f AnyName) -> Defn -> f Defn
$cclose :: AlphaCtx -> NamePatFind -> Defn -> Defn
close :: AlphaCtx -> NamePatFind -> Defn -> Defn
$copen :: AlphaCtx -> NthPatFind -> Defn -> Defn
open :: AlphaCtx -> NthPatFind -> Defn -> Defn
$cisPat :: Defn -> DisjointSet AnyName
isPat :: Defn -> DisjointSet AnyName
$cisTerm :: Defn -> All
isTerm :: Defn -> All
$cisEmbed :: Defn -> Bool
isEmbed :: Defn -> Bool
$cnthPatFind :: Defn -> NthPatFind
nthPatFind :: Defn -> NthPatFind
$cnamePatFind :: Defn -> NamePatFind
namePatFind :: Defn -> NamePatFind
$cswaps' :: AlphaCtx -> Perm AnyName -> Defn -> Defn
swaps' :: AlphaCtx -> Perm AnyName -> Defn -> Defn
$clfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b
lfreshen' :: forall (m :: * -> *) b.
LFresh m =>
AlphaCtx -> Defn -> (Defn -> Perm AnyName -> m b) -> m b
$cfreshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Defn -> m (Defn, Perm AnyName)
freshen' :: forall (m :: * -> *).
Fresh m =>
AlphaCtx -> Defn -> m (Defn, Perm AnyName)
$cacompare' :: AlphaCtx -> Defn -> Defn -> Ordering
acompare' :: AlphaCtx -> Defn -> Defn -> Ordering
Alpha, Typeable Defn
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 -> Constr
Defn -> DataType
(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)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Defn -> c Defn
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Defn
$ctoConstr :: Defn -> Constr
toConstr :: Defn -> Constr
$cdataTypeOf :: Defn -> DataType
dataTypeOf :: Defn -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Defn)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Defn)
$cgmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
gmapT :: (forall b. Data b => b -> b) -> Defn -> Defn
$cgmapQl :: 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
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Defn -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Defn -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Defn -> u
$cgmapM :: forall (m :: * -> *).
Monad 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
$cgmapMp :: 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
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m Defn
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Defn -> m 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 NonEmpty (Bind [APattern] ATerm)
clauses) =
    [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat ([Sem r (Doc ann)] -> Sem r (Doc ann))
-> [Sem r (Doc ann)] -> Sem r (Doc ann)
forall a b. (a -> b) -> a -> b
$
      Name ATerm -> Type -> Sem r (Doc ann)
forall (r :: EffectRow) t ann.
Members '[Reader PA, LFresh] r =>
Name t -> Type -> Sem r (Doc ann)
prettyTyDecl Name ATerm
x ((Type -> Type -> Type) -> Type -> [Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(:->:) Type
ty [Type]
patTys)
        Sem r (Doc ann) -> [Sem r (Doc ann)] -> [Sem r (Doc ann)]
forall a. a -> [a] -> [a]
: (Bind [APattern] ATerm -> Sem r (Doc ann))
-> [Bind [APattern] ATerm] -> [Sem r (Doc ann)]
forall a b. (a -> b) -> [a] -> [b]
map ((Name ATerm, Bind [Pattern] Term) -> Sem r (Doc ann)
forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
(Name ATerm, Bind [Pattern] Term) -> Sem r (Doc ann)
forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty ((Name ATerm, Bind [Pattern] Term) -> Sem r (Doc ann))
-> (Bind [APattern] ATerm -> (Name ATerm, Bind [Pattern] Term))
-> Bind [APattern] ATerm
-> Sem r (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name ATerm
x,) (Bind [Pattern] Term -> (Name ATerm, Bind [Pattern] Term))
-> (Bind [APattern] ATerm -> Bind [Pattern] Term)
-> Bind [APattern] ATerm
-> (Name ATerm, Bind [Pattern] Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bind [APattern] ATerm -> Bind [Pattern] Term
eraseClause) (NonEmpty (Bind [APattern] ATerm) -> [Bind [APattern] ATerm]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Bind [APattern] ATerm)
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 :: Bind [APattern] ATerm -> Bind [Pattern] Term
eraseClause Bind [APattern] ATerm
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) = Bind [APattern] ATerm -> ([APattern], ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind Bind [APattern] ATerm
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
$cshowsPrec :: Int -> ModuleInfo -> ShowS
showsPrec :: Int -> ModuleInfo -> ShowS
$cshow :: ModuleInfo -> String
show :: ModuleInfo -> String
$cshowList :: [ModuleInfo] -> ShowS
showList :: [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 :: forall a. Monoid a => 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map ModuleName a -> f (Map ModuleName 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 :: forall (r :: EffectRow).
Member (Embed IO) r =>
Resolver -> String -> Sem r (Maybe (String, ModuleProvenance))
resolveModule Resolver
resolver String
modname = do
  String
datadir <- IO String -> Sem r String
forall a. IO a -> Sem r a
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 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 (String -> ShowS
</> String -> ShowS
replaceExtension String
modname String
"disco")) [(String, ModuleProvenance)]
searchPath
  [(String, ModuleProvenance)]
fexists <- IO [(String, ModuleProvenance)]
-> Sem r [(String, ModuleProvenance)]
forall a. IO a -> Sem r a
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 a. a -> Sem r a
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