{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeSynonymInstances #-}

-- |
-- Module      :  Disco.Eval
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Top-level evaluation utilities.
module Disco.Eval (
  -- * Effects
  EvalEffects,
  DiscoEffects,

  -- * Top-level info record and associated lenses
  DiscoConfig,
  initDiscoConfig,
  debugMode,
  TopInfo,
  replModInfo,
  topEnv,
  topModMap,
  lastFile,
  discoConfig,

  -- * Running things
  runDisco,
  runTCM,
  inputTopEnv,
  parseDiscoModule,
  typecheckTop,

  -- * Loading modules
  loadDiscoModule,
  loadParsedDiscoModule,
  loadFile,
  addToREPLModule,
  setREPLModule,
  loadDefsFrom,
  loadDef,
)
where

import Control.Arrow ((&&&))
import Control.Exception (SomeException, handle)
import Control.Lens (
  makeLenses,
  toListOf,
  view,
  (%~),
  (.~),
  (<>~),
  (^.),
 )
import Control.Monad (unless, void, when)
import Control.Monad.IO.Class (liftIO)
import Data.Bifunctor
import Data.Map (Map)
import qualified Data.Map as M
import qualified Data.Set as S
import System.FilePath ((-<.>))
import Prelude

import qualified System.Console.Haskeline as H

import Disco.Effects.Fresh
import Disco.Effects.Input
import Disco.Effects.LFresh
import Disco.Effects.State
import Polysemy
import Polysemy.Embed
import Polysemy.Error
import Polysemy.Fail
import Polysemy.Output
import Polysemy.Random
import Polysemy.Reader

import Disco.AST.Core
import Disco.AST.Surface
import Disco.Compile (compileDefns)
import Disco.Context as Ctx
import Disco.Error
import Disco.Extensions
import Disco.Interpret.CESK
import Disco.Messages
import Disco.Module
import Disco.Names
import Disco.Parser
import Disco.Pretty hiding ((<>))
import qualified Disco.Pretty as Pretty
import Disco.Typecheck (checkModule)
import Disco.Typecheck.Util
import Disco.Types
import Disco.Value

------------------------------------------------------------
-- Configuation options
------------------------------------------------------------

data DiscoConfig = DiscoConfig
  { DiscoConfig -> Bool
_debugMode :: Bool
  }

makeLenses ''DiscoConfig

initDiscoConfig :: DiscoConfig
initDiscoConfig :: DiscoConfig
initDiscoConfig =
  DiscoConfig
    { _debugMode :: Bool
_debugMode = Bool
False
    }

------------------------------------------------------------
-- Top level info record
------------------------------------------------------------

-- | A record of information about the current top-level environment.
data TopInfo = TopInfo
  { TopInfo -> ModuleInfo
_replModInfo :: ModuleInfo
  -- ^ Info about the top-level module collecting stuff entered at
  --   the REPL.
  , TopInfo -> Env
_topEnv :: Env
  -- ^ Top-level environment mapping names to values.  Set by
  --   'loadDefs'.
  , TopInfo -> Map ModuleName ModuleInfo
_topModMap :: Map ModuleName ModuleInfo
  -- ^ Mapping from loaded module names to their 'ModuleInfo'
  --   records.
  , TopInfo -> Maybe FilePath
_lastFile :: Maybe FilePath
  -- ^ The most recent file which was :loaded by the user.
  , TopInfo -> DiscoConfig
_discoConfig :: DiscoConfig
  }

-- | The initial (empty) record of top-level info.
initTopInfo :: DiscoConfig -> TopInfo
initTopInfo :: DiscoConfig -> TopInfo
initTopInfo DiscoConfig
cfg =
  TopInfo
    { _replModInfo :: ModuleInfo
_replModInfo = ModuleInfo
emptyModuleInfo
    , _topEnv :: Env
_topEnv = forall a b. Ctx a b
emptyCtx
    , _topModMap :: Map ModuleName ModuleInfo
_topModMap = forall k a. Map k a
M.empty
    , _lastFile :: Maybe FilePath
_lastFile = forall a. Maybe a
Nothing
    , _discoConfig :: DiscoConfig
_discoConfig = DiscoConfig
cfg
    }

makeLenses ''TopInfo

------------------------------------------------------------
-- Top-level effects
------------------------------------------------------------

-- | Append two effect rows.
type family AppendEffects (r :: EffectRow) (s :: EffectRow) :: EffectRow where
  AppendEffects '[] s = s
  AppendEffects (e ': r) s = e ': AppendEffects r s

-- Didn't seem like this already existed in @polysemy@, though I
-- might have missed it.  Of course we could also use a polymorphic
-- version from somewhere --- it is just type-level list append.
-- However, just manually implementing it here seems easier.

-- | Effects needed at the top level.
type TopEffects = '[Error DiscoError, State TopInfo, Output (Message ()), Embed IO, Final (H.InputT IO)]

-- | Effects needed for evaluation.
type EvalEffects = [Error EvalError, Random, LFresh, Output (Message ()), State Mem]

-- XXX write about order.
-- memory, counter etc. should not be reset by errors.

-- | All effects needed for the top level + evaluation.
type DiscoEffects = AppendEffects EvalEffects TopEffects

------------------------------------------------------------
-- Running top-level Disco computations
------------------------------------------------------------

-- | Settings for running the 'InputT' monad from @haskeline@.  Just
--   uses the defaults and sets the history file to @.disco_history@.
inputSettings :: H.Settings IO
inputSettings :: Settings IO
inputSettings =
  forall (m :: * -> *). MonadIO m => Settings m
H.defaultSettings
    { historyFile :: Maybe FilePath
H.historyFile = forall a. a -> Maybe a
Just FilePath
".disco_history"
    }

-- | Run a top-level computation.
runDisco :: DiscoConfig -> (forall r. Members DiscoEffects r => Sem r ()) -> IO ()
runDisco :: DiscoConfig
-> (forall (r :: [(* -> *) -> * -> *]).
    Members DiscoEffects r =>
    Sem r ())
-> IO ()
runDisco DiscoConfig
cfg forall (r :: [(* -> *) -> * -> *]).
Members DiscoEffects r =>
Sem r ()
m =
  forall (f :: * -> *) a. Functor f => f a -> f ()
void
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
H.runInputT Settings IO
inputSettings
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => Sem '[Final m] a -> m a
runFinal @(H.InputT IO)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (r :: [(* -> *) -> * -> *]) a.
(Member (Final m) r, Functor m) =>
Sem (Embed m : r) a -> Sem r a
embedToFinal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m1 :: * -> *) (m2 :: * -> *) (r :: [(* -> *) -> * -> *]) a.
Member (Embed m2) r =>
(forall x. m1 x -> m2 x) -> Sem (Embed m1 : r) a -> Sem r a
runEmbedded @_ @(H.InputT IO) forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o (r :: [(* -> *) -> * -> *]) a.
(o -> Sem r ()) -> Sem (Output o : r) a -> Sem r a
runOutputSem (forall (r :: [(* -> *) -> * -> *]) ann.
Member (Embed IO) r =>
(Message ann -> Bool) -> Message ann -> Sem r ()
handleMsg Message () -> Bool
msgFilter) -- Handle Output Message via printing to console
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (r :: [(* -> *) -> * -> *]) a.
Member (Embed IO) r =>
s -> Sem (State s : r) a -> Sem r (s, a)
stateToIO (DiscoConfig -> TopInfo
initTopInfo DiscoConfig
cfg) -- Run State TopInfo via an IORef
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState -- Dispatch Input TopInfo effect via State effect
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (r :: [(* -> *) -> * -> *]) a.
s -> Sem (State s : r) a -> Sem r (s, a)
runState Mem
emptyMem -- Start with empty memory
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem (Error DiscoError : r) () -> Sem r ()
outputDiscoErrors -- Output any top-level errors
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a. Sem (LFresh : r) a -> Sem r a
runLFresh -- Generate locally fresh names
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a.
Member (Embed IO) r =>
Sem (Random : r) a -> Sem r a
runRandomIO -- Generate randomness via IO
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e1 e2 (r :: [(* -> *) -> * -> *]) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError EvalError -> DiscoError
EvalErr -- Embed runtime errors into top-level error type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
(FilePath -> e) -> Sem (Fail : r) a -> Sem r a
failToError FilePath -> DiscoError
Panic -- Turn pattern-match failures into a Panic error
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Reader i : r) a -> Sem r a
runReader forall a b. Ctx a b
emptyCtx -- Keep track of current Env
    forall a b. (a -> b) -> a -> b
$ forall (r :: [(* -> *) -> * -> *]).
Members DiscoEffects r =>
Sem r ()
m
 where
  msgFilter :: Message () -> Bool
msgFilter
    | DiscoConfig
cfg forall s a. s -> Getting a s a -> a
^. Iso' DiscoConfig Bool
debugMode = forall a b. a -> b -> a
const Bool
True
    | Bool
otherwise = (forall a. Eq a => a -> a -> Bool
/= MessageType
Debug) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall ann. Lens' (Message ann) MessageType
messageType

------------------------------------------------------------
-- Environment utilities
------------------------------------------------------------

-- XXX change name to inputREPLEnv, modify to actually get the Env
-- from the REPL module info?

-- | Run a computation that needs an input environment, grabbing the
--   current top-level environment from the 'TopInfo' records.
inputTopEnv :: Member (Input TopInfo) r => Sem (Input Env ': r) a -> Sem r a
inputTopEnv :: forall (r :: [(* -> *) -> * -> *]) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv Sem (Input Env : r) a
m = do
  Env
e <- forall i j (r :: [(* -> *) -> * -> *]).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' TopInfo Env
topEnv)
  forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Input i : r) a -> Sem r a
runInputConst Env
e Sem (Input Env : r) a
m

------------------------------------------------------------
-- High-level disco phases
------------------------------------------------------------

--------------------------------------------------
-- Parsing

-- | Parse a module from a file, re-throwing a parse error if it
--   fails.
parseDiscoModule :: Members '[Error DiscoError, Embed IO] r => FilePath -> Sem r Module
parseDiscoModule :: forall (r :: [(* -> *) -> * -> *]).
Members '[Error DiscoError, Embed IO] r =>
FilePath -> Sem r Module
parseDiscoModule FilePath
file = do
  FilePath
str <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readFile FilePath
file
  forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
Either e a -> Sem r a
fromEither 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 ParseErrorBundle FilePath DiscoParseError -> DiscoError
ParseErr forall a b. (a -> b) -> a -> b
$ forall a.
Parser a
-> FilePath
-> FilePath
-> Either (ParseErrorBundle FilePath DiscoParseError) a
runParser (LoadingMode -> Parser Module
wholeModule LoadingMode
Standalone) FilePath
file FilePath
str

--------------------------------------------------
-- Type checking

-- | Run a typechecking computation, providing it with local contexts
--   (initialized to the provided arguments) for variable types and
--   type definitions.
runTCM ::
  Member (Error DiscoError) r =>
  TyCtx ->
  TyDefCtx ->
  Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error LocTCError ': r) a ->
  Sem r a
runTCM :: forall (r :: [(* -> *) -> * -> *]) a.
Member (Error DiscoError) r =>
TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem r a
runTCM TyCtx
tyCtx TyDefCtx
tyDefCtx =
  forall e1 e2 (r :: [(* -> *) -> * -> *]) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError LocTCError -> DiscoError
TypeCheckErr
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Reader i : r) a -> Sem r a
runReader @TyDefCtx TyDefCtx
tyDefCtx
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Reader i : r) a -> Sem r a
runReader @TyCtx TyCtx
tyCtx

-- | A variant of 'runTCM' that requires only a 'TCError' instead
--   of a 'LocTCError'.
runTCM' ::
  Member (Error DiscoError) r =>
  TyCtx ->
  TyDefCtx ->
  Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error TCError ': r) a ->
  Sem r a
runTCM' :: forall (r :: [(* -> *) -> * -> *]) a.
Member (Error DiscoError) r =>
TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
runTCM' TyCtx
tyCtx TyDefCtx
tyDefCtx =
  forall e1 e2 (r :: [(* -> *) -> * -> *]) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError (LocTCError -> DiscoError
TypeCheckErr forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> LocTCError
noLoc)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a. Sem (Fresh : r) a -> Sem r a
runFresh
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Reader i : r) a -> Sem r a
runReader @TyDefCtx TyDefCtx
tyDefCtx
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: [(* -> *) -> * -> *]) a.
i -> Sem (Reader i : r) a -> Sem r a
runReader @TyCtx TyCtx
tyCtx

-- | Run a typechecking computation in the context of the top-level
--   REPL module, re-throwing a wrapped error if it fails.
typecheckTop ::
  Members '[Input TopInfo, Error DiscoError] r =>
  Sem (Reader TyCtx ': Reader TyDefCtx ': Fresh ': Error TCError ': r) a ->
  Sem r a
typecheckTop :: forall (r :: [(* -> *) -> * -> *]) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
tcm = do
  TyCtx
tyctx <- forall i j (r :: [(* -> *) -> * -> *]).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyCtx
miTys))
  [TyCtx]
imptyctx <- forall i j (r :: [(* -> *) -> * -> *]).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
. Lens' ModuleInfo TyCtx
miTys))
  TyDefCtx
tydefs <- forall i j (r :: [(* -> *) -> * -> *]).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyDefCtx
miTydefs))
  [TyDefCtx]
imptydefs <- forall i j (r :: [(* -> *) -> * -> *]).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
. Lens' ModuleInfo TyDefCtx
miTydefs))
  forall (r :: [(* -> *) -> * -> *]) a.
Member (Error DiscoError) r =>
TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
runTCM' (TyCtx
tyctx forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [TyCtx]
imptyctx) (TyDefCtx
tydefs forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [TyDefCtx]
imptydefs) Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
tcm

--------------------------------------------------
-- Loading

-- | Recursively loads a given module by first recursively loading and
--   typechecking its imported modules, adding the obtained
--   'ModuleInfo' records to a map from module names to info records,
--   and then typechecking the parent module in an environment with
--   access to this map. This is really just a depth-first search.
--
--   The 'Resolver' argument specifies where to look for imported
--   modules.
loadDiscoModule ::
  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
  Bool ->
  Resolver ->
  FilePath ->
  Sem r ModuleInfo
loadDiscoModule :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> FilePath -> Sem r ModuleInfo
loadDiscoModule Bool
quiet Resolver
resolver =
  forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
loadDiscoModule' Bool
quiet Resolver
resolver []

-- | Like 'loadDiscoModule', but start with an already parsed 'Module'
--   instead of loading a module from disk by name.  Also, check it in
--   a context that includes the current top-level context (unlike a
--   module loaded from disk).  Used for e.g. blocks/modules entered
--   at the REPL prompt.
loadParsedDiscoModule ::
  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
  Bool ->
  Resolver ->
  ModuleName ->
  Module ->
  Sem r ModuleInfo
loadParsedDiscoModule :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule Bool
quiet Resolver
resolver =
  forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool
-> LoadingMode
-> Resolver
-> [ModuleName]
-> ModuleName
-> Module
-> Sem r ModuleInfo
loadParsedDiscoModule' Bool
quiet LoadingMode
REPL Resolver
resolver []

-- | Recursively load a Disco module while keeping track of an extra
--   Map from module names to 'ModuleInfo' records, to avoid loading
--   any imported module more than once. Resolve the module, load and
--   parse it, then call 'loadParsedDiscoModule''.
loadDiscoModule' ::
  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
  Bool ->
  Resolver ->
  [ModuleName] ->
  FilePath ->
  Sem r ModuleInfo
loadDiscoModule' :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
loadDiscoModule' Bool
quiet Resolver
resolver [ModuleName]
inProcess FilePath
modPath = do
  (FilePath
resolvedPath, ModuleProvenance
prov) <-
    forall (r :: [(* -> *) -> * -> *]).
Member (Embed IO) r =>
Resolver -> FilePath -> Sem r (Maybe (FilePath, ModuleProvenance))
resolveModule Resolver
resolver FilePath
modPath
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ FilePath -> DiscoError
ModuleNotFound FilePath
modPath) forall (m :: * -> *) a. Monad m => a -> m a
return
  let name :: ModuleName
name = ModuleProvenance -> FilePath -> ModuleName
Named ModuleProvenance
prov FilePath
modPath
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleName
name forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ModuleName]
inProcess) (forall e (r :: [(* -> *) -> * -> *]) a.
Member (Error e) r =>
e -> Sem r a
throw forall a b. (a -> b) -> a -> b
$ [ModuleName] -> DiscoError
CyclicImport (ModuleName
name forall a. a -> [a] -> [a]
: [ModuleName]
inProcess))
  Map ModuleName ModuleInfo
modMap <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap
  case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ModuleName
name Map ModuleName ModuleInfo
modMap of
    Just ModuleInfo
mi -> forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
mi
    Maybe ModuleInfo
Nothing -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet forall a b. (a -> b) -> a -> b
$ forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Loading" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text (FilePath
modPath FilePath -> FilePath -> FilePath
-<.> FilePath
"disco") forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
Pretty.<> Sem r (Doc ann)
"..."
      Module
cm <- forall (r :: [(* -> *) -> * -> *]).
Members '[Error DiscoError, Embed IO] r =>
FilePath -> Sem r Module
parseDiscoModule FilePath
resolvedPath
      forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool
-> LoadingMode
-> Resolver
-> [ModuleName]
-> ModuleName
-> Module
-> Sem r ModuleInfo
loadParsedDiscoModule' Bool
quiet LoadingMode
Standalone Resolver
resolver (ModuleName
name forall a. a -> [a] -> [a]
: [ModuleName]
inProcess) ModuleName
name Module
cm

-- | A list of standard library module names, which should always be
--   loaded implicitly.
stdLib :: [String]
stdLib :: [FilePath]
stdLib = [FilePath
"list", FilePath
"container"]

-- | Recursively load an already-parsed Disco module while keeping
--   track of an extra Map from module names to 'ModuleInfo' records,
--   to avoid loading any imported module more than once.  Typecheck
--   it in the context of the top-level type context iff the
--   'LoadingMode' parameter is 'REPL'.  Recursively load all its
--   imports, then typecheck it.
loadParsedDiscoModule' ::
  Members '[State TopInfo, Output (Message ann), Random, State Mem, Error DiscoError, Embed IO] r =>
  Bool ->
  LoadingMode ->
  Resolver ->
  [ModuleName] ->
  ModuleName ->
  Module ->
  Sem r ModuleInfo
loadParsedDiscoModule' :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool
-> LoadingMode
-> Resolver
-> [ModuleName]
-> ModuleName
-> Module
-> Sem r ModuleInfo
loadParsedDiscoModule' Bool
quiet LoadingMode
mode Resolver
resolver [ModuleName]
inProcess ModuleName
name cm :: Module
cm@(Module Set Ext
_ [FilePath]
mns [Decl]
_ [(Name Term, Docs)]
_ [Term]
_) = do
  -- Recursively load any modules imported by this one, plus standard
  -- library modules (unless NoStdLib is enabled), and build a map with the results.
  [ModuleInfo]
mis <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
loadDiscoModule' Bool
quiet (Resolver -> Resolver
withStdlib Resolver
resolver) [ModuleName]
inProcess) [FilePath]
mns
  [ModuleInfo]
stdmis <- case Ext
NoStdLib forall a. Ord a => a -> Set a -> Bool
`S.member` Module -> Set Ext
modExts Module
cm of
    Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    Bool
False -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
loadDiscoModule' Bool
True Resolver
FromStdlib [ModuleName]
inProcess) [FilePath]
stdLib
  let modImps :: Map ModuleName ModuleInfo
modImps = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall a b. (a -> b) -> [a] -> [b]
map (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Lens' ModuleInfo ModuleName
miName forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall a. a -> a
id) ([ModuleInfo]
mis forall a. [a] -> [a] -> [a]
++ [ModuleInfo]
stdmis))

  -- Get context and type definitions from the REPL, in case we are in REPL mode.
  Map ModuleName ModuleInfo
topImports <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo (Map ModuleName ModuleInfo)
miImports)
  TyCtx
topTyCtx <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyCtx
miTys)
  TyDefCtx
topTyDefns <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Getter s a -> Sem r a
use (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyDefCtx
miTydefs)

  -- Choose the contexts to use based on mode: if we are loading a
  -- standalone module, we should start it in an empty context.  If we
  -- are loading something entered at the REPL, we need to include any
  -- existing top-level REPL context.
  let importMap :: Map ModuleName ModuleInfo
importMap = case LoadingMode
mode of LoadingMode
Standalone -> Map ModuleName ModuleInfo
modImps; LoadingMode
REPL -> Map ModuleName ModuleInfo
topImports forall a. Semigroup a => a -> a -> a
<> Map ModuleName ModuleInfo
modImps
      tyctx :: TyCtx
tyctx = case LoadingMode
mode of LoadingMode
Standalone -> forall a b. Ctx a b
emptyCtx; LoadingMode
REPL -> TyCtx
topTyCtx
      tydefns :: TyDefCtx
tydefns = case LoadingMode
mode of LoadingMode
Standalone -> forall k a. Map k a
M.empty; LoadingMode
REPL -> TyDefCtx
topTyDefns

  -- Typecheck (and resolve names in) the module.
  ModuleInfo
m <- forall (r :: [(* -> *) -> * -> *]) a.
Member (Error DiscoError) r =>
TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem r a
runTCM TyCtx
tyctx TyDefCtx
tydefns forall a b. (a -> b) -> a -> b
$ forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error LocTCError, Fresh]
  r =>
ModuleName
-> Map ModuleName ModuleInfo -> Module -> Sem r ModuleInfo
checkModule ModuleName
name Map ModuleName ModuleInfo
importMap Module
cm

  -- Evaluate all the module definitions and add them to the topEnv.
  forall e1 e2 (r :: [(* -> *) -> * -> *]) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError EvalError -> DiscoError
EvalErr forall a b. (a -> b) -> a -> b
$ forall (r :: [(* -> *) -> * -> *]).
Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
ModuleInfo -> Sem r ()
loadDefsFrom ModuleInfo
m

  -- Record the ModuleInfo record in the top-level map.
  forall s (r :: [(* -> *) -> * -> *]).
Member (State s) r =>
(s -> s) -> Sem r ()
modify (Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ModuleName
name ModuleInfo
m)
  forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
m

-- | Try loading the contents of a file from the filesystem, emitting
--   an error if it's not found.
loadFile :: Members '[Output (Message ann), Embed IO] r => FilePath -> Sem r (Maybe String)
loadFile :: forall ann (r :: [(* -> *) -> * -> *]).
Members '[Output (Message ann), Embed IO] r =>
FilePath -> Sem r (Maybe FilePath)
loadFile FilePath
file = do
  Either SomeException FilePath
res <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle @SomeException (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left) (forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
readFile FilePath
file)
  case Either SomeException FilePath
res of
    Left SomeException
_ -> forall ann (r :: [(* -> *) -> * -> *]).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ann)
"File not found:" forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
file) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Right FilePath
s -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just FilePath
s)

-- | Add things from the given module to the set of currently loaded
--   things.
addToREPLModule ::
  Members '[Error DiscoError, State TopInfo, Random, State Mem, Output (Message ann)] r =>
  ModuleInfo ->
  Sem r ()
addToREPLModule :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[Error DiscoError, State TopInfo, Random, State Mem,
    Output (Message ann)]
  r =>
ModuleInfo -> Sem r ()
addToREPLModule ModuleInfo
mi = forall s (r :: [(* -> *) -> * -> *]).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo (Lens' TopInfo ModuleInfo
replModInfo forall a s t. Semigroup a => ASetter s t a a -> a -> s -> t
<>~ ModuleInfo
mi)

-- | Set the given 'ModuleInfo' record as the currently loaded
--   module. This also includes updating the top-level state with new
--   term definitions, documentation, types, and type definitions.
--   Replaces any previously loaded module.
setREPLModule ::
  Members '[State TopInfo, Random, Error EvalError, State Mem, Output (Message ann)] r =>
  ModuleInfo ->
  Sem r ()
setREPLModule :: forall ann (r :: [(* -> *) -> * -> *]).
Members
  '[State TopInfo, Random, Error EvalError, State Mem,
    Output (Message ann)]
  r =>
ModuleInfo -> Sem r ()
setREPLModule ModuleInfo
mi = do
  forall s (r :: [(* -> *) -> * -> *]).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo forall a b. (a -> b) -> a -> b
$ Lens' TopInfo ModuleInfo
replModInfo forall s t a b. ASetter s t a b -> b -> s -> t
.~ ModuleInfo
mi

-- | Populate various pieces of the top-level info record (docs, type
--   context, type and term definitions) from the 'ModuleInfo' record
--   corresponding to the currently loaded module, and load all the
--   definitions into the current top-level environment.
loadDefsFrom ::
  Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
  ModuleInfo ->
  Sem r ()
loadDefsFrom :: forall (r :: [(* -> *) -> * -> *]).
Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
ModuleInfo -> Sem r ()
loadDefsFrom ModuleInfo
mi = do
  -- Note that the compiled definitions we get back from compileDefns
  -- are topologically sorted by mutually recursive group. Each
  -- definition needs to be evaluated in an environment containing the
  -- previous ones.

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (r :: [(* -> *) -> * -> *]).
Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
QName Core -> Core -> Sem r ()
loadDef) (Ctx ATerm Defn -> [(QName Core, Core)]
compileDefns (ModuleInfo
mi forall s a. s -> Getting a s a -> a
^. Lens' ModuleInfo (Ctx ATerm Defn)
miTermdefs))

loadDef ::
  Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
  QName Core ->
  Core ->
  Sem r ()
loadDef :: forall (r :: [(* -> *) -> * -> *]).
Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
QName Core -> Core -> Sem r ()
loadDef QName Core
x Core
body = do
  Value
v <- forall s (r :: [(* -> *) -> * -> *]) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: [(* -> *) -> * -> *]) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv forall a b. (a -> b) -> a -> b
$ forall (r :: [(* -> *) -> * -> *]).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Core -> Sem r Value
eval Core
body
  forall s (r :: [(* -> *) -> * -> *]).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo forall a b. (a -> b) -> a -> b
$ Lens' TopInfo Env
topEnv forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert QName Core
x Value
v