{-# LANGUAGE NondecreasingIndentation #-}
{-# 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
import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Fail ( MonadFail )
import Control.Monad.State ( MonadState(..), gets, modify, runStateT )
import Control.Monad.STM
import Control.Monad.State ( StateT )
import Control.Monad.Trans ( lift )
import qualified Data.Char as Char
import Data.Function (on)
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe
import System.Directory
import System.FilePath
import Agda.TypeChecking.Monad as TCM
hiding (initState, setCommandLineOptions)
import qualified Agda.TypeChecking.Monad as TCM
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings (runPM, warning)
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.Glyph
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.Syntax.TopLevelModuleName
import Agda.Interaction.Base
import Agda.Interaction.ExitCode
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.Highlighting.Precise hiding (Error, Postulate, singleton)
import Agda.Interaction.Imports ( Mode, pattern ScopeCheck, pattern TypeCheck )
import qualified Agda.Interaction.Imports as Imp
import Agda.Interaction.Highlighting.Generate
import Agda.Compiler.Backend
import Agda.Mimer.Mimer as Mimer
import qualified Control.DeepSeq as DeepSeq
import Agda.Utils.Either
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Hash
import Agda.Utils.IO (showIOException)
import Agda.Utils.Lens
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty hiding (Mode)
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.Singleton
import Agda.Utils.String
import Agda.Utils.Time
import Agda.Utils.Tuple
import Agda.Utils.WithDefault (lensCollapseDefault, lensKeepDefault)
import Agda.Utils.Impossible
import Agda.TypeChecking.Opacity (saturateOpaqueBlocks)
type CommandM = StateT CommandState TCM
localStateCommandM :: CommandM a -> CommandM a
localStateCommandM :: forall a. CommandM a -> CommandM a
localStateCommandM CommandM a
m = do
cSt <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
tcSt <- getTC
x <- m
putTC tcSt
put cSt
return x
liftLocalState :: TCM a -> CommandM a
liftLocalState :: forall a. TCM a -> CommandM a
liftLocalState = TCM a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM a -> StateT CommandState TCM a)
-> (TCM a -> TCM a) -> TCM a -> StateT CommandState TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCM a -> TCM a
forall a. TCM a -> TCM a
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 :: forall st (m :: * -> *) (k :: * -> *) a.
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 forall c. m c -> st -> k (c, st)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
st <- m st
forall s (m :: * -> *). MonadState s m => m s
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 :: forall (m :: * -> *) (k :: * -> *) a.
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 forall c. m c -> TCState -> k (c, TCState)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
st <- m TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
(a, st') <- lift' $ f (`run` st)
putTC st'
return a
commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO :: forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO forall x. (CommandM a -> IO x) -> IO x
ci_i = (forall c.
StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
-> (forall a. TCM a -> CommandM a)
-> (forall x. (CommandM a -> TCM x) -> TCM x)
-> CommandM a
forall st (m :: * -> *) (k :: * -> *) a.
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 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall c.
StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT TCM b -> StateT CommandState TCM b
forall a. TCM a -> CommandM a
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
-> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
forall a b. (a -> b) -> a -> b
$ \CommandM a -> TCM x
ct -> (forall c. TCM c -> TCState -> IO (c, TCState))
-> (forall b. IO b -> TCM b)
-> (forall x. (TCM x -> IO x) -> IO x)
-> TCM x
forall (m :: * -> *) (k :: * -> *) a.
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 TCM c -> TCState -> IO (c, TCState)
forall c. TCM c -> TCState -> IO (c, TCState)
runSafeTCM IO b -> TCM b
forall b. IO b -> TCM b
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((forall x. (TCM x -> IO x) -> IO x) -> TCM x)
-> (forall x. (TCM x -> IO x) -> IO x) -> TCM x
forall a b. (a -> b) -> a -> b
$ (CommandM a -> IO x) -> IO x
forall x. (CommandM a -> IO x) -> IO x
ci_i ((CommandM a -> IO x) -> IO x)
-> ((TCM x -> IO x) -> CommandM a -> IO x)
-> (TCM x -> IO x)
-> IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TCM x -> IO x) -> (CommandM a -> TCM x) -> CommandM a -> IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandM a -> TCM x
ct)
liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT :: forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT forall a. TCM a -> TCM a
f CommandM a
m = (forall c.
StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
-> (forall a. TCM a -> CommandM a)
-> (forall x. (CommandM a -> TCM x) -> TCM x)
-> CommandM a
forall st (m :: * -> *) (k :: * -> *) a.
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 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall c.
StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT TCM b -> StateT CommandState TCM b
forall a. TCM a -> CommandM a
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
-> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
forall a b. (a -> b) -> a -> b
$ TCM x -> TCM x
forall a. TCM a -> TCM a
f (TCM x -> TCM x)
-> ((CommandM a -> TCM x) -> TCM x)
-> (CommandM a -> TCM x)
-> TCM x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CommandM a -> TCM x) -> CommandM a -> TCM x
forall a b. (a -> b) -> a -> b
$ CommandM a
m)
liftCommandMTLocalState :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMTLocalState :: forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMTLocalState forall a. TCM a -> TCM a
f = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT TCM x -> TCM x
forall a. TCM a -> TCM a
f (CommandM a -> CommandM a)
-> (CommandM a -> CommandM a) -> CommandM a -> CommandM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandM a -> CommandM a
forall a. CommandM a -> CommandM a
localStateCommandM
putResponse :: Response -> CommandM ()
putResponse :: Response -> StateT CommandState TCM ()
putResponse = TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> (Response -> TCM ()) -> Response -> StateT CommandState TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Response -> TCM ()
appInteractionOutputCallback
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
modifyTheInteractionPoints [InteractionId] -> [InteractionId]
f = (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s ->
CommandState
s { theInteractionPoints = f (theInteractionPoints s) }
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ()
modifyOldInteractionScopes OldInteractionScopes -> OldInteractionScopes
f = (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s ->
CommandState
s { oldInteractionScopes = f $ oldInteractionScopes s }
insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope :: InteractionId -> ScopeInfo -> StateT CommandState TCM ()
insertOldInteractionScope InteractionId
ii ScopeInfo
scope = do
TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.scope" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"inserting old interaction scope " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
(OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ()
modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ())
-> (OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionId
-> ScopeInfo -> OldInteractionScopes -> OldInteractionScopes
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert InteractionId
ii ScopeInfo
scope
removeOldInteractionScope :: InteractionId -> CommandM ()
removeOldInteractionScope :: InteractionId -> StateT CommandState TCM ()
removeOldInteractionScope InteractionId
ii = do
TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.scope" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"removing old interaction scope " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
(OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ()
modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ())
-> (OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> OldInteractionScopes -> OldInteractionScopes
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete InteractionId
ii
getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope InteractionId
ii = do
ms <- (CommandState -> Maybe ScopeInfo)
-> StateT CommandState TCM (Maybe ScopeInfo)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CommandState -> Maybe ScopeInfo)
-> StateT CommandState TCM (Maybe ScopeInfo))
-> (CommandState -> Maybe ScopeInfo)
-> StateT CommandState TCM (Maybe ScopeInfo)
forall a b. (a -> b) -> a -> b
$ InteractionId -> OldInteractionScopes -> Maybe ScopeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InteractionId
ii (OldInteractionScopes -> Maybe ScopeInfo)
-> (CommandState -> OldInteractionScopes)
-> CommandState
-> Maybe ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandState -> OldInteractionScopes
oldInteractionScopes
case ms of
Maybe ScopeInfo
Nothing -> String -> CommandM ScopeInfo
forall a. String -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> CommandM ScopeInfo) -> String -> CommandM ScopeInfo
forall a b. (a -> b) -> a -> b
$ String
"not an old interaction point: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
Just ScopeInfo
scope -> ScopeInfo -> CommandM ScopeInfo
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ScopeInfo
scope
handleCommand_ :: CommandM () -> CommandM ()
handleCommand_ :: StateT CommandState TCM () -> StateT CommandState TCM ()
handleCommand_ = (forall a. CommandM a -> CommandM a)
-> StateT CommandState TCM ()
-> StateT CommandState TCM ()
-> StateT CommandState TCM ()
handleCommand CommandM a -> CommandM a
forall a. a -> a
forall a. CommandM a -> CommandM a
id (() -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ())
handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
handleCommand :: (forall a. CommandM a -> CommandM a)
-> StateT CommandState TCM ()
-> StateT CommandState TCM ()
-> StateT CommandState TCM ()
handleCommand forall a. CommandM a -> CommandM a
wrap StateT CommandState TCM ()
onFail StateT CommandState TCM ()
cmd = StateT CommandState TCM () -> StateT CommandState TCM ()
handleNastyErrors (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
wrap (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
oldState <- StateT CommandState TCM TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
cmd `catchErr` \ TCErr
e -> do
StateT CommandState TCM ()
onFail
Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
handleErr Maybe HighlightingMethod
forall a. Maybe a
Nothing TCErr
e
TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
newPersistentState <- Lens' TCState PersistentTCState -> TCMT IO PersistentTCState
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState
putTC oldState
lensPersistentState `setTCLens` newPersistentState
where
catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr :: forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr CommandM a
m TCErr -> CommandM a
h = do
s <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
(x, s') <- lift $ do runStateT m s
`catchError_` \ TCErr
e ->
CommandM a -> CommandState -> TCM (a, CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TCErr -> CommandM a
h TCErr
e) CommandState
s
put s'
return x
handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors :: StateT CommandState TCM () -> StateT CommandState TCM ()
handleNastyErrors StateT CommandState TCM ()
m = (forall x. (StateT CommandState TCM () -> IO x) -> IO x)
-> StateT CommandState TCM ()
forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ((forall x. (StateT CommandState TCM () -> IO x) -> IO x)
-> StateT CommandState TCM ())
-> (forall x. (StateT CommandState TCM () -> IO x) -> IO x)
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ StateT CommandState TCM () -> IO x
toIO -> do
let handle :: SomeException -> IO (Either AsyncCancelled x)
handle SomeException
e =
x -> Either AsyncCancelled x
forall a b. b -> Either a b
Right (x -> Either AsyncCancelled x)
-> IO x -> IO (Either AsyncCancelled x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
StateT CommandState TCM () -> IO x
toIO (StateT CommandState TCM () -> IO x)
-> StateT CommandState TCM () -> IO x
forall a b. (a -> b) -> a -> b
$ Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
handleErr (HighlightingMethod -> Maybe HighlightingMethod
forall a. a -> Maybe a
Just HighlightingMethod
Direct) (TCErr -> StateT CommandState TCM ())
-> TCErr -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$
Range -> Doc -> TCErr
Exception Range
forall a. Range' a
noRange (Doc -> TCErr) -> Doc -> TCErr
forall a b. (a -> b) -> a -> b
$ String -> Doc
forall a. String -> Doc a
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ SomeException -> String
forall e. Exception e => e -> String
showIOException SomeException
e
asyncHandler :: AsyncCancelled -> m (Either AsyncCancelled b)
asyncHandler e :: AsyncCancelled
e@AsyncCancelled
AsyncCancelled = Either AsyncCancelled b -> m (Either AsyncCancelled b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AsyncCancelled -> Either AsyncCancelled b
forall a b. a -> Either a b
Left AsyncCancelled
e)
generalHandler :: SomeException -> IO (Either AsyncCancelled x)
generalHandler (SomeException
e :: E.SomeException) = SomeException -> IO (Either AsyncCancelled x)
handle SomeException
e
r <- ((x -> Either AsyncCancelled x
forall a b. b -> Either a b
Right (x -> Either AsyncCancelled x)
-> IO x -> IO (Either AsyncCancelled x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CommandState TCM () -> IO x
toIO StateT CommandState TCM ()
m) IO (Either AsyncCancelled x)
-> (AsyncCancelled -> IO (Either AsyncCancelled x))
-> IO (Either AsyncCancelled x)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` AsyncCancelled -> IO (Either AsyncCancelled x)
forall {m :: * -> *} {b}.
Monad m =>
AsyncCancelled -> m (Either AsyncCancelled b)
asyncHandler)
IO (Either AsyncCancelled x)
-> (SomeException -> IO (Either AsyncCancelled x))
-> IO (Either AsyncCancelled x)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` SomeException -> IO (Either AsyncCancelled x)
generalHandler
case r of
Right x
x -> x -> IO x
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return x
x
Left AsyncCancelled
e -> AsyncCancelled -> IO x
forall e a. (HasCallStack, Exception e) => e -> IO a
E.throwIO AsyncCancelled
e
handleErr :: Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
handleErr Maybe HighlightingMethod
method TCErr
e = do
noError <- TCMT IO Bool -> StateT CommandState TCM Bool
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Bool -> StateT CommandState TCM Bool)
-> TCMT IO Bool -> StateT CommandState TCM Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall a. Null a => a -> Bool
null (String -> Bool) -> TCMT IO String -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCErr -> TCMT IO String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError TCErr
e
unless noError do
unsolved <- lift $ computeUnsolvedInfo
err <- lift $ errorHighlighting e
modFile <- lift $ useTC stModuleToSource
method <- case method of
Maybe HighlightingMethod
Nothing -> TCMT IO HighlightingMethod
-> StateT CommandState TCM HighlightingMethod
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO HighlightingMethod
-> StateT CommandState TCM HighlightingMethod)
-> TCMT IO HighlightingMethod
-> StateT CommandState TCM HighlightingMethod
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv HighlightingMethod -> TCMT IO HighlightingMethod
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (HighlightingMethod -> f HighlightingMethod) -> TCEnv -> f TCEnv
Lens' TCEnv HighlightingMethod
eHighlightingMethod
Just HighlightingMethod
m -> HighlightingMethod -> StateT CommandState TCM HighlightingMethod
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingMethod
m
let info = HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder -> HighlightingInfo)
-> HighlightingInfoBuilder -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ HighlightingInfoBuilder
err HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> HighlightingInfoBuilder
unsolved
showImpl <- lift $ optShowImplicit <$> useTC stPragmaOptions
showIrr <- lift $ optShowIrrelevant <$> useTC stPragmaOptions
do
mapM_ putResponse $
[ Resp_DisplayInfo $ Info_Error $ Info_GenericError e ] ++
tellEmacsToJumpToError (getRange e) ++
[ Resp_HighlightingInfo info KeepHighlighting
method modFile ] ++
[ Resp_Status $ Status { sChecked = False
, sShowImplicitArguments = showImpl
, sShowIrrelevantArguments = showIrr
} ]
whenM (optExitOnError <$> commandLineOptions) $
liftIO $ exitAgdaWith TCMError
runInteraction :: IOTCM -> CommandM ()
runInteraction :: IOTCM -> StateT CommandState TCM ()
runInteraction IOTCM
iotcm =
(forall a. CommandM a -> CommandM a)
-> StateT CommandState TCM ()
-> StateT CommandState TCM ()
-> StateT CommandState TCM ()
handleCommand CommandM a -> CommandM a
forall a. CommandM a -> CommandM a
inEmacs StateT CommandState TCM ()
onFail (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
currentAbs <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
-> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute String
current
cf <- gets theCurrentFile
cmd <- if independent cmd then return cmd else do
when (Just currentAbs /= (currentFilePath <$> cf)) $ do
let mode = Mode
TypeCheck
cmd_load' current [] True mode $ \CheckResult
_ -> () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
cf <- fromMaybe __IMPOSSIBLE__ <$> gets theCurrentFile
return $ case iotcm (Just (currentFileModule cf)) of
IOTCM String
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
cmd -> Interaction' Range
cmd
withCurrentFile $ interpret cmd
cf' <- gets theCurrentFile
when (updateInteractionPointsAfter cmd
&&
Just currentAbs == (currentFilePath <$> cf')) $ do
putResponse . Resp_InteractionPoints =<< gets theInteractionPoints
where
IOTCM String
current HighlightingLevel
highlighting HighlightingMethod
highlightingMethod Interaction' Range
cmd = IOTCM
iotcm Maybe TopLevelModuleName
forall a. Maybe a
Nothing
inEmacs :: forall a. CommandM a -> CommandM a
inEmacs :: forall a. CommandM a -> CommandM a
inEmacs = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT ((forall a. TCM a -> TCM a) -> CommandM a -> CommandM a)
-> (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
forall a b. (a -> b) -> a -> b
$ TCEnv -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a
withEnv (TCEnv -> TCMT IO x -> TCMT IO x)
-> TCEnv -> TCMT IO x -> TCMT IO x
forall a b. (a -> b) -> a -> b
$ TCEnv
initEnv
{ envHighlightingLevel = highlighting
, envHighlightingMethod = highlightingMethod
}
onFail :: StateT CommandState TCM ()
onFail | Interaction' Range -> Bool
independent Interaction' Range
cmd = (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s -> CommandState
s { theCurrentFile = Nothing }
| Bool
otherwise = () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort :: forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort IOTCM -> CommandM a
m = do
commandState <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
let q = CommandState -> CommandQueue
commandQueue CommandState
commandState
(n, cmd) <- liftIO $ atomically $ readTChan (commands q)
case cmd of
Command
Done -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Command' (Maybe a)
forall a. Command' a
Done
Error String
e -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Command' (Maybe a)
forall a. String -> Command' a
Error String
e)
Command IOTCM
c -> do
tcState <- StateT CommandState TCM TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
tcEnv <- askTC
result <- liftIO $ race
(runTCM tcEnv tcState $
runStateT (m c) commandState)
(waitForAbort n q)
case result of
Left ((a
x, CommandState
commandState'), TCState
tcState') -> do
TCState -> StateT CommandState TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcState'
CommandState -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CommandState
commandState'
case IOTCM
c Maybe TopLevelModuleName
forall a. Maybe a
Nothing of
IOTCM String
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
Cmd_exit -> do
Response -> StateT CommandState TCM ()
putResponse Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DoneExiting
Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Command' (Maybe a)
forall a. Command' a
Done
IOTCM' Range
_ -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Command' (Maybe a)
forall a. a -> Command' a
Command (a -> Maybe a
forall a. a -> Maybe a
Just a
x))
Right Integer
a -> do
IO () -> StateT CommandState TCM ()
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT CommandState TCM ())
-> IO () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ CommandQueue -> Integer -> IO ()
popAbortedCommands CommandQueue
q Integer
a
TCState -> StateT CommandState TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC (TCState -> StateT CommandState TCM ())
-> TCState -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ TCState
initState
{ stPersistentState = stPersistentState tcState
, stPreScopeState =
(stPreScopeState initState)
{ stPrePragmaOptions =
stPrePragmaOptions
(stPreScopeState tcState)
}
}
CommandState -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (CommandState -> StateT CommandState TCM ())
-> CommandState -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ (CommandQueue -> CommandState
initCommandState (CommandState -> CommandQueue
commandQueue CommandState
commandState))
{ optionsOnReload = optionsOnReload commandState
}
Response -> StateT CommandState TCM ()
putResponse Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DoneAborting
StateT CommandState TCM ()
displayStatus
Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Command' (Maybe a)
forall a. a -> Command' a
Command Maybe a
forall a. Maybe a
Nothing)
where
waitForAbort
:: Integer
-> CommandQueue
-> IO Integer
waitForAbort :: Integer -> CommandQueue -> IO Integer
waitForAbort Integer
n CommandQueue
q = do
STM Integer -> IO Integer
forall a. STM a -> IO a
atomically (STM Integer -> IO Integer) -> STM Integer -> IO Integer
forall a b. (a -> b) -> a -> b
$ do
a <- TVar (Maybe Integer) -> STM (Maybe Integer)
forall a. TVar a -> STM a
readTVar (CommandQueue -> TVar (Maybe Integer)
abort CommandQueue
q)
case a of
Just Integer
a' | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
a' -> Integer -> STM Integer
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
a'
Maybe Integer
_ -> STM Integer
forall a. STM a
retry
popAbortedCommands :: CommandQueue -> Integer -> IO ()
popAbortedCommands :: CommandQueue -> Integer -> IO ()
popAbortedCommands CommandQueue
q Integer
n = do
done <- STM Bool -> IO Bool
forall a. STM a -> IO a
atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
cmd <- TChan (Integer, Command) -> STM (Maybe (Integer, Command))
forall a. TChan a -> STM (Maybe a)
tryReadTChan (CommandQueue -> TChan (Integer, Command)
commands CommandQueue
q)
case cmd of
Maybe (Integer, Command)
Nothing -> Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Just (Integer, Command)
c ->
if (Integer, Command) -> Integer
forall a b. (a, b) -> a
fst (Integer, Command)
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n then
Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
else do
TChan (Integer, Command) -> (Integer, Command) -> STM ()
forall a. TChan a -> a -> STM ()
unGetTChan (CommandQueue -> TChan (Integer, Command)
commands CommandQueue
q) (Integer, Command)
c
Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
unless done $
popAbortedCommands q n
initialiseCommandQueue
:: IO Command
-> IO CommandQueue
initialiseCommandQueue :: IO Command -> IO CommandQueue
initialiseCommandQueue IO Command
next = do
commands <- IO (TChan (Integer, Command))
forall a. IO (TChan a)
newTChanIO
abort <- newTVarIO Nothing
let
readCommands Integer
n = do
c <- IO Command
next
case c of
Command IOTCM
c | IOTCM String
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
Cmd_abort <- IOTCM
c Maybe TopLevelModuleName
forall a. Maybe a
Nothing -> do
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Integer) -> Maybe Integer -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar (Maybe Integer)
abort (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n)
Integer -> IO ()
readCommands Integer
n
Command
_ -> do
let n' :: Integer
n' = (Integer -> Integer
forall a. Enum a => a -> a
succ Integer
n)
STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan (Integer, Command) -> (Integer, Command) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Integer, Command)
commands (Integer
n', Command
c)
case Command
c of
Command
Done -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Command
_ -> Integer -> IO ()
readCommands Integer
n'
_ <- forkIO (readCommands 0)
return (CommandQueue { .. })
independent :: Interaction -> Bool
independent :: Interaction' Range -> Bool
independent (Cmd_load {}) = Bool
True
independent (Cmd_compile {}) = Bool
True
independent (Cmd_load_highlighting_info {}) = Bool
True
independent Cmd_tokenHighlighting {} = Bool
True
independent Interaction' Range
Cmd_show_version = Bool
True
independent Interaction' Range
_ = Bool
False
updateInteractionPointsAfter :: Interaction -> Bool
updateInteractionPointsAfter :: Interaction' Range -> Bool
updateInteractionPointsAfter Cmd_load{} = Bool
True
updateInteractionPointsAfter Cmd_compile{} = Bool
True
updateInteractionPointsAfter Cmd_constraints{} = Bool
False
updateInteractionPointsAfter Cmd_metas{} = Bool
False
updateInteractionPointsAfter Cmd_no_metas{} = Bool
False
updateInteractionPointsAfter Cmd_show_module_contents_toplevel{} = Bool
False
updateInteractionPointsAfter Cmd_search_about_toplevel{} = Bool
False
updateInteractionPointsAfter Cmd_solveAll{} = Bool
True
updateInteractionPointsAfter Cmd_solveOne{} = Bool
True
updateInteractionPointsAfter Cmd_infer_toplevel{} = Bool
False
updateInteractionPointsAfter Cmd_compute_toplevel{} = Bool
False
updateInteractionPointsAfter Cmd_load_highlighting_info{} = Bool
False
updateInteractionPointsAfter Cmd_tokenHighlighting{} = Bool
False
updateInteractionPointsAfter Cmd_highlight{} = Bool
True
updateInteractionPointsAfter ShowImplicitArgs{} = Bool
False
updateInteractionPointsAfter ToggleImplicitArgs{} = Bool
False
updateInteractionPointsAfter ShowIrrelevantArgs{} = Bool
False
updateInteractionPointsAfter ToggleIrrelevantArgs{} = Bool
False
updateInteractionPointsAfter Cmd_give{} = Bool
True
updateInteractionPointsAfter Cmd_refine{} = Bool
True
updateInteractionPointsAfter Cmd_intro{} = Bool
True
updateInteractionPointsAfter Cmd_refine_or_intro{} = Bool
True
updateInteractionPointsAfter Cmd_autoOne{} = Bool
True
updateInteractionPointsAfter Cmd_autoAll{} = Bool
True
updateInteractionPointsAfter Cmd_context{} = Bool
False
updateInteractionPointsAfter Cmd_helper_function{} = Bool
False
updateInteractionPointsAfter Cmd_infer{} = Bool
False
updateInteractionPointsAfter Cmd_goal_type{} = Bool
False
updateInteractionPointsAfter Cmd_elaborate_give{} = Bool
True
updateInteractionPointsAfter Cmd_goal_type_context{} = Bool
False
updateInteractionPointsAfter Cmd_goal_type_context_infer{} = Bool
False
updateInteractionPointsAfter Cmd_goal_type_context_check{} = Bool
False
updateInteractionPointsAfter Cmd_show_module_contents{} = Bool
False
updateInteractionPointsAfter Cmd_make_case{} = Bool
True
updateInteractionPointsAfter Cmd_compute{} = Bool
False
updateInteractionPointsAfter Cmd_why_in_scope{} = Bool
False
updateInteractionPointsAfter Cmd_why_in_scope_toplevel{} = Bool
False
updateInteractionPointsAfter Cmd_show_version{} = Bool
False
updateInteractionPointsAfter Cmd_abort{} = Bool
False
updateInteractionPointsAfter Cmd_exit{} = Bool
False
interpret :: Interaction -> CommandM ()
interpret :: Interaction' Range -> StateT CommandState TCM ()
interpret (Cmd_load String
m [String]
argv) =
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
m [String]
argv Bool
True Mode
mode ((CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ())
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \CheckResult
_ -> Interaction' Range -> StateT CommandState TCM ()
interpret (Interaction' Range -> StateT CommandState TCM ())
-> Interaction' Range -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Interaction' Range
forall range. Rewrite -> Interaction' range
Cmd_metas Rewrite
AsIs
where
mode :: Mode
mode = Mode
TypeCheck
interpret (Cmd_compile CompilerBackend
backend String
file [String]
argv) =
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
file [String]
argv Bool
allowUnsolved Mode
mode ((CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ())
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CheckResult
checkResult -> do
mw <- TCM [TCWarning] -> StateT CommandState TCM [TCWarning]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [TCWarning] -> StateT CommandState TCM [TCWarning])
-> TCM [TCWarning] -> StateT CommandState TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TCM [TCWarning]
forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings ([TCWarning] -> TCM [TCWarning]) -> [TCWarning] -> TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ CheckResult -> [TCWarning]
crWarnings CheckResult
checkResult
case mw of
[] -> do
TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ case CompilerBackend
backend of
CompilerBackend
LaTeX -> String -> IsMain -> CheckResult -> TCM ()
callBackend String
"LaTeX" IsMain
IsMain CheckResult
checkResult
CompilerBackend
QuickLaTeX -> String -> IsMain -> CheckResult -> TCM ()
callBackend String
"LaTeX" IsMain
IsMain CheckResult
checkResult
OtherBackend String
"GHCNoMain" -> String -> IsMain -> CheckResult -> TCM ()
callBackend String
"GHC" IsMain
NotMain CheckResult
checkResult
OtherBackend String
b -> String -> IsMain -> CheckResult -> TCM ()
callBackend String
b IsMain
IsMain CheckResult
checkResult
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> (WarningsAndNonFatalErrors
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompilerBackend
-> WarningsAndNonFatalErrors
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
CompilerBackend
-> warningsAndNonFatalErrors
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_CompilationOk CompilerBackend
backend (WarningsAndNonFatalErrors -> StateT CommandState TCM ())
-> StateT CommandState TCM WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM WarningsAndNonFatalErrors
-> StateT CommandState TCM WarningsAndNonFatalErrors
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM WarningsAndNonFatalErrors
B.getWarningsAndNonFatalErrors
w :: [TCWarning]
w@(TCWarning
_:[TCWarning]
_) -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
Info_Error_boot tcErr tcWarning
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Error (Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> Info_Error
forall tcErr tcWarning.
[tcWarning] -> Info_Error_boot tcErr tcWarning
Info_CompilationError [TCWarning]
w
where
allowUnsolved :: Bool
allowUnsolved = CompilerBackend
backend CompilerBackend -> [CompilerBackend] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CompilerBackend
LaTeX, CompilerBackend
QuickLaTeX]
mode :: Mode
mode | CompilerBackend
QuickLaTeX <- CompilerBackend
backend = Mode
ScopeCheck
| Bool
otherwise = Mode
TypeCheck
interpret Interaction' Range
Cmd_constraints =
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> ([OutputForm_boot TCErr Expr Expr]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> [OutputForm_boot TCErr Expr Expr]
-> StateT CommandState TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OutputForm_boot TCErr Expr Expr]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
[OutputForm_boot tcErr Expr Expr]
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Constraints ([OutputForm_boot TCErr Expr Expr] -> StateT CommandState TCM ())
-> StateT CommandState TCM [OutputForm_boot TCErr Expr Expr]
-> StateT CommandState TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM [OutputForm_boot TCErr Expr Expr]
-> StateT CommandState TCM [OutputForm_boot TCErr Expr Expr]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM [OutputForm_boot TCErr Expr Expr]
B.getConstraints
interpret (Cmd_metas Rewrite
norm) = do
ms <- TCMT IO Goals -> StateT CommandState TCM Goals
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Goals -> StateT CommandState TCM Goals)
-> TCMT IO Goals -> StateT CommandState TCM Goals
forall a b. (a -> b) -> a -> b
$ Rewrite -> Rewrite -> TCMT IO Goals
B.getGoals' Rewrite
norm (Rewrite -> Rewrite -> Rewrite
forall a. Ord a => a -> a -> a
max Rewrite
Simplified Rewrite
norm)
display_info . Info_AllGoalsWarnings ms =<< lift B.getWarningsAndNonFatalErrors
interpret Interaction' Range
Cmd_no_metas = do
metas <- StateT CommandState TCM [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
unless (null metas) $
typeError $ GenericError "Unsolved meta-variables"
interpret (Cmd_show_module_contents_toplevel Rewrite
norm String
s) =
StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> String -> StateT CommandState TCM ()
showModuleContents Rewrite
norm Range
forall a. Range' a
noRange String
s
interpret (Cmd_search_about_toplevel Rewrite
norm String
s) =
StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> String -> StateT CommandState TCM ()
searchAbout Rewrite
norm Range
forall a. Range' a
noRange String
s
interpret (Cmd_solveAll Rewrite
norm) = Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
solveInstantiatedGoals Rewrite
norm Maybe InteractionId
forall a. Maybe a
Nothing
interpret (Cmd_solveOne Rewrite
norm InteractionId
ii Range
_ String
_) = Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
solveInstantiatedGoals Rewrite
norm' (InteractionId -> Maybe InteractionId
forall a. a -> Maybe a
Just InteractionId
ii)
where norm' :: Rewrite
norm' = case Rewrite
norm of
Rewrite
Simplified -> Rewrite
AsIs
Rewrite
Instantiated -> Rewrite
Simplified
Rewrite
_ -> Rewrite
norm
interpret (Cmd_infer_toplevel Rewrite
norm String
s) = do
(time, expr) <- (Expr -> TCM Expr) -> String -> CommandM (Maybe CPUTime, Expr)
forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel (Rewrite -> Expr -> TCM Expr
B.typeInCurrent Rewrite
norm) String
s
state <- get
display_info $ Info_InferredType state time expr
interpret (Cmd_compute_toplevel ComputeMode
cmode String
s) = do
(time, expr) <- (Expr -> TCM Expr) -> String -> CommandM (Maybe CPUTime, Expr)
forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM Expr
action (ComputeMode -> String -> String
B.computeWrapInput ComputeMode
cmode String
s)
state <- get
display_info $ Info_NormalForm state cmode time expr
where
action :: Expr -> TCM Expr
action = TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
(TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if ComputeMode -> Bool
B.computeIgnoreAbstract ComputeMode
cmode then TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
(TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputeMode -> Expr -> TCM Expr
B.evalInCurrent ComputeMode
cmode
interpret (ShowImplicitArgs Bool
showImpl) = do
opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
setCommandLineOpts $
set (lensPragmaOptions . lensOptShowImplicit . lensKeepDefault) showImpl opts
interpret Interaction' Range
ToggleImplicitArgs = do
opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
setCommandLineOpts $
over (lensPragmaOptions . lensOptShowImplicit . lensCollapseDefault) not opts
interpret (ShowIrrelevantArgs Bool
showIrr) = do
opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
setCommandLineOpts $
set (lensPragmaOptions . lensOptShowIrrelevant . lensKeepDefault) showIrr opts
interpret Interaction' Range
ToggleIrrelevantArgs = do
opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
setCommandLineOpts $
over (lensPragmaOptions . lensOptShowIrrelevant . lensCollapseDefault) not opts
interpret (Cmd_load_highlighting_info String
source) = do
l <- (TCEnv -> HighlightingLevel)
-> StateT CommandState TCM HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
when (l /= None) $ do
setCommandLineOpts =<< lift commandLineOptions
resp <- lift $ liftIO . tellToUpdateHighlighting =<< do
ex <- liftIO $ doesFileExist source
absSource <- liftIO $ SourceFile <$> absolute source
if ex
then
do
src <- Imp.parseSource absSource
let m = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
checkModuleName m absSource Nothing
mmi <- getVisitedModule m
case mmi of
Maybe ModuleInfo
Nothing -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
Just ModuleInfo
mi ->
if Text -> Hash
hashText (Source -> Text
Imp.srcText Source
src) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Interface -> Hash
iSourceHash (ModuleInfo -> Interface
miInterface ModuleInfo
mi)
then do
modFile <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource
method <- viewTC eHighlightingMethod
return $ Just (iHighlighting $ miInterface mi, method, modFile)
else
Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
`catchError` \TCErr
_ -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
else
return Nothing
mapM_ putResponse resp
interpret (Cmd_tokenHighlighting String
source Remove
remove) = do
info <- do l <- (TCEnv -> HighlightingLevel)
-> StateT CommandState TCM HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
if l == None
then return Nothing
else do
source' <- liftIO (absolute source)
lift $ (Just <$> generateTokenInfo source')
`catchError` \TCErr
_ ->
Maybe HighlightingInfo -> TCM (Maybe HighlightingInfo)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe HighlightingInfo
forall a. Maybe a
Nothing
StateT CommandState TCM (Maybe HighlightingInfo)
-> StateT CommandState TCM ()
-> StateT CommandState TCM (Maybe HighlightingInfo)
forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally`
case Remove
remove of
Remove
Remove -> IO () -> StateT CommandState TCM ()
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT CommandState TCM ())
-> IO () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
source
Remove
Keep -> () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
case info of
Just HighlightingInfo
info' -> TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
RemoveHighlighting HighlightingInfo
info'
Maybe HighlightingInfo
Nothing -> () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
interpret (Cmd_highlight InteractionId
ii Range
rng String
s) = do
l <- (TCEnv -> HighlightingLevel)
-> StateT CommandState TCM HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
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 :: ExceptT Info_Error TCM () -> StateT CommandState TCM ()
handle ExceptT Info_Error TCM ()
m = do
res <- TCM (Either Info_Error ())
-> StateT CommandState TCM (Either Info_Error ())
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Either Info_Error ())
-> StateT CommandState TCM (Either Info_Error ()))
-> TCM (Either Info_Error ())
-> StateT CommandState TCM (Either Info_Error ())
forall a b. (a -> b) -> a -> b
$ ExceptT Info_Error TCM () -> TCM (Either Info_Error ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT Info_Error TCM ()
m
case res of
Left Info_Error
err -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
Info_Error_boot tcErr tcWarning
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Error Info_Error
err
Right ()
_ -> () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
try :: Info_Error -> TCM a -> ExceptT Info_Error TCM a
try :: forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
try Info_Error
err TCM a
m = TCM (Either Info_Error a) -> ExceptT Info_Error TCM a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (TCM (Either Info_Error a) -> ExceptT Info_Error TCM a)
-> TCM (Either Info_Error a) -> ExceptT Info_Error TCM a
forall a b. (a -> b) -> a -> b
$ do
((TCErr -> Info_Error) -> Either TCErr a -> Either Info_Error a
forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft (Info_Error -> TCErr -> Info_Error
forall a b. a -> b -> a
const Info_Error
err) (Either TCErr a -> Either Info_Error a)
-> TCMT IO (Either TCErr a) -> TCM (Either Info_Error a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a -> TCMT IO (Either TCErr a)
forall a. TCM a -> TCM (Either TCErr a)
freshTCM TCM a
m) TCM (Either Info_Error a)
-> (TCErr -> TCM (Either Info_Error a))
-> TCM (Either Info_Error a)
forall a. TCM a -> (TCErr -> TCM a) -> TCM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> Either Info_Error a -> TCM (Either Info_Error a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Info_Error -> Either Info_Error a
forall a b. a -> Either a b
Left Info_Error
err)
interpret (Cmd_give UseForce
force InteractionId
ii Range
rng String
s) = UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
force InteractionId
ii Range
rng String
s GiveRefine
Give
interpret (Cmd_refine InteractionId
ii Range
rng String
s) = UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng String
s GiveRefine
Refine
interpret (Cmd_intro Bool
pmLambda InteractionId
ii Range
rng String
_) = do
ss <- TCMT IO [String] -> StateT CommandState TCM [String]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [String] -> StateT CommandState TCM [String])
-> TCMT IO [String] -> StateT CommandState TCM [String]
forall a b. (a -> b) -> a -> b
$ Bool -> InteractionId -> TCMT IO [String]
B.introTactic Bool
pmLambda InteractionId
ii
liftCommandMT (withInteractionId ii) $ case ss of
[] -> do
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Intro_NotFound
[String
s] -> UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng String
s GiveRefine
Intro
String
_:String
_:[String]
_ -> do
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ [String]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
[String]
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Intro_ConstructorUnknown [String]
ss
interpret (Cmd_refine_or_intro Bool
pmLambda InteractionId
ii Range
r String
s) = Interaction' Range -> StateT CommandState TCM ()
interpret (Interaction' Range -> StateT CommandState TCM ())
-> Interaction' Range -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$
let s' :: String
s' = String -> String
trim String
s
in (if String -> Bool
forall a. Null a => a -> Bool
null String
s' then Bool -> InteractionId -> Range -> String -> Interaction' Range
forall range.
Bool -> InteractionId -> range -> String -> Interaction' range
Cmd_intro Bool
pmLambda else InteractionId -> Range -> String -> Interaction' Range
forall range.
InteractionId -> range -> String -> Interaction' range
Cmd_refine) InteractionId
ii Range
r String
s'
interpret (Cmd_autoOne Rewrite
norm InteractionId
ii Range
rng String
str) = do
iscope <- InteractionId -> CommandM ScopeInfo
forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
(time, result) <- maybeTimed $ Mimer.mimer norm ii rng str
case result of
MimerResult
MimerNoResult -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
String
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Auto String
"No solution found"
MimerExpr String
str -> do
InteractionId -> ScopeInfo -> StateT CommandState TCM ()
insertOldInteractionScope InteractionId
ii ScopeInfo
iscope
Response -> StateT CommandState TCM ()
putResponse (Response -> StateT CommandState TCM ())
-> Response -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> GiveResult
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_GiveAction InteractionId
ii (GiveResult -> Response) -> GiveResult -> Response
forall a b. (a -> b) -> a -> b
$ String -> GiveResult
Give_String String
str
([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
modifyTheInteractionPoints (InteractionId -> [InteractionId] -> [InteractionId]
forall a. Eq a => a -> [a] -> [a]
List.delete InteractionId
ii)
StateT CommandState TCM ()
-> (CPUTime -> StateT CommandState TCM ())
-> Maybe CPUTime
-> StateT CommandState TCM ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> (CPUTime
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> CPUTime
-> StateT CommandState TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CPUTime
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
CPUTime
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Time) Maybe CPUTime
time
MimerList [(Int, String)]
sols -> do
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
String
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Auto (String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ String
"Solutions:" ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s | (Int
i, String
s) <- [(Int, String)]
sols ]
MimerClauses{} -> StateT CommandState TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
interpret (Cmd_autoAll Rewrite
norm) = do
iis <- StateT CommandState TCM [InteractionId]
forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
getOldScope <- do
st <- getTC
pure $ \ InteractionId
ii -> TCM ScopeInfo -> CommandM ScopeInfo
forall a. TCM a -> CommandM a
liftLocalState (TCM ScopeInfo -> CommandM ScopeInfo)
-> TCM ScopeInfo -> CommandM ScopeInfo
forall a b. (a -> b) -> a -> b
$ TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st TCM () -> TCM ScopeInfo -> TCM ScopeInfo
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> InteractionId -> TCM ScopeInfo
forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
unless (null iis) $ do
let time = Int
1000 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` [InteractionId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [InteractionId]
iis
st <- getTC
solved <- fmap concat $ forM iis $ \ InteractionId
ii -> do
rng <- InteractionId -> StateT CommandState TCM Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
ii
res <- Mimer.mimer norm ii rng ("-t " ++ show time ++ "ms")
case res of
MimerResult
MimerNoResult -> [InteractionId] -> StateT CommandState TCM [InteractionId]
forall a. a -> StateT CommandState TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
MimerExpr String
str -> do
InteractionId -> ScopeInfo -> StateT CommandState TCM ()
insertOldInteractionScope InteractionId
ii (ScopeInfo -> StateT CommandState TCM ())
-> CommandM ScopeInfo -> StateT CommandState TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> CommandM ScopeInfo
getOldScope InteractionId
ii
Response -> StateT CommandState TCM ()
putResponse (Response -> StateT CommandState TCM ())
-> Response -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> GiveResult
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_GiveAction InteractionId
ii (GiveResult -> Response) -> GiveResult -> Response
forall a b. (a -> b) -> a -> b
$ String -> GiveResult
Give_String String
str
[InteractionId] -> StateT CommandState TCM [InteractionId]
forall a. a -> StateT CommandState TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [InteractionId
ii]
MimerList{} -> [InteractionId] -> StateT CommandState TCM [InteractionId]
forall a. a -> StateT CommandState TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
MimerClauses{} -> StateT CommandState TCM [InteractionId]
forall a. HasCallStack => a
__IMPOSSIBLE__
modifyTheInteractionPoints (List.\\ solved)
interpret (Cmd_context Rewrite
norm InteractionId
ii Range
_ String
_) =
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> ([ResponseContextEntry]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> [ResponseContextEntry]
-> StateT CommandState TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId
-> [ResponseContextEntry]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> [ResponseContextEntry]
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Context InteractionId
ii ([ResponseContextEntry] -> StateT CommandState TCM ())
-> StateT CommandState TCM [ResponseContextEntry]
-> StateT CommandState TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM [ResponseContextEntry]
-> StateT CommandState TCM [ResponseContextEntry]
forall a. TCM a -> CommandM a
liftLocalState (Rewrite -> InteractionId -> TCM [ResponseContextEntry]
B.getResponseContext Rewrite
norm InteractionId
ii)
interpret (Cmd_helper_function Rewrite
norm InteractionId
ii Range
rng String
s) = do
helperType <- TCM (OutputConstraint' Expr Expr)
-> CommandM (OutputConstraint' Expr Expr)
forall a. TCM a -> CommandM a
liftLocalState (TCM (OutputConstraint' Expr Expr)
-> CommandM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> CommandM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ InteractionId
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ Rewrite
-> InteractionId
-> Range
-> String
-> TCM (OutputConstraint' Expr Expr)
B.metaHelperType Rewrite
norm InteractionId
ii Range
rng String
s
display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType)
interpret (Cmd_infer Rewrite
norm InteractionId
ii Range
rng String
s) = do
expr <- TCM Expr -> CommandM Expr
forall a. TCM a -> CommandM a
liftLocalState (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ InteractionId -> Rewrite -> Expr -> TCM Expr
B.typeInMeta InteractionId
ii Rewrite
norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng String
s
display_info $ Info_GoalSpecific ii (Goal_InferredType expr)
interpret (Cmd_goal_type Rewrite
norm InteractionId
ii Range
_ String
_) =
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ InteractionId
-> GoalDisplayInfo_boot TCErr
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> GoalDisplayInfo_boot tcErr
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_GoalSpecific InteractionId
ii (Rewrite -> GoalDisplayInfo_boot TCErr
forall tcErr. Rewrite -> GoalDisplayInfo_boot tcErr
Goal_CurrentGoal Rewrite
norm)
interpret (Cmd_elaborate_give Rewrite
norm InteractionId
ii Range
rng String
s) =
UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng String
s (GiveRefine -> StateT CommandState TCM ())
-> GiveRefine -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> GiveRefine
ElaborateGive Rewrite
norm
interpret (Cmd_goal_type_context Rewrite
norm InteractionId
ii Range
rng String
s) =
GoalTypeAux
-> Rewrite
-> InteractionId
-> Range
-> String
-> StateT CommandState TCM ()
cmd_goal_type_context_and GoalTypeAux
GoalOnly Rewrite
norm InteractionId
ii Range
rng String
s
interpret (Cmd_goal_type_context_infer Rewrite
norm InteractionId
ii Range
rng String
s) = do
aux <- if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
Char.isSpace String
s
then GoalTypeAux -> StateT CommandState TCM GoalTypeAux
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return GoalTypeAux
GoalOnly
else do
TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux
forall a. TCM a -> CommandM a
liftLocalState (TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux)
-> TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCM GoalTypeAux -> TCM GoalTypeAux
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM GoalTypeAux -> TCM GoalTypeAux)
-> TCM GoalTypeAux -> TCM GoalTypeAux
forall a b. (a -> b) -> a -> b
$ do
parsed <- InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng String
s
(typ, faces) <- B.typeAndFacesInMeta ii norm parsed
return (GoalAndHave typ faces)
cmd_goal_type_context_and aux norm ii rng s
interpret (Cmd_goal_type_context_check Rewrite
norm InteractionId
ii Range
rng String
s) = do
term <- TCM Term -> CommandM Term
forall a. TCM a -> CommandM a
liftLocalState (TCM Term -> CommandM Term) -> TCM Term -> CommandM Term
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCM Term -> TCM Term
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
expr <- InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng String
s
goal <- B.typeOfMeta AsIs ii
term <- case goal of
OfType InteractionId
_ Expr
ty -> Expr -> Type -> TCM Term
checkExpr Expr
expr (Type -> TCM Term) -> TCMT IO Type -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO Type
isType_ Expr
ty
OutputConstraint Expr InteractionId
_ -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
B.normalForm norm term
cmd_goal_type_context_and (GoalAndElaboration term) norm ii rng s
interpret (Cmd_show_module_contents Rewrite
norm InteractionId
ii Range
rng String
s) =
(forall a. TCM a -> TCM a)
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> String -> StateT CommandState TCM ()
showModuleContents Rewrite
norm Range
rng String
s
interpret (Cmd_why_in_scope_toplevel String
s) =
StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String -> StateT CommandState TCM ()
whyInScope String
s
interpret (Cmd_why_in_scope InteractionId
ii Range
_range String
s) =
(forall a. TCM a -> TCM a)
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String -> StateT CommandState TCM ()
whyInScope String
s
interpret (Cmd_make_case InteractionId
ii Range
rng String
s) = do
(f, casectxt, cs) <- TCMT IO (QName, CaseContext, [Clause])
-> StateT CommandState TCM (QName, CaseContext, [Clause])
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (QName, CaseContext, [Clause])
-> StateT CommandState TCM (QName, CaseContext, [Clause]))
-> TCMT IO (QName, CaseContext, [Clause])
-> StateT CommandState TCM (QName, CaseContext, [Clause])
forall a b. (a -> b) -> a -> b
$ InteractionId
-> Range -> String -> TCMT IO (QName, CaseContext, [Clause])
makeCase InteractionId
ii Range
rng String
s
liftCommandMT (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'
interpret (Cmd_compute ComputeMode
cmode InteractionId
ii Range
rng String
s) = do
expr <- TCM Expr -> CommandM Expr
forall a. TCM a -> CommandM a
liftLocalState (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ do
e <- InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng (String -> TCM Expr) -> String -> TCM Expr
forall a b. (a -> b) -> a -> b
$ ComputeMode -> String -> String
B.computeWrapInput ComputeMode
cmode String
s
withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e
display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr)
interpret Interaction' Range
Cmd_show_version = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Version
interpret Interaction' Range
Cmd_abort = () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
interpret Interaction' Range
Cmd_exit = () -> StateT CommandState TCM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
decorate :: Doc -> String
decorate :: Doc -> String
decorate = Style -> Doc -> String
forall a. Style -> Doc a -> String
renderStyle (Style
style { mode = OneLineMode })
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant CaseContext
Nothing = MakeCaseVariant
R.Function
makeCaseVariant Just{} = MakeCaseVariant
R.ExtendedLambda
extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
extlam_dropName UnicodeOrAscii
_ CaseContext
Nothing String
x = String
x
extlam_dropName UnicodeOrAscii
glyphMode Just{} String
x
= [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
replEquals ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop Int
1 ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
x
where
arrow :: String
arrow = Doc -> String
forall a. Doc a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SpecialCharacters -> Doc
_arrow (SpecialCharacters -> Doc) -> SpecialCharacters -> Doc
forall a b. (a -> b) -> a -> b
$ UnicodeOrAscii -> SpecialCharacters
specialCharactersForGlyphs UnicodeOrAscii
glyphMode
replEquals :: [String] -> [String]
replEquals (String
"=" : [String]
ws) = String
arrow String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ws
replEquals (String
w : [String]
ws) = String
w String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
replEquals [String]
ws
replEquals [] = []
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
solveInstantiatedGoals Rewrite
norm Maybe InteractionId
mii = do
out <- TCM [(InteractionId, Expr)]
-> StateT CommandState TCM [(InteractionId, Expr)]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [(InteractionId, Expr)]
-> StateT CommandState TCM [(InteractionId, Expr)])
-> TCM [(InteractionId, Expr)]
-> StateT CommandState TCM [(InteractionId, Expr)]
forall a b. (a -> b) -> a -> b
$ (TCEnv -> TCEnv)
-> TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)]
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envPrintMetasBare = True }) (TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)])
-> TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)]
forall a b. (a -> b) -> a -> b
$ do
sip <- Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
B.getSolvedInteractionPoints Bool
False Rewrite
norm
let sip' = ([(InteractionId, MetaId, Expr)]
-> [(InteractionId, MetaId, Expr)])
-> (InteractionId
-> [(InteractionId, MetaId, Expr)]
-> [(InteractionId, MetaId, Expr)])
-> Maybe InteractionId
-> [(InteractionId, MetaId, Expr)]
-> [(InteractionId, MetaId, Expr)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(InteractionId, MetaId, Expr)] -> [(InteractionId, MetaId, Expr)]
forall a. a -> a
id (\ InteractionId
ii -> ((InteractionId, MetaId, Expr) -> Bool)
-> [(InteractionId, MetaId, Expr)]
-> [(InteractionId, MetaId, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((InteractionId
ii InteractionId -> InteractionId -> Bool
forall a. Eq a => a -> a -> Bool
==) (InteractionId -> Bool)
-> ((InteractionId, MetaId, Expr) -> InteractionId)
-> (InteractionId, MetaId, Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId, MetaId, Expr) -> InteractionId
forall a b c. (a, b, c) -> a
fst3)) Maybe InteractionId
mii [(InteractionId, MetaId, Expr)]
sip
mapM prt sip'
putResponse $ Resp_SolveAll out
where
prt :: (a, MetaId, a) -> m (a, ConOfAbs a)
prt (a
i, MetaId
m, a
e) = do
mi <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> m MetaVariable -> m (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
e' <- withMetaInfo mi $ abstractToConcreteCtx TopCtx e
return (i, e')
cmd_load'
:: FilePath
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' :: forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
file [String]
argv Bool
unsolvedOK Mode
mode CheckResult -> CommandM a
cmd = do
fp <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
-> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute String
file
ex <- liftIO $ doesFileExist $ filePath fp
unless ex $ typeError $ GenericError $
"The file " ++ file ++ " was not found."
modify $ \ CommandState
st -> CommandState
st { theInteractionPoints = []
, theCurrentFile = Nothing
}
t <- liftIO $ getModificationTime file
displayStatus
lift resetState
putResponse Resp_ClearRunningInfo
putResponse (Resp_ClearHighlighting NotOnlyTokenBased)
src <- lift $ Imp.parseSource (SourceFile fp)
warnings <- useTC stTCWarnings
opts0 <- gets optionsOnReload
backends <- useTC stBackends
let (z, warns) = runOptM $ parseBackendOptions backends argv opts0
mapM_ (lift . warning . OptionWarning) warns
case z of
Left String
err -> TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
err
Right ([Backend]
_, CommandLineOptions
opts) -> do
opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions)
-> TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM CommandLineOptions
addTrustedExecutables CommandLineOptions
opts
let update = Lens' PragmaOptions Bool -> LensMap PragmaOptions Bool
forall o i. Lens' o i -> LensMap o i
over ((WithDefault 'False -> f (WithDefault 'False))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(WithDefault 'False -> f (WithDefault 'False))
-> PragmaOptions -> f PragmaOptions
lensOptAllowUnsolved ((WithDefault 'False -> f (WithDefault 'False))
-> PragmaOptions -> f PragmaOptions)
-> ((Bool -> f Bool)
-> WithDefault 'False -> f (WithDefault 'False))
-> (Bool -> f Bool)
-> PragmaOptions
-> f PragmaOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> f Bool) -> WithDefault 'False -> f (WithDefault 'False)
forall a (b :: Bool).
(Boolean a, Eq a, KnownBool b) =>
Lens' (WithDefault' a b) a
Lens' (WithDefault 'False) Bool
lensKeepDefault) (Bool
unsolvedOK Bool -> Bool -> Bool
&&)
root = AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
fp (TopLevelModuleName -> AbsolutePath)
-> TopLevelModuleName -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ Source -> TopLevelModuleName
Imp.srcModuleName Source
src
lift $ TCM.setCommandLineOptions' root $ mapPragmaOptions update opts
modifyTCLens stTCWarnings (++ warnings)
ok <- lift $ Imp.typeCheckMain mode src
t' <- liftIO $ getModificationTime file
when (t == t') $ do
is <- lift $ sortInteractionPoints =<< getInteractionPoints
modify $ \CommandState
st -> CommandState
st { theInteractionPoints = is
, theCurrentFile = Just $ CurrentFile
{ currentFilePath = fp
, currentFileModule = Imp.srcModuleName src
, currentFileArgs = argv
, currentFileStamp = t
}
}
cmd ok
withCurrentFile :: CommandM a -> CommandM a
withCurrentFile :: forall a. CommandM a -> CommandM a
withCurrentFile CommandM a
m = do
mfile <- (CommandState -> Maybe AbsolutePath)
-> StateT CommandState TCM (Maybe AbsolutePath)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CommandState -> Maybe AbsolutePath)
-> StateT CommandState TCM (Maybe AbsolutePath))
-> (CommandState -> Maybe AbsolutePath)
-> StateT CommandState TCM (Maybe AbsolutePath)
forall a b. (a -> b) -> a -> b
$ (CurrentFile -> AbsolutePath)
-> Maybe CurrentFile -> Maybe AbsolutePath
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CurrentFile -> AbsolutePath
currentFilePath (Maybe CurrentFile -> Maybe AbsolutePath)
-> (CommandState -> Maybe CurrentFile)
-> CommandState
-> Maybe AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandState -> Maybe CurrentFile
theCurrentFile
localTC (\ TCEnv
e -> TCEnv
e { envCurrentPath = mfile }) m
atTopLevel :: CommandM a -> CommandM a
atTopLevel :: forall a. CommandM a -> CommandM a
atTopLevel CommandM a
cmd = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT TCM x -> TCM x
forall a. TCM a -> TCM a
B.atTopLevel CommandM a
cmd
data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite
deriving (GiveRefine -> GiveRefine -> Bool
(GiveRefine -> GiveRefine -> Bool)
-> (GiveRefine -> GiveRefine -> Bool) -> Eq GiveRefine
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GiveRefine -> GiveRefine -> Bool
== :: GiveRefine -> GiveRefine -> Bool
$c/= :: GiveRefine -> GiveRefine -> Bool
/= :: GiveRefine -> GiveRefine -> Bool
Eq, Int -> GiveRefine -> String -> String
[GiveRefine] -> String -> String
GiveRefine -> String
(Int -> GiveRefine -> String -> String)
-> (GiveRefine -> String)
-> ([GiveRefine] -> String -> String)
-> Show GiveRefine
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> GiveRefine -> String -> String
showsPrec :: Int -> GiveRefine -> String -> String
$cshow :: GiveRefine -> String
show :: GiveRefine -> String
$cshowList :: [GiveRefine] -> String -> String
showList :: [GiveRefine] -> String -> String
Show)
give_gen
:: UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> CommandM ()
give_gen :: UseForce
-> InteractionId
-> Range
-> String
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
force InteractionId
ii Range
rng String
s0 GiveRefine
giveRefine = do
let s :: String
s = String -> String
trim String
s0
String -> Int -> String -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.give" Int
20 (String -> StateT CommandState TCM ())
-> String -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ String
"give_gen " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String -> Bool
forall a. Null a => a -> Bool
null String
s) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
let give_ref :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give_ref =
case GiveRefine
giveRefine of
GiveRefine
Give -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.give
GiveRefine
Refine -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.refine
GiveRefine
Intro -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.refine
ElaborateGive Rewrite
norm -> Rewrite
-> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.elaborate_give Rewrite
norm
scope <- InteractionId -> CommandM ScopeInfo
forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
(time, (ae, ae0, iis)) <- maybeTimed $ do
removeInteractionPoint ii
mis <- getInteractionPoints
reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis
given <- lift $ B.parseExprIn ii rng s
ae <- lift $ 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' <- sortInteractionPoints iis
modifyTheInteractionPoints $ replace ii iis'
ce <- abstractToConcreteScope scope ae
reportS "interaction.give" 30
[ "ce = " ++ show ce
, "scopePrecedence = " ++ show (scope ^. scopePrecedence)
]
saturateOpaqueBlocks
let literally = (GiveRefine
giveRefine GiveRefine -> GiveRefine -> Bool
forall a. Eq a => a -> a -> Bool
== GiveRefine
Give Bool -> Bool -> Bool
|| GiveRefine
giveRefine GiveRefine -> GiveRefine -> Bool
forall a. Eq a => a -> a -> Bool
== GiveRefine
Refine) Bool -> Bool -> Bool
&& Expr
ae Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ae0 Bool -> Bool -> Bool
&& Range
rng Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= Range
forall a. Range' a
noRange
when literally $ do
l <- asksTC envHighlightingLevel
when (l /= None) $ lift $ do
printHighlightingInfo KeepHighlighting =<<
generateTokenInfoFromString rng s
highlightExpr ae
putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce
reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"
maybe (interpret $ Cmd_metas AsIs) (display_info . Info_Time) time
reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed"
where
replace :: b -> [b] -> t b -> [b]
replace b
x [b]
xs t b
ys = (b -> [b]) -> t b -> [b]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ b
y -> if b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
x then [b]
xs else [b
y]) t b
ys
mkNewTxt :: Bool -> Expr -> GiveResult
mkNewTxt Bool
True C.Paren{} = GiveResult
Give_Paren
mkNewTxt Bool
True Expr
_ = GiveResult
Give_NoParen
mkNewTxt Bool
False Expr
ce = String -> GiveResult
Give_String (String -> GiveResult) -> String -> GiveResult
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. Pretty a => a -> String
prettyShow Expr
ce
highlightExpr :: A.Expr -> TCM ()
highlightExpr :: Expr -> TCM ()
highlightExpr Expr
e =
(TCEnv -> TCEnv) -> TCM () -> TCM ()
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
st -> TCEnv
st { envImportPath = []
, envHighlightingLevel = NonInteractive
, envHighlightingMethod = Direct }) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
decl Level
Full Bool
True
where
dummy :: Name
dummy = NameId -> String -> Name
forall a. MkName a => NameId -> a -> Name
mkName_ (Hash -> ModuleNameHash -> NameId
NameId Hash
0 ModuleNameHash
noModuleNameHash) (String
"dummy" :: String)
info :: DefInfo' Expr
info = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete Name
dummy) Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef (Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e)
decl :: Declaration
decl = KindOfName
-> DefInfo' Expr
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
OtherDefName DefInfo' Expr
info ArgInfo
defaultArgInfo Maybe [Occurrence]
forall a. Maybe a
Nothing (List1 Name -> QName
qnameFromList (List1 Name -> QName) -> List1 Name -> QName
forall a b. (a -> b) -> a -> b
$ Name -> List1 Name
forall el coll. Singleton el coll => el -> coll
singleton Name
dummy) Expr
e
sortInteractionPoints
:: (MonadInteractionPoints m, MonadError TCErr m, MonadFail m)
=> [InteractionId] -> m [InteractionId]
sortInteractionPoints :: forall (m :: * -> *).
(MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
[InteractionId] -> m [InteractionId]
sortInteractionPoints [InteractionId]
is =
((InteractionId, Range) -> InteractionId)
-> [(InteractionId, Range)] -> [InteractionId]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, Range) -> InteractionId
forall a b. (a, b) -> a
fst ([(InteractionId, Range)] -> [InteractionId])
-> ([(InteractionId, Range)] -> [(InteractionId, Range)])
-> [(InteractionId, Range)]
-> [InteractionId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, Range) -> (InteractionId, Range) -> Ordering)
-> [(InteractionId, Range)] -> [(InteractionId, Range)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Range -> Range -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Range -> Ordering)
-> ((InteractionId, Range) -> Range)
-> (InteractionId, Range)
-> (InteractionId, Range)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (InteractionId, Range) -> Range
forall a b. (a, b) -> b
snd) ([(InteractionId, Range)] -> [InteractionId])
-> m [(InteractionId, Range)] -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[InteractionId]
-> (InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [InteractionId]
is ((InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)])
-> (InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)]
forall a b. (a -> b) -> a -> b
$ \ InteractionId
i -> do
(InteractionId
i,) (Range -> (InteractionId, Range))
-> m Range -> m (InteractionId, Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range ->
String -> CommandM ()
cmd_goal_type_context_and :: GoalTypeAux
-> Rewrite
-> InteractionId
-> Range
-> String
-> StateT CommandState TCM ()
cmd_goal_type_context_and GoalTypeAux
aux Rewrite
norm InteractionId
ii Range
_ String
_ = do
ctx <- TCM [ResponseContextEntry]
-> StateT CommandState TCM [ResponseContextEntry]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [ResponseContextEntry]
-> StateT CommandState TCM [ResponseContextEntry])
-> TCM [ResponseContextEntry]
-> StateT CommandState TCM [ResponseContextEntry]
forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> TCM [ResponseContextEntry]
B.getResponseContext Rewrite
norm InteractionId
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 :: Rewrite -> Range -> String -> StateT CommandState TCM ()
showModuleContents Rewrite
norm Range
rng String
s = do
(modules, tel, types) <- TCMT IO ([Name], Telescope, [(Name, Type)])
-> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO ([Name], Telescope, [(Name, Type)])
-> StateT CommandState TCM ([Name], Telescope, [(Name, Type)]))
-> TCMT IO ([Name], Telescope, [(Name, Type)])
-> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ Rewrite
-> Range -> String -> TCMT IO ([Name], Telescope, [(Name, Type)])
B.moduleContents Rewrite
norm Range
rng String
s
display_info $ Info_ModuleContents modules tel types
searchAbout :: Rewrite -> Range -> String -> CommandM ()
searchAbout :: Rewrite -> Range -> String -> StateT CommandState TCM ()
searchAbout Rewrite
norm Range
rg String
names = do
String
-> (String -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (String -> String
trim String
names) ((String -> StateT CommandState TCM ())
-> StateT CommandState TCM ())
-> (String -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ String
trimmedNames -> do
hits <- TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)])
-> TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> String -> TCMT IO [(Name, Type)]
findMentions Rewrite
norm Range
rg String
trimmedNames
display_info $ Info_SearchAbout hits trimmedNames
whyInScope :: String -> CommandM ()
whyInScope :: String -> StateT CommandState TCM ()
whyInScope String
s = do
Just file <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
let cwd = String -> String
takeDirectory (AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ CurrentFile -> AbsolutePath
currentFilePath CurrentFile
file)
why <- liftLocalState $ B.whyInScope cwd s
display_info $ Info_WhyInScope why
setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts :: CommandLineOptions -> StateT CommandState TCM ()
setCommandLineOpts CommandLineOptions
opts = do
TCM () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT CommandState TCM ())
-> TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM ()
TCM.setCommandLineOptions CommandLineOptions
opts
StateT CommandState TCM ()
displayStatus
status :: CommandM Status
status :: CommandM Status
status = do
cf <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
showImpl <- lift showImplicitArguments
showIrr <- lift showIrrelevantArguments
checked <- lift $ case cf of
Maybe CurrentFile
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just CurrentFile
f -> do
t <- IO ClockTime -> TCMT IO ClockTime
forall b. IO b -> TCM b
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ClockTime -> TCMT IO ClockTime)
-> IO ClockTime -> TCMT IO ClockTime
forall a b. (a -> b) -> a -> b
$ String -> IO ClockTime
getModificationTime (String -> IO ClockTime) -> String -> IO ClockTime
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath (CurrentFile -> AbsolutePath
currentFilePath CurrentFile
f)
if currentFileStamp f == t
then
maybe False (null . miWarnings) <$>
getVisitedModule (currentFileModule f)
else
return False
return $ Status { sShowImplicitArguments = showImpl,
sShowIrrelevantArguments = showIrr,
sChecked = checked }
displayStatus :: CommandM ()
displayStatus :: StateT CommandState TCM ()
displayStatus =
Response -> StateT CommandState TCM ()
putResponse (Response -> StateT CommandState TCM ())
-> (Status -> Response) -> Status -> StateT CommandState TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Status -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Status -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_Status (Status -> StateT CommandState TCM ())
-> CommandM Status -> StateT CommandState TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CommandM Status
status
display_info :: DisplayInfo -> CommandM ()
display_info :: DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
display_info DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info = do
StateT CommandState TCM ()
displayStatus
Response -> StateT CommandState TCM ()
putResponse (Response -> StateT CommandState TCM ())
-> Response -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info
parseAndDoAtToplevel
:: (A.Expr -> TCM a)
-> String
-> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel :: forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM a
cmd String
s = do
CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
forall a. CommandM a -> CommandM a
localStateCommandM (CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a))
-> CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
forall a b. (a -> b) -> a -> b
$ do
(e, attrs) <- TCM (Expr, Attributes)
-> StateT CommandState TCM (Expr, Attributes)
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Expr, Attributes)
-> StateT CommandState TCM (Expr, Attributes))
-> TCM (Expr, Attributes)
-> StateT CommandState TCM (Expr, Attributes)
forall a b. (a -> b) -> a -> b
$ PM (Expr, Attributes) -> TCM (Expr, Attributes)
forall a. PM a -> TCM a
runPM (PM (Expr, Attributes) -> TCM (Expr, Attributes))
-> PM (Expr, Attributes) -> TCM (Expr, Attributes)
forall a b. (a -> b) -> a -> b
$ Parser Expr -> String -> PM (Expr, Attributes)
forall a. Parser a -> String -> PM (a, Attributes)
parse Parser Expr
exprParser String
s
lift $ checkAttributes attrs
maybeTimed $ atTopLevel $ lift $
cmd =<< concreteToAbstract_ e
maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed :: forall a. CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed CommandM a
work = do
doTime <- TCMT IO Bool -> StateT CommandState TCM Bool
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Bool -> StateT CommandState TCM Bool)
-> TCMT IO Bool -> StateT CommandState TCM Bool
forall a b. (a -> b) -> a -> b
$ ProfileOption -> TCMT IO Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
Profile.Interactive
if not doTime
then (Nothing,) <$> work
else do
(r, time) <- measureTime work
return (Just time, r)
tellToUpdateHighlighting
:: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> IO [Response]
tellToUpdateHighlighting Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
Nothing = [Response] -> IO [Response]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
tellToUpdateHighlighting (Just (HighlightingInfo
info, HighlightingMethod
method, ModuleToSource
modFile)) =
[Response] -> IO [Response]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
KeepHighlighting HighlightingMethod
method ModuleToSource
modFile]
tellEmacsToJumpToError :: Range -> [Response]
tellEmacsToJumpToError :: Range -> [Response]
tellEmacsToJumpToError Range
r =
case Range -> Maybe (Position' (Maybe RangeFile))
forall a. Range' a -> Maybe (Position' a)
rStart Range
r of
Maybe (Position' (Maybe RangeFile))
Nothing -> []
Just (Pn { srcFile :: forall a. Position' a -> a
srcFile = Maybe RangeFile
Strict.Nothing }) -> []
Just (Pn { srcFile :: forall a. Position' a -> a
srcFile = Strict.Just RangeFile
f, posPos :: forall a. Position' a -> Int32
posPos = Int32
p }) ->
[ String -> Int32 -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
String
-> Int32 -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_JumpToError (AbsolutePath -> String
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
f)) Int32
p ]