{-# LANGUAGE NondecreasingIndentation #-}
{-# OPTIONS_GHC -fno-cse #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Agda.Interaction.InteractionTop
  ( module Agda.Interaction.InteractionTop
  )
  where

import Prelude hiding (null)

import Control.Concurrent
import Control.Concurrent.Async
import Control.Concurrent.STM.TChan
import Control.Concurrent.STM.TVar

import qualified Control.Exception  as E

import Control.Monad
import Control.Monad.Except         ( MonadError(..), ExceptT(..), runExceptT )
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.Fail           ( MonadFail )
import Control.Monad.State          ( MonadState(..), gets, modify, runStateT )
import Control.Monad.STM
import Control.Monad.Trans          ( lift )

import qualified Data.Char as Char
import Data.Function
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe

import System.Directory
import System.FilePath

import Agda.TypeChecking.Monad as TCM
  hiding (initState, setCommandLineOptions)
import qualified Agda.TypeChecking.Monad as TCM
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Warnings (runPM)

import Agda.Syntax.Fixity
import Agda.Syntax.Position
import Agda.Syntax.Parser
import Agda.Syntax.Common
import Agda.Syntax.Concrete as C
import Agda.Syntax.Concrete.Glyph
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty
import Agda.Syntax.Info (mkDefInfo)
import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Translation.AbstractToConcrete hiding (withScope)
import Agda.Syntax.Scope.Base

import Agda.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.Highlighting.Precise hiding (Error, Postulate, singleton)
import Agda.Interaction.Imports  ( Mode, pattern ScopeCheck, pattern TypeCheck )
import qualified Agda.Interaction.Imports as Imp
import Agda.Interaction.Highlighting.Generate

import Agda.Compiler.Backend

import Agda.Auto.Auto as Auto

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 hiding (Mode)
import Agda.Utils.Singleton
import Agda.Utils.String
import Agda.Utils.Time
import Agda.Utils.Tuple

import Agda.Utils.Impossible

------------------------------------------------------------------------
-- The CommandM monad

-- | Restore both 'TCState' and 'CommandState'.

localStateCommandM :: CommandM a -> CommandM a
localStateCommandM :: CommandM a -> CommandM a
localStateCommandM 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

-- | Restore 'TCState', do not touch 'CommandState'.

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

-- | Build an opposite action to 'lift' for state monads.

revLift
    :: MonadState st m
    => (forall c . m c -> st -> k (c, st))      -- ^ run
    -> (forall b . k b -> m b)                  -- ^ lift
    -> (forall x . (m a -> k x) -> k x) -> m a  -- ^ reverse lift in double negative position
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 forall c. m c -> st -> k (c, st)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
    st
st <- m st
forall s (m :: * -> *). MonadState s m => m s
get
    (a
a, 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))  -- ^ run
    -> (forall b . k b -> m b)                        -- ^ lift
    -> (forall x . (m a -> k x) -> k x) -> m a        -- ^ reverse lift in double negative position
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 forall c. m c -> TCState -> k (c, TCState)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
    TCState
st <- m TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
    (a
a, 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

-- | Opposite of 'liftIO' for 'CommandM'.
--
-- This function should only be applied to computations that are
-- guaranteed not to raise any errors (except for 'IOException's).

commandMToIO :: (forall x . (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO forall x. (CommandM a -> IO x) -> IO x
ci_i = (forall c.
 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
-> (forall 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
$ \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)

-- | Lift a TCM action transformer to a CommandM action transformer.

liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT forall a. TCM a -> TCM a
f CommandM a
m = (forall c.
 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
-> (forall 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)

-- | Ditto, but restore state.

liftCommandMTLocalState :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMTLocalState :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMTLocalState forall a. TCM a -> TCM a
f = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT 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

-- | Put a response by the callback function given by 'stInteractionOutputCallback'.

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


-- | A Lens for 'theInteractionPoints'.

modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints :: ([InteractionId] -> [InteractionId]) -> StateT CommandState TCM ()
modifyTheInteractionPoints [InteractionId] -> [InteractionId]
f = (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s ->
  CommandState
s { theInteractionPoints :: [InteractionId]
theInteractionPoints = [InteractionId] -> [InteractionId]
f (CommandState -> [InteractionId]
theInteractionPoints CommandState
s) }


-- * Operations for manipulating 'oldInteractionScopes'.

-- | A Lens for 'oldInteractionScopes'.
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes)
-> StateT CommandState TCM ()
modifyOldInteractionScopes OldInteractionScopes -> OldInteractionScopes
f = (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s ->
  CommandState
s { oldInteractionScopes :: 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 InteractionId
ii 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 VerboseKey
"interaction.scope" VerboseLevel
20 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"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 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 VerboseKey
"interaction.scope" VerboseLevel
20 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"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 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
    Maybe ScopeInfo
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
$ VerboseKey
"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 ScopeInfo
scope -> ScopeInfo -> CommandM ScopeInfo
forall (m :: * -> *) a. Monad m => a -> m a
return ScopeInfo
scope

-- | Do setup and error handling for a command.

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 forall a. CommandM a -> CommandM a
wrap StateT CommandState TCM ()
onFail StateT CommandState TCM ()
cmd = StateT CommandState TCM () -> StateT CommandState TCM ()
handleNastyErrors (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
wrap (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
    TCState
oldState <- StateT CommandState TCM TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC

    -- -- Andreas, 2016-11-18 OLD CODE:
    -- -- onFail and handleErr are executed in "new" command state (not TCState).
    -- -- But it seems that if an exception is raised, it is identical to the old state,
    -- -- see code for catchErr.
    -- res <- (`catchErr` (return . Just)) $ Nothing <$ cmd
    -- maybe (return ()) (\ e -> onFail >> handleErr e) res

    -- Andreas, 2016-11-18 NEW CODE: execute onFail and handleErr in handler
    -- which means (looking at catchErr) they run in state s rathern than s'.
    -- Yet, it looks like s == s' in case the command failed.
    StateT CommandState TCM ()
cmd StateT CommandState TCM ()
-> (TCErr -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
`catchErr` \ TCErr
e -> do
      StateT CommandState TCM ()
onFail
      Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
handleErr Maybe HighlightingMethod
forall a. Maybe a
Nothing TCErr
e
      -- Andreas, 2016-11-18, issue #2174
      -- Reset TCState after error is handled, to get rid of metas created during failed command
      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
    -- Preserves state so we can do unsolved meta highlighting
    catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
    catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr CommandM a
m TCErr -> CommandM a
h = do
      CommandState
s       <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
      (a
x, 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_` \ 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

    -- Handle every possible kind of error (#637), except for
    -- AsyncCancelled, which is used to abort Agda.
    handleNastyErrors :: CommandM () -> CommandM ()
    handleNastyErrors :: StateT CommandState TCM () -> StateT CommandState TCM ()
handleNastyErrors StateT CommandState TCM ()
m = (forall x. (StateT CommandState TCM () -> IO x) -> IO x)
-> StateT CommandState TCM ()
forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ((forall x. (StateT CommandState TCM () -> IO x) -> IO x)
 -> StateT CommandState TCM ())
-> (forall x. (StateT CommandState TCM () -> IO x) -> IO x)
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ StateT CommandState TCM () -> IO x
toIO -> do
      let handle :: SomeException -> IO (Either AsyncCancelled x)
handle SomeException
e =
            x -> Either AsyncCancelled x
forall a b. b -> Either a b
Right (x -> Either AsyncCancelled x)
-> IO x -> IO (Either AsyncCancelled x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
              StateT CommandState TCM () -> IO x
toIO (Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
handleErr (HighlightingMethod -> Maybe HighlightingMethod
forall a. a -> Maybe a
Just HighlightingMethod
Direct) (TCErr -> StateT CommandState TCM ())
-> TCErr -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$
                        Range -> Doc -> TCErr
Exception Range
forall a. Range' a
noRange (Doc -> TCErr) -> Doc -> TCErr
forall a b. (a -> b) -> a -> b
$ VerboseKey -> Doc
text (VerboseKey -> Doc) -> VerboseKey -> Doc
forall a b. (a -> b) -> a -> b
$ SomeException -> VerboseKey
forall a. Show a => a -> VerboseKey
show SomeException
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 AsyncCancelled x)
generalHandler (SomeException
e :: E.SomeException) = SomeException -> IO (Either AsyncCancelled 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)
generalHandler
      case Either AsyncCancelled x
r of
        Right x
x -> x -> IO x
forall (m :: * -> *) a. Monad m => a -> m a
return x
x
        Left AsyncCancelled
e  -> AsyncCancelled -> IO x
forall e a. Exception e => e -> IO a
E.throwIO AsyncCancelled
e

    -- Displays an error and instructs Emacs to jump to the site of the
    -- error. Because this function may switch the focus to another file
    -- the status information is also updated.
    handleErr :: Maybe HighlightingMethod -> TCErr -> StateT CommandState TCM ()
handleErr Maybe HighlightingMethod
method TCErr
e = do
        HighlightingInfoBuilder
unsolved <- TCMT IO HighlightingInfoBuilder
-> StateT CommandState TCM HighlightingInfoBuilder
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO HighlightingInfoBuilder
 -> StateT CommandState TCM HighlightingInfoBuilder)
-> TCMT IO HighlightingInfoBuilder
-> StateT CommandState TCM HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ TCMT IO HighlightingInfoBuilder
computeUnsolvedInfo
        HighlightingInfoBuilder
err     <- TCMT IO HighlightingInfoBuilder
-> StateT CommandState TCM HighlightingInfoBuilder
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO HighlightingInfoBuilder
 -> StateT CommandState TCM HighlightingInfoBuilder)
-> TCMT IO HighlightingInfoBuilder
-> StateT CommandState TCM HighlightingInfoBuilder
forall a b. (a -> b) -> a -> b
$ TCErr -> TCMT IO HighlightingInfoBuilder
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  <- case Maybe HighlightingMethod
method of
          Maybe HighlightingMethod
Nothing -> 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
          Just HighlightingMethod
m  -> HighlightingMethod -> StateT CommandState TCM HighlightingMethod
forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingMethod
m
        let info :: HighlightingInfo
info = HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder -> HighlightingInfo)
-> HighlightingInfoBuilder -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ HighlightingInfoBuilder
err HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> HighlightingInfoBuilder
unsolved
                     -- Errors take precedence over unsolved things.

        -- TODO: make a better predicate for this
        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
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 -> 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
showIrr <- 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
optShowIrrelevant (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 a. HasRange a => a -> Range
getRange TCErr
e) [Response] -> [Response] -> [Response]
forall a. [a] -> [a] -> [a]
++
            [ HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response
Resp_HighlightingInfo HighlightingInfo
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 -> Bool -> Status
Status { sChecked :: Bool
sChecked = Bool
False
                                   , sShowImplicitArguments :: Bool
sShowImplicitArguments = Bool
showImpl
                                   , sShowIrrelevantArguments :: Bool
sShowIrrelevantArguments = Bool
showIrr
                                   } ]

-- | Run an 'IOTCM' value, catch the exceptions, emit output
--
--   If an error happens the state of 'CommandM' does not change,
--   but stPersistent may change (which contains successfully
--   loaded interfaces for example).

runInteraction :: IOTCM -> CommandM ()
runInteraction :: IOTCM -> StateT CommandState TCM ()
runInteraction (IOTCM VerboseKey
current HighlightingLevel
highlighting HighlightingMethod
highlightingMethod 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
    -- Raises an error if the given file is not the one currently
    -- loaded.
    Maybe CurrentFile
cf <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
    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
/= (CurrentFile -> AbsolutePath
currentFilePath (CurrentFile -> AbsolutePath)
-> Maybe CurrentFile -> Maybe AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CurrentFile
cf)) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
        let mode :: Mode
mode = Mode
TypeCheck
        VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a.
VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' VerboseKey
current [] Bool
True Mode
mode ((CheckResult -> StateT CommandState TCM ())
 -> StateT CommandState TCM ())
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \CheckResult
_ -> () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    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 CurrentFile
cf' <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
    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
== (CurrentFile -> AbsolutePath
currentFilePath (CurrentFile -> AbsolutePath)
-> Maybe CurrentFile -> Maybe AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CurrentFile
cf')) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
        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 :: forall a. CommandM a -> CommandM a
    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
            }

    -- If an independent command fails we should reset theCurrentFile (Issue853).
    onFail :: StateT CommandState TCM ()
onFail | Interaction' Range -> Bool
independent Interaction' Range
cmd = (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s -> CommandState
s { theCurrentFile :: Maybe CurrentFile
theCurrentFile = Maybe CurrentFile
forall a. Maybe a
Nothing }
           | Bool
otherwise       = () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

------------------------------------------------------------------------
-- Command queues

-- | If the next command from the command queue is anything but an
-- actual command, then the command is returned.
--
-- If the command is an 'IOTCM' command, then the following happens:
-- The given computation is applied to the command and executed. If an
-- abort command is encountered (and acted upon), then the computation
-- is interrupted, the persistent state and all options are restored,
-- and some commands are sent to the frontend. If the computation was
-- not interrupted, then its result is returned.

-- TODO: It might be nice if some of the changes to the persistent
-- state inflicted by the interrupted computation were preserved.

maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort :: (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort 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
  (Integer
n, 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
    Command
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 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 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 ((a
x, CommandState
commandState'), TCState
tcState') -> do
          TCState -> StateT CommandState TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcState'
          CommandState -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CommandState
commandState'
          case IOTCM
c of
            IOTCM VerboseKey
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
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
            IOTCM
_ -> 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 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

  -- Returns if the currently executing command should be aborted.
  -- The "abort number" is returned.

  waitForAbort
    :: Integer       -- The number of the currently executing command.
    -> CommandQueue  -- The command queue.
    -> IO Integer
  waitForAbort :: Integer -> CommandQueue -> IO Integer
waitForAbort Integer
n CommandQueue
q = do
    STM Integer -> IO Integer
forall a. STM a -> IO a
atomically (STM Integer -> IO Integer) -> STM Integer -> IO Integer
forall a b. (a -> b) -> a -> b
$ do
      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 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'
        Maybe Integer
_                 -> STM Integer
forall a. STM a
retry

  -- Removes every command for which the command number is at most
  -- the given number (the "abort number") from the command queue.
  --
  -- New commands could be added to the end of the queue while this
  -- computation is running. This does not lead to a race condition,
  -- because those commands have higher command numbers, so they will
  -- not be removed.

  popAbortedCommands :: CommandQueue -> Integer -> IO ()
  popAbortedCommands :: CommandQueue -> Integer -> IO ()
popAbortedCommands CommandQueue
q 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
        Maybe (Integer, Command)
Nothing -> Bool -> STM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Just (Integer, Command)
c  ->
          if (Integer, Command) -> Integer
forall a b. (a, b) -> a
fst (Integer, Command)
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n then
            Bool -> STM Bool
forall (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

-- | Creates a command queue, and forks a thread that writes commands
-- to the queue. The queue is returned.

initialiseCommandQueue
  :: IO Command
     -- ^ Returns the next command.
  -> IO CommandQueue
initialiseCommandQueue :: IO Command -> IO CommandQueue
initialiseCommandQueue 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 -- Read commands. The argument is the number of the previous
      -- command (other than abort commands) that was read, if any.
      readCommands :: Integer -> IO ()
readCommands Integer
n = do
        Command
c <- IO Command
next
        case Command
c of
          Command (IOTCM VerboseKey
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
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
          Command
_ -> do
            let n' :: Integer
n' = (Integer -> Integer
forall a. Enum a => a -> a
succ Integer
n)
            STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan (Integer, Command) -> (Integer, Command) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Integer, Command)
commands (Integer
n', Command
c)
            case Command
c of
              Command
Done -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Command
_    -> Integer -> IO ()
readCommands Integer
n'

  ThreadId
_ <- IO () -> IO ThreadId
forkIO (Integer -> IO ()
readCommands Integer
0)

  CommandQueue -> IO CommandQueue
forall (m :: * -> *) a. Monad m => a -> m a
return (CommandQueue :: TChan (Integer, Command) -> TVar (Maybe Integer) -> CommandQueue
CommandQueue { TVar (Maybe Integer)
TChan (Integer, Command)
abort :: TVar (Maybe Integer)
commands :: TChan (Integer, Command)
abort :: TVar (Maybe Integer)
commands :: TChan (Integer, Command)
.. })

---------------------------------------------------------

-- | Can the command run even if the relevant file has not been loaded
--   into the state?

independent :: Interaction -> Bool
independent :: Interaction' Range -> Bool
independent (Cmd_load {})                   = Bool
True
independent (Cmd_compile {})                = Bool
True
independent (Cmd_load_highlighting_info {}) = Bool
True
independent Cmd_tokenHighlighting {}        = Bool
True
independent Interaction' Range
Cmd_show_version                = Bool
True
independent Interaction' Range
_                               = Bool
False

-- | Should 'Resp_InteractionPoints' be issued after the command has
-- run?

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 ShowIrrelevantArgs{}                = Bool
False
updateInteractionPointsAfter ToggleIrrelevantArgs{}              = Bool
False
updateInteractionPointsAfter Cmd_give{}                          = Bool
True
updateInteractionPointsAfter Cmd_refine{}                        = Bool
True
updateInteractionPointsAfter Cmd_intro{}                         = Bool
True
updateInteractionPointsAfter Cmd_refine_or_intro{}               = Bool
True
updateInteractionPointsAfter Cmd_autoOne{}                       = Bool
True
updateInteractionPointsAfter Cmd_autoAll{}                       = Bool
True
updateInteractionPointsAfter Cmd_context{}                       = Bool
False
updateInteractionPointsAfter Cmd_helper_function{}               = Bool
False
updateInteractionPointsAfter Cmd_infer{}                         = Bool
False
updateInteractionPointsAfter Cmd_goal_type{}                     = Bool
False
updateInteractionPointsAfter Cmd_elaborate_give{}                = Bool
True
updateInteractionPointsAfter Cmd_goal_type_context{}             = Bool
False
updateInteractionPointsAfter Cmd_goal_type_context_infer{}       = Bool
False
updateInteractionPointsAfter Cmd_goal_type_context_check{}       = Bool
False
updateInteractionPointsAfter Cmd_show_module_contents{}          = Bool
False
updateInteractionPointsAfter Cmd_make_case{}                     = Bool
True
updateInteractionPointsAfter Cmd_compute{}                       = Bool
False
updateInteractionPointsAfter Cmd_why_in_scope{}                  = Bool
False
updateInteractionPointsAfter Cmd_why_in_scope_toplevel{}         = Bool
False
updateInteractionPointsAfter Cmd_show_version{}                  = Bool
False
updateInteractionPointsAfter Cmd_abort{}                         = Bool
False
updateInteractionPointsAfter Cmd_exit{}                          = Bool
False

-- | Interpret an interaction

interpret :: Interaction -> CommandM ()

interpret :: Interaction' Range -> StateT CommandState TCM ()
interpret (Cmd_load VerboseKey
m [VerboseKey]
argv) =
  VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a.
VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' VerboseKey
m [VerboseKey]
argv Bool
True Mode
mode ((CheckResult -> StateT CommandState TCM ())
 -> StateT CommandState TCM ())
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \CheckResult
_ -> Interaction' Range -> StateT CommandState TCM ()
interpret (Interaction' Range -> StateT CommandState TCM ())
-> Interaction' Range -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Interaction' Range
forall range. Rewrite -> Interaction' range
Cmd_metas Rewrite
AsIs
  where
  mode :: Mode
mode = Mode
TypeCheck

interpret (Cmd_compile CompilerBackend
backend VerboseKey
file [VerboseKey]
argv) =
  VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a.
VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' VerboseKey
file [VerboseKey]
argv Bool
allowUnsolved Mode
mode ((CheckResult -> StateT CommandState TCM ())
 -> StateT CommandState TCM ())
-> (CheckResult -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CheckResult
checkResult -> do
    [TCWarning]
mw <- TCM [TCWarning] -> StateT CommandState TCM [TCWarning]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [TCWarning] -> StateT CommandState TCM [TCWarning])
-> TCM [TCWarning] -> StateT CommandState TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ [TCWarning] -> TCM [TCWarning]
forall (m :: * -> *). HasOptions m => [TCWarning] -> m [TCWarning]
applyFlagsToTCWarnings ([TCWarning] -> TCM [TCWarning]) -> [TCWarning] -> TCM [TCWarning]
forall a b. (a -> b) -> a -> b
$ CheckResult -> [TCWarning]
crWarnings CheckResult
checkResult
    case [TCWarning]
mw of
      [] -> 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
          CompilerBackend
LaTeX                    -> VerboseKey -> IsMain -> CheckResult -> TCMT IO ()
callBackend VerboseKey
"LaTeX" IsMain
IsMain CheckResult
checkResult
          CompilerBackend
QuickLaTeX               -> VerboseKey -> IsMain -> CheckResult -> TCMT IO ()
callBackend VerboseKey
"LaTeX" IsMain
IsMain CheckResult
checkResult
          OtherBackend VerboseKey
"GHCNoMain" -> VerboseKey -> IsMain -> CheckResult -> TCMT IO ()
callBackend VerboseKey
"GHC" IsMain
NotMain CheckResult
checkResult   -- for backwards compatibility
          OtherBackend VerboseKey
b           -> VerboseKey -> IsMain -> CheckResult -> TCMT IO ()
callBackend VerboseKey
b IsMain
IsMain CheckResult
checkResult
        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
. CompilerBackend -> WarningsAndNonFatalErrors -> DisplayInfo
Info_CompilationOk CompilerBackend
backend (WarningsAndNonFatalErrors -> StateT CommandState TCM ())
-> StateT CommandState TCM WarningsAndNonFatalErrors
-> StateT CommandState TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO WarningsAndNonFatalErrors
-> StateT CommandState TCM WarningsAndNonFatalErrors
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO WarningsAndNonFatalErrors
B.getWarningsAndNonFatalErrors
      w :: [TCWarning]
w@(TCWarning
_:[TCWarning]
_) -> 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
  where
  allowUnsolved :: Bool
allowUnsolved = CompilerBackend
backend CompilerBackend -> [CompilerBackend] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CompilerBackend
LaTeX, CompilerBackend
QuickLaTeX]
  mode :: Mode
mode | CompilerBackend
QuickLaTeX <- CompilerBackend
backend = Mode
ScopeCheck
       | Bool
otherwise             = Mode
TypeCheck

interpret Interaction' Range
Cmd_constraints =
    DisplayInfo -> 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 Rewrite
norm) = 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 -> StateT CommandState TCM Goals)
-> TCMT IO Goals -> StateT CommandState TCM Goals
forall a b. (a -> b) -> a -> b
$ Rewrite -> Rewrite -> TCMT IO Goals
B.getGoals' Rewrite
norm (Rewrite -> Rewrite -> Rewrite
forall a. Ord a => a -> a -> a
max Rewrite
Simplified Rewrite
norm)
  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
B.getWarningsAndNonFatalErrors

interpret (Cmd_show_module_contents_toplevel Rewrite
norm VerboseKey
s) =
  StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> VerboseKey -> StateT CommandState TCM ()
showModuleContents Rewrite
norm Range
forall a. Range' a
noRange VerboseKey
s

interpret (Cmd_search_about_toplevel Rewrite
norm VerboseKey
s) =
  StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> VerboseKey -> StateT CommandState TCM ()
searchAbout Rewrite
norm Range
forall a. Range' a
noRange VerboseKey
s

interpret (Cmd_solveAll Rewrite
norm)        = Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
solveInstantiatedGoals Rewrite
norm Maybe InteractionId
forall a. Maybe a
Nothing
interpret (Cmd_solveOne Rewrite
norm InteractionId
ii Range
_ VerboseKey
_) = Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
solveInstantiatedGoals Rewrite
norm' (InteractionId -> Maybe InteractionId
forall a. a -> Maybe a
Just InteractionId
ii)
  -- `solveOne` is called via `agda2-maybe-normalised` which does not use
  -- AsIs < Simplified < Normalised but rather Simplified < Instantiated < Normalised
  -- So we remap the Rewrite modifiers to match solveAll's behaviour.
  -- NB: instantiate is called in getSolvedInteractionPoints no matter what.
  where norm' :: Rewrite
norm' = case Rewrite
norm of
                  Rewrite
Simplified   -> Rewrite
AsIs
                  Rewrite
Instantiated -> Rewrite
Simplified
                  Rewrite
_            -> Rewrite
norm

interpret (Cmd_infer_toplevel Rewrite
norm VerboseKey
s) = do
  (Maybe CPUTime
time, 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 ComputeMode
cmode VerboseKey
s) = do
  (Maybe CPUTime
time, 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
B.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
B.computeIgnoreAbstract ComputeMode
cmode then TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
           (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputeMode -> Expr -> TCM Expr
B.evalInCurrent ComputeMode
cmode
-- interpret (Cmd_compute_toplevel cmode s) =
--   parseAndDoAtToplevel action Info_NormalForm $ computeWrapInput cmode s
--   where
--   action = allowNonTerminatingReductions
--          . (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
--          . (B.showComputed cmode <=< B.evalInCurrent)


interpret (ShowImplicitArgs 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 Interaction' Range
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 (ShowIrrelevantArgs Bool
showIrr) = 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) { optShowIrrelevant :: Bool
optShowIrrelevant = Bool
showIrr } }

interpret Interaction' Range
ToggleIrrelevantArgs = 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 { optShowIrrelevant :: Bool
optShowIrrelevant = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optShowIrrelevant PragmaOptions
ps } }

interpret (Cmd_load_highlighting_info 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
    -- Make sure that the include directories have
    -- been set.
    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 (HighlightingInfo, HighlightingMethod, ModuleToSource)
    -> IO [Response])
-> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT IO [Response]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> IO [Response]
tellToUpdateHighlighting (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
 -> TCMT IO [Response])
-> TCMT
     IO (Maybe (HighlightingInfo, 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
      if Bool
ex
        then
           do
              Source
src <- SourceFile -> TCM Source
Imp.parseSource SourceFile
absSource
              let m :: TopLevelModuleName
m = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
              TopLevelModuleName
-> SourceFile -> Maybe TopLevelModuleName -> TCMT IO ()
checkModuleName TopLevelModuleName
m SourceFile
absSource Maybe TopLevelModuleName
forall a. Maybe a
Nothing
              Maybe ModuleInfo
mmi <- TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
m
              case Maybe ModuleInfo
mmi of
                Maybe ModuleInfo
Nothing -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
                Just ModuleInfo
mi ->
                  if Text -> Hash
hashText (Source -> Text
Imp.srcText Source
src) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Interface -> Hash
iSourceHash (ModuleInfo -> Interface
miInterface ModuleInfo
mi)
                    then do
                      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 (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
 -> TCMT
      IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)))
-> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a b. (a -> b) -> a -> b
$ (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. a -> Maybe a
Just (Interface -> HighlightingInfo
iHighlighting (Interface -> HighlightingInfo) -> Interface -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ ModuleInfo -> Interface
miInterface ModuleInfo
mi, HighlightingMethod
method, ModuleToSource
modFile)
                    else
                      Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
            TCMT
  IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
-> (TCErr
    -> TCMT
         IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)))
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
        else
          Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, 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 VerboseKey
source Remove
remove) = do
  Maybe HighlightingInfo
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 HighlightingInfo
-> StateT CommandState TCM (Maybe HighlightingInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe HighlightingInfo
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 HighlightingInfo)
-> StateT CommandState TCM (Maybe HighlightingInfo)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Maybe HighlightingInfo)
 -> StateT CommandState TCM (Maybe HighlightingInfo))
-> TCMT IO (Maybe HighlightingInfo)
-> StateT CommandState TCM (Maybe HighlightingInfo)
forall a b. (a -> b) -> a -> b
$ (HighlightingInfo -> Maybe HighlightingInfo
forall a. a -> Maybe a
Just (HighlightingInfo -> Maybe HighlightingInfo)
-> TCMT IO HighlightingInfo -> TCMT IO (Maybe HighlightingInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCMT IO HighlightingInfo
generateTokenInfo AbsolutePath
source')
                           TCMT IO (Maybe HighlightingInfo)
-> (TCErr -> TCMT IO (Maybe HighlightingInfo))
-> TCMT IO (Maybe HighlightingInfo)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ ->
                        Maybe HighlightingInfo -> TCMT IO (Maybe HighlightingInfo)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe HighlightingInfo
forall a. Maybe a
Nothing
      StateT CommandState TCM (Maybe HighlightingInfo)
-> StateT CommandState TCM ()
-> StateT CommandState TCM (Maybe HighlightingInfo)
forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally`
    case Remove
remove of
      Remove
Remove -> IO () -> StateT CommandState TCM ()
forall (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
      Remove
Keep   -> () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  case Maybe HighlightingInfo
info of
    Just HighlightingInfo
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 -> HighlightingInfo -> TCMT IO ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
RemoveHighlighting HighlightingInfo
info'
    Maybe HighlightingInfo
Nothing    -> () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

interpret (Cmd_highlight InteractionId
ii Range
rng 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 -> ScopeM (AbsOfCon Expr)
forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
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 -> HighlightingInfo -> TCMT IO ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (HighlightingInfo -> TCMT IO ())
-> TCMT IO HighlightingInfo -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
               Range -> VerboseKey -> TCMT IO HighlightingInfo
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 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 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 Info_Error
err TCM a
m = TCMT IO (Either Info_Error a) -> ExceptT Info_Error TCM a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (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` \ TCErr
_ -> 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)
      -- freshTCM to avoid scope checking creating new interaction points

interpret (Cmd_give   UseForce
force InteractionId
ii Range
rng 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 InteractionId
ii Range
rng 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 Bool
pmLambda InteractionId
ii Range
rng VerboseKey
_) = 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 -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ 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
    [VerboseKey
s]   -> UseForce
-> InteractionId
-> Range
-> VerboseKey
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng VerboseKey
s GiveRefine
Intro
    VerboseKey
_:VerboseKey
_:[VerboseKey]
_ -> 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 Bool
pmLambda InteractionId
ii Range
r 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 InteractionId
ii Range
rng VerboseKey
hint) = do
  -- Andreas, 2014-07-05 Issue 1226:
  -- Save the state to have access to even those interaction ids
  -- that Auto solves (since Auto gives the solution right away).
  TCState
st <- StateT CommandState TCM TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  (Maybe CPUTime
time , 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 [(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 VerboseKey
"auto" VerboseLevel
10 (VerboseKey -> TCMT IO ()) -> VerboseKey -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"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
$ \(InteractionId
ii', VerboseKey
sol) -> do
      -- Andreas, 2014-07-05 Issue 1226:
      -- For highlighting, Resp_GiveAction needs to access
      -- the @oldInteractionScope@s of the interaction points solved by Auto.
      -- We dig them out from the state before Auto was invoked.
      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
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii')
      -- Andreas, 2014-07-07: NOT TRUE:
      -- -- Andreas, 2014-07-05: The following should be obsolete,
      -- -- as Auto has removed the interaction points already:
      -- modifyTheInteractionPoints $ filter (/= 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
    -- Andreas, 2014-07-07: Remove the interaction points in one go.
    ([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
     Maybe VerboseKey
Nothing  -> Interaction' Range -> StateT CommandState TCM ()
interpret (Interaction' Range -> StateT CommandState TCM ())
-> Interaction' Range -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Interaction' Range
forall range. Rewrite -> Interaction' range
Cmd_metas Rewrite
AsIs
     Just 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 [VerboseKey]
cs -> do
    case AutoResult -> Maybe VerboseKey
autoMessage AutoResult
res of
     Maybe VerboseKey
Nothing  -> () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     Just 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 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 Interaction' Range
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 = VerboseLevel
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
$ \ 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 (VerboseKey
"-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]
++ VerboseKey
"ms")
      case AutoResult -> AutoProgress
autoProgress AutoResult
res of
        Solutions [(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
$ \ (InteractionId
jj, 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
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m 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
        AutoProgress
_ -> [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 Rewrite
norm InteractionId
ii Range
_ VerboseKey
_) =
  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]
B.getResponseContext Rewrite
norm InteractionId
ii)

interpret (Cmd_helper_function Rewrite
norm InteractionId
ii Range
rng VerboseKey
s) = do
  -- Create type of application of new helper function that would solve the goal.
  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 (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM (OutputConstraint' Expr Expr)
 -> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM (OutputConstraint' Expr Expr)
 -> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ Rewrite
-> InteractionId
-> Range
-> 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 Rewrite
norm InteractionId
ii Range
rng 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 (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ InteractionId -> Rewrite -> Expr -> TCM Expr
B.typeInMeta InteractionId
ii Rewrite
norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> Range -> 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 Rewrite
norm InteractionId
ii Range
_ VerboseKey
_) =
  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 Rewrite
norm InteractionId
ii Range
rng VerboseKey
s) =
  UseForce
-> InteractionId
-> Range
-> VerboseKey
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng VerboseKey
s (GiveRefine -> StateT CommandState TCM ())
-> GiveRefine -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> GiveRefine
ElaborateGive Rewrite
norm

interpret (Cmd_goal_type_context Rewrite
norm InteractionId
ii Range
rng 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 Rewrite
norm InteractionId
ii Range
rng VerboseKey
s) = do
  -- In case of the empty expression to type, don't fail with
  -- a stupid parse error, but just fall back to
  -- Cmd_goal_type_context.
  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 (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii
                    (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ InteractionId -> Rewrite -> Expr -> TCM Expr
B.typeInMeta InteractionId
ii Rewrite
norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> Range -> 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 Rewrite
norm InteractionId
ii Range
rng 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 (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Term -> TCM Term) -> TCM Term -> TCM Term
forall a b. (a -> b) -> a -> b
$ do
    Expr
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 InteractionId
_ Expr
ty -> Expr -> Type -> TCM Term
checkExpr Expr
expr (Type -> TCM Term) -> TCMT IO Type -> TCM Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO Type
isType_ Expr
ty
      OutputConstraint Expr InteractionId
_           -> TCM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    Rewrite -> Term -> TCM Term
forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
B.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 Rewrite
norm 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 -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> VerboseKey -> StateT CommandState TCM ()
showModuleContents Rewrite
norm Range
rng VerboseKey
s

interpret (Cmd_why_in_scope_toplevel VerboseKey
s) =
  StateT CommandState TCM () -> StateT CommandState TCM ()
forall a. CommandM a -> CommandM a
atTopLevel (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> StateT CommandState TCM ()
whyInScope VerboseKey
s

interpret (Cmd_why_in_scope InteractionId
ii Range
_range 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 -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> StateT CommandState TCM ()
whyInScope VerboseKey
s

interpret (Cmd_make_case InteractionId
ii Range
rng VerboseKey
s) = do
  (QName
f, CaseContext
casectxt, [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 -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ 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) -- don't shadow the names in this telescope
    UnicodeOrAscii
unicode <- (TCState -> UnicodeOrAscii)
-> StateT CommandState TCM UnicodeOrAscii
forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC ((TCState -> UnicodeOrAscii)
 -> StateT CommandState TCM UnicodeOrAscii)
-> (TCState -> UnicodeOrAscii)
-> StateT CommandState TCM UnicodeOrAscii
forall a b. (a -> b) -> a -> b
$ PragmaOptions -> UnicodeOrAscii
optUseUnicode (PragmaOptions -> UnicodeOrAscii)
-> (TCState -> PragmaOptions) -> TCState -> UnicodeOrAscii
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 -> TCM Doc) -> [Clause] -> TCM [Doc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), 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 (UnicodeOrAscii -> CaseContext -> VerboseKey -> VerboseKey
extlam_dropName UnicodeOrAscii
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 -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"interaction.case" VerboseLevel
60 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
      [ TCM Doc
"InteractionTop.Cmd_make_case"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TCP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
        [ TCM Doc
"cs   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat ((Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cs)
        , TCM Doc
"pcs  = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat ((Doc -> TCM Doc) -> [Doc] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return [Doc]
pcs)
        , TCM Doc
"pcs' = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat ((VerboseKey -> TCM Doc) -> [VerboseKey] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative 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 -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> TCM Doc -> m ()
reportSDoc VerboseKey
"interaction.case" VerboseLevel
90 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
      [ TCM Doc
"InteractionTop.Cmd_make_case"
      , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
TCP.nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
        [ TCM Doc
"cs   = " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> VerboseKey -> TCM Doc
forall (m :: * -> *). Applicative 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 CaseContext
Nothing = MakeCaseVariant
R.Function
    makeCaseVariant Just{}  = MakeCaseVariant
R.ExtendedLambda

    -- very dirty hack, string manipulation by dropping the function name
    -- and replacing the last " = " with " -> ". It's important not to replace
    -- the equal sign in named implicit with an arrow!
    extlam_dropName :: UnicodeOrAscii -> CaseContext -> String -> String
    extlam_dropName :: UnicodeOrAscii -> CaseContext -> VerboseKey -> VerboseKey
extlam_dropName UnicodeOrAscii
_ CaseContext
Nothing VerboseKey
x = VerboseKey
x
    extlam_dropName UnicodeOrAscii
glyphMode Just{}  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]
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 VerboseLevel
1 ([VerboseKey] -> [VerboseKey]) -> [VerboseKey] -> [VerboseKey]
forall a b. (a -> b) -> a -> b
$ VerboseKey -> [VerboseKey]
words VerboseKey
x
      where
        arrow :: VerboseKey
arrow = Doc -> VerboseKey
render (Doc -> VerboseKey) -> Doc -> VerboseKey
forall a b. (a -> b) -> a -> b
$ SpecialCharacters -> Doc
_arrow (SpecialCharacters -> Doc) -> SpecialCharacters -> Doc
forall a b. (a -> b) -> a -> b
$ UnicodeOrAscii -> SpecialCharacters
specialCharactersForGlyphs UnicodeOrAscii
glyphMode
        replEquals :: [VerboseKey] -> [VerboseKey]
replEquals (VerboseKey
"=" : [VerboseKey]
ws) = VerboseKey
arrow VerboseKey -> [VerboseKey] -> [VerboseKey]
forall a. a -> [a] -> [a]
: [VerboseKey]
ws
        replEquals (VerboseKey
w   : [VerboseKey]
ws) = VerboseKey
w VerboseKey -> [VerboseKey] -> [VerboseKey]
forall a. a -> [a] -> [a]
: [VerboseKey] -> [VerboseKey]
replEquals [VerboseKey]
ws
        replEquals []         = []

interpret (Cmd_compute ComputeMode
cmode InteractionId
ii Range
rng 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 (VerboseKey -> TCM Expr) -> VerboseKey -> TCM Expr
forall a b. (a -> b) -> a -> b
$ ComputeMode -> VerboseKey -> VerboseKey
B.computeWrapInput ComputeMode
cmode VerboseKey
s
    InteractionId -> TCM Expr -> TCM Expr
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ Bool -> (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a. Bool -> (a -> a) -> a -> a
applyWhen (ComputeMode -> Bool
B.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
$ ComputeMode -> Expr -> TCM Expr
B.evalInCurrent ComputeMode
cmode 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 Interaction' Range
Cmd_show_version = DisplayInfo -> StateT CommandState TCM ()
display_info DisplayInfo
Info_Version

interpret Interaction' Range
Cmd_abort = () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
interpret Interaction' Range
Cmd_exit  = () -> StateT CommandState TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Solved goals already instantiated internally
-- The second argument potentially limits it to one specific goal.
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> StateT CommandState TCM ()
solveInstantiatedGoals Rewrite
norm Maybe InteractionId
mii = do
  -- Andreas, 2016-10-23 issue #2280: throw away meta elims.
  [(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 (\ 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
           -- only solve metas which have a proper instantiation, i.e., not another meta
    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 (\ 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 (m :: * -> *) a a.
(MonadTrace m, ToConcrete a, MonadStConcreteNames m, HasOptions m,
 HasBuiltins m, MonadDebug m) =>
(a, MetaId, a) -> m (a, ConOfAbs a)
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) -> m (a, ConOfAbs a)
prt (a
i, MetaId
m, a
e) = do
        Closure Range
mi <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> m MetaVariable -> m (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
m
        ConOfAbs a
e' <- Closure Range -> m (ConOfAbs a) -> m (ConOfAbs a)
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
mi (m (ConOfAbs a) -> m (ConOfAbs a))
-> m (ConOfAbs a) -> m (ConOfAbs a)
forall a b. (a -> b) -> a -> b
$ Precedence -> a -> m (ConOfAbs a)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
Precedence -> a -> m (ConOfAbs a)
abstractToConcreteCtx Precedence
TopCtx a
e
        (a, ConOfAbs a) -> m (a, ConOfAbs a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
i, ConOfAbs a
e')

-- | @cmd_load' file argv unsolvedOk cmd@
--   loads the module in file @file@,
--   using @argv@ as the command-line options.
--
-- If type checking completes without any exceptions having been
-- encountered then the command @cmd r@ is executed, where @r@ is the
-- result of 'Imp.typeCheckMain'.

cmd_load'
  :: FilePath  -- ^ File to load into interaction.
  -> [String]  -- ^ Arguments to Agda for loading this file
  -> Bool      -- ^ Allow unsolved meta-variables?
  -> Mode      -- ^ Full type-checking, or only scope-checking?
  -> (CheckResult -> CommandM a)
               -- ^ Continuation after successful loading.
  -> CommandM a
cmd_load' :: VerboseKey
-> [VerboseKey]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' VerboseKey
file [VerboseKey]
argv Bool
unsolvedOK Mode
mode CheckResult -> CommandM a
cmd = do
    AbsolutePath
fp <- 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
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 AbsolutePath
fp
    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.
(HasCallStack, MonadTCError 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
$
      VerboseKey
"The file " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
file VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
" was not found."

    -- Forget the previous "current file" and interaction points.
    (CommandState -> CommandState) -> StateT CommandState TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> StateT CommandState TCM ())
-> (CommandState -> CommandState) -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
st -> CommandState
st { theInteractionPoints :: [InteractionId]
theInteractionPoints = []
                        , theCurrentFile :: Maybe CurrentFile
theCurrentFile       = Maybe CurrentFile
forall a. Maybe a
Nothing
                        }

    UTCTime
t <- IO UTCTime -> StateT CommandState TCM UTCTime
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO UTCTime -> StateT CommandState TCM UTCTime)
-> IO UTCTime -> StateT CommandState TCM UTCTime
forall a b. (a -> b) -> a -> b
$ VerboseKey -> IO UTCTime
getModificationTime VerboseKey
file

    -- Update the status. Because the "current file" is not set the
    -- status is not "Checked".
    StateT CommandState TCM ()
displayStatus

    -- Reset the state, preserving options and decoded modules. Note
    -- that if the include directories have changed, then the decoded
    -- modules are reset by TCM.setCommandLineOptions' below.
    TCMT IO () -> StateT CommandState TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO ()
resetState

    -- Clear the info buffer to make room for information about which
    -- module is currently being type-checked.
    Response -> StateT CommandState TCM ()
putResponse Response
Resp_ClearRunningInfo

    -- Remove any prior syntax highlighting.
    Response -> StateT CommandState TCM ()
putResponse (TokenBased -> Response
Resp_ClearHighlighting TokenBased
NotOnlyTokenBased)

    -- Parse the file.
    --
    -- Note that options are set below.
    Source
src <- TCM Source -> StateT CommandState TCM Source
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Source -> StateT CommandState TCM Source)
-> TCM Source -> StateT CommandState TCM Source
forall a b. (a -> b) -> a -> b
$ SourceFile -> TCM Source
Imp.parseSource (AbsolutePath -> SourceFile
SourceFile AbsolutePath
fp)

    -- Store the warnings.
    [TCWarning]
warnings <- Lens' [TCWarning] TCState -> StateT CommandState TCM [TCWarning]
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [TCWarning] TCState
stTCWarnings

    -- All options are reset when a file is reloaded, including the
    -- choice of whether or not to display implicit arguments.
    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 <- OptM ([Backend], CommandLineOptions)
-> StateT
     CommandState
     TCM
     (Either VerboseKey ([Backend], CommandLineOptions))
forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either VerboseKey opts)
runOptM (OptM ([Backend], CommandLineOptions)
 -> StateT
      CommandState
      TCM
      (Either VerboseKey ([Backend], CommandLineOptions)))
-> OptM ([Backend], CommandLineOptions)
-> StateT
     CommandState
     TCM
     (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 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.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ VerboseKey -> TypeError
GenericError VerboseKey
err
      Right ([Backend]
_, CommandLineOptions
opts) -> 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
 -> StateT CommandState TCM CommandLineOptions)
-> TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM CommandLineOptions
addTrustedExecutables CommandLineOptions
opts
        let update :: PragmaOptions -> PragmaOptions
update PragmaOptions
o = PragmaOptions
o { optAllowUnsolved :: Bool
optAllowUnsolved = Bool
unsolvedOK Bool -> Bool -> Bool
&& PragmaOptions -> Bool
optAllowUnsolved PragmaOptions
o}
            root :: AbsolutePath
root     = AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
fp (TopLevelModuleName -> AbsolutePath)
-> TopLevelModuleName -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ Source -> TopLevelModuleName
Imp.srcModuleName Source
src
        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 ()
TCM.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

    -- Restore the warnings that were saved above.
    Lens' [TCWarning] TCState
-> ([TCWarning] -> [TCWarning]) -> StateT CommandState TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
modifyTCLens Lens' [TCWarning] TCState
stTCWarnings ([TCWarning] -> [TCWarning] -> [TCWarning]
forall a. [a] -> [a] -> [a]
++ [TCWarning]
warnings)

    CheckResult
ok <- TCMT IO CheckResult -> StateT CommandState TCM CheckResult
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO CheckResult -> StateT CommandState TCM CheckResult)
-> TCMT IO CheckResult -> StateT CommandState TCM CheckResult
forall a b. (a -> b) -> a -> b
$ Mode -> Source -> TCMT IO CheckResult
Imp.typeCheckMain Mode
mode Source
src

    -- The module type checked. If the file was not changed while the
    -- type checker was running then the interaction points and the
    -- "current file" are stored.
    UTCTime
t' <- IO UTCTime -> StateT CommandState TCM UTCTime
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO UTCTime -> StateT CommandState TCM UTCTime)
-> IO UTCTime -> StateT CommandState TCM UTCTime
forall a b. (a -> b) -> a -> b
$ VerboseKey -> IO UTCTime
getModificationTime VerboseKey
file
    Bool -> StateT CommandState TCM () -> StateT CommandState TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (UTCTime
t UTCTime -> UTCTime -> Bool
forall a. Eq a => a -> a -> Bool
== UTCTime
t') (StateT CommandState TCM () -> StateT CommandState TCM ())
-> StateT CommandState TCM () -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ do
      [InteractionId]
is <- TCM [InteractionId] -> StateT CommandState TCM [InteractionId]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [InteractionId] -> StateT CommandState TCM [InteractionId])
-> TCM [InteractionId] -> StateT CommandState TCM [InteractionId]
forall a b. (a -> b) -> a -> b
$ [InteractionId] -> TCM [InteractionId]
forall (m :: * -> *).
(MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
[InteractionId] -> m [InteractionId]
sortInteractionPoints ([InteractionId] -> TCM [InteractionId])
-> TCM [InteractionId] -> TCM [InteractionId]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM [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
$ \CommandState
st -> CommandState
st { theInteractionPoints :: [InteractionId]
theInteractionPoints = [InteractionId]
is
                         , theCurrentFile :: Maybe CurrentFile
theCurrentFile       = CurrentFile -> Maybe CurrentFile
forall a. a -> Maybe a
Just (CurrentFile -> Maybe CurrentFile)
-> CurrentFile -> Maybe CurrentFile
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [VerboseKey] -> UTCTime -> CurrentFile
CurrentFile AbsolutePath
fp [VerboseKey]
argv UTCTime
t
                         }

    CheckResult -> CommandM a
cmd CheckResult
ok

-- | Set 'envCurrentPath' to 'theCurrentFile', if any.
withCurrentFile :: CommandM a -> CommandM a
withCurrentFile :: CommandM a -> CommandM a
withCurrentFile CommandM a
m = do
  Maybe AbsolutePath
mfile <- (CommandState -> Maybe AbsolutePath)
-> StateT CommandState TCM (Maybe AbsolutePath)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CommandState -> Maybe AbsolutePath)
 -> StateT CommandState TCM (Maybe AbsolutePath))
-> (CommandState -> Maybe AbsolutePath)
-> StateT CommandState TCM (Maybe AbsolutePath)
forall a b. (a -> b) -> a -> b
$ (CurrentFile -> AbsolutePath)
-> Maybe CurrentFile -> Maybe AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CurrentFile -> AbsolutePath
currentFilePath (Maybe CurrentFile -> Maybe AbsolutePath)
-> (CommandState -> Maybe CurrentFile)
-> CommandState
-> Maybe AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandState -> Maybe CurrentFile
theCurrentFile
  (TCEnv -> TCEnv) -> CommandM a -> CommandM a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envCurrentPath :: Maybe AbsolutePath
envCurrentPath = Maybe AbsolutePath
mfile }) CommandM a
m

atTopLevel :: CommandM a -> CommandM a
atTopLevel :: CommandM a -> CommandM a
atTopLevel CommandM a
cmd = (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT forall a. TCM a -> TCM a
B.atTopLevel CommandM a
cmd

---------------------------------------------------------------------------
-- Giving, refining.

data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite
  deriving (GiveRefine -> GiveRefine -> Bool
(GiveRefine -> GiveRefine -> Bool)
-> (GiveRefine -> GiveRefine -> Bool) -> Eq GiveRefine
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: 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)

-- | A "give"-like action (give, refine, etc).
--
--   @give_gen force ii rng s give_ref mk_newtxt@
--   acts on interaction point @ii@
--   occupying range @rng@,
--   placing the new content given by string @s@,
--   and replacing @ii@ by the newly created interaction points
--   in the state if safety checks pass (unless @force@ is applied).
give_gen
  :: UseForce       -- ^ Should safety checks be skipped?
  -> InteractionId
  -> Range
  -> String
  -> GiveRefine
  -> CommandM ()
give_gen :: UseForce
-> InteractionId
-> Range
-> VerboseKey
-> GiveRefine
-> StateT CommandState TCM ()
give_gen UseForce
force InteractionId
ii Range
rng VerboseKey
s0 GiveRefine
giveRefine = do
  let s :: VerboseKey
s = VerboseKey -> VerboseKey
trim VerboseKey
s0
  VerboseKey
-> VerboseLevel -> VerboseKey -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"interaction.give" VerboseLevel
20 (VerboseKey -> StateT CommandState TCM ())
-> VerboseKey -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"give_gen  " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ VerboseKey
s
  -- Andreas, 2015-02-26 if string is empty do nothing rather
  -- than giving a parse error.
  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
            GiveRefine
Give               -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.give
            GiveRefine
Refine             -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.refine
            GiveRefine
Intro              -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.refine
            ElaborateGive Rewrite
norm -> Rewrite
-> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.elaborate_give Rewrite
norm
    -- save scope of the interaction point (for printing the given expr. later)
    ScopeInfo
scope     <- InteractionId -> CommandM ScopeInfo
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
    -- parse string and "give", obtaining an abstract expression
    -- and newly created interaction points
    (Maybe CPUTime
time, (Expr
ae, Expr
ae0, [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
$ do
        -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential
        -- new interaction points introduced by the give.
        InteractionId -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii
        [InteractionId]
mis  <- StateT CommandState TCM [InteractionId]
forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
        VerboseKey
-> VerboseLevel -> VerboseKey -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"interaction.give" VerboseLevel
30 (VerboseKey -> StateT CommandState TCM ())
-> VerboseKey -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"interaction points before = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ [InteractionId] -> VerboseKey
forall a. Show a => a -> VerboseKey
show [InteractionId]
mis
        Expr
given <- TCM Expr -> CommandM Expr
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ InteractionId -> Range -> VerboseKey -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng VerboseKey
s
        Expr
ae    <- TCM Expr -> CommandM Expr
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give_ref UseForce
force InteractionId
ii Maybe Range
forall a. Maybe a
Nothing Expr
given
        [InteractionId]
mis' <- StateT CommandState TCM [InteractionId]
forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
        VerboseKey
-> VerboseLevel -> VerboseKey -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"interaction.give" VerboseLevel
30 (VerboseKey -> StateT CommandState TCM ())
-> VerboseKey -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"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])
-> CommandM (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)
    -- favonia: backup the old scope for highlighting
    InteractionId -> ScopeInfo -> StateT CommandState TCM ()
insertOldInteractionScope InteractionId
ii ScopeInfo
scope
    -- sort the new interaction points and put them into the state
    -- in replacement of the old interaction point
    [InteractionId]
iis' <- [InteractionId] -> StateT CommandState TCM [InteractionId]
forall (m :: * -> *).
(MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
[InteractionId] -> m [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'
    -- print abstract expr
    Expr
ce        <- ScopeInfo -> Expr -> StateT CommandState TCM (ConOfAbs Expr)
forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
ScopeInfo -> a -> m (ConOfAbs a)
abstractToConcreteScope ScopeInfo
scope Expr
ae
    VerboseKey
-> VerboseLevel -> [VerboseKey] -> StateT CommandState TCM ()
forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
VerboseKey -> VerboseLevel -> a -> m ()
reportS VerboseKey
"interaction.give" VerboseLevel
30
      [ VerboseKey
"ce = " VerboseKey -> VerboseKey -> VerboseKey
forall a. [a] -> [a] -> [a]
++ Expr -> VerboseKey
forall a. Show a => a -> VerboseKey
show Expr
ce
      , VerboseKey
"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)
      ]
    -- if the command was @Give@, use the literal user input;
    -- Andreas, 2014-01-15, see issue 1020:
    -- Refine could solve a goal by introducing the sole constructor
    -- without arguments.  Then there are no interaction metas, but
    -- we still cannot just `give' the user string (which may be empty).
    -- WRONG: also, if no interaction metas were created by @Refine@
    -- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange
    -- Ulf, 2015-03-30, if we're doing intro we can't do literal give since
    -- there is nothing in the hole (issue 1892).
    let literally :: Bool
literally = (GiveRefine
giveRefine GiveRefine -> GiveRefine -> Bool
forall a. Eq a => a -> a -> Bool
== GiveRefine
Give Bool -> Bool -> Bool
|| GiveRefine
giveRefine GiveRefine -> GiveRefine -> Bool
forall a. Eq a => a -> a -> Bool
== GiveRefine
Refine) Bool -> Bool -> Bool
&& Expr
ae Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
ae0 Bool -> Bool -> Bool
&& Range
rng Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
/= Range
forall a. Range' a
noRange
    -- Ulf, 2014-01-24: This works for give since we're highlighting the string
    -- that's already in the buffer. Doing it before the give action means that
    -- the highlighting is moved together with the text when the hole goes away.
    -- To make it work for refine we'd have to adjust the ranges.
    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
$ 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
$ 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
        RemoveTokenBasedHighlighting -> HighlightingInfo -> TCMT IO ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting (HighlightingInfo -> TCMT IO ())
-> TCMT IO HighlightingInfo -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          Range -> VerboseKey -> TCMT IO HighlightingInfo
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
    VerboseKey
-> VerboseLevel -> VerboseKey -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"interaction.give" VerboseLevel
30 (VerboseKey -> StateT CommandState TCM ())
-> VerboseKey -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"putResponse GiveAction passed"
    -- display new goal set (if not measuring time)
    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 -> StateT CommandState TCM ())
-> Interaction' Range -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Interaction' Range
forall range. Rewrite -> Interaction' range
Cmd_metas Rewrite
AsIs) (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
    VerboseKey
-> VerboseLevel -> VerboseKey -> StateT CommandState TCM ()
forall (m :: * -> *).
MonadDebug m =>
VerboseKey -> VerboseLevel -> VerboseKey -> m ()
reportSLn VerboseKey
"interaction.give" VerboseLevel
30 (VerboseKey -> StateT CommandState TCM ())
-> VerboseKey -> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ VerboseKey
"interpret Cmd_metas passed"
  where
    -- Substitutes xs for x in ys.
    replace :: b -> [b] -> t b -> [b]
replace b
x [b]
xs t b
ys = (b -> [b]) -> t b -> [b]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ b
y -> if b
y b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
x then [b]
xs else [b
y]) t b
ys
    -- For @Give@ we can replace the ii by the user given input.
    mkNewTxt :: Bool -> Expr -> GiveResult
mkNewTxt Bool
True  C.Paren{} = GiveResult
Give_Paren
    mkNewTxt Bool
True  Expr
_         = GiveResult
Give_NoParen
    -- Otherwise, we replace it by the reified value Agda computed.
    mkNewTxt Bool
False 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 Expr
e =
  (TCEnv -> TCEnv) -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
st -> TCEnv
st { envImportPath :: [TopLevelModuleName]
envImportPath         = []
                     , 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 -> ModuleNameHash -> NameId
NameId Hash
0 ModuleNameHash
noModuleNameHash) (VerboseKey
"dummy" :: String)
    info :: DefInfo' Expr
info  = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete Name
dummy) Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef (Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e)
    decl :: Declaration
decl  = KindOfName
-> DefInfo' Expr
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
OtherDefName DefInfo' Expr
info ArgInfo
defaultArgInfo Maybe [Occurrence]
forall a. Maybe a
Nothing (List1 Name -> QName
qnameFromList (List1 Name -> QName) -> List1 Name -> QName
forall a b. (a -> b) -> a -> b
$ Name -> List1 Name
forall el coll. Singleton el coll => el -> coll
singleton Name
dummy) Expr
e

-- | Sorts interaction points based on their ranges.

sortInteractionPoints
  :: (MonadInteractionPoints m, MonadError TCErr m, MonadFail m)
  => [InteractionId] -> m [InteractionId]
sortInteractionPoints :: [InteractionId] -> m [InteractionId]
sortInteractionPoints [InteractionId]
is =
  ((InteractionId, Range) -> InteractionId)
-> [(InteractionId, Range)] -> [InteractionId]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, Range) -> InteractionId
forall a b. (a, b) -> a
fst ([(InteractionId, Range)] -> [InteractionId])
-> ([(InteractionId, Range)] -> [(InteractionId, Range)])
-> [(InteractionId, Range)]
-> [InteractionId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, Range) -> (InteractionId, Range) -> Ordering)
-> [(InteractionId, Range)] -> [(InteractionId, Range)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Range -> Range -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Range -> Ordering)
-> ((InteractionId, Range) -> Range)
-> (InteractionId, Range)
-> (InteractionId, Range)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (InteractionId, Range) -> Range
forall a b. (a, b) -> b
snd) ([(InteractionId, Range)] -> [InteractionId])
-> m [(InteractionId, Range)] -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [InteractionId]
-> (InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [InteractionId]
is ((InteractionId -> m (InteractionId, Range))
 -> m [(InteractionId, Range)])
-> (InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)]
forall a b. (a -> b) -> a -> b
$ \ InteractionId
i -> do
      (InteractionId
i,) (Range -> (InteractionId, Range))
-> m Range -> m (InteractionId, Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i

-- | Displays the current goal, the given document, and the current
--   context.
--
--   Should not modify the state.

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 GoalTypeAux
aux Rewrite
norm InteractionId
ii Range
_ VerboseKey
_ = 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]
B.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)

-- | Shows all the top-level names in the given module, along with
-- their types.

showModuleContents :: Rewrite -> Range -> String -> CommandM ()
showModuleContents :: Rewrite -> Range -> VerboseKey -> StateT CommandState TCM ()
showModuleContents Rewrite
norm Range
rng VerboseKey
s = do
  ([Name]
modules, Telescope
tel, [(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

-- | Shows all the top-level names in scope which mention all the given
-- identifiers in their type.

searchAbout :: Rewrite -> Range -> String -> CommandM ()
searchAbout :: Rewrite -> Range -> VerboseKey -> StateT CommandState TCM ()
searchAbout Rewrite
norm Range
rg VerboseKey
names = do
  VerboseKey
-> (VerboseKey -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (VerboseKey -> VerboseKey
trim VerboseKey
names) ((VerboseKey -> StateT CommandState TCM ())
 -> StateT CommandState TCM ())
-> (VerboseKey -> StateT CommandState TCM ())
-> StateT CommandState TCM ()
forall a b. (a -> b) -> a -> b
$ \ VerboseKey
trimmedNames -> 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
$ 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

-- | Explain why something is in scope.

whyInScope :: String -> CommandM ()
whyInScope :: VerboseKey -> StateT CommandState TCM ()
whyInScope VerboseKey
s = do
  Just (CurrentFile AbsolutePath
file [VerboseKey]
_ UTCTime
_) <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
  let cwd :: VerboseKey
cwd = VerboseKey -> VerboseKey
takeDirectory (AbsolutePath -> VerboseKey
filePath AbsolutePath
file)
  (Maybe LocalVar
v, [AbstractName]
xs, [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

-- | Sets the command line options and updates the status information.

setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts :: CommandLineOptions -> StateT CommandState TCM ()
setCommandLineOpts 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 ()
TCM.setCommandLineOptions CommandLineOptions
opts
    StateT CommandState TCM ()
displayStatus


-- | Computes some status information.
--
--   Does not change the state.

status :: CommandM Status
status :: CommandM Status
status = do
  Maybe CurrentFile
cf       <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
  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
showIrr  <- 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
showIrrelevantArguments

  -- Check if the file was successfully type checked, and has not
  -- changed since. Note: This code does not check if any dependencies
  -- have changed, and uses a time stamp to check for changes.
  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 CurrentFile
cf of
    Maybe CurrentFile
Nothing     -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just (CurrentFile AbsolutePath
f [VerboseKey]
_ UTCTime
t) -> do
      UTCTime
t' <- IO UTCTime -> TCM UTCTime
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO UTCTime -> TCM UTCTime) -> IO UTCTime -> TCM UTCTime
forall a b. (a -> b) -> a -> b
$ VerboseKey -> IO UTCTime
getModificationTime (VerboseKey -> IO UTCTime) -> VerboseKey -> IO UTCTime
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> VerboseKey
filePath AbsolutePath
f
      if UTCTime
t UTCTime -> UTCTime -> Bool
forall a. Eq a => a -> a -> Bool
== UTCTime
t'
        then
          do
            Maybe TopLevelModuleName
mm <- AbsolutePath -> TCM (Maybe TopLevelModuleName)
forall (m :: * -> *).
ReadTCState m =>
AbsolutePath -> m (Maybe TopLevelModuleName)
lookupModuleFromSource AbsolutePath
f
            case Maybe TopLevelModuleName
mm of
              Maybe TopLevelModuleName
Nothing -> Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False -- work-around for Issue1007
              Just TopLevelModuleName
m  -> Bool -> (ModuleInfo -> Bool) -> Maybe ModuleInfo -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ([TCWarning] -> Bool
forall a. Null a => a -> Bool
null ([TCWarning] -> Bool)
-> (ModuleInfo -> [TCWarning]) -> ModuleInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> [TCWarning]
miWarnings) (Maybe ModuleInfo -> Bool)
-> TCMT IO (Maybe ModuleInfo) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TopLevelModuleName -> TCMT IO (Maybe ModuleInfo)
forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule TopLevelModuleName
m
        else
            Bool -> TCMT IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  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 -> Bool -> Status
Status { sShowImplicitArguments :: Bool
sShowImplicitArguments   = Bool
showImpl,
                    sShowIrrelevantArguments :: Bool
sShowIrrelevantArguments = Bool
showIrr,
                    sChecked :: Bool
sChecked                 = Bool
checked }

-- | Displays or updates status information.
--
--   Does not change the state.

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@ does what @'display_info'' False@ does, but
--   additionally displays some status information (see 'status' and
--   'displayStatus').

display_info :: DisplayInfo -> CommandM ()
display_info :: DisplayInfo -> StateT CommandState TCM ()
display_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

-- | Parses and scope checks an expression (using the \"inside scope\"
-- as the scope), performs the given command with the expression as
-- input, and returns the result and the time it takes.

parseAndDoAtToplevel
  :: (A.Expr -> TCM a)
     -- ^ The command to perform.
  -> String
     -- ^ The expression to parse.
  -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel :: (Expr -> TCM a) -> VerboseKey -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM a
cmd 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
$ CommandM a -> CommandM a
forall a. CommandM a -> CommandM a
atTopLevel (CommandM a -> CommandM a) -> CommandM a -> CommandM 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
$
      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 -> ScopeM (AbsOfCon Expr)
forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract_ Expr
e

maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed 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 VerboseKey
"profile.interactive" VerboseLevel
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
      (a
r, 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)

-- | Tell to highlight the code using the given highlighting
-- info (unless it is @Nothing@).

tellToUpdateHighlighting
  :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource) -> IO [Response]
tellToUpdateHighlighting :: Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> IO [Response]
tellToUpdateHighlighting Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
Nothing                = [Response] -> IO [Response]
forall (m :: * -> *) a. Monad m => a -> m a
return []
tellToUpdateHighlighting (Just (HighlightingInfo
info, HighlightingMethod
method, ModuleToSource
modFile)) =
  [Response] -> IO [Response]
forall (m :: * -> *) a. Monad m => a -> m a
return [HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
KeepHighlighting HighlightingMethod
method ModuleToSource
modFile]

-- | Tells the Emacs mode to go to the first error position (if any).

tellEmacsToJumpToError :: Range -> [Response]
tellEmacsToJumpToError :: Range -> [Response]
tellEmacsToJumpToError Range
r =
  case Range -> Maybe (Position' SrcFile)
forall a. Range' a -> Maybe (Position' a)
rStart Range
r of
    Maybe (Position' SrcFile)
Nothing                                           -> []
    Just (Pn { srcFile :: forall a. Position' a -> a
srcFile = SrcFile
Strict.Nothing })            -> []
    Just (Pn { srcFile :: forall a. Position' a -> a
srcFile = Strict.Just AbsolutePath
f, posPos :: forall a. Position' a -> Int32
posPos = Int32
p }) ->
       [ VerboseKey -> Int32 -> Response
Resp_JumpToError (AbsolutePath -> VerboseKey
filePath AbsolutePath
f) Int32
p ]