{-# OPTIONS_GHC -fno-cse #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Interaction.InteractionTop
( module Agda.Interaction.InteractionTop
)
where
import Prelude hiding (null)
import Control.Concurrent
import Control.Concurrent.Async
import Control.Concurrent.STM.TChan
import Control.Concurrent.STM.TVar
import qualified Control.Exception as E
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State hiding (state)
import Control.Monad.STM
import qualified Data.Char as Char
import Data.Function
import qualified Data.List as List
import qualified Data.Map as Map
import System.Directory
import System.FilePath
import Agda.TypeChecking.Monad as TM
hiding (initState, setCommandLineOptions)
import qualified Agda.TypeChecking.Monad as TM
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings (runPM)
import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Parser
import Agda.Syntax.Common
import Agda.Syntax.Concrete as C
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Info (mkDefInfo)
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
import Agda.Syntax.Scope.Base
import Agda.Interaction.Base
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses as Lenses
import Agda.Interaction.MakeCase
import Agda.Interaction.SearchAbout
import Agda.Interaction.Response hiding (Function, ExtendedLambda)
import qualified Agda.Interaction.Response as R
import qualified Agda.Interaction.BasicOps as B
import Agda.Interaction.BasicOps hiding (whyInScope)
import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate)
import qualified Agda.Interaction.Imports as Imp
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Highlighting.LaTeX as LaTeX
import Agda.Compiler.Common (IsMain (..))
import Agda.Compiler.Backend
import Agda.Auto.Auto as Auto
import Agda.Utils.Except
( ExceptT
, mkExceptT
, MonadError(catchError)
, runExceptT
)
import Agda.Utils.Either
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Hash
import Agda.Utils.Lens
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.String
import Agda.Utils.Time
import Agda.Utils.Tuple
import Agda.Utils.Impossible
localStateCommandM :: CommandM a -> CommandM a
localStateCommandM m = do
cSt <- get
tcSt <- getTC
x <- m
putTC tcSt
put cSt
return x
liftLocalState :: TCM a -> CommandM a
liftLocalState = lift . localTCState
revLift
:: MonadState st m
=> (forall c . m c -> st -> k (c, st))
-> (forall b . k b -> m b)
-> (forall x . (m a -> k x) -> k x) -> m a
revLift run lift' f = do
st <- get
(a, st') <- lift' $ f (`run` st)
put st'
return a
revLiftTC
:: MonadTCState m
=> (forall c . m c -> TCState -> k (c, TCState))
-> (forall b . k b -> m b)
-> (forall x . (m a -> k x) -> k x) -> m a
revLiftTC run lift' f = do
st <- getTC
(a, st') <- lift' $ f (`run` st)
putTC st'
return a
commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ci_i = revLift runStateT lift $ \ct -> revLiftTC runSafeTCM liftIO $ ci_i . (. ct)
liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT f m = revLift runStateT lift $ f . ($ m)
liftCommandMTLocalState :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMTLocalState f = liftCommandMT f . localStateCommandM
putResponse :: Response -> CommandM ()
putResponse = lift . appInteractionOutputCallback
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints f = modify $ \ s ->
s { theInteractionPoints = f (theInteractionPoints s) }
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes f = modify $ \ s ->
s { oldInteractionScopes = f $ oldInteractionScopes s }
insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope ii scope = do
lift $ reportSLn "interaction.scope" 20 $ "inserting old interaction scope " ++ show ii
modifyOldInteractionScopes $ Map.insert ii scope
removeOldInteractionScope :: InteractionId -> CommandM ()
removeOldInteractionScope ii = do
lift $ reportSLn "interaction.scope" 20 $ "removing old interaction scope " ++ show ii
modifyOldInteractionScopes $ Map.delete ii
getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope ii = do
ms <- gets $ Map.lookup ii . oldInteractionScopes
case ms of
Nothing -> fail $ "not an old interaction point: " ++ show ii
Just scope -> return scope
handleCommand_ :: CommandM () -> CommandM ()
handleCommand_ = handleCommand id (return ())
handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
handleCommand wrap onFail cmd = handleNastyErrors $ wrap $ do
oldState <- getTC
cmd `catchErr` \ e -> do
onFail
handleErr e
lift $ do
newPersistentState <- useTC lensPersistentState
putTC oldState
lensPersistentState `setTCLens` newPersistentState
where
catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr m h = do
s <- get
(x, s') <- lift $ do runStateT m s
`catchError_` \ e ->
runStateT (h e) s
put s'
return x
handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors m = commandMToIO $ \ toIO -> do
let handle e =
Right <$>
(toIO $ handleErr $ Exception noRange $ text $ show e)
asyncHandler e@AsyncCancelled = return (Left e)
generalHandler (e :: E.SomeException) = handle e
r <- ((Right <$> toIO m) `E.catch` asyncHandler)
`E.catch` generalHandler
case r of
Right x -> return x
Left e -> E.throwIO e
handleErr e = do
unsolvedNotOK <- lift $ not . optAllowUnsolved <$> pragmaOptions
meta <- lift $ computeUnsolvedMetaWarnings
constr <- lift $ computeUnsolvedConstraints
err <- lift $ errorHighlighting e
modFile <- lift $ useTC stModuleToSource
method <- lift $ viewTC eHighlightingMethod
let info = compress $ mconcat $
err : if unsolvedNotOK then [meta, constr] else []
noError <- lift $ null <$> prettyError e
x <- lift $ optShowImplicit <$> useTC stPragmaOptions
unless noError $ mapM_ putResponse $
[ Resp_DisplayInfo $ Info_Error $ Info_GenericError e ] ++
tellEmacsToJumpToError (getRange e) ++
[ Resp_HighlightingInfo info KeepHighlighting
method modFile ] ++
[ Resp_Status $ Status { sChecked = False
, sShowImplicitArguments = x
} ]
runInteraction :: IOTCM -> CommandM ()
runInteraction (IOTCM current highlighting highlightingMethod cmd) =
handleCommand inEmacs onFail $ do
currentAbs <- liftIO $ absolute current
cf <- gets theCurrentFile
when (not (independent cmd) && Just currentAbs /= (fst <$> cf)) $
lift $ typeError $ GenericError "Error: First load the file."
withCurrentFile $ interpret cmd
cf' <- gets theCurrentFile
when (updateInteractionPointsAfter cmd
&&
Just currentAbs == (fst <$> cf')) $
putResponse . Resp_InteractionPoints =<< gets theInteractionPoints
where
inEmacs = liftCommandMT $ withEnv $ initEnv
{ envHighlightingLevel = highlighting
, envHighlightingMethod = highlightingMethod
}
onFail | independent cmd = modify $ \ s -> s { theCurrentFile = Nothing }
| otherwise = return ()
maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort m = do
commandState <- get
let q = commandQueue commandState
(n, cmd) <- liftIO $ atomically $ readTChan (commands q)
case cmd of
Done -> return Done
Error e -> return (Error e)
Command c -> do
tcState <- getTC
tcEnv <- askTC
result <- liftIO $ race
(runTCM tcEnv tcState $ runStateT (m c) commandState)
(waitForAbort n q)
case result of
Left ((x, commandState'), tcState') -> do
putTC tcState'
put commandState'
case c of
IOTCM _ _ _ Cmd_exit -> do
putResponse Resp_DoneExiting
return Done
_ -> return (Command (Just x))
Right a -> do
liftIO $ popAbortedCommands q a
putTC $ initState
{ stPersistentState = stPersistentState tcState
, stPreScopeState =
(stPreScopeState initState)
{ stPrePragmaOptions =
stPrePragmaOptions
(stPreScopeState tcState)
}
}
put $ (initCommandState (commandQueue commandState))
{ optionsOnReload = optionsOnReload commandState
}
putResponse Resp_DoneAborting
displayStatus
return (Command Nothing)
where
waitForAbort
:: Integer
-> CommandQueue
-> IO Integer
waitForAbort n q = do
atomically $ do
a <- readTVar (abort q)
case a of
Just a' | n <= a' -> return a'
_ -> retry
popAbortedCommands :: CommandQueue -> Integer -> IO ()
popAbortedCommands q n = do
done <- atomically $ do
cmd <- tryReadTChan (commands q)
case cmd of
Nothing -> return True
Just c ->
if fst c <= n then
return False
else do
unGetTChan (commands q) c
return True
unless done $
popAbortedCommands q n
initialiseCommandQueue
:: IO Command
-> IO CommandQueue
initialiseCommandQueue next = do
commands <- newTChanIO
abort <- newTVarIO Nothing
let
readCommands n = do
c <- next
case c of
Command (IOTCM _ _ _ Cmd_abort) -> do
atomically $ writeTVar abort (Just n)
readCommands n
_ -> do
n' <- return (succ n)
atomically $ writeTChan commands (n', c)
case c of
Done -> return ()
_ -> readCommands n'
_ <- forkIO (readCommands 0)
return (CommandQueue { .. })
independent :: Interaction -> Bool
independent (Cmd_load {}) = True
independent (Cmd_compile {}) = True
independent (Cmd_load_highlighting_info {}) = True
independent Cmd_tokenHighlighting {} = True
independent Cmd_show_version = True
independent _ = False
updateInteractionPointsAfter :: Interaction -> Bool
updateInteractionPointsAfter Cmd_load{} = True
updateInteractionPointsAfter Cmd_compile{} = True
updateInteractionPointsAfter Cmd_constraints{} = False
updateInteractionPointsAfter Cmd_metas{} = False
updateInteractionPointsAfter Cmd_show_module_contents_toplevel{} = False
updateInteractionPointsAfter Cmd_search_about_toplevel{} = False
updateInteractionPointsAfter Cmd_solveAll{} = True
updateInteractionPointsAfter Cmd_solveOne{} = True
updateInteractionPointsAfter Cmd_infer_toplevel{} = False
updateInteractionPointsAfter Cmd_compute_toplevel{} = False
updateInteractionPointsAfter Cmd_load_highlighting_info{} = False
updateInteractionPointsAfter Cmd_tokenHighlighting{} = False
updateInteractionPointsAfter Cmd_highlight{} = True
updateInteractionPointsAfter ShowImplicitArgs{} = False
updateInteractionPointsAfter ToggleImplicitArgs{} = False
updateInteractionPointsAfter Cmd_give{} = True
updateInteractionPointsAfter Cmd_refine{} = True
updateInteractionPointsAfter Cmd_intro{} = True
updateInteractionPointsAfter Cmd_refine_or_intro{} = True
updateInteractionPointsAfter Cmd_autoOne{} = True
updateInteractionPointsAfter Cmd_autoAll{} = True
updateInteractionPointsAfter Cmd_context{} = False
updateInteractionPointsAfter Cmd_helper_function{} = False
updateInteractionPointsAfter Cmd_infer{} = False
updateInteractionPointsAfter Cmd_goal_type{} = False
updateInteractionPointsAfter Cmd_elaborate_give{} = True
updateInteractionPointsAfter Cmd_goal_type_context{} = False
updateInteractionPointsAfter Cmd_goal_type_context_infer{} = False
updateInteractionPointsAfter Cmd_goal_type_context_check{} = False
updateInteractionPointsAfter Cmd_show_module_contents{} = False
updateInteractionPointsAfter Cmd_make_case{} = True
updateInteractionPointsAfter Cmd_compute{} = False
updateInteractionPointsAfter Cmd_why_in_scope{} = False
updateInteractionPointsAfter Cmd_why_in_scope_toplevel{} = False
updateInteractionPointsAfter Cmd_show_version{} = False
updateInteractionPointsAfter Cmd_abort{} = False
updateInteractionPointsAfter Cmd_exit{} = False
interpret :: Interaction -> CommandM ()
interpret (Cmd_load m argv) =
cmd_load' m argv True Imp.TypeCheck $ \_ -> interpret Cmd_metas
interpret (Cmd_compile backend file argv) =
cmd_load' file argv (backend `elem` [LaTeX, QuickLaTeX])
(if backend == QuickLaTeX
then Imp.ScopeCheck
else Imp.TypeCheck) $ \(i, mw) -> do
mw' <- lift $ Imp.applyFlagsToMaybeWarnings mw
case mw' of
Imp.NoWarnings -> do
lift $ case backend of
LaTeX -> LaTeX.generateLaTeX i
QuickLaTeX -> LaTeX.generateLaTeX i
OtherBackend "GHCNoMain" -> callBackend "GHC" NotMain i
OtherBackend b -> callBackend b IsMain i
display_info . Info_CompilationOk =<< lift getWarningsAndNonFatalErrors
Imp.SomeWarnings w -> display_info $ Info_Error $ Info_CompilationError w
interpret Cmd_constraints =
display_info . Info_Constraints =<< lift B.getConstraints
interpret Cmd_metas = do
ms <- lift B.getGoals
display_info . Info_AllGoalsWarnings ms =<< lift getWarningsAndNonFatalErrors
interpret (Cmd_show_module_contents_toplevel norm s) =
liftCommandMT B.atTopLevel $ showModuleContents norm noRange s
interpret (Cmd_search_about_toplevel norm s) =
liftCommandMT B.atTopLevel $ searchAbout norm noRange s
interpret (Cmd_solveAll norm) = solveInstantiatedGoals norm Nothing
interpret (Cmd_solveOne norm ii _ _) = solveInstantiatedGoals norm' (Just ii)
where norm' = case norm of
Simplified -> AsIs
Instantiated -> Simplified
_ -> norm
interpret (Cmd_infer_toplevel norm s) = do
(time, expr) <- parseAndDoAtToplevel (B.typeInCurrent norm) s
state <- get
display_info $ Info_InferredType state time expr
interpret (Cmd_compute_toplevel cmode s) = do
(time, expr) <- parseAndDoAtToplevel action (computeWrapInput cmode s)
state <- get
display_info $ Info_NormalForm state cmode time expr
where
action = allowNonTerminatingReductions
. (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
. B.evalInCurrent
interpret (ShowImplicitArgs showImpl) = do
opts <- lift commandLineOptions
setCommandLineOpts $
opts { optPragmaOptions =
(optPragmaOptions opts) { optShowImplicit = showImpl } }
interpret ToggleImplicitArgs = do
opts <- lift commandLineOptions
let ps = optPragmaOptions opts
setCommandLineOpts $
opts { optPragmaOptions =
ps { optShowImplicit = not $ optShowImplicit ps } }
interpret (Cmd_load_highlighting_info source) = do
l <- asksTC envHighlightingLevel
when (l /= None) $ do
setCommandLineOpts =<< lift commandLineOptions
resp <- lift $ liftIO . tellToUpdateHighlighting =<< do
ex <- liftIO $ doesFileExist source
absSource <- liftIO $ SourceFile <$> absolute source
case ex of
False -> return Nothing
True -> (do
si <- Imp.sourceInfo absSource
let m = Imp.siModuleName si
checkModuleName m absSource Nothing
mmi <- getVisitedModule m
case mmi of
Nothing -> return Nothing
Just mi ->
if hashText (Imp.siSource si) ==
iSourceHash (miInterface mi)
then do
modFile <- useTC stModuleToSource
method <- viewTC eHighlightingMethod
return $ Just (iHighlighting $ miInterface mi, method, modFile)
else
return Nothing)
`catchError`
\_ -> return Nothing
mapM_ putResponse resp
interpret (Cmd_tokenHighlighting source remove) = do
info <- do l <- asksTC envHighlightingLevel
if l == None
then return Nothing
else do
source' <- liftIO (absolute source)
lift $ (Just <$> generateTokenInfo source')
`catchError` \_ ->
return Nothing
`finally`
case remove of
Remove -> liftIO $ removeFile source
Keep -> return ()
case info of
Just info' -> lift $ printHighlightingInfo RemoveHighlighting info'
Nothing -> return ()
interpret (Cmd_highlight ii rng s) = do
l <- asksTC envHighlightingLevel
when (l /= None) $ do
scope <- getOldInteractionScope ii
removeOldInteractionScope ii
handle $ do
parsed <- try (Info_HighlightingParseError ii) $
B.parseExpr rng s
expr <- try (Info_HighlightingScopeCheckError ii) $
concreteToAbstract scope parsed
lift $ printHighlightingInfo KeepHighlighting =<<
generateTokenInfoFromString rng s
lift $ highlightExpr expr
where
handle :: ExceptT Info_Error TCM () -> CommandM ()
handle m = do
res <- lift $ runExceptT m
case res of
Left err -> display_info $ Info_Error err
Right _ -> return ()
try :: Info_Error -> TCM a -> ExceptT Info_Error TCM a
try err m = mkExceptT $ do
(mapLeft (const err) <$> freshTCM m) `catchError` \ _ -> return (Left err)
interpret (Cmd_give force ii rng s) = give_gen force ii rng s Give
interpret (Cmd_refine ii rng s) = give_gen WithoutForce ii rng s Refine
interpret (Cmd_intro pmLambda ii rng _) = do
ss <- lift $ B.introTactic pmLambda ii
liftCommandMT (B.withInteractionId ii) $ case ss of
[] -> do
display_info $ Info_Intro_NotFound
[s] -> give_gen WithoutForce ii rng s Intro
_:_:_ -> do
display_info $ Info_Intro_ConstructorUnknown ss
interpret (Cmd_refine_or_intro pmLambda ii r s) = interpret $
let s' = trim s
in (if null s' then Cmd_intro pmLambda else Cmd_refine) ii r s'
interpret (Cmd_autoOne ii rng hint) = do
st <- getTC
(time , res) <- maybeTimed $ Auto.auto ii rng hint
case autoProgress res of
Solutions sols -> do
lift $ reportSLn "auto" 10 $ "Auto produced the following solutions " ++ show sols
forM_ sols $ \(ii', sol) -> do
insertOldInteractionScope ii' =<< liftLocalState (putTC st >> getInteractionScope ii')
putResponse $ Resp_GiveAction ii' $ Give_String sol
modifyTheInteractionPoints (List.\\ (map fst sols))
case autoMessage res of
Nothing -> interpret Cmd_metas
Just msg -> display_info $ Info_Auto msg
FunClauses cs -> do
case autoMessage res of
Nothing -> return ()
Just msg -> display_info $ Info_Auto msg
putResponse $ Resp_MakeCase ii R.Function cs
Refinement s -> give_gen WithoutForce ii rng s Refine
maybe (return ()) (display_info . Info_Time) time
interpret Cmd_autoAll = do
iis <- getInteractionPoints
unless (null iis) $ do
let time = 1000 `div` length iis
st <- getTC
solved <- forM iis $ \ ii -> do
rng <- getInteractionRange ii
res <- Auto.auto ii rng ("-t " ++ show time ++ "ms")
case autoProgress res of
Solutions sols -> forM sols $ \ (jj, s) -> do
oldInteractionScope <- liftLocalState (putTC st >> getInteractionScope jj)
insertOldInteractionScope jj oldInteractionScope
putResponse $ Resp_GiveAction ii $ Give_String s
return jj
_ -> return []
modifyTheInteractionPoints (List.\\ concat solved)
interpret (Cmd_context norm ii _ _) =
display_info . Info_Context ii =<< liftLocalState (getResponseContext norm ii)
interpret (Cmd_helper_function norm ii rng s) = do
helperType <- liftLocalState $ B.withInteractionId ii $ inTopContext $ B.metaHelperType norm ii rng s
display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType)
interpret (Cmd_infer norm ii rng s) = do
expr <- liftLocalState $ B.withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s
display_info $ Info_GoalSpecific ii (Goal_InferredType expr)
interpret (Cmd_goal_type norm ii _ _) =
display_info $ Info_GoalSpecific ii (Goal_CurrentGoal norm)
interpret (Cmd_elaborate_give norm ii rng s) = do
have <- liftLocalState $ B.withInteractionId ii $ do
expr <- B.parseExprIn ii rng s
goal <- B.typeOfMeta AsIs ii
term <- case goal of
OfType _ ty -> checkExpr expr =<< isType_ ty
_ -> __IMPOSSIBLE__
nf <- normalForm norm term
txt <- localTC (\ e -> e { envPrintMetasBare = True }) (TCP.prettyTCM nf)
return $ show txt
give_gen WithoutForce ii rng have ElaborateGive
interpret (Cmd_goal_type_context norm ii rng s) =
cmd_goal_type_context_and GoalOnly norm ii rng s
interpret (Cmd_goal_type_context_infer norm ii rng s) = do
aux <- if all Char.isSpace s
then return GoalOnly
else do
typ <- liftLocalState
$ B.withInteractionId ii
$ B.typeInMeta ii norm =<< B.parseExprIn ii rng s
return (GoalAndHave typ)
cmd_goal_type_context_and aux norm ii rng s
interpret (Cmd_goal_type_context_check norm ii rng s) = do
term <- liftLocalState $ B.withInteractionId ii $ do
expr <- B.parseExprIn ii rng s
goal <- B.typeOfMeta AsIs ii
term <- case goal of
OfType _ ty -> checkExpr expr =<< isType_ ty
_ -> __IMPOSSIBLE__
normalForm norm term
cmd_goal_type_context_and (GoalAndElaboration term) norm ii rng s
interpret (Cmd_show_module_contents norm ii rng s) =
liftCommandMT (B.withInteractionId ii) $ showModuleContents norm rng s
interpret (Cmd_why_in_scope_toplevel s) =
liftCommandMT B.atTopLevel $ whyInScope s
interpret (Cmd_why_in_scope ii _range s) =
liftCommandMT (B.withInteractionId ii) $ whyInScope s
interpret (Cmd_make_case ii rng s) = do
(f, casectxt, cs) <- lift $ makeCase ii rng s
liftCommandMT (B.withInteractionId ii) $ do
tel <- lift $ lookupSection (qnameModule f)
unicode <- getsTC $ optUseUnicode . getPragmaOptions
pcs :: [Doc] <- lift $ inTopContext $ addContext tel $ mapM prettyA cs
let pcs' :: [String] = List.map (extlam_dropName unicode casectxt . decorate) pcs
lift $ reportSDoc "interaction.case" 60 $ TCP.vcat
[ "InteractionTop.Cmd_make_case"
, TCP.nest 2 $ TCP.vcat
[ "cs = " TCP.<+> TCP.vcat (map prettyA cs)
, "pcs = " TCP.<+> TCP.vcat (map return pcs)
, "pcs' = " TCP.<+> TCP.vcat (map TCP.text pcs')
]
]
lift $ reportSDoc "interaction.case" 90 $ TCP.vcat
[ "InteractionTop.Cmd_make_case"
, TCP.nest 2 $ TCP.vcat
[ "cs = " TCP.<+> TCP.text (show cs)
]
]
putResponse $ Resp_MakeCase ii (makeCaseVariant casectxt) pcs'
where
decorate = renderStyle (style { mode = OneLineMode })
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant Nothing = R.Function
makeCaseVariant Just{} = R.ExtendedLambda
extlam_dropName :: Bool -> CaseContext -> String -> String
extlam_dropName _ Nothing x = x
extlam_dropName unicode Just{} x
= unwords $ reverse $ replEquals $ reverse $ drop 1 $ words x
where
replEquals ("=" : ws)
| unicode = "→" : ws
| otherwise = "->" : ws
replEquals (w : ws) = w : replEquals ws
replEquals [] = []
interpret (Cmd_compute cmode ii rng s) = do
expr <- liftLocalState $ do
e <- B.parseExprIn ii rng (computeWrapInput cmode s)
B.withInteractionId ii $ applyWhen (computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent e
display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr)
interpret Cmd_show_version = display_info Info_Version
interpret Cmd_abort = return ()
interpret Cmd_exit = return ()
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals norm mii = do
out <- lift $ localTC (\ e -> e { envPrintMetasBare = True }) $ do
sip <- B.getSolvedInteractionPoints False norm
let sip' = maybe id (\ ii -> filter ((ii ==) . fst3)) mii sip
mapM prt sip'
putResponse $ Resp_SolveAll out
where
prt (i, m, e) = do
mi <- getMetaInfo <$> lookupMeta m
e' <- withMetaInfo mi $ abstractToConcreteCtx TopCtx e
return (i, e')
cmd_load' :: FilePath -> [String]
-> Bool
-> Imp.Mode
-> ((Interface, Imp.MaybeWarnings) -> CommandM ())
-> CommandM ()
cmd_load' file argv unsolvedOK mode cmd = do
f <- liftIO $ SourceFile <$> absolute file
ex <- liftIO $ doesFileExist $ filePath (srcFilePath f)
unless ex $ typeError $ GenericError $
"The file " ++ file ++ " was not found."
modify $ \ st -> st { theInteractionPoints = []
, theCurrentFile = Nothing
}
t <- liftIO $ getModificationTime file
si <- lift (Imp.sourceInfo f)
opts0 <- gets optionsOnReload
backends <- useTC stBackends
z <- liftIO $ runOptM $ parseBackendOptions backends argv opts0
case z of
Left err -> lift $ typeError $ GenericError err
Right (_, opts) -> do
let update o = o { optAllowUnsolved = unsolvedOK && optAllowUnsolved o}
root = projectRoot (srcFilePath f) (Imp.siModuleName si)
lift $ TM.setCommandLineOptions' root $ mapPragmaOptions update opts
displayStatus
lift resetState
putResponse Resp_ClearRunningInfo
putResponse (Resp_ClearHighlighting NotOnlyTokenBased)
ok <- lift $ Imp.typeCheckMain f mode si
t' <- liftIO $ getModificationTime file
when (t == t') $ do
is <- lift $ sortInteractionPoints =<< getInteractionPoints
modify $ \st -> st { theInteractionPoints = is
, theCurrentFile = Just (srcFilePath f, t)
}
cmd ok
withCurrentFile :: CommandM a -> CommandM a
withCurrentFile m = do
mfile <- fmap fst <$> gets theCurrentFile
localTC (\ e -> e { envCurrentPath = mfile }) m
data GiveRefine = Give | Refine | Intro | ElaborateGive
deriving (Eq, Show)
give_gen
:: UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> CommandM ()
give_gen force ii rng s0 giveRefine = do
let s = trim s0
lift $ reportSLn "interaction.give" 20 $ "give_gen " ++ s
unless (null s) $ do
let give_ref =
case giveRefine of
Give -> B.give
Refine -> B.refine
Intro -> B.refine
ElaborateGive -> B.give
scope <- lift $ getInteractionScope ii
(time, (ae, ae0, iis)) <- maybeTimed $ lift $ do
mis <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis
given <- B.parseExprIn ii rng s
ae <- give_ref force ii Nothing given
mis' <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'
return (ae, given, mis' List.\\ mis)
insertOldInteractionScope ii scope
iis' <- lift $ sortInteractionPoints iis
modifyTheInteractionPoints $ replace ii iis'
ce <- lift $ abstractToConcreteScope scope ae
lift $ reportS "interaction.give" 30
[ "ce = " ++ show ce
, "scopePrecedence = " ++ show (scope ^. scopePrecedence)
]
let literally = giveRefine /= Intro && giveRefine /= ElaborateGive && ae == ae0 && rng /= noRange
when literally $ lift $ do
l <- asksTC envHighlightingLevel
when (l /= None) $ do
printHighlightingInfo KeepHighlighting =<<
generateTokenInfoFromString rng s
highlightExpr ae
putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce
lift $ reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"
maybe (interpret Cmd_metas) (display_info . Info_Time) time
lift $ reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed"
where
replace x xs ys = concatMap (\ y -> if y == x then xs else [y]) ys
mkNewTxt True C.Paren{} = Give_Paren
mkNewTxt True _ = Give_NoParen
mkNewTxt False ce = Give_String $ prettyShow ce
highlightExpr :: A.Expr -> TCM ()
highlightExpr e =
localTC (\st -> st { envModuleNestingLevel = 0
, envHighlightingLevel = NonInteractive
, envHighlightingMethod = Direct }) $
generateAndPrintSyntaxInfo decl Full True
where
dummy = mkName_ (NameId 0 0) ("dummy" :: String)
info = mkDefInfo (nameConcrete dummy) noFixity' PublicAccess ConcreteDef (getRange e)
decl = A.Axiom NoFunSig info defaultArgInfo Nothing (qnameFromList [dummy]) e
sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
sortInteractionPoints is =
map fst . List.sortBy (compare `on` snd) <$> do
forM is $ \ i -> do
(i,) <$> getInteractionRange i
cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range ->
String -> CommandM ()
cmd_goal_type_context_and aux norm ii _ _ = do
ctx <- lift $ getResponseContext norm ii
constr <- lift $ lookupInteractionId ii >>= B.getConstraintsMentioning norm
boundary <- lift $ B.getIPBoundary norm ii
display_info $ Info_GoalSpecific ii (Goal_GoalType norm aux ctx boundary constr)
showModuleContents :: Rewrite -> Range -> String -> CommandM ()
showModuleContents norm rng s = do
(modules, tel, types) <- lift $ B.moduleContents norm rng s
display_info $ Info_ModuleContents modules tel types
searchAbout :: Rewrite -> Range -> String -> CommandM ()
searchAbout norm rg names = do
let trimmedNames = trim names
unless (null trimmedNames) $ do
hits <- lift $ B.atTopLevel $ findMentions norm rg trimmedNames
display_info $ Info_SearchAbout hits trimmedNames
whyInScope :: String -> CommandM ()
whyInScope s = do
Just (file, _) <- gets theCurrentFile
let cwd = takeDirectory (filePath file)
(v, xs, ms) <- liftLocalState (B.whyInScope s)
display_info $ Info_WhyInScope s cwd v xs ms
setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts opts = do
lift $ TM.setCommandLineOptions opts
displayStatus
status :: CommandM Status
status = do
cf <- gets theCurrentFile
showImpl <- lift showImplicitArguments
checked <- lift $ case cf of
Nothing -> return False
Just (f, t) -> do
t' <- liftIO $ getModificationTime $ filePath f
case t == t' of
False -> return False
True -> do
mm <- lookupModuleFromSource f
case mm of
Nothing -> return False
Just m -> maybe False (not . miWarnings) <$> getVisitedModule m
return $ Status { sShowImplicitArguments = showImpl
, sChecked = checked
}
displayStatus :: CommandM ()
displayStatus =
putResponse . Resp_Status =<< status
display_info :: DisplayInfo -> CommandM ()
display_info info = do
displayStatus
putResponse $ Resp_DisplayInfo info
parseAndDoAtToplevel
:: (A.Expr -> TCM a)
-> String
-> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel cmd s = do
localStateCommandM $ do
e <- lift $ runPM $ parse exprParser s
maybeTimed $ lift $ B.atTopLevel $ do
cmd =<< concreteToAbstract_ e
maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed work = do
doTime <- lift $ hasVerbosity "profile.interactive" 10
if not doTime
then (Nothing,) <$> work
else do
(r, time) <- measureTime work
return (Just time, r)
tellToUpdateHighlighting
:: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
tellToUpdateHighlighting Nothing = return []
tellToUpdateHighlighting (Just (info, method, modFile)) =
return [Resp_HighlightingInfo info KeepHighlighting method modFile]
tellEmacsToJumpToError :: Range -> [Response]
tellEmacsToJumpToError r =
case rStart r of
Nothing -> []
Just (Pn { srcFile = Strict.Nothing }) -> []
Just (Pn { srcFile = Strict.Just f, posPos = p }) ->
[ Resp_JumpToError (filePath f) p ]