module Agda.Interaction.CommandLine ( runInteractionLoop ) where import Control.Monad.Except import Control.Monad.State import Control.Monad.Reader import qualified Data.List as List import Data.Maybe import Text.Read (readMaybe) import Agda.Interaction.Base hiding (Command) import Agda.Interaction.BasicOps as BasicOps hiding (parseExpr) import Agda.Interaction.Imports ( CheckResult, crInterface ) import Agda.Interaction.Monad import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Common import Agda.Syntax.Internal (telToList, alwaysUnblock) import qualified Agda.Syntax.Internal as I import Agda.Syntax.Parser import Agda.Syntax.Position import Agda.Syntax.Scope.Base import Agda.Syntax.Translation.ConcreteToAbstract import Agda.Syntax.Abstract.Pretty import Agda.TypeChecking.Constraints import Agda.TypeChecking.Monad import Agda.TypeChecking.Reduce import Agda.TypeChecking.Errors import Agda.TypeChecking.Pretty ( PrettyTCM(prettyTCM) ) import Agda.TypeChecking.Substitute import Agda.TypeChecking.Warnings (runPM) import Agda.Utils.FileName (absolute, AbsolutePath) import Agda.Utils.Maybe (caseMaybeM) import Agda.Utils.Pretty import Agda.Utils.Impossible data ReplEnv = ReplEnv { replSetupAction :: TCM () , replTypeCheckAction :: AbsolutePath -> TCM CheckResult } data ReplState = ReplState { currentFile :: Maybe AbsolutePath } newtype ReplM a = ReplM { unReplM :: ReaderT ReplEnv (StateT ReplState IM) a } deriving ( Functor, Applicative, Monad, MonadIO , HasOptions, MonadTCEnv, ReadTCState, MonadTCState, MonadTCM , MonadError TCErr , MonadReader ReplEnv, MonadState ReplState ) runReplM :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> ReplM () -> TCM () runReplM initialFile setup checkInterface = runIM . flip evalStateT (ReplState initialFile) . flip runReaderT replEnv . unReplM where replEnv = ReplEnv { replSetupAction = setup , replTypeCheckAction = checkInterface } data ExitCode a = Continue | ContinueIn TCEnv | Return a type Command a = (String, [String] -> ReplM (ExitCode a)) matchCommand :: String -> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a)) matchCommand x cmds = case List.filter (List.isPrefixOf x . fst) cmds of [(_,m)] -> Right m xs -> Left $ List.map fst xs interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a interaction prompt cmds eval = loop where go (Return x) = return x go Continue = loop go (ContinueIn env) = localTC (const env) loop loop = do ms <- ReplM $ lift $ lift $ 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 =<< (c args) Left [] -> do liftIO $ putStrLn $ "Unknown command '" ++ cmd ++ "'" loop Left xs -> do liftIO $ putStrLn $ "More than one command match: " ++ List.intercalate ", " xs loop Just _ -> do go =<< liftTCM (eval $ fromJust ms) `catchError` \e -> do s <- prettyError e liftIO $ putStrLn s loop runInteractionLoop :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM () runInteractionLoop initialFile setup check = runReplM initialFile setup check interactionLoop replSetup :: ReplM () replSetup = do liftTCM =<< asks replSetupAction liftIO $ putStr splashScreen checkCurrentFile :: ReplM (Maybe CheckResult) checkCurrentFile = traverse checkFile =<< gets currentFile checkFile :: AbsolutePath -> ReplM CheckResult checkFile file = liftTCM . ($ file) =<< asks replTypeCheckAction -- | The interaction loop. interactionLoop :: ReplM () interactionLoop = do -- Run the setup action replSetup reload interaction "Main> " commands evalTerm where reload :: ReplM () = do checked <- checkCurrentFile liftTCM $ setScope $ maybe emptyScopeInfo iInsideScope (crInterface <$> checked) -- Andreas, 2021-01-27, issue #5132, make Set and Prop available from Agda.Primitive -- if no module is loaded. when (isNothing checked) $ do -- @open import Agda.Primitive using (Set; Prop)@ void $ liftTCM importPrimitives `catchError` \e -> do s <- prettyError e liftIO $ putStrLn s liftIO $ putStrLn "Failed." commands = [ "quit" |> \_ -> return $ Return () , "?" |> \_ -> continueAfter $ liftIO $ help commands , "reload" |> \_ -> do reload ContinueIn <$> askTC , "constraints" |> \args -> continueAfter $ liftTCM $ showConstraints args , "Context" |> \args -> continueAfter $ liftTCM $ showContext args , "give" |> \args -> continueAfter $ liftTCM $ giveMeta args , "Refine" |> \args -> continueAfter $ liftTCM $ refineMeta args , "metas" |> \args -> continueAfter $ liftTCM $ showMetas args , "load" |> \args -> continueAfter $ loadFile reload args , "eval" |> \args -> continueAfter $ liftTCM $ evalIn args , "typeOf" |> \args -> continueAfter $ liftTCM $ typeOf args , "typeIn" |> \args -> continueAfter $ liftTCM $ typeIn args , "wakeup" |> \_ -> continueAfter $ liftTCM $ retryConstraints , "scope" |> \_ -> continueAfter $ liftTCM $ showScope ] where (|>) = (,) continueAfter :: ReplM a -> ReplM (ExitCode b) continueAfter m = withCurrentFile $ do m >> return Continue -- | Set 'envCurrentPath' to the repl's current file withCurrentFile :: ReplM a -> ReplM a withCurrentFile cont = do mpath <- gets currentFile localTC (\ e -> e { envCurrentPath = mpath }) cont loadFile :: ReplM () -> [String] -> ReplM () loadFile reload [file] = do absPath <- liftIO $ absolute file modify (\(ReplState _prevFile) -> ReplState (Just absPath)) withCurrentFile reload loadFile _ _ = liftIO $ putStrLn ":load file" showConstraints :: [String] -> TCM () showConstraints [] = do cs <- BasicOps.getConstraints liftIO $ putStrLn $ unlines (List.map prettyShow cs) showConstraints _ = liftIO $ putStrLn ":constraints [cid]" showMetas :: [String] -> TCM () showMetas [m] = do i <- InteractionId <$> readM m withInteractionId i $ do s <- typeOfMeta AsIs i r <- getInteractionRange i d <- prettyA s liftIO $ putStrLn $ render d ++ " " ++ prettyShow r showMetas [m,"normal"] = do i <- InteractionId <$> readM m withInteractionId i $ do s <- prettyA =<< typeOfMeta Normalised i r <- getInteractionRange i liftIO $ putStrLn $ render s ++ " " ++ prettyShow r showMetas [] = do interactionMetas <- typesOfVisibleMetas AsIs hiddenMetas <- typesOfHiddenMetas AsIs mapM_ (liftIO . print) =<< mapM showII interactionMetas mapM_ print' hiddenMetas where showII o = withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock o) $ prettyA o showM o = withMetaId (nmid $ outputFormId $ OutputForm noRange [] alwaysUnblock o) $ prettyA 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 $ nmid $ metaId x d <- showM x liftIO $ putStrLn $ render d ++ " [ at " ++ prettyShow r ++ " ]" showMetas _ = liftIO $ putStrLn $ ":meta [metaid]" showScope :: TCM () showScope = do scope <- getScope liftIO $ putStrLn $ prettyShow scope metaParseExpr :: InteractionId -> String -> TCM A.Expr metaParseExpr ii s = do m <- lookupInteractionId ii scope <- getMetaScope <$> lookupMeta m r <- getRange <$> lookupMeta m -- liftIO $ putStrLn $ prettyShow scope let pos = fromMaybe __IMPOSSIBLE__ (rStart r) e <- runPM $ 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 WithoutForce ii Nothing e return () giveMeta _ = liftIO $ putStrLn $ ": give" ++ " metaid expr" refineMeta :: [String] -> TCM () refineMeta s | length s >= 2 = do _ <- actOnMeta s $ \ ii e -> refine WithoutForce ii Nothing e return () refineMeta _ = liftIO $ putStrLn $ ": refine" ++ " metaid expr" retryConstraints :: TCM () retryConstraints = wakeupConstraints_ evalIn :: [String] -> TCM () evalIn s | length s >= 2 = do d <- actOnMeta s $ \_ e -> prettyA =<< evalInCurrent DefaultCompute e liftIO $ print d evalIn _ = liftIO $ putStrLn ":eval metaid expr" parseExpr :: String -> TCM A.Expr parseExpr s = do e <- runPM $ parse exprParser s localToAbstract e return evalTerm :: String -> TCM (ExitCode a) evalTerm s = do e <- parseExpr s v <- evalInCurrent DefaultCompute e e <- prettyTCM v liftIO $ print e return Continue typeOf :: [String] -> TCM () typeOf s = do e <- parseExpr (unwords s) e0 <- typeInCurrent Normalised e e1 <- typeInCurrent AsIs e liftIO . putStrLn =<< showA e1 typeIn :: [String] -> TCM () typeIn s@(_:_:_) = actOnMeta s $ \i e -> do e1 <- typeInMeta i Normalised e e2 <- typeInMeta i AsIs e liftIO . putStrLn =<< showA e1 typeIn _ = liftIO $ 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 I.unDom . 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 $ print $ text (argNameToString x) <+> ":" <+> d showContext _ = liftIO $ putStrLn ":Context meta" -- | The logo that prints when Agda is started in interactive mode. splashScreen :: String splashScreen = unlines [ " _ " , " ____ | |" , " / __ \\ | |" , " | |__| |___ __| | ___" , " | __ / _ \\/ _ |/ __\\ Agda Interactive" , " | | |/ /_\\ \\/_| / /_| \\" , " |_| |\\___ /____\\_____/ Type :? for help." , " __/ /" , " \\__/" , "" -- , "The interactive mode is no longer supported. Don't complain if it doesn't work." , "The interactive mode is no longer under active development. Use at your own risk." ] -- | The help message help :: [Command a] -> IO () help cs = putStr $ unlines $ [ "Command overview" ] ++ List.map explain cs ++ [ " Infer type of expression and evaluate it." ] where explain (x,_) = ":" ++ x -- Read ------------------------------------------------------------------- readM :: Read a => String -> TCM a readM s = maybe err return $ readMaybe s where err = throwError $ strMsg $ "Cannot parse: " ++ s strMsg = Exception noRange . text