module Agda.Interaction.CommandLine.CommandLine where
import Control.Monad.Error
import Control.Monad.Reader
import Control.Applicative
import Data.Char
import Data.Set as Set
import Data.Map as Map
import Data.List as List
import Data.Maybe
import qualified Agda.Utils.IO.Locale as LocIO
import Agda.Interaction.BasicOps as BasicOps hiding (parseExpr)
import Agda.Interaction.Monad
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Parser
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Abstract.Pretty
import Text.PrettyPrint
import Agda.TypeChecker
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Monad
import Agda.TypeChecking.MetaVars
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Substitute
import Agda.Utils.Monad
import Agda.Utils.Fresh
#include "../../undefined.h"
import Agda.Utils.Impossible
data ExitCode a = Continue | ContinueIn TCEnv | Return a
type Command a = (String, [String] -> TCM (ExitCode a))
matchCommand :: String -> [Command a] -> Either [String] ([String] -> TCM (ExitCode a))
matchCommand x cmds =
case List.filter (isPrefixOf x . fst) cmds of
[(_,m)] -> Right m
xs -> Left $ List.map fst xs
interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> IM a
interaction prompt cmds eval = loop
where
go (Return x) = return x
go Continue = loop
go (ContinueIn env) = local (const env) loop
loop =
do ms <- readline prompt
case fmap words ms of
Nothing -> return $ error "** EOF **"
Just [] -> loop
Just ((':':cmd):args) ->
do case matchCommand cmd cmds of
Right c -> go =<< liftTCM (c args)
Left [] ->
do liftIO $ LocIO.putStrLn $ "Unknown command '" ++ cmd ++ "'"
loop
Left xs ->
do liftIO $ LocIO.putStrLn $ "More than one command match: " ++ concat (intersperse ", " xs)
loop
Just _ ->
do go =<< liftTCM (eval $ fromJust ms)
`catchError` \e ->
do s <- prettyError e
liftIO $ LocIO.putStrLn s
loop
interactionLoop :: TCM (Maybe Interface) -> IM ()
interactionLoop typeCheck =
do liftTCM reload
interaction "Main> " commands evalTerm
where
reload = do
mi <- typeCheck
setScope $ case mi of
Just i -> iInsideScope i
Nothing -> emptyScopeInfo
`catchError` \e -> do
s <- prettyError e
liftIO $ LocIO.putStrLn s
liftIO $ LocIO.putStrLn "Failed."
commands =
[ "quit" |> \_ -> return $ Return ()
, "?" |> \_ -> continueAfter $ liftIO $ help commands
, "reload" |> \_ -> do reload
ContinueIn <$> ask
, "constraints" |> \args -> continueAfter $ showConstraints args
, "Context" |> \args -> continueAfter $ showContext args
, "give" |> \args -> continueAfter $ giveMeta args
, "Refine" |> \args -> continueAfter $ refineMeta args
, "metas" |> \args -> continueAfter $ showMetas args
, "load" |> \args -> continueAfter $ loadFile reload args
, "eval" |> \args -> continueAfter $ evalIn args
, "typeOf" |> \args -> continueAfter $ typeOf args
, "typeIn" |> \args -> continueAfter $ typeIn args
, "wakeup" |> \_ -> continueAfter $ retryConstraints
, "scope" |> \_ -> continueAfter $ showScope
]
where
(|>) = (,)
continueAfter :: TCM a -> TCM (ExitCode b)
continueAfter m = m >> return Continue
loadFile :: TCM () -> [String] -> TCM ()
loadFile reload [file] =
do setInputFile file
reload
loadFile _ _ = liftIO $ LocIO.putStrLn ":load file"
showConstraints :: [String] -> TCM ()
showConstraints [c] =
do i <- readM c
cc <- normalise =<< lookupConstraint i
d <- prettyTCM $ clValue cc
liftIO $ LocIO.print d
showConstraints [] =
do cs <- BasicOps.getConstraints
liftIO $ LocIO.putStrLn $ unlines (List.map show cs)
showConstraints _ = liftIO $ LocIO.putStrLn ":constraints [cid]"
showMetas :: [String] -> TCM ()
showMetas [m] =
do i <- InteractionId <$> readM m
withInteractionId i $ do
s <- typeOfMeta AsIs i
r <- getInteractionRange i
d <- showA s
liftIO $ LocIO.putStrLn $ d ++ " " ++ show r
showMetas [m,"normal"] =
do i <- InteractionId <$> readM m
withInteractionId i $ do
s <- showA =<< typeOfMeta Normalised i
r <- getInteractionRange i
liftIO $ LocIO.putStrLn $ s ++ " " ++ show r
showMetas [] =
do interactionMetas <- typesOfVisibleMetas AsIs
hiddenMetas <- typesOfHiddenMetas AsIs
mapM_ (liftIO . LocIO.putStrLn) =<< mapM showII interactionMetas
mapM_ print' hiddenMetas
where
showII o = withInteractionId (outputFormId o) $ showA o
showM o = withMetaId (outputFormId o) $ showA o
metaId (OfType i _) = i
metaId (JustType i) = i
metaId (JustSort i) = i
metaId (Assign i e) = i
metaId _ = __IMPOSSIBLE__
print' x = do
r <- getMetaRange (metaId x)
d <- showM x
liftIO $ LocIO.putStrLn $ d ++ " [ at " ++ show r ++ " ]"
showMetas _ = liftIO $ LocIO.putStrLn $ ":meta [metaid]"
showScope :: TCM ()
showScope = do
scope <- getScope
liftIO $ LocIO.print scope
metaParseExpr :: InteractionId -> String -> TCM A.Expr
metaParseExpr ii s =
do m <- lookupInteractionId ii
scope <- getMetaScope <$> lookupMeta m
r <- getRange <$> lookupMeta m
let pos = case rStart r of
Nothing -> __IMPOSSIBLE__
Just pos -> pos
e <- liftIO $ parsePosString exprParser pos s
concreteToAbstract scope e
actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
actOnMeta (is:es) f =
do i <- readM is
let ii = InteractionId i
e <- metaParseExpr ii (unwords es)
withInteractionId ii $ f ii e
actOnMeta _ _ = __IMPOSSIBLE__
giveMeta :: [String] -> TCM ()
giveMeta s | length s >= 2 =
do actOnMeta s (\ii -> \e -> give ii Nothing e)
return ()
giveMeta _ = liftIO $ LocIO.putStrLn $ ": give" ++ " metaid expr"
refineMeta :: [String] -> TCM ()
refineMeta s | length s >= 2 =
do actOnMeta s (\ii -> \e -> refine ii Nothing e)
return ()
refineMeta _ = liftIO $ LocIO.putStrLn $ ": refine" ++ " metaid expr"
retryConstraints :: TCM ()
retryConstraints = liftTCM wakeupConstraints
evalIn :: [String] -> TCM ()
evalIn s | length s >= 2 =
do d <- actOnMeta s $ \_ e -> prettyA =<< evalInCurrent e
liftIO $ LocIO.print d
evalIn _ = liftIO $ LocIO.putStrLn ":eval metaid expr"
parseExpr :: String -> TCM A.Expr
parseExpr s = do
e <- liftIO $ parse exprParser s
localToAbstract e return
evalTerm :: String -> TCM (ExitCode a)
evalTerm s =
do e <- parseExpr s
v <- evalInCurrent e
e <- prettyTCM v
liftIO $ LocIO.putStrLn $ show e
return Continue
where
evalInCurrent e = do
t <- newTypeMeta_
v <- checkExpr e t
v' <- normalise v
return v'
typeOf :: [String] -> TCM ()
typeOf s =
do e <- parseExpr (unwords s)
e0 <- typeInCurrent Normalised e
e1 <- typeInCurrent AsIs e
liftIO . LocIO.putStrLn =<< showA e1
typeIn :: [String] -> TCM ()
typeIn s@(_:_:_) =
actOnMeta s $ \i e ->
do e1 <- typeInMeta i Normalised e
e2 <- typeInMeta i AsIs e
liftIO . LocIO.putStrLn =<< showA e1
typeIn _ = liftIO $ LocIO.putStrLn ":typeIn meta expr"
showContext :: [String] -> TCM ()
showContext (meta:args) = do
i <- InteractionId <$> readM meta
mi <- lookupMeta =<< lookupInteractionId i
withMetaInfo (getMetaInfo mi) $ do
ctx <- List.map unArg . telToList <$> getContextTelescope
zipWithM_ display ctx $ reverse $ zipWith const [1..] ctx
where
display (x, t) n = do
t <- case args of
["normal"] -> normalise $ raise n t
_ -> return $ raise n t
d <- prettyTCM t
liftIO $ LocIO.print $ text x <+> text ":" <+> d
showContext _ = liftIO $ LocIO.putStrLn ":Context meta"
splashScreen :: String
splashScreen = unlines
[ " _ "
, " ____ | |"
, " / __ \\ | |"
, " | |__| |___ __| | ___"
, " | __ / _ \\/ _ |/ __\\ Agda Interactive"
, " | | |/ /_\\ \\/_| / /_| \\"
, " |_| |\\___ /____\\_____/ Type :? for help."
, " __/ /"
, " \\__/"
, ""
, "The interactive mode is no longer supported. Don't complain if it doesn't work."
]
help :: [Command a] -> IO ()
help cs = LocIO.putStr $ unlines $
[ "Command overview" ] ++ List.map explain cs ++
[ "<exp> Infer type of expression <exp> and evaluate it." ]
where
explain (x,_) = ":" ++ x