module Agda.Interaction.InteractionTop
( module Agda.Interaction.InteractionTop
)
where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import qualified Control.Exception as E
import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State
import qualified Data.Char as Char
import Data.Foldable (Foldable)
import Data.Function
import Data.List as List hiding (null)
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.Errors
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.Concrete.Generic as C
import Agda.Syntax.Concrete.Pretty ()
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.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses as Lenses
import Agda.Interaction.MakeCase
import Agda.Interaction.Response hiding (Function, ExtendedLambda)
import qualified Agda.Interaction.Response as R
import qualified Agda.Interaction.BasicOps as B
import Agda.Interaction.Highlighting.Precise hiding (Postulate)
import qualified Agda.Interaction.Imports as Imp
import Agda.Interaction.Highlighting.Generate
import qualified Agda.Interaction.Highlighting.Range as H
import qualified Agda.Compiler.Epic.Compiler as Epic
import qualified Agda.Compiler.MAlonzo.Compiler as MAlonzo
import qualified Agda.Compiler.JS.Compiler as JS
import qualified Agda.Auto.Auto as Auto
import Agda.Utils.Except
( ExceptT
, mkExceptT
, MonadError(catchError, throwError)
, runExceptT
)
import Agda.Utils.FileName
import Agda.Utils.Hash
import qualified Agda.Utils.HashMap as HMap
import Agda.Utils.Lens
import Agda.Utils.Maybe
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
}
type OldInteractionScopes = Map InteractionId ScopeInfo
initCommandState :: CommandState
initCommandState = CommandState
{ theInteractionPoints = []
, theCurrentFile = Nothing
, optionsOnReload = defaultOptions
, oldInteractionScopes = Map.empty
}
type CommandM = StateT CommandState TCM
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)
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
runInteraction :: IOTCM -> CommandM ()
runInteraction (IOTCM current highlighting highlightingMethod cmd)
= handleNastyErrors
$ inEmacs
$ do
current <- liftIO $ absolute current
res <- (`catchErr` (return . Just)) $ do
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 (Just current == (fst <$> cf)) $
putResponse . Resp_InteractionPoints =<< gets theInteractionPoints
return Nothing
maybe (return ()) handleErr res
where
catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr m h = do
s <- get
let sErr | independent cmd = s { theCurrentFile = Nothing }
| otherwise = s
(x, s') <- lift $ do
disableDestructiveUpdate (runStateT m s)
`catchError_` \ e ->
runStateT (h e) sErr
put s'
return x
inEmacs = liftCommandMT $ withEnv $ initEnv
{ envHighlightingLevel = highlighting
, envHighlightingMethod = highlightingMethod
}
handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors m = commandMToIO $ \ toIO ->
toIO m `E.catch` \ (e :: E.SomeException) ->
toIO $ handleErr $ Exception noRange $ text $ show e
handleErr e = do
meta <- lift $ computeUnsolvedMetaWarnings
constr <- lift $ computeUnsolvedConstraints
err <- lift $ errorHighlighting e
modFile <- lift $ use stModuleToSource
let info = compress $ mconcat
[err, meta, constr]
s <- lift $ prettyError e
x <- lift $ optShowImplicit <$> use stPragmaOptions
mapM_ putResponse $
[ Resp_DisplayInfo $ Info_Error s ] ++
tellEmacsToJumpToError (getRange e) ++
[ Resp_HighlightingInfo info modFile ] ++
[ Resp_Status $ Status { sChecked = False
, sShowImplicitArguments = x
} ]
type Interaction = Interaction' Range
data Interaction' range
= Cmd_load FilePath [FilePath]
| Cmd_compile Backend FilePath [FilePath]
| Cmd_constraints
| Cmd_metas
| Cmd_show_module_contents_toplevel
B.Rewrite
String
| Cmd_solveAll
| Cmd_infer_toplevel B.Rewrite
String
| Cmd_compute_toplevel Bool
String
| Cmd_load_highlighting_info
FilePath
| Cmd_highlight InteractionId range String
| ShowImplicitArgs Bool
| ToggleImplicitArgs
| Cmd_give 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_show_module_contents
B.Rewrite InteractionId range String
| Cmd_make_case InteractionId range String
| Cmd_compute Bool
InteractionId range String
| Cmd_why_in_scope InteractionId range String
| Cmd_why_in_scope_toplevel String
| Cmd_show_version
deriving (Read, Functor, Foldable, Traversable)
type IOTCM = IOTCM' Range
data IOTCM' range
= IOTCM
FilePath
HighlightingLevel
HighlightingMethod
(Interaction' range)
deriving (Read, Functor, Foldable, Traversable)
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)) . 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 $ do
exact "Range"
fmap Range readParse
`mplus` do
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_show_version = True
independent _ = False
interpret :: Interaction -> CommandM ()
interpret (Cmd_load m includes) =
cmd_load' m includes True $ \_ -> interpret Cmd_metas
interpret (Cmd_compile b file includes) =
cmd_load' file includes False $ \(i, mw) -> do
case mw of
Imp.NoWarnings -> do
lift $ case b of
MAlonzo -> MAlonzo.compilerMain True i
MAlonzoNoMain -> MAlonzo.compilerMain False i
Epic -> Epic.compilerMain i
JS -> JS.compilerMain i
display_info $ Info_CompilationOk
Imp.SomeWarnings w ->
display_info $ Info_Error $ unlines
[ "You can only compile modules without unsolved metavariables"
, "or termination checking problems."
]
interpret Cmd_constraints =
display_info . Info_Constraints . unlines . map show =<< lift B.getConstraints
interpret Cmd_metas = do
ms <- lift $ showOpenMetas
ifM (return (null ms) `and2M` do not . null <$> lift B.getConstraints)
(interpret Cmd_constraints)
(display_info $ Info_AllGoals $ unlines ms)
interpret (Cmd_show_module_contents_toplevel norm s) =
liftCommandMT B.atTopLevel $ showModuleContents norm noRange s
interpret Cmd_solveAll = do
out <- lift $ mapM lowr =<< B.getSolvedInteractionPoints False
putResponse $ Resp_SolveAll out
where
lowr (i, m, e) = do
mi <- getMetaInfo <$> lookupMeta m
e <- withMetaInfo mi $ lowerMeta <$> abstractToConcreteCtx TopCtx e
return (i, e)
interpret (Cmd_infer_toplevel norm s) =
parseAndDoAtToplevel (B.typeInCurrent norm) Info_InferredType s
interpret (Cmd_compute_toplevel ignore s) =
parseAndDoAtToplevel (allowNonTerminatingReductions .
if ignore then ignoreAbstractMode . c
else inConcreteMode . c)
Info_NormalForm
s
where c = B.evalInCurrent
interpret (ShowImplicitArgs showImpl) = do
opts <- lift commandLineOptions
setCommandLineOptions' $
opts { optPragmaOptions =
(optPragmaOptions opts) { optShowImplicit = showImpl } }
interpret ToggleImplicitArgs = do
opts <- lift commandLineOptions
let ps = optPragmaOptions opts
setCommandLineOptions' $
opts { optPragmaOptions =
ps { optShowImplicit = not $ optShowImplicit ps } }
interpret (Cmd_load_highlighting_info source) = do
setCommandLineOptions' =<< 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
return $ Just (iHighlighting $ miInterface mi, modFile)
else
return Nothing
mapM_ putResponse resp
interpret (Cmd_highlight ii rng s) = 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 =<< 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
(Right <$> m) `catchError` \ _ -> return (Left err)
interpret (Cmd_give ii rng s) = give_gen ii rng s Give
interpret (Cmd_refine ii rng s) = give_gen 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] -> do
interpret $ Cmd_refine ii rng s
_:_:_ -> 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
(res, msg) <- lift $ Auto.auto ii rng s
case res of
Left xs -> do
lift $ reportSLn "auto" 10 $ "Auto produced the following solutions " ++ show xs
forM_ xs $ \(ii, s) -> do
insertOldInteractionScope ii =<< lift (localState (put st >> getInteractionScope ii))
putResponse $ Resp_GiveAction ii $ Give_String s
modifyTheInteractionPoints (\\ (map fst xs))
case msg of
Nothing -> interpret Cmd_metas
Just msg -> display_info $ Info_Auto msg
Right (Left cs) -> do
case msg of
Nothing -> return ()
Just msg -> display_info $ Info_Auto msg
putResponse $ Resp_MakeCase R.Function cs
Right (Right s) -> give_gen ii rng s Refine
interpret (Cmd_context norm ii _ _) =
display_info . Info_Context =<< lift (prettyContext norm False ii)
interpret (Cmd_helper_function norm ii rng s) =
display_info . Info_HelperFunction =<< lift (cmd_helper_function norm ii rng s)
interpret (Cmd_infer norm ii rng s) =
display_info . Info_InferredType
=<< lift (B.withInteractionId ii
(prettyATop =<< B.typeInMeta ii norm =<< B.parseExprIn ii rng s))
interpret (Cmd_goal_type norm ii _ _) =
display_info . Info_CurrentGoal
=<< lift (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 do
typ <- lift $ 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_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
(casectxt , cs) <- lift $ makeCase ii rng s
liftCommandMT (B.withInteractionId ii) $ do
hidden <- lift $ showImplicitArguments
pcs <- lift $ mapM prettyA $ List.map (extlam_dropLLifted casectxt hidden) cs
putResponse $ Resp_MakeCase (makeCaseVariant casectxt) (List.map (extlam_dropName casectxt . render) pcs)
where
render = renderStyle (style { mode = OneLineMode })
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant FunctionDef = R.Function
makeCaseVariant (ExtendedLambda _ _) = R.ExtendedLambda
extlam_dropName :: CaseContext -> String -> String
extlam_dropName FunctionDef x = x
extlam_dropName (ExtendedLambda _ _) x
= unwords $ reverse $ replEquals $ reverse $ drop 1 $ words x
where
replEquals ("=" : ws) = "→" : ws
replEquals (w : ws) = w : replEquals ws
replEquals [] = []
extlam_dropLLifted :: CaseContext -> Bool -> A.Clause -> A.Clause
extlam_dropLLifted FunctionDef _ x = x
extlam_dropLLifted (ExtendedLambda h nh) hidden (A.Clause (A.LHS info (A.LHSProj{}) ps) rhs decl) = __IMPOSSIBLE__
extlam_dropLLifted (ExtendedLambda h nh) hidden (A.Clause (A.LHS info (A.LHSHead name nps) ps) rhs decl)
= let n = if hidden then h + nh else nh
in
(A.Clause (A.LHS info (A.LHSHead name (drop n nps)) ps) rhs decl)
interpret (Cmd_compute ignore ii rng s) = do
e <- lift $ B.parseExprIn ii rng s
d <- lift $ B.withInteractionId ii $ do
let c = B.evalInCurrent e
v <- if ignore then ignoreAbstractMode c else c
prettyATop v
display_info $ Info_NormalForm d
interpret Cmd_show_version = display_info Info_Version
showOpenMetas :: TCM [String]
showOpenMetas = do
ims <- B.typesOfVisibleMetas B.AsIs
di <- forM ims $ \ i ->
B.withInteractionId (B.outputFormId $ B.OutputForm noRange 0 i) $
showATop i
dh <- mapM showA' =<< B.typesOfHiddenMetas B.Simplified
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 -> [FilePath]
-> Bool
-> ((Interface, Imp.MaybeWarnings) -> CommandM ())
-> CommandM ()
cmd_load' file includes unsolvedOK cmd = do
f <- liftIO $ absolute file
ex <- liftIO $ doesFileExist $ filePath f
lift $ TM.setIncludeDirs includes $
if ex then ProjectRoot f else CurrentDir
modify $ \st -> st { theInteractionPoints = []
, theCurrentFile = Nothing
}
t <- liftIO $ getModificationTime file
opts <- lift $ commandLineOptions
defaultOptions <- gets optionsOnReload
setCommandLineOptions' $
Lenses.setIncludeDirs (optIncludeDirs opts) $
mapPragmaOptions (\ o -> o { optAllowUnsolved = unsolvedOK }) $
defaultOptions
lift resetState
putResponse Resp_ClearRunningInfo
putResponse Resp_ClearHighlighting
ok <- lift $ Imp.typeCheckMain f
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 Backend = MAlonzo
| MAlonzoNoMain
| Epic | JS
deriving (Show, Read)
data GiveRefine = Give | Refine
deriving (Eq, Show)
give_gen
:: InteractionId
-> Range
-> String
-> GiveRefine
-> CommandM ()
give_gen 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
scope <- lift $ getInteractionScope ii
(ae, iis) <- lift $ do
mis <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis
ae <- give_ref ii Nothing =<< B.parseExprIn ii rng s
mis' <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'
return (ae, mis' \\ mis)
insertOldInteractionScope ii scope
iis <- lift $ sortInteractionPoints iis
modifyTheInteractionPoints $ replace ii iis
ce <- lift $ abstractToConcreteEnv (makeEnv scope) ae
lift $ reportSLn "interaction.give" 30 $ "ce = " ++ show ce
let literally = giveRefine == Give && rng /= noRange
when literally $ lift $ do
printHighlightingInfo =<< generateTokenInfoFromString rng s
highlightExpr ae
putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce
lift $ reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"
interpret Cmd_metas
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
where
dummy = mkName_ (NameId 0 0) "dummy"
info = mkDefInfo (nameConcrete dummy) defaultFixity' PublicAccess ConcreteDef (getRange e)
decl = A.Axiom NoFunSig info defaultArgInfo (qnameFromList [dummy]) e
sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
sortInteractionPoints is =
map fst . 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
let shuffle = if rev then reverse else id
return $ align 10 $ filter (not . null. fst) $ shuffle $ 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 _ _ = do
goal <- lift $ B.withInteractionId ii $ prettyTypeOfMeta norm ii
ctx <- lift $ prettyContext norm True ii
display_info $ Info_GoalType
(text "Goal:" <+> goal $+$
doc $+$
text (replicate 60 '\x2014') $+$
ctx)
showModuleContents :: B.Rewrite -> Range -> String -> CommandM ()
showModuleContents norm rng s = do
(modules, types) <- lift $ B.moduleContents norm rng s
types' <- lift $ forM types $ \ (x, t) -> do
t <- TCP.prettyTCM t
return (show x, text ":" <+> t)
display_info $ Info_ModuleContents $
text "Modules" $$
nest 2 (vcat $ map (text . show) modules) $$
text "Names" $$
nest 2 (align 10 types')
whyInScope :: String -> CommandM ()
whyInScope s = do
(v, xs, ms) <- lift $ B.whyInScope s
cwd <- do
Just (file, _) <- gets $ theCurrentFile
return $ takeDirectory $ filePath file
display_info . Info_WhyInScope =<< do lift $ 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 ShadowedVar{} = 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 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
setCommandLineOptions' :: CommandLineOptions -> CommandM ()
setCommandLineOptions' 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 <- Map.lookup f <$> sourceToModule
case mm of
Nothing -> return False
Just m -> not . miWarnings . fromMaybe __IMPOSSIBLE__ <$> 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..]]
lowerMeta :: (C.ExprLike a) => a -> a
lowerMeta = C.mapExpr kill where
kill e =
case e of
C.QuestionMark{} -> preMeta
C.Underscore{} -> preUscore
C.App{} -> case appView e of
C.AppView (C.QuestionMark _ _) _ -> preMeta
C.AppView (C.Underscore _ _) _ -> preUscore
_ -> e
C.Paren r q@(C.QuestionMark _ Nothing) -> q
_ -> e
preMeta = C.QuestionMark noRange Nothing
preUscore = C.Underscore noRange Nothing
parseAndDoAtToplevel
:: (A.Expr -> TCM A.Expr)
-> (Doc -> DisplayInfo)
-> String
-> CommandM ()
parseAndDoAtToplevel cmd title s = do
e <- liftIO $ parse exprParser s
doTime <- lift $ hasVerbosity "profile.interactive" 10
let work = lift (B.atTopLevel $ prettyA =<< cmd =<< concreteToAbstract_ e)
res <- if not doTime then work else do
(r, time) <- measureTime work
return $ text "Time:" <+> pretty time $$ r
display_info (title res)
tellToUpdateHighlighting
:: Maybe (HighlightingInfo, ModuleToSource) -> IO [Response]
tellToUpdateHighlighting Nothing = return []
tellToUpdateHighlighting (Just (info, modFile)) =
return [Resp_HighlightingInfo info modFile]
tellEmacsToJumpToError :: Range -> [Response]
tellEmacsToJumpToError r =
case rStart r of
Nothing -> []
Just (Pn { srcFile = Nothing }) -> []
Just (Pn { srcFile = Just f, posPos = p }) ->
[ Resp_JumpToError (filePath f) p ]