{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE PatternSynonyms    #-}
{-# LANGUAGE StandaloneDeriving #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Disco.Interactive.Commands
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Defining and dispatching all commands/functionality available at
-- the REPL prompt.
-----------------------------------------------------------------------------

module Disco.Interactive.Commands
  ( dispatch,
    discoCommands,
    handleLoad,
    loadFile,
    parseLine
  ) where

import           Control.Arrow                    ((&&&))
import           Control.Lens                     (to, view, (%~), (.~), (?~),
                                                   (^.))
import           Control.Monad.Except
import           Data.Char                        (isSpace)
import           Data.Coerce
import           Data.List                        (find, isPrefixOf, sortBy)
import           Data.Map                         ((!))
import qualified Data.Map                         as M
import           Data.Typeable
import           Prelude                          as P
import           System.FilePath                  (splitFileName)

import           Text.Megaparsec                  hiding (State, runParser)
import qualified Text.Megaparsec.Char             as C
import           Unbound.Generics.LocallyNameless (Name, name2String,
                                                   string2Name)

import           Disco.Effects.Input
import           Disco.Effects.LFresh
import           Disco.Effects.State
import           Polysemy
import           Polysemy.Error                   hiding (try)
import           Polysemy.Output
import           Polysemy.Reader

import           Data.Maybe                       (maybeToList)
import           Disco.AST.Surface
import           Disco.AST.Typed
import           Disco.Compile
import           Disco.Context                    as Ctx
import           Disco.Desugar
import           Disco.Doc
import           Disco.Error
import           Disco.Eval
import           Disco.Extensions
import           Disco.Interpret.CESK
import           Disco.Messages
import           Disco.Module
import           Disco.Names
import           Disco.Parser                     (Parser, ident, reservedOp,
                                                   runParser, sc, symbol, term,
                                                   wholeModule, withExts)
import           Disco.Pretty                     hiding (empty, (<>))
import qualified Disco.Pretty                     as Pretty
import           Disco.Syntax.Operators
import           Disco.Syntax.Prims               (Prim (PrimBOp, PrimUOp),
                                                   toPrim)
import           Disco.Typecheck
import           Disco.Typecheck.Erase
import           Disco.Types                      (pattern TyString, toPolyType)
import           Disco.Value

------------------------------------------------------------
-- REPL expression type
------------------------------------------------------------

-- | Data type to represent things typed at the Disco REPL.  Each
--   constructor has a singleton type to facilitate dispatch.
data REPLExpr :: CmdTag -> * where
  TypeCheck :: Term      -> REPLExpr 'CTypeCheck -- Typecheck a term
  Eval      :: Module    -> REPLExpr 'CEval      -- Evaluate a block
  TestProp  :: Term      -> REPLExpr 'CTestProp  -- Run a property test
  ShowDefn  :: Name Term -> REPLExpr 'CShowDefn  -- Show a variable's definition
  Parse     :: Term      -> REPLExpr 'CParse     -- Show the parsed AST
  Pretty    :: Term      -> REPLExpr 'CPretty    -- Pretty-print a term
  Print     :: Term      -> REPLExpr 'CPrint     -- Print a string
  Ann       :: Term      -> REPLExpr 'CAnn       -- Show type-annotated term
  Desugar   :: Term      -> REPLExpr 'CDesugar   -- Show a desugared term
  Compile   :: Term      -> REPLExpr 'CCompile   -- Show a compiled term
  Load      :: FilePath  -> REPLExpr 'CLoad      -- Load a file.
  Reload    ::              REPLExpr 'CReload    -- Reloads the most recently
                                                 -- loaded file.
  Doc       :: DocInput  -> REPLExpr 'CDoc       -- Show documentation.
  Nop       ::              REPLExpr 'CNop       -- No-op, e.g. if the user
                                                 -- just enters a comment
  Help      ::              REPLExpr 'CHelp      -- Show help
  Names     ::              REPLExpr 'CNames     -- Show bound names

deriving instance Show (REPLExpr c)

-- | An existential wrapper around any REPL expression.
data SomeREPLExpr where
  SomeREPL :: Typeable c => REPLExpr c -> SomeREPLExpr

------------------------------------------------------------
-- REPL command types
------------------------------------------------------------

data REPLCommandCategory
  = -- | REPL commands for everyday users
    User
  | -- | REPL commands for developers working on Disco
    Dev
  deriving (REPLCommandCategory -> REPLCommandCategory -> Bool
(REPLCommandCategory -> REPLCommandCategory -> Bool)
-> (REPLCommandCategory -> REPLCommandCategory -> Bool)
-> Eq REPLCommandCategory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: REPLCommandCategory -> REPLCommandCategory -> Bool
$c/= :: REPLCommandCategory -> REPLCommandCategory -> Bool
== :: REPLCommandCategory -> REPLCommandCategory -> Bool
$c== :: REPLCommandCategory -> REPLCommandCategory -> Bool
Eq, Int -> REPLCommandCategory -> ShowS
[REPLCommandCategory] -> ShowS
REPLCommandCategory -> String
(Int -> REPLCommandCategory -> ShowS)
-> (REPLCommandCategory -> String)
-> ([REPLCommandCategory] -> ShowS)
-> Show REPLCommandCategory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [REPLCommandCategory] -> ShowS
$cshowList :: [REPLCommandCategory] -> ShowS
show :: REPLCommandCategory -> String
$cshow :: REPLCommandCategory -> String
showsPrec :: Int -> REPLCommandCategory -> ShowS
$cshowsPrec :: Int -> REPLCommandCategory -> ShowS
Show)

data REPLCommandType
  = -- | Things that don't start with a colon: eval and nop
    BuiltIn
  | -- | Things that start with a colon, e.g. :help, :names, :load...
    ColonCmd
  deriving (REPLCommandType -> REPLCommandType -> Bool
(REPLCommandType -> REPLCommandType -> Bool)
-> (REPLCommandType -> REPLCommandType -> Bool)
-> Eq REPLCommandType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: REPLCommandType -> REPLCommandType -> Bool
$c/= :: REPLCommandType -> REPLCommandType -> Bool
== :: REPLCommandType -> REPLCommandType -> Bool
$c== :: REPLCommandType -> REPLCommandType -> Bool
Eq, Int -> REPLCommandType -> ShowS
[REPLCommandType] -> ShowS
REPLCommandType -> String
(Int -> REPLCommandType -> ShowS)
-> (REPLCommandType -> String)
-> ([REPLCommandType] -> ShowS)
-> Show REPLCommandType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [REPLCommandType] -> ShowS
$cshowList :: [REPLCommandType] -> ShowS
show :: REPLCommandType -> String
$cshow :: REPLCommandType -> String
showsPrec :: Int -> REPLCommandType -> ShowS
$cshowsPrec :: Int -> REPLCommandType -> ShowS
Show)

-- | Tags used at the type level to denote each REPL command.
data CmdTag
  = CTypeCheck
  | CEval
  | CShowDefn
  | CParse
  | CPretty
  | CPrint
  | CAnn
  | CDesugar
  | CCompile
  | CLoad
  | CReload
  | CDoc
  | CNop
  | CHelp
  | CNames
  | CTestProp
  deriving (Int -> CmdTag -> ShowS
[CmdTag] -> ShowS
CmdTag -> String
(Int -> CmdTag -> ShowS)
-> (CmdTag -> String) -> ([CmdTag] -> ShowS) -> Show CmdTag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CmdTag] -> ShowS
$cshowList :: [CmdTag] -> ShowS
show :: CmdTag -> String
$cshow :: CmdTag -> String
showsPrec :: Int -> CmdTag -> ShowS
$cshowsPrec :: Int -> CmdTag -> ShowS
Show, CmdTag -> CmdTag -> Bool
(CmdTag -> CmdTag -> Bool)
-> (CmdTag -> CmdTag -> Bool) -> Eq CmdTag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CmdTag -> CmdTag -> Bool
$c/= :: CmdTag -> CmdTag -> Bool
== :: CmdTag -> CmdTag -> Bool
$c== :: CmdTag -> CmdTag -> Bool
Eq, Typeable)

------------------------------------------------------------
-- REPL command info record
------------------------------------------------------------

-- | Data type to represent all the information about a single REPL
--   command.
data REPLCommand (c :: CmdTag) = REPLCommand
  { -- | Name of the command
    REPLCommand c -> String
name      :: String,
    -- | Help text showing how to use the command, e.g. ":ann <term>"
    REPLCommand c -> String
helpcmd   :: String,
    -- | Short free-form text explaining the command.
    --   We could also consider adding long help text as well.
    REPLCommand c -> String
shortHelp :: String,
    -- | Is the command for users or devs?
    REPLCommand c -> REPLCommandCategory
category  :: REPLCommandCategory,
    -- | Is it a built-in command or colon command?
    REPLCommand c -> REPLCommandType
cmdtype   :: REPLCommandType,
    -- | The action to execute,
    -- given the input to the
    -- command.
    REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action    :: REPLExpr c -> (forall r. Members DiscoEffects r => Sem r ()),
    -- | Parser for the command argument(s).
    REPLCommand c -> Parser (REPLExpr c)
parser    :: Parser (REPLExpr c)
  }

-- | An existential wrapper around any REPL command info record.
data SomeREPLCommand where
  SomeCmd :: Typeable c => REPLCommand c -> SomeREPLCommand

------------------------------------------------------------
-- REPL command lists
------------------------------------------------------------

type REPLCommands = [SomeREPLCommand]

-- | Keep only commands of a certain type.
byCmdType :: REPLCommandType -> REPLCommands -> REPLCommands
byCmdType :: REPLCommandType -> REPLCommands -> REPLCommands
byCmdType REPLCommandType
ty = (SomeREPLCommand -> Bool) -> REPLCommands -> REPLCommands
forall a. (a -> Bool) -> [a] -> [a]
P.filter (\(SomeCmd REPLCommand c
rc) -> REPLCommand c -> REPLCommandType
forall (c :: CmdTag). REPLCommand c -> REPLCommandType
cmdtype REPLCommand c
rc REPLCommandType -> REPLCommandType -> Bool
forall a. Eq a => a -> a -> Bool
== REPLCommandType
ty)

-- | Given a list of REPL commands and something typed at the REPL,
--   pick the first command with a matching type-level tag and run its
--   associated action.
dispatch :: Members DiscoEffects r => REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch :: REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch [] SomeREPLExpr
_ = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
dispatch (SomeCmd REPLCommand c
c : REPLCommands
cs) r :: SomeREPLExpr
r@(SomeREPL REPLExpr c
e) = case REPLExpr c -> Maybe (REPLExpr c)
forall k (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast REPLExpr c
e of
  Just REPLExpr c
e' -> Sem (Error DiscoError : r) () -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem (Error DiscoError : r) () -> Sem r ()
outputDiscoErrors (Sem (Error DiscoError : r) () -> Sem r ())
-> Sem (Error DiscoError : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (c :: CmdTag).
REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action REPLCommand c
c REPLExpr c
e'
  Maybe (REPLExpr c)
Nothing -> REPLCommands -> SomeREPLExpr -> Sem r ()
forall (r :: EffectRow).
Members DiscoEffects r =>
REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch REPLCommands
cs SomeREPLExpr
r

-- | The list of all commands that can be used at the REPL.
--   Resolution of REPL commands searches this list /in order/, which
--   means ambiguous command prefixes (e.g. :t for :type) are resolved
--   to the first matching command.
discoCommands :: REPLCommands
discoCommands :: REPLCommands
discoCommands =
  [ REPLCommand 'CAnn -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CAnn
annCmd,
    REPLCommand 'CCompile -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CCompile
compileCmd,
    REPLCommand 'CDesugar -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CDesugar
desugarCmd,
    REPLCommand 'CDoc -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CDoc
docCmd,
    REPLCommand 'CEval -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CEval
evalCmd,
    REPLCommand 'CHelp -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CHelp
helpCmd,
    REPLCommand 'CLoad -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CLoad
loadCmd,
    REPLCommand 'CNames -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CNames
namesCmd,
    REPLCommand 'CNop -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CNop
nopCmd,
    REPLCommand 'CParse -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CParse
parseCmd,
    REPLCommand 'CPretty -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CPretty
prettyCmd,
    REPLCommand 'CPrint -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CPrint
printCmd,
    REPLCommand 'CReload -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CReload
reloadCmd,
    REPLCommand 'CShowDefn -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CShowDefn
showDefnCmd,
    REPLCommand 'CTypeCheck -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTypeCheck
typeCheckCmd,
    REPLCommand 'CTestProp -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTestProp
testPropCmd
  ]

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

builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
builtinCommandParser =
  (SomeREPLCommand -> Parser SomeREPLExpr -> Parser SomeREPLExpr)
-> Parser SomeREPLExpr -> REPLCommands -> Parser SomeREPLExpr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr)
-> (SomeREPLCommand -> Parser SomeREPLExpr)
-> SomeREPLCommand
-> Parser SomeREPLExpr
-> Parser SomeREPLExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(SomeCmd REPLCommand c
rc) -> REPLExpr c -> SomeREPLExpr
forall (c :: CmdTag). Typeable c => REPLExpr c -> SomeREPLExpr
SomeREPL (REPLExpr c -> SomeREPLExpr)
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
-> Parser SomeREPLExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (REPLCommand c
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc))) Parser SomeREPLExpr
forall (f :: * -> *) a. Alternative f => f a
empty
    (REPLCommands -> Parser SomeREPLExpr)
-> (REPLCommands -> REPLCommands)
-> REPLCommands
-> Parser SomeREPLExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLCommandType -> REPLCommands -> REPLCommands
byCmdType REPLCommandType
BuiltIn

-- | Parse one of the colon commands in the given list of commands.
commandParser :: REPLCommands -> Parser SomeREPLExpr
commandParser :: REPLCommands -> Parser SomeREPLExpr
commandParser REPLCommands
allCommands =
  (String -> Parser String
symbol String
":" Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.lowerChar) Parser String
-> (String -> Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= REPLCommands -> String -> Parser SomeREPLExpr
parseCommandArgs REPLCommands
allCommands

-- | Given a list of available commands and a string seen after a
--   colon, return a parser for its arguments.
parseCommandArgs :: REPLCommands -> String -> Parser SomeREPLExpr
parseCommandArgs :: REPLCommands -> String -> Parser SomeREPLExpr
parseCommandArgs REPLCommands
allCommands String
cmd = Parser SomeREPLExpr
-> ((String, Parser SomeREPLExpr) -> Parser SomeREPLExpr)
-> Maybe (String, Parser SomeREPLExpr)
-> Parser SomeREPLExpr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Parser SomeREPLExpr
badCmd (String, Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b. (a, b) -> b
snd (Maybe (String, Parser SomeREPLExpr) -> Parser SomeREPLExpr)
-> Maybe (String, Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ ((String, Parser SomeREPLExpr) -> Bool)
-> [(String, Parser SomeREPLExpr)]
-> Maybe (String, Parser SomeREPLExpr)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String
cmd String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`) (String -> Bool)
-> ((String, Parser SomeREPLExpr) -> String)
-> (String, Parser SomeREPLExpr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Parser SomeREPLExpr) -> String
forall a b. (a, b) -> a
fst) [(String, Parser SomeREPLExpr)]
parsers
  where
    badCmd :: Parser SomeREPLExpr
badCmd = String -> Parser SomeREPLExpr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser SomeREPLExpr) -> String -> Parser SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ String
"Command \":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" is unrecognized."

    parsers :: [(String, Parser SomeREPLExpr)]
parsers =
      (SomeREPLCommand -> (String, Parser SomeREPLExpr))
-> REPLCommands -> [(String, Parser SomeREPLExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
rc) -> (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
name REPLCommand c
rc, REPLExpr c -> SomeREPLExpr
forall (c :: CmdTag). Typeable c => REPLExpr c -> SomeREPLExpr
SomeREPL (REPLExpr c -> SomeREPLExpr)
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
-> Parser SomeREPLExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPLCommand c
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc)) (REPLCommands -> [(String, Parser SomeREPLExpr)])
-> REPLCommands -> [(String, Parser SomeREPLExpr)]
forall a b. (a -> b) -> a -> b
$
        REPLCommandType -> REPLCommands -> REPLCommands
byCmdType REPLCommandType
ColonCmd REPLCommands
allCommands

-- | Parse a file name.
fileParser :: Parser FilePath
fileParser :: Parser String
fileParser = StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.spaceChar Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ((Token String -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace))

-- | A parser for something entered at the REPL prompt.
lineParser :: REPLCommands -> Parser SomeREPLExpr
lineParser :: REPLCommands -> Parser SomeREPLExpr
lineParser REPLCommands
allCommands =
  REPLCommands -> Parser SomeREPLExpr
builtinCommandParser REPLCommands
allCommands
    Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> REPLCommands -> Parser SomeREPLExpr
commandParser REPLCommands
allCommands

-- | Given a list of available REPL commands and the currently enabled
--   extensions, parse a string entered at the REPL prompt, returning
--   either a parse error message or a parsed REPL expression.
parseLine :: REPLCommands -> ExtSet -> String -> Either String SomeREPLExpr
parseLine :: REPLCommands -> ExtSet -> String -> Either String SomeREPLExpr
parseLine REPLCommands
allCommands ExtSet
exts String
s =
  case Parser SomeREPLExpr
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) SomeREPLExpr
forall a.
Parser a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
runParser (ExtSet -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall a. ExtSet -> Parser a -> Parser a
withExts ExtSet
exts (REPLCommands -> Parser SomeREPLExpr
lineParser REPLCommands
allCommands)) String
"" String
s of
    Left ParseErrorBundle String DiscoParseError
e  -> String -> Either String SomeREPLExpr
forall a b. a -> Either a b
Left (String -> Either String SomeREPLExpr)
-> String -> Either String SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle String DiscoParseError -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String DiscoParseError
e
    Right SomeREPLExpr
l -> SomeREPLExpr -> Either String SomeREPLExpr
forall a b. b -> Either a b
Right SomeREPLExpr
l

--------------------------------------------------------------------------------
-- The commands!
--------------------------------------------------------------------------------

------------------------------------------------------------
-- :ann

annCmd :: REPLCommand 'CAnn
annCmd :: REPLCommand 'CAnn
annCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"ann",
      helpcmd :: String
helpcmd = String
":ann",
      shortHelp :: String
shortHelp = String
"Show type-annotated typechecked term",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CAnn
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CAnn
x -> 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) () -> Sem r ())
-> (REPLExpr 'CAnn -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CAnn
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CAnn -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Error DiscoError, Input TopInfo, Output Message] r =>
REPLExpr 'CAnn -> Sem r ()
handleAnn (REPLExpr 'CAnn -> Sem r ()) -> REPLExpr 'CAnn -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CAnn
x,
      parser :: Parser (REPLExpr 'CAnn)
parser = Term -> REPLExpr 'CAnn
Ann (Term -> REPLExpr 'CAnn)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handleAnn ::
  Members '[Error DiscoError, Input TopInfo, Output Message] r =>
  REPLExpr 'CAnn ->
  Sem r ()
handleAnn :: REPLExpr 'CAnn -> Sem r ()
handleAnn (Ann Term
t) = do
  (ATerm
at, PolyType
_) <- Sem
  (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
  (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
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)
   (ATerm, PolyType)
 -> Sem r (ATerm, PolyType))
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
forall (r :: EffectRow).
Members
  '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
    Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
  ATerm -> Sem r ()
forall (r :: EffectRow) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
infoPretty ATerm
at

------------------------------------------------------------
-- :compile

compileCmd :: REPLCommand 'CCompile
compileCmd :: REPLCommand 'CCompile
compileCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"compile",
      helpcmd :: String
helpcmd = String
":compile",
      shortHelp :: String
shortHelp = String
"Show a compiled term",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CCompile
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CCompile
x -> 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) () -> Sem r ())
-> (REPLExpr 'CCompile -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CCompile
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CCompile -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Error DiscoError, Input TopInfo, Output Message] r =>
REPLExpr 'CCompile -> Sem r ()
handleCompile (REPLExpr 'CCompile -> Sem r ()) -> REPLExpr 'CCompile -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CCompile
x,
      parser :: Parser (REPLExpr 'CCompile)
parser = Term -> REPLExpr 'CCompile
Compile (Term -> REPLExpr 'CCompile)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CCompile)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handleCompile ::
  Members '[Error DiscoError, Input TopInfo, Output Message] r =>
  REPLExpr 'CCompile ->
  Sem r ()
handleCompile :: REPLExpr 'CCompile -> Sem r ()
handleCompile (Compile Term
t) = do
  (ATerm
at, PolyType
_) <- Sem
  (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
  (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
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)
   (ATerm, PolyType)
 -> Sem r (ATerm, PolyType))
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
forall (r :: EffectRow).
Members
  '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
    Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
  Core -> Sem r ()
forall (r :: EffectRow) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
infoPretty (Core -> Sem r ()) -> (ATerm -> Core) -> ATerm -> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Core
compileTerm (ATerm -> Sem r ()) -> ATerm -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ATerm
at

------------------------------------------------------------
-- :desugar

desugarCmd :: REPLCommand 'CDesugar
desugarCmd :: REPLCommand 'CDesugar
desugarCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"desugar",
      helpcmd :: String
helpcmd = String
":desugar",
      shortHelp :: String
shortHelp = String
"Show a desugared term",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CDesugar
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CDesugar
x -> 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) () -> Sem r ())
-> (REPLExpr 'CDesugar -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CDesugar
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CDesugar -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CDesugar -> Sem r ()
handleDesugar (REPLExpr 'CDesugar -> Sem r ()) -> REPLExpr 'CDesugar -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CDesugar
x,
      parser :: Parser (REPLExpr 'CDesugar)
parser = Term -> REPLExpr 'CDesugar
Desugar (Term -> REPLExpr 'CDesugar)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CDesugar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handleDesugar ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
  REPLExpr 'CDesugar ->
  Sem r ()
handleDesugar :: REPLExpr 'CDesugar -> Sem r ()
handleDesugar (Desugar Term
t) = do
  (ATerm
at, PolyType
_) <- Sem
  (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
  (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
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)
   (ATerm, PolyType)
 -> Sem r (ATerm, PolyType))
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
forall (r :: EffectRow).
Members
  '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
    Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
  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
$ Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (Term -> Sem r Doc) -> (ATerm -> Term) -> ATerm -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTerm -> Term
eraseDTerm (DTerm -> Term) -> (ATerm -> DTerm) -> ATerm -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Fresh] DTerm -> DTerm
forall a. Sem '[Fresh] a -> a
runDesugar (Sem '[Fresh] DTerm -> DTerm)
-> (ATerm -> Sem '[Fresh] DTerm) -> ATerm -> DTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Sem '[Fresh] DTerm
forall (r :: EffectRow). Member Fresh r => ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r Doc) -> ATerm -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ ATerm
at

------------------------------------------------------------
-- :doc

docCmd :: REPLCommand 'CDoc
docCmd :: REPLCommand 'CDoc
docCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"doc",
      helpcmd :: String
helpcmd = String
":doc <term>",
      shortHelp :: String
shortHelp = String
"Show documentation",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CDoc
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CDoc
x -> 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) () -> Sem r ())
-> (REPLExpr 'CDoc -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CDoc
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CDoc -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CDoc -> Sem r ()
handleDoc (REPLExpr 'CDoc -> Sem r ()) -> REPLExpr 'CDoc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CDoc
x,
      parser :: Parser (REPLExpr 'CDoc)
parser = DocInput -> REPLExpr 'CDoc
Doc (DocInput -> REPLExpr 'CDoc)
-> StateT ParserState (Parsec DiscoParseError String) DocInput
-> Parser (REPLExpr 'CDoc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) DocInput
parseDoc
    }

-- XXX
data DocInput = DocTerm Term | DocPrim Prim | DocOther String
  deriving (Int -> DocInput -> ShowS
[DocInput] -> ShowS
DocInput -> String
(Int -> DocInput -> ShowS)
-> (DocInput -> String) -> ([DocInput] -> ShowS) -> Show DocInput
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DocInput] -> ShowS
$cshowList :: [DocInput] -> ShowS
show :: DocInput -> String
$cshow :: DocInput -> String
showsPrec :: Int -> DocInput -> ShowS
$cshowsPrec :: Int -> DocInput -> ShowS
Show)

parseDoc :: Parser DocInput
parseDoc :: StateT ParserState (Parsec DiscoParseError String) DocInput
parseDoc =
      (Term -> DocInput
DocTerm (Term -> DocInput)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Term
term)
  StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Prim -> DocInput
DocPrim (Prim -> DocInput)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) Prim
parseNakedOpPrim StateT ParserState (Parsec DiscoParseError String) Prim
-> String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator"))
  StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> DocInput
DocOther (String -> DocInput)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
sc Parser () -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Token s -> m (Token s)
anySingleBut Char
Token String
' ')))

handleDoc ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
  REPLExpr 'CDoc ->
  Sem r ()
handleDoc :: REPLExpr 'CDoc -> Sem r ()
handleDoc (Doc (DocTerm (TBool Bool
_))) = Sem r ()
forall (r :: EffectRow). Members '[Output Message] r => Sem r ()
handleDocBool
handleDoc (Doc (DocTerm (TPrim Prim
p))) = Prim -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim -> Sem r ()
handleDocPrim Prim
p
handleDoc (Doc (DocTerm (TVar Name Term
x)))  = Name Term -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Name Term -> Sem r ()
handleDocVar Name Term
x
handleDoc (Doc (DocTerm Term
_))         =
  Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
err Sem r Doc
"Can't display documentation for an expression.  Try asking about a function, operator, or type name."
handleDoc (Doc (DocPrim Prim
p))         = Prim -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim -> Sem r ()
handleDocPrim Prim
p
handleDoc (Doc (DocOther String
s))        = String -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
String -> Sem r ()
handleDocOther String
s

handleDocBool :: Members '[Output Message] r => Sem r ()
handleDocBool :: Sem r ()
handleDocBool =
  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
"true and false (also written True and False) are the two possible values of type Boolean."
    Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
    String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
"bool"

handleDocVar ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
  Name Term ->
  Sem r ()
handleDocVar :: Name Term -> Sem r ()
handleDocVar Name Term
x = do
  TyCtx
replCtx  <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (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))
  TyDefCtx
replTydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (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))
  Ctx Term [DocThing]
replDocs <- (TopInfo -> Ctx Term [DocThing]) -> Sem r (Ctx Term [DocThing])
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting (Ctx Term [DocThing]) TopInfo (Ctx Term [DocThing])
-> TopInfo -> Ctx Term [DocThing]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> TopInfo -> Const (Ctx Term [DocThing]) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
 -> TopInfo -> Const (Ctx Term [DocThing]) TopInfo)
-> ((Ctx Term [DocThing]
     -> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
    -> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> Getting (Ctx Term [DocThing]) TopInfo (Ctx Term [DocThing])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ctx Term [DocThing]
 -> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
-> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo
Lens' ModuleInfo (Ctx Term [DocThing])
miDocs))

  TyCtx
importCtx <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([TyCtx] -> TyCtx
forall a b. [Ctx a b] -> Ctx a b
joinCtxs ([TyCtx] -> TyCtx) -> (TopInfo -> [TyCtx]) -> TopInfo -> TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyCtx) -> [ModuleInfo] -> [TyCtx]
forall a b. (a -> b) -> [a] -> [b]
map (((TyCtx -> Const TyCtx TyCtx)
 -> ModuleInfo -> Const TyCtx ModuleInfo)
-> ModuleInfo -> TyCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo
Lens' ModuleInfo TyCtx
miTys) ([ModuleInfo] -> [TyCtx])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [TyCtx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
M.elems (Map ModuleName ModuleInfo -> [ModuleInfo])
-> (TopInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> [ModuleInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
-> TopInfo -> Map ModuleName ModuleInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap)
  TyDefCtx
importTydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([TyDefCtx] -> TyDefCtx
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([TyDefCtx] -> TyDefCtx)
-> (TopInfo -> [TyDefCtx]) -> TopInfo -> TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyDefCtx) -> [ModuleInfo] -> [TyDefCtx]
forall a b. (a -> b) -> [a] -> [b]
map (((TyDefCtx -> Const TyDefCtx TyDefCtx)
 -> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> ModuleInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs) ([ModuleInfo] -> [TyDefCtx])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [TyDefCtx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
M.elems (Map ModuleName ModuleInfo -> [ModuleInfo])
-> (TopInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> [ModuleInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
-> TopInfo -> Map ModuleName ModuleInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap)
  Ctx Term [DocThing]
importDocs <- (TopInfo -> Ctx Term [DocThing]) -> Sem r (Ctx Term [DocThing])
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([Ctx Term [DocThing]] -> Ctx Term [DocThing]
forall a b. [Ctx a b] -> Ctx a b
joinCtxs ([Ctx Term [DocThing]] -> Ctx Term [DocThing])
-> (TopInfo -> [Ctx Term [DocThing]])
-> TopInfo
-> Ctx Term [DocThing]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Ctx Term [DocThing])
-> [ModuleInfo] -> [Ctx Term [DocThing]]
forall a b. (a -> b) -> [a] -> [b]
map (((Ctx Term [DocThing]
  -> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
 -> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> ModuleInfo -> Ctx Term [DocThing]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Ctx Term [DocThing]
 -> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
-> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo
Lens' ModuleInfo (Ctx Term [DocThing])
miDocs) ([ModuleInfo] -> [Ctx Term [DocThing]])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [Ctx Term [DocThing]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
M.elems (Map ModuleName ModuleInfo -> [ModuleInfo])
-> (TopInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> [ModuleInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
-> TopInfo -> Map ModuleName ModuleInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
  (Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap)

  let ctx :: TyCtx
ctx = TyCtx
replCtx TyCtx -> TyCtx -> TyCtx
forall a b. Ctx a b -> Ctx a b -> Ctx a b
`joinCtx` TyCtx
importCtx
      tydefs :: TyDefCtx
tydefs = TyDefCtx
importTydefs TyDefCtx -> TyDefCtx -> TyDefCtx
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` TyDefCtx
replTydefs
      docs :: Ctx Term [DocThing]
docs = Ctx Term [DocThing]
replDocs Ctx Term [DocThing] -> Ctx Term [DocThing] -> Ctx Term [DocThing]
forall a b. Ctx a b -> Ctx a b -> Ctx a b
`joinCtx` Ctx Term [DocThing]
importDocs

  Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc)
-> (Ctx Term [DocThing] -> String)
-> Ctx Term [DocThing]
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx Term [DocThing] -> String
forall a. Show a => a -> String
show (Ctx Term [DocThing] -> Sem r Doc)
-> Ctx Term [DocThing] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Ctx Term [DocThing]
docs

  case (Name Term -> TyCtx -> [(QName Term, PolyType)]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' Name Term
x TyCtx
ctx, String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Name Term -> String
forall a. Name a -> String
name2String Name Term
x) TyDefCtx
tydefs) of
    ([], Maybe TyDefBody
Nothing) ->
      -- Maybe the variable name entered by the user is actually a prim.
      case String -> [Prim]
toPrim (Name Term -> String
forall a. Name a -> String
name2String Name Term
x) of
        (Prim
prim:[Prim]
_) -> Prim -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim -> Sem r ()
handleDocPrim Prim
prim
        [Prim]
_        -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
err (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"No documentation found for '" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Name Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name Term
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"'."
    ([(QName Term, PolyType)]
binds, Maybe TyDefBody
def) ->
      (Either (QName Term, PolyType) TyDefBody -> Sem r ())
-> [Either (QName Term, PolyType) TyDefBody] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ctx Term [DocThing]
-> Either (QName Term, PolyType) TyDefBody -> Sem r ()
showDoc Ctx Term [DocThing]
docs) (((QName Term, PolyType) -> Either (QName Term, PolyType) TyDefBody)
-> [(QName Term, PolyType)]
-> [Either (QName Term, PolyType) TyDefBody]
forall a b. (a -> b) -> [a] -> [b]
map (QName Term, PolyType) -> Either (QName Term, PolyType) TyDefBody
forall a b. a -> Either a b
Left [(QName Term, PolyType)]
binds [Either (QName Term, PolyType) TyDefBody]
-> [Either (QName Term, PolyType) TyDefBody]
-> [Either (QName Term, PolyType) TyDefBody]
forall a. [a] -> [a] -> [a]
++ (TyDefBody -> Either (QName Term, PolyType) TyDefBody)
-> [TyDefBody] -> [Either (QName Term, PolyType) TyDefBody]
forall a b. (a -> b) -> [a] -> [b]
map TyDefBody -> Either (QName Term, PolyType) TyDefBody
forall a b. b -> Either a b
Right (Maybe TyDefBody -> [TyDefBody]
forall a. Maybe a -> [a]
maybeToList Maybe TyDefBody
def))

  where
    showDoc :: Ctx Term [DocThing]
-> Either (QName Term, PolyType) TyDefBody -> Sem r ()
showDoc Ctx Term [DocThing]
docMap (Left (QName Term
qn, PolyType
ty)) = 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] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name Term
x, Sem r Doc
":", PolyType -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' PolyType
ty]
      Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
      case QName Term -> Ctx Term [DocThing] -> Maybe [DocThing]
forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' QName Term
qn Ctx Term [DocThing]
docMap of
        Just (DocString [String]
ss : [DocThing]
_) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"" Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
: (String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
ss [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""])
        Maybe [DocThing]
_                       -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
    showDoc Ctx Term [DocThing]
docMap (Right TyDefBody
tdBody) = 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
$
      (String, TyDefBody) -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (Name Term -> String
forall a. Name a -> String
name2String Name Term
x, TyDefBody
tdBody)
      Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
      case Name Term -> Ctx Term [DocThing] -> [(QName Term, [DocThing])]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' Name Term
x Ctx Term [DocThing]
docMap of
        ((QName Term
_, DocString [String]
ss : [DocThing]
_) : [(QName Term, [DocThing])]
_) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"" Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
: (String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
ss [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""])
        [(QName Term, [DocThing])]
_                           -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty

handleDocPrim ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
  Prim ->
  Sem r ()
handleDocPrim :: Prim -> Sem r ()
handleDocPrim Prim
prim = do
  REPLExpr 'CTypeCheck -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck (Term -> REPLExpr 'CTypeCheck
TypeCheck (Prim -> Term
TPrim Prim
prim))
  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] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat
    [ case Prim
prim of
        PrimUOp UOp
u -> Bool -> Bool -> [String] -> Sem r Doc
forall (m :: * -> *).
(IsString (m Doc), Monad m) =>
Bool -> Bool -> [String] -> m Doc
describeAlts (UFixity
f UFixity -> UFixity -> Bool
forall a. Eq a => a -> a -> Bool
== UFixity
Post) (UFixity
f UFixity -> UFixity -> Bool
forall a. Eq a => a -> a -> Bool
== UFixity
Pre) [String]
syns
          where
            OpInfo (UOpF UFixity
f UOp
_) [String]
syns Int
_ = Map UOp OpInfo
uopMap Map UOp OpInfo -> UOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
! UOp
u
        PrimBOp BOp
b -> Bool -> Bool -> [String] -> Sem r Doc
forall (m :: * -> *).
(IsString (m Doc), Monad m) =>
Bool -> Bool -> [String] -> m Doc
describeAlts Bool
True Bool
True (OpInfo -> [String]
opSyns (OpInfo -> [String]) -> OpInfo -> [String]
forall a b. (a -> b) -> a -> b
$ Map BOp OpInfo
bopMap Map BOp OpInfo -> BOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
! BOp
b)
        Prim
_         -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
    , case Prim
prim of
        PrimUOp UOp
u -> Int -> Sem r Doc
forall (f :: * -> *) a.
(Applicative f, IsString (f Doc), Show a) =>
a -> f Doc
describePrec (UOp -> Int
uPrec UOp
u)
        PrimBOp BOp
b -> Int -> Sem r Doc
forall (f :: * -> *) a.
(Applicative f, IsString (f Doc), Show a) =>
a -> f Doc
describePrec (BOp -> Int
bPrec BOp
b) Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> BFixity -> Sem r Doc
forall (m :: * -> *).
(Applicative m, IsString (m Doc)) =>
BFixity -> m Doc
describeFixity (BOp -> BFixity
assoc BOp
b)
        Prim
_         -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
    ]
  case (Prim -> Map Prim String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Prim
prim Map Prim String
primDoc, Prim -> Map Prim String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Prim
prim Map Prim String
primReference) of
    (Maybe String
Nothing, Maybe String
Nothing) -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    (Maybe String
Nothing, Just String
p)  -> 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
$ String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p
    (Just String
d, Maybe String
mp)  ->
      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
"" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
d Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc -> (String -> Sem r Doc) -> Maybe String -> Sem r Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty (\String
p -> String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"") Maybe String
mp
  where
    describePrec :: a -> f Doc
describePrec a
p = f Doc
"precedence level" f Doc -> f Doc -> f Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> f Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (a -> String
forall a. Show a => a -> String
show a
p)
    describeFixity :: BFixity -> m Doc
describeFixity BFixity
In  = m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
    describeFixity BFixity
InL = m Doc
", left associative"
    describeFixity BFixity
InR = m Doc
", right associative"
    describeAlts :: Bool -> Bool -> [String] -> m Doc
describeAlts Bool
_ Bool
_ []            = m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
    describeAlts Bool
_ Bool
_ [String
_]           = m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
    describeAlts Bool
pre Bool
post (String
_:[String]
alts) = m Doc
"Alternative syntax:" m Doc -> m Doc -> m Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> m Doc -> [m Doc] -> m Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate m Doc
"," ((String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> m Doc
showOp [String]
alts)
      where
        showOp :: String -> m Doc
showOp String
op = [m Doc] -> m Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hcat
          [ if Bool
pre then m Doc
"~" else m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
          , String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
op
          , if Bool
post then m Doc
"~" else m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty]


mkReference :: String -> Sem r Doc
mkReference :: String -> Sem r Doc
mkReference String
p =
  Sem r Doc
"https://disco-lang.readthedocs.io/en/latest/reference/" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
p Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
".html"

handleDocOther ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
  String ->
  Sem r ()
handleDocOther :: String -> Sem r ()
handleDocOther String
s =
  case (String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
s Map String String
otherDoc, String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
s Map String String
otherReference) of
    (Maybe String
Nothing, Maybe String
Nothing) -> 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
"No documentation found for '" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
s Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"'."
    (Maybe String
Nothing, Just String
p)  -> 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
$ String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p
    (Just String
d, Maybe String
mp)  ->
      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
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
d Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc -> (String -> Sem r Doc) -> Maybe String -> Sem r Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty (\String
p -> String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"") Maybe String
mp

------------------------------------------------------------
-- eval

evalCmd :: REPLCommand 'CEval
evalCmd :: REPLCommand 'CEval
evalCmd = REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
  { name :: String
name      = String
"eval"
  , helpcmd :: String
helpcmd   = String
"<code>"
  , shortHelp :: String
shortHelp = String
"Evaluate a block of code"
  , category :: REPLCommandCategory
category  = REPLCommandCategory
User
  , cmdtype :: REPLCommandType
cmdtype   = REPLCommandType
BuiltIn
  , action :: REPLExpr 'CEval
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action    = \REPLExpr 'CEval
x -> REPLExpr 'CEval -> Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output Message : Embed IO : EvalEffects)
  r =>
REPLExpr 'CEval -> Sem r ()
handleEval REPLExpr 'CEval
x
  , parser :: Parser (REPLExpr 'CEval)
parser    = Module -> REPLExpr 'CEval
Eval (Module -> REPLExpr 'CEval)
-> StateT ParserState (Parsec DiscoParseError String) Module
-> Parser (REPLExpr 'CEval)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoadingMode
-> StateT ParserState (Parsec DiscoParseError String) Module
wholeModule LoadingMode
REPL
  }

handleEval
  :: Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r
  => REPLExpr 'CEval -> Sem r ()
handleEval :: REPLExpr 'CEval -> Sem r ()
handleEval (Eval Module
m) = do
  ModuleInfo
mi <- 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) ModuleInfo -> Sem r ModuleInfo)
-> Sem (Input TopInfo : r) ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ Bool
-> Resolver
-> ModuleName
-> Module
-> Sem (Input TopInfo : r) ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule Bool
False Resolver
FromCwdOrStdlib ModuleName
REPLModule Module
m
  ModuleInfo -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, State TopInfo, Random, State Mem,
    Output Message]
  r =>
ModuleInfo -> Sem r ()
addToREPLModule ModuleInfo
mi
  [(ATerm, PolyType)]
-> ((ATerm, PolyType) -> Sem r Value) -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ModuleInfo
mi ModuleInfo
-> Getting [(ATerm, PolyType)] ModuleInfo [(ATerm, PolyType)]
-> [(ATerm, PolyType)]
forall s a. s -> Getting a s a -> a
^. Getting [(ATerm, PolyType)] ModuleInfo [(ATerm, PolyType)]
Lens' ModuleInfo [(ATerm, PolyType)]
miTerms) ((EvalError -> DiscoError)
-> Sem (Error EvalError : r) Value -> Sem r Value
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) Value -> Sem r Value)
-> ((ATerm, PolyType) -> Sem (Error EvalError : r) Value)
-> (ATerm, PolyType)
-> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ATerm -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members
  (Error EvalError : State TopInfo : Output Message : EvalEffects)
  r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
True (ATerm -> Sem (Error EvalError : r) Value)
-> ((ATerm, PolyType) -> ATerm)
-> (ATerm, PolyType)
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, PolyType) -> ATerm
forall a b. (a, b) -> a
fst)
  -- garbageCollect?

-- First argument = should the value be printed?
evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => Bool -> ATerm -> Sem r Value
evalTerm :: Bool -> ATerm -> Sem r Value
evalTerm Bool
pr ATerm
at = do
  Env
env <- Getter TopInfo Env -> Sem r Env
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo Lens' TopInfo Env
Getter TopInfo Env
topEnv
  Value
v <- Env -> Sem (Input Env : r) Value -> Sem r Value
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst Env
env (Sem (Input Env : r) Value -> Sem r Value)
-> Sem (Input Env : r) Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Core -> Sem (Input Env : r) Value
forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Core -> Sem r Value
eval (ATerm -> Core
compileTerm ATerm
at)

  TyDefCtx
tydefs <- Getter TopInfo TyDefCtx -> Sem r TyDefCtx
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo ((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
. (ModuleInfo -> TyDefCtx)
-> (TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleInfo -> TyDefCtx
allTydefs)
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pr (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
$ TyDefCtx -> Sem (Input TyDefCtx : r) Doc -> Sem r Doc
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs (Sem (Input TyDefCtx : r) Doc -> Sem r Doc)
-> Sem (Input TyDefCtx : r) Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Type -> Value -> Sem (Input TyDefCtx : r) Doc
forall (r :: EffectRow).
Member (Input TyDefCtx) r =>
Type -> Value -> Sem r Doc
prettyValue' Type
ty Value
v

  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)
-> ((TyCtx -> Identity TyCtx) -> ModuleInfo -> Identity ModuleInfo)
-> (TyCtx -> Identity TyCtx)
-> TopInfo
-> Identity TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Identity TyCtx) -> ModuleInfo -> Identity ModuleInfo
Lens' ModuleInfo TyCtx
miTys ((TyCtx -> Identity TyCtx) -> TopInfo -> Identity TopInfo)
-> (TyCtx -> TyCtx) -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ QName Term -> PolyType -> TyCtx -> TyCtx
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (NameProvenance -> Name Term -> QName Term
forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
REPLModule) (String -> Name Term
forall a. String -> Name a
string2Name String
"it")) (Type -> PolyType
toPolyType Type
ty)) (TopInfo -> TopInfo) -> (TopInfo -> TopInfo) -> TopInfo -> TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ((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 (NameProvenance -> Name Core -> QName Core
forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
REPLModule) (String -> Name Core
forall a. String -> Name a
string2Name String
"it")) Value
v)
  Value -> Sem r Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
  where
    ty :: Type
ty = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at

------------------------------------------------------------
-- :help

helpCmd :: REPLCommand 'CHelp
helpCmd :: REPLCommand 'CHelp
helpCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"help",
      helpcmd :: String
helpcmd = String
":help",
      shortHelp :: String
shortHelp = String
"Show help",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CHelp
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CHelp
x -> REPLExpr 'CHelp -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
REPLExpr 'CHelp -> Sem r ()
handleHelp REPLExpr 'CHelp
x,
      parser :: Parser (REPLExpr 'CHelp)
parser = REPLExpr 'CHelp -> Parser (REPLExpr 'CHelp)
forall (m :: * -> *) a. Monad m => a -> m a
return REPLExpr 'CHelp
Help
    }

handleHelp :: Member (Output Message) r => REPLExpr 'CHelp -> Sem r ()
handleHelp :: REPLExpr 'CHelp -> Sem r ()
handleHelp REPLExpr 'CHelp
Help =
  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] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat
    [ Sem r Doc
"Commands available from the prompt:"
    , String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""
    , [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ((SomeREPLCommand -> Sem r Doc) -> REPLCommands -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
c) -> REPLCommand c -> Sem r Doc
forall (m :: * -> *) (c :: CmdTag).
Applicative m =>
REPLCommand c -> m Doc
showCmd REPLCommand c
c) (REPLCommands -> [Sem r Doc]) -> REPLCommands -> [Sem r Doc]
forall a b. (a -> b) -> a -> b
$ REPLCommands -> REPLCommands
sortedList REPLCommands
discoCommands)
    , String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""
    ]
  where
    maxlen :: Int
maxlen = REPLCommands -> Int
longestCmd REPLCommands
discoCommands
    sortedList :: REPLCommands -> REPLCommands
sortedList REPLCommands
cmds =
      (SomeREPLCommand -> SomeREPLCommand -> Ordering)
-> REPLCommands -> REPLCommands
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(SomeCmd REPLCommand c
x) (SomeCmd REPLCommand c
y) -> String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
name REPLCommand c
x) (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
name REPLCommand c
y)) (REPLCommands -> REPLCommands) -> REPLCommands -> REPLCommands
forall a b. (a -> b) -> a -> b
$ REPLCommands -> REPLCommands
filteredCommands REPLCommands
cmds
    --  don't show dev-only commands by default
    filteredCommands :: REPLCommands -> REPLCommands
filteredCommands REPLCommands
cmds = (SomeREPLCommand -> Bool) -> REPLCommands -> REPLCommands
forall a. (a -> Bool) -> [a] -> [a]
P.filter (\(SomeCmd REPLCommand c
c) -> REPLCommand c -> REPLCommandCategory
forall (c :: CmdTag). REPLCommand c -> REPLCommandCategory
category REPLCommand c
c REPLCommandCategory -> REPLCommandCategory -> Bool
forall a. Eq a => a -> a -> Bool
== REPLCommandCategory
User) REPLCommands
cmds
    showCmd :: REPLCommand c -> m Doc
showCmd REPLCommand c
c = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Int -> String
padRight (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
helpcmd REPLCommand c
c) Int
maxlen String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
shortHelp REPLCommand c
c)
    longestCmd :: REPLCommands -> Int
longestCmd REPLCommands
cmds = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (SomeREPLCommand -> Int) -> REPLCommands -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
c) -> String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
helpcmd REPLCommand c
c) REPLCommands
cmds
    padRight :: String -> Int -> String
padRight String
s Int
maxsize = Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
maxsize (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
' ')

------------------------------------------------------------
-- :load

loadCmd :: REPLCommand 'CLoad
loadCmd :: REPLCommand 'CLoad
loadCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"load",
      helpcmd :: String
helpcmd = String
":load <filename>",
      shortHelp :: String
shortHelp = String
"Load a file",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CLoad
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CLoad
x -> REPLExpr 'CLoad -> Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output Message : Embed IO : EvalEffects)
  r =>
REPLExpr 'CLoad -> Sem r ()
handleLoadWrapper REPLExpr 'CLoad
x,
      parser :: Parser (REPLExpr 'CLoad)
parser = String -> REPLExpr 'CLoad
Load (String -> REPLExpr 'CLoad)
-> Parser String -> Parser (REPLExpr 'CLoad)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
fileParser
    }

-- | Parses, typechecks, and loads a module by first recursively loading any imported
--   modules by calling loadDiscoModule. If no errors are thrown, any tests present
--   in the parent module are executed.
--   Disco.Interactive.CmdLine uses a version of this function that returns a Bool.
handleLoadWrapper ::
  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
  REPLExpr 'CLoad ->
  Sem r ()
handleLoadWrapper :: REPLExpr 'CLoad -> Sem r ()
handleLoadWrapper (Load String
fp) = Sem r Bool -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (String -> Sem r Bool
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output Message : Embed IO : EvalEffects)
  r =>
String -> Sem r Bool
handleLoad String
fp)

handleLoad ::
  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
  FilePath ->
  Sem r Bool
handleLoad :: String -> Sem r Bool
handleLoad String
fp = do
  let (String
directory, String
modName) = String -> (String, String)
splitFileName String
fp

  -- Reset top-level module map and context to empty, so we start
  -- fresh and pick up any changes to imported modules etc.
  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
$ (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 -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map ModuleName ModuleInfo
forall k a. Map k a
M.empty
  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 -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Env
forall a b. Ctx a b
Ctx.emptyCtx

  -- Load the module.
  ModuleInfo
m <- 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) ModuleInfo -> Sem r ModuleInfo)
-> Sem (Input TopInfo : r) ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ Bool -> Resolver -> String -> Sem (Input TopInfo : r) ModuleInfo
forall (r :: EffectRow).
Members
  '[State TopInfo, Output Message, Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> String -> Sem r ModuleInfo
loadDiscoModule Bool
False (String -> Resolver
FromDir String
directory) String
modName
  ModuleInfo -> Sem r ()
forall (r :: EffectRow).
Members
  '[State TopInfo, Random, Error EvalError, State Mem,
    Output Message]
  r =>
ModuleInfo -> Sem r ()
setREPLModule ModuleInfo
m

  -- Now run any tests
  Bool
t <- Sem (Input TopInfo : r) Bool -> Sem r Bool
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) Bool -> Sem r Bool)
-> Sem (Input TopInfo : r) Bool -> Sem r Bool
forall a b. (a -> b) -> a -> b
$ Ctx ATerm [ATerm] -> Sem (Input TopInfo : r) Bool
forall (r :: EffectRow).
Members (Output Message : Input TopInfo : EvalEffects) r =>
Ctx ATerm [ATerm] -> Sem r Bool
runAllTests (ModuleInfo
m ModuleInfo
-> Getting (Ctx ATerm [ATerm]) ModuleInfo (Ctx ATerm [ATerm])
-> Ctx ATerm [ATerm]
forall s a. s -> Getting a s a -> a
^. Getting (Ctx ATerm [ATerm]) ModuleInfo (Ctx ATerm [ATerm])
Lens' ModuleInfo (Ctx ATerm [ATerm])
miProps)

  -- Evaluate and print any top-level terms
  [(ATerm, PolyType)]
-> ((ATerm, PolyType) -> Sem r Value) -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ModuleInfo
m ModuleInfo
-> Getting [(ATerm, PolyType)] ModuleInfo [(ATerm, PolyType)]
-> [(ATerm, PolyType)]
forall s a. s -> Getting a s a -> a
^. Getting [(ATerm, PolyType)] ModuleInfo [(ATerm, PolyType)]
Lens' ModuleInfo [(ATerm, PolyType)]
miTerms) ((EvalError -> DiscoError)
-> Sem (Error EvalError : r) Value -> Sem r Value
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) Value -> Sem r Value)
-> ((ATerm, PolyType) -> Sem (Error EvalError : r) Value)
-> (ATerm, PolyType)
-> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ATerm -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members
  (Error EvalError : State TopInfo : Output Message : EvalEffects)
  r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
True (ATerm -> Sem (Error EvalError : r) Value)
-> ((ATerm, PolyType) -> ATerm)
-> (ATerm, PolyType)
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, PolyType) -> ATerm
forall a b. (a, b) -> a
fst)

  -- Remember which was the most recently loaded file, so we can :reload
  (TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((Maybe String -> Identity (Maybe String))
-> TopInfo -> Identity TopInfo
Lens' TopInfo (Maybe String)
lastFile ((Maybe String -> Identity (Maybe String))
 -> TopInfo -> Identity TopInfo)
-> String -> TopInfo -> TopInfo
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ String
fp)
  Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info Sem r Doc
"Loaded."
  Bool -> Sem r Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
t

-- XXX Return a structured summary of the results, not a Bool;
-- separate out results generation and pretty-printing, & move this
-- somewhere else.
runAllTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult])
runAllTests :: Ctx ATerm [ATerm] -> Sem r Bool
runAllTests Ctx ATerm [ATerm]
aprops
  | Ctx ATerm [ATerm] -> Bool
forall a b. Ctx a b -> Bool
Ctx.null Ctx ATerm [ATerm]
aprops = Bool -> Sem r Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  | Bool
otherwise     = do
      Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info Sem r Doc
"Running tests..."
      [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Sem r [Bool] -> Sem r Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((QName ATerm, [ATerm]) -> Sem r Bool)
-> [(QName ATerm, [ATerm])] -> Sem r [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((QName ATerm -> [ATerm] -> Sem r Bool)
-> (QName ATerm, [ATerm]) -> Sem r Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry QName ATerm -> [ATerm] -> Sem r Bool
forall (r :: EffectRow).
Members (Output Message : Input TopInfo : EvalEffects) r =>
QName ATerm -> [ATerm] -> Sem r Bool
runTests) (Ctx ATerm [ATerm] -> [(QName ATerm, [ATerm])]
forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs Ctx ATerm [ATerm]
aprops)

  where
    numSamples :: Int
    numSamples :: Int
numSamples = Int
50   -- XXX make this configurable somehow

    runTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => QName ATerm -> [AProperty] -> Sem r Bool
    runTests :: QName ATerm -> [ATerm] -> Sem r Bool
runTests (QName NameProvenance
_ Name ATerm
n) [ATerm]
props = do
      [(ATerm, TestResult)]
results <- Sem (Input Env : r) [(ATerm, TestResult)]
-> Sem r [(ATerm, TestResult)]
forall (r :: EffectRow) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv (Sem (Input Env : r) [(ATerm, TestResult)]
 -> Sem r [(ATerm, TestResult)])
-> Sem (Input Env : r) [(ATerm, TestResult)]
-> Sem r [(ATerm, TestResult)]
forall a b. (a -> b) -> a -> b
$ (ATerm -> Sem (Input Env : r) (ATerm, TestResult))
-> [ATerm] -> Sem (Input Env : r) [(ATerm, TestResult)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ATerm, Sem (Input Env : r) TestResult)
-> Sem (Input Env : r) (ATerm, TestResult)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA ((ATerm, Sem (Input Env : r) TestResult)
 -> Sem (Input Env : r) (ATerm, TestResult))
-> (ATerm -> (ATerm, Sem (Input Env : r) TestResult))
-> ATerm
-> Sem (Input Env : r) (ATerm, TestResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm -> ATerm
forall a. a -> a
id (ATerm -> ATerm)
-> (ATerm -> Sem (Input Env : r) TestResult)
-> ATerm
-> (ATerm, Sem (Input Env : r) TestResult)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Int -> ATerm -> Sem (Input Env : r) TestResult
forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Int -> ATerm -> Sem r TestResult
runTest Int
numSamples)) [ATerm]
props
      let failures :: [(ATerm, TestResult)]
failures = ((ATerm, TestResult) -> Bool)
-> [(ATerm, TestResult)] -> [(ATerm, TestResult)]
forall a. (a -> Bool) -> [a] -> [a]
P.filter (Bool -> Bool
not (Bool -> Bool)
-> ((ATerm, TestResult) -> Bool) -> (ATerm, TestResult) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestResult -> Bool
testIsOk (TestResult -> Bool)
-> ((ATerm, TestResult) -> TestResult)
-> (ATerm, TestResult)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, TestResult) -> TestResult
forall a b. (a, b) -> b
snd) [(ATerm, TestResult)]
results
          hdr :: Sem r Doc
hdr = Name ATerm -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name ATerm
n Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
":"

      case [(ATerm, TestResult)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures of
        Bool
True  -> 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
$ Int -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
hdr Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"OK"
        Bool
False -> do
          TyDefCtx
tydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (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
. (ModuleInfo -> TyDefCtx)
-> (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo
-> Const TyDefCtx ModuleInfo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleInfo -> TyDefCtx
allTydefs))
          let prettyFailures :: Sem r Doc
prettyFailures =
                TyDefCtx -> Sem (Input TyDefCtx : r) Doc -> Sem r Doc
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs (Sem (Input TyDefCtx : r) Doc -> Sem r Doc)
-> (Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
    -> Sem (Input TyDefCtx : r) Doc)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PA
-> Sem (Reader PA : Input TyDefCtx : r) Doc
-> Sem (Input TyDefCtx : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA (Sem (Reader PA : Input TyDefCtx : r) Doc
 -> Sem (Input TyDefCtx : r) Doc)
-> (Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
    -> Sem (Reader PA : Input TyDefCtx : r) Doc)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem (Input TyDefCtx : r) Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem (Reader PA : Input TyDefCtx : r) Doc
forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh (Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc -> Sem r Doc)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
                  Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> [Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall (f :: * -> *). Applicative f => f Doc -> [f Doc] -> f Doc
bulletList Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
"-" ([Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
 -> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc)
-> [Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall a b. (a -> b) -> a -> b
$ ((ATerm, TestResult)
 -> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc)
-> [(ATerm, TestResult)]
-> [Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((ATerm
 -> TestResult -> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc)
-> (ATerm, TestResult)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ATerm
-> TestResult -> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
ATerm -> TestResult -> Sem r Doc
prettyTestFailure) [(ATerm, TestResult)]
failures
          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
$ Int -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
hdr Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
prettyFailures
      Bool -> Sem r Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([(ATerm, TestResult)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures)

------------------------------------------------------------
-- :names

namesCmd :: REPLCommand 'CNames
namesCmd :: REPLCommand 'CNames
namesCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"names",
      helpcmd :: String
helpcmd = String
":names",
      shortHelp :: String
shortHelp = String
"Show all names in current scope",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CNames
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CNames
x -> Sem (Input TopInfo : r) () -> Sem r ()
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CNames -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CNames
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CNames -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CNames -> Sem r ()
handleNames (REPLExpr 'CNames -> Sem r ()) -> REPLExpr 'CNames -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CNames
x,
      parser :: Parser (REPLExpr 'CNames)
parser = REPLExpr 'CNames -> Parser (REPLExpr 'CNames)
forall (m :: * -> *) a. Monad m => a -> m a
return REPLExpr 'CNames
Names
    }

-- | Show names and types for each item in the top-level context.
handleNames ::
  Members '[Input TopInfo, LFresh, Output Message] r =>
  REPLExpr 'CNames ->
  Sem r ()
handleNames :: REPLExpr 'CNames -> Sem r ()
handleNames REPLExpr 'CNames
Names = do
  TyDefCtx
tyDef <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (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))
  TyCtx
ctx <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (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))
  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] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((String, TyDefBody) -> Sem r Doc)
-> [(String, TyDefBody)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, TyDefBody) -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (TyDefCtx -> [(String, TyDefBody)]
forall k a. Map k a -> [(k, a)]
M.assocs TyDefCtx
tyDef))
    Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
    [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((QName Term, PolyType) -> Sem r Doc)
-> [(QName Term, PolyType)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName Term, PolyType) -> Sem r Doc
forall t a (r :: EffectRow). Pretty t => (QName a, t) -> Sem r Doc
showFn (TyCtx -> [(QName Term, PolyType)]
forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs TyCtx
ctx))
  where
    showFn :: (QName a, t) -> Sem r Doc
showFn (QName NameProvenance
_ Name a
x, t
ty) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name a -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name a
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":", t -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' t
ty]

------------------------------------------------------------
-- nop

nopCmd :: REPLCommand 'CNop
nopCmd :: REPLCommand 'CNop
nopCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"nop",
      helpcmd :: String
helpcmd = String
"",
      shortHelp :: String
shortHelp = String
"No-op, e.g. if the user just enters a comment",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
BuiltIn,
      action :: REPLExpr 'CNop
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CNop
x -> REPLExpr 'CNop -> Sem r ()
forall (r :: EffectRow). REPLExpr 'CNop -> Sem r ()
handleNop REPLExpr 'CNop
x,
      parser :: Parser (REPLExpr 'CNop)
parser = REPLExpr 'CNop
Nop REPLExpr 'CNop -> Parser () -> Parser (REPLExpr 'CNop)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Parser ()
sc Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)
    }

handleNop :: REPLExpr 'CNop -> Sem r ()
handleNop :: REPLExpr 'CNop -> Sem r ()
handleNop REPLExpr 'CNop
Nop = () -> Sem r ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

------------------------------------------------------------
-- :parse

parseCmd :: REPLCommand 'CParse
parseCmd :: REPLCommand 'CParse
parseCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"parse",
      helpcmd :: String
helpcmd = String
":parse <expr>",
      shortHelp :: String
shortHelp = String
"Show the parsed AST",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CParse
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CParse
x -> REPLExpr 'CParse -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
REPLExpr 'CParse -> Sem r ()
handleParse REPLExpr 'CParse
x,
      parser :: Parser (REPLExpr 'CParse)
parser = Term -> REPLExpr 'CParse
Parse (Term -> REPLExpr 'CParse)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CParse)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handleParse :: Member (Output Message) r => REPLExpr 'CParse -> Sem r ()
handleParse :: REPLExpr 'CParse -> Sem r ()
handleParse (Parse Term
t) = Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Term -> String
forall a. Show a => a -> String
show Term
t))

------------------------------------------------------------
-- :pretty

prettyCmd :: REPLCommand 'CPretty
prettyCmd :: REPLCommand 'CPretty
prettyCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"pretty",
      helpcmd :: String
helpcmd = String
":pretty <expr>",
      shortHelp :: String
shortHelp = String
"Pretty-print a term",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CPretty
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CPretty
x -> REPLExpr 'CPretty -> Sem r ()
forall (r :: EffectRow).
Members '[LFresh, Output Message] r =>
REPLExpr 'CPretty -> Sem r ()
handlePretty REPLExpr 'CPretty
x,
      parser :: Parser (REPLExpr 'CPretty)
parser = Term -> REPLExpr 'CPretty
Pretty (Term -> REPLExpr 'CPretty)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CPretty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handlePretty :: Members '[LFresh, Output Message] r => REPLExpr 'CPretty -> Sem r ()
handlePretty :: REPLExpr 'CPretty -> Sem r ()
handlePretty (Pretty Term
t) = 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
$ Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Term
t

------------------------------------------------------------
-- :print

printCmd :: REPLCommand 'CPrint
printCmd :: REPLCommand 'CPrint
printCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"print",
      helpcmd :: String
helpcmd = String
":print <expr>",
      shortHelp :: String
shortHelp = String
"Print a string without the double quotes, interpreting special characters",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CPrint
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CPrint
x -> REPLExpr 'CPrint -> Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError : State TopInfo : Output Message : EvalEffects)
  r =>
REPLExpr 'CPrint -> Sem r ()
handlePrint REPLExpr 'CPrint
x,
      parser :: Parser (REPLExpr 'CPrint)
parser = Term -> REPLExpr 'CPrint
Print (Term -> REPLExpr 'CPrint)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CPrint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handlePrint :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()
handlePrint :: REPLExpr 'CPrint -> Sem r ()
handlePrint (Print Term
t) = do
  ATerm
at <- Sem (Input TopInfo : r) ATerm -> Sem r ATerm
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) ATerm -> Sem r ATerm)
-> (Sem
      (Reader TyCtx
         : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
      ATerm
    -> Sem (Input TopInfo : r) ATerm)
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     ATerm
-> Sem r ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  (Reader TyCtx
     : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
  ATerm
-> Sem (Input TopInfo : r) ATerm
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 : Input TopInfo : r)
   ATerm
 -> Sem r ATerm)
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     ATerm
-> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Term
-> PolyType
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     ATerm
forall (r :: EffectRow).
Members
  '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
    Fresh]
  r =>
Term -> PolyType -> Sem r ATerm
checkTop Term
t (Type -> PolyType
toPolyType Type
TyString)
  Value
v <- (EvalError -> DiscoError)
-> Sem (Error EvalError : r) Value -> Sem r Value
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) Value -> Sem r Value)
-> (ATerm -> Sem (Error EvalError : r) Value)
-> ATerm
-> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ATerm -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members
  (Error EvalError : State TopInfo : Output Message : EvalEffects)
  r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
False (ATerm -> Sem r Value) -> ATerm -> Sem r Value
forall a b. (a -> b) -> a -> b
$ ATerm
at
  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
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ((Value -> Char) -> Value -> String
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar Value
v)

------------------------------------------------------------
-- :reload

reloadCmd :: REPLCommand 'CReload
reloadCmd :: REPLCommand 'CReload
reloadCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"reload",
      helpcmd :: String
helpcmd = String
":reload",
      shortHelp :: String
shortHelp = String
"Reloads the most recently loaded file",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CReload
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CReload
x -> REPLExpr 'CReload -> Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output Message : Embed IO : EvalEffects)
  r =>
REPLExpr 'CReload -> Sem r ()
handleReload REPLExpr 'CReload
x,
      parser :: Parser (REPLExpr 'CReload)
parser = REPLExpr 'CReload -> Parser (REPLExpr 'CReload)
forall (m :: * -> *) a. Monad m => a -> m a
return REPLExpr 'CReload
Reload
    }

handleReload ::
  Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
  REPLExpr 'CReload ->
  Sem r ()
handleReload :: REPLExpr 'CReload -> Sem r ()
handleReload REPLExpr 'CReload
Reload = do
  Maybe String
file <- Getter TopInfo (Maybe String) -> Sem r (Maybe String)
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' TopInfo (Maybe String)
Getter TopInfo (Maybe String)
lastFile
  case Maybe String
file of
    Maybe String
Nothing -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info Sem r Doc
"No file to reload."
    Just String
f  -> Sem r Bool -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (String -> Sem r Bool
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output Message : Embed IO : EvalEffects)
  r =>
String -> Sem r Bool
handleLoad String
f)

------------------------------------------------------------
-- :defn

showDefnCmd :: REPLCommand 'CShowDefn
showDefnCmd :: REPLCommand 'CShowDefn
showDefnCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"defn",
      helpcmd :: String
helpcmd = String
":defn <var>",
      shortHelp :: String
shortHelp = String
"Show a variable's definition",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CShowDefn
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CShowDefn
x -> 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) () -> Sem r ())
-> (REPLExpr 'CShowDefn -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CShowDefn
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CShowDefn -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CShowDefn -> Sem r ()
handleShowDefn (REPLExpr 'CShowDefn -> Sem r ())
-> REPLExpr 'CShowDefn -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CShowDefn
x,
      parser :: Parser (REPLExpr 'CShowDefn)
parser = Name Term -> REPLExpr 'CShowDefn
ShowDefn (Name Term -> REPLExpr 'CShowDefn)
-> StateT ParserState (Parsec DiscoParseError String) (Name Term)
-> Parser (REPLExpr 'CShowDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
sc Parser ()
-> StateT ParserState (Parsec DiscoParseError String) (Name Term)
-> StateT ParserState (Parsec DiscoParseError String) (Name Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) (Name Term)
ident)
    }

handleShowDefn ::
  Members '[Input TopInfo, LFresh, Output Message] r =>
  REPLExpr 'CShowDefn ->
  Sem r ()
handleShowDefn :: REPLExpr 'CShowDefn -> Sem r ()
handleShowDefn (ShowDefn Name Term
x) = do
  let name2s :: String
name2s = Name Term -> String
forall a. Name a -> String
name2String Name Term
x
  Ctx ATerm Defn
defns   <- (TopInfo -> Ctx ATerm Defn) -> Sem r (Ctx ATerm Defn)
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting (Ctx ATerm Defn) TopInfo (Ctx ATerm Defn)
-> TopInfo -> Ctx ATerm Defn
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo)
-> TopInfo -> Const (Ctx ATerm Defn) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo)
 -> TopInfo -> Const (Ctx ATerm Defn) TopInfo)
-> ((Ctx ATerm Defn -> Const (Ctx ATerm Defn) (Ctx ATerm Defn))
    -> ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo)
-> Getting (Ctx ATerm Defn) TopInfo (Ctx ATerm Defn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ctx ATerm Defn -> Const (Ctx ATerm Defn) (Ctx ATerm Defn))
-> ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo
Lens' ModuleInfo (Ctx ATerm Defn)
miTermdefs))
  TyDefCtx
tyDefns <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (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))

  let xdefs :: [(QName ATerm, Defn)]
xdefs = Name ATerm -> Ctx ATerm Defn -> [(QName ATerm, Defn)]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' (Name Term -> Name ATerm
coerce Name Term
x) Ctx ATerm Defn
defns
      mtydef :: Maybe TyDefBody
mtydef = String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name2s TyDefCtx
tyDefns

  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
$ do
    let ds :: [Sem r Doc]
ds = ((QName ATerm, Defn) -> Sem r Doc)
-> [(QName ATerm, Defn)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Defn -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (Defn -> Sem r Doc)
-> ((QName ATerm, Defn) -> Defn)
-> (QName ATerm, Defn)
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName ATerm, Defn) -> Defn
forall a b. (a, b) -> b
snd) [(QName ATerm, Defn)]
xdefs [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [Sem r Doc]
-> (TyDefBody -> [Sem r Doc]) -> Maybe TyDefBody -> [Sem r Doc]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Sem r Doc -> [Sem r Doc]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sem r Doc -> [Sem r Doc])
-> (TyDefBody -> Sem r Doc) -> TyDefBody -> [Sem r Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, TyDefBody) -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' ((String, TyDefBody) -> Sem r Doc)
-> (TyDefBody -> (String, TyDefBody)) -> TyDefBody -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
name2s,)) Maybe TyDefBody
mtydef
    case [Sem r Doc]
ds of
      [] -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"No definition for" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Name Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name Term
x
      [Sem r Doc]
_  -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat [Sem r Doc]
ds

------------------------------------------------------------
-- :test

testPropCmd :: REPLCommand 'CTestProp
testPropCmd :: REPLCommand 'CTestProp
testPropCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"test",
      helpcmd :: String
helpcmd = String
":test <property>",
      shortHelp :: String
shortHelp = String
"Test a property using random examples",
      category :: REPLCommandCategory
category = REPLCommandCategory
User,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CTestProp
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CTestProp
x -> REPLExpr 'CTestProp -> Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError : State TopInfo : Output Message : EvalEffects)
  r =>
REPLExpr 'CTestProp -> Sem r ()
handleTest REPLExpr 'CTestProp
x,
      parser :: Parser (REPLExpr 'CTestProp)
parser = Term -> REPLExpr 'CTestProp
TestProp (Term -> REPLExpr 'CTestProp)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CTestProp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
    }

handleTest ::
  Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r =>
  REPLExpr 'CTestProp ->
  Sem r ()
handleTest :: REPLExpr 'CTestProp -> Sem r ()
handleTest (TestProp Term
t) = do
  ATerm
at <- Sem (Input TopInfo : r) ATerm -> Sem r ATerm
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) ATerm -> Sem r ATerm)
-> (Sem
      (Reader TyCtx
         : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
      ATerm
    -> Sem (Input TopInfo : r) ATerm)
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     ATerm
-> Sem r ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  (Reader TyCtx
     : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
  ATerm
-> Sem (Input TopInfo : r) ATerm
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 : Input TopInfo : r)
   ATerm
 -> Sem r ATerm)
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     ATerm
-> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     ATerm
forall (r :: EffectRow).
Members
  '[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
    Output Message]
  r =>
Term -> Sem r ATerm
checkProperty Term
t
  TyDefCtx
tydefs <- Getter TopInfo TyDefCtx -> Sem r TyDefCtx
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo ((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
. (ModuleInfo -> TyDefCtx)
-> (TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleInfo -> TyDefCtx
allTydefs)
  Sem (Input TopInfo : r) () -> Sem r ()
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) () -> Sem r ())
-> (Sem (Input Env : Input TopInfo : r) ()
    -> Sem (Input TopInfo : r) ())
-> Sem (Input Env : Input TopInfo : r) ()
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Input Env : Input TopInfo : r) ()
-> Sem (Input TopInfo : r) ()
forall (r :: EffectRow) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv (Sem (Input Env : Input TopInfo : r) () -> Sem r ())
-> Sem (Input Env : Input TopInfo : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ do
    TestResult
r <- Int -> ATerm -> Sem (Input Env : Input TopInfo : r) TestResult
forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Int -> ATerm -> Sem r TestResult
runTest Int
100 ATerm
at -- XXX make configurable
    Sem (Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem (Input Env : Input TopInfo : r) Doc
 -> Sem (Input Env : Input TopInfo : r) ())
-> Sem (Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) ()
forall a b. (a -> b) -> a -> b
$ TyDefCtx
-> Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs (Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc
 -> Sem (Input Env : Input TopInfo : r) Doc)
-> (Sem
      (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
    -> Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc)
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PA
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA (Sem
   (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
 -> Sem (Input Env : Input TopInfo : r) Doc)
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc
forall a b. (a -> b) -> a -> b
$ Int
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (Sem
   (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
 -> Sem
      (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc)
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall a b. (a -> b) -> a -> b
$ Sem
  (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
"-" Sem
  (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> ATerm
-> TestResult
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
ATerm -> TestResult -> Sem r Doc
prettyTestResult ATerm
at TestResult
r

------------------------------------------------------------
-- :type

typeCheckCmd :: REPLCommand 'CTypeCheck
typeCheckCmd :: REPLCommand 'CTypeCheck
typeCheckCmd =
  REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
    -> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
    { name :: String
name = String
"type",
      helpcmd :: String
helpcmd = String
":type <term>",
      shortHelp :: String
shortHelp = String
"Typecheck a term",
      category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
      cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
      action :: REPLExpr 'CTypeCheck
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CTypeCheck
x -> 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) () -> Sem r ())
-> (REPLExpr 'CTypeCheck -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CTypeCheck
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CTypeCheck -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck (REPLExpr 'CTypeCheck -> Sem r ())
-> REPLExpr 'CTypeCheck -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CTypeCheck
x,
      parser :: Parser (REPLExpr 'CTypeCheck)
parser = Parser (REPLExpr 'CTypeCheck)
parseTypeCheck
    }

handleTypeCheck ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
  REPLExpr 'CTypeCheck ->
  Sem r ()
handleTypeCheck :: REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck (TypeCheck Term
t) = do
  (ATerm
_, PolyType
sig) <- Sem
  (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
  (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
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)
   (ATerm, PolyType)
 -> Sem r (ATerm, PolyType))
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (ATerm, PolyType)
forall (r :: EffectRow).
Members
  '[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
    Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
  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
$ Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Term
t Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> PolyType -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' PolyType
sig

parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)
parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)
parseTypeCheck =
  Term -> REPLExpr 'CTypeCheck
TypeCheck
    (Term -> REPLExpr 'CTypeCheck)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CTypeCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Term
term StateT ParserState (Parsec DiscoParseError String) Term
-> String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"expression")
            StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (StateT ParserState (Parsec DiscoParseError String) Term
parseNakedOp StateT ParserState (Parsec DiscoParseError String) Term
-> String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator")
        )

-- In a :type or :doc command, allow naked operators, as in :type + ,
-- even though + by itself is not a syntactically valid term.
-- However, this seems like it may be a common thing for a student to
-- ask and there is no reason we can't have this as a special case.
parseNakedOp :: Parser Term
parseNakedOp :: StateT ParserState (Parsec DiscoParseError String) Term
parseNakedOp = Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Prim
parseNakedOpPrim

parseNakedOpPrim :: Parser Prim
parseNakedOpPrim :: StateT ParserState (Parsec DiscoParseError String) Prim
parseNakedOpPrim = Parser ()
sc Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((OpInfo -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [OpInfo]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> StateT ParserState (Parsec DiscoParseError String) Prim
mkOpParser ([[OpInfo]] -> [OpInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[OpInfo]]
opTable))
  where
    mkOpParser :: OpInfo -> Parser Prim
    mkOpParser :: OpInfo -> StateT ParserState (Parsec DiscoParseError String) Prim
mkOpParser (OpInfo (UOpF UFixity
_ UOp
op) [String]
syns Int
_) = [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map ((UOp -> Prim
PrimUOp UOp
op Prim
-> Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Parser ()
 -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> (String -> Parser ())
-> String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Parser ()
reservedOp) [String]
syns)
    mkOpParser (OpInfo (BOpF BFixity
_ BOp
op) [String]
syns Int
_) = [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map ((BOp -> Prim
PrimBOp BOp
op Prim
-> Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Parser ()
 -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> (String -> Parser ())
-> String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Parser ()
reservedOp) [String]
syns)