1
2module Agda.Interaction.CommandLine
3  ( runInteractionLoop
4  ) where
5
6import Control.Monad.Except
7import Control.Monad.State
8import Control.Monad.Reader
9
10import qualified Data.List as List
11import Data.Maybe
12
13import Text.Read (readMaybe)
14
15import Agda.Interaction.Base hiding (Command)
16import Agda.Interaction.BasicOps as BasicOps hiding (parseExpr)
17import Agda.Interaction.Imports ( CheckResult, crInterface )
18import Agda.Interaction.Monad
19
20import qualified Agda.Syntax.Abstract as A
21import Agda.Syntax.Common
22import Agda.Syntax.Internal (telToList, alwaysUnblock)
23import qualified Agda.Syntax.Internal as I
24import Agda.Syntax.Parser
25import Agda.Syntax.Position
26import Agda.Syntax.Scope.Base
27import Agda.Syntax.Translation.ConcreteToAbstract
28import Agda.Syntax.Abstract.Pretty
29
30import Agda.TypeChecking.Constraints
31import Agda.TypeChecking.Monad
32import Agda.TypeChecking.Reduce
33import Agda.TypeChecking.Errors
34import Agda.TypeChecking.Pretty ( PrettyTCM(prettyTCM) )
35import Agda.TypeChecking.Substitute
36import Agda.TypeChecking.Warnings (runPM)
37
38import Agda.Utils.FileName (absolute, AbsolutePath)
39import Agda.Utils.Maybe (caseMaybeM)
40import Agda.Utils.Pretty
41
42import Agda.Utils.Impossible
43
44data ReplEnv = ReplEnv
45    { replSetupAction     :: TCM ()
46    , replTypeCheckAction :: AbsolutePath -> TCM CheckResult
47    }
48
49data ReplState = ReplState
50    { currentFile :: Maybe AbsolutePath
51    }
52
53newtype ReplM a = ReplM { unReplM :: ReaderT ReplEnv (StateT ReplState IM) a }
54    deriving
55    ( Functor, Applicative, Monad, MonadIO
56    , HasOptions, MonadTCEnv, ReadTCState, MonadTCState, MonadTCM
57    , MonadError TCErr
58    , MonadReader ReplEnv, MonadState ReplState
59    )
60
61runReplM :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> ReplM () -> TCM ()
62runReplM initialFile setup checkInterface
63    = runIM
64    . flip evalStateT (ReplState initialFile)
65    . flip runReaderT replEnv
66    . unReplM
67  where
68  replEnv = ReplEnv
69    { replSetupAction     = setup
70    , replTypeCheckAction = checkInterface
71    }
72
73data ExitCode a = Continue | ContinueIn TCEnv | Return a
74
75type Command a = (String, [String] -> ReplM (ExitCode a))
76
77matchCommand :: String -> [Command a] -> Either [String] ([String] -> ReplM (ExitCode a))
78matchCommand x cmds =
79    case List.filter (List.isPrefixOf x . fst) cmds of
80        [(_,m)] -> Right m
81        xs      -> Left $ List.map fst xs
82
83interaction :: String -> [Command a] -> (String -> TCM (ExitCode a)) -> ReplM a
84interaction prompt cmds eval = loop
85    where
86        go (Return x)       = return x
87        go Continue         = loop
88        go (ContinueIn env) = localTC (const env) loop
89
90        loop =
91            do  ms <- ReplM $ lift $ lift $ readline prompt
92                case fmap words ms of
93                    Nothing               -> return $ error "** EOF **"
94                    Just []               -> loop
95                    Just ((':':cmd):args) ->
96                        do  case matchCommand cmd cmds of
97                                Right c -> go =<< (c args)
98                                Left [] ->
99                                    do  liftIO $ putStrLn $ "Unknown command '" ++ cmd ++ "'"
100                                        loop
101                                Left xs ->
102                                    do  liftIO $ putStrLn $ "More than one command match: " ++
103                                                            List.intercalate ", " xs
104                                        loop
105                    Just _ ->
106                        do  go =<< liftTCM (eval $ fromJust ms)
107            `catchError` \e ->
108                do  s <- prettyError e
109                    liftIO $ putStrLn s
110                    loop
111
112runInteractionLoop :: Maybe AbsolutePath -> TCM () -> (AbsolutePath -> TCM CheckResult) -> TCM ()
113runInteractionLoop initialFile setup check = runReplM initialFile setup check interactionLoop
114
115replSetup :: ReplM ()
116replSetup = do
117    liftTCM =<< asks replSetupAction
118    liftIO $ putStr splashScreen
119
120checkCurrentFile :: ReplM (Maybe CheckResult)
121checkCurrentFile = traverse checkFile =<< gets currentFile
122
123checkFile :: AbsolutePath -> ReplM CheckResult
124checkFile file = liftTCM . ($ file) =<< asks replTypeCheckAction
125
126-- | The interaction loop.
127interactionLoop :: ReplM ()
128interactionLoop = do
129    -- Run the setup action
130    replSetup
131    reload
132    interaction "Main> " commands evalTerm
133    where
134        reload :: ReplM () = do
135            checked <- checkCurrentFile
136            liftTCM $ setScope $ maybe emptyScopeInfo iInsideScope (crInterface <$> checked)
137            -- Andreas, 2021-01-27, issue #5132, make Set and Prop available from Agda.Primitive
138            -- if no module is loaded.
139            when (isNothing checked) $ do
140              -- @open import Agda.Primitive using (Set; Prop)@
141              void $ liftTCM importPrimitives
142          `catchError` \e -> do
143            s <- prettyError e
144            liftIO $ putStrLn s
145            liftIO $ putStrLn "Failed."
146
147        commands =
148            [ "quit"        |>  \_ -> return $ Return ()
149            , "?"           |>  \_ -> continueAfter $ liftIO $ help commands
150            , "reload"      |>  \_ -> do reload
151                                         ContinueIn <$> askTC
152            , "constraints" |> \args -> continueAfter $ liftTCM $ showConstraints args
153            , "Context"     |> \args -> continueAfter $ liftTCM $ showContext args
154            , "give"        |> \args -> continueAfter $ liftTCM $ giveMeta args
155            , "Refine"      |> \args -> continueAfter $ liftTCM $ refineMeta args
156            , "metas"       |> \args -> continueAfter $ liftTCM $ showMetas args
157            , "load"        |> \args -> continueAfter $ loadFile reload args
158            , "eval"        |> \args -> continueAfter $ liftTCM $ evalIn args
159            , "typeOf"      |> \args -> continueAfter $ liftTCM $ typeOf args
160            , "typeIn"      |> \args -> continueAfter $ liftTCM $ typeIn args
161            , "wakeup"      |> \_ -> continueAfter $ liftTCM $ retryConstraints
162            , "scope"       |> \_ -> continueAfter $ liftTCM $ showScope
163            ]
164            where
165                (|>) = (,)
166
167continueAfter :: ReplM a -> ReplM (ExitCode b)
168continueAfter m = withCurrentFile $ do
169  m >> return Continue
170
171-- | Set 'envCurrentPath' to the repl's current file
172withCurrentFile :: ReplM a -> ReplM a
173withCurrentFile cont = do
174  mpath <- gets currentFile
175  localTC (\ e -> e { envCurrentPath = mpath }) cont
176
177loadFile :: ReplM () -> [String] -> ReplM ()
178loadFile reload [file] = do
179  absPath <- liftIO $ absolute file
180  modify (\(ReplState _prevFile) -> ReplState (Just absPath))
181  withCurrentFile reload
182loadFile _ _ = liftIO $ putStrLn ":load file"
183
184showConstraints :: [String] -> TCM ()
185showConstraints [] =
186    do  cs <- BasicOps.getConstraints
187        liftIO $ putStrLn $ unlines (List.map prettyShow cs)
188showConstraints _ = liftIO $ putStrLn ":constraints [cid]"
189
190
191showMetas :: [String] -> TCM ()
192showMetas [m] =
193    do  i <- InteractionId <$> readM m
194        withInteractionId i $ do
195          s <- typeOfMeta AsIs i
196          r <- getInteractionRange i
197          d <- prettyA s
198          liftIO $ putStrLn $ render d ++ " " ++ prettyShow r
199showMetas [m,"normal"] =
200    do  i <- InteractionId <$> readM m
201        withInteractionId i $ do
202          s <- prettyA =<< typeOfMeta Normalised i
203          r <- getInteractionRange i
204          liftIO $ putStrLn $ render s ++ " " ++ prettyShow r
205showMetas [] =
206    do  interactionMetas <- typesOfVisibleMetas AsIs
207        hiddenMetas      <- typesOfHiddenMetas  AsIs
208        mapM_ (liftIO . print) =<< mapM showII interactionMetas
209        mapM_ print' hiddenMetas
210    where
211        showII o = withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock o) $ prettyA o
212        showM  o = withMetaId (nmid $ outputFormId $ OutputForm noRange [] alwaysUnblock o) $ prettyA o
213
214        metaId (OfType i _) = i
215        metaId (JustType i) = i
216        metaId (JustSort i) = i
217        metaId (Assign i e) = i
218        metaId _ = __IMPOSSIBLE__
219        print' x = do
220            r <- getMetaRange $ nmid $ metaId x
221            d <- showM x
222            liftIO $ putStrLn $ render d ++ "  [ at " ++ prettyShow r ++ " ]"
223showMetas _ = liftIO $ putStrLn $ ":meta [metaid]"
224
225
226showScope :: TCM ()
227showScope = do
228  scope <- getScope
229  liftIO $ putStrLn $ prettyShow scope
230
231metaParseExpr ::  InteractionId -> String -> TCM A.Expr
232metaParseExpr ii s =
233    do  m <- lookupInteractionId ii
234        scope <- getMetaScope <$> lookupMeta m
235        r <- getRange <$> lookupMeta m
236        -- liftIO $ putStrLn $ prettyShow scope
237        let pos = fromMaybe __IMPOSSIBLE__ (rStart r)
238        e <- runPM $ parsePosString exprParser pos s
239        concreteToAbstract scope e
240
241actOnMeta :: [String] -> (InteractionId -> A.Expr -> TCM a) -> TCM a
242actOnMeta (is:es) f =
243     do  i <- readM is
244         let ii = InteractionId i
245         e <- metaParseExpr ii (unwords es)
246         withInteractionId ii $ f ii e
247actOnMeta _ _ = __IMPOSSIBLE__
248
249
250giveMeta :: [String] -> TCM ()
251giveMeta s | length s >= 2 = do
252  _ <- actOnMeta s $ \ ii e -> give WithoutForce ii Nothing e
253  return ()
254giveMeta _ = liftIO $ putStrLn $ ": give" ++ " metaid expr"
255
256
257
258refineMeta :: [String] -> TCM ()
259refineMeta s | length s >= 2 = do
260  _ <- actOnMeta s $ \ ii e -> refine WithoutForce ii Nothing e
261  return ()
262refineMeta _ = liftIO $ putStrLn $ ": refine" ++ " metaid expr"
263
264
265
266retryConstraints :: TCM ()
267retryConstraints = wakeupConstraints_
268
269
270evalIn :: [String] -> TCM ()
271evalIn s | length s >= 2 =
272    do  d <- actOnMeta s $ \_ e -> prettyA =<< evalInCurrent DefaultCompute e
273        liftIO $ print d
274evalIn _ = liftIO $ putStrLn ":eval metaid expr"
275
276parseExpr :: String -> TCM A.Expr
277parseExpr s = do
278    e <- runPM $ parse exprParser s
279    localToAbstract e return
280
281evalTerm :: String -> TCM (ExitCode a)
282evalTerm s =
283    do  e <- parseExpr s
284        v <- evalInCurrent DefaultCompute e
285        e <- prettyTCM v
286        liftIO $ print e
287        return Continue
288
289typeOf :: [String] -> TCM ()
290typeOf s =
291    do  e  <- parseExpr (unwords s)
292        e0 <- typeInCurrent Normalised e
293        e1 <- typeInCurrent AsIs e
294        liftIO . putStrLn =<< showA e1
295
296typeIn :: [String] -> TCM ()
297typeIn s@(_:_:_) =
298    actOnMeta s $ \i e ->
299    do  e1 <- typeInMeta i Normalised e
300        e2 <- typeInMeta i AsIs e
301        liftIO . putStrLn =<< showA e1
302typeIn _ = liftIO $ putStrLn ":typeIn meta expr"
303
304showContext :: [String] -> TCM ()
305showContext (meta:args) = do
306    i <- InteractionId <$> readM meta
307    mi <- lookupMeta =<< lookupInteractionId i
308    withMetaInfo (getMetaInfo mi) $ do
309      ctx <- List.map I.unDom . telToList <$> getContextTelescope
310      zipWithM_ display ctx $ reverse $ zipWith const [1..] ctx
311    where
312        display (x, t) n = do
313            t <- case args of
314                    ["normal"] -> normalise $ raise n t
315                    _          -> return $ raise n t
316            d <- prettyTCM t
317            liftIO $ print $ text (argNameToString x) <+> ":" <+> d
318showContext _ = liftIO $ putStrLn ":Context meta"
319
320-- | The logo that prints when Agda is started in interactive mode.
321splashScreen :: String
322splashScreen = unlines
323    [ "                 _ "
324    , "   ____         | |"
325    , "  / __ \\        | |"
326    , " | |__| |___  __| | ___"
327    , " |  __  / _ \\/ _  |/ __\\     Agda Interactive"
328    , " | |  |/ /_\\ \\/_| / /_| \\"
329    , " |_|  |\\___  /____\\_____/    Type :? for help."
330    , "        __/ /"
331    , "        \\__/"
332    , ""
333    -- , "The interactive mode is no longer supported. Don't complain if it doesn't work."
334    , "The interactive mode is no longer under active development. Use at your own risk."
335    ]
336
337-- | The help message
338help :: [Command a] -> IO ()
339help cs = putStr $ unlines $
340    [ "Command overview" ] ++ List.map explain cs ++
341    [ "<exp> Infer type of expression <exp> and evaluate it." ]
342    where
343        explain (x,_) = ":" ++ x
344
345-- Read -------------------------------------------------------------------
346
347readM :: Read a => String -> TCM a
348readM s = maybe err return $ readMaybe s
349  where
350  err    = throwError $ strMsg $ "Cannot parse: " ++ s
351  strMsg = Exception noRange . text
352