{-# 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 qualified Data.List.NonEmpty as NonEmpty
import Disco.AST.Core
import Disco.AST.Surface
import Disco.Compile (compileDefns)
import Disco.Context as Ctx
import Disco.Error
import Disco.Exhaustiveness (checkClauses)
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
------------------------------------------------------------

newtype 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 = 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
    { H.historyFile = Just ".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 =
  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 (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 (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) IO x -> InputT IO x
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) ann.
Member (Embed IO) r =>
(Message ann -> Bool) -> Message ann -> 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 ann (r :: EffectRow).
Member (Output (Message ann)) 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
 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
forall ann (f :: * -> *).
Functor f =>
(MessageType -> f MessageType) -> Message ann -> f (Message ann)
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 :: EffectRow) a.
Member (Input TopInfo) r =>
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 :: forall (r :: EffectRow).
Members '[Error DiscoError, Embed IO] r =>
FilePath -> Sem r Module
parseDiscoModule FilePath
file = do
  FilePath
str <- IO FilePath -> Sem r FilePath
forall a. IO a -> Sem r a
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 a b c. (a -> b) -> Either a c -> Either b c
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 :: 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
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
. 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
. 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' :: 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 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
. 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
. 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 :: forall (r :: EffectRow) 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 <- (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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map ModuleName a -> f (Map ModuleName 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map ModuleName a -> f (Map ModuleName 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 ann), Random, State Mem, Error DiscoError, Embed IO] r =>
  Bool ->
  Resolver ->
  FilePath ->
  Sem r ModuleInfo
loadDiscoModule :: forall ann (r :: EffectRow).
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 =
  Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
forall ann (r :: EffectRow).
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 :: EffectRow).
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 =
  Bool
-> LoadingMode
-> Resolver
-> [ModuleName]
-> ModuleName
-> Module
-> Sem r ModuleInfo
forall ann (r :: EffectRow).
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 :: EffectRow).
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) <-
    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 a b. Sem r a -> (a -> Sem r b) -> Sem r b
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 a. a -> Sem r a
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 a. Eq a => a -> [a] -> 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
name ModuleName -> [ModuleName] -> [ModuleName]
forall a. a -> [a] -> [a]
: [ModuleName]
inProcess))
  Map ModuleName ModuleInfo
modMap <- forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo (Map ModuleName ModuleInfo -> f (Map ModuleName ModuleInfo))
-> TopInfo -> f 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 a. a -> Sem r a
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 ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ann) -> Sem r ()) -> Sem r (Doc ann) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ann)
"Loading" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> FilePath -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text (FilePath
modPath FilePath -> FilePath -> FilePath
-<.> FilePath
"disco") Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
Pretty.<> Sem r (Doc ann)
"..."
      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 ann (r :: EffectRow).
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 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 ann), Random, State Mem, Error DiscoError, Embed IO] r =>
  Bool ->
  LoadingMode ->
  Resolver ->
  [ModuleName] ->
  ModuleName ->
  Module ->
  Sem r ModuleInfo
loadParsedDiscoModule' :: forall ann (r :: EffectRow).
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 <- (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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
forall ann (r :: EffectRow).
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 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 a. a -> Sem r a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Bool -> Resolver -> [ModuleName] -> FilePath -> Sem r ModuleInfo
forall ann (r :: EffectRow).
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 = [(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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
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 ann (r :: EffectRow).
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

  -- Check for partial functions
  let allTyDefs :: TyDefCtx
allTyDefs = (TyDefBody -> TyDefBody -> TyDefBody)
-> TyDefCtx -> TyDefCtx -> TyDefCtx
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith TyDefBody -> TyDefBody -> TyDefBody
forall a b. a -> b -> a
const TyDefCtx
tydefns (ModuleInfo
m ModuleInfo
-> ((TyDefCtx -> Const TyDefCtx TyDefCtx)
    -> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TyDefCtx
forall s a. s -> Getting a s a -> a
^. (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs)
  Sem (Fresh : r) () -> Sem r ()
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh (Sem (Fresh : r) () -> Sem r ()) -> Sem (Fresh : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ (Defn -> Sem (Fresh : r) ()) -> [Defn] -> Sem (Fresh : r) ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TyDefCtx -> Defn -> Sem (Fresh : r) ()
forall ann (r :: EffectRow).
Members '[Fresh, Output (Message ann), Embed IO] r =>
TyDefCtx -> Defn -> Sem r ()
checkExhaustive TyDefCtx
allTyDefs) (Ctx ATerm Defn -> [Defn]
forall a b. Ctx a b -> [b]
Ctx.elems (Ctx ATerm Defn -> [Defn]) -> Ctx ATerm Defn -> [Defn]
forall a b. (a -> b) -> a -> b
$ ModuleInfo
m 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)

  -- 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 a. a -> Sem r a
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 :: EffectRow).
Members '[Output (Message ann), Embed IO] r =>
FilePath -> Sem r (Maybe FilePath)
loadFile FilePath
file = do
  Either SomeException FilePath
res <- IO (Either SomeException FilePath)
-> Sem r (Either SomeException FilePath)
forall a. IO a -> Sem r a
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
$ forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle @SomeException (Either SomeException FilePath -> IO (Either SomeException FilePath)
forall a. a -> IO a
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 ann) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ann)
"File not found:" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> FilePath -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
file) Sem r () -> Sem r (Maybe FilePath) -> Sem r (Maybe FilePath)
forall a b. Sem r a -> Sem r b -> Sem r b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe FilePath -> Sem r (Maybe FilePath)
forall a. a -> Sem r a
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 a. a -> Sem r a
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 ann)] r =>
  ModuleInfo ->
  Sem r ()
addToREPLModule :: forall ann (r :: EffectRow).
Members
  '[Error DiscoError, State TopInfo, Random, State Mem,
    Output (Message ann)]
  r =>
ModuleInfo -> Sem r ()
addToREPLModule ModuleInfo
mi = 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 ann)] r =>
  ModuleInfo ->
  Sem r ()
setREPLModule :: forall ann (r :: EffectRow).
Members
  '[State TopInfo, Random, Error EvalError, State Mem,
    Output (Message ann)]
  r =>
ModuleInfo -> Sem r ()
setREPLModule ModuleInfo
mi = do
  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 :: forall (r :: EffectRow).
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.

  ((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 :: forall (r :: EffectRow).
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 :: 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 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

checkExhaustive :: Members '[Fresh, Output (Message ann), Embed IO] r => TyDefCtx -> Defn -> Sem r ()
checkExhaustive :: forall ann (r :: EffectRow).
Members '[Fresh, Output (Message ann), Embed IO] r =>
TyDefCtx -> Defn -> Sem r ()
checkExhaustive TyDefCtx
tyDefCtx (Defn Name ATerm
name [Type]
argsType Type
_ NonEmpty (Bind [APattern] ATerm)
boundClauses) = do
  NonEmpty [APattern]
clauses <- (([APattern], ATerm) -> [APattern])
-> NonEmpty ([APattern], ATerm) -> NonEmpty [APattern]
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NonEmpty.map ([APattern], ATerm) -> [APattern]
forall a b. (a, b) -> a
fst (NonEmpty ([APattern], ATerm) -> NonEmpty [APattern])
-> Sem r (NonEmpty ([APattern], ATerm))
-> Sem r (NonEmpty [APattern])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bind [APattern] ATerm -> Sem r ([APattern], ATerm))
-> NonEmpty (Bind [APattern] ATerm)
-> Sem r (NonEmpty ([APattern], ATerm))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM Bind [APattern] ATerm -> Sem r ([APattern], ATerm)
forall (r :: EffectRow) p t.
(Member Fresh r, Alpha p, Alpha t) =>
Bind p t -> Sem r (p, t)
unbind NonEmpty (Bind [APattern] ATerm)
boundClauses
  forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader @TyDefCtx TyDefCtx
tyDefCtx (Sem (Reader TyDefCtx : r) () -> Sem r ())
-> Sem (Reader TyDefCtx : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Name ATerm
-> [Type] -> NonEmpty [APattern] -> Sem (Reader TyDefCtx : r) ()
forall ann (r :: EffectRow).
Members
  '[Fresh, Reader TyDefCtx, Output (Message ann), Embed IO] r =>
Name ATerm -> [Type] -> NonEmpty [APattern] -> Sem r ()
checkClauses Name ATerm
name [Type]
argsType NonEmpty [APattern]
clauses