content: {-# 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 (Eq, 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 (Eq, 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 (Show, Eq, Typeable)
  
  ------------------------------------------------------------
  -- REPL command info record
  ------------------------------------------------------------
  
  -- | Data type to represent all the information about a single REPL
  --   command.
  data REPLCommand (c :: CmdTag) = REPLCommand
    { name :: String
    -- ^ Name of the command
    , helpcmd :: String
    -- ^ Help text showing how to use the command, e.g. ":ann <term>"
    , shortHelp :: String
    -- ^ Short free-form text explaining the command.
    --   We could also consider adding long help text as well.
    , category :: REPLCommandCategory
    -- ^ Is the command for users or devs?
    , cmdtype :: REPLCommandType
    -- ^ Is it a built-in command or colon command?
    , action :: REPLExpr c -> (forall r. Members DiscoEffects r => Sem r ())
    -- ^ The action to execute,
    -- given the input to the
    -- command.
    , 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 ty = P.filter (\(SomeCmd rc) -> cmdtype rc == 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 [] _ = return ()
  dispatch (SomeCmd c : cs) r@(SomeREPL e) = case gcast e of
    Just e' -> outputDiscoErrors $ action c e'
    Nothing -> dispatch cs 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 =
    [ SomeCmd annCmd
    , SomeCmd compileCmd
    , SomeCmd desugarCmd
    , SomeCmd docCmd
    , SomeCmd evalCmd
    , SomeCmd helpCmd
    , SomeCmd loadCmd
    , SomeCmd namesCmd
    , SomeCmd nopCmd
    , SomeCmd parseCmd
    , SomeCmd prettyCmd
    , SomeCmd printCmd
    , SomeCmd tableCmd
    , SomeCmd reloadCmd
    , SomeCmd showDefnCmd
    , SomeCmd typeCheckCmd
    , SomeCmd testPropCmd
    ]
  
  ------------------------------------------------------------
  -- Parsing
  ------------------------------------------------------------
  
  builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
  builtinCommandParser =
    foldr ((<|>) . (\(SomeCmd rc) -> SomeREPL <$> try (parser rc))) empty
      . byCmdType BuiltIn
  
  -- | Parse one of the colon commands in the given list of commands.
  commandParser :: REPLCommands -> Parser SomeREPLExpr
  commandParser allCommands =
    (symbol ":" *> many C.lowerChar) >>= parseCommandArgs 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 allCommands cmd = maybe badCmd snd $ find ((cmd `isPrefixOf`) . fst) parsers
   where
    badCmd = fail $ "Command \":" ++ cmd ++ "\" is unrecognized."
  
    parsers =
      map (\(SomeCmd rc) -> (name rc, SomeREPL <$> parser rc)) $
        byCmdType ColonCmd allCommands
  
  -- | Parse a file name.
  fileParser :: Parser FilePath
  fileParser = many C.spaceChar *> some (escapedSpace <|> L.charLiteral <|> anySingle)
   where
    escapedSpace = try (C.char '\\' *> C.char ' ')
  
  -- | A parser for something entered at the REPL prompt.
  lineParser :: REPLCommands -> Parser SomeREPLExpr
  lineParser allCommands =
    builtinCommandParser allCommands
      <|> commandParser 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 allCommands exts s =
    case runParser (withExts exts (lineParser allCommands)) "" s of
      Left e -> Left $ errorBundlePretty e
      Right l -> Right l
  
  --------------------------------------------------------------------------------
  -- The commands!
  --------------------------------------------------------------------------------
  
  ------------------------------------------------------------
  -- :ann
  
  annCmd :: REPLCommand 'CAnn
  annCmd =
    REPLCommand
      { name = "ann"
      , helpcmd = ":ann"
      , shortHelp = "Show type-annotated typechecked term"
      , category = Dev
      , cmdtype = ColonCmd
      , action = inputToState @TopInfo . handleAnn
      , parser = Ann <$> term
      }
  
  handleAnn ::
    Members '[Error DiscoError, Input TopInfo, Output (Message ())] r =>
    REPLExpr 'CAnn ->
    Sem r ()
  handleAnn (Ann t) = do
    (at, _) <- typecheckTop $ inferTop1 t
    infoPretty at
  
  ------------------------------------------------------------
  -- :compile
  
  compileCmd :: REPLCommand 'CCompile
  compileCmd =
    REPLCommand
      { name = "compile"
      , helpcmd = ":compile"
      , shortHelp = "Show a compiled term"
      , category = Dev
      , cmdtype = ColonCmd
      , action = inputToState @TopInfo . handleCompile
      , parser = Compile <$> term
      }
  
  handleCompile ::
    Members '[Error DiscoError, Input TopInfo, Output (Message ())] r =>
    REPLExpr 'CCompile ->
    Sem r ()
  handleCompile (Compile t) = do
    (at, _) <- typecheckTop $ inferTop1 t
    infoPretty . compileTerm $ at
  
  ------------------------------------------------------------
  -- :desugar
  
  desugarCmd :: REPLCommand 'CDesugar
  desugarCmd =
    REPLCommand
      { name = "desugar"
      , helpcmd = ":desugar"
      , shortHelp = "Show a desugared term"
      , category = Dev
      , cmdtype = ColonCmd
      , action = inputToState @TopInfo . handleDesugar
      , parser = Desugar <$> term
      }
  
  handleDesugar ::
    Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
    REPLExpr 'CDesugar ->
    Sem r ()
  handleDesugar (Desugar t) = do
    (at, _) <- typecheckTop $ inferTop1 t
    info $ pretty' . eraseDTerm . runDesugar . desugarTerm $ at
  
  ------------------------------------------------------------
  -- :doc
  
  docCmd :: REPLCommand 'CDoc
  docCmd =
    REPLCommand
      { name = "doc"
      , helpcmd = ":doc <term>"
      , shortHelp = "Show documentation"
      , category = User
      , cmdtype = ColonCmd
      , action = inputToState @TopInfo . handleDoc
      , parser = Doc <$> 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 (Show)
  
  parseDoc :: Parser DocInput
  parseDoc =
    (DocTerm <$> try term)
      <|> (DocPrim <$> try (parseNakedOpPrim <?> "operator"))
      <|> (DocOther <$> (sc *> many (anySingleBut ' ')))
  
  handleDoc ::
    Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
    REPLExpr 'CDoc ->
    Sem r ()
  handleDoc (Doc (DocTerm (TBool _))) = handleDocBool
  handleDoc (Doc (DocTerm TUnit)) = handleDocUnit
  handleDoc (Doc (DocTerm TWild)) = handleDocWild
  handleDoc (Doc (DocTerm (TPrim p))) = handleDocPrim p
  handleDoc (Doc (DocTerm (TVar x))) = handleDocVar x
  handleDoc (Doc (DocTerm _)) =
    err "Can't display documentation for an expression.  Try asking about a function, operator, or type name."
  handleDoc (Doc (DocPrim p)) = handleDocPrim p
  handleDoc (Doc (DocOther s)) = handleDocMap (OtherKey s)
  
  handleDocBool :: Members '[Output (Message ())] r => Sem r ()
  handleDocBool =
    info $
      "T and F (also written true and false, or True and False) are the two possible values of type Boolean."
        $+$ formatReference (mkRef "bool")
  
  handleDocUnit :: Members '[Output (Message ())] r => Sem r ()
  handleDocUnit =
    info $
      "The unit value, i.e. the single value of type Unit."
        $+$ formatReference (mkRef "unit")
  
  handleDocWild :: Members '[Output (Message ())] r => Sem r ()
  handleDocWild =
    info $
      "A wildcard pattern."
        $+$ formatReference (mkRef "wild-pattern")
  
  handleDocVar ::
    Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
    Name Term ->
    Sem r ()
  handleDocVar x = do
    replCtx <- inputs @TopInfo (view (replModInfo . miTys))
    replTydefs <- inputs @TopInfo (view (replModInfo . miTydefs))
    replDocs <- inputs @TopInfo (view (replModInfo . miDocs))
  
    importCtx <- inputs @TopInfo (joinCtxs . map (view miTys) . M.elems . view topModMap)
    importTydefs <- inputs @TopInfo (M.unions . map (view miTydefs) . M.elems . view topModMap)
    importDocs <- inputs @TopInfo (joinCtxs . map (view miDocs) . M.elems . view topModMap)
  
    let ctx = replCtx `joinCtx` importCtx
        tydefs = importTydefs `M.union` replTydefs
        docs = replDocs `joinCtx` importDocs
  
    debug $ text . show $ docs
  
    case (Ctx.lookupAll' x ctx, M.lookup (name2String x) tydefs) of
      ([], Nothing) ->
        -- Maybe the variable name entered by the user is actually a prim.
        case toPrim (name2String x) of
          (prim : _) -> handleDocPrim prim
          _ -> err $ "No documentation found for '" <> pretty' x <> "'."
      (binds, def) ->
        mapM_ (showDoc docs) (map Left binds ++ map Right (maybeToList def))
   where
    showDoc docs (Left (qn, ty)) =
      info $
        hsep [pretty' x, ":", pretty' ty]
          $+$ case Ctx.lookup' qn docs of
            Just (DocString ss : _) -> vcat (text "" : map text ss ++ [text ""])
            _ -> PP.empty
    showDoc docs (Right tdBody) =
      info $
        pretty' (name2String x, tdBody)
          $+$ case Ctx.lookupAll' x docs of
            ((_, DocString ss : _) : _) -> vcat (text "" : map text ss ++ [text ""])
            _ -> PP.empty
  
  handleDocPrim ::
    Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
    Prim ->
    Sem r ()
  handleDocPrim prim = do
    handleTypeCheck (TypeCheck (TPrim prim))
    let attrs =
          ( case prim of
              PrimUOp u -> case uopMap ! u of
                OpInfo (UOpF f _) syns _ -> describeAlts (f == Post) (f == Pre) syns
                _ -> error $ "handleDocPrim: No OpInfo for unary op " ++ show u
              PrimBOp b -> describeAlts True True (opSyns $ bopMap ! b)
              PrimFloor -> describeAlts False False ["floor(x)", "⌊x⌋"]
              PrimCeil -> describeAlts False False ["ceiling(x)", "⌈x⌉"]
              PrimAbs -> describeAlts False False ["abs(x)", "|x|"]
              _ -> []
          )
            ++ ( case prim of
                  PrimUOp u -> [describePrec (uPrec u)]
                  PrimBOp b -> [describePrec (bPrec b) <> describeFixity (assoc b)]
                  _ -> []
               )
    case attrs of
      [] -> pure ()
      _ -> info . vcat $ attrs
    info PP.empty
    handleDocMap (PrimKey prim)
   where
    describePrec p = "precedence level" <+> text (show p)
    describeFixity In = PP.empty
    describeFixity InL = ", left associative"
    describeFixity InR = ", right associative"
    describeAlts _ _ [] = []
    describeAlts _ _ [_] = []
    describeAlts pre post (_ : alts) = ["Alternative syntax:" <+> intercalate "," (map showOp alts)]
     where
      showOp op =
        hcat
          [ if pre then "~" else PP.empty
          , text op
          , if post then "~" else PP.empty
          ]
  
  formatReference :: Reference -> Sem r (Doc ann)
  formatReference (Reference rty p) = case rty of
    Ref -> "https://disco-lang.readthedocs.io/en/latest/reference/" <> text p <> ".html"
    Intro -> "https://disco-lang.readthedocs.io/en/latest/introduction/" <> text p <> ".html"
    URL -> text p
  
  handleDocMap ::
    Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
    DocKey ->
    Sem r ()
  handleDocMap k = case M.lookup k docMap of
    Nothing -> case k of
      PrimKey _ -> pure ()
      OtherKey s -> info $ "No documentation found for '" <> text s <> "'."
    Just (d, refs) ->
      info . vcat $
        [ text d
        , PP.empty
        ]
          ++ case refs of
            [] -> []
            _ -> map formatReference refs ++ [PP.empty]
  
  ------------------------------------------------------------
  -- eval
  
  evalCmd :: REPLCommand 'CEval
  evalCmd =
    REPLCommand
      { name = "eval"
      , helpcmd = "<code>"
      , shortHelp = "Evaluate a block of code"
      , category = User
      , cmdtype = BuiltIn
      , action = handleEval
      , parser = Eval <$> wholeModule REPL
      }
  
  handleEval ::
    Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
    REPLExpr 'CEval ->
    Sem r ()
  handleEval (Eval m) = do
    mi <- loadParsedDiscoModule False FromCwdOrStdlib REPLModule m
    addToREPLModule mi
    forM_ (mi ^. miTerms) (mapError EvalErr . evalTerm True . 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 pr at = do
    env <- use @TopInfo topEnv
    v <- runInputConst env $ eval (compileTerm at)
  
    tydefs <- use @TopInfo (replModInfo . to allTydefs)
    when pr $ info $ runInputConst tydefs $ prettyValue' ty v
  
    modify @TopInfo $
      (replModInfo . miTys %~ Ctx.insert (QName (QualifiedName REPLModule) (string2Name "it")) (toPolyType ty))
        . (topEnv %~ Ctx.insert (QName (QualifiedName REPLModule) (string2Name "it")) v)
    return v
   where
    ty = getType at
  
  ------------------------------------------------------------
  -- :help
  
  helpCmd :: REPLCommand 'CHelp
  helpCmd =
    REPLCommand
      { name = "help"
      , helpcmd = ":help"
      , shortHelp = "Show help"
      , category = User
      , cmdtype = ColonCmd
      , action = handleHelp
      , parser = return Help
      }
  
  handleHelp :: Member (Output (Message ())) r => REPLExpr 'CHelp -> Sem r ()
  handleHelp Help =
    info $
      vcat
        [ "Commands available from the prompt:"
        , text ""
        , vcat (map (\(SomeCmd c) -> showCmd c) $ sortedList discoCommands)
        , text ""
        ]
   where
    maxlen = longestCmd discoCommands
    sortedList cmds =
      sortBy (\(SomeCmd x) (SomeCmd y) -> compare (name x) (name y)) $ filteredCommands cmds
    showCmd c = text (padRight (helpcmd c) maxlen ++ "  " ++ shortHelp c)
    longestCmd cmds = maximum0 $ map (\(SomeCmd c) -> length $ helpcmd c) cmds
    padRight s maxsize = take maxsize (s ++ repeat ' ')
    --  don't show dev-only commands by default
    filteredCommands = P.filter (\(SomeCmd c) -> category c == User)
  
  ------------------------------------------------------------
  -- :load
  
  loadCmd :: REPLCommand 'CLoad
  loadCmd =
    REPLCommand
      { name = "load"
      , helpcmd = ":load <filename>"
      , shortHelp = "Load a file"
      , category = User
      , cmdtype = ColonCmd
      , action = handleLoadWrapper
      , parser = Load <$> 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 (Load fp) = void (handleLoad fp)
  
  handleLoad ::
    Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
    FilePath ->
    Sem r Bool
  handleLoad fp = do
    let (directory, modName) = splitFileName fp
  
    -- Reset top-level module map and context to empty, so we start
    -- fresh and pick up any changes to imported modules etc.
    modify @TopInfo $ topModMap .~ M.empty
    modify @TopInfo $ topEnv .~ Ctx.emptyCtx
  
    -- Load the module.
    m <- inputToState @TopInfo $ loadDiscoModule False (FromDir directory) modName
    setREPLModule m
  
    -- Now run any tests
    t <- inputToState $ runAllTests (m ^. miNames) (m ^. miProps)
  
    -- Evaluate and print any top-level terms
    forM_ (m ^. miTerms) (mapError EvalErr . evalTerm True . fst)
  
    -- Remember which was the most recently loaded file, so we can :reload
    modify @TopInfo (lastFile ?~ fp)
    info "Loaded."
    return 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 declNames aprops
    | Ctx.null aprops = return True
    | otherwise = do
        info "Running tests..."
        -- Use the order the names were defined in the module
        and <$> mapM (uncurry runTests) (mapMaybe (\n -> (n,) <$> Ctx.lookup' (coerce n) aprops) declNames)
   where
    numSamples :: Int
    numSamples = 50 -- XXX make this configurable somehow
    runTests :: Members (Output (Message ()) ': Input TopInfo ': EvalEffects) r => QName Term -> [AProperty] -> Sem r Bool
    runTests (QName _ n) props = do
      results <- inputTopEnv $ traverse (sequenceA . (id &&& runTest numSamples)) props
      let failures = P.filter (not . testIsOk . snd) results
          hdr = pretty' n <> ":"
  
      case P.null failures of
        True -> info $ indent 2 $ hdr <+> "OK"
        False -> do
          tydefs <- inputs @TopInfo (view (replModInfo . to allTydefs))
          let prettyFailures =
                runInputConst tydefs
                  . runReader initPA
                  . runLFresh
                  $ bulletList "-"
                  $ map (uncurry prettyTestResult) failures
          info $ indent 2 $ hdr $+$ prettyFailures
      return (P.null failures)
  
  ------------------------------------------------------------
  -- :names
  
  namesCmd :: REPLCommand 'CNames
  namesCmd =
    REPLCommand
      { name = "names"
      , helpcmd = ":names"
      , shortHelp = "Show all names in current scope"
      , category = User
      , cmdtype = ColonCmd
      , action = inputToState . handleNames
      , parser = return 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 Names = do
    tyDef <- inputs @TopInfo (view (replModInfo . miTydefs))
    ctx <- inputs @TopInfo (view (replModInfo . miTys))
    info $
      vcat (map pretty' (M.assocs tyDef))
        $+$ vcat (map showFn (Ctx.assocs ctx))
   where
    showFn (QName _ x, ty) = hsep [pretty' x, text ":", pretty' ty]
  
  ------------------------------------------------------------
  -- nop
  
  nopCmd :: REPLCommand 'CNop
  nopCmd =
    REPLCommand
      { name = "nop"
      , helpcmd = ""
      , shortHelp = "No-op, e.g. if the user just enters a comment"
      , category = Dev
      , cmdtype = BuiltIn
      , action = handleNop
      , parser = Nop <$ (sc <* eof)
      }
  
  handleNop :: REPLExpr 'CNop -> Sem r ()
  handleNop Nop = pure ()
  
  ------------------------------------------------------------
  -- :parse
  
  parseCmd :: REPLCommand 'CParse
  parseCmd =
    REPLCommand
      { name = "parse"
      , helpcmd = ":parse <expr>"
      , shortHelp = "Show the parsed AST"
      , category = Dev
      , cmdtype = ColonCmd
      , action = handleParse
      , parser = Parse <$> term
      }
  
  handleParse :: Member (Output (Message ())) r => REPLExpr 'CParse -> Sem r ()
  handleParse (Parse t) = info (text (show t))
  
  ------------------------------------------------------------
  -- :pretty
  
  prettyCmd :: REPLCommand 'CPretty
  prettyCmd =
    REPLCommand
      { name = "pretty"
      , helpcmd = ":pretty <expr>"
      , shortHelp = "Pretty-print a term"
      , category = Dev
      , cmdtype = ColonCmd
      , action = handlePretty
      , parser = Pretty <$> term
      }
  
  handlePretty :: Members '[LFresh, Output (Message ())] r => REPLExpr 'CPretty -> Sem r ()
  handlePretty (Pretty t) = info $ pretty' t
  
  ------------------------------------------------------------
  -- :print
  
  printCmd :: REPLCommand 'CPrint
  printCmd =
    REPLCommand
      { name = "print"
      , helpcmd = ":print <expr>"
      , shortHelp = "Print a string without the double quotes, interpreting special characters"
      , category = User
      , cmdtype = ColonCmd
      , action = handlePrint
      , parser = Print <$> term
      }
  
  handlePrint :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()
  handlePrint (Print t) = do
    at <- inputToState . typecheckTop $ checkTop t (toPolyType TyString)
    v <- mapError EvalErr . evalTerm False $ at
    info $ text (vlist vchar v)
  
  ------------------------------------------------------------
  -- :table
  
  tableCmd :: REPLCommand 'CTable
  tableCmd =
    REPLCommand
      { name = "table"
      , helpcmd = ":table <expr>"
      , shortHelp = "Print a formatted table for a list or function"
      , category = User
      , cmdtype = ColonCmd
      , action = handleTable
      , parser = Table <$> parseTermOrOp
      }
  
  handleTable :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CTable -> Sem r ()
  handleTable (Table t) = do
    (at, ty) <- inputToState . typecheckTop $ inferTop1 t
    v <- mapError EvalErr . evalTerm False $ at
  
    tydefs <- use @TopInfo (replModInfo . to allTydefs)
    info $ runInputConst tydefs $ formatTableFor ty v >>= text
  
  -- | The max number of rows to show in the output of :table.
  maxFunTableRows :: Int
  maxFunTableRows = 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 (tyA :->: tyB) = (tyA :*: tyAs, tyRes)
   where
    (tyAs, tyRes) = uncurryTy tyB
  uncurryTy ty = (TyUnit, ty)
  
  -- | Evaluate the application of a curried function to an uncurried
  --   input.
  evalCurried :: Members EvalEffects r => Type -> Value -> Type -> Value -> Sem r Value
  evalCurried (_ :->: tyB) f (_ :*: tyY) v = do
    let (v1, v2) = vpair id id v
    f' <- evalApp f [v1]
    evalCurried tyB f' tyY v2
  evalCurried _ v _ _ = return v
  
  formatTableFor ::
    Members (LFresh ': Input TyDefCtx ': EvalEffects) r =>
    PolyType ->
    Value ->
    Sem r String
  formatTableFor (Forall bnd) v = lunbind bnd $ \(vars, ty) ->
    case vars of
      [] -> case ty of
        TyList ety -> do
          byRows <- mapM (formatCols TopLevel ety) . vlist id $ v
          return $ renderTable byRows
        (_ :->: _) -> do
          let (tyInputs, tyRes) = uncurryTy ty
              vs = take (maxFunTableRows + 1) $ enumerateType tyInputs
              (tyInputs', stripV) = stripFinalUnit tyInputs
          results <- mapM (evalCurried ty v tyInputs) vs
          byRows <-
            mapM
              (formatCols TopLevel (tyInputs' :*: tyRes))
              (zipWith (curry (pairv id id)) (take maxFunTableRows (map stripV vs)) results)
          return $ renderTable (byRows ++ [[(B.left, "...")] | length vs == maxFunTableRows + 1])
        _otherTy -> do
          tyStr <- prettyStr ty
          return $ "Don't know how to make a table for type " ++ tyStr
      _vars -> return "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 (tA :*: TyUnit) = (tA, fst . vpair id id)
  stripFinalUnit (tA :*: tB) = (tA :*: tB', pairv id id . second v' . vpair id id)
   where
    (tB', v') = stripFinalUnit tB
  stripFinalUnit ty = (ty, id)
  
  data Level = TopLevel | NestedPair | InnerLevel
    deriving (Eq, Ord, 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 l (t1 :*: t2) (vpair id id -> (v1, v2))
    | l `elem` [TopLevel, NestedPair] =
        (++) <$> formatCols NestedPair t1 v1 <*> formatCols NestedPair t2 v2
  -- Special case for String (= List Char), just print as string value
  formatCols TopLevel TyString v = formatColDefault TyString v
  -- For any other lists @ top level, print each element in a separate column
  formatCols TopLevel (TyList ety) (vlist id -> vs) =
    concat <$> mapM (formatCols InnerLevel ety) vs
  formatCols _ ty v = formatColDefault ty 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 ty v = (: []) . (alignmentForType ty,) <$> renderDoc (prettyValue ty v)
  
  alignmentForType :: Type -> B.Alignment
  alignmentForType ty | ty `elem` [TyN, TyZ, TyF, TyQ] = B.right
  alignmentForType _ = 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 = stripTrailingWS . B.render . B.hsep 2 B.top . map renderCol . transpose . pad
   where
    pad :: [[(B.Alignment, String)]] -> [[(B.Alignment, String)]]
    pad rows = map (padTo (maximum0 . map length $ rows)) rows
    padTo n = take n . (++ repeat (B.left, ""))
  
    renderCol :: [(B.Alignment, String)] -> B.Box
    renderCol [] = B.nullBox
    renderCol ((align, x) : xs) = B.vcat align . map B.text $ x : map snd xs
  
    stripTrailingWS = unlines . map stripEnd . lines
    stripEnd = reverse . dropWhile isSpace . reverse
  
  ------------------------------------------------------------
  -- :reload
  
  reloadCmd :: REPLCommand 'CReload
  reloadCmd =
    REPLCommand
      { name = "reload"
      , helpcmd = ":reload"
      , shortHelp = "Reloads the most recently loaded file"
      , category = User
      , cmdtype = ColonCmd
      , action = handleReload
      , parser = return Reload
      }
  
  handleReload ::
    Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': Embed IO ': EvalEffects) r =>
    REPLExpr 'CReload ->
    Sem r ()
  handleReload Reload = do
    file <- use lastFile
    case file of
      Nothing -> info "No file to reload."
      Just f -> void (handleLoad f)
  
  ------------------------------------------------------------
  -- :defn
  
  showDefnCmd :: REPLCommand 'CShowDefn
  showDefnCmd =
    REPLCommand
      { name = "defn"
      , helpcmd = ":defn <var>"
      , shortHelp = "Show a variable's definition"
      , category = User
      , cmdtype = ColonCmd
      , action = inputToState @TopInfo . handleShowDefn
      , parser = ShowDefn <$> (sc *> ident)
      }
  
  handleShowDefn ::
    Members '[Input TopInfo, LFresh, Output (Message ())] r =>
    REPLExpr 'CShowDefn ->
    Sem r ()
  handleShowDefn (ShowDefn x) = do
    let name2s = name2String x
    defns <- inputs @TopInfo (view (replModInfo . miTermdefs))
    tyDefns <- inputs @TopInfo (view (replModInfo . miTydefs))
  
    let xdefs = Ctx.lookupAll' (coerce x) defns
        mtydef = M.lookup name2s tyDefns
  
    info $ do
      let ds = map (pretty' . snd) xdefs ++ maybe [] (pure . pretty' . (name2s,)) mtydef
      case ds of
        [] -> text "No definition for" <+> pretty' x
        _nonEmptyList -> vcat ds
  
  ------------------------------------------------------------
  -- :test
  
  testPropCmd :: REPLCommand 'CTestProp
  testPropCmd =
    REPLCommand
      { name = "test"
      , helpcmd = ":test <property>"
      , shortHelp = "Test a property using random examples"
      , category = User
      , cmdtype = ColonCmd
      , action = handleTest
      , parser = TestProp <$> term
      }
  
  handleTest ::
    Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r =>
    REPLExpr 'CTestProp ->
    Sem r ()
  handleTest (TestProp t) = do
    at <- inputToState . typecheckTop $ checkProperty t
    tydefs <- use @TopInfo (replModInfo . to allTydefs)
    inputToState . inputTopEnv $ do
      r <- runTest 100 at -- XXX make configurable
      info $ runInputConst tydefs . runReader initPA $ indent 2 . nest 2 $ "-" <+> prettyTestResult at r
  
  ------------------------------------------------------------
  -- :type
  
  typeCheckCmd :: REPLCommand 'CTypeCheck
  typeCheckCmd =
    REPLCommand
      { name = "type"
      , helpcmd = ":type <term>"
      , shortHelp = "Typecheck a term"
      , category = Dev
      , cmdtype = ColonCmd
      , action = inputToState @TopInfo . handleTypeCheck
      , parser = TypeCheck <$> parseTermOrOp
      }
  
  maxInferredTypes :: Int
  maxInferredTypes = 16
  
  handleTypeCheck ::
    Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
    REPLExpr 'CTypeCheck ->
    Sem r ()
  handleTypeCheck (TypeCheck t) = do
    asigs <- typecheckTop $ inferTop maxInferredTypes t
    sigs <- runFresh . mapInput (view (replModInfo . miTydefs)) $ thin $ NE.map snd asigs
    let (toShow, extra) = NE.splitAt 8 sigs
    when (length sigs > 1) $ info "This expression has multiple possible types.  Some examples:"
    info $
      vcat $
        map (\sig -> pretty' t <+> text ":" <+> pretty' sig) toShow
          ++ ["..." | not (P.null 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 =
    (try term <?> "expression")
      <|> (parseNakedOp <?> "operator")
  
  parseNakedOp :: Parser Term
  parseNakedOp = TPrim <$> parseNakedOpPrim
  
  parseNakedOpPrim :: Parser Prim
  parseNakedOpPrim = sc *> choice (map mkOpParser (concat opTable))
   where
    mkOpParser :: OpInfo -> Parser Prim
    mkOpParser (OpInfo (UOpF _ op) syns _) = choice (map ((PrimUOp op <$) . reservedOp) syns)
    mkOpParser (OpInfo (BOpF _ op) syns _) = choice (map ((PrimBOp op <$) . reservedOp) syns)
  