{-# 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.Except         ( MonadError(..), ExceptT(..), runExceptT )
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.State          ( MonadState(..), gets, modify, runStateT )
import Control.Monad.STM
import Control.Monad.State          ( StateT )

import qualified Data.Char as Char
import Data.Function (on)
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe

import System.Directory
import System.FilePath

import Agda.TypeChecking.Monad as TCM
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Errors
import Agda.TypeChecking.Opacity (saturateOpaqueBlocks)
import Agda.TypeChecking.Rules.Term (checkExpr, isType_)
import Agda.TypeChecking.Warnings (warning)

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

import Agda.Interaction.Base
import Agda.Interaction.ExitCode (pattern TCMError, exitAgdaWith)
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.Command
  (CommandM, liftLocalState, revLift, revLiftTC, localStateCommandM)
import Agda.Interaction.Highlighting.Generate

import Agda.Compiler.Backend

import Agda.Mimer.Mimer as Mimer
import qualified Control.DeepSeq as DeepSeq

import Agda.Utils.Either
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Hash
import Agda.Utils.IO (showIOException)
import Agda.Utils.Lens
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty hiding (Mode)
import qualified Agda.Utils.ProfileOptions as Profile
import Agda.Utils.Singleton
import Agda.Utils.String
import Agda.Utils.Time
import Agda.Utils.Tuple
import Agda.Utils.WithDefault (lensCollapseDefault, lensKeepDefault)

import Agda.Utils.Impossible

-- | 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 a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO forall x. (CommandM a -> IO x) -> IO x
ci_i = (forall c.
 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState))
-> (forall 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 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall c.
StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT TCM b -> StateT CommandState TCM b
forall b. TCM b -> StateT CommandState TCM b
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
-> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
forall a b. (a -> b) -> a -> b
$ \CommandM a -> TCM x
ct -> (forall c. TCM c -> TCState -> IO (c, TCState))
-> (forall b. IO b -> TCM b)
-> (forall x. (TCM x -> IO x) -> IO x)
-> TCM x
forall (m :: * -> *) (k :: * -> *) a.
MonadTCState m =>
(forall c. m c -> TCState -> k (c, TCState))
-> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
revLiftTC TCM c -> TCState -> IO (c, TCState)
forall c. TCM c -> TCState -> IO (c, TCState)
runSafeTCM IO b -> TCM b
forall b. IO b -> TCM b
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ((forall x. (TCM x -> IO x) -> IO x) -> TCM x)
-> (forall x. (TCM x -> IO x) -> IO x) -> TCM x
forall a b. (a -> b) -> a -> b
$ (CommandM a -> IO x) -> IO x
forall x. (CommandM a -> IO x) -> IO x
ci_i ((CommandM a -> IO x) -> IO x)
-> ((TCM x -> IO x) -> CommandM a -> IO x)
-> (TCM x -> IO x)
-> IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TCM x -> IO x) -> (CommandM a -> TCM x) -> CommandM a -> IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandM a -> TCM x
ct)

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

liftCommandMT :: (forall x . TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT :: forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT forall x. TCM x -> TCM x
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 StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall c.
StateT CommandState TCM c -> CommandState -> TCM (c, CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT TCMT IO b -> StateT CommandState TCM b
forall b. TCM b -> StateT CommandState TCM b
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ((forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a)
-> (forall x. (CommandM a -> TCM x) -> TCM x) -> CommandM a
forall a b. (a -> b) -> a -> b
$ TCM x -> TCM x
forall x. TCM x -> TCM x
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. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMTLocalState forall x. TCM x -> TCM x
f = (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT TCM x -> TCM x
forall x. TCM x -> TCM x
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 -> CommandM ()
putResponse = TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ())
-> (Response -> TCM ()) -> Response -> CommandM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Response -> TCM ()
appInteractionOutputCallback


-- | A Lens for 'theInteractionPoints'.

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


-- * Operations for manipulating 'oldInteractionScopes'.

-- | A Lens for 'oldInteractionScopes'.
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes :: (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes OldInteractionScopes -> OldInteractionScopes
f = (CommandState -> CommandState) -> CommandM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> CommandM ())
-> (CommandState -> CommandState) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s ->
  CommandState
s { oldInteractionScopes = f $ oldInteractionScopes s }

insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope :: InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope InteractionId
ii ScopeInfo
scope = do
  TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.scope" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"inserting old interaction scope " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
  (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes) -> CommandM ())
-> (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
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 -> CommandM ()
removeOldInteractionScope InteractionId
ii = do
  TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.scope" Int
20 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"removing old interaction scope " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
  (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
modifyOldInteractionScopes ((OldInteractionScopes -> OldInteractionScopes) -> CommandM ())
-> (OldInteractionScopes -> OldInteractionScopes) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> OldInteractionScopes -> OldInteractionScopes
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete InteractionId
ii

getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope InteractionId
ii = do
  ms <- (CommandState -> Maybe ScopeInfo)
-> StateT CommandState TCM (Maybe ScopeInfo)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((CommandState -> Maybe ScopeInfo)
 -> StateT CommandState TCM (Maybe ScopeInfo))
-> (CommandState -> Maybe ScopeInfo)
-> StateT CommandState TCM (Maybe ScopeInfo)
forall a b. (a -> b) -> a -> b
$ InteractionId -> OldInteractionScopes -> Maybe ScopeInfo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InteractionId
ii (OldInteractionScopes -> Maybe ScopeInfo)
-> (CommandState -> OldInteractionScopes)
-> CommandState
-> Maybe ScopeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandState -> OldInteractionScopes
oldInteractionScopes
  case ms of
    Maybe ScopeInfo
Nothing    -> String -> CommandM ScopeInfo
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (String -> CommandM ScopeInfo) -> String -> CommandM ScopeInfo
forall a b. (a -> b) -> a -> b
$ String
"not an old interaction point: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
    Just ScopeInfo
scope -> ScopeInfo -> CommandM ScopeInfo
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ScopeInfo
scope

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

handleCommand_ :: CommandM () -> CommandM ()
handleCommand_ :: CommandM () -> CommandM ()
handleCommand_ = (forall a. CommandM a -> CommandM a)
-> CommandM () -> CommandM () -> CommandM ()
handleCommand CommandM a -> CommandM a
forall a. a -> a
forall a. CommandM a -> CommandM a
id (() -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ())

handleCommand :: (forall a. CommandM a -> CommandM a) -> CommandM () -> CommandM () -> CommandM ()
handleCommand :: (forall a. CommandM a -> CommandM a)
-> CommandM () -> CommandM () -> CommandM ()
handleCommand forall a. CommandM a -> CommandM a
wrap CommandM ()
onFail CommandM ()
cmd = CommandM () -> CommandM ()
handleNastyErrors (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ CommandM () -> CommandM ()
forall a. CommandM a -> CommandM a
wrap (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ do
    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.
    cmd `catchErr` \ TCErr
e -> do
      CommandM ()
onFail
      Maybe HighlightingMethod -> TCErr -> CommandM ()
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
      TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ do
        newPersistentState <- Lens' TCState PersistentTCState -> TCMT IO PersistentTCState
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (PersistentTCState -> f PersistentTCState) -> TCState -> f TCState
Lens' TCState PersistentTCState
lensPersistentState
        putTC oldState
        lensPersistentState `setTCLens` newPersistentState

  where
    -- Preserves state so we can do unsolved meta highlighting
    catchErr :: CommandM a -> (TCErr -> CommandM a) -> CommandM a
    catchErr :: forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
catchErr CommandM a
m TCErr -> CommandM a
h = do
      s       <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
      (x, s') <- lift $ do runStateT m s
         `catchError_` \ TCErr
e ->
           CommandM a -> CommandState -> TCM (a, CommandState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (TCErr -> CommandM a
h TCErr
e) CommandState
s
      put s'
      return x

    -- Handle every possible kind of error (#637), except for
    -- AsyncCancelled, which is used to abort Agda.
    handleNastyErrors :: CommandM () -> CommandM ()
    handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors CommandM ()
m = (forall x. (CommandM () -> IO x) -> IO x) -> CommandM ()
forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO ((forall x. (CommandM () -> IO x) -> IO x) -> CommandM ())
-> (forall x. (CommandM () -> IO x) -> IO x) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \ CommandM () -> IO x
toIO -> do

      let asyncHandler :: AsyncCancelled -> m (Either AsyncCancelled b)
asyncHandler e :: AsyncCancelled
e@AsyncCancelled
AsyncCancelled = Either AsyncCancelled b -> m (Either AsyncCancelled b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (AsyncCancelled -> Either AsyncCancelled b
forall a b. a -> Either a b
Left AsyncCancelled
e)

          ioHandler :: IOException -> IO (Either AsyncCancelled x)
ioHandler (IOException
e :: E.IOException) = x -> Either AsyncCancelled x
forall a b. b -> Either a b
Right (x -> Either AsyncCancelled x)
-> IO x -> IO (Either AsyncCancelled x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            CommandM () -> IO x
toIO (CommandM () -> IO x) -> CommandM () -> IO x
forall a b. (a -> b) -> a -> b
$ Maybe HighlightingMethod -> TCErr -> CommandM ()
handleErr (HighlightingMethod -> Maybe HighlightingMethod
forall a. a -> Maybe a
Just HighlightingMethod
Direct) (TCErr -> CommandM ()) -> TCErr -> CommandM ()
forall a b. (a -> b) -> a -> b
$ Maybe TCState -> Range -> IOException -> TCErr
IOException Maybe TCState
forall a. Maybe a
Nothing Range
forall a. Range' a
noRange IOException
e

          generalHandler :: SomeException -> IO (Either AsyncCancelled x)
generalHandler (SomeException
e :: E.SomeException) = x -> Either AsyncCancelled x
forall a b. b -> Either a b
Right (x -> Either AsyncCancelled x)
-> IO x -> IO (Either AsyncCancelled x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
            CommandM () -> IO x
toIO (CommandM () -> IO x) -> CommandM () -> IO x
forall a b. (a -> b) -> a -> b
$ Maybe HighlightingMethod -> TCErr -> CommandM ()
handleErr (HighlightingMethod -> Maybe HighlightingMethod
forall a. a -> Maybe a
Just HighlightingMethod
Direct) (TCErr -> CommandM ()) -> TCErr -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String -> TCErr
GenericException (String -> TCErr) -> String -> TCErr
forall a b. (a -> b) -> a -> b
$ SomeException -> String
forall e. Exception e => e -> String
showIOException SomeException
e

      r <- (x -> Either AsyncCancelled x
forall a b. b -> Either a b
Right (x -> Either AsyncCancelled x)
-> IO x -> IO (Either AsyncCancelled x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CommandM () -> IO x
toIO CommandM ()
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)
-> (IOException -> IO (Either AsyncCancelled x))
-> IO (Either AsyncCancelled x)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` IOException -> IO (Either AsyncCancelled x)
ioHandler
             IO (Either AsyncCancelled x)
-> (SomeException -> IO (Either AsyncCancelled x))
-> IO (Either AsyncCancelled x)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` SomeException -> IO (Either AsyncCancelled x)
generalHandler
      case r of
        Right x
x -> x -> IO x
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return x
x
        Left AsyncCancelled
e  -> AsyncCancelled -> IO x
forall e a. (HasCallStack, Exception e) => e -> IO a
E.throwIO AsyncCancelled
e

    -- 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 -> CommandM ()
handleErr Maybe HighlightingMethod
method TCErr
e = do

      -- TODO: make a better predicate for this
      noError <- TCMT IO Bool -> StateT CommandState TCM Bool
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Bool -> StateT CommandState TCM Bool)
-> TCMT IO Bool -> StateT CommandState TCM Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall a. Null a => a -> Bool
null (String -> Bool) -> TCMT IO String -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCErr -> TCMT IO String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
renderError TCErr
e
      unless noError do

        unsolved <- lift $ computeUnsolvedInfo
        err     <- lift $ errorHighlighting e
        modFile <- lift $ useTC stModuleToSource
        method  <- case method of
          Maybe HighlightingMethod
Nothing -> TCMT IO HighlightingMethod
-> StateT CommandState TCM HighlightingMethod
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO HighlightingMethod
 -> StateT CommandState TCM HighlightingMethod)
-> TCMT IO HighlightingMethod
-> StateT CommandState TCM HighlightingMethod
forall a b. (a -> b) -> a -> b
$ Lens' TCEnv HighlightingMethod -> TCMT IO HighlightingMethod
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (HighlightingMethod -> f HighlightingMethod) -> TCEnv -> f TCEnv
Lens' TCEnv HighlightingMethod
eHighlightingMethod
          Just HighlightingMethod
m  -> HighlightingMethod -> StateT CommandState TCM HighlightingMethod
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingMethod
m
        let info = HighlightingInfoBuilder -> HighlightingInfo
forall a b. Convert a b => a -> b
convert (HighlightingInfoBuilder -> HighlightingInfo)
-> HighlightingInfoBuilder -> HighlightingInfo
forall a b. (a -> b) -> a -> b
$ HighlightingInfoBuilder
err HighlightingInfoBuilder
-> HighlightingInfoBuilder -> HighlightingInfoBuilder
forall a. Semigroup a => a -> a -> a
<> HighlightingInfoBuilder
unsolved
                     -- Errors take precedence over unsolved things.

        showImpl <- lift $ optShowImplicit <$> useTC stPragmaOptions
        showIrr <- lift $ optShowIrrelevant <$> useTC stPragmaOptions
        do
          mapM_ putResponse $
            [ Resp_DisplayInfo $ Info_Error $ Info_GenericError e ] ++
            tellEmacsToJumpToError (getRange e) ++
            [ Resp_HighlightingInfo info KeepHighlighting
                                    method modFile ] ++
            [ Resp_Status $ Status { sChecked = False
                                   , sShowImplicitArguments = showImpl
                                   , sShowIrrelevantArguments = showIrr
                                   } ]
          whenM (optExitOnError <$> commandLineOptions) $
            liftIO $ exitAgdaWith TCMError

-- | 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 -> CommandM ()
runInteraction IOTCM
iotcm =
  (forall a. CommandM a -> CommandM a)
-> CommandM () -> CommandM () -> CommandM ()
handleCommand CommandM a -> CommandM a
forall a. CommandM a -> CommandM a
inEmacs CommandM ()
onFail (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ do
    currentAbs <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
-> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute String
current
    cf  <- gets theCurrentFile
    cmd <- if independent cmd then return cmd else do
      when (Just currentAbs /= (currentFilePath <$> cf)) $ do
        let mode = Mode
TypeCheck
        cmd_load' current [] True mode $ \CheckResult
_ -> () -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      cf <- fromMaybe __IMPOSSIBLE__ <$> gets theCurrentFile
      return $ case iotcm (Just (currentFileModule cf)) of
        IOTCM String
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
cmd -> Interaction' Range
cmd

    withCurrentFile $ interpret cmd

    cf' <- gets theCurrentFile
    when (updateInteractionPointsAfter cmd
            &&
          Just currentAbs == (currentFilePath <$> cf')) $ do
        putResponse . Resp_InteractionPoints =<< gets theInteractionPoints

  where
    -- The ranges in cmd might be incorrect because of the use of
    -- Nothing here. That is taken care of above.
    IOTCM String
current HighlightingLevel
highlighting HighlightingMethod
highlightingMethod Interaction' Range
cmd = IOTCM
iotcm Maybe TopLevelModuleName
forall a. Maybe a
Nothing

    inEmacs :: forall a. CommandM a -> CommandM a
    inEmacs :: forall a. CommandM a -> CommandM a
inEmacs = (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT ((forall x. TCM x -> TCM x) -> CommandM a -> CommandM a)
-> (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
forall a b. (a -> b) -> a -> b
$ TCEnv -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a. MonadTCEnv m => TCEnv -> m a -> m a
withEnv (TCEnv -> TCMT IO x -> TCMT IO x)
-> TCEnv -> TCMT IO x -> TCMT IO x
forall a b. (a -> b) -> a -> b
$ TCEnv
initEnv
            { envHighlightingLevel  = highlighting
            , envHighlightingMethod = highlightingMethod
            }

    -- If an independent command fails we should reset theCurrentFile (Issue853).
    onFail :: CommandM ()
onFail | Interaction' Range -> Bool
independent Interaction' Range
cmd = (CommandState -> CommandState) -> CommandM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((CommandState -> CommandState) -> CommandM ())
-> (CommandState -> CommandState) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \ CommandState
s -> CommandState
s { theCurrentFile = Nothing }
           | Bool
otherwise       = () -> CommandM ()
forall a. a -> StateT CommandState TCM a
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 :: forall a. (IOTCM -> CommandM a) -> CommandM (Command' (Maybe a))
maybeAbort IOTCM -> CommandM a
m = do
  commandState <- StateT CommandState TCM CommandState
forall s (m :: * -> *). MonadState s m => m s
get
  let q = CommandState -> CommandQueue
commandQueue CommandState
commandState
  (n, cmd) <- liftIO $ atomically $ readTChan (commands q)
  case cmd of
    Command
Done      -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Command' (Maybe a)
forall a. Command' a
Done
    Error String
e   -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Command' (Maybe a)
forall a. String -> Command' a
Error String
e)
    Command IOTCM
c -> do
      tcState <- StateT CommandState TCM TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      tcEnv   <- askTC
      result  <- liftIO $ race
                   (runTCM tcEnv tcState $
                    runStateT (m c) commandState)
                   (waitForAbort n q)
      case result of
        Left ((a
x, CommandState
commandState'), TCState
tcState') -> do
          TCState -> CommandM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcState'
          CommandState -> CommandM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put CommandState
commandState'
          case IOTCM
c Maybe TopLevelModuleName
forall a. Maybe a
Nothing of
            IOTCM String
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
Cmd_exit -> do
              Response -> CommandM ()
putResponse Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DoneExiting
              Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return Command' (Maybe a)
forall a. Command' a
Done
            IOTCM' Range
_ -> Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Command' (Maybe a)
forall a. a -> Command' a
Command (a -> Maybe a
forall a. a -> Maybe a
Just a
x))
        Right Integer
a -> do
          IO () -> CommandM ()
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CommandM ()) -> IO () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ CommandQueue -> Integer -> IO ()
popAbortedCommands CommandQueue
q Integer
a
          TCState -> CommandM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC (TCState -> CommandM ()) -> TCState -> CommandM ()
forall a b. (a -> b) -> a -> b
$ Lens' TCState PragmaOptions -> LensSet TCState PragmaOptions
forall o i. Lens' o i -> LensSet o i
set (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
forall a. LensPragmaOptions a => Lens' a PragmaOptions
Lens' TCState PragmaOptions
lensPragmaOptions (TCState
tcState TCState -> Lens' TCState PragmaOptions -> PragmaOptions
forall o i. o -> Lens' o i -> i
^. (PragmaOptions -> f PragmaOptions) -> TCState -> f TCState
forall a. LensPragmaOptions a => Lens' a PragmaOptions
Lens' TCState PragmaOptions
lensPragmaOptions) (TCState -> TCState) -> TCState -> TCState
forall a b. (a -> b) -> a -> b
$
            PersistentTCState -> TCState
initStateFromPersistentState (PersistentTCState -> TCState) -> PersistentTCState -> TCState
forall a b. (a -> b) -> a -> b
$ TCState -> PersistentTCState
stPersistentState TCState
tcState
          CommandState -> CommandM ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (CommandState -> CommandM ()) -> CommandState -> CommandM ()
forall a b. (a -> b) -> a -> b
$ (CommandQueue -> CommandState
initCommandState (CommandState -> CommandQueue
commandQueue CommandState
commandState))
            { optionsOnReload = optionsOnReload commandState
            }
          Response -> CommandM ()
putResponse Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DoneAborting
          CommandM ()
displayStatus
          Command' (Maybe a) -> StateT CommandState TCM (Command' (Maybe a))
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> Command' (Maybe a)
forall a. a -> Command' a
Command Maybe a
forall a. Maybe a
Nothing)
  where

  -- 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
      a <- TVar (Maybe Integer) -> STM (Maybe Integer)
forall a. TVar a -> STM a
readTVar (CommandQueue -> TVar (Maybe Integer)
abort CommandQueue
q)
      case a of
        Just Integer
a' | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
a' -> Integer -> STM Integer
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
a'
        Maybe Integer
_                 -> STM Integer
forall a. STM a
retry

  -- 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
    done <- STM Bool -> IO Bool
forall a. STM a -> IO a
atomically (STM Bool -> IO Bool) -> STM Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
      cmd <- TChan (Integer, Command) -> STM (Maybe (Integer, Command))
forall a. TChan a -> STM (Maybe a)
tryReadTChan (CommandQueue -> TChan (Integer, Command)
commands CommandQueue
q)
      case cmd of
        Maybe (Integer, Command)
Nothing -> Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
        Just (Integer, Command)
c  ->
          if (Integer, Command) -> Integer
forall a b. (a, b) -> a
fst (Integer, Command)
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
n then
            Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
           else do
            TChan (Integer, Command) -> (Integer, Command) -> STM ()
forall a. TChan a -> a -> STM ()
unGetTChan (CommandQueue -> TChan (Integer, Command)
commands CommandQueue
q) (Integer, Command)
c
            Bool -> STM Bool
forall a. a -> STM a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    unless done $
      popAbortedCommands q n

-- | 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
  commands <- IO (TChan (Integer, Command))
forall a. IO (TChan a)
newTChanIO
  abort    <- newTVarIO Nothing

  let -- Read commands. The argument is the number of the previous
      -- command (other than abort commands) that was read, if any.
      readCommands Integer
n = do
        c <- IO Command
next
        case c of
          Command IOTCM
c | IOTCM String
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
Cmd_abort <- IOTCM
c Maybe TopLevelModuleName
forall a. Maybe a
Nothing -> do
            STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TVar (Maybe Integer) -> Maybe Integer -> STM ()
forall a. TVar a -> a -> STM ()
writeTVar TVar (Maybe Integer)
abort (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n)
            Integer -> IO ()
readCommands Integer
n
          Command
_ -> do
            let n' :: Integer
n' = (Integer -> Integer
forall a. Enum a => a -> a
succ Integer
n)
            STM () -> IO ()
forall a. STM a -> IO a
atomically (STM () -> IO ()) -> STM () -> IO ()
forall a b. (a -> b) -> a -> b
$ TChan (Integer, Command) -> (Integer, Command) -> STM ()
forall a. TChan a -> a -> STM ()
writeTChan TChan (Integer, Command)
commands (Integer
n', Command
c)
            case Command
c of
              Command
Done -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Command
_    -> Integer -> IO ()
readCommands Integer
n'

  _ <- forkIO (readCommands 0)

  return (CommandQueue { .. })

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

-- | 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_load_no_metas{}             = 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_backend_top{}                   = Bool
True
updateInteractionPointsAfter Cmd_backend_hole{}                  = Bool
True
updateInteractionPointsAfter Cmd_constraints{}                   = Bool
False
updateInteractionPointsAfter Cmd_metas{}                         = Bool
False
updateInteractionPointsAfter Cmd_load_no_metas{}                 = Bool
False
updateInteractionPointsAfter Cmd_show_module_contents_toplevel{} = Bool
False
updateInteractionPointsAfter Cmd_search_about_toplevel{}         = Bool
False
updateInteractionPointsAfter Cmd_solveAll{}                      = Bool
True
updateInteractionPointsAfter Cmd_solveOne{}                      = Bool
True
updateInteractionPointsAfter Cmd_infer_toplevel{}                = Bool
False
updateInteractionPointsAfter Cmd_compute_toplevel{}              = Bool
False
updateInteractionPointsAfter Cmd_load_highlighting_info{}        = Bool
False
updateInteractionPointsAfter Cmd_tokenHighlighting{}             = Bool
False
updateInteractionPointsAfter Cmd_highlight{}                     = Bool
True
updateInteractionPointsAfter ShowImplicitArgs{}                  = Bool
False
updateInteractionPointsAfter ToggleImplicitArgs{}                = Bool
False
updateInteractionPointsAfter ShowIrrelevantArgs{}                = Bool
False
updateInteractionPointsAfter ToggleIrrelevantArgs{}              = Bool
False
updateInteractionPointsAfter Cmd_give{}                          = Bool
True
updateInteractionPointsAfter Cmd_refine{}                        = Bool
True
updateInteractionPointsAfter Cmd_intro{}                         = Bool
True
updateInteractionPointsAfter Cmd_refine_or_intro{}               = Bool
True
updateInteractionPointsAfter Cmd_autoOne{}                       = Bool
True
updateInteractionPointsAfter Cmd_autoAll{}                       = Bool
True
updateInteractionPointsAfter Cmd_context{}                       = Bool
False
updateInteractionPointsAfter Cmd_helper_function{}               = Bool
False
updateInteractionPointsAfter Cmd_infer{}                         = Bool
False
updateInteractionPointsAfter Cmd_goal_type{}                     = Bool
False
updateInteractionPointsAfter Cmd_elaborate_give{}                = Bool
True
updateInteractionPointsAfter Cmd_goal_type_context{}             = Bool
False
updateInteractionPointsAfter Cmd_goal_type_context_infer{}       = Bool
False
updateInteractionPointsAfter Cmd_goal_type_context_check{}       = Bool
False
updateInteractionPointsAfter Cmd_show_module_contents{}          = Bool
False
updateInteractionPointsAfter Cmd_make_case{}                     = Bool
True
updateInteractionPointsAfter Cmd_compute{}                       = Bool
False
updateInteractionPointsAfter Cmd_why_in_scope{}                  = Bool
False
updateInteractionPointsAfter Cmd_why_in_scope_toplevel{}         = Bool
False
updateInteractionPointsAfter Cmd_show_version{}                  = Bool
False
updateInteractionPointsAfter Cmd_abort{}                         = Bool
False
updateInteractionPointsAfter Cmd_exit{}                          = Bool
False

-- | Interpret an interaction

getBackendName :: CompilerBackend -> BackendName
getBackendName :: CompilerBackend -> BackendName
getBackendName = \case
  CompilerBackend
LaTeX -> BackendName
"LaTeX"
  CompilerBackend
QuickLaTeX -> BackendName
"LaTeX"
  OtherBackend BackendName
"GHCNoMain" -> BackendName
"GHC"
  OtherBackend BackendName
b -> BackendName
b

interpret :: Interaction -> CommandM ()

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

interpret (Cmd_compile CompilerBackend
backend String
file [String]
argv) =
  String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM ())
-> CommandM ()
forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
file [String]
argv Bool
allowUnsolved Mode
mode ((CheckResult -> CommandM ()) -> CommandM ())
-> (CheckResult -> CommandM ()) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \ CheckResult
checkResult -> do
    ws <- TCM (Set TCWarning) -> StateT CommandState TCM (Set TCWarning)
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Set TCWarning) -> StateT CommandState TCM (Set TCWarning))
-> TCM (Set TCWarning) -> StateT CommandState TCM (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> TCM (Set TCWarning)
forall (m :: * -> *).
HasOptions m =>
Set TCWarning -> m (Set TCWarning)
applyFlagsToTCWarnings (Set TCWarning -> TCM (Set TCWarning))
-> Set TCWarning -> TCM (Set TCWarning)
forall a b. (a -> b) -> a -> b
$ CheckResult -> Set TCWarning
crWarnings CheckResult
checkResult
    case null ws of
      Bool
True -> do
        TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ BackendName -> IsMain -> CheckResult -> TCM ()
callBackend (CompilerBackend -> BackendName
getBackendName CompilerBackend
backend) IsMain
isMain CheckResult
checkResult
        DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> (WarningsAndNonFatalErrors
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> WarningsAndNonFatalErrors
-> CommandM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompilerBackend
-> WarningsAndNonFatalErrors
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
CompilerBackend
-> warningsAndNonFatalErrors
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_CompilationOk CompilerBackend
backend (WarningsAndNonFatalErrors -> CommandM ())
-> StateT CommandState TCM WarningsAndNonFatalErrors -> CommandM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM WarningsAndNonFatalErrors
-> StateT CommandState TCM WarningsAndNonFatalErrors
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM WarningsAndNonFatalErrors
B.getWarningsAndNonFatalErrors
      Bool
False -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
Info_Error_boot tcErr tcWarning
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Error (Info_Error
 -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ Set TCWarning -> Info_Error
forall tcErr tcWarning.
Set tcWarning -> Info_Error_boot tcErr tcWarning
Info_CompilationError Set TCWarning
ws
  where
  allowUnsolved :: Bool
allowUnsolved = CompilerBackend
backend CompilerBackend -> [CompilerBackend] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [CompilerBackend
LaTeX, CompilerBackend
QuickLaTeX]
  mode :: Mode
mode | CompilerBackend
QuickLaTeX <- CompilerBackend
backend = Mode
ScopeCheck
       | Bool
otherwise             = Mode
TypeCheck
  isMain :: IsMain
isMain | OtherBackend BackendName
"GHCNoMain" <- CompilerBackend
backend = IsMain
NotMain
         | Bool
otherwise                           = IsMain
IsMain

interpret (Cmd_backend_top CompilerBackend
backend String
cmd) =
  BackendName -> String -> CommandM ()
callBackendInteractTop (CompilerBackend -> BackendName
getBackendName CompilerBackend
backend) String
cmd

interpret (Cmd_backend_hole InteractionId
ii Range
rng String
s CompilerBackend
backend String
cmd) =
  BackendName
-> String -> InteractionId -> Range -> String -> CommandM ()
callBackendInteractHole (CompilerBackend -> BackendName
getBackendName CompilerBackend
backend) String
cmd InteractionId
ii Range
rng String
s

interpret Interaction' Range
Cmd_constraints =
  DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> ([OutputForm_boot TCErr Expr Expr]
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> [OutputForm_boot TCErr Expr Expr]
-> CommandM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OutputForm_boot TCErr Expr Expr]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
[OutputForm_boot tcErr Expr Expr]
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Constraints ([OutputForm_boot TCErr Expr Expr] -> CommandM ())
-> StateT CommandState TCM [OutputForm_boot TCErr Expr Expr]
-> CommandM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM [OutputForm_boot TCErr Expr Expr]
-> StateT CommandState TCM [OutputForm_boot TCErr Expr Expr]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM [OutputForm_boot TCErr Expr Expr]
B.getConstraints

interpret (Cmd_metas Rewrite
norm) = do
  ms <- TCMT IO Goals -> StateT CommandState TCM Goals
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Goals -> StateT CommandState TCM Goals)
-> TCMT IO Goals -> StateT CommandState TCM Goals
forall a b. (a -> b) -> a -> b
$ Rewrite -> Rewrite -> TCMT IO Goals
B.getGoals' Rewrite
norm (Rewrite -> Rewrite -> Rewrite
forall a. Ord a => a -> a -> a
max Rewrite
Simplified Rewrite
norm)
  display_info . Info_AllGoalsWarnings ms =<< lift B.getWarningsAndNonFatalErrors

interpret (Cmd_load_no_metas String
file) = do
  -- Fail if there are open metas.
  let allowMetas :: Bool
allowMetas = Bool
False
  String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM ())
-> CommandM ()
forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
file [] Bool
allowMetas Mode
TypeCheck ((CheckResult -> CommandM ()) -> CommandM ())
-> (CheckResult -> CommandM ()) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \ CheckResult
result -> do
    CheckResult -> CommandM ()
forall (m :: * -> *).
(HasOptions m, MonadTCError m) =>
CheckResult -> m ()
Imp.raiseNonFatalErrors CheckResult
result
    StateT CommandState TCM Bool -> CommandM () -> CommandM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ([MetaId] -> Bool
forall a. Null a => a -> Bool
null ([MetaId] -> Bool)
-> StateT CommandState TCM [MetaId] -> StateT CommandState TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT CommandState TCM [MetaId]
forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas) CommandM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

interpret (Cmd_solveAll Rewrite
norm)        = Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals Rewrite
norm Maybe InteractionId
forall a. Maybe a
Nothing
interpret (Cmd_solveOne Rewrite
norm InteractionId
ii Range
_ String
_) = Rewrite -> Maybe InteractionId -> CommandM ()
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 String
s) = do
  (time, expr) <- (Expr -> TCM Expr) -> String -> CommandM (Maybe CPUTime, Expr)
forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel (Rewrite -> Expr -> TCM Expr
B.typeInCurrent Rewrite
norm) String
s
  state <- get
  display_info $ Info_InferredType state time expr

interpret (Cmd_compute_toplevel ComputeMode
cmode String
s) = do
  (time, expr) <- (Expr -> TCM Expr) -> String -> CommandM (Maybe CPUTime, Expr)
forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM Expr
action (ComputeMode -> String -> String
B.computeWrapInput ComputeMode
cmode String
s)
  state <- get
  display_info $ Info_NormalForm state cmode time expr
    where
    action :: Expr -> TCM Expr
action = TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
           (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if ComputeMode -> Bool
B.computeIgnoreAbstract ComputeMode
cmode then TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCM Expr -> TCM Expr
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
           (TCM Expr -> TCM Expr) -> (Expr -> TCM Expr) -> Expr -> TCM Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputeMode -> Expr -> TCM Expr
B.evalInCurrent ComputeMode
cmode
-- interpret (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
  opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  setCommandLineOpts $
    set (lensPragmaOptions . lensOptShowImplicit . lensKeepDefault) showImpl opts

interpret Interaction' Range
ToggleImplicitArgs = do
  opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  setCommandLineOpts $
    over (lensPragmaOptions . lensOptShowImplicit . lensCollapseDefault) not opts

interpret (ShowIrrelevantArgs Bool
showIrr) = do
  opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  setCommandLineOpts $
    set (lensPragmaOptions . lensOptShowIrrelevant . lensKeepDefault) showIrr opts

interpret Interaction' Range
ToggleIrrelevantArgs = do
  opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  setCommandLineOpts $
    over (lensPragmaOptions . lensOptShowIrrelevant . lensCollapseDefault) not opts

interpret (Cmd_load_highlighting_info String
source) = do
  l <- (TCEnv -> HighlightingLevel)
-> StateT CommandState TCM HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
  when (l /= None) $ do
    -- Make sure that the include directories have
    -- been set.
    setCommandLineOpts =<< lift commandLineOptions
    resp <- lift $ liftIO . tellToUpdateHighlighting =<< do
      ex        <- liftIO $ doesFileExist source
      absSource <- srcFromPath =<< liftIO (absolute source)
      if ex
        then
           do
              src <- Imp.parseSource absSource
              let m = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
              checkModuleName m absSource Nothing
              mmi <- getVisitedModule m
              case mmi of
                Maybe ModuleInfo
Nothing -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
                Just ModuleInfo
mi ->
                  if Text -> Hash
hashText (Source -> Text
Imp.srcText Source
src) Hash -> Hash -> Bool
forall a. Eq a => a -> a -> Bool
== Interface -> Hash
iSourceHash (ModuleInfo -> Interface
miInterface ModuleInfo
mi)
                    then do
                      modFile <- Lens' TCState ModuleToSource -> TCMT IO ModuleToSource
forall (m :: * -> *) a. ReadTCState m => Lens' TCState a -> m a
useTC (ModuleToSource -> f ModuleToSource) -> TCState -> f TCState
Lens' TCState ModuleToSource
stModuleToSource
                      method  <- viewTC eHighlightingMethod
                      return $ Just (iHighlighting $ miInterface mi, method, modFile)
                    else
                      Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
            `catchError` \TCErr
_ -> Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
-> TCMT
     IO (Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (HighlightingInfo, HighlightingMethod, ModuleToSource)
forall a. Maybe a
Nothing
        else
          return Nothing
    mapM_ putResponse resp

interpret (Cmd_tokenHighlighting String
source Remove
remove) = do
  info <- do l <- (TCEnv -> HighlightingLevel)
-> StateT CommandState TCM HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
             if l == None
               then return Nothing
               else do
                 source' <- liftIO (absolute source)
                 lift $ (Just <$> generateTokenInfo source')
                           `catchError` \TCErr
_ ->
                        Maybe HighlightingInfo -> TCM (Maybe HighlightingInfo)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe HighlightingInfo
forall a. Maybe a
Nothing
      StateT CommandState TCM (Maybe HighlightingInfo)
-> CommandM () -> 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 () -> CommandM ()
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CommandM ()) -> IO () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
removeFile String
source
      Remove
Keep   -> () -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  case info of
    Just HighlightingInfo
info' -> TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ RemoveTokenBasedHighlighting -> HighlightingInfo -> TCM ()
forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
RemoveHighlighting HighlightingInfo
info'
    Maybe HighlightingInfo
Nothing    -> () -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

interpret (Cmd_highlight InteractionId
ii Range
rng String
s) = do
  l <- (TCEnv -> HighlightingLevel)
-> StateT CommandState TCM HighlightingLevel
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
  when (l /= None) $ do
    scope <- getOldInteractionScope ii
    removeOldInteractionScope ii
    handle $ do
      parsed <- try (Info_HighlightingParseError ii) $
             B.parseExpr rng s
      expr <- try (Info_HighlightingScopeCheckError ii) $
             concreteToAbstract scope parsed
      lift $ printHighlightingInfo KeepHighlighting =<<
               generateTokenInfoFromString rng s
      lift $ highlightExpr expr
  where
    handle :: ExceptT Info_Error TCM () -> CommandM ()
    handle :: ExceptT Info_Error TCM () -> CommandM ()
handle ExceptT Info_Error TCM ()
m = do
      res <- TCM (Either Info_Error ())
-> StateT CommandState TCM (Either Info_Error ())
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Either Info_Error ())
 -> StateT CommandState TCM (Either Info_Error ()))
-> TCM (Either Info_Error ())
-> StateT CommandState TCM (Either Info_Error ())
forall a b. (a -> b) -> a -> b
$ ExceptT Info_Error TCM () -> TCM (Either Info_Error ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT Info_Error TCM ()
m
      case res of
        Left Info_Error
err -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ Info_Error
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
Info_Error_boot tcErr tcWarning
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Error Info_Error
err
        Right ()
_ -> () -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    try :: Info_Error -> TCM a -> ExceptT Info_Error TCM a
    try :: forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
try Info_Error
err TCM a
m = TCM (Either Info_Error a) -> ExceptT Info_Error TCM a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (TCM (Either Info_Error a) -> ExceptT Info_Error TCM a)
-> TCM (Either Info_Error a) -> ExceptT Info_Error TCM a
forall a b. (a -> b) -> a -> b
$ do
      ((TCErr -> Info_Error) -> Either TCErr a -> Either Info_Error a
forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft (Info_Error -> TCErr -> Info_Error
forall a b. a -> b -> a
const Info_Error
err) (Either TCErr a -> Either Info_Error a)
-> TCMT IO (Either TCErr a) -> TCM (Either Info_Error a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM a -> TCMT IO (Either TCErr a)
forall a. TCM a -> TCM (Either TCErr a)
freshTCM TCM a
m) TCM (Either Info_Error a)
-> (TCErr -> TCM (Either Info_Error a))
-> TCM (Either Info_Error a)
forall a. TCM a -> (TCErr -> TCM a) -> TCM a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> Either Info_Error a -> TCM (Either Info_Error a)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Info_Error -> Either Info_Error a
forall a b. a -> Either a b
Left Info_Error
err)
      -- freshTCM to avoid scope checking creating new interaction points

interpret (Cmd_give   UseForce
force InteractionId
ii Range
rng String
s) = UseForce
-> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
give_gen UseForce
force InteractionId
ii Range
rng String
s GiveRefine
Give
interpret (Cmd_refine InteractionId
ii Range
rng String
s) = UseForce
-> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng String
s GiveRefine
Refine

interpret (Cmd_intro Bool
pmLambda InteractionId
ii Range
rng String
_) = do
  ss <- TCMT IO [String] -> StateT CommandState TCM [String]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [String] -> StateT CommandState TCM [String])
-> TCMT IO [String] -> StateT CommandState TCM [String]
forall a b. (a -> b) -> a -> b
$ Bool -> InteractionId -> TCMT IO [String]
B.introTactic Bool
pmLambda InteractionId
ii
  liftCommandMT (withInteractionId ii) $ case ss of
    []    -> do
      DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Intro_NotFound
    [String
s]   -> UseForce
-> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng String
s GiveRefine
Intro
    String
_:String
_:[String]
_ -> do
      DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ [String]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
[String]
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Intro_ConstructorUnknown [String]
ss

interpret (Cmd_refine_or_intro Bool
pmLambda InteractionId
ii Range
r String
s) = Interaction' Range -> CommandM ()
interpret (Interaction' Range -> CommandM ())
-> Interaction' Range -> CommandM ()
forall a b. (a -> b) -> a -> b
$
  let s' :: String
s' = String -> String
trim String
s
  in (if String -> Bool
forall a. Null a => a -> Bool
null String
s' then Bool -> InteractionId -> Range -> String -> Interaction' Range
forall range.
Bool -> InteractionId -> range -> String -> Interaction' range
Cmd_intro Bool
pmLambda else InteractionId -> Range -> String -> Interaction' Range
forall range.
InteractionId -> range -> String -> Interaction' range
Cmd_refine) InteractionId
ii Range
r String
s'

interpret (Cmd_autoOne Rewrite
norm InteractionId
ii Range
rng String
str) = do
  iscope <- InteractionId -> CommandM ScopeInfo
forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
  (time, result) <- maybeTimed $ Mimer.mimer norm ii rng str
  case result of
    MimerResult
MimerNoResult -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
String
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Auto String
"No solution found"
    MimerExpr String
str -> do
      InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope InteractionId
ii ScopeInfo
iscope
      Response -> CommandM ()
putResponse (Response -> CommandM ()) -> Response -> CommandM ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> GiveResult
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_GiveAction InteractionId
ii (GiveResult -> Response) -> GiveResult -> Response
forall a b. (a -> b) -> a -> b
$ String -> GiveResult
Give_String String
str
      ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints (InteractionId -> [InteractionId] -> [InteractionId]
forall a. Eq a => a -> [a] -> [a]
List.delete InteractionId
ii)
      CommandM ()
-> (CPUTime -> CommandM ()) -> Maybe CPUTime -> CommandM ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> CommandM ()
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> (CPUTime
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> CPUTime
-> CommandM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CPUTime
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
CPUTime
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Time) Maybe CPUTime
time
    MimerList [(Int, String)]
sols -> do
      DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
String
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Auto (String
 -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> String
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
        [ String
"Solutions:" ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
        [ String
"  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s | (Int
i, String
s) <- [(Int, String)]
sols ]
    MimerClauses{} -> CommandM ()
forall a. HasCallStack => a
__IMPOSSIBLE__    -- Mimer can't do case splitting yet

interpret (Cmd_autoAll Rewrite
norm) = do
  iis <- StateT CommandState TCM [InteractionId]
forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
  getOldScope <- do
    st <- getTC
    pure $ \ InteractionId
ii -> TCM ScopeInfo -> CommandM ScopeInfo
forall b. TCM b -> StateT CommandState TCM b
liftLocalState (TCM ScopeInfo -> CommandM ScopeInfo)
-> TCM ScopeInfo -> CommandM ScopeInfo
forall a b. (a -> b) -> a -> b
$ TCState -> TCM ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st TCM () -> TCM ScopeInfo -> TCM ScopeInfo
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> InteractionId -> TCM ScopeInfo
forall (m :: * -> *).
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
  unless (null iis) $ do
    let time = Int
1000 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` [InteractionId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [InteractionId]
iis
    st <- getTC
    solved <- fmap concat $ forM iis $ \ InteractionId
ii -> do
      rng <- InteractionId -> StateT CommandState TCM Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadDebug m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
ii
      res <- Mimer.mimer norm ii rng ("-t " ++ show time ++ "ms")
      case res of
        MimerResult
MimerNoResult -> [InteractionId] -> StateT CommandState TCM [InteractionId]
forall a. a -> StateT CommandState TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        MimerExpr String
str -> do
          InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope InteractionId
ii (ScopeInfo -> CommandM ()) -> CommandM ScopeInfo -> CommandM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> CommandM ScopeInfo
getOldScope InteractionId
ii
          Response -> CommandM ()
putResponse (Response -> CommandM ()) -> Response -> CommandM ()
forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> GiveResult
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_GiveAction InteractionId
ii (GiveResult -> Response) -> GiveResult -> Response
forall a b. (a -> b) -> a -> b
$ String -> GiveResult
Give_String String
str
          [InteractionId] -> StateT CommandState TCM [InteractionId]
forall a. a -> StateT CommandState TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [InteractionId
ii]
        MimerList{} -> [InteractionId] -> StateT CommandState TCM [InteractionId]
forall a. a -> StateT CommandState TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []    -- Don't list solutions in autoAll
        MimerClauses{} -> StateT CommandState TCM [InteractionId]
forall a. HasCallStack => a
__IMPOSSIBLE__  -- Mimer can't do case splitting yet
    modifyTheInteractionPoints (List.\\ solved)

interpret (Cmd_context Rewrite
norm InteractionId
ii Range
_ String
_) =
  DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> ([ResponseContextEntry]
    -> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors)
-> [ResponseContextEntry]
-> CommandM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId
-> [ResponseContextEntry]
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> [ResponseContextEntry]
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Context InteractionId
ii ([ResponseContextEntry] -> CommandM ())
-> StateT CommandState TCM [ResponseContextEntry] -> CommandM ()
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 String
s) = do
  -- Create type of application of new helper function that would solve the goal.
  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.
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM (OutputConstraint' Expr Expr)
 -> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM (OutputConstraint' Expr Expr)
 -> TCM (OutputConstraint' Expr Expr))
-> TCM (OutputConstraint' Expr Expr)
-> TCM (OutputConstraint' Expr Expr)
forall a b. (a -> b) -> a -> b
$ Rewrite
-> InteractionId
-> Range
-> String
-> TCM (OutputConstraint' Expr Expr)
B.metaHelperType Rewrite
norm InteractionId
ii Range
rng String
s
  display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType)

interpret (Cmd_infer Rewrite
norm InteractionId
ii Range
rng String
s) = do
  expr <- TCM Expr -> CommandM Expr
forall 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.
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall a b. (a -> b) -> a -> b
$ InteractionId -> Rewrite -> Expr -> TCM Expr
B.typeInMeta InteractionId
ii Rewrite
norm (Expr -> TCM Expr) -> TCM Expr -> TCM Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng String
s
  display_info $ Info_GoalSpecific ii (Goal_InferredType expr)

interpret (Cmd_goal_type Rewrite
norm InteractionId
ii Range
_ String
_) =
  DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info (DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
 -> CommandM ())
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
forall a b. (a -> b) -> a -> b
$ InteractionId
-> GoalDisplayInfo_boot TCErr
-> DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
InteractionId
-> GoalDisplayInfo_boot tcErr
-> DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_GoalSpecific InteractionId
ii (Rewrite -> GoalDisplayInfo_boot TCErr
forall tcErr. Rewrite -> GoalDisplayInfo_boot tcErr
Goal_CurrentGoal Rewrite
norm)

interpret (Cmd_elaborate_give Rewrite
norm InteractionId
ii Range
rng String
s) =
  UseForce
-> InteractionId -> Range -> String -> GiveRefine -> CommandM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng String
s (GiveRefine -> CommandM ()) -> GiveRefine -> CommandM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> GiveRefine
ElaborateGive Rewrite
norm

interpret (Cmd_goal_type_context Rewrite
norm InteractionId
ii Range
rng String
s) =
  GoalTypeAux
-> Rewrite -> InteractionId -> Range -> String -> CommandM ()
cmd_goal_type_context_and GoalTypeAux
GoalOnly Rewrite
norm InteractionId
ii Range
rng String
s

interpret (Cmd_goal_type_context_infer Rewrite
norm InteractionId
ii Range
rng String
s) = do
  -- 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.
  aux <- if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
Char.isSpace String
s
            then GoalTypeAux -> StateT CommandState TCM GoalTypeAux
forall a. a -> StateT CommandState TCM a
forall (m :: * -> *) a. Monad m => a -> m a
return GoalTypeAux
GoalOnly
            else do
              TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux
forall b. TCM b -> StateT CommandState TCM b
liftLocalState (TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux)
-> TCM GoalTypeAux -> StateT CommandState TCM GoalTypeAux
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCM GoalTypeAux -> TCM GoalTypeAux
forall (m :: * -> *) a.
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCM GoalTypeAux -> TCM GoalTypeAux)
-> TCM GoalTypeAux -> TCM GoalTypeAux
forall a b. (a -> b) -> a -> b
$ do
                parsed <- InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng String
s
                (typ, faces) <- B.typeAndFacesInMeta ii norm parsed
                return (GoalAndHave typ faces)
  cmd_goal_type_context_and aux norm ii rng s

interpret (Cmd_goal_type_context_check Rewrite
norm InteractionId
ii Range
rng String
s) = do
  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.
(MonadDebug 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
$ do
    expr <- InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng String
s
    goal <- B.typeOfMeta AsIs ii
    term <- case goal of
      OfType InteractionId
_ Expr
ty -> Expr -> Type -> TCMT IO Term
checkExpr Expr
expr (Type -> TCMT IO Term) -> TCMT IO Type -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCMT IO Type
isType_ Expr
ty
      OutputConstraint Expr InteractionId
_           -> TCMT IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    reify =<< B.normalForm norm term
  cmd_goal_type_context_and (GoalAndElaboration expr) norm ii rng s

interpret (Cmd_show_module_contents Rewrite
norm InteractionId
ii Range
rng String
s) =
  (forall x. TCM x -> TCM x) -> CommandM () -> CommandM ()
forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> String -> CommandM ()
showModuleContents Rewrite
norm Range
rng String
s

interpret (Cmd_why_in_scope_toplevel String
s) =
  CommandM () -> CommandM ()
forall a. CommandM a -> CommandM a
atTopLevel (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String -> CommandM ()
whyInScope String
s

interpret (Cmd_why_in_scope InteractionId
ii Range
_range String
s) =
  (forall x. TCM x -> TCM x) -> CommandM () -> CommandM ()
forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT (InteractionId -> TCMT IO x -> TCMT IO x
forall (m :: * -> *) a.
(MonadDebug m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String -> CommandM ()
whyInScope String
s

interpret (Cmd_make_case InteractionId
ii Range
rng String
s) = do
  (f, casectxt, cs) <- TCMT IO (QName, CaseContext, [Clause])
-> StateT CommandState TCM (QName, CaseContext, [Clause])
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (QName, CaseContext, [Clause])
 -> StateT CommandState TCM (QName, CaseContext, [Clause]))
-> TCMT IO (QName, CaseContext, [Clause])
-> StateT CommandState TCM (QName, CaseContext, [Clause])
forall a b. (a -> b) -> a -> b
$ InteractionId
-> Range -> String -> TCMT IO (QName, CaseContext, [Clause])
makeCase InteractionId
ii Range
rng String
s
  liftCommandMT (withInteractionId ii) $ do
    tel <- lift $ lookupSection (qnameModule f) -- don't shadow the names in this telescope
    unicode <- getsTC $ optUseUnicode . getPragmaOptions
    pcs      :: [Doc]      <- lift $ inTopContext $ addContext tel $ mapM prettyAUnqualify cs
    let pcs' :: [String]    = List.map (extlam_dropName unicode casectxt . decorate) pcs
    lift $ reportSDoc "interaction.case" 60 $ TCP.vcat
      [ "InteractionTop.Cmd_make_case"
      , TCP.nest 2 $ TCP.vcat
        [ "cs   = " TCP.<+> TCP.vcat (map prettyA cs)
        , "pcs  = " TCP.<+> TCP.vcat (map return pcs)
        , "pcs' = " TCP.<+> TCP.vcat (map TCP.text pcs')
        ]
      ]
    lift $ reportSDoc "interaction.case" 90 $ TCP.vcat
      [ "InteractionTop.Cmd_make_case"
      , TCP.nest 2 $ TCP.vcat
        [ "cs   = " TCP.<+> TCP.text (show cs)
        ]
      ]
    putResponse $ Resp_MakeCase ii (makeCaseVariant casectxt) pcs'


interpret (Cmd_compute ComputeMode
cmode InteractionId
ii Range
rng String
s) = do
  expr <- TCM Expr -> CommandM Expr
forall b. TCM b -> StateT CommandState TCM b
liftLocalState (TCM Expr -> CommandM Expr) -> TCM Expr -> CommandM Expr
forall a b. (a -> b) -> a -> b
$ do
    e <- InteractionId -> Range -> String -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng (String -> TCM Expr) -> String -> TCM Expr
forall a b. (a -> b) -> a -> b
$ ComputeMode -> String -> String
B.computeWrapInput ComputeMode
cmode String
s
    withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e
  display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr)

interpret Interaction' Range
Cmd_show_version = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
Info_Version

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


decorate :: Doc -> String
decorate :: Doc -> String
decorate = Style -> Doc -> String
forall a. Style -> Doc a -> String
renderStyle (Style
style { mode = OneLineMode })

makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant :: CaseContext -> MakeCaseVariant
makeCaseVariant CaseContext
Nothing = MakeCaseVariant
R.Function
makeCaseVariant Just{}  = MakeCaseVariant
R.ExtendedLambda

-- 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 -> String -> String
extlam_dropName UnicodeOrAscii
_ CaseContext
Nothing String
x = String
x
extlam_dropName UnicodeOrAscii
glyphMode Just{}  String
x
    = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
replEquals ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
drop Int
1 ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
x
  where
    arrow :: String
arrow = Doc -> String
forall a. Doc a -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ SpecialCharacters -> Doc
_arrow (SpecialCharacters -> Doc) -> SpecialCharacters -> Doc
forall a b. (a -> b) -> a -> b
$ UnicodeOrAscii -> SpecialCharacters
specialCharactersForGlyphs UnicodeOrAscii
glyphMode
    replEquals :: [String] -> [String]
replEquals (String
"=" : [String]
ws) = String
arrow String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ws
    replEquals (String
w   : [String]
ws) = String
w String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String] -> [String]
replEquals [String]
ws
    replEquals []         = []

-- | Solved goals already instantiated internally
-- The second argument potentially limits it to one specific goal.
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals :: Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals Rewrite
norm Maybe InteractionId
mii = do
  -- Andreas, 2016-10-23 issue #2280: throw away meta elims.
  out <- TCM [(InteractionId, Expr)]
-> StateT CommandState TCM [(InteractionId, Expr)]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [(InteractionId, Expr)]
 -> StateT CommandState TCM [(InteractionId, Expr)])
-> TCM [(InteractionId, Expr)]
-> StateT CommandState TCM [(InteractionId, Expr)]
forall a b. (a -> b) -> a -> b
$ (TCEnv -> TCEnv)
-> TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)]
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\ TCEnv
e -> TCEnv
e { envPrintMetasBare = True }) (TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)])
-> TCM [(InteractionId, Expr)] -> TCM [(InteractionId, Expr)]
forall a b. (a -> b) -> a -> b
$ do
    sip <- Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
B.getSolvedInteractionPoints Bool
False Rewrite
norm
           -- only solve metas which have a proper instantiation, i.e., not another meta
    let sip' = ([(InteractionId, MetaId, Expr)]
 -> [(InteractionId, MetaId, Expr)])
-> (InteractionId
    -> [(InteractionId, MetaId, Expr)]
    -> [(InteractionId, MetaId, Expr)])
-> Maybe InteractionId
-> [(InteractionId, MetaId, Expr)]
-> [(InteractionId, MetaId, Expr)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [(InteractionId, MetaId, Expr)] -> [(InteractionId, MetaId, Expr)]
forall a. a -> a
id (\ InteractionId
ii -> ((InteractionId, MetaId, Expr) -> Bool)
-> [(InteractionId, MetaId, Expr)]
-> [(InteractionId, MetaId, Expr)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((InteractionId
ii InteractionId -> InteractionId -> Bool
forall a. Eq a => a -> a -> Bool
==) (InteractionId -> Bool)
-> ((InteractionId, MetaId, Expr) -> InteractionId)
-> (InteractionId, MetaId, Expr)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionId, MetaId, Expr) -> InteractionId
forall a b c. (a, b, c) -> a
fst3)) Maybe InteractionId
mii [(InteractionId, MetaId, Expr)]
sip
    mapM prt sip'
  putResponse $ Resp_SolveAll out
  where
      prt :: (a, MetaId, a) -> m (a, ConOfAbs a)
prt (a
i, MetaId
m, a
e) = do
        mi <- MetaVariable -> Closure Range
getMetaInfo (MetaVariable -> Closure Range)
-> m MetaVariable -> m (Closure Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MetaId -> m MetaVariable
forall (m :: * -> *).
(HasCallStack, MonadDebug m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupLocalMeta MetaId
m
        e' <- withMetaInfo mi $ abstractToConcreteCtx TopCtx e
        return (i, e')

-- | @cmd_load' 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' :: forall a.
String
-> [String]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' String
file [String]
argv Bool
unsolvedOK Mode
mode CheckResult -> CommandM a
cmd = do

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

    -- Update the status. Because the "current file" is not set the
    -- status is not "Checked".
    CommandM ()
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.
    TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM ()
resetState

    -- Clear the info buffer to make room for information about which
    -- module is currently being type-checked.
    Response -> CommandM ()
putResponse Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_ClearRunningInfo

    -- Remove any prior syntax highlighting.
    Response -> CommandM ()
putResponse (TokenBased -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
TokenBased
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_ClearHighlighting TokenBased
NotOnlyTokenBased)

    -- Parse the file.
    --
    -- Note that options are set below.
    fp  <- IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a. IO a -> StateT CommandState TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO AbsolutePath -> StateT CommandState TCM AbsolutePath)
-> IO AbsolutePath -> StateT CommandState TCM AbsolutePath
forall a b. (a -> b) -> a -> b
$ String -> IO AbsolutePath
absolute String
file
    sf  <- liftTCM $ srcFromPath fp
    src <- lift $ Imp.parseSource sf
    -- Andreas, 2024-08-03, see test/interaction/FileNotFound:
    -- Run 'getModificationTime' after 'parseSource',
    -- otherwise the user gets a weird error for non-existing files.
    -- (We assume that parsing is fast in comparison to type-checking,
    -- so it should not matter much whether we get the time stamp
    -- before or after parsing.)
    t   <- liftIO $ getModificationTime file

    -- Store the warnings.
    warnings <- useTC stTCWarnings

    -- All options are reset when a file is reloaded, including the
    -- choice of whether or not to display implicit arguments.
    opts0 <- gets optionsOnReload
    backends <- useTC stBackends
    let (z, warns) = runOptM $ parseBackendOptions backends argv opts0
    mapM_ (lift . warning . OptionWarning) warns
    case z of
      Left String
err -> TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
OptionError String
err
      Right ([Backend]
_, CommandLineOptions
opts) -> do
        opts <- TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM CommandLineOptions
 -> StateT CommandState TCM CommandLineOptions)
-> TCM CommandLineOptions
-> StateT CommandState TCM CommandLineOptions
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM CommandLineOptions
addTrustedExecutables CommandLineOptions
opts
        let update = Lens' PragmaOptions Bool -> LensMap PragmaOptions Bool
forall o i. Lens' o i -> LensMap o i
over ((WithDefault 'False -> f (WithDefault 'False))
-> PragmaOptions -> f PragmaOptions
forall (f :: * -> *).
Functor f =>
(WithDefault 'False -> f (WithDefault 'False))
-> PragmaOptions -> f PragmaOptions
lensOptAllowUnsolved ((WithDefault 'False -> f (WithDefault 'False))
 -> PragmaOptions -> f PragmaOptions)
-> ((Bool -> f Bool)
    -> WithDefault 'False -> f (WithDefault 'False))
-> (Bool -> f Bool)
-> PragmaOptions
-> f PragmaOptions
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> f Bool) -> WithDefault 'False -> f (WithDefault 'False)
forall a (b :: Bool).
(Boolean a, Eq a, KnownBool b) =>
Lens' (WithDefault' a b) a
Lens' (WithDefault 'False) Bool
lensKeepDefault) (Bool
unsolvedOK Bool -> Bool -> Bool
&&)
            root   = AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
fp (TopLevelModuleName -> AbsolutePath)
-> TopLevelModuleName -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ Source -> TopLevelModuleName
Imp.srcModuleName Source
src
        lift $ TCM.setCommandLineOptions' root $ mapPragmaOptions update opts

    -- Restore the warnings that were saved above.
    modifyTCLens stTCWarnings $ Set.union warnings

    ok <- lift $ Imp.typeCheckMain mode 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.
    t' <- liftIO $ getModificationTime file
    when (t == t') $ do
      is <- lift $ sortInteractionPoints =<< getInteractionPoints
      modify $ \CommandState
st -> CommandState
st { theInteractionPoints = is
                         , theCurrentFile       = Just $ CurrentFile
                             { currentFilePath   = fp
                             , currentFileModule = Imp.srcModuleName src
                             , currentFileArgs   = argv
                             , currentFileStamp  = t
                             }
                         }

    cmd ok

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

atTopLevel :: CommandM a -> CommandM a
atTopLevel :: forall a. CommandM a -> CommandM a
atTopLevel CommandM a
cmd = (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
forall a. (forall x. TCM x -> TCM x) -> CommandM a -> CommandM a
liftCommandMT TCM x -> TCM x
forall x. TCM x -> TCM x
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
$c== :: GiveRefine -> GiveRefine -> Bool
== :: GiveRefine -> GiveRefine -> Bool
$c/= :: GiveRefine -> GiveRefine -> Bool
/= :: GiveRefine -> GiveRefine -> Bool
Eq, Int -> GiveRefine -> String -> String
[GiveRefine] -> String -> String
GiveRefine -> String
(Int -> GiveRefine -> String -> String)
-> (GiveRefine -> String)
-> ([GiveRefine] -> String -> String)
-> Show GiveRefine
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> GiveRefine -> String -> String
showsPrec :: Int -> GiveRefine -> String -> String
$cshow :: GiveRefine -> String
show :: GiveRefine -> String
$cshowList :: [GiveRefine] -> String -> String
showList :: [GiveRefine] -> String -> String
Show)

-- | 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 -> String -> GiveRefine -> CommandM ()
give_gen UseForce
force InteractionId
ii Range
rng String
s0 GiveRefine
giveRefine = do
  let s :: String
s = String -> String
trim String
s0
  String -> Int -> String -> CommandM ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"interaction.give" Int
20 (String -> CommandM ()) -> String -> CommandM ()
forall a b. (a -> b) -> a -> b
$ String
"give_gen  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
  -- Andreas, 2015-02-26 if string is empty do nothing rather
  -- than giving a parse error.
  Bool -> CommandM () -> CommandM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (String -> Bool
forall a. Null a => a -> Bool
null String
s) (CommandM () -> CommandM ()) -> CommandM () -> CommandM ()
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)
    scope     <- InteractionId -> CommandM ScopeInfo
forall (m :: * -> *).
(MonadDebug 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
    (time, (ae, ae0, iis)) <- maybeTimed $ do
        -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential
        -- new interaction points introduced by the give.
        removeInteractionPoint ii
        mis  <- getInteractionPoints
        reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis
        given <- lift $ B.parseExprIn ii rng s
        ae    <- lift $ give_ref force ii Nothing given
        mis' <- getInteractionPoints
        reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'
        return (ae, given, mis' List.\\ mis)
    -- favonia: backup the old scope for highlighting
    insertOldInteractionScope ii scope
    -- sort the new interaction points and put them into the state
    -- in replacement of the old interaction point
    iis' <- sortInteractionPoints iis
    modifyTheInteractionPoints $ replace ii iis'
    -- print abstract expr
    ce        <- abstractToConcreteScope scope ae
    reportS "interaction.give" 30
      [ "ce = " ++ show ce
      , "scopePrecedence = " ++ show (scope ^. scopePrecedence)
      ]

    -- Issue 7218: if the give/refine command creates an extended
    -- lambda, it also needs to be added to the relevant unfolding sets.
    -- The easiest way to make sure this is consistent is to just re-run
    -- the saturation procedures.
    saturateOpaqueBlocks

    -- 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 = (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.
    when literally $ do
      l <- asksTC envHighlightingLevel
      when (l /= None) $ lift $ do
        printHighlightingInfo KeepHighlighting =<<
          generateTokenInfoFromString rng s
        highlightExpr ae
    putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce
    reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"
    -- display new goal set (if not measuring time)
    maybe (interpret $ Cmd_metas AsIs) (display_info . Info_Time) time
    reportSLn "interaction.give" 30 $ "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        = String -> GiveResult
Give_String (String -> GiveResult) -> String -> GiveResult
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. Pretty a => a -> String
prettyShow Expr
ce

highlightExpr :: A.Expr -> TCM ()
highlightExpr :: Expr -> TCM ()
highlightExpr Expr
e =
  (TCEnv -> TCEnv) -> TCM () -> TCM ()
forall a. (TCEnv -> TCEnv) -> TCMT IO a -> TCMT IO a
forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
st -> TCEnv
st { envImportPath         = []
                     , envHighlightingLevel  = NonInteractive
                     , envHighlightingMethod = Direct }) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
decl Level
Full Bool
True
  where
    dummy :: Name
dummy = NameId -> String -> Name
forall a. MkName a => NameId -> a -> Name
mkName_ (Hash -> ModuleNameHash -> NameId
NameId Hash
0 ModuleNameHash
noModuleNameHash) (String
"dummy" :: String)
    info :: DefInfo' Expr
info  = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete Name
dummy) Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef (Expr -> Range
forall a. HasRange a => a -> Range
getRange Expr
e)
    decl :: Declaration
decl  = KindOfName
-> DefInfo' Expr
-> ArgInfo
-> Maybe PragmaPolarities
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
OtherDefName DefInfo' Expr
info ArgInfo
defaultArgInfo Maybe PragmaPolarities
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, MonadDebug m)
  => [InteractionId] -> m [InteractionId]
sortInteractionPoints :: forall (m :: * -> *).
(MonadInteractionPoints m, MonadError TCErr m, MonadDebug m) =>
[InteractionId] -> m [InteractionId]
sortInteractionPoints [InteractionId]
is =
  ((InteractionId, Range) -> InteractionId)
-> [(InteractionId, Range)] -> [InteractionId]
forall a b. (a -> b) -> [a] -> [b]
map (InteractionId, Range) -> InteractionId
forall a b. (a, b) -> a
fst ([(InteractionId, Range)] -> [InteractionId])
-> ([(InteractionId, Range)] -> [(InteractionId, Range)])
-> [(InteractionId, Range)]
-> [InteractionId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InteractionId, Range) -> (InteractionId, Range) -> Ordering)
-> [(InteractionId, Range)] -> [(InteractionId, Range)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (Range -> Range -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Range -> Range -> Ordering)
-> ((InteractionId, Range) -> Range)
-> (InteractionId, Range)
-> (InteractionId, Range)
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (InteractionId, Range) -> Range
forall a b. (a, b) -> b
snd) ([(InteractionId, Range)] -> [InteractionId])
-> m [(InteractionId, Range)] -> m [InteractionId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
    [InteractionId]
-> (InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [InteractionId]
is ((InteractionId -> m (InteractionId, Range))
 -> m [(InteractionId, Range)])
-> (InteractionId -> m (InteractionId, Range))
-> m [(InteractionId, Range)]
forall a b. (a -> b) -> a -> b
$ \ InteractionId
i -> do
      (InteractionId
i,) (Range -> (InteractionId, Range))
-> m Range -> m (InteractionId, Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InteractionId -> m Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadDebug 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 -> String -> CommandM ()
cmd_goal_type_context_and GoalTypeAux
aux Rewrite
norm InteractionId
ii Range
_ String
_ = do
  ctx <- TCM [ResponseContextEntry]
-> StateT CommandState TCM [ResponseContextEntry]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [ResponseContextEntry]
 -> StateT CommandState TCM [ResponseContextEntry])
-> TCM [ResponseContextEntry]
-> StateT CommandState TCM [ResponseContextEntry]
forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> TCM [ResponseContextEntry]
B.getResponseContext Rewrite
norm InteractionId
ii
  constr <- lift $ lookupInteractionId ii >>= B.getConstraintsMentioning norm
  boundary <- lift $ B.getIPBoundary norm ii
  display_info $ Info_GoalSpecific ii (Goal_GoalType norm aux ctx boundary constr)

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

showModuleContents :: Rewrite -> Range -> String -> CommandM ()
showModuleContents :: Rewrite -> Range -> String -> CommandM ()
showModuleContents Rewrite
norm Range
rng String
s = do
  (modules, tel, types) <- TCMT IO ([Name], Telescope, [(Name, Type)])
-> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO ([Name], Telescope, [(Name, Type)])
 -> StateT CommandState TCM ([Name], Telescope, [(Name, Type)]))
-> TCMT IO ([Name], Telescope, [(Name, Type)])
-> StateT CommandState TCM ([Name], Telescope, [(Name, Type)])
forall a b. (a -> b) -> a -> b
$ Rewrite
-> Range -> String -> TCMT IO ([Name], Telescope, [(Name, Type)])
B.moduleContents Rewrite
norm Range
rng String
s
  display_info $ Info_ModuleContents modules tel types

-- | 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 -> String -> CommandM ()
searchAbout Rewrite
norm Range
rg String
names = do
  String -> (String -> CommandM ()) -> CommandM ()
forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull (String -> String
trim String
names) ((String -> CommandM ()) -> CommandM ())
-> (String -> CommandM ()) -> CommandM ()
forall a b. (a -> b) -> a -> b
$ \ String
trimmedNames -> do
    hits <- TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)])
-> TCMT IO [(Name, Type)] -> StateT CommandState TCM [(Name, Type)]
forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> String -> TCMT IO [(Name, Type)]
findMentions Rewrite
norm Range
rg String
trimmedNames
    display_info $ Info_SearchAbout hits trimmedNames

-- | Explain why something is in scope.

whyInScope :: String -> CommandM ()
whyInScope :: String -> CommandM ()
whyInScope String
s = do
  Just file <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
  let cwd = String -> String
takeDirectory (AbsolutePath -> String
filePath (AbsolutePath -> String) -> AbsolutePath -> String
forall a b. (a -> b) -> a -> b
$ CurrentFile -> AbsolutePath
currentFilePath CurrentFile
file)
  why <- liftLocalState $ B.whyInScope cwd s
  display_info $ Info_WhyInScope why

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

setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts CommandLineOptions
opts = do
    TCM () -> CommandM ()
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> CommandM ()) -> TCM () -> CommandM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM ()
TCM.setCommandLineOptions CommandLineOptions
opts
    CommandM ()
displayStatus


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

status :: CommandM Status
status :: CommandM Status
status = do
  cf       <- (CommandState -> Maybe CurrentFile)
-> StateT CommandState TCM (Maybe CurrentFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
  showImpl <- lift showImplicitArguments
  showIrr  <- lift showIrrelevantArguments

  -- 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.
  checked  <- lift $ case cf of
    Maybe CurrentFile
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just CurrentFile
f  -> do
      t <- IO ClockTime -> TCMT IO ClockTime
forall b. IO b -> TCM b
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ClockTime -> TCMT IO ClockTime)
-> IO ClockTime -> TCMT IO ClockTime
forall a b. (a -> b) -> a -> b
$ String -> IO ClockTime
getModificationTime (String -> IO ClockTime) -> String -> IO ClockTime
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath (CurrentFile -> AbsolutePath
currentFilePath CurrentFile
f)
      if currentFileStamp f == t
        then
          maybe False (null . miWarnings) <$>
          getVisitedModule (currentFileModule f)
        else
            return False

  return $ Status { sShowImplicitArguments   = showImpl,
                    sShowIrrelevantArguments = showIrr,
                    sChecked                 = checked }

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

displayStatus :: CommandM ()
displayStatus :: CommandM ()
displayStatus =
  Response -> CommandM ()
putResponse (Response -> CommandM ())
-> (Status -> Response) -> Status -> CommandM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Status -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
Status -> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_Status  (Status -> CommandM ()) -> CommandM Status -> CommandM ()
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_boot TCErr TCWarning WarningsAndNonFatalErrors
-> CommandM ()
display_info DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info = do
  CommandM ()
displayStatus
  Response -> CommandM ()
putResponse (Response -> CommandM ()) -> Response -> CommandM ()
forall a b. (a -> b) -> a -> b
$ DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
DisplayInfo_boot tcErr tcWarning warningsAndNonFatalErrors
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_DisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info

-- | 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 :: forall a. (Expr -> TCM a) -> String -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM a
cmd String
s = do
  CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
forall a. CommandM a -> CommandM a
localStateCommandM (CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a))
-> CommandM (Maybe CPUTime, a) -> CommandM (Maybe CPUTime, a)
forall a b. (a -> b) -> a -> b
$ do
    (e, attrs) <- TCM (Expr, Attributes)
-> StateT CommandState TCM (Expr, Attributes)
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Expr, Attributes)
 -> StateT CommandState TCM (Expr, Attributes))
-> TCM (Expr, Attributes)
-> StateT CommandState TCM (Expr, Attributes)
forall a b. (a -> b) -> a -> b
$ PM (Expr, Attributes) -> TCM (Expr, Attributes)
forall a. PM a -> TCM a
runPM (PM (Expr, Attributes) -> TCM (Expr, Attributes))
-> PM (Expr, Attributes) -> TCM (Expr, Attributes)
forall a b. (a -> b) -> a -> b
$ Parser Expr -> String -> PM (Expr, Attributes)
forall a. Parser a -> String -> PM (a, Attributes)
parse Parser Expr
exprParser String
s
    lift $ checkAttributes attrs
    maybeTimed $ atTopLevel $ lift $
      cmd =<< concreteToAbstract_ e

maybeTimed :: CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed :: forall a. CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed CommandM a
work = do
  doTime <- TCMT IO Bool -> StateT CommandState TCM Bool
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Bool -> StateT CommandState TCM Bool)
-> TCMT IO Bool -> StateT CommandState TCM Bool
forall a b. (a -> b) -> a -> b
$ ProfileOption -> TCMT IO Bool
forall (m :: * -> *). MonadDebug m => ProfileOption -> m Bool
hasProfileOption ProfileOption
Profile.Interactive
  if not doTime
    then (Nothing,) <$> work
    else do
      (r, time) <- measureTime work
      return (Just time, r)

-- | 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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
tellToUpdateHighlighting (Just (HighlightingInfo
info, HighlightingMethod
method, ModuleToSource
modFile)) =
  [Response] -> IO [Response]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
KeepHighlighting HighlightingMethod
method ModuleToSource
modFile]

-- | 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' (Maybe RangeFile))
forall a. Range' a -> Maybe (Position' a)
rStart Range
r of
    Maybe (Position' (Maybe RangeFile))
Nothing                                           -> []
    Just (Pn { srcFile :: forall a. Position' a -> a
srcFile = Maybe RangeFile
Strict.Nothing })            -> []
    Just (Pn { srcFile :: forall a. Position' a -> a
srcFile = Strict.Just RangeFile
f, posPos :: forall a. Position' a -> Word32
posPos = Word32
p }) ->
       [ String -> Word32 -> Response
forall tcErr tcWarning warningsAndNonFatalErrors.
String
-> Word32
-> Response_boot tcErr tcWarning warningsAndNonFatalErrors
Resp_JumpToError (AbsolutePath -> String
filePath (RangeFile -> AbsolutePath
rangeFilePath RangeFile
f)) Word32
p ]