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

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 (mapMaybe, 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 PP
import Disco.Property (prettyTestResult)
import Disco.Syntax.Operators
import Disco.Syntax.Prims (
  Prim (PrimBOp, PrimUOp),
  toPrim,
 )
import Disco.Typecheck
import Disco.Typecheck.Erase
import Disco.Types (toPolyType, pattern TyString)
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
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 -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [REPLCommandCategory] -> ShowS
$cshowList :: [REPLCommandCategory] -> ShowS
show :: REPLCommandCategory -> FilePath
$cshow :: REPLCommandCategory -> FilePath
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
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 -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [REPLCommandType] -> ShowS
$cshowList :: [REPLCommandType] -> ShowS
show :: REPLCommandType -> FilePath
$cshow :: REPLCommandType -> FilePath
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 -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [CmdTag] -> ShowS
$cshowList :: [CmdTag] -> ShowS
show :: CmdTag -> FilePath
$cshow :: CmdTag -> FilePath
showsPrec :: Int -> CmdTag -> ShowS
$cshowsPrec :: Int -> CmdTag -> ShowS
Show, CmdTag -> CmdTag -> Bool
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
  { forall (c :: CmdTag). REPLCommand c -> FilePath
name :: String
  -- ^ Name of the command
  , forall (c :: CmdTag). REPLCommand c -> FilePath
helpcmd :: String
  -- ^ Help text showing how to use the command, e.g. ":ann <term>"
  , forall (c :: CmdTag). REPLCommand c -> FilePath
shortHelp :: String
  -- ^ Short free-form text explaining the command.
  --   We could also consider adding long help text as well.
  , forall (c :: CmdTag). REPLCommand c -> REPLCommandCategory
category :: REPLCommandCategory
  -- ^ Is the command for users or devs?
  , forall (c :: CmdTag). REPLCommand c -> REPLCommandType
cmdtype :: REPLCommandType
  -- ^ Is it a built-in command or colon command?
  , forall (c :: CmdTag).
REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action :: REPLExpr c -> (forall r. Members DiscoEffects r => Sem r ())
  -- ^ The action to execute,
  -- given the input to the
  -- command.
  , forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser :: Parser (REPLExpr c)
  -- ^ Parser for the command argument(s).
  }

-- | 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 = forall a. (a -> Bool) -> [a] -> [a]
P.filter (\(SomeCmd REPLCommand c
rc) -> forall (c :: CmdTag). REPLCommand c -> REPLCommandType
cmdtype REPLCommand c
rc 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 :: forall (r :: EffectRow).
Members DiscoEffects r =>
REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch [] SomeREPLExpr
_ = forall (m :: * -> *) a. Monad m => a -> m a
return ()
dispatch (SomeCmd REPLCommand c
c : REPLCommands
cs) r :: SomeREPLExpr
r@(SomeREPL REPLExpr c
e) = case 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' -> forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem (Error DiscoError : r) () -> Sem r ()
outputDiscoErrors forall a b. (a -> b) -> a -> b
$ 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 -> 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 =
  [ forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CAnn
annCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CCompile
compileCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CDesugar
desugarCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CDoc
docCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CEval
evalCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CHelp
helpCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CLoad
loadCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CNames
namesCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CNop
nopCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CParse
parseCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CPretty
prettyCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CPrint
printCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CReload
reloadCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CShowDefn
showDefnCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTypeCheck
typeCheckCmd
  , forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTestProp
testPropCmd
  ]

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

builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
builtinCommandParser =
  forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(SomeCmd REPLCommand c
rc) -> forall (c :: CmdTag). Typeable c => REPLExpr c -> SomeREPLExpr
SomeREPL forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc))) forall (f :: * -> *) a. Alternative f => f a
empty
    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 =
  (FilePath
-> StateT ParserState (Parsec DiscoParseError FilePath) FilePath
symbol FilePath
":" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.lowerChar) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= REPLCommands -> FilePath -> 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 -> FilePath -> Parser SomeREPLExpr
parseCommandArgs REPLCommands
allCommands FilePath
cmd = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Parser SomeREPLExpr
badCmd forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((FilePath
cmd forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(FilePath, Parser SomeREPLExpr)]
parsers
 where
  badCmd :: Parser SomeREPLExpr
badCmd = forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail forall a b. (a -> b) -> a -> b
$ FilePath
"Command \":" forall a. [a] -> [a] -> [a]
++ FilePath
cmd forall a. [a] -> [a] -> [a]
++ FilePath
"\" is unrecognized."

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

-- | Parse a file name.
fileParser :: Parser FilePath
fileParser :: StateT ParserState (Parsec DiscoParseError FilePath) FilePath
fileParser = forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.spaceChar forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (Bool -> Bool
not 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
    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 -> FilePath -> Either FilePath SomeREPLExpr
parseLine REPLCommands
allCommands ExtSet
exts FilePath
s =
  case forall a.
Parser a
-> FilePath
-> FilePath
-> Either (ParseErrorBundle FilePath DiscoParseError) a
runParser (forall a. ExtSet -> Parser a -> Parser a
withExts ExtSet
exts (REPLCommands -> Parser SomeREPLExpr
lineParser REPLCommands
allCommands)) FilePath
"" FilePath
s of
    Left ParseErrorBundle FilePath DiscoParseError
e -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> FilePath
errorBundlePretty ParseErrorBundle FilePath DiscoParseError
e
    Right SomeREPLExpr
l -> forall a b. b -> Either a b
Right SomeREPLExpr
l

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

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

annCmd :: REPLCommand 'CAnn
annCmd :: REPLCommand 'CAnn
annCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"ann"
    , helpcmd :: FilePath
helpcmd = FilePath
":ann"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, Output (Message ())] r =>
REPLExpr 'CAnn -> Sem r ()
handleAnn
    , parser :: Parser (REPLExpr 'CAnn)
parser = Term -> REPLExpr 'CAnn
Ann forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

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

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

compileCmd :: REPLCommand 'CCompile
compileCmd :: REPLCommand 'CCompile
compileCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"compile"
    , helpcmd :: FilePath
helpcmd = FilePath
":compile"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, Output (Message ())] r =>
REPLExpr 'CCompile -> Sem r ()
handleCompile
    , parser :: Parser (REPLExpr 'CCompile)
parser = Term -> REPLExpr 'CCompile
Compile forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

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

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

desugarCmd :: REPLCommand 'CDesugar
desugarCmd :: REPLCommand 'CDesugar
desugarCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"desugar"
    , helpcmd :: FilePath
helpcmd = FilePath
":desugar"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
REPLExpr 'CDesugar -> Sem r ()
handleDesugar
    , parser :: Parser (REPLExpr 'CDesugar)
parser = Term -> REPLExpr 'CDesugar
Desugar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

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

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

docCmd :: REPLCommand 'CDoc
docCmd :: REPLCommand 'CDoc
docCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"doc"
    , helpcmd :: FilePath
helpcmd = FilePath
":doc <term>"
    , shortHelp :: FilePath
shortHelp = FilePath
"Show documentation"
    , category :: REPLCommandCategory
category = REPLCommandCategory
User
    , cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd
    , action :: REPLExpr 'CDoc
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
REPLExpr 'CDoc -> Sem r ()
handleDoc
    , parser :: Parser (REPLExpr 'CDoc)
parser = DocInput -> REPLExpr 'CDoc
Doc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser DocInput
parseDoc
    }

-- An input to the :doc command can be either a term, a primitive
-- operator, or something else.
data DocInput = DocTerm Term | DocPrim Prim | DocOther String
  deriving (Int -> DocInput -> ShowS
[DocInput] -> ShowS
DocInput -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [DocInput] -> ShowS
$cshowList :: [DocInput] -> ShowS
show :: DocInput -> FilePath
$cshow :: DocInput -> FilePath
showsPrec :: Int -> DocInput -> ShowS
$cshowsPrec :: Int -> DocInput -> ShowS
Show)

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

handleDoc ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
  REPLExpr 'CDoc ->
  Sem r ()
handleDoc :: forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
REPLExpr 'CDoc -> Sem r ()
handleDoc (Doc (DocTerm (TBool Bool
_))) = forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocBool
handleDoc (Doc (DocTerm Term
TUnit)) = forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocUnit
handleDoc (Doc (DocTerm Term
TWild)) = forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocWild
handleDoc (Doc (DocTerm (TPrim Prim
p))) = 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))) = forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
Name Term -> Sem r ()
handleDocVar Name Term
x
handleDoc (Doc (DocTerm Term
_)) =
  forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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)) = forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
Prim -> Sem r ()
handleDocPrim Prim
p
handleDoc (Doc (DocOther FilePath
s)) = forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
FilePath -> Sem r ()
handleDocOther FilePath
s

handleDocBool :: Members '[Output (Message ())] r => Sem r ()
handleDocBool :: forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocBool =
  forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info 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."
      forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (r :: EffectRow) ann. FilePath -> Sem r (Doc ann)
mkReference FilePath
"bool"

handleDocUnit :: Members '[Output (Message ())] r => Sem r ()
handleDocUnit :: forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocUnit =
  forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$
    Sem r (Doc ())
"The unit value, i.e. the single value of type Unit."
      forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (r :: EffectRow) ann. FilePath -> Sem r (Doc ann)
mkReference FilePath
"unit"

handleDocWild :: Members '[Output (Message ())] r => Sem r ()
handleDocWild :: forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocWild =
  forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$
    Sem r (Doc ())
"A wildcard pattern."
      forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (r :: EffectRow) ann. FilePath -> Sem r (Doc ann)
mkReference FilePath
"wild-pattern"

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

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

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

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

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

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

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

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

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

evalCmd :: REPLCommand 'CEval
evalCmd :: REPLCommand 'CEval
evalCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"eval"
    , helpcmd :: FilePath
helpcmd = FilePath
"<code>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CEval -> Sem r ()
handleEval
    , parser :: Parser (REPLExpr 'CEval)
parser = Module -> REPLExpr 'CEval
Eval forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoadingMode -> Parser Module
wholeModule LoadingMode
REPL
    }

handleEval ::
  Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
  REPLExpr 'CEval ->
  Sem r ()
handleEval :: forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CEval -> Sem r ()
handleEval (Eval Module
m) = do
  ModuleInfo
mi <- forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall a b. (a -> b) -> a -> b
$ forall ann (r :: EffectRow).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule Bool
False Resolver
FromCwdOrStdlib ModuleName
REPLModule Module
m
  forall ann (r :: EffectRow).
Members
  '[Error DiscoError, State TopInfo, Random, State Mem,
    Output (Message ann)]
  r =>
ModuleInfo -> Sem r ()
addToREPLModule ModuleInfo
mi
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ModuleInfo
mi forall s a. s -> Getting a s a -> a
^. Lens' ModuleInfo [(ATerm, PolyType)]
miTerms) (forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError EvalError -> DiscoError
EvalErr forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members
  (Error EvalError
     : State TopInfo : Output (Message ()) : EvalEffects)
  r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
True forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: forall (r :: EffectRow).
Members
  (Error EvalError
     : State TopInfo : Output (Message ()) : EvalEffects)
  r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
pr ATerm
at = do
  Env
env <- forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo Lens' TopInfo Env
topEnv
  Value
v <- forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst Env
env forall a b. (a -> b) -> a -> b
$ forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Core -> Sem r Value
eval (ATerm -> Core
compileTerm ATerm
at)

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

  forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo forall a b. (a -> b) -> a -> b
$
    (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyCtx
miTys forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
REPLModule) (forall a. FilePath -> Name a
string2Name FilePath
"it")) (Type -> PolyType
toPolyType Type
ty))
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lens' TopInfo Env
topEnv forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
REPLModule) (forall a. FilePath -> Name a
string2Name FilePath
"it")) Value
v)
  forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
 where
  ty :: Type
ty = forall t. HasType t => t -> Type
getType ATerm
at

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

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

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

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

loadCmd :: REPLCommand 'CLoad
loadCmd :: REPLCommand 'CLoad
loadCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"load"
    , helpcmd :: FilePath
helpcmd = FilePath
":load <filename>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CLoad -> Sem r ()
handleLoadWrapper
    , parser :: Parser (REPLExpr 'CLoad)
parser = FilePath -> REPLExpr 'CLoad
Load forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) FilePath
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 :: forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CLoad -> Sem r ()
handleLoadWrapper (Load FilePath
fp) = forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
FilePath -> Sem r Bool
handleLoad FilePath
fp)

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

  -- Reset top-level module map and context to empty, so we start
  -- fresh and pick up any changes to imported modules etc.
  forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo forall a b. (a -> b) -> a -> b
$ Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall k a. Map k a
M.empty
  forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo forall a b. (a -> b) -> a -> b
$ Lens' TopInfo Env
topEnv forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall a b. Ctx a b
Ctx.emptyCtx

  -- Load the module.
  ModuleInfo
m <- forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall a b. (a -> b) -> a -> b
$ forall ann (r :: EffectRow).
Members
  '[State TopInfo, Output (Message ann), Random, State Mem,
    Error DiscoError, Embed IO]
  r =>
Bool -> Resolver -> FilePath -> Sem r ModuleInfo
loadDiscoModule Bool
False (FilePath -> Resolver
FromDir FilePath
directory) FilePath
modName
  forall ann (r :: EffectRow).
Members
  '[State TopInfo, Random, Error EvalError, State Mem,
    Output (Message ann)]
  r =>
ModuleInfo -> Sem r ()
setREPLModule ModuleInfo
m

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

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

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

-- XXX Return a structured summary of the results, not a Bool; & move
-- this somewhere else?
runAllTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => [QName Term] -> Ctx ATerm [AProperty] -> Sem r Bool -- (Ctx ATerm [TestResult])
runAllTests :: forall (r :: EffectRow).
Members (Output (Message ()) : Input TopInfo : EvalEffects) r =>
[QName Term] -> Ctx ATerm [ATerm] -> Sem r Bool
runAllTests [QName Term]
declNames Ctx ATerm [ATerm]
aprops
  | forall a b. Ctx a b -> Bool
Ctx.null Ctx ATerm [ATerm]
aprops = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  | Bool
otherwise = do
      forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info Sem r (Doc ())
"Running tests..."
      -- Use the order the names were defined in the module
      forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (r :: EffectRow).
Members (Output (Message ()) : Input TopInfo : EvalEffects) r =>
QName Term -> [ATerm] -> Sem r Bool
runTests) (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\QName Term
n -> (QName Term
n,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' (coerce :: forall a b. Coercible a b => a -> b
coerce QName Term
n) Ctx ATerm [ATerm]
aprops) [QName Term]
declNames)
 where
  numSamples :: Int
  numSamples :: Int
numSamples = Int
50 -- XXX make this configurable somehow
  runTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool
  runTests :: forall (r :: EffectRow).
Members (Output (Message ()) : Input TopInfo : EvalEffects) r =>
QName Term -> [ATerm] -> Sem r Bool
runTests (QName NameProvenance
_ Name Term
n) [ATerm]
props = do
    [(ATerm, TestResult)]
results <- forall (r :: EffectRow) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> a
id forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& 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 = forall a. (a -> Bool) -> [a] -> [a]
P.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestResult -> Bool
testIsOk forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(ATerm, TestResult)]
results
        hdr :: Sem r (Doc ())
hdr = forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
n forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ())
":"

    case forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures of
      Bool
True -> forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ Sem r (Doc ())
hdr forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Sem r (Doc ())
"OK"
      Bool
False -> do
        TyDefCtx
tydefs <- forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 =
              forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA
                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh
                forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
bulletList Sem (LFresh : Reader PA : Input TyDefCtx : r) (Doc ())
"-"
                forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
ATerm -> TestResult -> Sem r (Doc ann)
prettyTestResult) [(ATerm, TestResult)]
failures
        forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent Int
2 forall a b. (a -> b) -> a -> b
$ Sem r (Doc ())
hdr forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Sem r (Doc ())
prettyFailures
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures)

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

namesCmd :: REPLCommand 'CNames
namesCmd :: REPLCommand 'CNames
namesCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"names"
    , helpcmd :: FilePath
helpcmd = FilePath
":names"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output (Message ())] r =>
REPLExpr 'CNames -> Sem r ()
handleNames
    , parser :: Parser (REPLExpr 'CNames)
parser = 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 :: forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output (Message ())] r =>
REPLExpr 'CNames -> Sem r ()
handleNames REPLExpr 'CNames
Names = do
  TyDefCtx
tyDef <- forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyDefCtx
miTydefs))
  TyCtx
ctx <- forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Lens' TopInfo ModuleInfo
replModInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' ModuleInfo TyCtx
miTys))
  forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$
    forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' (forall k a. Map k a -> [(k, a)]
M.assocs TyDefCtx
tyDef))
      forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall {t} {a} {r :: EffectRow} {ann}.
Pretty t =>
(QName a, t) -> Sem r (Doc ann)
showFn (forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs TyCtx
ctx))
 where
  showFn :: (QName a, t) -> Sem r (Doc ann)
showFn (QName NameProvenance
_ Name a
x, t
ty) = forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name a
x, forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
":", forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' t
ty]

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

nopCmd :: REPLCommand 'CNop
nopCmd :: REPLCommand 'CNop
nopCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"nop"
    , helpcmd :: FilePath
helpcmd = FilePath
""
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow). REPLExpr 'CNop -> Sem r ()
handleNop
    , parser :: Parser (REPLExpr 'CNop)
parser = REPLExpr 'CNop
Nop forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Parser ()
sc forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)
    }

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

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

parseCmd :: REPLCommand 'CParse
parseCmd :: REPLCommand 'CParse
parseCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"parse"
    , helpcmd :: FilePath
helpcmd = FilePath
":parse <expr>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Member (Output (Message ())) r =>
REPLExpr 'CParse -> Sem r ()
handleParse
    , parser :: Parser (REPLExpr 'CParse)
parser = Term -> REPLExpr 'CParse
Parse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

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

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

prettyCmd :: REPLCommand 'CPretty
prettyCmd :: REPLCommand 'CPretty
prettyCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"pretty"
    , helpcmd :: FilePath
helpcmd = FilePath
":pretty <expr>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Members '[LFresh, Output (Message ())] r =>
REPLExpr 'CPretty -> Sem r ()
handlePretty
    , parser :: Parser (REPLExpr 'CPretty)
parser = Term -> REPLExpr 'CPretty
Pretty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

handlePretty :: Members '[LFresh, Output (Message ())] r => REPLExpr 'CPretty -> Sem r ()
handlePretty :: forall (r :: EffectRow).
Members '[LFresh, Output (Message ())] r =>
REPLExpr 'CPretty -> Sem r ()
handlePretty (Pretty Term
t) = forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info forall a b. (a -> b) -> a -> b
$ forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Term
t

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

printCmd :: REPLCommand 'CPrint
printCmd :: REPLCommand 'CPrint
printCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"print"
    , helpcmd :: FilePath
helpcmd = FilePath
":print <expr>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : EvalEffects)
  r =>
REPLExpr 'CPrint -> Sem r ()
handlePrint
    , parser :: Parser (REPLExpr 'CPrint)
parser = Term -> REPLExpr 'CPrint
Print forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

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

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

reloadCmd :: REPLCommand 'CReload
reloadCmd :: REPLCommand 'CReload
reloadCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"reload"
    , helpcmd :: FilePath
helpcmd = FilePath
":reload"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CReload -> Sem r ()
handleReload
    , parser :: Parser (REPLExpr 'CReload)
parser = 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 :: forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CReload -> Sem r ()
handleReload REPLExpr 'CReload
Reload = do
  Maybe FilePath
file <- forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' TopInfo (Maybe FilePath)
lastFile
  case Maybe FilePath
file of
    Maybe FilePath
Nothing -> forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info Sem r (Doc ())
"No file to reload."
    Just FilePath
f -> forall (f :: * -> *) a. Functor f => f a -> f ()
void (forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
FilePath -> Sem r Bool
handleLoad FilePath
f)

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

showDefnCmd :: REPLCommand 'CShowDefn
showDefnCmd :: REPLCommand 'CShowDefn
showDefnCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"defn"
    , helpcmd :: FilePath
helpcmd = FilePath
":defn <var>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output (Message ())] r =>
REPLExpr 'CShowDefn -> Sem r ()
handleShowDefn
    , parser :: Parser (REPLExpr 'CShowDefn)
parser = Name Term -> REPLExpr 'CShowDefn
ShowDefn forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
sc forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError FilePath) (Name Term)
ident)
    }

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

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

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

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

testPropCmd :: REPLCommand 'CTestProp
testPropCmd :: REPLCommand 'CTestProp
testPropCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"test"
    , helpcmd :: FilePath
helpcmd = FilePath
":test <property>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : EvalEffects)
  r =>
REPLExpr 'CTestProp -> Sem r ()
handleTest
    , parser :: Parser (REPLExpr 'CTestProp)
parser = Term -> REPLExpr 'CTestProp
TestProp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    }

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

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

typeCheckCmd :: REPLCommand 'CTypeCheck
typeCheckCmd :: REPLCommand 'CTypeCheck
typeCheckCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"type"
    , helpcmd :: FilePath
helpcmd = FilePath
":type <term>"
    , shortHelp :: FilePath
shortHelp = FilePath
"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 = forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck
    , parser :: Parser (REPLExpr 'CTypeCheck)
parser = Parser (REPLExpr 'CTypeCheck)
parseTypeCheck
    }

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

parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)
parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)
parseTypeCheck =
  Term -> REPLExpr 'CTypeCheck
TypeCheck
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Term
term forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> FilePath -> m a
<?> FilePath
"expression")
            forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Parser Term
parseNakedOp forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> FilePath -> m a
<?> FilePath
"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 :: Parser Term
parseNakedOp = Prim -> Term
TPrim forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) Prim
parseNakedOpPrim

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