{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE StandaloneDeriving #-}
module Disco.Interactive.Commands
( dispatch,
discoCommands,
handleLoad,
loadFile,
parseLine
) where
import Control.Arrow ((&&&))
import Control.Lens (to, view, (%~), (.~), (?~),
(^.))
import Control.Monad.Except
import Data.Char (isSpace)
import Data.Coerce
import Data.List (find, isPrefixOf, sortBy)
import Data.Map ((!))
import qualified Data.Map as M
import Data.Typeable
import Prelude as P
import System.FilePath (splitFileName)
import Text.Megaparsec hiding (State, runParser)
import qualified Text.Megaparsec.Char as C
import Unbound.Generics.LocallyNameless (Name, name2String,
string2Name)
import Disco.Effects.Input
import Disco.Effects.LFresh
import Disco.Effects.State
import Polysemy
import Polysemy.Error hiding (try)
import Polysemy.Output
import Polysemy.Reader
import Data.Maybe (maybeToList)
import Disco.AST.Surface
import Disco.AST.Typed
import Disco.Compile
import Disco.Context as Ctx
import Disco.Desugar
import Disco.Doc
import Disco.Error
import Disco.Eval
import Disco.Extensions
import Disco.Interpret.CESK
import Disco.Messages
import Disco.Module
import Disco.Names
import Disco.Parser (Parser, ident, reservedOp,
runParser, sc, symbol, term,
wholeModule, withExts)
import Disco.Pretty hiding (empty, (<>))
import qualified Disco.Pretty as Pretty
import Disco.Syntax.Operators
import Disco.Syntax.Prims (Prim (PrimBOp, PrimUOp),
toPrim)
import Disco.Typecheck
import Disco.Typecheck.Erase
import Disco.Types (pattern TyString, toPolyType)
import Disco.Value
data REPLExpr :: CmdTag -> * where
TypeCheck :: Term -> REPLExpr 'CTypeCheck
Eval :: Module -> REPLExpr 'CEval
TestProp :: Term -> REPLExpr 'CTestProp
ShowDefn :: Name Term -> REPLExpr 'CShowDefn
Parse :: Term -> REPLExpr 'CParse
Pretty :: Term -> REPLExpr 'CPretty
Print :: Term -> REPLExpr 'CPrint
Ann :: Term -> REPLExpr 'CAnn
Desugar :: Term -> REPLExpr 'CDesugar
Compile :: Term -> REPLExpr 'CCompile
Load :: FilePath -> REPLExpr 'CLoad
Reload :: REPLExpr 'CReload
Doc :: DocInput -> REPLExpr 'CDoc
Nop :: REPLExpr 'CNop
Help :: REPLExpr 'CHelp
Names :: REPLExpr 'CNames
deriving instance Show (REPLExpr c)
data SomeREPLExpr where
SomeREPL :: Typeable c => REPLExpr c -> SomeREPLExpr
data REPLCommandCategory
=
User
|
Dev
deriving (REPLCommandCategory -> REPLCommandCategory -> Bool
(REPLCommandCategory -> REPLCommandCategory -> Bool)
-> (REPLCommandCategory -> REPLCommandCategory -> Bool)
-> Eq REPLCommandCategory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: REPLCommandCategory -> REPLCommandCategory -> Bool
$c/= :: REPLCommandCategory -> REPLCommandCategory -> Bool
== :: REPLCommandCategory -> REPLCommandCategory -> Bool
$c== :: REPLCommandCategory -> REPLCommandCategory -> Bool
Eq, Int -> REPLCommandCategory -> ShowS
[REPLCommandCategory] -> ShowS
REPLCommandCategory -> String
(Int -> REPLCommandCategory -> ShowS)
-> (REPLCommandCategory -> String)
-> ([REPLCommandCategory] -> ShowS)
-> Show REPLCommandCategory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [REPLCommandCategory] -> ShowS
$cshowList :: [REPLCommandCategory] -> ShowS
show :: REPLCommandCategory -> String
$cshow :: REPLCommandCategory -> String
showsPrec :: Int -> REPLCommandCategory -> ShowS
$cshowsPrec :: Int -> REPLCommandCategory -> ShowS
Show)
data REPLCommandType
=
BuiltIn
|
ColonCmd
deriving (REPLCommandType -> REPLCommandType -> Bool
(REPLCommandType -> REPLCommandType -> Bool)
-> (REPLCommandType -> REPLCommandType -> Bool)
-> Eq REPLCommandType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: REPLCommandType -> REPLCommandType -> Bool
$c/= :: REPLCommandType -> REPLCommandType -> Bool
== :: REPLCommandType -> REPLCommandType -> Bool
$c== :: REPLCommandType -> REPLCommandType -> Bool
Eq, Int -> REPLCommandType -> ShowS
[REPLCommandType] -> ShowS
REPLCommandType -> String
(Int -> REPLCommandType -> ShowS)
-> (REPLCommandType -> String)
-> ([REPLCommandType] -> ShowS)
-> Show REPLCommandType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [REPLCommandType] -> ShowS
$cshowList :: [REPLCommandType] -> ShowS
show :: REPLCommandType -> String
$cshow :: REPLCommandType -> String
showsPrec :: Int -> REPLCommandType -> ShowS
$cshowsPrec :: Int -> REPLCommandType -> ShowS
Show)
data CmdTag
= CTypeCheck
| CEval
| CShowDefn
| CParse
| CPretty
| CPrint
| CAnn
| CDesugar
| CCompile
| CLoad
| CReload
| CDoc
| CNop
| CHelp
| CNames
| CTestProp
deriving (Int -> CmdTag -> ShowS
[CmdTag] -> ShowS
CmdTag -> String
(Int -> CmdTag -> ShowS)
-> (CmdTag -> String) -> ([CmdTag] -> ShowS) -> Show CmdTag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CmdTag] -> ShowS
$cshowList :: [CmdTag] -> ShowS
show :: CmdTag -> String
$cshow :: CmdTag -> String
showsPrec :: Int -> CmdTag -> ShowS
$cshowsPrec :: Int -> CmdTag -> ShowS
Show, CmdTag -> CmdTag -> Bool
(CmdTag -> CmdTag -> Bool)
-> (CmdTag -> CmdTag -> Bool) -> Eq CmdTag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CmdTag -> CmdTag -> Bool
$c/= :: CmdTag -> CmdTag -> Bool
== :: CmdTag -> CmdTag -> Bool
$c== :: CmdTag -> CmdTag -> Bool
Eq, Typeable)
data REPLCommand (c :: CmdTag) = REPLCommand
{
REPLCommand c -> String
name :: String,
REPLCommand c -> String
helpcmd :: String,
REPLCommand c -> String
shortHelp :: String,
REPLCommand c -> REPLCommandCategory
category :: REPLCommandCategory,
REPLCommand c -> REPLCommandType
cmdtype :: REPLCommandType,
REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action :: REPLExpr c -> (forall r. Members DiscoEffects r => Sem r ()),
REPLCommand c -> Parser (REPLExpr c)
parser :: Parser (REPLExpr c)
}
data SomeREPLCommand where
SomeCmd :: Typeable c => REPLCommand c -> SomeREPLCommand
type REPLCommands = [SomeREPLCommand]
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)
dispatch :: Members DiscoEffects r => REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch :: REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch [] SomeREPLExpr
_ = () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
dispatch (SomeCmd REPLCommand c
c : REPLCommands
cs) r :: SomeREPLExpr
r@(SomeREPL REPLExpr c
e) = case REPLExpr c -> Maybe (REPLExpr c)
forall k (a :: k) (b :: k) (c :: k -> *).
(Typeable a, Typeable b) =>
c a -> Maybe (c b)
gcast REPLExpr c
e of
Just REPLExpr c
e' -> Sem (Error DiscoError : r) () -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem (Error DiscoError : r) () -> Sem r ()
outputDiscoErrors (Sem (Error DiscoError : r) () -> Sem r ())
-> Sem (Error DiscoError : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
forall (c :: CmdTag).
REPLCommand c
-> REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action REPLCommand c
c REPLExpr c
e'
Maybe (REPLExpr c)
Nothing -> REPLCommands -> SomeREPLExpr -> Sem r ()
forall (r :: EffectRow).
Members DiscoEffects r =>
REPLCommands -> SomeREPLExpr -> Sem r ()
dispatch REPLCommands
cs SomeREPLExpr
r
discoCommands :: REPLCommands
discoCommands :: REPLCommands
discoCommands =
[ REPLCommand 'CAnn -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CAnn
annCmd,
REPLCommand 'CCompile -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CCompile
compileCmd,
REPLCommand 'CDesugar -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CDesugar
desugarCmd,
REPLCommand 'CDoc -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CDoc
docCmd,
REPLCommand 'CEval -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CEval
evalCmd,
REPLCommand 'CHelp -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CHelp
helpCmd,
REPLCommand 'CLoad -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CLoad
loadCmd,
REPLCommand 'CNames -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CNames
namesCmd,
REPLCommand 'CNop -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CNop
nopCmd,
REPLCommand 'CParse -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CParse
parseCmd,
REPLCommand 'CPretty -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CPretty
prettyCmd,
REPLCommand 'CPrint -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CPrint
printCmd,
REPLCommand 'CReload -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CReload
reloadCmd,
REPLCommand 'CShowDefn -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CShowDefn
showDefnCmd,
REPLCommand 'CTypeCheck -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTypeCheck
typeCheckCmd,
REPLCommand 'CTestProp -> SomeREPLCommand
forall (c :: CmdTag).
Typeable c =>
REPLCommand c -> SomeREPLCommand
SomeCmd REPLCommand 'CTestProp
testPropCmd
]
builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
builtinCommandParser :: REPLCommands -> Parser SomeREPLExpr
builtinCommandParser =
(SomeREPLCommand -> Parser SomeREPLExpr -> Parser SomeREPLExpr)
-> Parser SomeREPLExpr -> REPLCommands -> Parser SomeREPLExpr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr)
-> (SomeREPLCommand -> Parser SomeREPLExpr)
-> SomeREPLCommand
-> Parser SomeREPLExpr
-> Parser SomeREPLExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(SomeCmd REPLCommand c
rc) -> REPLExpr c -> SomeREPLExpr
forall (c :: CmdTag). Typeable c => REPLExpr c -> SomeREPLExpr
SomeREPL (REPLExpr c -> SomeREPLExpr)
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
-> Parser SomeREPLExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (REPLCommand c
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc))) Parser SomeREPLExpr
forall (f :: * -> *) a. Alternative f => f a
empty
(REPLCommands -> Parser SomeREPLExpr)
-> (REPLCommands -> REPLCommands)
-> REPLCommands
-> Parser SomeREPLExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLCommandType -> REPLCommands -> REPLCommands
byCmdType REPLCommandType
BuiltIn
commandParser :: REPLCommands -> Parser SomeREPLExpr
commandParser :: REPLCommands -> Parser SomeREPLExpr
commandParser REPLCommands
allCommands =
(String -> Parser String
symbol String
":" Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.lowerChar) Parser String
-> (String -> Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= REPLCommands -> String -> Parser SomeREPLExpr
parseCommandArgs REPLCommands
allCommands
parseCommandArgs :: REPLCommands -> String -> Parser SomeREPLExpr
parseCommandArgs :: REPLCommands -> String -> Parser SomeREPLExpr
parseCommandArgs REPLCommands
allCommands String
cmd = Parser SomeREPLExpr
-> ((String, Parser SomeREPLExpr) -> Parser SomeREPLExpr)
-> Maybe (String, Parser SomeREPLExpr)
-> Parser SomeREPLExpr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Parser SomeREPLExpr
badCmd (String, Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b. (a, b) -> b
snd (Maybe (String, Parser SomeREPLExpr) -> Parser SomeREPLExpr)
-> Maybe (String, Parser SomeREPLExpr) -> Parser SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ ((String, Parser SomeREPLExpr) -> Bool)
-> [(String, Parser SomeREPLExpr)]
-> Maybe (String, Parser SomeREPLExpr)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String
cmd String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf`) (String -> Bool)
-> ((String, Parser SomeREPLExpr) -> String)
-> (String, Parser SomeREPLExpr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Parser SomeREPLExpr) -> String
forall a b. (a, b) -> a
fst) [(String, Parser SomeREPLExpr)]
parsers
where
badCmd :: Parser SomeREPLExpr
badCmd = String -> Parser SomeREPLExpr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser SomeREPLExpr) -> String -> Parser SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ String
"Command \":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
cmd String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" is unrecognized."
parsers :: [(String, Parser SomeREPLExpr)]
parsers =
(SomeREPLCommand -> (String, Parser SomeREPLExpr))
-> REPLCommands -> [(String, Parser SomeREPLExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
rc) -> (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
name REPLCommand c
rc, REPLExpr c -> SomeREPLExpr
forall (c :: CmdTag). Typeable c => REPLExpr c -> SomeREPLExpr
SomeREPL (REPLExpr c -> SomeREPLExpr)
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
-> Parser SomeREPLExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> REPLCommand c
-> StateT ParserState (Parsec DiscoParseError String) (REPLExpr c)
forall (c :: CmdTag). REPLCommand c -> Parser (REPLExpr c)
parser REPLCommand c
rc)) (REPLCommands -> [(String, Parser SomeREPLExpr)])
-> REPLCommands -> [(String, Parser SomeREPLExpr)]
forall a b. (a -> b) -> a -> b
$
REPLCommandType -> REPLCommands -> REPLCommands
byCmdType REPLCommandType
ColonCmd REPLCommands
allCommands
fileParser :: Parser FilePath
fileParser :: Parser String
fileParser = StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
C.spaceChar Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ((Token String -> Bool)
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace))
lineParser :: REPLCommands -> Parser SomeREPLExpr
lineParser :: REPLCommands -> Parser SomeREPLExpr
lineParser REPLCommands
allCommands =
REPLCommands -> Parser SomeREPLExpr
builtinCommandParser REPLCommands
allCommands
Parser SomeREPLExpr -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> REPLCommands -> Parser SomeREPLExpr
commandParser REPLCommands
allCommands
parseLine :: REPLCommands -> ExtSet -> String -> Either String SomeREPLExpr
parseLine :: REPLCommands -> ExtSet -> String -> Either String SomeREPLExpr
parseLine REPLCommands
allCommands ExtSet
exts String
s =
case Parser SomeREPLExpr
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) SomeREPLExpr
forall a.
Parser a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
runParser (ExtSet -> Parser SomeREPLExpr -> Parser SomeREPLExpr
forall a. ExtSet -> Parser a -> Parser a
withExts ExtSet
exts (REPLCommands -> Parser SomeREPLExpr
lineParser REPLCommands
allCommands)) String
"" String
s of
Left ParseErrorBundle String DiscoParseError
e -> String -> Either String SomeREPLExpr
forall a b. a -> Either a b
Left (String -> Either String SomeREPLExpr)
-> String -> Either String SomeREPLExpr
forall a b. (a -> b) -> a -> b
$ ParseErrorBundle String DiscoParseError -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String DiscoParseError
e
Right SomeREPLExpr
l -> SomeREPLExpr -> Either String SomeREPLExpr
forall a b. b -> Either a b
Right SomeREPLExpr
l
annCmd :: REPLCommand 'CAnn
annCmd :: REPLCommand 'CAnn
annCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"ann",
helpcmd :: String
helpcmd = String
":ann",
shortHelp :: String
shortHelp = String
"Show type-annotated typechecked term",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CAnn
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CAnn
x -> forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CAnn -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CAnn
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CAnn -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Error DiscoError, Input TopInfo, Output Message] r =>
REPLExpr 'CAnn -> Sem r ()
handleAnn (REPLExpr 'CAnn -> Sem r ()) -> REPLExpr 'CAnn -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CAnn
x,
parser :: Parser (REPLExpr 'CAnn)
parser = Term -> REPLExpr 'CAnn
Ann (Term -> REPLExpr 'CAnn)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CAnn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handleAnn ::
Members '[Error DiscoError, Input TopInfo, Output Message] r =>
REPLExpr 'CAnn ->
Sem r ()
handleAnn :: REPLExpr 'CAnn -> Sem r ()
handleAnn (Ann Term
t) = do
(ATerm
at, PolyType
_) <- Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall (r :: EffectRow) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop (Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType))
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
forall (r :: EffectRow).
Members
'[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
Fresh]
r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
ATerm -> Sem r ()
forall (r :: EffectRow) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
infoPretty ATerm
at
compileCmd :: REPLCommand 'CCompile
compileCmd :: REPLCommand 'CCompile
compileCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"compile",
helpcmd :: String
helpcmd = String
":compile",
shortHelp :: String
shortHelp = String
"Show a compiled term",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CCompile
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CCompile
x -> forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CCompile -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CCompile
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CCompile -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Error DiscoError, Input TopInfo, Output Message] r =>
REPLExpr 'CCompile -> Sem r ()
handleCompile (REPLExpr 'CCompile -> Sem r ()) -> REPLExpr 'CCompile -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CCompile
x,
parser :: Parser (REPLExpr 'CCompile)
parser = Term -> REPLExpr 'CCompile
Compile (Term -> REPLExpr 'CCompile)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CCompile)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handleCompile ::
Members '[Error DiscoError, Input TopInfo, Output Message] r =>
REPLExpr 'CCompile ->
Sem r ()
handleCompile :: REPLExpr 'CCompile -> Sem r ()
handleCompile (Compile Term
t) = do
(ATerm
at, PolyType
_) <- Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall (r :: EffectRow) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop (Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType))
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
forall (r :: EffectRow).
Members
'[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
Fresh]
r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
Core -> Sem r ()
forall (r :: EffectRow) t.
(Member (Output Message) r, Pretty t) =>
t -> Sem r ()
infoPretty (Core -> Sem r ()) -> (ATerm -> Core) -> ATerm -> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Core
compileTerm (ATerm -> Sem r ()) -> ATerm -> Sem r ()
forall a b. (a -> b) -> a -> b
$ ATerm
at
desugarCmd :: REPLCommand 'CDesugar
desugarCmd :: REPLCommand 'CDesugar
desugarCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"desugar",
helpcmd :: String
helpcmd = String
":desugar",
shortHelp :: String
shortHelp = String
"Show a desugared term",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CDesugar
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CDesugar
x -> forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CDesugar -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CDesugar
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CDesugar -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CDesugar -> Sem r ()
handleDesugar (REPLExpr 'CDesugar -> Sem r ()) -> REPLExpr 'CDesugar -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CDesugar
x,
parser :: Parser (REPLExpr 'CDesugar)
parser = Term -> REPLExpr 'CDesugar
Desugar (Term -> REPLExpr 'CDesugar)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CDesugar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handleDesugar ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CDesugar ->
Sem r ()
handleDesugar :: REPLExpr 'CDesugar -> Sem r ()
handleDesugar (Desugar Term
t) = do
(ATerm
at, PolyType
_) <- Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall (r :: EffectRow) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop (Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType))
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
forall (r :: EffectRow).
Members
'[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
Fresh]
r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (Term -> Sem r Doc) -> (ATerm -> Term) -> ATerm -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTerm -> Term
eraseDTerm (DTerm -> Term) -> (ATerm -> DTerm) -> ATerm -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem '[Fresh] DTerm -> DTerm
forall a. Sem '[Fresh] a -> a
runDesugar (Sem '[Fresh] DTerm -> DTerm)
-> (ATerm -> Sem '[Fresh] DTerm) -> ATerm -> DTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Sem '[Fresh] DTerm
forall (r :: EffectRow). Member Fresh r => ATerm -> Sem r DTerm
desugarTerm (ATerm -> Sem r Doc) -> ATerm -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ ATerm
at
docCmd :: REPLCommand 'CDoc
docCmd :: REPLCommand 'CDoc
docCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"doc",
helpcmd :: String
helpcmd = String
":doc <term>",
shortHelp :: String
shortHelp = String
"Show documentation",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CDoc
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CDoc
x -> forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CDoc -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CDoc
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CDoc -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CDoc -> Sem r ()
handleDoc (REPLExpr 'CDoc -> Sem r ()) -> REPLExpr 'CDoc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CDoc
x,
parser :: Parser (REPLExpr 'CDoc)
parser = DocInput -> REPLExpr 'CDoc
Doc (DocInput -> REPLExpr 'CDoc)
-> StateT ParserState (Parsec DiscoParseError String) DocInput
-> Parser (REPLExpr 'CDoc)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) DocInput
parseDoc
}
data DocInput = DocTerm Term | DocPrim Prim | DocOther String
deriving (Int -> DocInput -> ShowS
[DocInput] -> ShowS
DocInput -> String
(Int -> DocInput -> ShowS)
-> (DocInput -> String) -> ([DocInput] -> ShowS) -> Show DocInput
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DocInput] -> ShowS
$cshowList :: [DocInput] -> ShowS
show :: DocInput -> String
$cshow :: DocInput -> String
showsPrec :: Int -> DocInput -> ShowS
$cshowsPrec :: Int -> DocInput -> ShowS
Show)
parseDoc :: Parser DocInput
parseDoc :: StateT ParserState (Parsec DiscoParseError String) DocInput
parseDoc =
(Term -> DocInput
DocTerm (Term -> DocInput)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Term
term)
StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Prim -> DocInput
DocPrim (Prim -> DocInput)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) Prim
parseNakedOpPrim StateT ParserState (Parsec DiscoParseError String) Prim
-> String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator"))
StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> DocInput
DocOther (String -> DocInput)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) DocInput
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
sc Parser () -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Token s -> m (Token s)
anySingleBut Char
Token String
' ')))
handleDoc ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CDoc ->
Sem r ()
handleDoc :: REPLExpr 'CDoc -> Sem r ()
handleDoc (Doc (DocTerm (TBool Bool
_))) = Sem r ()
forall (r :: EffectRow). Members '[Output Message] r => Sem r ()
handleDocBool
handleDoc (Doc (DocTerm (TPrim Prim
p))) = Prim -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim -> Sem r ()
handleDocPrim Prim
p
handleDoc (Doc (DocTerm (TVar Name Term
x))) = Name Term -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Name Term -> Sem r ()
handleDocVar Name Term
x
handleDoc (Doc (DocTerm Term
_)) =
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
err Sem r Doc
"Can't display documentation for an expression. Try asking about a function, operator, or type name."
handleDoc (Doc (DocPrim Prim
p)) = Prim -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim -> Sem r ()
handleDocPrim Prim
p
handleDoc (Doc (DocOther String
s)) = String -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
String -> Sem r ()
handleDocOther String
s
handleDocBool :: Members '[Output Message] r => Sem r ()
handleDocBool :: Sem r ()
handleDocBool =
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$
Sem r Doc
"true and false (also written True and False) are the two possible values of type Boolean."
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
"bool"
handleDocVar ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Name Term ->
Sem r ()
handleDocVar :: Name Term -> Sem r ()
handleDocVar Name Term
x = do
TyCtx
replCtx <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting TyCtx TopInfo TyCtx -> TopInfo -> TyCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyCtx ModuleInfo)
-> TopInfo -> Const TyCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyCtx ModuleInfo)
-> TopInfo -> Const TyCtx TopInfo)
-> ((TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo)
-> Getting TyCtx TopInfo TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo
Lens' ModuleInfo TyCtx
miTys))
TyDefCtx
replTydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting TyDefCtx TopInfo TyDefCtx -> TopInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo)
-> ((TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> Getting TyDefCtx TopInfo TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs))
Ctx Term [DocThing]
replDocs <- (TopInfo -> Ctx Term [DocThing]) -> Sem r (Ctx Term [DocThing])
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting (Ctx Term [DocThing]) TopInfo (Ctx Term [DocThing])
-> TopInfo -> Ctx Term [DocThing]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> TopInfo -> Const (Ctx Term [DocThing]) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> TopInfo -> Const (Ctx Term [DocThing]) TopInfo)
-> ((Ctx Term [DocThing]
-> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
-> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> Getting (Ctx Term [DocThing]) TopInfo (Ctx Term [DocThing])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ctx Term [DocThing]
-> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
-> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo
Lens' ModuleInfo (Ctx Term [DocThing])
miDocs))
TyCtx
importCtx <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([TyCtx] -> TyCtx
forall a b. [Ctx a b] -> Ctx a b
joinCtxs ([TyCtx] -> TyCtx) -> (TopInfo -> [TyCtx]) -> TopInfo -> TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyCtx) -> [ModuleInfo] -> [TyCtx]
forall a b. (a -> b) -> [a] -> [b]
map (((TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo)
-> ModuleInfo -> TyCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo
Lens' ModuleInfo TyCtx
miTys) ([ModuleInfo] -> [TyCtx])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [TyCtx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
M.elems (Map ModuleName ModuleInfo -> [ModuleInfo])
-> (TopInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> [ModuleInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
(Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
-> TopInfo -> Map ModuleName ModuleInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap)
TyDefCtx
importTydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([TyDefCtx] -> TyDefCtx
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([TyDefCtx] -> TyDefCtx)
-> (TopInfo -> [TyDefCtx]) -> TopInfo -> TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyDefCtx) -> [ModuleInfo] -> [TyDefCtx]
forall a b. (a -> b) -> [a] -> [b]
map (((TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> ModuleInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs) ([ModuleInfo] -> [TyDefCtx])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [TyDefCtx]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
M.elems (Map ModuleName ModuleInfo -> [ModuleInfo])
-> (TopInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> [ModuleInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
(Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
-> TopInfo -> Map ModuleName ModuleInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap)
Ctx Term [DocThing]
importDocs <- (TopInfo -> Ctx Term [DocThing]) -> Sem r (Ctx Term [DocThing])
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo ([Ctx Term [DocThing]] -> Ctx Term [DocThing]
forall a b. [Ctx a b] -> Ctx a b
joinCtxs ([Ctx Term [DocThing]] -> Ctx Term [DocThing])
-> (TopInfo -> [Ctx Term [DocThing]])
-> TopInfo
-> Ctx Term [DocThing]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> Ctx Term [DocThing])
-> [ModuleInfo] -> [Ctx Term [DocThing]]
forall a b. (a -> b) -> [a] -> [b]
map (((Ctx Term [DocThing]
-> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
-> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo)
-> ModuleInfo -> Ctx Term [DocThing]
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view (Ctx Term [DocThing]
-> Const (Ctx Term [DocThing]) (Ctx Term [DocThing]))
-> ModuleInfo -> Const (Ctx Term [DocThing]) ModuleInfo
Lens' ModuleInfo (Ctx Term [DocThing])
miDocs) ([ModuleInfo] -> [Ctx Term [DocThing]])
-> (TopInfo -> [ModuleInfo]) -> TopInfo -> [Ctx Term [DocThing]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map ModuleName ModuleInfo -> [ModuleInfo]
forall k a. Map k a -> [a]
M.elems (Map ModuleName ModuleInfo -> [ModuleInfo])
-> (TopInfo -> Map ModuleName ModuleInfo)
-> TopInfo
-> [ModuleInfo]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
(Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
-> TopInfo -> Map ModuleName ModuleInfo
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting
(Map ModuleName ModuleInfo) TopInfo (Map ModuleName ModuleInfo)
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap)
let ctx :: TyCtx
ctx = TyCtx
replCtx TyCtx -> TyCtx -> TyCtx
forall a b. Ctx a b -> Ctx a b -> Ctx a b
`joinCtx` TyCtx
importCtx
tydefs :: TyDefCtx
tydefs = TyDefCtx
importTydefs TyDefCtx -> TyDefCtx -> TyDefCtx
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` TyDefCtx
replTydefs
docs :: Ctx Term [DocThing]
docs = Ctx Term [DocThing]
replDocs Ctx Term [DocThing] -> Ctx Term [DocThing] -> Ctx Term [DocThing]
forall a b. Ctx a b -> Ctx a b -> Ctx a b
`joinCtx` Ctx Term [DocThing]
importDocs
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
debug (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Sem r Doc)
-> (Ctx Term [DocThing] -> String)
-> Ctx Term [DocThing]
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx Term [DocThing] -> String
forall a. Show a => a -> String
show (Ctx Term [DocThing] -> Sem r Doc)
-> Ctx Term [DocThing] -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Ctx Term [DocThing]
docs
case (Name Term -> TyCtx -> [(QName Term, PolyType)]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' Name Term
x TyCtx
ctx, String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Name Term -> String
forall a. Name a -> String
name2String Name Term
x) TyDefCtx
tydefs) of
([], Maybe TyDefBody
Nothing) ->
case String -> [Prim]
toPrim (Name Term -> String
forall a. Name a -> String
name2String Name Term
x) of
(Prim
prim:[Prim]
_) -> Prim -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim -> Sem r ()
handleDocPrim Prim
prim
[Prim]
_ -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
err (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"No documentation found for '" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Name Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name Term
x Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"'."
([(QName Term, PolyType)]
binds, Maybe TyDefBody
def) ->
(Either (QName Term, PolyType) TyDefBody -> Sem r ())
-> [Either (QName Term, PolyType) TyDefBody] -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Ctx Term [DocThing]
-> Either (QName Term, PolyType) TyDefBody -> Sem r ()
showDoc Ctx Term [DocThing]
docs) (((QName Term, PolyType) -> Either (QName Term, PolyType) TyDefBody)
-> [(QName Term, PolyType)]
-> [Either (QName Term, PolyType) TyDefBody]
forall a b. (a -> b) -> [a] -> [b]
map (QName Term, PolyType) -> Either (QName Term, PolyType) TyDefBody
forall a b. a -> Either a b
Left [(QName Term, PolyType)]
binds [Either (QName Term, PolyType) TyDefBody]
-> [Either (QName Term, PolyType) TyDefBody]
-> [Either (QName Term, PolyType) TyDefBody]
forall a. [a] -> [a] -> [a]
++ (TyDefBody -> Either (QName Term, PolyType) TyDefBody)
-> [TyDefBody] -> [Either (QName Term, PolyType) TyDefBody]
forall a b. (a -> b) -> [a] -> [b]
map TyDefBody -> Either (QName Term, PolyType) TyDefBody
forall a b. b -> Either a b
Right (Maybe TyDefBody -> [TyDefBody]
forall a. Maybe a -> [a]
maybeToList Maybe TyDefBody
def))
where
showDoc :: Ctx Term [DocThing]
-> Either (QName Term, PolyType) TyDefBody -> Sem r ()
showDoc Ctx Term [DocThing]
docMap (Left (QName Term
qn, PolyType
ty)) = Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name Term
x, Sem r Doc
":", PolyType -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' PolyType
ty]
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
case QName Term -> Ctx Term [DocThing] -> Maybe [DocThing]
forall a b. QName a -> Ctx a b -> Maybe b
Ctx.lookup' QName Term
qn Ctx Term [DocThing]
docMap of
Just (DocString [String]
ss : [DocThing]
_) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"" Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
: (String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
ss [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""])
Maybe [DocThing]
_ -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
showDoc Ctx Term [DocThing]
docMap (Right TyDefBody
tdBody) = Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$
(String, TyDefBody) -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (Name Term -> String
forall a. Name a -> String
name2String Name Term
x, TyDefBody
tdBody)
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
case Name Term -> Ctx Term [DocThing] -> [(QName Term, [DocThing])]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' Name Term
x Ctx Term [DocThing]
docMap of
((QName Term
_, DocString [String]
ss : [DocThing]
_) : [(QName Term, [DocThing])]
_) -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"" Sem r Doc -> [Sem r Doc] -> [Sem r Doc]
forall a. a -> [a] -> [a]
: (String -> Sem r Doc) -> [String] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text [String]
ss [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""])
[(QName Term, [DocThing])]
_ -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
handleDocPrim ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
Prim ->
Sem r ()
handleDocPrim :: Prim -> Sem r ()
handleDocPrim Prim
prim = do
REPLExpr 'CTypeCheck -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck (Term -> REPLExpr 'CTypeCheck
TypeCheck (Prim -> Term
TPrim Prim
prim))
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat
[ case Prim
prim of
PrimUOp UOp
u -> Bool -> Bool -> [String] -> Sem r Doc
forall (m :: * -> *).
(IsString (m Doc), Monad m) =>
Bool -> Bool -> [String] -> m Doc
describeAlts (UFixity
f UFixity -> UFixity -> Bool
forall a. Eq a => a -> a -> Bool
== UFixity
Post) (UFixity
f UFixity -> UFixity -> Bool
forall a. Eq a => a -> a -> Bool
== UFixity
Pre) [String]
syns
where
OpInfo (UOpF UFixity
f UOp
_) [String]
syns Int
_ = Map UOp OpInfo
uopMap Map UOp OpInfo -> UOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
! UOp
u
PrimBOp BOp
b -> Bool -> Bool -> [String] -> Sem r Doc
forall (m :: * -> *).
(IsString (m Doc), Monad m) =>
Bool -> Bool -> [String] -> m Doc
describeAlts Bool
True Bool
True (OpInfo -> [String]
opSyns (OpInfo -> [String]) -> OpInfo -> [String]
forall a b. (a -> b) -> a -> b
$ Map BOp OpInfo
bopMap Map BOp OpInfo -> BOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
! BOp
b)
Prim
_ -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
, case Prim
prim of
PrimUOp UOp
u -> Int -> Sem r Doc
forall (f :: * -> *) a.
(Applicative f, IsString (f Doc), Show a) =>
a -> f Doc
describePrec (UOp -> Int
uPrec UOp
u)
PrimBOp BOp
b -> Int -> Sem r Doc
forall (f :: * -> *) a.
(Applicative f, IsString (f Doc), Show a) =>
a -> f Doc
describePrec (BOp -> Int
bPrec BOp
b) Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> BFixity -> Sem r Doc
forall (m :: * -> *).
(Applicative m, IsString (m Doc)) =>
BFixity -> m Doc
describeFixity (BOp -> BFixity
assoc BOp
b)
Prim
_ -> Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
]
case (Prim -> Map Prim String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Prim
prim Map Prim String
primDoc, Prim -> Map Prim String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Prim
prim Map Prim String
primReference) of
(Maybe String
Nothing, Maybe String
Nothing) -> () -> Sem r ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Maybe String
Nothing, Just String
p) -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p
(Just String
d, Maybe String
mp) ->
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
d Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc -> (String -> Sem r Doc) -> Maybe String -> Sem r Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty (\String
p -> String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"") Maybe String
mp
where
describePrec :: a -> f Doc
describePrec a
p = f Doc
"precedence level" f Doc -> f Doc -> f Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> f Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (a -> String
forall a. Show a => a -> String
show a
p)
describeFixity :: BFixity -> m Doc
describeFixity BFixity
In = m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
describeFixity BFixity
InL = m Doc
", left associative"
describeFixity BFixity
InR = m Doc
", right associative"
describeAlts :: Bool -> Bool -> [String] -> m Doc
describeAlts Bool
_ Bool
_ [] = m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
describeAlts Bool
_ Bool
_ [String
_] = m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
describeAlts Bool
pre Bool
post (String
_:[String]
alts) = m Doc
"Alternative syntax:" m Doc -> m Doc -> m Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> m Doc -> [m Doc] -> m Doc
forall (f :: * -> *). Monad f => f Doc -> [f Doc] -> f Doc
intercalate m Doc
"," ((String -> m Doc) -> [String] -> [m Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> m Doc
showOp [String]
alts)
where
showOp :: String -> m Doc
showOp String
op = [m Doc] -> m Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hcat
[ if Bool
pre then m Doc
"~" else m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty
, String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
op
, if Bool
post then m Doc
"~" else m Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty]
mkReference :: String -> Sem r Doc
mkReference :: String -> Sem r Doc
mkReference String
p =
Sem r Doc
"https://disco-lang.readthedocs.io/en/latest/reference/" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
p Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
".html"
handleDocOther ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
String ->
Sem r ()
handleDocOther :: String -> Sem r ()
handleDocOther String
s =
case (String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
s Map String String
otherDoc, String -> Map String String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
s Map String String
otherReference) of
(Maybe String
Nothing, Maybe String
Nothing) -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc
"No documentation found for '" Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
s Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
"'."
(Maybe String
Nothing, Just String
p) -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p
(Just String
d, Maybe String
mp) ->
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
d Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc -> (String -> Sem r Doc) -> Maybe String -> Sem r Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Sem r Doc
forall (m :: * -> *). Applicative m => m Doc
Pretty.empty (\String
p -> String -> Sem r Doc
forall (r :: EffectRow). String -> Sem r Doc
mkReference String
p Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
"") Maybe String
mp
evalCmd :: REPLCommand 'CEval
evalCmd :: REPLCommand 'CEval
evalCmd = REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"eval"
, helpcmd :: String
helpcmd = String
"<code>"
, shortHelp :: String
shortHelp = String
"Evaluate a block of code"
, category :: REPLCommandCategory
category = REPLCommandCategory
User
, cmdtype :: REPLCommandType
cmdtype = REPLCommandType
BuiltIn
, action :: REPLExpr 'CEval
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CEval
x -> REPLExpr 'CEval -> Sem r ()
forall (r :: EffectRow).
Members
(Error DiscoError
: State TopInfo : Output Message : Embed IO : EvalEffects)
r =>
REPLExpr 'CEval -> Sem r ()
handleEval REPLExpr 'CEval
x
, parser :: Parser (REPLExpr 'CEval)
parser = Module -> REPLExpr 'CEval
Eval (Module -> REPLExpr 'CEval)
-> StateT ParserState (Parsec DiscoParseError String) Module
-> Parser (REPLExpr 'CEval)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LoadingMode
-> StateT ParserState (Parsec DiscoParseError String) Module
wholeModule LoadingMode
REPL
}
handleEval
:: Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r
=> REPLExpr 'CEval -> Sem r ()
handleEval :: REPLExpr 'CEval -> Sem r ()
handleEval (Eval Module
m) = do
ModuleInfo
mi <- forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) ModuleInfo -> Sem r ModuleInfo)
-> Sem (Input TopInfo : r) ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ Bool
-> Resolver
-> ModuleName
-> Module
-> Sem (Input TopInfo : r) ModuleInfo
forall (r :: EffectRow).
Members
'[State TopInfo, Output Message, Random, State Mem,
Error DiscoError, Embed IO]
r =>
Bool -> Resolver -> ModuleName -> Module -> Sem r ModuleInfo
loadParsedDiscoModule Bool
False Resolver
FromCwdOrStdlib ModuleName
REPLModule Module
m
ModuleInfo -> Sem r ()
forall (r :: EffectRow).
Members
'[Error DiscoError, State TopInfo, Random, State Mem,
Output Message]
r =>
ModuleInfo -> Sem r ()
addToREPLModule ModuleInfo
mi
[(ATerm, PolyType)]
-> ((ATerm, PolyType) -> Sem r Value) -> Sem r ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ModuleInfo
mi ModuleInfo
-> Getting [(ATerm, PolyType)] ModuleInfo [(ATerm, PolyType)]
-> [(ATerm, PolyType)]
forall s a. s -> Getting a s a -> a
^. Getting [(ATerm, PolyType)] ModuleInfo [(ATerm, PolyType)]
Lens' ModuleInfo [(ATerm, PolyType)]
miTerms) ((EvalError -> DiscoError)
-> Sem (Error EvalError : r) Value -> Sem r Value
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError EvalError -> DiscoError
EvalErr (Sem (Error EvalError : r) Value -> Sem r Value)
-> ((ATerm, PolyType) -> Sem (Error EvalError : r) Value)
-> (ATerm, PolyType)
-> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ATerm -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members
(Error EvalError : State TopInfo : Output Message : EvalEffects)
r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
True (ATerm -> Sem (Error EvalError : r) Value)
-> ((ATerm, PolyType) -> ATerm)
-> (ATerm, PolyType)
-> Sem (Error EvalError : r) Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, PolyType) -> ATerm
forall a b. (a, b) -> a
fst)
evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => Bool -> ATerm -> Sem r Value
evalTerm :: Bool -> ATerm -> Sem r Value
evalTerm Bool
pr ATerm
at = do
Env
env <- Getter TopInfo Env -> Sem r Env
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo Lens' TopInfo Env
Getter TopInfo Env
topEnv
Value
v <- Env -> Sem (Input Env : r) Value -> Sem r Value
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst Env
env (Sem (Input Env : r) Value -> Sem r Value)
-> Sem (Input Env : r) Value -> Sem r Value
forall a b. (a -> b) -> a -> b
$ Core -> Sem (Input Env : r) Value
forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Core -> Sem r Value
eval (ATerm -> Core
compileTerm ATerm
at)
TyDefCtx
tydefs <- Getter TopInfo TyDefCtx -> Sem r TyDefCtx
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo)
-> ((TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo)
-> (TyDefCtx -> f TyDefCtx)
-> TopInfo
-> f TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyDefCtx)
-> (TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleInfo -> TyDefCtx
allTydefs)
Bool -> Sem r () -> Sem r ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pr (Sem r () -> Sem r ()) -> Sem r () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ TyDefCtx -> Sem (Input TyDefCtx : r) Doc -> Sem r Doc
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs (Sem (Input TyDefCtx : r) Doc -> Sem r Doc)
-> Sem (Input TyDefCtx : r) Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Type -> Value -> Sem (Input TyDefCtx : r) Doc
forall (r :: EffectRow).
Member (Input TyDefCtx) r =>
Type -> Value -> Sem r Doc
prettyValue' Type
ty Value
v
forall (r :: EffectRow).
Member (State TopInfo) r =>
(TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((TopInfo -> TopInfo) -> Sem r ())
-> (TopInfo -> TopInfo) -> Sem r ()
forall a b. (a -> b) -> a -> b
$
((ModuleInfo -> Identity ModuleInfo) -> TopInfo -> Identity TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Identity ModuleInfo)
-> TopInfo -> Identity TopInfo)
-> ((TyCtx -> Identity TyCtx) -> ModuleInfo -> Identity ModuleInfo)
-> (TyCtx -> Identity TyCtx)
-> TopInfo
-> Identity TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Identity TyCtx) -> ModuleInfo -> Identity ModuleInfo
Lens' ModuleInfo TyCtx
miTys ((TyCtx -> Identity TyCtx) -> TopInfo -> Identity TopInfo)
-> (TyCtx -> TyCtx) -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ QName Term -> PolyType -> TyCtx -> TyCtx
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (NameProvenance -> Name Term -> QName Term
forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
REPLModule) (String -> Name Term
forall a. String -> Name a
string2Name String
"it")) (Type -> PolyType
toPolyType Type
ty)) (TopInfo -> TopInfo) -> (TopInfo -> TopInfo) -> TopInfo -> TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
((Env -> Identity Env) -> TopInfo -> Identity TopInfo
Lens' TopInfo Env
topEnv ((Env -> Identity Env) -> TopInfo -> Identity TopInfo)
-> (Env -> Env) -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ QName Core -> Value -> Env -> Env
forall a b. QName a -> b -> Ctx a b -> Ctx a b
Ctx.insert (NameProvenance -> Name Core -> QName Core
forall a. NameProvenance -> Name a -> QName a
QName (ModuleName -> NameProvenance
QualifiedName ModuleName
REPLModule) (String -> Name Core
forall a. String -> Name a
string2Name String
"it")) Value
v)
Value -> Sem r Value
forall (m :: * -> *) a. Monad m => a -> m a
return Value
v
where
ty :: Type
ty = ATerm -> Type
forall t. HasType t => t -> Type
getType ATerm
at
helpCmd :: REPLCommand 'CHelp
helpCmd :: REPLCommand 'CHelp
helpCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"help",
helpcmd :: String
helpcmd = String
":help",
shortHelp :: String
shortHelp = String
"Show help",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CHelp
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CHelp
x -> REPLExpr 'CHelp -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
REPLExpr 'CHelp -> Sem r ()
handleHelp REPLExpr 'CHelp
x,
parser :: Parser (REPLExpr 'CHelp)
parser = REPLExpr 'CHelp -> Parser (REPLExpr 'CHelp)
forall (m :: * -> *) a. Monad m => a -> m a
return REPLExpr 'CHelp
Help
}
handleHelp :: Member (Output Message) r => REPLExpr 'CHelp -> Sem r ()
handleHelp :: REPLExpr 'CHelp -> Sem r ()
handleHelp REPLExpr 'CHelp
Help =
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat
[ Sem r Doc
"Commands available from the prompt:"
, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""
, [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat ((SomeREPLCommand -> Sem r Doc) -> REPLCommands -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
c) -> REPLCommand c -> Sem r Doc
forall (m :: * -> *) (c :: CmdTag).
Applicative m =>
REPLCommand c -> m Doc
showCmd REPLCommand c
c) (REPLCommands -> [Sem r Doc]) -> REPLCommands -> [Sem r Doc]
forall a b. (a -> b) -> a -> b
$ REPLCommands -> REPLCommands
sortedList REPLCommands
discoCommands)
, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
""
]
where
maxlen :: Int
maxlen = REPLCommands -> Int
longestCmd REPLCommands
discoCommands
sortedList :: REPLCommands -> REPLCommands
sortedList REPLCommands
cmds =
(SomeREPLCommand -> SomeREPLCommand -> Ordering)
-> REPLCommands -> REPLCommands
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (\(SomeCmd REPLCommand c
x) (SomeCmd REPLCommand c
y) -> String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
name REPLCommand c
x) (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
name REPLCommand c
y)) (REPLCommands -> REPLCommands) -> REPLCommands -> REPLCommands
forall a b. (a -> b) -> a -> b
$ REPLCommands -> REPLCommands
filteredCommands REPLCommands
cmds
filteredCommands :: REPLCommands -> REPLCommands
filteredCommands REPLCommands
cmds = (SomeREPLCommand -> Bool) -> REPLCommands -> REPLCommands
forall a. (a -> Bool) -> [a] -> [a]
P.filter (\(SomeCmd REPLCommand c
c) -> REPLCommand c -> REPLCommandCategory
forall (c :: CmdTag). REPLCommand c -> REPLCommandCategory
category REPLCommand c
c REPLCommandCategory -> REPLCommandCategory -> Bool
forall a. Eq a => a -> a -> Bool
== REPLCommandCategory
User) REPLCommands
cmds
showCmd :: REPLCommand c -> m Doc
showCmd REPLCommand c
c = String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> Int -> String
padRight (REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
helpcmd REPLCommand c
c) Int
maxlen String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
shortHelp REPLCommand c
c)
longestCmd :: REPLCommands -> Int
longestCmd REPLCommands
cmds = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (SomeREPLCommand -> Int) -> REPLCommands -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(SomeCmd REPLCommand c
c) -> String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ REPLCommand c -> String
forall (c :: CmdTag). REPLCommand c -> String
helpcmd REPLCommand c
c) REPLCommands
cmds
padRight :: String -> Int -> String
padRight String
s Int
maxsize = Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
maxsize (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
' ')
loadCmd :: REPLCommand 'CLoad
loadCmd :: REPLCommand 'CLoad
loadCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"load",
helpcmd :: String
helpcmd = String
":load <filename>",
shortHelp :: String
shortHelp = String
"Load a file",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CLoad
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CLoad
x -> REPLExpr 'CLoad -> Sem r ()
forall (r :: EffectRow).
Members
(Error DiscoError
: State TopInfo : Output Message : Embed IO : EvalEffects)
r =>
REPLExpr 'CLoad -> Sem r ()
handleLoadWrapper REPLExpr 'CLoad
x,
parser :: Parser (REPLExpr 'CLoad)
parser = String -> REPLExpr 'CLoad
Load (String -> REPLExpr 'CLoad)
-> Parser String -> Parser (REPLExpr 'CLoad)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
fileParser
}
handleLoadWrapper ::
Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
REPLExpr 'CLoad ->
Sem r ()
handleLoadWrapper :: REPLExpr 'CLoad -> Sem r ()
handleLoadWrapper (Load String
fp) = Sem r Bool -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (String -> Sem r Bool
forall (r :: EffectRow).
Members
(Error DiscoError
: State TopInfo : Output Message : Embed IO : EvalEffects)
r =>
String -> Sem r Bool
handleLoad String
fp)
handleLoad ::
Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
FilePath ->
Sem r Bool
handleLoad :: String -> Sem r Bool
handleLoad String
fp = do
let (String
directory, String
modName) = String -> (String, String)
splitFileName String
fp
forall (r :: EffectRow).
Member (State TopInfo) r =>
(TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((TopInfo -> TopInfo) -> Sem r ())
-> (TopInfo -> TopInfo) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ (Map ModuleName ModuleInfo -> Identity (Map ModuleName ModuleInfo))
-> TopInfo -> Identity TopInfo
Lens' TopInfo (Map ModuleName ModuleInfo)
topModMap ((Map ModuleName ModuleInfo
-> Identity (Map ModuleName ModuleInfo))
-> TopInfo -> Identity TopInfo)
-> Map ModuleName ModuleInfo -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map ModuleName ModuleInfo
forall k a. Map k a
M.empty
forall (r :: EffectRow).
Member (State TopInfo) r =>
(TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((TopInfo -> TopInfo) -> Sem r ())
-> (TopInfo -> TopInfo) -> Sem r ()
forall a b. (a -> b) -> a -> b
$ (Env -> Identity Env) -> TopInfo -> Identity TopInfo
Lens' TopInfo Env
topEnv ((Env -> Identity Env) -> TopInfo -> Identity TopInfo)
-> Env -> TopInfo -> TopInfo
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Env
forall a b. Ctx a b
Ctx.emptyCtx
ModuleInfo
m <- forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) ModuleInfo -> Sem r ModuleInfo)
-> Sem (Input TopInfo : r) ModuleInfo -> Sem r ModuleInfo
forall a b. (a -> b) -> a -> b
$ Bool -> Resolver -> String -> Sem (Input TopInfo : r) ModuleInfo
forall (r :: EffectRow).
Members
'[State TopInfo, Output Message, Random, State Mem,
Error DiscoError, Embed IO]
r =>
Bool -> Resolver -> String -> Sem r ModuleInfo
loadDiscoModule Bool
False (String -> Resolver
FromDir String
directory) String
modName
ModuleInfo -> Sem r ()
forall (r :: EffectRow).
Members
'[State TopInfo, Random, Error EvalError, State Mem,
Output Message]
r =>
ModuleInfo -> Sem r ()
setREPLModule ModuleInfo
m
Bool
t <- Sem (Input TopInfo : r) Bool -> Sem r Bool
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) Bool -> Sem r Bool)
-> Sem (Input TopInfo : r) Bool -> Sem r Bool
forall a b. (a -> b) -> a -> b
$ Ctx ATerm [ATerm] -> Sem (Input TopInfo : r) Bool
forall (r :: EffectRow).
Members (Output Message : Input TopInfo : EvalEffects) r =>
Ctx ATerm [ATerm] -> Sem r Bool
runAllTests (ModuleInfo
m ModuleInfo
-> Getting (Ctx ATerm [ATerm]) ModuleInfo (Ctx ATerm [ATerm])
-> Ctx ATerm [ATerm]
forall s a. s -> Getting a s a -> a
^. Getting (Ctx ATerm [ATerm]) ModuleInfo (Ctx ATerm [ATerm])
Lens' ModuleInfo (Ctx ATerm [ATerm])
miProps)
[(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)
(TopInfo -> TopInfo) -> Sem r ()
forall s (r :: EffectRow).
Member (State s) r =>
(s -> s) -> Sem r ()
modify @TopInfo ((Maybe String -> Identity (Maybe String))
-> TopInfo -> Identity TopInfo
Lens' TopInfo (Maybe String)
lastFile ((Maybe String -> Identity (Maybe String))
-> TopInfo -> Identity TopInfo)
-> String -> TopInfo -> TopInfo
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ String
fp)
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info Sem r Doc
"Loaded."
Bool -> Sem r Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
t
runAllTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => Ctx ATerm [AProperty] -> Sem r Bool
runAllTests :: Ctx ATerm [ATerm] -> Sem r Bool
runAllTests Ctx ATerm [ATerm]
aprops
| Ctx ATerm [ATerm] -> Bool
forall a b. Ctx a b -> Bool
Ctx.null Ctx ATerm [ATerm]
aprops = Bool -> Sem r Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
| Bool
otherwise = do
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info Sem r Doc
"Running tests..."
[Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> Sem r [Bool] -> Sem r Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((QName ATerm, [ATerm]) -> Sem r Bool)
-> [(QName ATerm, [ATerm])] -> Sem r [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((QName ATerm -> [ATerm] -> Sem r Bool)
-> (QName ATerm, [ATerm]) -> Sem r Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry QName ATerm -> [ATerm] -> Sem r Bool
forall (r :: EffectRow).
Members (Output Message : Input TopInfo : EvalEffects) r =>
QName ATerm -> [ATerm] -> Sem r Bool
runTests) (Ctx ATerm [ATerm] -> [(QName ATerm, [ATerm])]
forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs Ctx ATerm [ATerm]
aprops)
where
numSamples :: Int
numSamples :: Int
numSamples = Int
50
runTests :: Members (Output Message ': Input TopInfo ': EvalEffects) r => QName ATerm -> [AProperty] -> Sem r Bool
runTests :: QName ATerm -> [ATerm] -> Sem r Bool
runTests (QName NameProvenance
_ Name ATerm
n) [ATerm]
props = do
[(ATerm, TestResult)]
results <- Sem (Input Env : r) [(ATerm, TestResult)]
-> Sem r [(ATerm, TestResult)]
forall (r :: EffectRow) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv (Sem (Input Env : r) [(ATerm, TestResult)]
-> Sem r [(ATerm, TestResult)])
-> Sem (Input Env : r) [(ATerm, TestResult)]
-> Sem r [(ATerm, TestResult)]
forall a b. (a -> b) -> a -> b
$ (ATerm -> Sem (Input Env : r) (ATerm, TestResult))
-> [ATerm] -> Sem (Input Env : r) [(ATerm, TestResult)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((ATerm, Sem (Input Env : r) TestResult)
-> Sem (Input Env : r) (ATerm, TestResult)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA ((ATerm, Sem (Input Env : r) TestResult)
-> Sem (Input Env : r) (ATerm, TestResult))
-> (ATerm -> (ATerm, Sem (Input Env : r) TestResult))
-> ATerm
-> Sem (Input Env : r) (ATerm, TestResult)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm -> ATerm
forall a. a -> a
id (ATerm -> ATerm)
-> (ATerm -> Sem (Input Env : r) TestResult)
-> ATerm
-> (ATerm, Sem (Input Env : r) TestResult)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Int -> ATerm -> Sem (Input Env : r) TestResult
forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Int -> ATerm -> Sem r TestResult
runTest Int
numSamples)) [ATerm]
props
let failures :: [(ATerm, TestResult)]
failures = ((ATerm, TestResult) -> Bool)
-> [(ATerm, TestResult)] -> [(ATerm, TestResult)]
forall a. (a -> Bool) -> [a] -> [a]
P.filter (Bool -> Bool
not (Bool -> Bool)
-> ((ATerm, TestResult) -> Bool) -> (ATerm, TestResult) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestResult -> Bool
testIsOk (TestResult -> Bool)
-> ((ATerm, TestResult) -> TestResult)
-> (ATerm, TestResult)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ATerm, TestResult) -> TestResult
forall a b. (a, b) -> b
snd) [(ATerm, TestResult)]
results
hdr :: Sem r Doc
hdr = Name ATerm -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name ATerm
n Sem r Doc -> Sem r Doc -> Sem r Doc
forall a. Semigroup a => a -> a -> a
<> Sem r Doc
":"
case [(ATerm, TestResult)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures of
Bool
True -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Int -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
hdr Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Sem r Doc
"OK"
Bool
False -> do
TyDefCtx
tydefs <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting TyDefCtx TopInfo TyDefCtx -> TopInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo)
-> ((TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> Getting TyDefCtx TopInfo TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyDefCtx)
-> (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo
-> Const TyDefCtx ModuleInfo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleInfo -> TyDefCtx
allTydefs))
let prettyFailures :: Sem r Doc
prettyFailures =
TyDefCtx -> Sem (Input TyDefCtx : r) Doc -> Sem r Doc
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs (Sem (Input TyDefCtx : r) Doc -> Sem r Doc)
-> (Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem (Input TyDefCtx : r) Doc)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PA
-> Sem (Reader PA : Input TyDefCtx : r) Doc
-> Sem (Input TyDefCtx : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA (Sem (Reader PA : Input TyDefCtx : r) Doc
-> Sem (Input TyDefCtx : r) Doc)
-> (Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem (Reader PA : Input TyDefCtx : r) Doc)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem (Input TyDefCtx : r) Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> Sem (Reader PA : Input TyDefCtx : r) Doc
forall (r :: EffectRow) a. Sem (LFresh : r) a -> Sem r a
runLFresh (Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc -> Sem r Doc)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$
Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
-> [Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall (f :: * -> *). Applicative f => f Doc -> [f Doc] -> f Doc
bulletList Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
"-" ([Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc)
-> [Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall a b. (a -> b) -> a -> b
$ ((ATerm, TestResult)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc)
-> [(ATerm, TestResult)]
-> [Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((ATerm
-> TestResult -> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc)
-> (ATerm, TestResult)
-> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ATerm
-> TestResult -> Sem (LFresh : Reader PA : Input TyDefCtx : r) Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
ATerm -> TestResult -> Sem r Doc
prettyTestFailure) [(ATerm, TestResult)]
failures
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Int -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (Sem r Doc -> Sem r Doc) -> Sem r Doc -> Sem r Doc
forall a b. (a -> b) -> a -> b
$ Sem r Doc
hdr Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$ Sem r Doc
prettyFailures
Bool -> Sem r Bool
forall (m :: * -> *) a. Monad m => a -> m a
return ([(ATerm, TestResult)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
P.null [(ATerm, TestResult)]
failures)
namesCmd :: REPLCommand 'CNames
namesCmd :: REPLCommand 'CNames
namesCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"names",
helpcmd :: String
helpcmd = String
":names",
shortHelp :: String
shortHelp = String
"Show all names in current scope",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CNames
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CNames
x -> Sem (Input TopInfo : r) () -> Sem r ()
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CNames -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CNames
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CNames -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CNames -> Sem r ()
handleNames (REPLExpr 'CNames -> Sem r ()) -> REPLExpr 'CNames -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CNames
x,
parser :: Parser (REPLExpr 'CNames)
parser = REPLExpr 'CNames -> Parser (REPLExpr 'CNames)
forall (m :: * -> *) a. Monad m => a -> m a
return REPLExpr 'CNames
Names
}
handleNames ::
Members '[Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CNames ->
Sem r ()
handleNames :: REPLExpr 'CNames -> Sem r ()
handleNames REPLExpr 'CNames
Names = do
TyDefCtx
tyDef <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting TyDefCtx TopInfo TyDefCtx -> TopInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo)
-> ((TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> Getting TyDefCtx TopInfo TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs))
TyCtx
ctx <- (TopInfo -> TyCtx) -> Sem r TyCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting TyCtx TopInfo TyCtx -> TopInfo -> TyCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyCtx ModuleInfo)
-> TopInfo -> Const TyCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyCtx ModuleInfo)
-> TopInfo -> Const TyCtx TopInfo)
-> ((TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo)
-> Getting TyCtx TopInfo TyCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCtx -> Const TyCtx TyCtx)
-> ModuleInfo -> Const TyCtx ModuleInfo
Lens' ModuleInfo TyCtx
miTys))
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((String, TyDefBody) -> Sem r Doc)
-> [(String, TyDefBody)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String, TyDefBody) -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (TyDefCtx -> [(String, TyDefBody)]
forall k a. Map k a -> [(k, a)]
M.assocs TyDefCtx
tyDef))
Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
$+$
[Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat (((QName Term, PolyType) -> Sem r Doc)
-> [(QName Term, PolyType)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (QName Term, PolyType) -> Sem r Doc
forall t a (r :: EffectRow). Pretty t => (QName a, t) -> Sem r Doc
showFn (TyCtx -> [(QName Term, PolyType)]
forall a b. Ctx a b -> [(QName a, b)]
Ctx.assocs TyCtx
ctx))
where
showFn :: (QName a, t) -> Sem r Doc
showFn (QName NameProvenance
_ Name a
x, t
ty) = [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
hsep [Name a -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name a
x, String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":", t -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' t
ty]
nopCmd :: REPLCommand 'CNop
nopCmd :: REPLCommand 'CNop
nopCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"nop",
helpcmd :: String
helpcmd = String
"",
shortHelp :: String
shortHelp = String
"No-op, e.g. if the user just enters a comment",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
BuiltIn,
action :: REPLExpr 'CNop
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CNop
x -> REPLExpr 'CNop -> Sem r ()
forall (r :: EffectRow). REPLExpr 'CNop -> Sem r ()
handleNop REPLExpr 'CNop
x,
parser :: Parser (REPLExpr 'CNop)
parser = REPLExpr 'CNop
Nop REPLExpr 'CNop -> Parser () -> Parser (REPLExpr 'CNop)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Parser ()
sc Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof)
}
handleNop :: REPLExpr 'CNop -> Sem r ()
handleNop :: REPLExpr 'CNop -> Sem r ()
handleNop REPLExpr 'CNop
Nop = () -> Sem r ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
parseCmd :: REPLCommand 'CParse
parseCmd :: REPLCommand 'CParse
parseCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"parse",
helpcmd :: String
helpcmd = String
":parse <expr>",
shortHelp :: String
shortHelp = String
"Show the parsed AST",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CParse
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CParse
x -> REPLExpr 'CParse -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
REPLExpr 'CParse -> Sem r ()
handleParse REPLExpr 'CParse
x,
parser :: Parser (REPLExpr 'CParse)
parser = Term -> REPLExpr 'CParse
Parse (Term -> REPLExpr 'CParse)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CParse)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handleParse :: Member (Output Message) r => REPLExpr 'CParse -> Sem r ()
handleParse :: REPLExpr 'CParse -> Sem r ()
handleParse (Parse Term
t) = Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (Term -> String
forall a. Show a => a -> String
show Term
t))
prettyCmd :: REPLCommand 'CPretty
prettyCmd :: REPLCommand 'CPretty
prettyCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"pretty",
helpcmd :: String
helpcmd = String
":pretty <expr>",
shortHelp :: String
shortHelp = String
"Pretty-print a term",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CPretty
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CPretty
x -> REPLExpr 'CPretty -> Sem r ()
forall (r :: EffectRow).
Members '[LFresh, Output Message] r =>
REPLExpr 'CPretty -> Sem r ()
handlePretty REPLExpr 'CPretty
x,
parser :: Parser (REPLExpr 'CPretty)
parser = Term -> REPLExpr 'CPretty
Pretty (Term -> REPLExpr 'CPretty)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CPretty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handlePretty :: Members '[LFresh, Output Message] r => REPLExpr 'CPretty -> Sem r ()
handlePretty :: REPLExpr 'CPretty -> Sem r ()
handlePretty (Pretty Term
t) = Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Term
t
printCmd :: REPLCommand 'CPrint
printCmd :: REPLCommand 'CPrint
printCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"print",
helpcmd :: String
helpcmd = String
":print <expr>",
shortHelp :: String
shortHelp = String
"Print a string without the double quotes, interpreting special characters",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CPrint
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CPrint
x -> REPLExpr 'CPrint -> Sem r ()
forall (r :: EffectRow).
Members
(Error DiscoError : State TopInfo : Output Message : EvalEffects)
r =>
REPLExpr 'CPrint -> Sem r ()
handlePrint REPLExpr 'CPrint
x,
parser :: Parser (REPLExpr 'CPrint)
parser = Term -> REPLExpr 'CPrint
Print (Term -> REPLExpr 'CPrint)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CPrint)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handlePrint :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()
handlePrint :: REPLExpr 'CPrint -> Sem r ()
handlePrint (Print Term
t) = do
ATerm
at <- Sem (Input TopInfo : r) ATerm -> Sem r ATerm
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) ATerm -> Sem r ATerm)
-> (Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem (Input TopInfo : r) ATerm)
-> Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem r ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem (Input TopInfo : r) ATerm
forall (r :: EffectRow) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop (Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem r ATerm)
-> Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Term
-> PolyType
-> Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
forall (r :: EffectRow).
Members
'[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
Fresh]
r =>
Term -> PolyType -> Sem r ATerm
checkTop Term
t (Type -> PolyType
toPolyType Type
TyString)
Value
v <- (EvalError -> DiscoError)
-> Sem (Error EvalError : r) Value -> Sem r Value
forall e1 e2 (r :: EffectRow) a.
Member (Error e2) r =>
(e1 -> e2) -> Sem (Error e1 : r) a -> Sem r a
mapError EvalError -> DiscoError
EvalErr (Sem (Error EvalError : r) Value -> Sem r Value)
-> (ATerm -> Sem (Error EvalError : r) Value)
-> ATerm
-> Sem r Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> ATerm -> Sem (Error EvalError : r) Value
forall (r :: EffectRow).
Members
(Error EvalError : State TopInfo : Output Message : EvalEffects)
r =>
Bool -> ATerm -> Sem r Value
evalTerm Bool
False (ATerm -> Sem r Value) -> ATerm -> Sem r Value
forall a b. (a -> b) -> a -> b
$ ATerm
at
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text ((Value -> Char) -> Value -> String
forall a. (Value -> a) -> Value -> [a]
vlist Value -> Char
vchar Value
v)
reloadCmd :: REPLCommand 'CReload
reloadCmd :: REPLCommand 'CReload
reloadCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"reload",
helpcmd :: String
helpcmd = String
":reload",
shortHelp :: String
shortHelp = String
"Reloads the most recently loaded file",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CReload
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CReload
x -> REPLExpr 'CReload -> Sem r ()
forall (r :: EffectRow).
Members
(Error DiscoError
: State TopInfo : Output Message : Embed IO : EvalEffects)
r =>
REPLExpr 'CReload -> Sem r ()
handleReload REPLExpr 'CReload
x,
parser :: Parser (REPLExpr 'CReload)
parser = REPLExpr 'CReload -> Parser (REPLExpr 'CReload)
forall (m :: * -> *) a. Monad m => a -> m a
return REPLExpr 'CReload
Reload
}
handleReload ::
Members (Error DiscoError ': State TopInfo ': Output Message ': Embed IO ': EvalEffects) r =>
REPLExpr 'CReload ->
Sem r ()
handleReload :: REPLExpr 'CReload -> Sem r ()
handleReload REPLExpr 'CReload
Reload = do
Maybe String
file <- Getter TopInfo (Maybe String) -> Sem r (Maybe String)
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use Lens' TopInfo (Maybe String)
Getter TopInfo (Maybe String)
lastFile
case Maybe String
file of
Maybe String
Nothing -> Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info Sem r Doc
"No file to reload."
Just String
f -> Sem r Bool -> Sem r ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (String -> Sem r Bool
forall (r :: EffectRow).
Members
(Error DiscoError
: State TopInfo : Output Message : Embed IO : EvalEffects)
r =>
String -> Sem r Bool
handleLoad String
f)
showDefnCmd :: REPLCommand 'CShowDefn
showDefnCmd :: REPLCommand 'CShowDefn
showDefnCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"defn",
helpcmd :: String
helpcmd = String
":defn <var>",
shortHelp :: String
shortHelp = String
"Show a variable's definition",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CShowDefn
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CShowDefn
x -> forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CShowDefn -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CShowDefn
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CShowDefn -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members '[Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CShowDefn -> Sem r ()
handleShowDefn (REPLExpr 'CShowDefn -> Sem r ())
-> REPLExpr 'CShowDefn -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CShowDefn
x,
parser :: Parser (REPLExpr 'CShowDefn)
parser = Name Term -> REPLExpr 'CShowDefn
ShowDefn (Name Term -> REPLExpr 'CShowDefn)
-> StateT ParserState (Parsec DiscoParseError String) (Name Term)
-> Parser (REPLExpr 'CShowDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser ()
sc Parser ()
-> StateT ParserState (Parsec DiscoParseError String) (Name Term)
-> StateT ParserState (Parsec DiscoParseError String) (Name Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) (Name Term)
ident)
}
handleShowDefn ::
Members '[Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CShowDefn ->
Sem r ()
handleShowDefn :: REPLExpr 'CShowDefn -> Sem r ()
handleShowDefn (ShowDefn Name Term
x) = do
let name2s :: String
name2s = Name Term -> String
forall a. Name a -> String
name2String Name Term
x
Ctx ATerm Defn
defns <- (TopInfo -> Ctx ATerm Defn) -> Sem r (Ctx ATerm Defn)
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting (Ctx ATerm Defn) TopInfo (Ctx ATerm Defn)
-> TopInfo -> Ctx ATerm Defn
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo)
-> TopInfo -> Const (Ctx ATerm Defn) TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo)
-> TopInfo -> Const (Ctx ATerm Defn) TopInfo)
-> ((Ctx ATerm Defn -> Const (Ctx ATerm Defn) (Ctx ATerm Defn))
-> ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo)
-> Getting (Ctx ATerm Defn) TopInfo (Ctx ATerm Defn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ctx ATerm Defn -> Const (Ctx ATerm Defn) (Ctx ATerm Defn))
-> ModuleInfo -> Const (Ctx ATerm Defn) ModuleInfo
Lens' ModuleInfo (Ctx ATerm Defn)
miTermdefs))
TyDefCtx
tyDefns <- (TopInfo -> TyDefCtx) -> Sem r TyDefCtx
forall i j (r :: EffectRow).
Member (Input i) r =>
(i -> j) -> Sem r j
inputs @TopInfo (Getting TyDefCtx TopInfo TyDefCtx -> TopInfo -> TyDefCtx
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> Const TyDefCtx ModuleInfo)
-> TopInfo -> Const TyDefCtx TopInfo)
-> ((TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo)
-> Getting TyDefCtx TopInfo TyDefCtx
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyDefCtx -> Const TyDefCtx TyDefCtx)
-> ModuleInfo -> Const TyDefCtx ModuleInfo
Lens' ModuleInfo TyDefCtx
miTydefs))
let xdefs :: [(QName ATerm, Defn)]
xdefs = Name ATerm -> Ctx ATerm Defn -> [(QName ATerm, Defn)]
forall a b. Name a -> Ctx a b -> [(QName a, b)]
Ctx.lookupAll' (Name Term -> Name ATerm
coerce Name Term
x) Ctx ATerm Defn
defns
mtydef :: Maybe TyDefBody
mtydef = String -> TyDefCtx -> Maybe TyDefBody
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
name2s TyDefCtx
tyDefns
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ do
let ds :: [Sem r Doc]
ds = ((QName ATerm, Defn) -> Sem r Doc)
-> [(QName ATerm, Defn)] -> [Sem r Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Defn -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' (Defn -> Sem r Doc)
-> ((QName ATerm, Defn) -> Defn)
-> (QName ATerm, Defn)
-> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName ATerm, Defn) -> Defn
forall a b. (a, b) -> b
snd) [(QName ATerm, Defn)]
xdefs [Sem r Doc] -> [Sem r Doc] -> [Sem r Doc]
forall a. [a] -> [a] -> [a]
++ [Sem r Doc]
-> (TyDefBody -> [Sem r Doc]) -> Maybe TyDefBody -> [Sem r Doc]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Sem r Doc -> [Sem r Doc]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sem r Doc -> [Sem r Doc])
-> (TyDefBody -> Sem r Doc) -> TyDefBody -> [Sem r Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, TyDefBody) -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' ((String, TyDefBody) -> Sem r Doc)
-> (TyDefBody -> (String, TyDefBody)) -> TyDefBody -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
name2s,)) Maybe TyDefBody
mtydef
case [Sem r Doc]
ds of
[] -> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"No definition for" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> Name Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Name Term
x
[Sem r Doc]
_ -> [Sem r Doc] -> Sem r Doc
forall (f :: * -> *). Applicative f => [f Doc] -> f Doc
vcat [Sem r Doc]
ds
testPropCmd :: REPLCommand 'CTestProp
testPropCmd :: REPLCommand 'CTestProp
testPropCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"test",
helpcmd :: String
helpcmd = String
":test <property>",
shortHelp :: String
shortHelp = String
"Test a property using random examples",
category :: REPLCommandCategory
category = REPLCommandCategory
User,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CTestProp
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CTestProp
x -> REPLExpr 'CTestProp -> Sem r ()
forall (r :: EffectRow).
Members
(Error DiscoError : State TopInfo : Output Message : EvalEffects)
r =>
REPLExpr 'CTestProp -> Sem r ()
handleTest REPLExpr 'CTestProp
x,
parser :: Parser (REPLExpr 'CTestProp)
parser = Term -> REPLExpr 'CTestProp
TestProp (Term -> REPLExpr 'CTestProp)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CTestProp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
term
}
handleTest ::
Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r =>
REPLExpr 'CTestProp ->
Sem r ()
handleTest :: REPLExpr 'CTestProp -> Sem r ()
handleTest (TestProp Term
t) = do
ATerm
at <- Sem (Input TopInfo : r) ATerm -> Sem r ATerm
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) ATerm -> Sem r ATerm)
-> (Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem (Input TopInfo : r) ATerm)
-> Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem r ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem (Input TopInfo : r) ATerm
forall (r :: EffectRow) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop (Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem r ATerm)
-> Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
-> Sem r ATerm
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
(Reader TyCtx
: Reader TyDefCtx : Fresh : Error TCError : Input TopInfo : r)
ATerm
forall (r :: EffectRow).
Members
'[Reader TyCtx, Reader TyDefCtx, Error TCError, Fresh,
Output Message]
r =>
Term -> Sem r ATerm
checkProperty Term
t
TyDefCtx
tydefs <- Getter TopInfo TyDefCtx -> Sem r TyDefCtx
forall s (r :: EffectRow) a.
Member (State s) r =>
Getter s a -> Sem r a
use @TopInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo
Lens' TopInfo ModuleInfo
replModInfo ((ModuleInfo -> f ModuleInfo) -> TopInfo -> f TopInfo)
-> ((TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo)
-> (TyDefCtx -> f TyDefCtx)
-> TopInfo
-> f TopInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleInfo -> TyDefCtx)
-> (TyDefCtx -> f TyDefCtx) -> ModuleInfo -> f ModuleInfo
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ModuleInfo -> TyDefCtx
allTydefs)
Sem (Input TopInfo : r) () -> Sem r ()
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState (Sem (Input TopInfo : r) () -> Sem r ())
-> (Sem (Input Env : Input TopInfo : r) ()
-> Sem (Input TopInfo : r) ())
-> Sem (Input Env : Input TopInfo : r) ()
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sem (Input Env : Input TopInfo : r) ()
-> Sem (Input TopInfo : r) ()
forall (r :: EffectRow) a.
Member (Input TopInfo) r =>
Sem (Input Env : r) a -> Sem r a
inputTopEnv (Sem (Input Env : Input TopInfo : r) () -> Sem r ())
-> Sem (Input Env : Input TopInfo : r) () -> Sem r ()
forall a b. (a -> b) -> a -> b
$ do
TestResult
r <- Int -> ATerm -> Sem (Input Env : Input TopInfo : r) TestResult
forall (r :: EffectRow).
Members '[Random, Error EvalError, Input Env, State Mem] r =>
Int -> ATerm -> Sem r TestResult
runTest Int
100 ATerm
at
Sem (Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem (Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) ())
-> Sem (Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) ()
forall a b. (a -> b) -> a -> b
$ TyDefCtx
-> Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Input i : r) a -> Sem r a
runInputConst TyDefCtx
tydefs (Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc)
-> (Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc)
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PA
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall i (r :: EffectRow) a. i -> Sem (Reader i : r) a -> Sem r a
runReader PA
initPA (Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc)
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem (Input Env : Input TopInfo : r) Doc
forall a b. (a -> b) -> a -> b
$ Int
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall (f :: * -> *). Functor f => Int -> f Doc -> f Doc
nest Int
2 (Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc)
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall a b. (a -> b) -> a -> b
$ Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
"-" Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> ATerm
-> TestResult
-> Sem
(Reader PA : Input TyDefCtx : Input Env : Input TopInfo : r) Doc
forall (r :: EffectRow).
Members '[Input TyDefCtx, LFresh, Reader PA] r =>
ATerm -> TestResult -> Sem r Doc
prettyTestResult ATerm
at TestResult
r
typeCheckCmd :: REPLCommand 'CTypeCheck
typeCheckCmd :: REPLCommand 'CTypeCheck
typeCheckCmd =
REPLCommand :: forall (c :: CmdTag).
String
-> String
-> String
-> REPLCommandCategory
-> REPLCommandType
-> (REPLExpr c
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ())
-> Parser (REPLExpr c)
-> REPLCommand c
REPLCommand
{ name :: String
name = String
"type",
helpcmd :: String
helpcmd = String
":type <term>",
shortHelp :: String
shortHelp = String
"Typecheck a term",
category :: REPLCommandCategory
category = REPLCommandCategory
Dev,
cmdtype :: REPLCommandType
cmdtype = REPLCommandType
ColonCmd,
action :: REPLExpr 'CTypeCheck
-> forall (r :: EffectRow). Members DiscoEffects r => Sem r ()
action = \REPLExpr 'CTypeCheck
x -> forall (r :: EffectRow) a.
Member (State TopInfo) r =>
Sem (Input TopInfo : r) a -> Sem r a
forall s (r :: EffectRow) a.
Member (State s) r =>
Sem (Input s : r) a -> Sem r a
inputToState @TopInfo (Sem (Input TopInfo : r) () -> Sem r ())
-> (REPLExpr 'CTypeCheck -> Sem (Input TopInfo : r) ())
-> REPLExpr 'CTypeCheck
-> Sem r ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. REPLExpr 'CTypeCheck -> Sem (Input TopInfo : r) ()
forall (r :: EffectRow).
Members
'[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck (REPLExpr 'CTypeCheck -> Sem r ())
-> REPLExpr 'CTypeCheck -> Sem r ()
forall a b. (a -> b) -> a -> b
$ REPLExpr 'CTypeCheck
x,
parser :: Parser (REPLExpr 'CTypeCheck)
parser = Parser (REPLExpr 'CTypeCheck)
parseTypeCheck
}
handleTypeCheck ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output Message] r =>
REPLExpr 'CTypeCheck ->
Sem r ()
handleTypeCheck :: REPLExpr 'CTypeCheck -> Sem r ()
handleTypeCheck (TypeCheck Term
t) = do
(ATerm
_, PolyType
sig) <- Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall (r :: EffectRow) a.
Members '[Input TopInfo, Error DiscoError] r =>
Sem (Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r) a
-> Sem r a
typecheckTop (Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType))
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
-> Sem r (ATerm, PolyType)
forall a b. (a -> b) -> a -> b
$ Term
-> Sem
(Reader TyCtx : Reader TyDefCtx : Fresh : Error TCError : r)
(ATerm, PolyType)
forall (r :: EffectRow).
Members
'[Output Message, Reader TyCtx, Reader TyDefCtx, Error TCError,
Fresh]
r =>
Term -> Sem r (ATerm, PolyType)
inferTop Term
t
Sem r Doc -> Sem r ()
forall (r :: EffectRow).
Member (Output Message) r =>
Sem r Doc -> Sem r ()
info (Sem r Doc -> Sem r ()) -> Sem r Doc -> Sem r ()
forall a b. (a -> b) -> a -> b
$ Term -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' Term
t Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> String -> Sem r Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
":" Sem r Doc -> Sem r Doc -> Sem r Doc
forall (f :: * -> *). Applicative f => f Doc -> f Doc -> f Doc
<+> PolyType -> Sem r Doc
forall t (r :: EffectRow). Pretty t => t -> Sem r Doc
pretty' PolyType
sig
parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)
parseTypeCheck :: Parser (REPLExpr 'CTypeCheck)
parseTypeCheck =
Term -> REPLExpr 'CTypeCheck
TypeCheck
(Term -> REPLExpr 'CTypeCheck)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser (REPLExpr 'CTypeCheck)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Term
term StateT ParserState (Parsec DiscoParseError String) Term
-> String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"expression")
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (StateT ParserState (Parsec DiscoParseError String) Term
parseNakedOp StateT ParserState (Parsec DiscoParseError String) Term
-> String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator")
)
parseNakedOp :: Parser Term
parseNakedOp :: StateT ParserState (Parsec DiscoParseError String) Term
parseNakedOp = Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Prim
parseNakedOpPrim
parseNakedOpPrim :: Parser Prim
parseNakedOpPrim :: StateT ParserState (Parsec DiscoParseError String) Prim
parseNakedOpPrim = Parser ()
sc Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((OpInfo -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [OpInfo]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map OpInfo -> StateT ParserState (Parsec DiscoParseError String) Prim
mkOpParser ([[OpInfo]] -> [OpInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[OpInfo]]
opTable))
where
mkOpParser :: OpInfo -> Parser Prim
mkOpParser :: OpInfo -> StateT ParserState (Parsec DiscoParseError String) Prim
mkOpParser (OpInfo (UOpF UFixity
_ UOp
op) [String]
syns Int
_) = [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map ((UOp -> Prim
PrimUOp UOp
op Prim
-> Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim)
-> (String -> Parser ())
-> String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Parser ()
reservedOp) [String]
syns)
mkOpParser (OpInfo (BOpF BFixity
_ BOp
op) [String]
syns Int
_) = [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map ((BOp -> Prim
PrimBOp BOp
op Prim
-> Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) (Parser ()
-> StateT ParserState (Parsec DiscoParseError String) Prim)
-> (String -> Parser ())
-> String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Parser ()
reservedOp) [String]
syns)