{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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 (forM_, void, when)
import Control.Monad.Except ()
import Data.Bifunctor (second)
import Data.Char (isSpace)
import Data.Coerce
import Data.List (find, isPrefixOf, sortBy, transpose)
import Data.List.NonEmpty qualified as NE
import Data.Map ((!))
import Data.Map qualified as M
import Data.Maybe (mapMaybe, maybeToList)
import Data.Typeable
import Disco.AST.Surface
import Disco.AST.Typed
import Disco.Compile
import Disco.Context as Ctx
import Disco.Desugar
import Disco.Doc
import Disco.Effects.Fresh (runFresh)
import Disco.Effects.Input
import Disco.Effects.LFresh
import Disco.Effects.State
import Disco.Enumerate (enumerateType)
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 Disco.Pretty qualified as PP
import Disco.Property (prettyTestResult)
import Disco.Syntax.Operators
import Disco.Syntax.Prims (
  Prim (PrimAbs, PrimBOp, PrimCeil, PrimFloor, PrimUOp),
  toPrim,
 )
import Disco.Typecheck
import Disco.Typecheck.Erase
import Disco.Types
import Disco.Util (maximum0)
import Disco.Value
import Polysemy
import Polysemy.Error hiding (try)
import Polysemy.Output
import Polysemy.Reader
import System.FilePath (splitFileName)
import Text.Megaparsec hiding (State, runParser)
import Text.Megaparsec.Char qualified as C
import Text.Megaparsec.Char.Lexer qualified as L
import Text.PrettyPrint.Boxes qualified as B
import Unbound.Generics.LocallyNameless (
  Name,
  name2String,
  string2Name,
 )
import Prelude as P

------------------------------------------------------------
-- 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
  Table :: Term -> REPLExpr 'CTable -- Print a table
  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
$c== :: REPLCommandCategory -> REPLCommandCategory -> Bool
== :: REPLCommandCategory -> REPLCommandCategory -> Bool
$c/= :: REPLCommandCategory -> REPLCommandCategory -> Bool
/= :: REPLCommandCategory -> REPLCommandCategory -> Bool
Eq, Int -> REPLCommandCategory -> ShowS
[REPLCommandCategory] -> ShowS
REPLCommandCategory -> FilePath
(Int -> REPLCommandCategory -> ShowS)
-> (REPLCommandCategory -> FilePath)
-> ([REPLCommandCategory] -> ShowS)
-> Show REPLCommandCategory
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> REPLCommandCategory -> ShowS
showsPrec :: Int -> REPLCommandCategory -> ShowS
$cshow :: REPLCommandCategory -> FilePath
show :: REPLCommandCategory -> FilePath
$cshowList :: [REPLCommandCategory] -> ShowS
showList :: [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
$c== :: REPLCommandType -> REPLCommandType -> Bool
== :: REPLCommandType -> REPLCommandType -> Bool
$c/= :: REPLCommandType -> REPLCommandType -> Bool
/= :: REPLCommandType -> REPLCommandType -> Bool
Eq, Int -> REPLCommandType -> ShowS
[REPLCommandType] -> ShowS
REPLCommandType -> FilePath
(Int -> REPLCommandType -> ShowS)
-> (REPLCommandType -> FilePath)
-> ([REPLCommandType] -> ShowS)
-> Show REPLCommandType
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> REPLCommandType -> ShowS
showsPrec :: Int -> REPLCommandType -> ShowS
$cshow :: REPLCommandType -> FilePath
show :: REPLCommandType -> FilePath
$cshowList :: [REPLCommandType] -> ShowS
showList :: [REPLCommandType] -> ShowS
Show)

-- | Tags used at the type level to denote each REPL command.
data CmdTag
  = CTypeCheck
  | CEval
  | CShowDefn
  | CParse
  | CPretty
  | CPrint
  | CTable
  | CAnn
  | CDesugar
  | CCompile
  | CLoad
  | CReload
  | CDoc
  | CNop
  | CHelp
  | CNames
  | CTestProp
  deriving (Int -> CmdTag -> ShowS
[CmdTag] -> ShowS
CmdTag -> FilePath
(Int -> CmdTag -> ShowS)
-> (CmdTag -> FilePath) -> ([CmdTag] -> ShowS) -> Show CmdTag
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CmdTag -> ShowS
showsPrec :: Int -> CmdTag -> ShowS
$cshow :: CmdTag -> FilePath
show :: CmdTag -> FilePath
$cshowList :: [CmdTag] -> ShowS
showList :: [CmdTag] -> ShowS
Show, CmdTag -> CmdTag -> Bool
(CmdTag -> CmdTag -> Bool)
-> (CmdTag -> CmdTag -> Bool) -> Eq CmdTag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CmdTag -> CmdTag -> Bool
== :: CmdTag -> CmdTag -> Bool
$c/= :: CmdTag -> CmdTag -> Bool
/= :: 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 = (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 :: forall (r :: EffectRow).
Members DiscoEffects r =>
REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch [] SomeREPLExpr
_ = () -> Sem r ()
forall a. a -> Sem r a
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 ann (r :: EffectRow).
Member (Output (Message ann)) 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 'CTable -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTable
tableCmd
  , 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 a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
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 FilePath) (REPLExpr c)
-> Parser SomeREPLExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) (REPLExpr c)
-> StateT
     ParserState (Parsec DiscoParseError FilePath) (REPLExpr c)
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (REPLCommand c
-> StateT
     ParserState (Parsec DiscoParseError FilePath) (REPLExpr c)
forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc))) Parser SomeREPLExpr
forall a. StateT ParserState (Parsec DiscoParseError FilePath) a
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 =
  (FilePath -> Parser FilePath
symbol FilePath
":" Parser FilePath -> Parser FilePath -> Parser FilePath
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError FilePath) Char
-> Parser FilePath
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError FilePath) Char
StateT
  ParserState (Parsec DiscoParseError FilePath) (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.lowerChar) Parser FilePath
-> (FilePath -> Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> (a -> StateT ParserState (Parsec DiscoParseError FilePath) b)
-> StateT ParserState (Parsec DiscoParseError FilePath) b
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 = Parser SomeREPLExpr
-> ((FilePath, Parser SomeREPLExpr) -> Parser SomeREPLExpr)
-> Maybe (FilePath, Parser SomeREPLExpr)
-> Parser SomeREPLExpr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Parser SomeREPLExpr
badCmd (FilePath, Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b. (a, b) -> b
snd (Maybe (FilePath, Parser SomeREPLExpr) -> Parser SomeREPLExpr)
-> Maybe (FilePath, Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ ((FilePath, Parser SomeREPLExpr) -> Bool)
-> [(FilePath, Parser SomeREPLExpr)]
-> Maybe (FilePath, Parser SomeREPLExpr)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((FilePath
cmd FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`) (FilePath -> Bool)
-> ((FilePath, Parser SomeREPLExpr) -> FilePath)
-> (FilePath, Parser SomeREPLExpr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath, Parser SomeREPLExpr) -> FilePath
forall a b. (a, b) -> a
fst) [(FilePath, Parser SomeREPLExpr)]
parsers
 where
  badCmd :: Parser SomeREPLExpr
badCmd = FilePath -> Parser SomeREPLExpr
forall a.
FilePath -> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
fail (FilePath -> Parser SomeREPLExpr)
-> FilePath -> Parser SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ FilePath
"Command \":" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
cmd FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"\" is unrecognized."

  parsers :: [(FilePath, Parser SomeREPLExpr)]
parsers =
    (SomeREPLCommand -> (FilePath, Parser SomeREPLExpr))
-> REPLCommands -> [(FilePath, Parser SomeREPLExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
rc) -> (REPLCommand c -> FilePath
forall (c :: CmdTag). REPLCommand c -> FilePath
name REPLCommand c
rc, REPLExpr c -> SomeREPLExpr
forall (c :: CmdTag). Typeable c => REPLExpr c -> SomeREPLExpr
SomeREPL (REPLExpr c -> SomeREPLExpr)
-> StateT
     ParserState (Parsec DiscoParseError FilePath) (REPLExpr c)
-> Parser SomeREPLExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPLCommand c
-> StateT
     ParserState (Parsec DiscoParseError FilePath) (REPLExpr c)
forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc)) (REPLCommands -> [(FilePath, Parser SomeREPLExpr)])
-> REPLCommands -> [(FilePath, 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 FilePath
fileParser = StateT ParserState (Parsec DiscoParseError FilePath) Char
-> Parser FilePath
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError FilePath) Char
StateT
  ParserState (Parsec DiscoParseError FilePath) (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.spaceChar Parser FilePath -> Parser FilePath -> Parser FilePath
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError FilePath) Char
-> Parser FilePath
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some (StateT ParserState (Parsec DiscoParseError FilePath) Char
escapedSpace StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError FilePath) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError FilePath) Char
StateT
  ParserState (Parsec DiscoParseError FilePath) (Token FilePath)
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle)
 where
  escapedSpace :: StateT ParserState (Parsec DiscoParseError FilePath) Char
escapedSpace = StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token FilePath
-> StateT
     ParserState (Parsec DiscoParseError FilePath) (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
C.char Char
Token FilePath
'\\' StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
-> StateT ParserState (Parsec DiscoParseError FilePath) Char
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token FilePath
-> StateT
     ParserState (Parsec DiscoParseError FilePath) (Token FilePath)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
C.char Char
Token FilePath
' ')

-- | 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 a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
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 Parser SomeREPLExpr
-> FilePath
-> FilePath
-> Either (ParseErrorBundle FilePath DiscoParseError) SomeREPLExpr
forall a.
Parser a
-> FilePath
-> FilePath
-> Either (ParseErrorBundle FilePath DiscoParseError) a
runParser (ExtSet -> Parser SomeREPLExpr -> Parser SomeREPLExpr
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 -> FilePath -> Either FilePath SomeREPLExpr
forall a b. a -> Either a b
Left (FilePath -> Either FilePath SomeREPLExpr)
-> FilePath -> Either FilePath SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle FilePath DiscoParseError -> FilePath
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> FilePath
errorBundlePretty ParseErrorBundle FilePath DiscoParseError
e
    Right SomeREPLExpr
l -> SomeREPLExpr -> Either FilePath SomeREPLExpr
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 (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
    , parser :: Parser (REPLExpr 'CAnn)
parser = Term -> REPLExpr 'CAnn
Ann (Term -> REPLExpr 'CAnn)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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
_) <- 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 ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop1 Term
t
  ATerm -> Sem r ()
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 (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
    , parser :: Parser (REPLExpr 'CCompile)
parser = Term -> REPLExpr 'CCompile
Compile (Term -> REPLExpr 'CCompile)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CCompile)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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
_) <- 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 ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop1 Term
t
  Core -> Sem r ()
forall ann (r :: EffectRow) t.
(Member (Output (Message ann)) 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
    { 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 (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
    , parser :: Parser (REPLExpr 'CDesugar)
parser = Term -> REPLExpr 'CDesugar
Desugar (Term -> REPLExpr 'CDesugar)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CDesugar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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
_) <- 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 ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop1 Term
t
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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) ann. Pretty t => t -> Sem r (Doc ann)
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
    { 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 (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
    , parser :: Parser (REPLExpr 'CDoc)
parser = DocInput -> REPLExpr 'CDoc
Doc (DocInput -> REPLExpr 'CDoc)
-> StateT ParserState (Parsec DiscoParseError FilePath) DocInput
-> Parser (REPLExpr 'CDoc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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
(Int -> DocInput -> ShowS)
-> (DocInput -> FilePath) -> ([DocInput] -> ShowS) -> Show DocInput
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DocInput -> ShowS
showsPrec :: Int -> DocInput -> ShowS
$cshow :: DocInput -> FilePath
show :: DocInput -> FilePath
$cshowList :: [DocInput] -> ShowS
showList :: [DocInput] -> ShowS
Show)

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

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
_))) = Sem r ()
forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocBool
handleDoc (Doc (DocTerm Term
TUnit)) = Sem r ()
forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocUnit
handleDoc (Doc (DocTerm Term
TWild)) = Sem r ()
forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocWild
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 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)) = Prim -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
Prim -> Sem r ()
handleDocPrim Prim
p
handleDoc (Doc (DocOther FilePath
s)) = DocKey -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
DocKey -> Sem r ()
handleDocMap (FilePath -> DocKey
OtherKey FilePath
s)

handleDocBool :: Members '[Output (Message ())] r => Sem r ()
handleDocBool :: forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocBool =
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ()) -> Sem r ()) -> Sem r (Doc ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$
    Sem r (Doc ())
"T and F (also written true and false, or True and False) are the two possible values of type Boolean."
      Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Reference -> Sem r (Doc ())
forall (r :: EffectRow) ann. Reference -> Sem r (Doc ann)
formatReference (FilePath -> Reference
mkRef FilePath
"bool")

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

handleDocWild :: Members '[Output (Message ())] r => Sem r ()
handleDocWild :: forall (r :: EffectRow).
Members '[Output (Message ())] r =>
Sem r ()
handleDocWild =
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ()) -> Sem r ()) -> Sem r (Doc ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$
    Sem r (Doc ())
"A wildcard pattern."
      Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Reference -> Sem r (Doc ())
forall (r :: EffectRow) ann. Reference -> Sem r (Doc ann)
formatReference (FilePath -> Reference
mkRef 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 (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 <- 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 Docs
replDocs <- forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting (Ctx Term Docs) TopInfo (Ctx Term Docs)
-> TopInfo -> Ctx Term Docs
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const (Ctx Term Docs) ModuleInfo)
-> TopInfo -> Const (Ctx Term Docs) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Ctx Term Docs) ModuleInfo)
 -> TopInfo -> Const (Ctx Term Docs) TopInfo)
-> ((Ctx Term Docs -> Const (Ctx Term Docs) (Ctx Term Docs))
    -> ModuleInfo -> Const (Ctx Term Docs) ModuleInfo)
-> Getting (Ctx Term Docs) TopInfo (Ctx Term Docs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ctx Term Docs -> Const (Ctx Term Docs) (Ctx Term Docs))
-> ModuleInfo -> Const (Ctx Term Docs) ModuleInfo
Lens' ModuleInfo (Ctx Term Docs)
miDocs))

  TyCtx
importCtx <- 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 <- 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 Docs
importDocs <- forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([Ctx Term Docs] -> Ctx Term Docs
forall a b. [Ctx a b] -> Ctx a b
joinCtxs ([Ctx Term Docs] -> Ctx Term Docs)
-> (TopInfo -> [Ctx Term Docs]) -> TopInfo -> Ctx Term Docs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Ctx Term Docs) -> [ModuleInfo] -> [Ctx Term Docs]
forall a b. (a -> b) -> [a] -> [b]
map (((Ctx Term Docs -> Const (Ctx Term Docs) (Ctx Term Docs))
 -> ModuleInfo -> Const (Ctx Term Docs) ModuleInfo)
-> ModuleInfo -> Ctx Term Docs
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Ctx Term Docs -> Const (Ctx Term Docs) (Ctx Term Docs))
-> ModuleInfo -> Const (Ctx Term Docs) ModuleInfo
Lens' ModuleInfo (Ctx Term Docs)
miDocs) ([ModuleInfo] -> [Ctx Term Docs])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [Ctx Term Docs]
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 Docs
docs = Ctx Term Docs
replDocs Ctx Term Docs -> Ctx Term Docs -> Ctx Term Docs
forall a b. Ctx a b -> Ctx a b -> Ctx a b
`joinCtx` Ctx Term Docs
importDocs

  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
debug (Sem r (Doc ()) -> Sem r ()) -> Sem r (Doc ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text (FilePath -> Sem r (Doc ()))
-> (Ctx Term Docs -> FilePath) -> Ctx Term Docs -> Sem r (Doc ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx Term Docs -> FilePath
forall a. Show a => a -> FilePath
show (Ctx Term Docs -> Sem r (Doc ()))
-> Ctx Term Docs -> Sem r (Doc ())
forall a b. (a -> b) -> a -> b
$ Ctx Term Docs
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, FilePath -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Name Term -> FilePath
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 (Name Term -> FilePath
forall a. Name a -> FilePath
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 ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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) ann. Pretty t => t -> Sem r (Doc ann)
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 Docs
-> Either (QName Term, PolyType) TyDefBody -> Sem r ()
showDoc Ctx Term Docs
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 Docs
-> Either (QName Term, PolyType) TyDefBody -> Sem r ()
showDoc Ctx Term Docs
docs (Left (QName Term
qn, PolyType
ty)) =
    Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Name Term -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x, Sem r (Doc ())
":", PolyType -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' PolyType
ty]
        Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ case QName Term -> Ctx Term Docs -> Maybe Docs
forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' QName Term
qn Ctx Term Docs
docs of
          Just (DocString [FilePath]
ss : Docs
_) -> [Sem r (Doc ())] -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
"" Sem r (Doc ()) -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. a -> [a] -> [a]
: (FilePath -> Sem r (Doc ())) -> [FilePath] -> [Sem r (Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text [FilePath]
ss [Sem r (Doc ())] -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. [a] -> [a] -> [a]
++ [FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
""])
          Maybe Docs
_ -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
PP.empty
  showDoc Ctx Term Docs
docs (Right TyDefBody
tdBody) =
    Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ()) -> Sem r ()) -> Sem r (Doc ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$
      (FilePath, TyDefBody) -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' (Name Term -> FilePath
forall a. Name a -> FilePath
name2String Name Term
x, TyDefBody
tdBody)
        Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ case Name Term -> Ctx Term Docs -> [(QName Term, Docs)]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' Name Term
x Ctx Term Docs
docs of
          ((QName Term
_, DocString [FilePath]
ss : Docs
_) : [(QName Term, Docs)]
_) -> [Sem r (Doc ())] -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
"" Sem r (Doc ()) -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. a -> [a] -> [a]
: (FilePath -> Sem r (Doc ())) -> [FilePath] -> [Sem r (Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text [FilePath]
ss [Sem r (Doc ())] -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. [a] -> [a] -> [a]
++ [FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
""])
          [(QName Term, Docs)]
_ -> Sem r (Doc ())
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
  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))
  let attrs :: [Sem r (Doc ())]
attrs =
        ( case Prim
prim of
            PrimUOp UOp
u -> case Map UOp OpInfo
uopMap Map UOp OpInfo -> UOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
! UOp
u of
              OpInfo (UOpF UFixity
f UOp
_) [FilePath]
syns Int
_ -> Bool -> Bool -> [FilePath] -> [Sem r (Doc ())]
forall {f :: * -> *} {ann}.
(IsString (f (Doc ann)), Monad f) =>
Bool -> Bool -> [FilePath] -> [f (Doc ann)]
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) [FilePath]
syns
              OpInfo
_ -> FilePath -> [Sem r (Doc ())]
forall a. HasCallStack => FilePath -> a
error (FilePath -> [Sem r (Doc ())]) -> FilePath -> [Sem r (Doc ())]
forall a b. (a -> b) -> a -> b
$ FilePath
"handleDocPrim: No OpInfo for unary op " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ UOp -> FilePath
forall a. Show a => a -> FilePath
show UOp
u
            PrimBOp BOp
b -> Bool -> Bool -> [FilePath] -> [Sem r (Doc ())]
forall {f :: * -> *} {ann}.
(IsString (f (Doc ann)), Monad f) =>
Bool -> Bool -> [FilePath] -> [f (Doc ann)]
describeAlts Bool
True Bool
True (OpInfo -> [FilePath]
opSyns (OpInfo -> [FilePath]) -> OpInfo -> [FilePath]
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
PrimFloor -> Bool -> Bool -> [FilePath] -> [Sem r (Doc ())]
forall {f :: * -> *} {ann}.
(IsString (f (Doc ann)), Monad f) =>
Bool -> Bool -> [FilePath] -> [f (Doc ann)]
describeAlts Bool
False Bool
False [FilePath
"floor(x)", FilePath
"⌊x⌋"]
            Prim
PrimCeil -> Bool -> Bool -> [FilePath] -> [Sem r (Doc ())]
forall {f :: * -> *} {ann}.
(IsString (f (Doc ann)), Monad f) =>
Bool -> Bool -> [FilePath] -> [f (Doc ann)]
describeAlts Bool
False Bool
False [FilePath
"ceiling(x)", FilePath
"⌈x⌉"]
            Prim
PrimAbs -> Bool -> Bool -> [FilePath] -> [Sem r (Doc ())]
forall {f :: * -> *} {ann}.
(IsString (f (Doc ann)), Monad f) =>
Bool -> Bool -> [FilePath] -> [f (Doc ann)]
describeAlts Bool
False Bool
False [FilePath
"abs(x)", FilePath
"|x|"]
            Prim
_ -> []
        )
          [Sem r (Doc ())] -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. [a] -> [a] -> [a]
++ ( case Prim
prim of
                PrimUOp UOp
u -> [Int -> Sem r (Doc ())
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 -> [Int -> Sem r (Doc ())
forall {f :: * -> *} {ann} {a}.
(Applicative f, IsString (f (Doc ann)), Show a) =>
a -> f (Doc ann)
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 :: * -> *} {ann}.
(Applicative m, IsString (m (Doc ann))) =>
BFixity -> m (Doc ann)
describeFixity (BOp -> BFixity
assoc BOp
b)]
                Prim
_ -> []
             )
  case [Sem r (Doc ())]
attrs of
    [] -> () -> Sem r ()
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    [Sem r (Doc ())]
_ -> Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ()) -> Sem r ())
-> ([Sem r (Doc ())] -> Sem r (Doc ()))
-> [Sem r (Doc ())]
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r (Doc ())] -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat ([Sem r (Doc ())] -> Sem r ()) -> [Sem r (Doc ())] -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [Sem r (Doc ())]
attrs
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
PP.empty
  DocKey -> Sem r ()
forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
DocKey -> Sem r ()
handleDocMap (Prim -> DocKey
PrimKey Prim
prim)
 where
  describePrec :: a -> f (Doc ann)
describePrec a
p = f (Doc ann)
"precedence level" f (Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> FilePath -> f (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text (a -> FilePath
forall a. Show a => a -> FilePath
show a
p)
  describeFixity :: BFixity -> m (Doc ann)
describeFixity BFixity
In = m (Doc ann)
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:" f (Doc ann) -> f (Doc ann) -> f (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> 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)
"," ((FilePath -> f (Doc ann)) -> [FilePath] -> [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 =
      [f (Doc ann)] -> f (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hcat
        [ if Bool
pre then f (Doc ann)
"~" else f (Doc ann)
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
PP.empty
        , FilePath -> f (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
op
        , if Bool
post then f (Doc ann)
"~" else f (Doc ann)
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
PP.empty
        ]

formatReference :: Reference -> Sem r (Doc ann)
formatReference :: forall (r :: EffectRow) ann. Reference -> Sem r (Doc ann)
formatReference (Reference RefType
rty FilePath
p) = case RefType
rty of
  RefType
Ref -> Sem r (Doc ann)
"https://disco-lang.readthedocs.io/en/latest/reference/" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> FilePath -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
p Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
".html"
  RefType
Intro -> Sem r (Doc ann)
"https://disco-lang.readthedocs.io/en/latest/introduction/" Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> FilePath -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
p Sem r (Doc ann) -> Sem r (Doc ann) -> Sem r (Doc ann)
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ann)
".html"
  RefType
URL -> FilePath -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
p

handleDocMap ::
  Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
  DocKey ->
  Sem r ()
handleDocMap :: forall (r :: EffectRow).
Members
  '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())]
  r =>
DocKey -> Sem r ()
handleDocMap DocKey
k = case DocKey
-> Map DocKey (FilePath, [Reference])
-> Maybe (FilePath, [Reference])
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup DocKey
k Map DocKey (FilePath, [Reference])
docMap of
  Maybe (FilePath, [Reference])
Nothing -> case DocKey
k of
    PrimKey Prim
_ -> () -> Sem r ()
forall a. a -> Sem r a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    OtherKey FilePath
s -> Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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
<> FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
s Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall a. Semigroup a => a -> a -> a
<> Sem r (Doc ())
"'."
  Just (FilePath
d, [Reference]
refs) ->
    Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ()) -> Sem r ())
-> ([Sem r (Doc ())] -> Sem r (Doc ()))
-> [Sem r (Doc ())]
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Sem r (Doc ())] -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat ([Sem r (Doc ())] -> Sem r ()) -> [Sem r (Doc ())] -> Sem r ()
forall a b. (a -> b) -> a -> b
$
      [ FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
d
      , Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
PP.empty
      ]
        [Sem r (Doc ())] -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. [a] -> [a] -> [a]
++ case [Reference]
refs of
          [] -> []
          [Reference]
_ -> (Reference -> Sem r (Doc ())) -> [Reference] -> [Sem r (Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map Reference -> Sem r (Doc ())
forall (r :: EffectRow) ann. Reference -> Sem r (Doc ann)
formatReference [Reference]
refs [Sem r (Doc ())] -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. [a] -> [a] -> [a]
++ [Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => m (Doc ann)
PP.empty]

------------------------------------------------------------
-- 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 = REPLExpr 'CEval -> Sem r ()
REPLExpr 'CEval
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
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 (Module -> REPLExpr 'CEval)
-> StateT ParserState (Parsec DiscoParseError FilePath) Module
-> Parser (REPLExpr 'CEval)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoadingMode
-> StateT ParserState (Parsec DiscoParseError FilePath) 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 <- Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
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
  ModuleInfo -> Sem r ()
forall ann (r :: EffectRow).
Members
  '[Error DiscoError, State TopInfo, Random, State Mem,
    Output (Message ann)]
  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 :: 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 (Env -> f Env) -> TopInfo -> f 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 <- 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 ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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) 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 ((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) (FilePath -> Name Term
forall a. FilePath -> Name a
string2Name FilePath
"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) (FilePath -> Name Core
forall a. FilePath -> Name a
string2Name FilePath
"it")) Value
v)
  Value -> Sem r Value
forall a. a -> Sem r a
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
    { 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 = REPLExpr 'CHelp -> Sem r ()
REPLExpr 'CHelp
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (r :: EffectRow).
Member (Output (Message ())) r =>
REPLExpr 'CHelp -> Sem r ()
handleHelp
    , parser :: Parser (REPLExpr 'CHelp)
parser = REPLExpr 'CHelp -> Parser (REPLExpr 'CHelp)
forall a.
a -> StateT ParserState (Parsec DiscoParseError FilePath) a
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 =
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat
      [ Sem r (Doc ())
"Commands available from the prompt:"
      , FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
""
      , [Sem r (Doc ())] -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
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} {ann}.
Applicative m =>
REPLCommand c -> m (Doc ann)
showCmd REPLCommand c
c) (REPLCommands -> [Sem r (Doc ())])
-> REPLCommands -> [Sem r (Doc ())]
forall a b. (a -> b) -> a -> b
$ REPLCommands -> REPLCommands
sortedList REPLCommands
discoCommands)
      , FilePath -> Sem r (Doc ())
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 =
    (SomeREPLCommand -> SomeREPLCommand -> Ordering)
-> REPLCommands -> REPLCommands
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(SomeCmd REPLCommand c
x) (SomeCmd REPLCommand c
y) -> FilePath -> FilePath -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (REPLCommand c -> FilePath
forall (c :: CmdTag). REPLCommand c -> FilePath
name REPLCommand c
x) (REPLCommand c -> FilePath
forall (c :: CmdTag). REPLCommand c -> FilePath
name REPLCommand c
y)) (REPLCommands -> REPLCommands) -> REPLCommands -> REPLCommands
forall a b. (a -> b) -> a -> b
$ REPLCommands -> REPLCommands
filteredCommands REPLCommands
cmds
  showCmd :: REPLCommand c -> m (Doc ann)
showCmd REPLCommand c
c = FilePath -> m (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text (FilePath -> Int -> FilePath
padRight (REPLCommand c -> FilePath
forall (c :: CmdTag). REPLCommand c -> FilePath
helpcmd REPLCommand c
c) Int
maxlen FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"  " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ REPLCommand c -> FilePath
forall (c :: CmdTag). REPLCommand c -> FilePath
shortHelp REPLCommand c
c)
  longestCmd :: REPLCommands -> Int
longestCmd REPLCommands
cmds = [Int] -> Int
forall a. (Num a, Ord a) => [a] -> a
maximum0 ([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) -> FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ REPLCommand c -> FilePath
forall (c :: CmdTag). REPLCommand c -> FilePath
helpcmd REPLCommand c
c) REPLCommands
cmds
  padRight :: FilePath -> Int -> FilePath
padRight FilePath
s Int
maxsize = Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
maxsize (FilePath
s FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> FilePath
forall a. a -> [a]
repeat Char
' ')
  --  don't show dev-only commands by default
  filteredCommands :: REPLCommands -> REPLCommands
filteredCommands = (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)

------------------------------------------------------------
-- :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 = REPLExpr 'CLoad -> Sem r ()
REPLExpr 'CLoad
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
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 (FilePath -> REPLExpr 'CLoad)
-> Parser FilePath -> Parser (REPLExpr 'CLoad)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser 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) = Sem r Bool -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (FilePath -> Sem r Bool
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 ((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 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 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 -> FilePath -> Sem (Input TopInfo : r) ModuleInfo
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
  ModuleInfo -> Sem r ()
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 <- 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
$ [QName Term] -> Ctx ATerm [ATerm] -> Sem (Input TopInfo : r) Bool
forall (r :: EffectRow).
Members (Output (Message ()) : Input TopInfo : EvalEffects) r =>
[QName Term] -> Ctx ATerm [ATerm] -> Sem r Bool
runAllTests (ModuleInfo
m ModuleInfo
-> Getting [QName Term] ModuleInfo [QName Term] -> [QName Term]
forall s a. s -> Getting a s a -> a
^. Getting [QName Term] ModuleInfo [QName Term]
Lens' ModuleInfo [QName Term]
miNames) (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
  forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((Maybe FilePath -> Identity (Maybe FilePath))
-> TopInfo -> Identity TopInfo
Lens' TopInfo (Maybe FilePath)
lastFile ((Maybe FilePath -> Identity (Maybe FilePath))
 -> TopInfo -> Identity TopInfo)
-> FilePath -> TopInfo -> TopInfo
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ FilePath
fp)
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info Sem r (Doc ())
"Loaded."
  Bool -> Sem r Bool
forall a. a -> Sem r a
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
  | Ctx ATerm [ATerm] -> Bool
forall a b. Ctx a b -> Bool
Ctx.null Ctx ATerm [ATerm]
aprops = Bool -> Sem r Bool
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  | Bool
otherwise = do
      Sem r (Doc ()) -> Sem r ()
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
      [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 Term, [ATerm]) -> Sem r Bool)
-> [(QName Term, [ATerm])] -> Sem r [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((QName Term -> [ATerm] -> Sem r Bool)
-> (QName Term, [ATerm]) -> Sem r Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry QName Term -> [ATerm] -> Sem r Bool
forall (r :: EffectRow).
Members (Output (Message ()) : Input TopInfo : EvalEffects) r =>
QName Term -> [ATerm] -> Sem r Bool
runTests) ((QName Term -> Maybe (QName Term, [ATerm]))
-> [QName Term] -> [(QName Term, [ATerm])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\QName Term
n -> (QName Term
n,) ([ATerm] -> (QName Term, [ATerm]))
-> Maybe [ATerm] -> Maybe (QName Term, [ATerm])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName ATerm -> Ctx ATerm [ATerm] -> Maybe [ATerm]
forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' (QName Term -> QName ATerm
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 <- 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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)
forall (f :: * -> *) a.
Applicative f =>
(ATerm, f a) -> f (ATerm, 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 b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& 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 Term -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures of
      Bool
True -> Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent 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 :: * -> *) 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 (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 :: * -> *) ann.
Applicative f =>
f (Doc ann) -> [f (Doc ann)] -> f (Doc ann)
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) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
ATerm -> TestResult -> Sem r (Doc ann)
prettyTestResult) [(ATerm, TestResult)]
failures
        Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent 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 :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ Sem r (Doc ())
prettyFailures
    Bool -> Sem r Bool
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(ATerm, TestResult)] -> Bool
forall a. [a] -> Bool
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 = 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
    , parser :: Parser (REPLExpr 'CNames)
parser = REPLExpr 'CNames -> Parser (REPLExpr 'CNames)
forall a.
a -> StateT ParserState (Parsec DiscoParseError FilePath) a
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 (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 <- 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 ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat (((FilePath, TyDefBody) -> Sem r (Doc ()))
-> [(FilePath, TyDefBody)] -> [Sem r (Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath, TyDefBody) -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' (TyDefCtx -> [(FilePath, TyDefBody)]
forall k a. Map k a -> [(k, a)]
M.assocs TyDefCtx
tyDef))
      Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
$+$ [Sem r (Doc ())] -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
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} {ann}.
Pretty t =>
(QName a, t) -> Sem r (Doc ann)
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 ann)
showFn (QName NameProvenance
_ Name a
x, t
ty) = [Sem r (Doc ann)] -> Sem r (Doc ann)
forall (f :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
hsep [Name a -> Sem r (Doc ann)
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name a
x, FilePath -> Sem r (Doc ann)
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
":", t -> Sem r (Doc ann)
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 = REPLExpr 'CNop -> Sem r ()
REPLExpr 'CNop
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (r :: EffectRow). REPLExpr 'CNop -> Sem r ()
handleNop
    , parser :: Parser (REPLExpr 'CNop)
parser = REPLExpr 'CNop
Nop REPLExpr 'CNop -> Parser () -> Parser (REPLExpr 'CNop)
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Parser ()
sc Parser () -> Parser () -> Parser ()
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) a
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 :: forall (r :: EffectRow). REPLExpr 'CNop -> Sem r ()
handleNop REPLExpr 'CNop
Nop = () -> Sem r ()
forall a. a -> Sem r a
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 = REPLExpr 'CParse -> Sem r ()
REPLExpr 'CParse
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (r :: EffectRow).
Member (Output (Message ())) r =>
REPLExpr 'CParse -> Sem r ()
handleParse
    , parser :: Parser (REPLExpr 'CParse)
parser = Term -> REPLExpr 'CParse
Parse (Term -> REPLExpr 'CParse)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CParse)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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) = Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text (Term -> FilePath
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 = REPLExpr 'CPretty -> Sem r ()
REPLExpr 'CPretty
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (r :: EffectRow).
Members '[LFresh, Output (Message ())] r =>
REPLExpr 'CPretty -> Sem r ()
handlePretty
    , parser :: Parser (REPLExpr 'CPretty)
parser = Term -> REPLExpr 'CPretty
Pretty (Term -> REPLExpr 'CPretty)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CPretty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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) = Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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) 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 = REPLExpr 'CPrint -> Sem r ()
REPLExpr 'CPrint
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
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 (Term -> REPLExpr 'CPrint)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CPrint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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 <- 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 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 <- (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 ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info (Sem r (Doc ()) -> Sem r ()) -> Sem r (Doc ()) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text ((Value -> Char) -> Value -> FilePath
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar Value
v)

------------------------------------------------------------
-- :table

tableCmd :: REPLCommand 'CTable
tableCmd :: REPLCommand 'CTable
tableCmd =
  REPLCommand
    { name :: FilePath
name = FilePath
"table"
    , helpcmd :: FilePath
helpcmd = FilePath
":table <expr>"
    , shortHelp :: FilePath
shortHelp = FilePath
"Print a formatted table for a list or function"
    , category :: REPLCommandCategory
category = REPLCommandCategory
User
    , cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd
    , action :: REPLExpr 'CTable
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = REPLExpr 'CTable -> Sem r ()
REPLExpr 'CTable
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : EvalEffects)
  r =>
REPLExpr 'CTable -> Sem r ()
handleTable
    , parser :: Parser (REPLExpr 'CTable)
parser = Term -> REPLExpr 'CTable
Table (Term -> REPLExpr 'CTable)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CTable)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) Term
parseTermOrOp
    }

handleTable :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CTable -> Sem r ()
handleTable :: forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : EvalEffects)
  r =>
REPLExpr 'CTable -> Sem r ()
handleTable (Table Term
t) = do
  (ATerm
at, PolyType
ty) <- Sem (Input TopInfo : r) (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) (ATerm, PolyType)
 -> Sem r (ATerm, PolyType))
-> (Sem
      (Reader TyCtx
         : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
      (ATerm, PolyType)
    -> Sem (Input TopInfo : r) (ATerm, PolyType))
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
  (Reader TyCtx
     : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
  (ATerm, PolyType)
-> Sem (Input TopInfo : 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 : Input TopInfo : r)
   (ATerm, PolyType)
 -> Sem r (ATerm, PolyType))
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     (ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
     (Reader TyCtx
        : Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
     (ATerm, PolyType)
forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Term -> Sem r (ATerm, PolyType)
inferTop1 Term
t
  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

  TyDefCtx
tydefs <- 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 r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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
$ PolyType -> Value -> Sem (Input TyDefCtx : r) FilePath
forall (r :: EffectRow).
Members (LFresh : Input TyDefCtx : EvalEffects) r =>
PolyType -> Value -> Sem r FilePath
formatTableFor PolyType
ty Value
v Sem (Input TyDefCtx : r) FilePath
-> (FilePath -> Sem (Input TyDefCtx : r) (Doc ()))
-> Sem (Input TyDefCtx : r) (Doc ())
forall a b.
Sem (Input TyDefCtx : r) a
-> (a -> Sem (Input TyDefCtx : r) b) -> Sem (Input TyDefCtx : r) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> Sem (Input TyDefCtx : r) (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text

-- | The max number of rows to show in the output of :table.
maxFunTableRows :: Int
maxFunTableRows :: Int
maxFunTableRows = Int
25

-- | Uncurry a type, turning a type of the form A -> B -> ... -> Y ->
--   Z into the pair of types (A * B * ... * Y * Unit, Z).  Note we do
--   not optimize away the Unit at the end of the chain, since this
--   needs to be an isomorphism.  Otherwise we would not be able to
--   distinguish between e.g.  Z and Unit -> Z.
uncurryTy :: Type -> (Type, Type)
uncurryTy :: Type -> (Type, Type)
uncurryTy (Type
tyA :->: Type
tyB) = (Type
tyA Type -> Type -> Type
:*: Type
tyAs, Type
tyRes)
 where
  (Type
tyAs, Type
tyRes) = Type -> (Type, Type)
uncurryTy Type
tyB
uncurryTy Type
ty = (Type
TyUnit, Type
ty)

-- | Evaluate the application of a curried function to an uncurried
--   input.
evalCurried :: Members EvalEffects r => Type -> Value -> Type -> Value -> Sem r Value
evalCurried :: forall (r :: EffectRow).
Members EvalEffects r =>
Type -> Value -> Type -> Value -> Sem r Value
evalCurried (Type
_ :->: Type
tyB) Value
f (Type
_ :*: Type
tyY) Value
v = do
  let (Value
v1, Value
v2) = (Value -> Value) -> (Value -> Value) -> Value -> (Value, Value)
forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> Value
forall a. a -> a
id Value -> Value
forall a. a -> a
id Value
v
  Value
f' <- Value -> [Value] -> Sem r Value
forall (r :: EffectRow).
Members '[Random, Error EvalError, State Mem] r =>
Value -> [Value] -> Sem r Value
evalApp Value
f [Value
v1]
  Type -> Value -> Type -> Value -> Sem r Value
forall (r :: EffectRow).
Members EvalEffects r =>
Type -> Value -> Type -> Value -> Sem r Value
evalCurried Type
tyB Value
f' Type
tyY Value
v2
evalCurried Type
_ Value
v Type
_ Value
_ = Value -> Sem r Value
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v

formatTableFor ::
  Members (LFresh ': Input TyDefCtx ': EvalEffects) r =>
  PolyType ->
  Value ->
  Sem r String
formatTableFor :: forall (r :: EffectRow).
Members (LFresh : Input TyDefCtx : EvalEffects) r =>
PolyType -> Value -> Sem r FilePath
formatTableFor (Forall Bind [Name Type] Type
bnd) Value
v = Bind [Name Type] Type
-> (([Name Type], Type) -> Sem r FilePath) -> Sem r FilePath
forall (r :: EffectRow) p t c.
(Member LFresh r, Alpha p, Alpha t) =>
Bind p t -> ((p, t) -> Sem r c) -> Sem r c
lunbind Bind [Name Type] Type
bnd ((([Name Type], Type) -> Sem r FilePath) -> Sem r FilePath)
-> (([Name Type], Type) -> Sem r FilePath) -> Sem r FilePath
forall a b. (a -> b) -> a -> b
$ \([Name Type]
vars, Type
ty) ->
  case [Name Type]
vars of
    [] -> case Type
ty of
      TyList Type
ety -> do
        [[(Alignment, FilePath)]]
byRows <- (Value -> Sem r [(Alignment, FilePath)])
-> [Value] -> Sem r [[(Alignment, FilePath)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member LFresh r, Member (Input TyDefCtx) r) =>
Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
formatCols Level
TopLevel Type
ety) ([Value] -> Sem r [[(Alignment, FilePath)]])
-> (Value -> [Value]) -> Value -> Sem r [[(Alignment, FilePath)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> Value -> [Value]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Value
forall a. a -> a
id (Value -> Sem r [[(Alignment, FilePath)]])
-> Value -> Sem r [[(Alignment, FilePath)]]
forall a b. (a -> b) -> a -> b
$ Value
v
        FilePath -> Sem r FilePath
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Sem r FilePath) -> FilePath -> Sem r FilePath
forall a b. (a -> b) -> a -> b
$ [[(Alignment, FilePath)]] -> FilePath
renderTable [[(Alignment, FilePath)]]
byRows
      (Type
_ :->: Type
_) -> do
        let (Type
tyInputs, Type
tyRes) = Type -> (Type, Type)
uncurryTy Type
ty
            vs :: [Value]
vs = Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take (Int
maxFunTableRows Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([Value] -> [Value]) -> [Value] -> [Value]
forall a b. (a -> b) -> a -> b
$ Type -> [Value]
enumerateType Type
tyInputs
            (Type
tyInputs', Value -> Value
stripV) = Type -> (Type, Value -> Value)
stripFinalUnit Type
tyInputs
        [Value]
results <- (Value -> Sem r Value) -> [Value] -> Sem r [Value]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Type -> Value -> Type -> Value -> Sem r Value
forall (r :: EffectRow).
Members EvalEffects r =>
Type -> Value -> Type -> Value -> Sem r Value
evalCurried Type
ty Value
v Type
tyInputs) [Value]
vs
        [[(Alignment, FilePath)]]
byRows <-
          (Value -> Sem r [(Alignment, FilePath)])
-> [Value] -> Sem r [[(Alignment, FilePath)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM
            (Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member LFresh r, Member (Input TyDefCtx) r) =>
Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
formatCols Level
TopLevel (Type
tyInputs' Type -> Type -> Type
:*: Type
tyRes))
            ((Value -> Value -> Value) -> [Value] -> [Value] -> [Value]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Value, Value) -> Value) -> Value -> Value -> Value
forall a b c. ((a, b) -> c) -> a -> b -> c
curry ((Value -> Value) -> (Value -> Value) -> (Value, Value) -> Value
forall a b. (a -> Value) -> (b -> Value) -> (a, b) -> Value
pairv Value -> Value
forall a. a -> a
id Value -> Value
forall a. a -> a
id)) (Int -> [Value] -> [Value]
forall a. Int -> [a] -> [a]
take Int
maxFunTableRows ((Value -> Value) -> [Value] -> [Value]
forall a b. (a -> b) -> [a] -> [b]
map Value -> Value
stripV [Value]
vs)) [Value]
results)
        FilePath -> Sem r FilePath
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Sem r FilePath) -> FilePath -> Sem r FilePath
forall a b. (a -> b) -> a -> b
$ [[(Alignment, FilePath)]] -> FilePath
renderTable ([[(Alignment, FilePath)]]
byRows [[(Alignment, FilePath)]]
-> [[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]]
forall a. [a] -> [a] -> [a]
++ [[(Alignment
B.left, FilePath
"...")] | [Value] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
maxFunTableRows Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1])
      Type
_otherTy -> do
        FilePath
tyStr <- Type -> Sem r FilePath
forall t (r :: EffectRow). Pretty t => t -> Sem r FilePath
prettyStr Type
ty
        FilePath -> Sem r FilePath
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return (FilePath -> Sem r FilePath) -> FilePath -> Sem r FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"Don't know how to make a table for type " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
tyStr
    [Name Type]
_vars -> FilePath -> Sem r FilePath
forall a. a -> Sem r a
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
"Can't make a table for a polymorphic type"

-- | Strip the unit type from the end of a chain like (tA :*: (tB :*: (tC :*: Unit))),
--   which is an output of 'uncurryTy', and return a function to make the corresponding
--   change to a value of that type.
stripFinalUnit :: Type -> (Type, Value -> Value)
stripFinalUnit :: Type -> (Type, Value -> Value)
stripFinalUnit (Type
tA :*: Type
TyUnit) = (Type
tA, (Value, Value) -> Value
forall a b. (a, b) -> a
fst ((Value, Value) -> Value)
-> (Value -> (Value, Value)) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> (Value -> Value) -> Value -> (Value, Value)
forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> Value
forall a. a -> a
id Value -> Value
forall a. a -> a
id)
stripFinalUnit (Type
tA :*: Type
tB) = (Type
tA Type -> Type -> Type
:*: Type
tB', (Value -> Value) -> (Value -> Value) -> (Value, Value) -> Value
forall a b. (a -> Value) -> (b -> Value) -> (a, b) -> Value
pairv Value -> Value
forall a. a -> a
id Value -> Value
forall a. a -> a
id ((Value, Value) -> Value)
-> (Value -> (Value, Value)) -> Value -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> (Value, Value) -> (Value, Value)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Value -> Value
v' ((Value, Value) -> (Value, Value))
-> (Value -> (Value, Value)) -> Value -> (Value, Value)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Value -> Value) -> (Value -> Value) -> Value -> (Value, Value)
forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> Value
forall a. a -> a
id Value -> Value
forall a. a -> a
id)
 where
  (Type
tB', Value -> Value
v') = Type -> (Type, Value -> Value)
stripFinalUnit Type
tB
stripFinalUnit Type
ty = (Type
ty, Value -> Value
forall a. a -> a
id)

data Level = TopLevel | NestedPair | InnerLevel
  deriving (Level -> Level -> Bool
(Level -> Level -> Bool) -> (Level -> Level -> Bool) -> Eq Level
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Level -> Level -> Bool
== :: Level -> Level -> Bool
$c/= :: Level -> Level -> Bool
/= :: Level -> Level -> Bool
Eq, Eq Level
Eq Level =>
(Level -> Level -> Ordering)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Bool)
-> (Level -> Level -> Level)
-> (Level -> Level -> Level)
-> Ord Level
Level -> Level -> Bool
Level -> Level -> Ordering
Level -> Level -> Level
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Level -> Level -> Ordering
compare :: Level -> Level -> Ordering
$c< :: Level -> Level -> Bool
< :: Level -> Level -> Bool
$c<= :: Level -> Level -> Bool
<= :: Level -> Level -> Bool
$c> :: Level -> Level -> Bool
> :: Level -> Level -> Bool
$c>= :: Level -> Level -> Bool
>= :: Level -> Level -> Bool
$cmax :: Level -> Level -> Level
max :: Level -> Level -> Level
$cmin :: Level -> Level -> Level
min :: Level -> Level -> Level
Ord, Int -> Level -> ShowS
[Level] -> ShowS
Level -> FilePath
(Int -> Level -> ShowS)
-> (Level -> FilePath) -> ([Level] -> ShowS) -> Show Level
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Level -> ShowS
showsPrec :: Int -> Level -> ShowS
$cshow :: Level -> FilePath
show :: Level -> FilePath
$cshowList :: [Level] -> ShowS
showList :: [Level] -> ShowS
Show)

-- | Turn a value into a list of formatted columns in a type-directed
--   way.  Lists and tuples are only split out into columns if they
--   occur at the top level; lists or tuples nested inside of other
--   data structures are simply pretty-printed.  However, note we have
--   to make a special case for nested tuples: if a pair type occurs
--   at the top level we keep recursively splitting out its children
--   into columns as long as they are also pair types.
--
--   Any value of a type other than a list or tuple is simply
--   pretty-printed.
formatCols ::
  (Member LFresh r, Member (Input TyDefCtx) r) =>
  Level ->
  Type ->
  Value ->
  Sem r [(B.Alignment, String)]
formatCols :: forall (r :: EffectRow).
(Member LFresh r, Member (Input TyDefCtx) r) =>
Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
formatCols Level
l (Type
t1 :*: Type
t2) ((Value -> Value) -> (Value -> Value) -> Value -> (Value, Value)
forall a b. (Value -> a) -> (Value -> b) -> Value -> (a, b)
vpair Value -> Value
forall a. a -> a
id Value -> Value
forall a. a -> a
id -> (Value
v1, Value
v2))
  | Level
l Level -> [Level] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Level
TopLevel, Level
NestedPair] =
      [(Alignment, FilePath)]
-> [(Alignment, FilePath)] -> [(Alignment, FilePath)]
forall a. [a] -> [a] -> [a]
(++) ([(Alignment, FilePath)]
 -> [(Alignment, FilePath)] -> [(Alignment, FilePath)])
-> Sem r [(Alignment, FilePath)]
-> Sem r ([(Alignment, FilePath)] -> [(Alignment, FilePath)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member LFresh r, Member (Input TyDefCtx) r) =>
Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
formatCols Level
NestedPair Type
t1 Value
v1 Sem r ([(Alignment, FilePath)] -> [(Alignment, FilePath)])
-> Sem r [(Alignment, FilePath)] -> Sem r [(Alignment, FilePath)]
forall a b. Sem r (a -> b) -> Sem r a -> Sem r b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member LFresh r, Member (Input TyDefCtx) r) =>
Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
formatCols Level
NestedPair Type
t2 Value
v2
-- Special case for String (= List Char), just print as string value
formatCols Level
TopLevel Type
TyString Value
v = Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member (Input TyDefCtx) r, Member LFresh r) =>
Type -> Value -> Sem r [(Alignment, FilePath)]
formatColDefault Type
TyString Value
v
-- For any other lists @ top level, print each element in a separate column
formatCols Level
TopLevel (TyList Type
ety) ((Value -> Value) -> Value -> [Value]
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Value
forall a. a -> a
id -> [Value]
vs) =
  [[(Alignment, FilePath)]] -> [(Alignment, FilePath)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Alignment, FilePath)]] -> [(Alignment, FilePath)])
-> Sem r [[(Alignment, FilePath)]] -> Sem r [(Alignment, FilePath)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Value -> Sem r [(Alignment, FilePath)])
-> [Value] -> Sem r [[(Alignment, FilePath)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member LFresh r, Member (Input TyDefCtx) r) =>
Level -> Type -> Value -> Sem r [(Alignment, FilePath)]
formatCols Level
InnerLevel Type
ety) [Value]
vs
formatCols Level
_ Type
ty Value
v = Type -> Value -> Sem r [(Alignment, FilePath)]
forall (r :: EffectRow).
(Member (Input TyDefCtx) r, Member LFresh r) =>
Type -> Value -> Sem r [(Alignment, FilePath)]
formatColDefault Type
ty Value
v

-- | Default formatting of a typed column value by simply
--   pretty-printing it, and using the alignment appropriate for its
--   type.
formatColDefault ::
  (Member (Input TyDefCtx) r, Member LFresh r) =>
  Type ->
  Value ->
  Sem r [(B.Alignment, String)]
formatColDefault :: forall (r :: EffectRow).
(Member (Input TyDefCtx) r, Member LFresh r) =>
Type -> Value -> Sem r [(Alignment, FilePath)]
formatColDefault Type
ty Value
v = ((Alignment, FilePath)
-> [(Alignment, FilePath)] -> [(Alignment, FilePath)]
forall a. a -> [a] -> [a]
: []) ((Alignment, FilePath) -> [(Alignment, FilePath)])
-> (FilePath -> (Alignment, FilePath))
-> FilePath
-> [(Alignment, FilePath)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type -> Alignment
alignmentForType Type
ty,) (FilePath -> [(Alignment, FilePath)])
-> Sem r FilePath -> Sem r [(Alignment, FilePath)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Sem (Reader PA : r) (Doc Any) -> Sem r FilePath
forall (r :: EffectRow) ann.
Sem (Reader PA : r) (Doc ann) -> Sem r FilePath
renderDoc (Type -> Value -> Sem (Reader PA : r) (Doc Any)
forall (r :: EffectRow) ann.
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
Type -> Value -> Sem r (Doc ann)
prettyValue Type
ty Value
v)

alignmentForType :: Type -> B.Alignment
alignmentForType :: Type -> Alignment
alignmentForType Type
ty | Type
ty Type -> [Type] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type
TyN, Type
TyZ, Type
TyF, Type
TyQ] = Alignment
B.right
alignmentForType Type
_ = Alignment
B.left

-- | Render a table, given as a list of rows, formatting it so that
-- each column is aligned.
renderTable :: [[(B.Alignment, String)]] -> String
renderTable :: [[(Alignment, FilePath)]] -> FilePath
renderTable = ShowS
stripTrailingWS ShowS
-> ([[(Alignment, FilePath)]] -> FilePath)
-> [[(Alignment, FilePath)]]
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Box -> FilePath
B.render (Box -> FilePath)
-> ([[(Alignment, FilePath)]] -> Box)
-> [[(Alignment, FilePath)]]
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Alignment -> [Box] -> Box
forall (f :: * -> *).
Foldable f =>
Int -> Alignment -> f Box -> Box
B.hsep Int
2 Alignment
B.top ([Box] -> Box)
-> ([[(Alignment, FilePath)]] -> [Box])
-> [[(Alignment, FilePath)]]
-> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Alignment, FilePath)] -> Box)
-> [[(Alignment, FilePath)]] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map [(Alignment, FilePath)] -> Box
renderCol ([[(Alignment, FilePath)]] -> [Box])
-> ([[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]])
-> [[(Alignment, FilePath)]]
-> [Box]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]]
forall a. [[a]] -> [[a]]
transpose ([[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]])
-> ([[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]])
-> [[(Alignment, FilePath)]]
-> [[(Alignment, FilePath)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]]
pad
 where
  pad :: [[(B.Alignment, String)]] -> [[(B.Alignment, String)]]
  pad :: [[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]]
pad [[(Alignment, FilePath)]]
rows = ([(Alignment, FilePath)] -> [(Alignment, FilePath)])
-> [[(Alignment, FilePath)]] -> [[(Alignment, FilePath)]]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [(Alignment, FilePath)] -> [(Alignment, FilePath)]
forall {b}.
IsString b =>
Int -> [(Alignment, b)] -> [(Alignment, b)]
padTo ([Int] -> Int
forall a. (Num a, Ord a) => [a] -> a
maximum0 ([Int] -> Int)
-> ([[(Alignment, FilePath)]] -> [Int])
-> [[(Alignment, FilePath)]]
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Alignment, FilePath)] -> Int)
-> [[(Alignment, FilePath)]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [(Alignment, FilePath)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[(Alignment, FilePath)]] -> Int)
-> [[(Alignment, FilePath)]] -> Int
forall a b. (a -> b) -> a -> b
$ [[(Alignment, FilePath)]]
rows)) [[(Alignment, FilePath)]]
rows
  padTo :: Int -> [(Alignment, b)] -> [(Alignment, b)]
padTo Int
n = Int -> [(Alignment, b)] -> [(Alignment, b)]
forall a. Int -> [a] -> [a]
take Int
n ([(Alignment, b)] -> [(Alignment, b)])
-> ([(Alignment, b)] -> [(Alignment, b)])
-> [(Alignment, b)]
-> [(Alignment, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Alignment, b)] -> [(Alignment, b)] -> [(Alignment, b)]
forall a. [a] -> [a] -> [a]
++ (Alignment, b) -> [(Alignment, b)]
forall a. a -> [a]
repeat (Alignment
B.left, b
""))

  renderCol :: [(B.Alignment, String)] -> B.Box
  renderCol :: [(Alignment, FilePath)] -> Box
renderCol [] = Box
B.nullBox
  renderCol ((Alignment
align, FilePath
x) : [(Alignment, FilePath)]
xs) = Alignment -> [Box] -> Box
forall (f :: * -> *). Foldable f => Alignment -> f Box -> Box
B.vcat Alignment
align ([Box] -> Box) -> ([FilePath] -> [Box]) -> [FilePath] -> Box
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> Box) -> [FilePath] -> [Box]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> Box
B.text ([FilePath] -> Box) -> [FilePath] -> Box
forall a b. (a -> b) -> a -> b
$ FilePath
x FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: ((Alignment, FilePath) -> FilePath)
-> [(Alignment, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Alignment, FilePath) -> FilePath
forall a b. (a, b) -> b
snd [(Alignment, FilePath)]
xs

  stripTrailingWS :: ShowS
stripTrailingWS = [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> (FilePath -> [FilePath]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
stripEnd ([FilePath] -> [FilePath])
-> (FilePath -> [FilePath]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines
  stripEnd :: ShowS
stripEnd = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse

------------------------------------------------------------
-- :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 = REPLExpr 'CReload -> Sem r ()
REPLExpr 'CReload
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (r :: EffectRow).
Members
  (Error DiscoError
     : State TopInfo : Output (Message ()) : Embed IO : EvalEffects)
  r =>
REPLExpr 'CReload -> Sem r ()
handleReload
    , parser :: Parser (REPLExpr 'CReload)
parser = REPLExpr 'CReload -> Parser (REPLExpr 'CReload)
forall a.
a -> StateT ParserState (Parsec DiscoParseError FilePath) a
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 <- Getter TopInfo (Maybe FilePath) -> Sem r (Maybe FilePath)
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use (Maybe FilePath -> f (Maybe FilePath)) -> TopInfo -> f TopInfo
Lens' TopInfo (Maybe FilePath)
Getter TopInfo (Maybe FilePath)
lastFile
  case Maybe FilePath
file of
    Maybe FilePath
Nothing -> Sem r (Doc ()) -> Sem r ()
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 -> Sem r Bool -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (FilePath -> Sem r Bool
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 (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
    , parser :: Parser (REPLExpr 'CShowDefn)
parser = Name Term -> REPLExpr 'CShowDefn
ShowDefn (Name Term -> REPLExpr 'CShowDefn)
-> StateT ParserState (Parsec DiscoParseError FilePath) (Name Term)
-> Parser (REPLExpr 'CShowDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
sc Parser ()
-> StateT ParserState (Parsec DiscoParseError FilePath) (Name Term)
-> StateT ParserState (Parsec DiscoParseError FilePath) (Name Term)
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) b
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 = Name Term -> FilePath
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 (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 <- 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
forall a b. Coercible a b => a -> b
coerce Name Term
x) Ctx ATerm Defn
defns
      mtydef :: Maybe TyDefBody
mtydef = FilePath -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup FilePath
name2s TyDefCtx
tyDefns

  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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) ann. Pretty t => t -> Sem r (Doc ann)
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 a. a -> [a]
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
. (FilePath, TyDefBody) -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' ((FilePath, TyDefBody) -> Sem r (Doc ()))
-> (TyDefBody -> (FilePath, TyDefBody))
-> TyDefBody
-> Sem r (Doc ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath
name2s,)) Maybe TyDefBody
mtydef
    case [Sem r (Doc ())]
ds of
      [] -> FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
"No definition for" Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> Name Term -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Name Term
x
      [Sem r (Doc ())]
_nonEmptyList -> [Sem r (Doc ())] -> 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 = REPLExpr 'CTestProp -> Sem r ()
REPLExpr 'CTestProp
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
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 (Term -> REPLExpr 'CTestProp)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CTestProp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) 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 <- 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 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 ((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 ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
indent 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 ()))
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r)
     (Doc ())
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r)
     (Doc ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 :: * -> *) ann.
Functor f =>
Int -> f (Doc ann) -> f (Doc ann)
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 :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> ATerm
-> TestResult
-> Sem
     (Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r)
     (Doc ())
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 (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
    , parser :: Parser (REPLExpr 'CTypeCheck)
parser = Term -> REPLExpr 'CTypeCheck
TypeCheck (Term -> REPLExpr 'CTypeCheck)
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> Parser (REPLExpr 'CTypeCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError FilePath) Term
parseTermOrOp
    }

maxInferredTypes :: Int
maxInferredTypes :: Int
maxInferredTypes = Int
16

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
  NonEmpty (ATerm, PolyType)
asigs <- Sem
  (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
  (NonEmpty (ATerm, PolyType))
-> Sem r (NonEmpty (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)
   (NonEmpty (ATerm, PolyType))
 -> Sem r (NonEmpty (ATerm, PolyType)))
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (NonEmpty (ATerm, PolyType))
-> Sem r (NonEmpty (ATerm, PolyType))
forall a b. (a -> b) -> a -> b
$ Int
-> Term
-> Sem
     (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
     (NonEmpty (ATerm, PolyType))
forall ann (r :: EffectRow).
Members
  '[Output (Message ann), Reader TyCtx, Reader TyDefCtx,
    Error TCError, Fresh]
  r =>
Int -> Term -> Sem r (NonEmpty (ATerm, PolyType))
inferTop Int
maxInferredTypes Term
t
  NonEmpty PolyType
sigs <- Sem (Fresh : r) (NonEmpty PolyType) -> Sem r (NonEmpty PolyType)
forall (r :: EffectRow) a. Sem (Fresh : r) a -> Sem r a
runFresh (Sem (Fresh : r) (NonEmpty PolyType) -> Sem r (NonEmpty PolyType))
-> (Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
    -> Sem (Fresh : r) (NonEmpty PolyType))
-> Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
-> Sem r (NonEmpty PolyType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopInfo -> TyDefCtx)
-> Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
-> Sem (Fresh : r) (NonEmpty PolyType)
forall s t (r :: EffectRow) a.
Member (Input s) r =>
(s -> t) -> Sem (Input t : r) a -> Sem r a
mapInput (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)) (Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
 -> Sem r (NonEmpty PolyType))
-> Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
-> Sem r (NonEmpty PolyType)
forall a b. (a -> b) -> a -> b
$ NonEmpty PolyType
-> Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
forall ann (r :: EffectRow).
Members '[Input TyDefCtx, Output (Message ann), Fresh] r =>
NonEmpty PolyType -> Sem r (NonEmpty PolyType)
thin (NonEmpty PolyType
 -> Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType))
-> NonEmpty PolyType
-> Sem (Input TyDefCtx : Fresh : r) (NonEmpty PolyType)
forall a b. (a -> b) -> a -> b
$ ((ATerm, PolyType) -> PolyType)
-> NonEmpty (ATerm, PolyType) -> NonEmpty PolyType
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (ATerm, PolyType) -> PolyType
forall a b. (a, b) -> b
snd NonEmpty (ATerm, PolyType)
asigs
  let ([PolyType]
toShow, [PolyType]
extra) = Int -> NonEmpty PolyType -> ([PolyType], [PolyType])
forall a. Int -> NonEmpty a -> ([a], [a])
NE.splitAt Int
8 NonEmpty PolyType
sigs
  Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (NonEmpty PolyType -> Int
forall a. NonEmpty a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty PolyType
sigs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> Sem r ()
info Sem r (Doc ())
"This expression has multiple possible types.  Some examples:"
  Sem r (Doc ()) -> Sem r ()
forall ann (r :: EffectRow).
Member (Output (Message ann)) r =>
Sem r (Doc ann) -> 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 :: * -> *) ann.
Applicative f =>
[f (Doc ann)] -> f (Doc ann)
vcat ([Sem r (Doc ())] -> Sem r (Doc ()))
-> [Sem r (Doc ())] -> Sem r (Doc ())
forall a b. (a -> b) -> a -> b
$
      (PolyType -> Sem r (Doc ())) -> [PolyType] -> [Sem r (Doc ())]
forall a b. (a -> b) -> [a] -> [b]
map (\PolyType
sig -> Term -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' Term
t Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> FilePath -> Sem r (Doc ())
forall (m :: * -> *) ann. Applicative m => FilePath -> m (Doc ann)
text FilePath
":" Sem r (Doc ()) -> Sem r (Doc ()) -> Sem r (Doc ())
forall (f :: * -> *) ann.
Applicative f =>
f (Doc ann) -> f (Doc ann) -> f (Doc ann)
<+> PolyType -> Sem r (Doc ())
forall t (r :: EffectRow) ann. Pretty t => t -> Sem r (Doc ann)
pretty' PolyType
sig) [PolyType]
toShow
        [Sem r (Doc ())] -> [Sem r (Doc ())] -> [Sem r (Doc ())]
forall a. [a] -> [a] -> [a]
++ [Sem r (Doc ())
"..." | Bool -> Bool
not ([PolyType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [PolyType]
extra)]

------------------------------------------------------------

-- In :type, :doc, or :table commands, 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.
parseTermOrOp :: Parser Term
parseTermOrOp :: StateT ParserState (Parsec DiscoParseError FilePath) Term
parseTermOrOp =
  (StateT ParserState (Parsec DiscoParseError FilePath) Term
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError FilePath) Term
term StateT ParserState (Parsec DiscoParseError FilePath) Term
-> FilePath
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> FilePath -> m a
<?> FilePath
"expression")
    StateT ParserState (Parsec DiscoParseError FilePath) Term
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
forall a.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (StateT ParserState (Parsec DiscoParseError FilePath) Term
parseNakedOp StateT ParserState (Parsec DiscoParseError FilePath) Term
-> FilePath
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> FilePath -> m a
<?> FilePath
"operator")

parseNakedOp :: Parser Term
parseNakedOp :: StateT ParserState (Parsec DiscoParseError FilePath) Term
parseNakedOp = Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
-> StateT ParserState (Parsec DiscoParseError FilePath) Term
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 Parser ()
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall a b.
StateT ParserState (Parsec DiscoParseError FilePath) a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [StateT ParserState (Parsec DiscoParseError FilePath) Prim]
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((OpInfo
 -> StateT ParserState (Parsec DiscoParseError FilePath) Prim)
-> [OpInfo]
-> [StateT ParserState (Parsec DiscoParseError FilePath) Prim]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> StateT ParserState (Parsec DiscoParseError FilePath) 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 FilePath) Prim
mkOpParser (OpInfo (UOpF UFixity
_ UOp
op) [FilePath]
syns Int
_) = [StateT ParserState (Parsec DiscoParseError FilePath) Prim]
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((FilePath
 -> StateT ParserState (Parsec DiscoParseError FilePath) Prim)
-> [FilePath]
-> [StateT ParserState (Parsec DiscoParseError FilePath) Prim]
forall a b. (a -> b) -> [a] -> [b]
map ((UOp -> Prim
PrimUOp UOp
op Prim
-> Parser ()
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Parser ()
 -> StateT ParserState (Parsec DiscoParseError FilePath) Prim)
-> (FilePath -> Parser ())
-> FilePath
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Parser ()
reservedOp) [FilePath]
syns)
  mkOpParser (OpInfo (BOpF BFixity
_ BOp
op) [FilePath]
syns Int
_) = [StateT ParserState (Parsec DiscoParseError FilePath) Prim]
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((FilePath
 -> StateT ParserState (Parsec DiscoParseError FilePath) Prim)
-> [FilePath]
-> [StateT ParserState (Parsec DiscoParseError FilePath) Prim]
forall a b. (a -> b) -> [a] -> [b]
map ((BOp -> Prim
PrimBOp BOp
op Prim
-> Parser ()
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError FilePath) b
-> StateT ParserState (Parsec DiscoParseError FilePath) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Parser ()
 -> StateT ParserState (Parsec DiscoParseError FilePath) Prim)
-> (FilePath -> Parser ())
-> FilePath
-> StateT ParserState (Parsec DiscoParseError FilePath) Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Parser ()
reservedOp) [FilePath]
syns)