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