{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -fno-cse #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Interaction.InteractionTop
( module Agda.Interaction.InteractionTop
)
where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Concurrent
import Control.Concurrent.Async
import Control.Concurrent.STM.TChan
import qualified Control.Exception as E
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.STM
import qualified Data.Char as Char
import Data.Foldable (Foldable)
import Data.Function
import qualified Data.List as List
import Data.Maybe
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid
import Data.Traversable (Traversable)
import qualified Data.Traversable as Trav
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.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Parser
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Generic as C
import Agda.Syntax.Concrete.Pretty ()
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty
import qualified Agda.Syntax.Internal as I
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.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 (Postulate)
import qualified Agda.Interaction.Imports as Imp
import Agda.TypeChecking.Warnings
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Highlighting.LaTeX as LaTeX
import qualified Agda.Interaction.Highlighting.Range as H
import Agda.Compiler.Common (IsMain (..))
import Agda.Compiler.Backend
import Agda.Auto.Auto as Auto
import Agda.Utils.Except
( ExceptT
, mkExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.Either
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Hash
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Lens
import Agda.Utils.Maybe
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
#include "undefined.h"
import Agda.Utils.Impossible
data CommandState = CommandState
{ theInteractionPoints :: [InteractionId]
, theCurrentFile :: Maybe (AbsolutePath, ClockTime)
, optionsOnReload :: CommandLineOptions
, oldInteractionScopes :: !OldInteractionScopes
, commandQueue :: CommandQueue
}
type OldInteractionScopes = Map InteractionId ScopeInfo
initCommandState :: CommandQueue -> CommandState
initCommandState commandQueue =
CommandState
{ theInteractionPoints = []
, theCurrentFile = Nothing
, optionsOnReload = defaultOptions
, oldInteractionScopes = Map.empty
, commandQueue = commandQueue
}
type CommandM = StateT CommandState TCM
localStateCommandM :: CommandM a -> CommandM a
localStateCommandM m = do
cSt <- get
tcSt <- lift $ get
x <- m
lift $ put tcSt
put cSt
return x
liftLocalState :: TCM a -> CommandM a
liftLocalState = lift . localState
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
commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ci_i = revLift runStateT lift $ \ct -> revLift runSafeTCM liftIO $ ci_i . (. ct)
liftCommandMT :: (forall a . TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT f m = revLift runStateT lift $ f . ($ m)
liftCommandMTLocalState :: (forall a . TCM a -> TCM a) -> 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 <- lift get
cmd `catchErr` \ e -> do
onFail
handleErr e
lift $ do
newPersistentState <- use lensPersistentState
put oldState
lensPersistentState .= newPersistentState
where
catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr m h = do
s <- get
(x, s') <- lift $ do disableDestructiveUpdate (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 $ use stModuleToSource
method <- lift $ view eHighlightingMethod
let info = compress $ mconcat $
err : if unsolvedNotOK then [meta, constr] else []
s1 <- lift $ prettyError e
s2 <- lift $ prettyTCWarnings' =<< Imp.errorWarningsOfTCErr e
let s = List.intercalate "\n" $ filter (not . null) $ s1 : s2
x <- lift $ optShowImplicit <$> use stPragmaOptions
unless (null s1) $ mapM_ putResponse $
[ Resp_DisplayInfo $ Info_Error s ] ++
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
current <- liftIO $ absolute current
cf <- gets theCurrentFile
when (not (independent cmd) && Just current /= (fst <$> cf)) $
lift $ typeError $ GenericError "Error: First load the file."
withCurrentFile $ interpret cmd
cf <- gets theCurrentFile
when (updateInteractionPointsAfter cmd
&&
Just current == (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 ()
data Command
= Command IOTCM
| Done
| Error String
deriving Show
type CommandQueue = TChan Command
nextCommand :: CommandM Command
nextCommand =
liftIO . atomically . readTChan =<< gets commandQueue
maybeAbort :: CommandM () -> CommandM ()
maybeAbort c = do
commandState <- get
tcState <- lift get
tcEnv <- lift ask
result <- liftIO $ race
(runTCM tcEnv tcState $ runStateT c commandState)
(waitForAbort $ commandQueue commandState)
case result of
Left (((), commandState), tcState) -> do
lift $ put tcState
put commandState
Right () -> do
lift $ put $ initState
{ stPersistentState = stPersistentState tcState
, stPreScopeState =
(stPreScopeState initState)
{ stPrePragmaOptions =
stPrePragmaOptions
(stPreScopeState tcState)
}
}
put $ (initCommandState (commandQueue commandState))
{ optionsOnReload = optionsOnReload commandState
}
putResponse Resp_DoneAborting
displayStatus
where
waitForAbort :: CommandQueue -> IO ()
waitForAbort q = atomically $ do
c <- peekTChan q
case c of
Command (IOTCM _ _ _ Cmd_abort) -> void $ readTChan q
_ -> retry
initialiseCommandQueue
:: IO Command
-> IO CommandQueue
initialiseCommandQueue next = do
q <- newTChanIO
let readCommands = do
c <- next
atomically $ writeTChan q c
case c of
Done -> return ()
_ -> readCommands
_ <- forkIO readCommands
return q
type Interaction = Interaction' Range
data Interaction' range
= Cmd_load FilePath [String]
| Cmd_compile CompilerBackend FilePath [String]
| Cmd_constraints
| Cmd_metas
| Cmd_show_module_contents_toplevel
B.Rewrite
String
| Cmd_search_about_toplevel B.Rewrite String
| Cmd_solveAll B.Rewrite
| Cmd_solveOne B.Rewrite InteractionId range String
| Cmd_infer_toplevel B.Rewrite
String
| Cmd_compute_toplevel B.ComputeMode
String
| Cmd_load_highlighting_info
FilePath
| Cmd_tokenHighlighting FilePath Remove
| Cmd_highlight InteractionId range String
| ShowImplicitArgs Bool
| ToggleImplicitArgs
| Cmd_give UseForce InteractionId range String
| Cmd_refine InteractionId range String
| Cmd_intro Bool InteractionId range String
| Cmd_refine_or_intro Bool InteractionId range String
| Cmd_auto InteractionId range String
| Cmd_context B.Rewrite InteractionId range String
| Cmd_helper_function B.Rewrite InteractionId range String
| Cmd_infer B.Rewrite InteractionId range String
| Cmd_goal_type B.Rewrite InteractionId range String
| Cmd_goal_type_context B.Rewrite InteractionId range String
| Cmd_goal_type_context_infer
B.Rewrite InteractionId range String
| Cmd_goal_type_context_check
B.Rewrite InteractionId range String
| Cmd_show_module_contents
B.Rewrite InteractionId range String
| Cmd_make_case InteractionId range String
| Cmd_compute B.ComputeMode
InteractionId range String
| Cmd_why_in_scope InteractionId range String
| Cmd_why_in_scope_toplevel String
| Cmd_show_version
| Cmd_abort
deriving (Show, Read, Functor, Foldable, Traversable)
type IOTCM = IOTCM' Range
data IOTCM' range
= IOTCM
FilePath
HighlightingLevel
HighlightingMethod
(Interaction' range)
deriving (Show, Read, Functor, Foldable, Traversable)
data Remove
= Remove
| Keep
deriving (Show, Read)
type Parse a = ExceptT String (StateT String Identity) a
readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a
readsToParse s f = do
st <- lift get
case f st of
Nothing -> throwError s
Just (a, st) -> do
lift $ put st
return a
parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)]
parseToReadsPrec p i s = case runIdentity . flip runStateT s . runExceptT $ parens' p of
(Right a, s) -> [(a,s)]
_ -> []
exact :: String -> Parse ()
exact s = readsToParse (show s) $ fmap (\x -> ((),x)) . List.stripPrefix s . dropWhile (==' ')
readParse :: Read a => Parse a
readParse = readsToParse "read failed" $ listToMaybe . reads
parens' :: Parse a -> Parse a
parens' p = do
exact "("
x <- p
exact ")"
return x
`mplus`
p
instance Read InteractionId where
readsPrec = parseToReadsPrec $
fmap InteractionId readParse
instance Read a => Read (Range' a) where
readsPrec = parseToReadsPrec $
(exact "intervalsToRange" >>
liftM2 intervalsToRange readParse readParse)
`mplus`
(exact "noRange" >> return noRange)
instance Read a => Read (Interval' a) where
readsPrec = parseToReadsPrec $ do
exact "Interval"
liftM2 Interval readParse readParse
instance Read AbsolutePath where
readsPrec = parseToReadsPrec $ do
exact "mkAbsolute"
fmap mkAbsolute readParse
instance Read a => Read (Position' a) where
readsPrec = parseToReadsPrec $ do
exact "Pn"
liftM4 Pn readParse readParse readParse readParse
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_auto{} = True
updateInteractionPointsAfter Cmd_context{} = False
updateInteractionPointsAfter Cmd_helper_function{} = False
updateInteractionPointsAfter Cmd_infer{} = False
updateInteractionPointsAfter Cmd_goal_type{} = False
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
interpret :: Interaction -> CommandM ()
interpret (Cmd_load m argv) =
cmd_load' m argv True Imp.TypeCheck $ \_ -> interpret Cmd_metas
interpret (Cmd_compile b file argv) =
cmd_load' file argv (b `elem` [LaTeX, QuickLaTeX])
(if b == QuickLaTeX
then Imp.ScopeCheck
else Imp.TypeCheck) $ \(i, mw) -> do
mw <- lift $ Imp.applyFlagsToMaybeWarnings RespectFlags mw
case mw of
Imp.NoWarnings -> do
lift $ case b of
LaTeX -> LaTeX.generateLaTeX i
QuickLaTeX -> LaTeX.generateLaTeX i
OtherBackend "GHCNoMain" -> callBackend "GHC" NotMain i
OtherBackend b -> callBackend b IsMain i
(pwe, pwa) <- interpretWarnings
display_info $ Info_CompilationOk pwa pwe
Imp.SomeWarnings w -> do
pw <- lift $ prettyTCWarnings w
display_info $ Info_Error $ unlines
[ "You need to fix the following errors before you can compile"
, "the module:"
, ""
, pw
]
interpret Cmd_constraints =
display_info . Info_Constraints . unlines . map show =<< lift B.getConstraints
interpret Cmd_metas = do
unsolvedNotOK <- lift $ not . optAllowUnsolved <$> pragmaOptions
ms <- lift showOpenMetas
(pwe, pwa) <- interpretWarnings
display_info $ Info_AllGoalsWarnings (unlines ms) pwa pwe
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) =
parseAndDoAtToplevel (prettyA <=< B.typeInCurrent norm) Info_InferredType s
interpret (Cmd_compute_toplevel cmode s) =
parseAndDoAtToplevel action Info_NormalForm $ computeWrapInput cmode s
where
action = allowNonTerminatingReductions
. (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
. (B.showComputed cmode <=< 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 <- envHighlightingLevel <$> ask
when (l /= None) $ do
setCommandLineOpts =<< lift commandLineOptions
resp <- lift $ liftIO . tellToUpdateHighlighting =<< do
ex <- liftIO $ doesFileExist source
absSource <- liftIO $ absolute source
case ex of
False -> return Nothing
True -> do
mmi <- (getVisitedModule =<<
moduleName absSource)
`catchError`
\_ -> return Nothing
case mmi of
Nothing -> return Nothing
Just mi -> do
sourceH <- liftIO $ hashFile absSource
if sourceH == iSourceHash (miInterface mi)
then do
modFile <- use stModuleToSource
method <- view eHighlightingMethod
return $ Just (iHighlighting $ miInterface mi, method, modFile)
else
return Nothing
mapM_ putResponse resp
interpret (Cmd_tokenHighlighting source remove) = do
info <- do l <- envHighlightingLevel <$> ask
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 <- envHighlightingLevel <$> ask
when (l /= None) $ do
scope <- getOldInteractionScope ii
removeOldInteractionScope ii
handle $ do
e <- try ("Highlighting failed to parse expression in " ++ show ii) $
B.parseExpr rng s
e <- try ("Highlighting failed to scope check expression in " ++ show ii) $
concreteToAbstract scope e
lift $ printHighlightingInfo KeepHighlighting =<<
generateTokenInfoFromString rng s
lift $ highlightExpr e
where
handle :: ExceptT String TCM () -> CommandM ()
handle m = do
res <- lift $ runExceptT m
case res of
Left s -> display_info $ Info_Error s
Right _ -> return ()
try :: String -> TCM a -> ExceptT String 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 $ text "No introduction forms found."
[s] -> give_gen WithoutForce ii rng s Intro
_:_:_ -> do
display_info $ Info_Intro $
sep [ text "Don't know which constructor to introduce of"
, let mkOr [] = []
mkOr [x, y] = [text x <+> text "or" <+> text y]
mkOr (x:xs) = text x : mkOr xs
in nest 2 $ fsep $ punctuate comma (mkOr 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_auto ii rng s) = do
st <- lift $ get
(time , res) <- maybeTimed $ lift $ Auto.auto ii rng s
case autoProgress res of
Solutions sols -> do
lift $ reportSLn "auto" 10 $ "Auto produced the following solutions " ++ show sols
forM_ sols $ \(ii, s) -> do
insertOldInteractionScope ii =<< liftLocalState (put st >> getInteractionScope ii)
putResponse $ Resp_GiveAction ii $ Give_String s
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 R.Function cs
Refinement s -> give_gen WithoutForce ii rng s Refine
maybe (return ()) (display_info . Info_Time) time
interpret (Cmd_context norm ii _ _) =
display_info . Info_Context =<< liftLocalState (prettyContext norm False ii)
interpret (Cmd_helper_function norm ii rng s) =
display_info . Info_HelperFunction =<< liftLocalState (cmd_helper_function norm ii rng s)
interpret (Cmd_infer norm ii rng s) =
display_info . Info_InferredType
=<< liftLocalState (B.withInteractionId ii
(prettyATop =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s))
interpret (Cmd_goal_type norm ii _ _) =
display_info . Info_CurrentGoal
=<< liftLocalState (B.withInteractionId ii $ prettyTypeOfMeta norm ii)
interpret (Cmd_goal_type_context norm ii rng s) =
cmd_goal_type_context_and empty norm ii rng s
interpret (Cmd_goal_type_context_infer norm ii rng s) = do
have <- if all Char.isSpace s then return empty else liftLocalState $ do
typ <- B.withInteractionId ii $
prettyATop =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s
return $ text "Have:" <+> typ
cmd_goal_type_context_and have norm ii rng s
interpret (Cmd_goal_type_context_check 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__
txt <- TCP.prettyTCM =<< normalForm norm term
return $ text "Elaborates to:" <+> txt
cmd_goal_type_context_and have 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 rng 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
hidden <- lift $ showImplicitArguments
tel <- lift $ lookupSection (qnameModule f)
pcs :: [Doc] <- lift $ inTopContext $ addContext tel $ mapM prettyA cs
let pcs' :: [String] = List.map (extlam_dropName casectxt . render) pcs
lift $ reportSDoc "interaction.case" 60 $ TCP.vcat
[ TCP.text "InteractionTop.Cmd_make_case"
, TCP.nest 2 $ TCP.vcat
[ TCP.text "cs = " TCP.<+> TCP.vcat (map prettyA cs)
, TCP.text "pcs = " TCP.<+> TCP.vcat (map return pcs)
, TCP.text "pcs' = " TCP.<+> TCP.vcat (map TCP.text pcs')
]
]
lift $ reportSDoc "interaction.case" 90 $ TCP.vcat
[ TCP.text "InteractionTop.Cmd_make_case"
, TCP.nest 2 $ TCP.vcat
[ TCP.text "cs = " TCP.<+> TCP.text (show cs)
]
]
putResponse $ Resp_MakeCase (makeCaseVariant casectxt) pcs'
where
render = renderStyle (style { mode = OneLineMode })
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant Nothing = R.Function
makeCaseVariant Just{} = R.ExtendedLambda
extlam_dropName :: CaseContext -> String -> String
extlam_dropName Nothing x = x
extlam_dropName Just{} x
= unwords $ reverse $ replEquals $ reverse $ drop 1 $ words x
where
replEquals ("=" : ws) = "→" : ws
replEquals (w : ws) = w : replEquals ws
replEquals [] = []
interpret (Cmd_compute cmode ii rng s) = display_info . Info_NormalForm =<< do
liftLocalState $ do
e <- B.parseExprIn ii rng $ computeWrapInput cmode s
B.withInteractionId ii $ do
showComputed cmode =<< do applyWhen (computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent e
interpret Cmd_show_version = display_info Info_Version
interpret Cmd_abort = return ()
interpretWarnings :: CommandM (String, String)
interpretWarnings = do
mws <- lift $ Imp.getAllWarnings AllWarnings RespectFlags
case filter isNotMeta <$> mws of
Imp.SomeWarnings ws@(_:_) -> do
let (we, wa) = classifyWarnings ws
pwe <- lift $ prettyTCWarnings we
pwa <- lift $ prettyTCWarnings wa
return (pwe, pwa)
_ -> return ("", "")
where isNotMeta w = case tcWarning w of
UnsolvedInteractionMetas{} -> False
UnsolvedMetaVariables{} -> False
_ -> True
solveInstantiatedGoals :: B.Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals norm mii = do
out <- lift $ local (\ e -> e { envPrintMetasBare = True }) $ do
sip <- B.getSolvedInteractionPoints False norm
maybe id (\ ii -> filter ((ii ==) . fst)) mii <$> 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)
showOpenMetas :: TCM [String]
showOpenMetas = do
ims <- B.typesOfVisibleMetas B.AsIs
di <- forM ims $ \ i ->
B.withInteractionId (B.outputFormId $ B.OutputForm noRange [] i) $
showATop i
unsolvedNotOK <- not . optAllowUnsolved <$> pragmaOptions
hms <- (guard unsolvedNotOK >>) <$> B.typesOfHiddenMetas B.Simplified
dh <- mapM showA' hms
return $ di ++ dh
where
metaId (B.OfType i _) = i
metaId (B.JustType i) = i
metaId (B.JustSort i) = i
metaId (B.Assign i e) = i
metaId _ = __IMPOSSIBLE__
showA' :: B.OutputConstraint A.Expr NamedMeta -> TCM String
showA' m = do
let i = nmid $ metaId m
r <- getMetaRange i
d <- B.withMetaId i (showATop m)
return $ d ++ " [ at " ++ show r ++ " ]"
cmd_load' :: FilePath -> [String]
-> Bool
-> Imp.Mode
-> ((Interface, Imp.MaybeWarnings) -> CommandM ())
-> CommandM ()
cmd_load' file argv unsolvedOK mode cmd = do
f <- liftIO $ absolute file
ex <- liftIO $ doesFileExist $ filePath f
let relativeTo | ex = ProjectRoot f
| otherwise = CurrentDir
modify $ \st -> st { theInteractionPoints = []
, theCurrentFile = Nothing
}
t <- liftIO $ getModificationTime file
opts0 <- gets optionsOnReload
z <- liftIO $ runOptM $ parseStandardOptions' argv opts0
case z of
Left err -> lift $ typeError $ GenericError err
Right opts -> do
let update o = o { optAllowUnsolved = unsolvedOK && optAllowUnsolved o}
lift $ TM.setCommandLineOptions' relativeTo $ mapPragmaOptions update opts
displayStatus
lift resetState
putResponse Resp_ClearRunningInfo
putResponse (Resp_ClearHighlighting NotOnlyTokenBased)
ok <- lift $ Imp.typeCheckMain f mode
t' <- liftIO $ getModificationTime file
when (t == t') $ do
is <- lift $ sortInteractionPoints =<< getInteractionPoints
modify $ \st -> st { theInteractionPoints = is
, theCurrentFile = Just (f, t)
}
cmd ok
withCurrentFile :: CommandM a -> CommandM a
withCurrentFile m = do
mfile <- fmap fst <$> gets theCurrentFile
local (\ e -> e { envCurrentPath = mfile }) m
data CompilerBackend = LaTeX | QuickLaTeX | OtherBackend String
deriving (Eq)
instance Show CompilerBackend where
show LaTeX = "LaTeX"
show QuickLaTeX = "QuickLaTeX"
show (OtherBackend s) = s
instance Read CompilerBackend where
readsPrec _ s = do
(t, s) <- lex s
let b = case t of
"LaTeX" -> LaTeX
"QuickLaTeX" -> QuickLaTeX
_ -> OtherBackend t
return (b, s)
data GiveRefine = Give | Refine | Intro
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
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 $ reportSLn "interaction.give" 30 $ unlines
[ "ce = " ++ show ce
, "scopePrecedence = " ++ show (scopePrecedence scope)
]
let literally = giveRefine /= Intro && ae == ae0 && rng /= noRange
when literally $ lift $ do
l <- envHighlightingLevel <$> ask
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 $ show ce
highlightExpr :: A.Expr -> TCM ()
highlightExpr e =
local (\e -> e { envModuleNestingLevel = 0
, envHighlightingLevel = NonInteractive
, envHighlightingMethod = Direct }) $
generateAndPrintSyntaxInfo decl Full True
where
dummy = mkName_ (NameId 0 0) "dummy"
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
prettyTypeOfMeta :: B.Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta norm ii = do
form <- B.typeOfMeta norm ii
case form of
B.OfType _ e -> prettyATop e
_ -> text <$> showATop form
prettyContext
:: B.Rewrite
-> Bool
-> InteractionId
-> TCM Doc
prettyContext norm rev ii = B.withInteractionId ii $ do
ctx <- B.contextOfMeta ii norm
es <- mapM (prettyATop . B.ofExpr) ctx
ns <- mapM (showATop . B.ofName) ctx
return $ align 10 $ applyWhen rev reverse $
filter (not . null . fst) $ zip ns $ map (text ":" <+>) es
cmd_helper_function :: B.Rewrite -> InteractionId -> Range -> String -> TCM Doc
cmd_helper_function norm ii r s = B.withInteractionId ii $ inTopContext $
prettyATop =<< B.metaHelperType norm ii r s
cmd_goal_type_context_and :: Doc -> B.Rewrite -> InteractionId -> Range ->
String -> StateT CommandState (TCMT IO) ()
cmd_goal_type_context_and doc norm ii _ _ = display_info . Info_GoalType =<< do
lift $ do
goal <- B.withInteractionId ii $ prettyTypeOfMeta norm ii
ctx <- prettyContext norm True ii
return $ vcat
[ text "Goal:" <+> goal
, doc
, text (replicate 60 '\x2014')
, ctx
]
showModuleContents :: B.Rewrite -> Range -> String -> CommandM ()
showModuleContents norm rng s = display_info . Info_ModuleContents =<< do
liftLocalState $ do
(modules, types) <- B.moduleContents norm rng s
types' <- forM types $ \ (x, t) -> do
t <- TCP.prettyTCM t
return (prettyShow x, text ":" <+> t)
return $ vcat
[ text "Modules"
, nest 2 $ vcat $ map (text . show) modules
, text "Names"
, nest 2 $ align 10 types'
]
searchAbout :: B.Rewrite -> Range -> String -> CommandM ()
searchAbout norm rg nm = do
let tnm = trim nm
unless (null tnm) $ do
fancy <- lift $ B.atTopLevel $ do
hits <- findMentions norm rg tnm
forM hits $ \ (x, t) -> do
t <- TCP.prettyTCM t
return (prettyShow x, text ":" <+> t)
display_info $ Info_SearchAbout $
text "Definitions about" <+> text (List.intercalate ", " $ words nm) $$
nest 2 (align 10 fancy)
whyInScope :: String -> CommandM ()
whyInScope s = display_info . Info_WhyInScope =<< do
Just (file, _) <- gets theCurrentFile
let cwd = takeDirectory $ filePath file
liftLocalState $ do
(v, xs, ms) <- B.whyInScope s
explanation cwd v xs ms
where
explanation _ Nothing [] [] = TCP.text (s ++ " is not in scope.")
explanation cwd v xs ms = TCP.vcat
[ TCP.text (s ++ " is in scope as")
, TCP.nest 2 $ TCP.vcat [variable v xs, modules ms]
]
where
prettyRange :: Range -> TCM Doc
prettyRange r = text . show . (fmap . fmap) mkRel <$> do
return r
mkRel = Str . makeRelative cwd . filePath
variable Nothing xs = names xs
variable (Just x) xs
| null xs = asVar
| otherwise = TCP.vcat
[ TCP.sep [ asVar, TCP.nest 2 $ shadowing x]
, TCP.nest 2 $ names xs
]
where
asVar :: TCM Doc
asVar = do
TCP.text "* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x)
shadowing :: LocalVar -> TCM Doc
shadowing (LocalVar _ _ []) = TCP.text "shadowing"
shadowing _ = TCP.text "in conflict with"
names xs = TCP.vcat $ map pName xs
modules ms = TCP.vcat $ map pMod ms
pKind DefName = TCP.text "defined name"
pKind ConName = TCP.text "constructor"
pKind FldName = TCP.text "record field"
pKind PatternSynName = TCP.text "pattern synonym"
pKind MacroName = TCP.text "macro name"
pKind QuotableName = TCP.text "quotable name"
pName :: AbstractName -> TCM Doc
pName a = TCP.sep
[ TCP.text "* a"
TCP.<+> pKind (anameKind a)
TCP.<+> TCP.text (prettyShow $ anameName a)
, TCP.nest 2 $ TCP.text "brought into scope by"
] TCP.$$
TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))
pMod :: AbstractModule -> TCM Doc
pMod a = TCP.sep
[ TCP.text "* a module" TCP.<+> TCP.text (prettyShow $ amodName a)
, TCP.nest 2 $ TCP.text "brought into scope by"
] TCP.$$
TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a))
pWhy :: Range -> WhyInScope -> TCM Doc
pWhy r Defined = TCP.text "- its definition at" TCP.<+> TCP.prettyTCM r
pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w
pWhy r (Opened m w) =
TCP.text "- the opening of"
TCP.<+> TCP.text (show m)
TCP.<+> TCP.text "at"
TCP.<+> TCP.prettyTCM (getRange m)
TCP.$$
pWhy r w
pWhy r (Applied m w) =
TCP.text "- the application of"
TCP.<+> TCP.text (show m)
TCP.<+> TCP.text "at"
TCP.<+> TCP.prettyTCM (getRange m)
TCP.$$
pWhy r w
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
refreshStr :: [String] -> String -> ([String], String)
refreshStr taken s = go nameModifiers where
go (m:mods) = let s' = s ++ m in
if s' `elem` taken then go mods else (s':taken, s')
go _ = __IMPOSSIBLE__
nameModifiers :: [String]
nameModifiers = "" : "'" : "''" : [show i | i <-[3..]]
parseAndDoAtToplevel
:: (A.Expr -> TCM Doc)
-> (Doc -> DisplayInfo)
-> String
-> CommandM ()
parseAndDoAtToplevel cmd title s = do
(time, res) <- localStateCommandM $ do
e <- lift $ runPM $ parse exprParser s
maybeTimed $ lift $ B.atTopLevel $ do
cmd =<< concreteToAbstract_ e
display_info $ title $ fromMaybe empty time $$ res
maybeTimed :: CommandM a -> CommandM (Maybe Doc, a)
maybeTimed work = do
doTime <- lift $ hasVerbosity "profile.interactive" 10
if not doTime then (Nothing,) <$> work else do
(r, time) <- measureTime work
return (Just $ text "Time:" <+> pretty 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 ]