{-# 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           Prelude
import           System.FilePath          ((-<.>))

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 :: Bool -> DiscoConfig
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 :: ModuleInfo
-> Env
-> Map ModuleName ModuleInfo
-> Maybe FilePath
-> DiscoConfig
-> TopInfo
TopInfo
  { _replModInfo :: ModuleInfo
_replModInfo = ModuleInfo
emptyModuleInfo
  , _topEnv :: Env
_topEnv      = Env
forall a b. Ctx a b
emptyCtx
  , _topModMap :: Map ModuleName ModuleInfo
_topModMap   = Map ModuleName ModuleInfo
forall k a. Map k a
M.empty
  , _lastFile :: Maybe FilePath
_lastFile    = Maybe FilePath
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 =
  Settings IO
forall (m :: * -> *). MonadIO m => Settings m
H.defaultSettings
    { historyFile :: Maybe FilePath
H.historyFile = FilePath -> Maybe FilePath
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 :: EffectRow). Members DiscoEffects r => Sem r ())
-> IO ()
runDisco DiscoConfig
cfg forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
m =
  IO (TopInfo, (Mem, ())) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void
    (IO (TopInfo, (Mem, ())) -> IO ())
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> IO (TopInfo, (Mem, ())))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Settings IO
-> InputT IO (TopInfo, (Mem, ())) -> IO (TopInfo, (Mem, ()))
forall (m :: * -> *) a.
(MonadIO m, MonadMask m) =>
Settings m -> InputT m a -> m a
H.runInputT Settings IO
inputSettings
    (InputT IO (TopInfo, (Mem, ())) -> IO (TopInfo, (Mem, ())))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> InputT IO (TopInfo, (Mem, ())))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> IO (TopInfo, (Mem, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Monad (InputT IO) =>
Sem '[Final (InputT IO)] a -> InputT IO a
forall (m :: * -> *) a. Monad m => Sem '[Final m] a -> m a
runFinal @(H.InputT IO)
    (Sem '[Final (InputT IO)] (TopInfo, (Mem, ()))
 -> InputT IO (TopInfo, (Mem, ())))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem '[Final (InputT IO)] (TopInfo, (Mem, ())))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> InputT IO (TopInfo, (Mem, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Embed (InputT IO), Final (InputT IO)] (TopInfo, (Mem, ()))
-> Sem '[Final (InputT IO)] (TopInfo, (Mem, ()))
forall (m :: * -> *) (r :: EffectRow) a.
(Member (Final m) r, Functor m) =>
Sem (Embed m : r) a -> Sem r a
embedToFinal
    (Sem '[Embed (InputT IO), Final (InputT IO)] (TopInfo, (Mem, ()))
 -> Sem '[Final (InputT IO)] (TopInfo, (Mem, ())))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Embed (InputT IO), Final (InputT IO)] (TopInfo, (Mem, ())))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem '[Final (InputT IO)] (TopInfo, (Mem, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall x. IO x -> InputT IO x)
-> Sem
     '[Embed IO, Embed (InputT IO), Final (InputT IO)]
     (TopInfo, (Mem, ()))
-> Sem '[Embed (InputT IO), Final (InputT IO)] (TopInfo, (Mem, ()))
forall (m1 :: * -> *) (m2 :: * -> *) (r :: EffectRow) a.
Member (Embed m2) r =>
(forall x. m1 x -> m2 x) -> Sem (Embed m1 : r) a -> Sem r a
runEmbedded @_ @(H.InputT IO) forall x. IO x -> InputT IO x
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
    (Sem
   '[Embed IO, Embed (InputT IO), Final (InputT IO)]
   (TopInfo, (Mem, ()))
 -> Sem
      '[Embed (InputT IO), Final (InputT IO)] (TopInfo, (Mem, ())))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Embed IO, Embed (InputT IO), Final (InputT IO)]
         (TopInfo, (Mem, ())))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem '[Embed (InputT IO), Final (InputT IO)] (TopInfo, (Mem, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Message
 -> Sem '[Embed IO, Embed (InputT IO), Final (InputT IO)] ())
-> Sem
     '[Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     (TopInfo, (Mem, ()))
-> Sem
     '[Embed IO, Embed (InputT IO), Final (InputT IO)]
     (TopInfo, (Mem, ()))
forall o (r :: EffectRow) a.
(o -> Sem r ()) -> Sem (Output o : r) a -> Sem r a
runOutputSem ((Message -> Bool)
-> Message
-> Sem '[Embed IO, Embed (InputT IO), Final (InputT IO)] ()
forall (r :: EffectRow).
Member (Embed IO) r =>
(Message -> Bool) -> Message -> Sem r ()
handleMsg Message -> Bool
msgFilter)    -- Handle Output Message via printing to console
    (Sem
   '[Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
   (TopInfo, (Mem, ()))
 -> Sem
      '[Embed IO, Embed (InputT IO), Final (InputT IO)]
      (TopInfo, (Mem, ())))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
         (TopInfo, (Mem, ())))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Embed IO, Embed (InputT IO), Final (InputT IO)]
     (TopInfo, (Mem, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopInfo
-> Sem
     '[State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     (Mem, ())
-> Sem
     '[Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     (TopInfo, (Mem, ()))
forall s (r :: EffectRow) 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
    (Sem
   '[State TopInfo, Output Message, Embed IO, Embed (InputT IO),
     Final (InputT IO)]
   (Mem, ())
 -> Sem
      '[Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      (TopInfo, (Mem, ())))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[State TopInfo, Output Message, Embed IO, Embed (InputT IO),
           Final (InputT IO)]
         (Mem, ()))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     (TopInfo, (Mem, ()))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  '[Input TopInfo, State TopInfo, Output Message, Embed IO,
    Embed (InputT IO), Final (InputT IO)]
  (Mem, ())
-> Sem
     '[State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     (Mem, ())
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState                          -- Dispatch Input TopInfo effect via State effect
    (Sem
   '[Input TopInfo, State TopInfo, Output Message, Embed IO,
     Embed (InputT IO), Final (InputT IO)]
   (Mem, ())
 -> Sem
      '[State TopInfo, Output Message, Embed IO, Embed (InputT IO),
        Final (InputT IO)]
      (Mem, ()))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Input TopInfo, State TopInfo, Output Message, Embed IO,
           Embed (InputT IO), Final (InputT IO)]
         (Mem, ()))
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     (Mem, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mem
-> Sem
     '[State Mem, Input TopInfo, State TopInfo, Output Message,
       Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     (Mem, ())
forall s (r :: EffectRow) a.
s -> Sem (State s : r) a -> Sem r (s, a)
runState Mem
emptyMem                     -- Start with empty memory
    (Sem
   '[State Mem, Input TopInfo, State TopInfo, Output Message,
     Embed IO, Embed (InputT IO), Final (InputT IO)]
   ()
 -> Sem
      '[Input TopInfo, State TopInfo, Output Message, Embed IO,
        Embed (InputT IO), Final (InputT IO)]
      (Mem, ()))
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[State Mem, Input TopInfo, State TopInfo, Output Message,
           Embed IO, Embed (InputT IO), Final (InputT IO)]
         ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     (Mem, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  '[Error DiscoError, State Mem, Input TopInfo, State TopInfo,
    Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
  ()
-> Sem
     '[State Mem, Input TopInfo, State TopInfo, Output Message,
       Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem (Error DiscoError : r) () -> Sem r ()
outputDiscoErrors                     -- Output any top-level errors
    (Sem
   '[Error DiscoError, State Mem, Input TopInfo, State TopInfo,
     Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
   ()
 -> Sem
      '[State Mem, Input TopInfo, State TopInfo, Output Message,
        Embed IO, Embed (InputT IO), Final (InputT IO)]
      ())
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Error DiscoError, State Mem, Input TopInfo, State TopInfo,
           Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
         ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[State Mem, Input TopInfo, State TopInfo, Output Message,
       Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  '[LFresh, Error DiscoError, State Mem, Input TopInfo,
    State TopInfo, Output Message, Embed IO, Embed (InputT IO),
    Final (InputT IO)]
  ()
-> Sem
     '[Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh                             -- Generate locally fresh names
    (Sem
   '[LFresh, Error DiscoError, State Mem, Input TopInfo,
     State TopInfo, Output Message, Embed IO, Embed (InputT IO),
     Final (InputT IO)]
   ()
 -> Sem
      '[Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ())
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[LFresh, Error DiscoError, State Mem, Input TopInfo,
           State TopInfo, Output Message, Embed IO, Embed (InputT IO),
           Final (InputT IO)]
         ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  '[Random, LFresh, Error DiscoError, State Mem, Input TopInfo,
    State TopInfo, Output Message, Embed IO, Embed (InputT IO),
    Final (InputT IO)]
  ()
-> Sem
     '[LFresh, Error DiscoError, State Mem, Input TopInfo,
       State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     ()
forall (r :: EffectRow) a.
Member (Embed IO) r =>
Sem (Random : r) a -> Sem r a
runRandomIO                           -- Generate randomness via IO
    (Sem
   '[Random, LFresh, Error DiscoError, State Mem, Input TopInfo,
     State TopInfo, Output Message, Embed IO, Embed (InputT IO),
     Final (InputT IO)]
   ()
 -> Sem
      '[LFresh, Error DiscoError, State Mem, Input TopInfo,
        State TopInfo, Output Message, Embed IO, Embed (InputT IO),
        Final (InputT IO)]
      ())
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Random, LFresh, Error DiscoError, State Mem, Input TopInfo,
           State TopInfo, Output Message, Embed IO, Embed (InputT IO),
           Final (InputT IO)]
         ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[LFresh, Error DiscoError, State Mem, Input TopInfo,
       State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (EvalError -> DiscoError)
-> Sem
     '[Error EvalError, Random, LFresh, Error DiscoError, State Mem,
       Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Random, LFresh, Error DiscoError, State Mem, Input TopInfo,
       State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     ()
forall e1 e2 (r :: EffectRow) 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
    (Sem
   '[Error EvalError, Random, LFresh, Error DiscoError, State Mem,
     Input TopInfo, State TopInfo, Output Message, Embed IO,
     Embed (InputT IO), Final (InputT IO)]
   ()
 -> Sem
      '[Random, LFresh, Error DiscoError, State Mem, Input TopInfo,
        State TopInfo, Output Message, Embed IO, Embed (InputT IO),
        Final (InputT IO)]
      ())
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Error EvalError, Random, LFresh, Error DiscoError, State Mem,
           Input TopInfo, State TopInfo, Output Message, Embed IO,
           Embed (InputT IO), Final (InputT IO)]
         ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Random, LFresh, Error DiscoError, State Mem, Input TopInfo,
       State TopInfo, Output Message, Embed IO, Embed (InputT IO),
       Final (InputT IO)]
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> DiscoError)
-> Sem
     '[Fail, Error EvalError, Random, LFresh, Error DiscoError,
       State Mem, Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Error EvalError, Random, LFresh, Error DiscoError, State Mem,
       Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     ()
forall e (r :: EffectRow) 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
    (Sem
   '[Fail, Error EvalError, Random, LFresh, Error DiscoError,
     State Mem, Input TopInfo, State TopInfo, Output Message, Embed IO,
     Embed (InputT IO), Final (InputT IO)]
   ()
 -> Sem
      '[Error EvalError, Random, LFresh, Error DiscoError, State Mem,
        Input TopInfo, State TopInfo, Output Message, Embed IO,
        Embed (InputT IO), Final (InputT IO)]
      ())
-> (Sem
      '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
        Error DiscoError, State Mem, Input TopInfo, State TopInfo,
        Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
      ()
    -> Sem
         '[Fail, Error EvalError, Random, LFresh, Error DiscoError,
           State Mem, Input TopInfo, State TopInfo, Output Message, Embed IO,
           Embed (InputT IO), Final (InputT IO)]
         ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Error EvalError, Random, LFresh, Error DiscoError, State Mem,
       Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx Any Any
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> Sem
     '[Fail, Error EvalError, Random, LFresh, Error DiscoError,
       State Mem, Input TopInfo, State TopInfo, Output Message, Embed IO,
       Embed (InputT IO), Final (InputT IO)]
     ()
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader Ctx Any Any
forall a b. Ctx a b
emptyCtx                    -- Keep track of current Env
    (Sem
   '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
     Error DiscoError, State Mem, Input TopInfo, State TopInfo,
     Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
   ()
 -> IO ())
-> Sem
     '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
       Error DiscoError, State Mem, Input TopInfo, State TopInfo,
       Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
     ()
-> IO ()
forall a b. (a -> b) -> a -> b
$ Sem
  '[Reader (Ctx Any Any), Fail, Error EvalError, Random, LFresh,
    Error DiscoError, State Mem, Input TopInfo, State TopInfo,
    Output Message, Embed IO, Embed (InputT IO), Final (InputT IO)]
  ()
forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
m
  where
    msgFilter :: Message -> Bool
msgFilter
      | DiscoConfig
cfg DiscoConfig -> Getting Bool DiscoConfig Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool DiscoConfig Bool
Iso' DiscoConfig Bool
debugMode = Bool -> Message -> Bool
forall a b. a -> b -> a
const Bool
True
      | Bool
otherwise        = (MessageType -> MessageType -> Bool
forall a. Eq a => a -> a -> Bool
/= MessageType
Debug) (MessageType -> Bool)
-> (Message -> MessageType) -> Message -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting MessageType Message MessageType -> Message -> MessageType
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting MessageType Message MessageType
Lens' Message 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 :: Sem (Input Env : r) a -> Sem r a
inputTopEnv Sem (Input Env : r) a
m = do
  Env
e <- (TopInfo -> Env) -> Sem r Env
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (Getting Env TopInfo Env -> TopInfo -> Env
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting Env TopInfo Env
Lens' TopInfo Env
topEnv)
  Env -> Sem (Input Env : r) a -> Sem r a
forall i (r :: EffectRow) 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 :: FilePath -> Sem r Module
parseDiscoModule FilePath
file = do
  FilePath
str <- IO FilePath -> Sem r FilePath
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FilePath -> Sem r FilePath) -> IO FilePath -> Sem r FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> IO FilePath
readFile FilePath
file
  Either DiscoError Module -> Sem r Module
forall e (r :: EffectRow) a.
Member (Error e) r =>
Either e a -> Sem r a
fromEither (Either DiscoError Module -> Sem r Module)
-> (Either (ParseErrorBundle FilePath DiscoParseError) Module
    -> Either DiscoError Module)
-> Either (ParseErrorBundle FilePath DiscoParseError) Module
-> Sem r Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ParseErrorBundle FilePath DiscoParseError -> DiscoError)
-> Either (ParseErrorBundle FilePath DiscoParseError) Module
-> Either DiscoError Module
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ParseErrorBundle FilePath DiscoParseError -> DiscoError
ParseErr (Either (ParseErrorBundle FilePath DiscoParseError) Module
 -> Sem r Module)
-> Either (ParseErrorBundle FilePath DiscoParseError) Module
-> Sem r Module
forall a b. (a -> b) -> a -> b
$ Parser Module
-> FilePath
-> FilePath
-> Either (ParseErrorBundle FilePath DiscoParseError) Module
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 :: TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem r a
runTCM TyCtx
tyCtx TyDefCtx
tyDefCtx =
  (LocTCError -> DiscoError)
-> Sem (Error LocTCError : r) a -> Sem r a
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError LocTCError -> DiscoError
TypeCheckErr
    (Sem (Error LocTCError : r) a -> Sem r a)
-> (Sem
      (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
    -> Sem (Error LocTCError : r) a)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Fresh : Error LocTCError : r) a
-> Sem (Error LocTCError : r) a
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh
    (Sem (Fresh : Error LocTCError : r) a
 -> Sem (Error LocTCError : r) a)
-> (Sem
      (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
    -> Sem (Fresh : Error LocTCError : r) a)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem (Error LocTCError : r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyDefCtx
-> Sem (Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem (Fresh : Error LocTCError : r) a
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader @TyDefCtx TyDefCtx
tyDefCtx
    (Sem (Reader TyDefCtx : Fresh : Error LocTCError : r) a
 -> Sem (Fresh : Error LocTCError : r) a)
-> (Sem
      (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
    -> Sem (Reader TyDefCtx : Fresh : Error LocTCError : r) a)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem (Fresh : Error LocTCError : r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r) a
-> Sem (Reader TyDefCtx : Fresh : Error LocTCError : r) a
forall i (r :: EffectRow) 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' :: TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
runTCM' TyCtx
tyCtx TyDefCtx
tyDefCtx =
  (TCError -> DiscoError) -> Sem (Error TCError : r) a -> Sem r a
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError (LocTCError -> DiscoError
TypeCheckErr (LocTCError -> DiscoError)
-> (TCError -> LocTCError) -> TCError -> DiscoError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCError -> LocTCError
noLoc)
    (Sem (Error TCError : r) a -> Sem r a)
-> (Sem
      (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
    -> Sem (Error TCError : r) a)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Fresh : Error TCError : r) a -> Sem (Error TCError : r) a
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh
    (Sem (Fresh : Error TCError : r) a -> Sem (Error TCError : r) a)
-> (Sem
      (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
    -> Sem (Fresh : Error TCError : r) a)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem (Error TCError : r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyDefCtx
-> Sem (Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem (Fresh : Error TCError : r) a
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader @TyDefCtx TyDefCtx
tyDefCtx
    (Sem (Reader TyDefCtx : Fresh : Error TCError : r) a
 -> Sem (Fresh : Error TCError : r) a)
-> (Sem
      (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
    -> Sem (Reader TyDefCtx : Fresh : Error TCError : r) a)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem (Fresh : Error TCError : r) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem (Reader TyDefCtx : Fresh : Error TCError : r) a
forall i (r :: EffectRow) 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 :: 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  <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (Getting TyCtx TopInfo TyCtx -> TopInfo -> TyCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyCtx ModuleInfo)
-> TopInfo -> Const TyCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyCtx ModuleInfo)
 -> TopInfo -> Const TyCtx TopInfo)
-> ((TyCtx -> Const TyCtx TyCtx)
    -> ModuleInfo -> Const TyCtx ModuleInfo)
-> Getting TyCtx TopInfo TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo
Lens' ModuleInfo TyCtx
miTys))
  [TyCtx]
imptyctx <- (TopInfo -> [TyCtx]) -> Sem r [TyCtx]
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (Getting (Endo [TyCtx]) TopInfo TyCtx -> TopInfo -> [TyCtx]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf ((ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> TopInfo -> Const (Endo [TyCtx]) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
 -> TopInfo -> Const (Endo [TyCtx]) TopInfo)
-> ((TyCtx -> Const (Endo [TyCtx]) TyCtx)
    -> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> Getting (Endo [TyCtx]) TopInfo TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ModuleName ModuleInfo
 -> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo))
-> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo
Lens' ModuleInfo (Map ModuleName ModuleInfo)
miImports ((Map ModuleName ModuleInfo
  -> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo))
 -> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> ((TyCtx -> Const (Endo [TyCtx]) TyCtx)
    -> Map ModuleName ModuleInfo
    -> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo))
-> (TyCtx -> Const (Endo [TyCtx]) TyCtx)
-> ModuleInfo
-> Const (Endo [TyCtx]) ModuleInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> Map ModuleName ModuleInfo
-> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
 -> Map ModuleName ModuleInfo
 -> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo))
-> ((TyCtx -> Const (Endo [TyCtx]) TyCtx)
    -> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo)
-> (TyCtx -> Const (Endo [TyCtx]) TyCtx)
-> Map ModuleName ModuleInfo
-> Const (Endo [TyCtx]) (Map ModuleName ModuleInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Const (Endo [TyCtx]) TyCtx)
-> ModuleInfo -> Const (Endo [TyCtx]) ModuleInfo
Lens' ModuleInfo TyCtx
miTys))
  TyDefCtx
tydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (Getting TyDefCtx TopInfo TyDefCtx -> TopInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyDefCtx ModuleInfo)
 -> TopInfo -> Const TyDefCtx TopInfo)
-> ((TyDefCtx -> Const TyDefCtx TyDefCtx)
    -> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> Getting TyDefCtx TopInfo TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs))
  [TyDefCtx]
imptydefs <- (TopInfo -> [TyDefCtx]) -> Sem r [TyDefCtx]
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs (Getting (Endo [TyDefCtx]) TopInfo TyDefCtx -> TopInfo -> [TyDefCtx]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf ((ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> TopInfo -> Const (Endo [TyDefCtx]) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
 -> TopInfo -> Const (Endo [TyDefCtx]) TopInfo)
-> ((TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
    -> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> Getting (Endo [TyDefCtx]) TopInfo TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ModuleName ModuleInfo
 -> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo))
-> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo
Lens' ModuleInfo (Map ModuleName ModuleInfo)
miImports ((Map ModuleName ModuleInfo
  -> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo))
 -> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> ((TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
    -> Map ModuleName ModuleInfo
    -> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo))
-> (TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
-> ModuleInfo
-> Const (Endo [TyDefCtx]) ModuleInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> Map ModuleName ModuleInfo
-> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
 -> Map ModuleName ModuleInfo
 -> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo))
-> ((TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
    -> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo)
-> (TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
-> Map ModuleName ModuleInfo
-> Const (Endo [TyDefCtx]) (Map ModuleName ModuleInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> Const (Endo [TyDefCtx]) TyDefCtx)
-> ModuleInfo -> Const (Endo [TyDefCtx]) ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs))
  TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
forall (r :: EffectRow) a.
Member (Error DiscoError) r =>
TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
runTCM' (TyCtx
tyctx TyCtx -> TyCtx -> TyCtx
forall a. Semigroup a => a -> a -> a
<> [TyCtx] -> TyCtx
forall a. Monoid a => [a] -> a
mconcat [TyCtx]
imptyctx) (TyDefCtx
tydefs TyDefCtx -> TyDefCtx -> TyDefCtx
forall a. Semigroup a => a -> a -> a
<> [TyDefCtx] -> TyDefCtx
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, Random, State Mem, Error DiscoError, Embed IO] r
  => Bool -> Resolver -> FilePath -> Sem r ModuleInfo
loadDiscoModule :: Bool -> Resolver -> FilePath -> Sem r ModuleInfo
loadDiscoModule Bool
quiet Resolver
resolver =
  Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, 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, Random, State Mem, Error DiscoError, Embed IO] r
  => Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule :: Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule Bool
quiet Resolver
resolver =
  Bool
-> LoadingMode
-> Resolver
-> [ModuleName]
-> ModuleName
-> Module
-> Sem r ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, 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, Random, State Mem, Error DiscoError, Embed IO] r
  => Bool -> Resolver -> [ModuleName] -> FilePath
  -> Sem r ModuleInfo
loadDiscoModule' :: Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
loadDiscoModule' Bool
quiet Resolver
resolver [ModuleName]
inProcess FilePath
modPath  = do
  (FilePath
resolvedPath, ModuleProvenance
prov) <- Resolver -> FilePath -> Sem r (Maybe (FilePath, ModuleProvenance))
forall (r :: EffectRow).
Member (Embed IO) r =>
Resolver -> FilePath -> Sem r (Maybe (FilePath, ModuleProvenance))
resolveModule Resolver
resolver FilePath
modPath
                  Sem r (Maybe (FilePath, ModuleProvenance))
-> (Maybe (FilePath, ModuleProvenance)
    -> Sem r (FilePath, ModuleProvenance))
-> Sem r (FilePath, ModuleProvenance)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sem r (FilePath, ModuleProvenance)
-> ((FilePath, ModuleProvenance)
    -> Sem r (FilePath, ModuleProvenance))
-> Maybe (FilePath, ModuleProvenance)
-> Sem r (FilePath, ModuleProvenance)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (DiscoError -> Sem r (FilePath, ModuleProvenance)
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (DiscoError -> Sem r (FilePath, ModuleProvenance))
-> DiscoError -> Sem r (FilePath, ModuleProvenance)
forall a b. (a -> b) -> a -> b
$ FilePath -> DiscoError
ModuleNotFound FilePath
modPath) (FilePath, ModuleProvenance) -> Sem r (FilePath, ModuleProvenance)
forall (m :: * -> *) a. Monad m => a -> m a
return
  let name :: ModuleName
name = ModuleProvenance -> FilePath -> ModuleName
Named ModuleProvenance
prov FilePath
modPath
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ModuleName
name ModuleName -> [ModuleName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ModuleName]
inProcess) (DiscoError -> Sem r ()
forall e (r :: EffectRow) a. Member (Error e) r => e -> Sem r a
throw (DiscoError -> Sem r ()) -> DiscoError -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [ModuleName] -> DiscoError
CyclicImport (ModuleName
nameModuleName -> [ModuleName] -> [ModuleName]
forall a. a -> [a] -> [a]
:[ModuleName]
inProcess))
  Map ModuleName ModuleInfo
modMap <- Getter TopInfo (Map ModuleName ModuleInfo)
-> Sem r (Map ModuleName ModuleInfo)
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo Lens' TopInfo (Map ModuleName ModuleInfo)
Getter TopInfo (Map ModuleName ModuleInfo)
topModMap
  case ModuleName -> Map ModuleName ModuleInfo -> Maybe ModuleInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ModuleName
name Map ModuleName ModuleInfo
modMap of
    Just ModuleInfo
mi -> ModuleInfo -> Sem r ModuleInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ModuleInfo
mi
    Maybe ModuleInfo
Nothing -> do
      Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
quiet (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"Loading" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> FilePath -> Sem r Doc
forall (m :: * -> *). Applicative m => FilePath -> m Doc
text (FilePath
modPath FilePath -> FilePath -> FilePath
-<.> FilePath
"disco") Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
Pretty.<> Sem r Doc
"..."
      Module
cm <- FilePath -> Sem r Module
forall (r :: EffectRow).
Members '[Error DiscoError, Embed IO] r =>
FilePath -> Sem r Module
parseDiscoModule FilePath
resolvedPath
      Bool
-> LoadingMode
-> Resolver
-> [ModuleName]
-> ModuleName
-> Module
-> Sem r ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, 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 ModuleName -> [ModuleName] -> [ModuleName]
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, Random, State Mem, Error DiscoError, Embed IO] r
  => Bool -> LoadingMode -> Resolver -> [ModuleName] -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule' :: 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 <- (FilePath -> Sem r ModuleInfo) -> [FilePath] -> Sem r [ModuleInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, 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 Ext -> Set Ext -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Module -> Set Ext
modExts Module
cm of
    Bool
True  -> [ModuleInfo] -> Sem r [ModuleInfo]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    Bool
False -> (FilePath -> Sem r ModuleInfo) -> [FilePath] -> Sem r [ModuleInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, 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 = [(ModuleName, ModuleInfo)] -> Map ModuleName ModuleInfo
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((ModuleInfo -> (ModuleName, ModuleInfo))
-> [ModuleInfo] -> [(ModuleName, ModuleInfo)]
forall a b. (a -> b) -> [a] -> [b]
map (Getting ModuleName ModuleInfo ModuleName
-> ModuleInfo -> ModuleName
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting ModuleName ModuleInfo ModuleName
Lens' ModuleInfo ModuleName
miName (ModuleInfo -> ModuleName)
-> (ModuleInfo -> ModuleInfo)
-> ModuleInfo
-> (ModuleName, ModuleInfo)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& ModuleInfo -> ModuleInfo
forall a. a -> a
id) ([ModuleInfo]
mis [ModuleInfo] -> [ModuleInfo] -> [ModuleInfo]
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 <- Getter TopInfo (Map ModuleName ModuleInfo)
-> Sem r (Map ModuleName ModuleInfo)
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo)
-> ((Map ModuleName ModuleInfo -> f (Map ModuleName ModuleInfo))
    -> ModuleInfo -> f ModuleInfo)
-> (Map ModuleName ModuleInfo -> f (Map ModuleName ModuleInfo))
-> TopInfo
-> f TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map ModuleName ModuleInfo -> f (Map ModuleName ModuleInfo))
-> ModuleInfo -> f ModuleInfo
Lens' ModuleInfo (Map ModuleName ModuleInfo)
miImports)
  TyCtx
topTyCtx   <- Getter TopInfo TyCtx -> Sem r TyCtx
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo)
-> ((TyCtx -> f TyCtx) -> ModuleInfo -> f ModuleInfo)
-> (TyCtx -> f TyCtx)
-> TopInfo
-> f TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> f TyCtx) -> ModuleInfo -> f ModuleInfo
Lens' ModuleInfo TyCtx
miTys)
  TyDefCtx
topTyDefns <- Getter TopInfo TyDefCtx -> Sem r TyDefCtx
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo)
-> ((TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo)
-> (TyDefCtx -> f TyDefCtx)
-> TopInfo
-> f TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo
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 Map ModuleName ModuleInfo
-> Map ModuleName ModuleInfo -> Map ModuleName ModuleInfo
forall a. Semigroup a => a -> a -> a
<> Map ModuleName ModuleInfo
modImps }
      tyctx :: TyCtx
tyctx   = case LoadingMode
mode of { LoadingMode
Standalone -> TyCtx
forall a b. Ctx a b
emptyCtx ; LoadingMode
REPL -> TyCtx
topTyCtx }
      tydefns :: TyDefCtx
tydefns = case LoadingMode
mode of { LoadingMode
Standalone -> TyDefCtx
forall k a. Map k a
M.empty ; LoadingMode
REPL -> TyDefCtx
topTyDefns }

  -- Typecheck (and resolve names in) the module.
  ModuleInfo
m  <- TyCtx
-> TyDefCtx
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r)
     ModuleInfo
-> Sem r ModuleInfo
forall (r :: EffectRow) 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 (Sem
   (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r)
   ModuleInfo
 -> Sem r ModuleInfo)
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r)
     ModuleInfo
-> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ ModuleName
-> Map ModuleName ModuleInfo
-> Module
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error LocTCError : r)
     ModuleInfo
forall (r :: EffectRow).
Members
  '[Output Message, 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.
  (EvalError -> DiscoError)
-> Sem (Error EvalError : r) () -> Sem r ()
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError EvalError -> DiscoError
EvalErr (Sem (Error EvalError : r) () -> Sem r ())
-> Sem (Error EvalError : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Sem (Error EvalError : r) ()
forall (r :: EffectRow).
Members '[State TopInfo, Random, Error EvalError, State Mem] r =>
ModuleInfo -> Sem r ()
loadDefsFrom ModuleInfo
m

  -- Record the ModuleInfo record in the top-level map.
  (TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify ((Map ModuleName ModuleInfo -> Identity (Map ModuleName ModuleInfo))
-> TopInfo -> Identity TopInfo
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap ((Map ModuleName ModuleInfo
  -> Identity (Map ModuleName ModuleInfo))
 -> TopInfo -> Identity TopInfo)
-> (Map ModuleName ModuleInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> TopInfo
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ModuleName
-> ModuleInfo
-> Map ModuleName ModuleInfo
-> Map ModuleName ModuleInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ModuleName
name ModuleInfo
m)
  ModuleInfo -> Sem r ModuleInfo
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, Embed IO] r => FilePath -> Sem r (Maybe String)
loadFile :: FilePath -> Sem r (Maybe FilePath)
loadFile FilePath
file = do
  Either SomeException FilePath
res <- IO (Either SomeException FilePath)
-> Sem r (Either SomeException FilePath)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either SomeException FilePath)
 -> Sem r (Either SomeException FilePath))
-> IO (Either SomeException FilePath)
-> Sem r (Either SomeException FilePath)
forall a b. (a -> b) -> a -> b
$ (SomeException -> IO (Either SomeException FilePath))
-> IO (Either SomeException FilePath)
-> IO (Either SomeException FilePath)
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle @SomeException (Either SomeException FilePath -> IO (Either SomeException FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SomeException FilePath
 -> IO (Either SomeException FilePath))
-> (SomeException -> Either SomeException FilePath)
-> SomeException
-> IO (Either SomeException FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> Either SomeException FilePath
forall a b. a -> Either a b
Left) (FilePath -> Either SomeException FilePath
forall a b. b -> Either a b
Right (FilePath -> Either SomeException FilePath)
-> IO FilePath -> IO (Either SomeException FilePath)
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
_  -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc
"File not found:" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> FilePath -> Sem r Doc
forall (m :: * -> *). Applicative m => FilePath -> m Doc
text FilePath
file) Sem r () -> Sem r (Maybe FilePath) -> Sem r (Maybe FilePath)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe FilePath -> Sem r (Maybe FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe FilePath
forall a. Maybe a
Nothing
    Right FilePath
s -> Maybe FilePath -> Sem r (Maybe FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Maybe FilePath
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] r
  => ModuleInfo -> Sem r ()
addToREPLModule :: ModuleInfo -> Sem r ()
addToREPLModule ModuleInfo
mi = (TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((ModuleInfo -> Identity ModuleInfo) -> TopInfo -> Identity TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Identity ModuleInfo)
 -> TopInfo -> Identity TopInfo)
-> ModuleInfo -> TopInfo -> TopInfo
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] r
  => ModuleInfo -> Sem r ()
setREPLModule :: ModuleInfo -> Sem r ()
setREPLModule ModuleInfo
mi = do
  forall (r :: EffectRow).
Member (State TopInfo) r =>
(TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((TopInfo -> TopInfo) -> Sem r ())
-> (TopInfo -> TopInfo) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ (ModuleInfo -> Identity ModuleInfo) -> TopInfo -> Identity TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Identity ModuleInfo)
 -> TopInfo -> Identity TopInfo)
-> ModuleInfo -> TopInfo -> TopInfo
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 :: 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.

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

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