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

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

import Prelude hiding (null)

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

import qualified Control.Exception  as E

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

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

import System.Directory
import System.FilePath

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

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

import Agda.Interaction.Base
import Agda.Interaction.ExitCode
import Agda.Interaction.FindFile
import Agda.Interaction.Options
import Agda.Interaction.Options.Lenses as Lenses
import Agda.Interaction.MakeCase
import Agda.Interaction.SearchAbout
import Agda.Interaction.Response hiding (Function, ExtendedLambda)
import qualified Agda.Interaction.Response as R
import qualified Agda.Interaction.BasicOps as B
import Agda.Interaction.Highlighting.Precise hiding (Error, Postulate, singleton)
import Agda.Interaction.Imports  ( Mode, pattern ScopeCheck, pattern TypeCheck )
import qualified Agda.Interaction.Imports as Imp
import Agda.Interaction.Highlighting.Generate

import Agda.Compiler.Backend

import Agda.Auto.Auto as Auto

import Agda.Utils.Either
import Agda.Utils.FileName
import Agda.Utils.Function
import Agda.Utils.Hash
import Agda.Utils.Lens
import qualified Agda.Utils.Maybe.Strict as Strict
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Pretty hiding (Mode)
import 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.Impossible

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

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

localStateCommandM :: CommandM a -> CommandM a
localStateCommandM :: forall a. CommandM a -> CommandM a
localStateCommandM CommandM a
m = do
  CommandState
cSt <- forall s (m :: * -> *). MonadState s m => m s
get
  TCState
tcSt <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
  a
x <- CommandM a
m
  forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcSt
  forall s (m :: * -> *). MonadState s m => s -> m ()
put CommandState
cSt
  forall (m :: * -> *) a. Monad m => a -> m a
return a
x

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

liftLocalState :: TCM a -> CommandM a
liftLocalState :: forall a. TCM a -> CommandM a
liftLocalState = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. TCM a -> TCM a
localTCState

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

revLift
    :: MonadState st m
    => (forall c . m c -> st -> k (c, st))      -- ^ run
    -> (forall b . k b -> m b)                  -- ^ lift
    -> (forall x . (m a -> k x) -> k x) -> m a  -- ^ reverse lift in double negative position
revLift :: forall st (m :: * -> *) (k :: * -> *) a.
MonadState st m =>
(forall c. m c -> st -> k (c, st))
-> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
revLift forall c. m c -> st -> k (c, st)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
    st
st <- forall s (m :: * -> *). MonadState s m => m s
get
    (a
a, st
st') <- forall b. k b -> m b
lift' forall a b. (a -> b) -> a -> b
$ forall x. (m a -> k x) -> k x
f (forall c. m c -> st -> k (c, st)
`run` st
st)
    forall s (m :: * -> *). MonadState s m => s -> m ()
put st
st'
    forall (m :: * -> *) a. Monad m => a -> m a
return a
a

revLiftTC
    :: MonadTCState m
    => (forall c . m c -> TCState -> k (c, TCState))  -- ^ run
    -> (forall b . k b -> m b)                        -- ^ lift
    -> (forall x . (m a -> k x) -> k x) -> m a        -- ^ reverse lift in double negative position
revLiftTC :: forall (m :: * -> *) (k :: * -> *) a.
MonadTCState m =>
(forall c. m c -> TCState -> k (c, TCState))
-> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
revLiftTC forall c. m c -> TCState -> k (c, TCState)
run forall b. k b -> m b
lift' forall x. (m a -> k x) -> k x
f = do
    TCState
st <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
    (a
a, TCState
st') <- forall b. k b -> m b
lift' forall a b. (a -> b) -> a -> b
$ forall x. (m a -> k x) -> k x
f (forall c. m c -> TCState -> k (c, TCState)
`run` TCState
st)
    forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st'
    forall (m :: * -> *) a. Monad m => a -> m a
return a
a

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

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

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

putResponse :: Response -> CommandM ()
putResponse :: Response -> CommandM ()
putResponse = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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 = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ CommandState
s ->
  CommandState
s { theInteractionPoints :: [InteractionId]
theInteractionPoints = [InteractionId] -> [InteractionId]
f (CommandState -> [InteractionId]
theInteractionPoints CommandState
s) }


-- * Operations for manipulating 'oldInteractionScopes'.

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

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

getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope :: InteractionId -> CommandM ScopeInfo
getOldInteractionScope InteractionId
ii = do
  Maybe ScopeInfo
ms <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InteractionId
ii forall b c a. (b -> c) -> (a -> b) -> a -> c
. CommandState -> OldInteractionScopes
oldInteractionScopes
  case Maybe ScopeInfo
ms of
    Maybe ScopeInfo
Nothing    -> forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail forall a b. (a -> b) -> a -> b
$ [Char]
"not an old interaction point: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show InteractionId
ii
    Just ScopeInfo
scope -> 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 forall a. a -> a
id (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 forall a b. (a -> b) -> a -> b
$ forall a. CommandM a -> CommandM a
wrap forall a b. (a -> b) -> a -> b
$ do
    TCState
oldState <- 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.
    CommandM ()
cmd forall a. CommandM a -> (TCErr -> CommandM a) -> CommandM a
`catchErr` \ TCErr
e -> do
      CommandM ()
onFail
      Maybe HighlightingMethod -> TCErr -> CommandM ()
handleErr 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
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
        PersistentTCState
newPersistentState <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PersistentTCState TCState
lensPersistentState
        forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
        Lens' PersistentTCState TCState
lensPersistentState forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` PersistentTCState
newPersistentState

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

    -- Handle every possible kind of error (#637), except for
    -- AsyncCancelled, which is used to abort Agda.
    handleNastyErrors :: CommandM () -> CommandM ()
    handleNastyErrors :: CommandM () -> CommandM ()
handleNastyErrors CommandM ()
m = forall a. (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
commandMToIO forall a b. (a -> b) -> a -> b
$ \ CommandM () -> IO x
toIO -> do
      let handle :: SomeException -> IO (Either AsyncCancelled x)
handle SomeException
e =
            forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
              CommandM () -> IO x
toIO (Maybe HighlightingMethod -> TCErr -> CommandM ()
handleErr (forall a. a -> Maybe a
Just HighlightingMethod
Direct) forall a b. (a -> b) -> a -> b
$
                        Range -> Doc -> TCErr
Exception forall a. Range' a
noRange forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ forall e. Exception e => e -> [Char]
E.displayException SomeException
e)

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

          generalHandler :: SomeException -> IO (Either AsyncCancelled x)
generalHandler (SomeException
e :: E.SomeException) = SomeException -> IO (Either AsyncCancelled x)
handle SomeException
e

      Either AsyncCancelled x
r <- ((forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CommandM () -> IO x
toIO CommandM ()
m) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` forall {m :: * -> *} {b}.
Monad m =>
AsyncCancelled -> m (Either AsyncCancelled b)
asyncHandler)
             forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` SomeException -> IO (Either AsyncCancelled x)
generalHandler
      case Either AsyncCancelled x
r of
        Right x
x -> forall (m :: * -> *) a. Monad m => a -> m a
return x
x
        Left AsyncCancelled
e  -> forall e a. Exception e => e -> IO a
E.throwIO AsyncCancelled
e

    -- Displays an error and instructs Emacs to jump to the site of the
    -- error. Because this function may switch the focus to another file
    -- the status information is also updated.
    handleErr :: Maybe HighlightingMethod -> TCErr -> CommandM ()
handleErr Maybe HighlightingMethod
method TCErr
e = do
        HighlightingInfoBuilder
unsolved <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ TCM HighlightingInfoBuilder
computeUnsolvedInfo
        HighlightingInfoBuilder
err     <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ TCErr -> TCM HighlightingInfoBuilder
errorHighlighting TCErr
e
        ModuleToSource
modFile <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' ModuleToSource TCState
stModuleToSource
        HighlightingMethod
method  <- case Maybe HighlightingMethod
method of
          Maybe HighlightingMethod
Nothing -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' HighlightingMethod TCEnv
eHighlightingMethod
          Just HighlightingMethod
m  -> forall (m :: * -> *) a. Monad m => a -> m a
return HighlightingMethod
m
        let info :: HighlightingInfo
info = forall a b. Convert a b => a -> b
convert forall a b. (a -> b) -> a -> b
$ HighlightingInfoBuilder
err forall a. Semigroup a => a -> a -> a
<> HighlightingInfoBuilder
unsolved
                     -- Errors take precedence over unsolved things.

        -- TODO: make a better predicate for this
        Bool
noError <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
e

        Bool
showImpl <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optShowImplicit forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
        Bool
showIrr <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optShowIrrelevant forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' PragmaOptions TCState
stPragmaOptions
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
noError forall a b. (a -> b) -> a -> b
$ do
          forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$
            [ DisplayInfo -> Response
Resp_DisplayInfo forall a b. (a -> b) -> a -> b
$ Info_Error -> DisplayInfo
Info_Error forall a b. (a -> b) -> a -> b
$ TCErr -> Info_Error
Info_GenericError TCErr
e ] forall a. [a] -> [a] -> [a]
++
            Range -> [Response]
tellEmacsToJumpToError (forall a. HasRange a => a -> Range
getRange TCErr
e) forall a. [a] -> [a] -> [a]
++
            [ HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> Response
Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
KeepHighlighting
                                    HighlightingMethod
method ModuleToSource
modFile ] forall a. [a] -> [a] -> [a]
++
            [ Status -> Response
Resp_Status forall a b. (a -> b) -> a -> b
$ Status { sChecked :: Bool
sChecked = Bool
False
                                   , sShowImplicitArguments :: Bool
sShowImplicitArguments = Bool
showImpl
                                   , sShowIrrelevantArguments :: Bool
sShowIrrelevantArguments = Bool
showIrr
                                   } ]
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (CommandLineOptions -> Bool
optExitOnError forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions) forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. AgdaError -> IO a
exitAgdaWith AgdaError
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 forall a. CommandM a -> CommandM a
inEmacs CommandM ()
onFail forall a b. (a -> b) -> a -> b
$ do
    AbsolutePath
currentAbs <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO AbsolutePath
absolute [Char]
current
    Maybe CurrentFile
cf  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
    Interaction' Range
cmd <- if Interaction' Range -> Bool
independent Interaction' Range
cmd then forall (m :: * -> *) a. Monad m => a -> m a
return Interaction' Range
cmd else do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. a -> Maybe a
Just AbsolutePath
currentAbs forall a. Eq a => a -> a -> Bool
/= (CurrentFile -> AbsolutePath
currentFilePath forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CurrentFile
cf)) forall a b. (a -> b) -> a -> b
$ do
        let mode :: Mode
mode = Mode
TypeCheck
        forall a.
[Char]
-> [[Char]]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' [Char]
current [] Bool
True Mode
mode forall a b. (a -> b) -> a -> b
$ \CheckResult
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      CurrentFile
cf <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case IOTCM
iotcm (forall a. a -> Maybe a
Just (CurrentFile -> TopLevelModuleName
currentFileModule CurrentFile
cf)) of
        IOTCM [Char]
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
cmd -> Interaction' Range
cmd

    forall a. CommandM a -> CommandM a
withCurrentFile forall a b. (a -> b) -> a -> b
$ Interaction' Range -> CommandM ()
interpret Interaction' Range
cmd

    Maybe CurrentFile
cf' <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Interaction' Range -> Bool
updateInteractionPointsAfter Interaction' Range
cmd
            Bool -> Bool -> Bool
&&
          forall a. a -> Maybe a
Just AbsolutePath
currentAbs forall a. Eq a => a -> a -> Bool
== (CurrentFile -> AbsolutePath
currentFilePath forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CurrentFile
cf')) forall a b. (a -> b) -> a -> b
$ do
        Response -> CommandM ()
putResponse forall b c a. (b -> c) -> (a -> b) -> a -> c
. [InteractionId] -> Response
Resp_InteractionPoints forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> [InteractionId]
theInteractionPoints

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

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

    -- If an independent command fails we should reset theCurrentFile (Issue853).
    onFail :: CommandM ()
onFail | Interaction' Range -> Bool
independent Interaction' Range
cmd = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ CommandState
s -> CommandState
s { theCurrentFile :: Maybe CurrentFile
theCurrentFile = forall a. Maybe a
Nothing }
           | Bool
otherwise       = 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
commandState <- forall s (m :: * -> *). MonadState s m => m s
get
  let q :: CommandQueue
q = CommandState -> CommandQueue
commandQueue CommandState
commandState
  (Integer
n, Command
cmd) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ forall a. TChan a -> STM a
readTChan (CommandQueue -> TChan (Integer, Command)
commands CommandQueue
q)
  case Command
cmd of
    Command
Done      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Command' a
Done
    Error [Char]
e   -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [Char] -> Command' a
Error [Char]
e)
    Command IOTCM
c -> do
      TCState
tcState <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
      TCEnv
tcEnv   <- forall (m :: * -> *). MonadTCEnv m => m TCEnv
askTC
      Either ((a, CommandState), TCState) Integer
result  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a b. IO a -> IO b -> IO (Either a b)
race
                   (forall (m :: * -> *) a.
MonadIO m =>
TCEnv -> TCState -> TCMT m a -> m (a, TCState)
runTCM TCEnv
tcEnv TCState
tcState forall a b. (a -> b) -> a -> b
$
                    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (IOTCM -> CommandM a
m IOTCM
c) CommandState
commandState)
                   (Integer -> CommandQueue -> IO Integer
waitForAbort Integer
n CommandQueue
q)
      case Either ((a, CommandState), TCState) Integer
result of
        Left ((a
x, CommandState
commandState'), TCState
tcState') -> do
          forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
tcState'
          forall s (m :: * -> *). MonadState s m => s -> m ()
put CommandState
commandState'
          case IOTCM
c forall a. Maybe a
Nothing of
            IOTCM [Char]
_ HighlightingLevel
_ HighlightingMethod
_ Interaction' Range
Cmd_exit -> do
              Response -> CommandM ()
putResponse Response
Resp_DoneExiting
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Command' a
Done
            IOTCM' Range
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Command' a
Command (forall a. a -> Maybe a
Just a
x))
        Right Integer
a -> do
          forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ CommandQueue -> Integer -> IO ()
popAbortedCommands CommandQueue
q Integer
a
          forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC forall a b. (a -> b) -> a -> b
$ TCState
initState
            { stPersistentState :: PersistentTCState
stPersistentState = TCState -> PersistentTCState
stPersistentState TCState
tcState
            , stPreScopeState :: PreScopeState
stPreScopeState   =
                (TCState -> PreScopeState
stPreScopeState TCState
initState)
                  { stPrePragmaOptions :: PragmaOptions
stPrePragmaOptions =
                      PreScopeState -> PragmaOptions
stPrePragmaOptions
                        (TCState -> PreScopeState
stPreScopeState TCState
tcState)
                  }
            }
          forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ (CommandQueue -> CommandState
initCommandState (CommandState -> CommandQueue
commandQueue CommandState
commandState))
            { optionsOnReload :: CommandLineOptions
optionsOnReload = CommandState -> CommandLineOptions
optionsOnReload CommandState
commandState
            }
          Response -> CommandM ()
putResponse Response
Resp_DoneAborting
          CommandM ()
displayStatus
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Command' a
Command 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
    forall a. STM a -> IO a
atomically forall a b. (a -> b) -> a -> b
$ do
      Maybe Integer
a <- forall a. TVar a -> STM a
readTVar (CommandQueue -> TVar (Maybe Integer)
abort CommandQueue
q)
      case Maybe Integer
a of
        Just Integer
a' | Integer
n forall a. Ord a => a -> a -> Bool
<= Integer
a' -> forall (m :: * -> *) a. Monad m => a -> m a
return Integer
a'
        Maybe Integer
_                 -> forall a. STM a
retry

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

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

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

initialiseCommandQueue
  :: IO Command
     -- ^ Returns the next command.
  -> IO CommandQueue
initialiseCommandQueue :: IO Command -> IO CommandQueue
initialiseCommandQueue IO Command
next = do
  TChan (Integer, Command)
commands <- forall a. IO (TChan a)
newTChanIO
  TVar (Maybe Integer)
abort    <- forall a. a -> IO (TVar a)
newTVarIO forall a. Maybe a
Nothing

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

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

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

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

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

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

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

updateInteractionPointsAfter :: Interaction -> Bool
updateInteractionPointsAfter :: Interaction' Range -> Bool
updateInteractionPointsAfter Cmd_load{}                          = Bool
True
updateInteractionPointsAfter Cmd_compile{}                       = Bool
True
updateInteractionPointsAfter Cmd_constraints{}                   = Bool
False
updateInteractionPointsAfter Cmd_metas{}                         = Bool
False
updateInteractionPointsAfter Cmd_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

interpret :: Interaction -> CommandM ()

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

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

interpret Interaction' Range
Cmd_constraints =
    DisplayInfo -> CommandM ()
display_info forall b c a. (b -> c) -> (a -> b) -> a -> c
. [OutputForm Expr Expr] -> DisplayInfo
Info_Constraints forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM [OutputForm Expr Expr]
B.getConstraints

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

interpret Interaction' Range
Cmd_no_metas = do
  [MetaId]
metas <- forall (m :: * -> *). ReadTCState m => m [MetaId]
getOpenMetas
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [MetaId]
metas) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Unsolved meta-variables"

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

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

interpret (Cmd_solveAll Rewrite
norm)        = Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals Rewrite
norm forall a. Maybe a
Nothing
interpret (Cmd_solveOne Rewrite
norm InteractionId
ii Range
_ [Char]
_) = Rewrite -> Maybe InteractionId -> CommandM ()
solveInstantiatedGoals Rewrite
norm' (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 [Char]
s) = do
  (Maybe CPUTime
time, Expr
expr) <- forall a. (Expr -> TCM a) -> [Char] -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel (Rewrite -> Expr -> TCM Expr
B.typeInCurrent Rewrite
norm) [Char]
s
  CommandState
state <- forall s (m :: * -> *). MonadState s m => m s
get
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ CommandState -> Maybe CPUTime -> Expr -> DisplayInfo
Info_InferredType CommandState
state Maybe CPUTime
time Expr
expr

interpret (Cmd_compute_toplevel ComputeMode
cmode [Char]
s) = do
  (Maybe CPUTime
time, Expr
expr) <- forall a. (Expr -> TCM a) -> [Char] -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM Expr
action (ComputeMode -> [Char] -> [Char]
B.computeWrapInput ComputeMode
cmode [Char]
s)
  CommandState
state <- forall s (m :: * -> *). MonadState s m => m s
get
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ CommandState -> ComputeMode -> Maybe CPUTime -> Expr -> DisplayInfo
Info_NormalForm CommandState
state ComputeMode
cmode Maybe CPUTime
time Expr
expr
    where
    action :: Expr -> TCM Expr
action = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
           forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if ComputeMode -> Bool
B.computeIgnoreAbstract ComputeMode
cmode then forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
           forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputeMode -> Expr -> TCM Expr
B.evalInCurrent ComputeMode
cmode
-- interpret (Cmd_compute_toplevel cmode s) =
--   parseAndDoAtToplevel action Info_NormalForm $ computeWrapInput cmode s
--   where
--   action = allowNonTerminatingReductions
--          . (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode)
--          . (B.showComputed cmode <=< B.evalInCurrent)


interpret (ShowImplicitArgs Bool
showImpl) = do
  CommandLineOptions
opts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  CommandLineOptions -> CommandM ()
setCommandLineOpts forall a b. (a -> b) -> a -> b
$
    CommandLineOptions
opts { optPragmaOptions :: PragmaOptions
optPragmaOptions =
             (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts) { optShowImplicit :: Bool
optShowImplicit = Bool
showImpl } }

interpret Interaction' Range
ToggleImplicitArgs = do
  CommandLineOptions
opts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let ps :: PragmaOptions
ps = CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts
  CommandLineOptions -> CommandM ()
setCommandLineOpts forall a b. (a -> b) -> a -> b
$
    CommandLineOptions
opts { optPragmaOptions :: PragmaOptions
optPragmaOptions =
             PragmaOptions
ps { optShowImplicit :: Bool
optShowImplicit = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optShowImplicit PragmaOptions
ps } }

interpret (ShowIrrelevantArgs Bool
showIrr) = do
  CommandLineOptions
opts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  CommandLineOptions -> CommandM ()
setCommandLineOpts forall a b. (a -> b) -> a -> b
$
    CommandLineOptions
opts { optPragmaOptions :: PragmaOptions
optPragmaOptions =
             (CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts) { optShowIrrelevant :: Bool
optShowIrrelevant = Bool
showIrr } }

interpret Interaction' Range
ToggleIrrelevantArgs = do
  CommandLineOptions
opts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  let ps :: PragmaOptions
ps = CommandLineOptions -> PragmaOptions
optPragmaOptions CommandLineOptions
opts
  CommandLineOptions -> CommandM ()
setCommandLineOpts forall a b. (a -> b) -> a -> b
$
    CommandLineOptions
opts { optPragmaOptions :: PragmaOptions
optPragmaOptions =
             PragmaOptions
ps { optShowIrrelevant :: Bool
optShowIrrelevant = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ PragmaOptions -> Bool
optShowIrrelevant PragmaOptions
ps } }

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

interpret (Cmd_tokenHighlighting [Char]
source Remove
remove) = do
  Maybe HighlightingInfo
info <- do HighlightingLevel
l <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
             if HighlightingLevel
l forall a. Eq a => a -> a -> Bool
== HighlightingLevel
None
               then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
               else do
                 AbsolutePath
source' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ([Char] -> IO AbsolutePath
absolute [Char]
source)
                 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCM HighlightingInfo
generateTokenInfo AbsolutePath
source')
                           forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ ->
                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
      forall e (m :: * -> *) a. MonadError e m => m a -> m () -> m a
`finally`
    case Remove
remove of
      Remove
Remove -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO ()
removeFile [Char]
source
      Remove
Keep   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
  case Maybe HighlightingInfo
info of
    Just HighlightingInfo
info' -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
RemoveHighlighting HighlightingInfo
info'
    Maybe HighlightingInfo
Nothing    -> forall (m :: * -> *) a. Monad m => a -> m a
return ()

interpret (Cmd_highlight InteractionId
ii Range
rng [Char]
s) = do
  HighlightingLevel
l <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HighlightingLevel
l forall a. Eq a => a -> a -> Bool
/= HighlightingLevel
None) forall a b. (a -> b) -> a -> b
$ do
    ScopeInfo
scope <- InteractionId -> CommandM ScopeInfo
getOldInteractionScope InteractionId
ii
    InteractionId -> CommandM ()
removeOldInteractionScope InteractionId
ii
    ExceptT Info_Error TCM () -> CommandM ()
handle forall a b. (a -> b) -> a -> b
$ do
      Expr
parsed <- forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
try (InteractionId -> Info_Error
Info_HighlightingParseError InteractionId
ii) forall a b. (a -> b) -> a -> b
$
             Range -> [Char] -> TCM Expr
B.parseExpr Range
rng [Char]
s
      Expr
expr <- forall a. Info_Error -> TCM a -> ExceptT Info_Error TCM a
try (InteractionId -> Info_Error
Info_HighlightingScopeCheckError InteractionId
ii) forall a b. (a -> b) -> a -> b
$
             forall c. ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
concreteToAbstract ScopeInfo
scope Expr
parsed
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
               Range -> [Char] -> TCM HighlightingInfo
generateTokenInfoFromString Range
rng [Char]
s
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Expr -> TCM ()
highlightExpr Expr
expr
  where
    handle :: ExceptT Info_Error TCM () -> CommandM ()
    handle :: ExceptT Info_Error TCM () -> CommandM ()
handle ExceptT Info_Error TCM ()
m = do
      Either Info_Error ()
res <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT ExceptT Info_Error TCM ()
m
      case Either Info_Error ()
res of
        Left Info_Error
err -> DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ Info_Error -> DisplayInfo
Info_Error Info_Error
err
        Right ()
_ -> 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 = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ do
      (forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft (forall a b. a -> b -> a
const Info_Error
err) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. TCM a -> TCM (Either TCErr a)
freshTCM TCM a
m) forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 [Char]
s) = UseForce
-> InteractionId -> Range -> [Char] -> GiveRefine -> CommandM ()
give_gen UseForce
force InteractionId
ii Range
rng [Char]
s GiveRefine
Give
interpret (Cmd_refine InteractionId
ii Range
rng [Char]
s) = UseForce
-> InteractionId -> Range -> [Char] -> GiveRefine -> CommandM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng [Char]
s GiveRefine
Refine

interpret (Cmd_intro Bool
pmLambda InteractionId
ii Range
rng [Char]
_) = do
  [[Char]]
ss <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Bool -> InteractionId -> TCM [[Char]]
B.introTactic Bool
pmLambda InteractionId
ii
  forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT (forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) forall a b. (a -> b) -> a -> b
$ case [[Char]]
ss of
    []    -> do
      DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ DisplayInfo
Info_Intro_NotFound
    [[Char]
s]   -> UseForce
-> InteractionId -> Range -> [Char] -> GiveRefine -> CommandM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng [Char]
s GiveRefine
Intro
    [Char]
_:[Char]
_:[[Char]]
_ -> do
      DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ [[Char]] -> DisplayInfo
Info_Intro_ConstructorUnknown [[Char]]
ss

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

interpret (Cmd_autoOne InteractionId
ii Range
rng [Char]
hint) = do
  -- Andreas, 2014-07-05 Issue 1226:
  -- Save the state to have access to even those interaction ids
  -- that Auto solves (since Auto gives the solution right away).
  TCState
st <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
  (Maybe CPUTime
time , AutoResult
res) <- forall a. CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *).
MonadTCM tcm =>
InteractionId -> Range -> [Char] -> tcm AutoResult
Auto.auto InteractionId
ii Range
rng [Char]
hint
  case AutoResult -> AutoProgress
autoProgress AutoResult
res of
   Solutions [(InteractionId, [Char])]
sols -> do
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"auto" Int
10 forall a b. (a -> b) -> a -> b
$ [Char]
"Auto produced the following solutions " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [(InteractionId, [Char])]
sols
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(InteractionId, [Char])]
sols forall a b. (a -> b) -> a -> b
$ \(InteractionId
ii', [Char]
sol) -> do
      -- Andreas, 2014-07-05 Issue 1226:
      -- For highlighting, Resp_GiveAction needs to access
      -- the @oldInteractionScope@s of the interaction points solved by Auto.
      -- We dig them out from the state before Auto was invoked.
      InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope InteractionId
ii' forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. TCM a -> CommandM a
liftLocalState (forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii')
      -- Andreas, 2014-07-07: NOT TRUE:
      -- -- Andreas, 2014-07-05: The following should be obsolete,
      -- -- as Auto has removed the interaction points already:
      -- modifyTheInteractionPoints $ filter (/= ii)
      Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
Resp_GiveAction InteractionId
ii' forall a b. (a -> b) -> a -> b
$ [Char] -> GiveResult
Give_String [Char]
sol
    -- Andreas, 2014-07-07: Remove the interaction points in one go.
    ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints (forall a. Eq a => [a] -> [a] -> [a]
List.\\ (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(InteractionId, [Char])]
sols))
    case AutoResult -> Maybe [Char]
autoMessage AutoResult
res of
     Maybe [Char]
Nothing  -> Interaction' Range -> CommandM ()
interpret forall a b. (a -> b) -> a -> b
$ forall range. Rewrite -> Interaction' range
Cmd_metas Rewrite
AsIs
     Just [Char]
msg -> DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ [Char] -> DisplayInfo
Info_Auto [Char]
msg
   FunClauses [[Char]]
cs -> do
    case AutoResult -> Maybe [Char]
autoMessage AutoResult
res of
     Maybe [Char]
Nothing  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
     Just [Char]
msg -> DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ [Char] -> DisplayInfo
Info_Auto [Char]
msg
    Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$ InteractionId -> MakeCaseVariant -> [[Char]] -> Response
Resp_MakeCase InteractionId
ii MakeCaseVariant
R.Function [[Char]]
cs
   Refinement [Char]
s -> UseForce
-> InteractionId -> Range -> [Char] -> GiveRefine -> CommandM ()
give_gen UseForce
WithoutForce InteractionId
ii Range
rng [Char]
s GiveRefine
Refine
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return ()) (DisplayInfo -> CommandM ()
display_info forall b c a. (b -> c) -> (a -> b) -> a -> c
. CPUTime -> DisplayInfo
Info_Time) Maybe CPUTime
time

interpret Interaction' Range
Cmd_autoAll = do
  [InteractionId]
iis <- forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [InteractionId]
iis) forall a b. (a -> b) -> a -> b
$ do
    let time :: Int
time = Int
1000 forall a. Integral a => a -> a -> a
`div` forall (t :: * -> *) a. Foldable t => t a -> Int
length [InteractionId]
iis
    TCState
st <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
    [[InteractionId]]
solved <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [InteractionId]
iis forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii -> do
      Range
rng <- forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
ii
      AutoResult
res <- forall (tcm :: * -> *).
MonadTCM tcm =>
InteractionId -> Range -> [Char] -> tcm AutoResult
Auto.auto InteractionId
ii Range
rng ([Char]
"-t " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
time forall a. [a] -> [a] -> [a]
++ [Char]
"ms")
      case AutoResult -> AutoProgress
autoProgress AutoResult
res of
        Solutions [(InteractionId, [Char])]
sols -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(InteractionId, [Char])]
sols forall a b. (a -> b) -> a -> b
$ \ (InteractionId
jj, [Char]
s) -> do
            ScopeInfo
oldInteractionScope <- forall a. TCM a -> CommandM a
liftLocalState (forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
st forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
jj)
            InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope InteractionId
jj ScopeInfo
oldInteractionScope
            Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
Resp_GiveAction InteractionId
ii forall a b. (a -> b) -> a -> b
$ [Char] -> GiveResult
Give_String [Char]
s
            forall (m :: * -> *) a. Monad m => a -> m a
return InteractionId
jj
        AutoProgress
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints (forall a. Eq a => [a] -> [a] -> [a]
List.\\ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[InteractionId]]
solved)

interpret (Cmd_context Rewrite
norm InteractionId
ii Range
_ [Char]
_) =
  DisplayInfo -> CommandM ()
display_info forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> [ResponseContextEntry] -> DisplayInfo
Info_Context InteractionId
ii forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. TCM a -> CommandM a
liftLocalState (Rewrite -> InteractionId -> TCM [ResponseContextEntry]
B.getResponseContext Rewrite
norm InteractionId
ii)

interpret (Cmd_helper_function Rewrite
norm InteractionId
ii Range
rng [Char]
s) = do
  -- Create type of application of new helper function that would solve the goal.
  OutputConstraint' Expr Expr
helperType <- forall a. TCM a -> CommandM a
liftLocalState forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ Rewrite
-> InteractionId
-> Range
-> [Char]
-> TCMT IO (OutputConstraint' Expr Expr)
B.metaHelperType Rewrite
norm InteractionId
ii Range
rng [Char]
s
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ InteractionId -> GoalDisplayInfo -> DisplayInfo
Info_GoalSpecific InteractionId
ii (OutputConstraint' Expr Expr -> GoalDisplayInfo
Goal_HelperFunction OutputConstraint' Expr Expr
helperType)

interpret (Cmd_infer Rewrite
norm InteractionId
ii Range
rng [Char]
s) = do
  Expr
expr <- forall a. TCM a -> CommandM a
liftLocalState forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ InteractionId -> Rewrite -> Expr -> TCM Expr
B.typeInMeta InteractionId
ii Rewrite
norm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> Range -> [Char] -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng [Char]
s
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ InteractionId -> GoalDisplayInfo -> DisplayInfo
Info_GoalSpecific InteractionId
ii (Expr -> GoalDisplayInfo
Goal_InferredType Expr
expr)

interpret (Cmd_goal_type Rewrite
norm InteractionId
ii Range
_ [Char]
_) =
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ InteractionId -> GoalDisplayInfo -> DisplayInfo
Info_GoalSpecific InteractionId
ii (Rewrite -> GoalDisplayInfo
Goal_CurrentGoal Rewrite
norm)

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

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

interpret (Cmd_goal_type_context_infer Rewrite
norm InteractionId
ii Range
rng [Char]
s) = do
  -- In case of the empty expression to type, don't fail with
  -- a stupid parse error, but just fall back to
  -- Cmd_goal_type_context.
  GoalTypeAux
aux <- if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
Char.isSpace [Char]
s
            then forall (m :: * -> *) a. Monad m => a -> m a
return GoalTypeAux
GoalOnly
            else do
              Expr
typ <- forall a. TCM a -> CommandM a
liftLocalState
                    forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii
                    forall a b. (a -> b) -> a -> b
$ InteractionId -> Rewrite -> Expr -> TCM Expr
B.typeInMeta InteractionId
ii Rewrite
norm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> Range -> [Char] -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng [Char]
s
              forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> GoalTypeAux
GoalAndHave Expr
typ)
  GoalTypeAux
-> Rewrite -> InteractionId -> Range -> [Char] -> CommandM ()
cmd_goal_type_context_and GoalTypeAux
aux Rewrite
norm InteractionId
ii Range
rng [Char]
s

interpret (Cmd_goal_type_context_check Rewrite
norm InteractionId
ii Range
rng [Char]
s) = do
  Term
term <- forall a. TCM a -> CommandM a
liftLocalState forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ do
    Expr
expr <- InteractionId -> Range -> [Char] -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng [Char]
s
    OutputConstraint Expr InteractionId
goal <- Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
B.typeOfMeta Rewrite
AsIs InteractionId
ii
    Term
term <- case OutputConstraint Expr InteractionId
goal of
      OfType InteractionId
_ Expr
ty -> Expr -> Type -> TCMT IO Term
checkExpr Expr
expr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> TCM Type
isType_ Expr
ty
      OutputConstraint Expr InteractionId
_           -> forall a. HasCallStack => a
__IMPOSSIBLE__
    forall t.
(Reduce t, Simplify t, Instantiate t, Normalise t) =>
Rewrite -> t -> TCM t
B.normalForm Rewrite
norm Term
term
  GoalTypeAux
-> Rewrite -> InteractionId -> Range -> [Char] -> CommandM ()
cmd_goal_type_context_and (Term -> GoalTypeAux
GoalAndElaboration Term
term) Rewrite
norm InteractionId
ii Range
rng [Char]
s

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

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

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

interpret (Cmd_make_case InteractionId
ii Range
rng [Char]
s) = do
  (QName
f, CaseContext
casectxt, [Clause]
cs) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ InteractionId
-> Range -> [Char] -> TCM (QName, CaseContext, [Clause])
makeCase InteractionId
ii Range
rng [Char]
s
  forall a. (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
liftCommandMT (forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii) forall a b. (a -> b) -> a -> b
$ do
    Telescope
tel <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection (QName -> ModuleName
qnameModule QName
f) -- don't shadow the names in this telescope
    UnicodeOrAscii
unicode <- forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
getsTC forall a b. (a -> b) -> a -> b
$ PragmaOptions -> UnicodeOrAscii
optUseUnicode forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensPragmaOptions a => a -> PragmaOptions
getPragmaOptions
    [Doc]
pcs      :: [Doc]      <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cs
    let [[Char]]
pcs' :: [String]    = forall a b. (a -> b) -> [a] -> [b]
List.map (UnicodeOrAscii -> CaseContext -> [Char] -> [Char]
extlam_dropName UnicodeOrAscii
unicode CaseContext
casectxt forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
decorate) [Doc]
pcs
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"interaction.case" Int
60 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
      [ TCMT IO Doc
"InteractionTop.Cmd_make_case"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
        [ TCMT IO Doc
"cs   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cs)
        , TCMT IO Doc
"pcs  = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. Monad m => a -> m a
return [Doc]
pcs)
        , TCMT IO Doc
"pcs' = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat (forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text [[Char]]
pcs')
        ]
      ]
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"interaction.case" Int
90 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
      [ TCMT IO Doc
"InteractionTop.Cmd_make_case"
      , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest Int
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat
        [ TCMT IO Doc
"cs   = " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text (forall a. Show a => a -> [Char]
show [Clause]
cs)
        ]
      ]
    Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$ InteractionId -> MakeCaseVariant -> [[Char]] -> Response
Resp_MakeCase InteractionId
ii (CaseContext -> MakeCaseVariant
makeCaseVariant CaseContext
casectxt) [[Char]]
pcs'
  where
    decorate :: Doc -> [Char]
decorate = Style -> Doc -> [Char]
renderStyle (Style
style { mode :: Mode
mode = Mode
OneLineMode })

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

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

interpret (Cmd_compute ComputeMode
cmode InteractionId
ii Range
rng [Char]
s) = do
  Expr
expr <- forall a. TCM a -> CommandM a
liftLocalState forall a b. (a -> b) -> a -> b
$ do
    Expr
e <- InteractionId -> Range -> [Char] -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng forall a b. (a -> b) -> a -> b
$ ComputeMode -> [Char] -> [Char]
B.computeWrapInput ComputeMode
cmode [Char]
s
    forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii forall a b. (a -> b) -> a -> b
$ forall a. Bool -> (a -> a) -> a -> a
applyWhen (ComputeMode -> Bool
B.computeIgnoreAbstract ComputeMode
cmode) forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ ComputeMode -> Expr -> TCM Expr
B.evalInCurrent ComputeMode
cmode Expr
e
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ InteractionId -> GoalDisplayInfo -> DisplayInfo
Info_GoalSpecific InteractionId
ii (ComputeMode -> Expr -> GoalDisplayInfo
Goal_NormalForm ComputeMode
cmode Expr
expr)

interpret Interaction' Range
Cmd_show_version = DisplayInfo -> CommandM ()
display_info DisplayInfo
Info_Version

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

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

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

cmd_load'
  :: FilePath  -- ^ File to load into interaction.
  -> [String]  -- ^ Arguments to Agda for loading this file
  -> Bool      -- ^ Allow unsolved meta-variables?
  -> Mode      -- ^ Full type-checking, or only scope-checking?
  -> (CheckResult -> CommandM a)
               -- ^ Continuation after successful loading.
  -> CommandM a
cmd_load' :: forall a.
[Char]
-> [[Char]]
-> Bool
-> Mode
-> (CheckResult -> CommandM a)
-> CommandM a
cmd_load' [Char]
file [[Char]]
argv Bool
unsolvedOK Mode
mode CheckResult -> CommandM a
cmd = do
    AbsolutePath
fp <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO AbsolutePath
absolute [Char]
file
    Bool
ex <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO Bool
doesFileExist forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath AbsolutePath
fp
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
ex forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
      [Char]
"The file " forall a. [a] -> [a] -> [a]
++ [Char]
file forall a. [a] -> [a] -> [a]
++ [Char]
" was not found."

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

    ClockTime
t <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO ClockTime
getModificationTime [Char]
file

    -- 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.
    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
Resp_ClearRunningInfo

    -- Remove any prior syntax highlighting.
    Response -> CommandM ()
putResponse (TokenBased -> Response
Resp_ClearHighlighting TokenBased
NotOnlyTokenBased)

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

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

    -- All options are reset when a file is reloaded, including the
    -- choice of whether or not to display implicit arguments.
    CommandLineOptions
opts0 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> CommandLineOptions
optionsOnReload
    [Backend]
backends <- forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' [Backend] TCState
stBackends
    Either [Char] ([Backend], CommandLineOptions)
z <- forall (m :: * -> *) opts.
Monad m =>
OptM opts -> m (Either [Char] opts)
runOptM forall a b. (a -> b) -> a -> b
$ [Backend]
-> [[Char]]
-> CommandLineOptions
-> OptM ([Backend], CommandLineOptions)
parseBackendOptions [Backend]
backends [[Char]]
argv CommandLineOptions
opts0
    case Either [Char] ([Backend], CommandLineOptions)
z of
      Left [Char]
err   -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
err
      Right ([Backend]
_, CommandLineOptions
opts) -> do
        CommandLineOptions
opts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ CommandLineOptions -> TCM CommandLineOptions
addTrustedExecutables CommandLineOptions
opts
        let update :: PragmaOptions -> PragmaOptions
update PragmaOptions
o = PragmaOptions
o { optAllowUnsolved :: Bool
optAllowUnsolved = Bool
unsolvedOK Bool -> Bool -> Bool
&& PragmaOptions -> Bool
optAllowUnsolved PragmaOptions
o}
            root :: AbsolutePath
root     = AbsolutePath -> TopLevelModuleName -> AbsolutePath
projectRoot AbsolutePath
fp forall a b. (a -> b) -> a -> b
$ Source -> TopLevelModuleName
Imp.srcModuleName Source
src
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ AbsolutePath -> CommandLineOptions -> TCM ()
TCM.setCommandLineOptions' AbsolutePath
root forall a b. (a -> b) -> a -> b
$ forall a.
LensPragmaOptions a =>
(PragmaOptions -> PragmaOptions) -> a -> a
mapPragmaOptions PragmaOptions -> PragmaOptions
update CommandLineOptions
opts

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

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

    -- The module type checked. If the file was not changed while the
    -- type checker was running then the interaction points and the
    -- "current file" are stored.
    ClockTime
t' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO ClockTime
getModificationTime [Char]
file
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ClockTime
t forall a. Eq a => a -> a -> Bool
== ClockTime
t') forall a b. (a -> b) -> a -> b
$ do
      [InteractionId]
is <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
[InteractionId] -> m [InteractionId]
sortInteractionPoints forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CommandState
st -> CommandState
st { theInteractionPoints :: [InteractionId]
theInteractionPoints = [InteractionId]
is
                         , theCurrentFile :: Maybe CurrentFile
theCurrentFile       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CurrentFile
                             { currentFilePath :: AbsolutePath
currentFilePath   = AbsolutePath
fp
                             , currentFileModule :: TopLevelModuleName
currentFileModule = Source -> TopLevelModuleName
Imp.srcModuleName Source
src
                             , currentFileArgs :: [[Char]]
currentFileArgs   = [[Char]]
argv
                             , currentFileStamp :: ClockTime
currentFileStamp  = ClockTime
t
                             }
                         }

    CheckResult -> CommandM a
cmd CheckResult
ok

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

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

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

data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite
  deriving (GiveRefine -> GiveRefine -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GiveRefine -> GiveRefine -> Bool
$c/= :: GiveRefine -> GiveRefine -> Bool
== :: GiveRefine -> GiveRefine -> Bool
$c== :: GiveRefine -> GiveRefine -> Bool
Eq, Int -> GiveRefine -> [Char] -> [Char]
[GiveRefine] -> [Char] -> [Char]
GiveRefine -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
showList :: [GiveRefine] -> [Char] -> [Char]
$cshowList :: [GiveRefine] -> [Char] -> [Char]
show :: GiveRefine -> [Char]
$cshow :: GiveRefine -> [Char]
showsPrec :: Int -> GiveRefine -> [Char] -> [Char]
$cshowsPrec :: Int -> GiveRefine -> [Char] -> [Char]
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 -> [Char] -> GiveRefine -> CommandM ()
give_gen UseForce
force InteractionId
ii Range
rng [Char]
s0 GiveRefine
giveRefine = do
  let s :: [Char]
s = [Char] -> [Char]
trim [Char]
s0
  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
20 forall a b. (a -> b) -> a -> b
$ [Char]
"give_gen  " forall a. [a] -> [a] -> [a]
++ [Char]
s
  -- Andreas, 2015-02-26 if string is empty do nothing rather
  -- than giving a parse error.
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Null a => a -> Bool
null [Char]
s) forall a b. (a -> b) -> a -> b
$ do
    let give_ref :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give_ref =
          case GiveRefine
giveRefine of
            GiveRefine
Give               -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.give
            GiveRefine
Refine             -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.refine
            GiveRefine
Intro              -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.refine
            ElaborateGive Rewrite
norm -> Rewrite
-> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
B.elaborate_give Rewrite
norm
    -- save scope of the interaction point (for printing the given expr. later)
    ScopeInfo
scope     <- forall (m :: * -> *).
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
 MonadTCEnv m) =>
InteractionId -> m ScopeInfo
getInteractionScope InteractionId
ii
    -- parse string and "give", obtaining an abstract expression
    -- and newly created interaction points
    (Maybe CPUTime
time, (Expr
ae, Expr
ae0, [InteractionId]
iis)) <- forall a. CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed forall a b. (a -> b) -> a -> b
$ do
        -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential
        -- new interaction points introduced by the give.
        forall (m :: * -> *).
MonadInteractionPoints m =>
InteractionId -> m ()
removeInteractionPoint InteractionId
ii
        [InteractionId]
mis  <- forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"interaction points before = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [InteractionId]
mis
        Expr
given <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ InteractionId -> Range -> [Char] -> TCM Expr
B.parseExprIn InteractionId
ii Range
rng [Char]
s
        Expr
ae    <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
give_ref UseForce
force InteractionId
ii forall a. Maybe a
Nothing Expr
given
        [InteractionId]
mis' <- forall (m :: * -> *). ReadTCState m => m [InteractionId]
getInteractionPoints
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"interaction points after = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [InteractionId]
mis'
        forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
ae, Expr
given, [InteractionId]
mis' forall a. Eq a => [a] -> [a] -> [a]
List.\\ [InteractionId]
mis)
    -- favonia: backup the old scope for highlighting
    InteractionId -> ScopeInfo -> CommandM ()
insertOldInteractionScope InteractionId
ii ScopeInfo
scope
    -- sort the new interaction points and put them into the state
    -- in replacement of the old interaction point
    [InteractionId]
iis' <- forall (m :: * -> *).
(MonadInteractionPoints m, MonadError TCErr m, MonadFail m) =>
[InteractionId] -> m [InteractionId]
sortInteractionPoints [InteractionId]
iis
    ([InteractionId] -> [InteractionId]) -> CommandM ()
modifyTheInteractionPoints forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *} {b}.
(Foldable t, Eq b) =>
b -> [b] -> t b -> [b]
replace InteractionId
ii [InteractionId]
iis'
    -- print abstract expr
    Expr
ce        <- forall a (m :: * -> *).
(ToConcrete a, MonadAbsToCon m) =>
ScopeInfo -> a -> m (ConOfAbs a)
abstractToConcreteScope ScopeInfo
scope Expr
ae
    forall a (m :: * -> *).
(ReportS a, MonadDebug m) =>
[Char] -> Int -> a -> m ()
reportS [Char]
"interaction.give" Int
30
      [ [Char]
"ce = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Expr
ce
      , [Char]
"scopePrecedence = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (ScopeInfo
scope forall o i. o -> Lens' i o -> i
^. Lens' PrecedenceStack ScopeInfo
scopePrecedence)
      ]
    -- if the command was @Give@, use the literal user input;
    -- Andreas, 2014-01-15, see issue 1020:
    -- Refine could solve a goal by introducing the sole constructor
    -- without arguments.  Then there are no interaction metas, but
    -- we still cannot just `give' the user string (which may be empty).
    -- WRONG: also, if no interaction metas were created by @Refine@
    -- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange
    -- Ulf, 2015-03-30, if we're doing intro we can't do literal give since
    -- there is nothing in the hole (issue 1892).
    let literally :: Bool
literally = (GiveRefine
giveRefine forall a. Eq a => a -> a -> Bool
== GiveRefine
Give Bool -> Bool -> Bool
|| GiveRefine
giveRefine forall a. Eq a => a -> a -> Bool
== GiveRefine
Refine) Bool -> Bool -> Bool
&& Expr
ae forall a. Eq a => a -> a -> Bool
== Expr
ae0 Bool -> Bool -> Bool
&& Range
rng forall a. Eq a => a -> a -> Bool
/= 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.
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
literally forall a b. (a -> b) -> a -> b
$ do
      HighlightingLevel
l <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> HighlightingLevel
envHighlightingLevel
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HighlightingLevel
l forall a. Eq a => a -> a -> Bool
/= HighlightingLevel
None) forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadTrace m =>
RemoveTokenBasedHighlighting -> HighlightingInfo -> m ()
printHighlightingInfo RemoveTokenBasedHighlighting
KeepHighlighting forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          Range -> [Char] -> TCM HighlightingInfo
generateTokenInfoFromString Range
rng [Char]
s
        Expr -> TCM ()
highlightExpr Expr
ae
    Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$ InteractionId -> GiveResult -> Response
Resp_GiveAction InteractionId
ii forall a b. (a -> b) -> a -> b
$ Bool -> Expr -> GiveResult
mkNewTxt Bool
literally Expr
ce
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"putResponse GiveAction passed"
    -- display new goal set (if not measuring time)
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Interaction' Range -> CommandM ()
interpret forall a b. (a -> b) -> a -> b
$ forall range. Rewrite -> Interaction' range
Cmd_metas Rewrite
AsIs) (DisplayInfo -> CommandM ()
display_info forall b c a. (b -> c) -> (a -> b) -> a -> c
. CPUTime -> DisplayInfo
Info_Time) Maybe CPUTime
time
    forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"interaction.give" Int
30 forall a b. (a -> b) -> a -> b
$ [Char]
"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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ b
y -> if b
y 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        = [Char] -> GiveResult
Give_String forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow Expr
ce

highlightExpr :: A.Expr -> TCM ()
highlightExpr :: Expr -> TCM ()
highlightExpr Expr
e =
  forall (m :: * -> *) a.
MonadTCEnv m =>
(TCEnv -> TCEnv) -> m a -> m a
localTC (\TCEnv
st -> TCEnv
st { envImportPath :: [TopLevelModuleName]
envImportPath         = []
                     , envHighlightingLevel :: HighlightingLevel
envHighlightingLevel  = HighlightingLevel
NonInteractive
                     , envHighlightingMethod :: HighlightingMethod
envHighlightingMethod = HighlightingMethod
Direct }) forall a b. (a -> b) -> a -> b
$
    Declaration -> Level -> Bool -> TCM ()
generateAndPrintSyntaxInfo Declaration
decl Level
Full Bool
True
  where
    dummy :: Name
dummy = forall a. MkName a => NameId -> a -> Name
mkName_ (Hash -> ModuleNameHash -> NameId
NameId Hash
0 ModuleNameHash
noModuleNameHash) ([Char]
"dummy" :: String)
    info :: DefInfo' Expr
info  = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete Name
dummy) Fixity'
noFixity' Access
PublicAccess IsAbstract
ConcreteDef (forall a. HasRange a => a -> Range
getRange Expr
e)
    decl :: Declaration
decl  = KindOfName
-> DefInfo' Expr
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
OtherDefName DefInfo' Expr
info ArgInfo
defaultArgInfo forall a. Maybe a
Nothing (List1 Name -> QName
qnameFromList forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton Name
dummy) Expr
e

-- | Sorts interaction points based on their ranges.

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

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

cmd_goal_type_context_and :: GoalTypeAux -> Rewrite -> InteractionId -> Range ->
                             String -> CommandM ()
cmd_goal_type_context_and :: GoalTypeAux
-> Rewrite -> InteractionId -> Range -> [Char] -> CommandM ()
cmd_goal_type_context_and GoalTypeAux
aux Rewrite
norm InteractionId
ii Range
_ [Char]
_ = do
  [ResponseContextEntry]
ctx <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> TCM [ResponseContextEntry]
B.getResponseContext Rewrite
norm InteractionId
ii
  [OutputForm Expr Expr]
constr <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
ii forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
B.getConstraintsMentioning Rewrite
norm
  [IPBoundary' Expr]
boundary <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Rewrite -> InteractionId -> TCM [IPBoundary' Expr]
B.getIPBoundary Rewrite
norm InteractionId
ii
  DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ InteractionId -> GoalDisplayInfo -> DisplayInfo
Info_GoalSpecific InteractionId
ii (Rewrite
-> GoalTypeAux
-> [ResponseContextEntry]
-> [IPBoundary' Expr]
-> [OutputForm Expr Expr]
-> GoalDisplayInfo
Goal_GoalType Rewrite
norm GoalTypeAux
aux [ResponseContextEntry]
ctx [IPBoundary' Expr]
boundary [OutputForm Expr Expr]
constr)

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

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

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

searchAbout :: Rewrite -> Range -> String -> CommandM ()
searchAbout :: Rewrite -> Range -> [Char] -> CommandM ()
searchAbout Rewrite
norm Range
rg [Char]
names = do
  forall (m :: * -> *) a.
(Monad m, Null a) =>
a -> (a -> m ()) -> m ()
unlessNull ([Char] -> [Char]
trim [Char]
names) forall a b. (a -> b) -> a -> b
$ \ [Char]
trimmedNames -> do
    [(Name, Type)]
hits <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Rewrite -> Range -> [Char] -> ScopeM [(Name, Type)]
findMentions Rewrite
norm Range
rg [Char]
trimmedNames
    DisplayInfo -> CommandM ()
display_info forall a b. (a -> b) -> a -> b
$ [(Name, Type)] -> [Char] -> DisplayInfo
Info_SearchAbout [(Name, Type)]
hits [Char]
trimmedNames

-- | Explain why something is in scope.

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

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

setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts :: CommandLineOptions -> CommandM ()
setCommandLineOpts CommandLineOptions
opts = do
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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
  Maybe CurrentFile
cf       <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CommandState -> Maybe CurrentFile
theCurrentFile
  Bool
showImpl <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m Bool
showImplicitArguments
  Bool
showIrr  <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m Bool
showIrrelevantArguments

  -- Check if the file was successfully type checked, and has not
  -- changed since. Note: This code does not check if any dependencies
  -- have changed, and uses a time stamp to check for changes.
  Bool
checked  <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ case Maybe CurrentFile
cf of
    Maybe CurrentFile
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just CurrentFile
f  -> do
      ClockTime
t <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO ClockTime
getModificationTime forall a b. (a -> b) -> a -> b
$ AbsolutePath -> [Char]
filePath (CurrentFile -> AbsolutePath
currentFilePath CurrentFile
f)
      if CurrentFile -> ClockTime
currentFileStamp CurrentFile
f forall a. Eq a => a -> a -> Bool
== ClockTime
t
        then
          forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall a. Null a => a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleInfo -> [TCWarning]
miWarnings) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          forall (m :: * -> *).
ReadTCState m =>
TopLevelModuleName -> m (Maybe ModuleInfo)
getVisitedModule (CurrentFile -> TopLevelModuleName
currentFileModule CurrentFile
f)
        else
            forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Status { sShowImplicitArguments :: Bool
sShowImplicitArguments   = Bool
showImpl,
                    sShowIrrelevantArguments :: Bool
sShowIrrelevantArguments = Bool
showIrr,
                    sChecked :: Bool
sChecked                 = Bool
checked }

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

displayStatus :: CommandM ()
displayStatus :: CommandM ()
displayStatus =
  Response -> CommandM ()
putResponse forall b c a. (b -> c) -> (a -> b) -> a -> c
. Status -> Response
Resp_Status  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 -> CommandM ()
display_info DisplayInfo
info = do
  CommandM ()
displayStatus
  Response -> CommandM ()
putResponse forall a b. (a -> b) -> a -> b
$ DisplayInfo -> Response
Resp_DisplayInfo DisplayInfo
info

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

parseAndDoAtToplevel
  :: (A.Expr -> TCM a)
     -- ^ The command to perform.
  -> String
     -- ^ The expression to parse.
  -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel :: forall a. (Expr -> TCM a) -> [Char] -> CommandM (Maybe CPUTime, a)
parseAndDoAtToplevel Expr -> TCM a
cmd [Char]
s = do
  forall a. CommandM a -> CommandM a
localStateCommandM forall a b. (a -> b) -> a -> b
$ do
    (Expr
e, CohesionAttributes
coh) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. PM a -> TCM a
runPM forall a b. (a -> b) -> a -> b
$ forall a. Parser a -> [Char] -> PM (a, CohesionAttributes)
parse Parser Expr
exprParser [Char]
s
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ CohesionAttributes -> TCM ()
checkCohesionAttributes CohesionAttributes
coh
    forall a. CommandM a -> CommandM (Maybe CPUTime, a)
maybeTimed forall a b. (a -> b) -> a -> b
$ forall a. CommandM a -> CommandM a
atTopLevel forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
      Expr -> TCM a
cmd forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall c. ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract_ Expr
e

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

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

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

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

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