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

    module Agda.Interaction.Base where

    import           Control.Applicative          ( liftA3 )
    import           Control.Concurrent.STM.TChan
    import           Control.Concurrent.STM.TVar
    import           Control.Monad                ( mplus, liftM2, liftM4 )
    import           Control.Monad.Except
    import           Control.Monad.Identity
    import           Control.Monad.State

    import qualified Data.List                    as List
    import           Data.Map                     (Map)
    import qualified Data.Map                     as Map
    import           Data.Maybe                   (listToMaybe)
    import qualified Data.Text                    as T

    import Agda.TypeChecking.Monad.Base.Types
      (HighlightingLevel, HighlightingMethod, Comparison, Polarity)

    import           Agda.Syntax.Abstract         (QName)
    import           Agda.Syntax.Common           (BackendName, InteractionId (..), Modality)
    import           Agda.Syntax.Internal         (ProblemId, Blocker)
    import           Agda.Syntax.Position
    import           Agda.Syntax.Scope.Base       (ScopeInfo)
    import           Agda.Syntax.TopLevelModuleName

    import           Agda.Interaction.Options     (CommandLineOptions,
                                                   defaultOptions)

    import           Agda.Utils.FileName          (AbsolutePath, mkAbsolute)
    import           Agda.Syntax.Common.Pretty            (Pretty(..), prettyShow, text)
    import           Agda.Utils.Time              (ClockTime)

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

    -- | Auxiliary state of an interactive computation.

    data CommandState = CommandState
      { CommandState -> [InteractionId]
    theInteractionPoints :: [InteractionId]
        -- ^ The interaction points of the buffer, in the order in which
        --   they appear in the buffer. The interaction points are
        --   recorded in 'theTCState', but when new interaction points are
        --   added by give or refine Agda does not ensure that the ranges
        --   of later interaction points are updated.
      , CommandState -> Maybe CurrentFile
    theCurrentFile       :: Maybe CurrentFile
        -- ^ The file which the state applies to. Only stored if the
        -- module was successfully type checked (potentially with
        -- warnings).
      , CommandState -> CommandLineOptions
    optionsOnReload      :: CommandLineOptions
        -- ^ Reset the options on each reload to these.
      , CommandState -> OldInteractionScopes
    oldInteractionScopes :: !OldInteractionScopes
        -- ^ We remember (the scope of) old interaction points to make it
        --   possible to parse and compute highlighting information for the
        --   expression that it got replaced by.
      , CommandState -> CommandQueue
    commandQueue         :: !CommandQueue
        -- ^ The command queue.
        --
        -- This queue should only be manipulated by
        -- 'initialiseCommandQueue' and 'maybeAbort'.
      }

    type OldInteractionScopes = Map InteractionId ScopeInfo

    -- | Initial auxiliary interaction state

    initCommandState :: CommandQueue -> CommandState
    initCommandState :: CommandQueue -> CommandState
    initCommandState CommandQueue
    commandQueue =
      CommandState
        { theInteractionPoints :: [InteractionId]
    theInteractionPoints = []
        , theCurrentFile :: Maybe CurrentFile
    theCurrentFile       = Maybe CurrentFile
    forall a. Maybe a
    Nothing
        , optionsOnReload :: CommandLineOptions
    optionsOnReload      = CommandLineOptions
    defaultOptions
        , oldInteractionScopes :: OldInteractionScopes
    oldInteractionScopes = OldInteractionScopes
    forall k a. Map k a
    Map.empty
        , commandQueue :: CommandQueue
    commandQueue         = CommandQueue
    commandQueue
        }

    -- | Information about the current main module.
    data CurrentFile = CurrentFile
      { CurrentFile -> AbsolutePath
    currentFilePath  :: AbsolutePath
          -- ^ The file currently loaded into interaction.
      , CurrentFile -> TopLevelModuleName
    currentFileModule :: TopLevelModuleName
          -- ^ The top-level module name of the currently loaded file.
      , CurrentFile -> [String]
    currentFileArgs  :: [String]
          -- ^ The arguments to Agda used for loading the file.
      , CurrentFile -> ClockTime
    currentFileStamp :: ClockTime
          -- ^ The modification time stamp of the file when it was loaded.
      } deriving (Int -> CurrentFile -> ShowS
    [CurrentFile] -> ShowS
    CurrentFile -> String
    (Int -> CurrentFile -> ShowS)
    -> (CurrentFile -> String)
    -> ([CurrentFile] -> ShowS)
    -> Show CurrentFile
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> CurrentFile -> ShowS
    showsPrec :: Int -> CurrentFile -> ShowS
    $cshow :: CurrentFile -> String
    show :: CurrentFile -> String
    $cshowList :: [CurrentFile] -> ShowS
    showList :: [CurrentFile] -> ShowS
    Show)

    type CommandM' = StateT CommandState

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

    -- | A generalised command type.

    data Command' a
      = Command !a
        -- ^ A command.
      | Done
        -- ^ Stop processing commands.
      | Error String
        -- ^ An error message for a command that could not be parsed.
      deriving Int -> Command' a -> ShowS
    [Command' a] -> ShowS
    Command' a -> String
    (Int -> Command' a -> ShowS)
    -> (Command' a -> String)
    -> ([Command' a] -> ShowS)
    -> Show (Command' a)
    forall a. Show a => Int -> Command' a -> ShowS
    forall a. Show a => [Command' a] -> ShowS
    forall a. Show a => Command' a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall a. Show a => Int -> Command' a -> ShowS
    showsPrec :: Int -> Command' a -> ShowS
    $cshow :: forall a. Show a => Command' a -> String
    show :: Command' a -> String
    $cshowList :: forall a. Show a => [Command' a] -> ShowS
    showList :: [Command' a] -> ShowS
    Show

    -- | IOTCM commands.

    type Command = Command' IOTCM

    -- | IOTCM commands.
    --
    -- The commands are obtained by applying the functions to the current
    -- top-level module name, if any. Note that the top-level module name
    -- is not used by independent commands. For other commands the
    -- top-level module name should be known.

    type IOTCM = Maybe TopLevelModuleName -> IOTCM' Range

    -- | Command queues.

    data CommandQueue = CommandQueue
      { CommandQueue -> TChan (Integer, Command)
    commands :: !(TChan (Integer, Command))
        -- ^ Commands that should be processed, in the order in which they
        -- should be processed. Each command is associated with a number,
        -- and the numbers are strictly increasing. Abort commands are not
        -- put on this queue.
      , CommandQueue -> TVar (Maybe Integer)
    abort    :: !(TVar (Maybe Integer))
        -- ^ When this variable is set to @Just n@ an attempt is made to
        -- abort all commands with a command number that is at most @n@.
      }

    ----------------------------------------------------------------------------
    -- | An interactive computation.

    type Interaction = Interaction' Range

    data Interaction' range
        -- | @cmd_load m argv@ loads the module in file @m@, using
        -- @argv@ as the command-line options.
      = Cmd_load FilePath [String]

      | Cmd_constraints

        -- | Show unsolved metas. If there are no unsolved metas but unsolved constraints
        -- show those instead.
      | Cmd_metas Rewrite

        -- | Load a file and fail if there are any unsolved
        -- meta-variables. By default no output is generated if the
        -- command is successful.
        -- (This command was previously used in Agda's installation script (Setup.hs)).
      | Cmd_load_no_metas FilePath

        -- | Shows all the top-level names in the given module, along with
        -- their types. Uses the top-level scope.
      | Cmd_show_module_contents_toplevel Rewrite String

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

        -- | Solve (all goals / the goal at point) whose values are determined by
        -- the constraints.
      | Cmd_solveAll Rewrite
      | Cmd_solveOne Rewrite InteractionId range String

        -- | Solve (all goals / the goal at point) by using Mimer proof search.
      | Cmd_autoOne  Rewrite   InteractionId range String
      | Cmd_autoAll  Rewrite

        -- | Parse the given expression (as if it were defined at the
        -- top-level of the current module) and infer its type.
      | Cmd_infer_toplevel Rewrite -- Normalise the type?
                           String

        -- | Parse and type check the given expression (as if it were defined
        -- at the top-level of the current module) and normalise it.
      | Cmd_compute_toplevel ComputeMode String

        ------------------------------------------------------------------------
        -- Backend commands

        -- | @cmd_compile b m argv@ compiles the module in file @m@ using
        -- the backend @b@, using @argv@ as the command-line options.
      | Cmd_compile CompilerBackend FilePath [String]

        -- | Custom top-level command for backends.
      | Cmd_backend_top
          CompilerBackend -- ^ which backend
          String          -- ^ arbitrary user payload

        -- | Custom hole-level command for backends.
      | Cmd_backend_hole
          InteractionId   -- ^ the hole's ID
          range           -- ^ range of the hole
          String          -- ^ text inside the hole
          CompilerBackend -- ^ which backend
          String          -- ^ arbitrary payload

        ------------------------------------------------------------------------
        -- Syntax highlighting

        -- | @cmd_load_highlighting_info source@ loads syntax highlighting
        -- information for the module in @source@, and asks Emacs to apply
        -- highlighting info from this file.
        --
        -- If the module does not exist, or its module name is malformed or
        -- cannot be determined, or the module has not already been visited,
        -- or the cached info is out of date, then no highlighting information
        -- is printed.
        --
        -- This command is used to load syntax highlighting information when a
        -- new file is opened, and it would probably be annoying if jumping to
        -- the definition of an identifier reset the proof state, so this
        -- command tries not to do that. One result of this is that the
        -- command uses the current include directories, whatever they happen
        -- to be.
      | Cmd_load_highlighting_info FilePath

        -- | Tells Agda to compute token-based highlighting information
        -- for the file.
        --
        -- This command works even if the file's module name does not
        -- match its location in the file system, or if the file is not
        -- scope-correct. Furthermore no file names are put in the
        -- generated output. Thus it is fine to put source code into a
        -- temporary file before calling this command. However, the file
        -- extension should be correct.
        --
        -- If the second argument is 'Remove', then the (presumably
        -- temporary) file is removed after it has been read.
      | Cmd_tokenHighlighting FilePath Remove

        -- | Tells Agda to compute highlighting information for the expression just
        --   spliced into an interaction point.
      | Cmd_highlight InteractionId range String

        ------------------------------------------------------------------------
        -- Implicit arguments

        -- | Tells Agda whether or not to show implicit arguments.
      | ShowImplicitArgs Bool-- Show them?

        -- | Toggle display of implicit arguments.
      | ToggleImplicitArgs

        ------------------------------------------------------------------------
        -- Irrelevant arguments

        -- | Tells Agda whether or not to show irrelevant arguments.
      | ShowIrrelevantArgs Bool -- Show them?

        -- | Toggle display of irrelevant arguments.
      | ToggleIrrelevantArgs

        ------------------------------------------------------------------------
        -- | Goal commands
        --
        -- If the range is 'noRange', then the string comes from the
        -- minibuffer rather than the goal.

      | Cmd_give            UseForce InteractionId range String

      | Cmd_refine          InteractionId range String

      | Cmd_intro           Bool InteractionId range String

      | Cmd_refine_or_intro Bool InteractionId range String

      | Cmd_context         Rewrite InteractionId range String

      | Cmd_helper_function Rewrite InteractionId range String

      | Cmd_infer           Rewrite InteractionId range String

      | Cmd_goal_type       Rewrite InteractionId range String

      -- | Grabs the current goal's type and checks the expression in the hole
      -- against it. Returns the elaborated term.
      | Cmd_elaborate_give
                            Rewrite InteractionId range String

        -- | Displays the current goal and context.
      | Cmd_goal_type_context Rewrite InteractionId range String

        -- | Displays the current goal and context /and/ infers the type of an
        -- expression.
      | Cmd_goal_type_context_infer
                            Rewrite InteractionId range String

      -- | Grabs the current goal's type and checks the expression in the hole
      -- against it.
      | Cmd_goal_type_context_check
                            Rewrite InteractionId range String

        -- | Shows all the top-level names in the given module, along with
        -- their types. Uses the scope of the given goal.
      | Cmd_show_module_contents
                            Rewrite InteractionId range String

      | Cmd_make_case       InteractionId range String

      | Cmd_compute         ComputeMode
                            InteractionId range String

      | Cmd_why_in_scope    InteractionId range String
      | Cmd_why_in_scope_toplevel String
        -- | Displays version of the running Agda
      | Cmd_show_version
      | Cmd_abort
        -- ^ Abort the current computation.
        --
        -- Does nothing if no computation is in progress.
      | Cmd_exit
        -- ^ Exit the program.
            deriving (Int -> Interaction' range -> ShowS
    [Interaction' range] -> ShowS
    Interaction' range -> String
    (Int -> Interaction' range -> ShowS)
    -> (Interaction' range -> String)
    -> ([Interaction' range] -> ShowS)
    -> Show (Interaction' range)
    forall range. Show range => Int -> Interaction' range -> ShowS
    forall range. Show range => [Interaction' range] -> ShowS
    forall range. Show range => Interaction' range -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall range. Show range => Int -> Interaction' range -> ShowS
    showsPrec :: Int -> Interaction' range -> ShowS
    $cshow :: forall range. Show range => Interaction' range -> String
    show :: Interaction' range -> String
    $cshowList :: forall range. Show range => [Interaction' range] -> ShowS
    showList :: [Interaction' range] -> ShowS
    Show, ReadPrec [Interaction' range]
    ReadPrec (Interaction' range)
    Int -> ReadS (Interaction' range)
    ReadS [Interaction' range]
    (Int -> ReadS (Interaction' range))
    -> ReadS [Interaction' range]
    -> ReadPrec (Interaction' range)
    -> ReadPrec [Interaction' range]
    -> Read (Interaction' range)
    forall range. Read range => ReadPrec [Interaction' range]
    forall range. Read range => ReadPrec (Interaction' range)
    forall range. Read range => Int -> ReadS (Interaction' range)
    forall range. Read range => ReadS [Interaction' range]
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: forall range. Read range => Int -> ReadS (Interaction' range)
    readsPrec :: Int -> ReadS (Interaction' range)
    $creadList :: forall range. Read range => ReadS [Interaction' range]
    readList :: ReadS [Interaction' range]
    $creadPrec :: forall range. Read range => ReadPrec (Interaction' range)
    readPrec :: ReadPrec (Interaction' range)
    $creadListPrec :: forall range. Read range => ReadPrec [Interaction' range]
    readListPrec :: ReadPrec [Interaction' range]
    Read, (forall a b. (a -> b) -> Interaction' a -> Interaction' b)
    -> (forall a b. a -> Interaction' b -> Interaction' a)
    -> Functor Interaction'
    forall a b. a -> Interaction' b -> Interaction' a
    forall a b. (a -> b) -> Interaction' a -> Interaction' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> Interaction' a -> Interaction' b
    fmap :: forall a b. (a -> b) -> Interaction' a -> Interaction' b
    $c<$ :: forall a b. a -> Interaction' b -> Interaction' a
    <$ :: forall a b. a -> Interaction' b -> Interaction' a
    Functor, (forall m. Monoid m => Interaction' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Interaction' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Interaction' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Interaction' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Interaction' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Interaction' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Interaction' a -> b)
    -> (forall a. (a -> a -> a) -> Interaction' a -> a)
    -> (forall a. (a -> a -> a) -> Interaction' a -> a)
    -> (forall a. Interaction' a -> [a])
    -> (forall a. Interaction' a -> Bool)
    -> (forall a. Interaction' a -> Int)
    -> (forall a. Eq a => a -> Interaction' a -> Bool)
    -> (forall a. Ord a => Interaction' a -> a)
    -> (forall a. Ord a => Interaction' a -> a)
    -> (forall a. Num a => Interaction' a -> a)
    -> (forall a. Num a => Interaction' a -> a)
    -> Foldable Interaction'
    forall a. Eq a => a -> Interaction' a -> Bool
    forall a. Num a => Interaction' a -> a
    forall a. Ord a => Interaction' a -> a
    forall m. Monoid m => Interaction' m -> m
    forall a. Interaction' a -> Bool
    forall a. Interaction' a -> Int
    forall a. Interaction' a -> [a]
    forall a. (a -> a -> a) -> Interaction' a -> a
    forall m a. Monoid m => (a -> m) -> Interaction' a -> m
    forall b a. (b -> a -> b) -> b -> Interaction' a -> b
    forall a b. (a -> b -> b) -> b -> Interaction' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => Interaction' m -> m
    fold :: forall m. Monoid m => Interaction' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> Interaction' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Interaction' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> Interaction' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> Interaction' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> Interaction' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Interaction' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> Interaction' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Interaction' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> Interaction' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Interaction' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> Interaction' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> Interaction' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> Interaction' a -> a
    foldr1 :: forall a. (a -> a -> a) -> Interaction' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> Interaction' a -> a
    foldl1 :: forall a. (a -> a -> a) -> Interaction' a -> a
    $ctoList :: forall a. Interaction' a -> [a]
    toList :: forall a. Interaction' a -> [a]
    $cnull :: forall a. Interaction' a -> Bool
    null :: forall a. Interaction' a -> Bool
    $clength :: forall a. Interaction' a -> Int
    length :: forall a. Interaction' a -> Int
    $celem :: forall a. Eq a => a -> Interaction' a -> Bool
    elem :: forall a. Eq a => a -> Interaction' a -> Bool
    $cmaximum :: forall a. Ord a => Interaction' a -> a
    maximum :: forall a. Ord a => Interaction' a -> a
    $cminimum :: forall a. Ord a => Interaction' a -> a
    minimum :: forall a. Ord a => Interaction' a -> a
    $csum :: forall a. Num a => Interaction' a -> a
    sum :: forall a. Num a => Interaction' a -> a
    $cproduct :: forall a. Num a => Interaction' a -> a
    product :: forall a. Num a => Interaction' a -> a
    Foldable, Functor Interaction'
    Foldable Interaction'
    (Functor Interaction', Foldable Interaction') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> Interaction' a -> f (Interaction' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Interaction' (f a) -> f (Interaction' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Interaction' a -> m (Interaction' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Interaction' (m a) -> m (Interaction' a))
    -> Traversable Interaction'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    Interaction' (m a) -> m (Interaction' a)
    forall (f :: * -> *) a.
    Applicative f =>
    Interaction' (f a) -> f (Interaction' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Interaction' a -> m (Interaction' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Interaction' a -> f (Interaction' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Interaction' a -> f (Interaction' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Interaction' a -> f (Interaction' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Interaction' (f a) -> f (Interaction' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Interaction' (f a) -> f (Interaction' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Interaction' a -> m (Interaction' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Interaction' a -> m (Interaction' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    Interaction' (m a) -> m (Interaction' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    Interaction' (m a) -> m (Interaction' a)
    Traversable)

    data IOTCM' range
        = IOTCM
            FilePath
             -- -^ The current file. If this file does not match
             -- 'theCurrentFile, and the 'Interaction' is not
             -- \"independent\", then an error is raised.
            HighlightingLevel
            HighlightingMethod
            (Interaction' range)
             -- -^ What to do
                deriving (Int -> IOTCM' range -> ShowS
    [IOTCM' range] -> ShowS
    IOTCM' range -> String
    (Int -> IOTCM' range -> ShowS)
    -> (IOTCM' range -> String)
    -> ([IOTCM' range] -> ShowS)
    -> Show (IOTCM' range)
    forall range. Show range => Int -> IOTCM' range -> ShowS
    forall range. Show range => [IOTCM' range] -> ShowS
    forall range. Show range => IOTCM' range -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall range. Show range => Int -> IOTCM' range -> ShowS
    showsPrec :: Int -> IOTCM' range -> ShowS
    $cshow :: forall range. Show range => IOTCM' range -> String
    show :: IOTCM' range -> String
    $cshowList :: forall range. Show range => [IOTCM' range] -> ShowS
    showList :: [IOTCM' range] -> ShowS
    Show, ReadPrec [IOTCM' range]
    ReadPrec (IOTCM' range)
    Int -> ReadS (IOTCM' range)
    ReadS [IOTCM' range]
    (Int -> ReadS (IOTCM' range))
    -> ReadS [IOTCM' range]
    -> ReadPrec (IOTCM' range)
    -> ReadPrec [IOTCM' range]
    -> Read (IOTCM' range)
    forall range. Read range => ReadPrec [IOTCM' range]
    forall range. Read range => ReadPrec (IOTCM' range)
    forall range. Read range => Int -> ReadS (IOTCM' range)
    forall range. Read range => ReadS [IOTCM' range]
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: forall range. Read range => Int -> ReadS (IOTCM' range)
    readsPrec :: Int -> ReadS (IOTCM' range)
    $creadList :: forall range. Read range => ReadS [IOTCM' range]
    readList :: ReadS [IOTCM' range]
    $creadPrec :: forall range. Read range => ReadPrec (IOTCM' range)
    readPrec :: ReadPrec (IOTCM' range)
    $creadListPrec :: forall range. Read range => ReadPrec [IOTCM' range]
    readListPrec :: ReadPrec [IOTCM' range]
    Read, (forall a b. (a -> b) -> IOTCM' a -> IOTCM' b)
    -> (forall a b. a -> IOTCM' b -> IOTCM' a) -> Functor IOTCM'
    forall a b. a -> IOTCM' b -> IOTCM' a
    forall a b. (a -> b) -> IOTCM' a -> IOTCM' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> IOTCM' a -> IOTCM' b
    fmap :: forall a b. (a -> b) -> IOTCM' a -> IOTCM' b
    $c<$ :: forall a b. a -> IOTCM' b -> IOTCM' a
    <$ :: forall a b. a -> IOTCM' b -> IOTCM' a
    Functor, (forall m. Monoid m => IOTCM' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> IOTCM' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> IOTCM' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> IOTCM' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> IOTCM' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> IOTCM' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> IOTCM' a -> b)
    -> (forall a. (a -> a -> a) -> IOTCM' a -> a)
    -> (forall a. (a -> a -> a) -> IOTCM' a -> a)
    -> (forall a. IOTCM' a -> [a])
    -> (forall a. IOTCM' a -> Bool)
    -> (forall a. IOTCM' a -> Int)
    -> (forall a. Eq a => a -> IOTCM' a -> Bool)
    -> (forall a. Ord a => IOTCM' a -> a)
    -> (forall a. Ord a => IOTCM' a -> a)
    -> (forall a. Num a => IOTCM' a -> a)
    -> (forall a. Num a => IOTCM' a -> a)
    -> Foldable IOTCM'
    forall a. Eq a => a -> IOTCM' a -> Bool
    forall a. Num a => IOTCM' a -> a
    forall a. Ord a => IOTCM' a -> a
    forall m. Monoid m => IOTCM' m -> m
    forall a. IOTCM' a -> Bool
    forall a. IOTCM' a -> Int
    forall a. IOTCM' a -> [a]
    forall a. (a -> a -> a) -> IOTCM' a -> a
    forall m a. Monoid m => (a -> m) -> IOTCM' a -> m
    forall b a. (b -> a -> b) -> b -> IOTCM' a -> b
    forall a b. (a -> b -> b) -> b -> IOTCM' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => IOTCM' m -> m
    fold :: forall m. Monoid m => IOTCM' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> IOTCM' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> IOTCM' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> IOTCM' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> IOTCM' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> IOTCM' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> IOTCM' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> IOTCM' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> IOTCM' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> IOTCM' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> IOTCM' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> IOTCM' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> IOTCM' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
    foldr1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
    foldl1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
    $ctoList :: forall a. IOTCM' a -> [a]
    toList :: forall a. IOTCM' a -> [a]
    $cnull :: forall a. IOTCM' a -> Bool
    null :: forall a. IOTCM' a -> Bool
    $clength :: forall a. IOTCM' a -> Int
    length :: forall a. IOTCM' a -> Int
    $celem :: forall a. Eq a => a -> IOTCM' a -> Bool
    elem :: forall a. Eq a => a -> IOTCM' a -> Bool
    $cmaximum :: forall a. Ord a => IOTCM' a -> a
    maximum :: forall a. Ord a => IOTCM' a -> a
    $cminimum :: forall a. Ord a => IOTCM' a -> a
    minimum :: forall a. Ord a => IOTCM' a -> a
    $csum :: forall a. Num a => IOTCM' a -> a
    sum :: forall a. Num a => IOTCM' a -> a
    $cproduct :: forall a. Num a => IOTCM' a -> a
    product :: forall a. Num a => IOTCM' a -> a
    Foldable, Functor IOTCM'
    Foldable IOTCM'
    (Functor IOTCM', Foldable IOTCM') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> IOTCM' a -> f (IOTCM' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        IOTCM' (f a) -> f (IOTCM' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> IOTCM' a -> m (IOTCM' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        IOTCM' (m a) -> m (IOTCM' a))
    -> Traversable IOTCM'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a. Monad m => IOTCM' (m a) -> m (IOTCM' a)
    forall (f :: * -> *) a.
    Applicative f =>
    IOTCM' (f a) -> f (IOTCM' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> IOTCM' a -> m (IOTCM' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> IOTCM' a -> f (IOTCM' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> IOTCM' a -> f (IOTCM' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> IOTCM' a -> f (IOTCM' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    IOTCM' (f a) -> f (IOTCM' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    IOTCM' (f a) -> f (IOTCM' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> IOTCM' a -> m (IOTCM' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> IOTCM' a -> m (IOTCM' b)
    $csequence :: forall (m :: * -> *) a. Monad m => IOTCM' (m a) -> m (IOTCM' a)
    sequence :: forall (m :: * -> *) a. Monad m => IOTCM' (m a) -> m (IOTCM' a)
    Traversable)

    -- | Used to indicate whether something should be removed or not.

    data Remove
      = Remove
      | Keep
      deriving (Int -> Remove -> ShowS
    [Remove] -> ShowS
    Remove -> String
    (Int -> Remove -> ShowS)
    -> (Remove -> String) -> ([Remove] -> ShowS) -> Show Remove
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Remove -> ShowS
    showsPrec :: Int -> Remove -> ShowS
    $cshow :: Remove -> String
    show :: Remove -> String
    $cshowList :: [Remove] -> ShowS
    showList :: [Remove] -> ShowS
    Show, ReadPrec [Remove]
    ReadPrec Remove
    Int -> ReadS Remove
    ReadS [Remove]
    (Int -> ReadS Remove)
    -> ReadS [Remove]
    -> ReadPrec Remove
    -> ReadPrec [Remove]
    -> Read Remove
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS Remove
    readsPrec :: Int -> ReadS Remove
    $creadList :: ReadS [Remove]
    readList :: ReadS [Remove]
    $creadPrec :: ReadPrec Remove
    readPrec :: ReadPrec Remove
    $creadListPrec :: ReadPrec [Remove]
    readListPrec :: ReadPrec [Remove]
    Read)

    ---------------------------------------------------------
    -- Read instances

    -- | An 'IOTCM' parser.
    --
    -- If the parse fails, then an error message is returned.

    parseIOTCM ::
      String -> Either String IOTCM
    parseIOTCM :: String -> Either String IOTCM
    parseIOTCM String
    s = case [(IOTCM' (Range' (Maybe RangeFile)), String)]
    -> Maybe (IOTCM' (Range' (Maybe RangeFile)), String)
    forall a. [a] -> Maybe a
    listToMaybe ([(IOTCM' (Range' (Maybe RangeFile)), String)]
     -> Maybe (IOTCM' (Range' (Maybe RangeFile)), String))
    -> [(IOTCM' (Range' (Maybe RangeFile)), String)]
    -> Maybe (IOTCM' (Range' (Maybe RangeFile)), String)
    forall a b. (a -> b) -> a -> b
    $ ReadS (IOTCM' (Range' (Maybe RangeFile)))
    forall a. Read a => ReadS a
    reads String
    s of
      Just (IOTCM' (Range' (Maybe RangeFile))
    x, String
    "")  -> IOTCM -> Either String IOTCM
    forall a b. b -> Either a b
    Right (IOTCM -> Either String IOTCM) -> IOTCM -> Either String IOTCM
    forall a b. (a -> b) -> a -> b
    $ \Maybe TopLevelModuleName
    top -> case IOTCM' (Range' (Maybe RangeFile))
    x of
        IOTCM String
    f HighlightingLevel
    l HighlightingMethod
    m Interaction' (Range' (Maybe RangeFile))
    i -> String
    -> HighlightingLevel
    -> HighlightingMethod
    -> Interaction' (Range' (Maybe RangeFile))
    -> IOTCM' (Range' (Maybe RangeFile))
    forall range.
    String
    -> HighlightingLevel
    -> HighlightingMethod
    -> Interaction' range
    -> IOTCM' range
    IOTCM String
    f HighlightingLevel
    l HighlightingMethod
    m (Interaction' (Range' (Maybe RangeFile))
     -> IOTCM' (Range' (Maybe RangeFile)))
    -> Interaction' (Range' (Maybe RangeFile))
    -> IOTCM' (Range' (Maybe RangeFile))
    forall a b. (a -> b) -> a -> b
    $
          ((Range' (Maybe RangeFile) -> Range' (Maybe RangeFile))
    -> Interaction' (Range' (Maybe RangeFile))
    -> Interaction' (Range' (Maybe RangeFile))
    forall a b. (a -> b) -> Interaction' a -> Interaction' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Range' (Maybe RangeFile) -> Range' (Maybe RangeFile))
     -> Interaction' (Range' (Maybe RangeFile))
     -> Interaction' (Range' (Maybe RangeFile)))
    -> ((RangeFile -> RangeFile)
        -> Range' (Maybe RangeFile) -> Range' (Maybe RangeFile))
    -> (RangeFile -> RangeFile)
    -> Interaction' (Range' (Maybe RangeFile))
    -> Interaction' (Range' (Maybe RangeFile))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Maybe RangeFile -> Maybe RangeFile)
    -> Range' (Maybe RangeFile) -> Range' (Maybe RangeFile)
    forall a b. (a -> b) -> Range' a -> Range' b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Maybe RangeFile -> Maybe RangeFile)
     -> Range' (Maybe RangeFile) -> Range' (Maybe RangeFile))
    -> ((RangeFile -> RangeFile) -> Maybe RangeFile -> Maybe RangeFile)
    -> (RangeFile -> RangeFile)
    -> Range' (Maybe RangeFile)
    -> Range' (Maybe RangeFile)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (RangeFile -> RangeFile) -> Maybe RangeFile -> Maybe RangeFile
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap) (\RangeFile
    rf -> AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
    mkRangeFile (RangeFile -> AbsolutePath
    rangeFilePath RangeFile
    rf) Maybe TopLevelModuleName
    top) Interaction' (Range' (Maybe RangeFile))
    i
      Just (IOTCM' (Range' (Maybe RangeFile))
    _, String
    rem) -> String -> Either String IOTCM
    forall a b. a -> Either a b
    Left (String -> Either String IOTCM) -> String -> Either String IOTCM
    forall a b. (a -> b) -> a -> b
    $ String
    "not consumed: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    rem
      Maybe (IOTCM' (Range' (Maybe RangeFile)), String)
    _             -> String -> Either String IOTCM
    forall a b. a -> Either a b
    Left (String -> Either String IOTCM) -> String -> Either String IOTCM
    forall a b. (a -> b) -> a -> b
    $ String
    "cannot read: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s

    -- | The 'Parse' monad.
    --   'StateT' state holds the remaining input.

    type Parse a = ExceptT String (StateT String Identity) a

    -- | Converter from the type of 'reads' to 'Parse'
    --   The first paramter is part of the error message
    --   in case the parse fails.

    readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a
    readsToParse :: forall a. String -> (String -> Maybe (a, String)) -> Parse a
    readsToParse String
    s String -> Maybe (a, String)
    f = do
      st <- StateT String Identity String
    -> ExceptT String (StateT String Identity) String
    forall (m :: * -> *) a. Monad m => m a -> ExceptT String m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift StateT String Identity String
    forall s (m :: * -> *). MonadState s m => m s
    get
      case f st of
        Maybe (a, String)
    Nothing -> String -> ExceptT String (StateT String Identity) a
    forall a. String -> ExceptT String (StateT String Identity) a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError String
    s
        Just (a
    a, String
    st) -> do
            StateT String Identity ()
    -> ExceptT String (StateT String Identity) ()
    forall (m :: * -> *) a. Monad m => m a -> ExceptT String m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (StateT String Identity ()
     -> ExceptT String (StateT String Identity) ())
    -> StateT String Identity ()
    -> ExceptT String (StateT String Identity) ()
    forall a b. (a -> b) -> a -> b
    $ String -> StateT String Identity ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put String
    st
            a -> ExceptT String (StateT String Identity) a
    forall a. a -> ExceptT String (StateT String Identity) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a

    parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec :: forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec Parse a
    p Int
    i String
    s = case Identity (Either String a, String) -> (Either String a, String)
    forall a. Identity a -> a
    runIdentity (Identity (Either String a, String) -> (Either String a, String))
    -> (Parse a -> Identity (Either String a, String))
    -> Parse a
    -> (Either String a, String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (StateT String Identity (Either String a)
     -> String -> Identity (Either String a, String))
    -> String
    -> StateT String Identity (Either String a)
    -> Identity (Either String a, String)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip StateT String Identity (Either String a)
    -> String -> Identity (Either String a, String)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT String
    s (StateT String Identity (Either String a)
     -> Identity (Either String a, String))
    -> (Parse a -> StateT String Identity (Either String a))
    -> Parse a
    -> Identity (Either String a, String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Parse a -> StateT String Identity (Either String a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (Parse a -> (Either String a, String))
    -> Parse a -> (Either String a, String)
    forall a b. (a -> b) -> a -> b
    $ Parse a -> Parse a
    forall a. Parse a -> Parse a
    parens' Parse a
    p of
      (Right a
    a, String
    s) -> [(a
    a,String
    s)]
      (Either String a, String)
    _            -> []

    -- | Demand an exact string.

    exact :: String -> Parse ()
    exact :: String -> ExceptT String (StateT String Identity) ()
    exact String
    s = String
    -> (String -> Maybe ((), String))
    -> ExceptT String (StateT String Identity) ()
    forall a. String -> (String -> Maybe (a, String)) -> Parse a
    readsToParse (ShowS
    forall a. Show a => a -> String
    show String
    s) ((String -> Maybe ((), String))
     -> ExceptT String (StateT String Identity) ())
    -> (String -> Maybe ((), String))
    -> ExceptT String (StateT String Identity) ()
    forall a b. (a -> b) -> a -> b
    $ (String -> ((), String)) -> Maybe String -> Maybe ((), String)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((),) (Maybe String -> Maybe ((), String))
    -> (String -> Maybe String) -> String -> Maybe ((), String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> String -> Maybe String
    forall a. Eq a => [a] -> [a] -> Maybe [a]
    List.stripPrefix String
    s (String -> Maybe String) -> ShowS -> String -> Maybe String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    ' ')

    readParse :: Read a => Parse a
    readParse :: forall a. Read a => Parse a
    readParse = String -> (String -> Maybe (a, String)) -> Parse a
    forall a. String -> (String -> Maybe (a, String)) -> Parse a
    readsToParse String
    "read failed" ((String -> Maybe (a, String)) -> Parse a)
    -> (String -> Maybe (a, String)) -> Parse a
    forall a b. (a -> b) -> a -> b
    $ [(a, String)] -> Maybe (a, String)
    forall a. [a] -> Maybe a
    listToMaybe ([(a, String)] -> Maybe (a, String))
    -> (String -> [(a, String)]) -> String -> Maybe (a, String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [(a, String)]
    forall a. Read a => ReadS a
    reads

    parens' :: Parse a -> Parse a
    parens' :: forall a. Parse a -> Parse a
    parens' Parse a
    p = do
        String -> ExceptT String (StateT String Identity) ()
    exact String
    "("
        x <- Parse a
    p
        exact ")"
        return x
      Parse a -> Parse a -> Parse a
    forall a.
    ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
        Parse a
    p

    instance Read InteractionId where
        readsPrec :: Int -> ReadS InteractionId
    readsPrec = Parse InteractionId -> Int -> ReadS InteractionId
    forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec (Parse InteractionId -> Int -> ReadS InteractionId)
    -> Parse InteractionId -> Int -> ReadS InteractionId
    forall a b. (a -> b) -> a -> b
    $
            (Int -> InteractionId)
    -> ExceptT String (StateT String Identity) Int
    -> Parse InteractionId
    forall a b.
    (a -> b)
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Int -> InteractionId
    InteractionId ExceptT String (StateT String Identity) Int
    forall a. Read a => Parse a
    readParse

    -- | Note that the grammar implemented by this instance does not
    -- necessarily match the current representation of ranges.

    instance Read a => Read (Range' a) where
        readsPrec :: Int -> ReadS (Range' a)
    readsPrec = Parse (Range' a) -> Int -> ReadS (Range' a)
    forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec (Parse (Range' a) -> Int -> ReadS (Range' a))
    -> Parse (Range' a) -> Int -> ReadS (Range' a)
    forall a b. (a -> b) -> a -> b
    $
          (String -> ExceptT String (StateT String Identity) ()
    exact String
    "intervalsToRange" ExceptT String (StateT String Identity) ()
    -> Parse (Range' a) -> Parse (Range' a)
    forall a b.
    ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) b
    -> ExceptT String (StateT String Identity) b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >>
           (a -> [IntervalWithoutFile] -> Range' a)
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) [IntervalWithoutFile]
    -> Parse (Range' a)
    forall (m :: * -> *) a1 a2 r.
    Monad m =>
    (a1 -> a2 -> r) -> m a1 -> m a2 -> m r
    liftM2 a -> [IntervalWithoutFile] -> Range' a
    forall a. a -> [IntervalWithoutFile] -> Range' a
    intervalsToRange ExceptT String (StateT String Identity) a
    forall a. Read a => Parse a
    readParse ExceptT String (StateT String Identity) [IntervalWithoutFile]
    forall a. Read a => Parse a
    readParse)
            Parse (Range' a) -> Parse (Range' a) -> Parse (Range' a)
    forall a.
    ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) a
    forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
    `mplus`
          (String -> ExceptT String (StateT String Identity) ()
    exact String
    "noRange" ExceptT String (StateT String Identity) ()
    -> Parse (Range' a) -> Parse (Range' a)
    forall a b.
    ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) b
    -> ExceptT String (StateT String Identity) b
    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
    >> Range' a -> Parse (Range' a)
    forall a. a -> ExceptT String (StateT String Identity) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Range' a
    forall a. Range' a
    noRange)

    instance Read a => Read (Interval' a) where
        readsPrec :: Int -> ReadS (Interval' a)
    readsPrec = Parse (Interval' a) -> Int -> ReadS (Interval' a)
    forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec (Parse (Interval' a) -> Int -> ReadS (Interval' a))
    -> Parse (Interval' a) -> Int -> ReadS (Interval' a)
    forall a b. (a -> b) -> a -> b
    $ do
            String -> ExceptT String (StateT String Identity) ()
    exact String
    "Interval"
            (a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a)
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) PositionWithoutFile
    -> ExceptT String (StateT String Identity) PositionWithoutFile
    -> Parse (Interval' a)
    forall (f :: * -> *) a b c d.
    Applicative f =>
    (a -> b -> c -> d) -> f a -> f b -> f c -> f d
    liftA3 a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
    forall a.
    a -> PositionWithoutFile -> PositionWithoutFile -> Interval' a
    Interval ExceptT String (StateT String Identity) a
    forall a. Read a => Parse a
    readParse ExceptT String (StateT String Identity) PositionWithoutFile
    forall a. Read a => Parse a
    readParse ExceptT String (StateT String Identity) PositionWithoutFile
    forall a. Read a => Parse a
    readParse

    instance Read AbsolutePath where
        readsPrec :: Int -> ReadS AbsolutePath
    readsPrec = Parse AbsolutePath -> Int -> ReadS AbsolutePath
    forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec (Parse AbsolutePath -> Int -> ReadS AbsolutePath)
    -> Parse AbsolutePath -> Int -> ReadS AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ do
            String -> ExceptT String (StateT String Identity) ()
    exact String
    "mkAbsolute"
            (String -> AbsolutePath)
    -> ExceptT String (StateT String Identity) String
    -> Parse AbsolutePath
    forall a b.
    (a -> b)
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap String -> AbsolutePath
    mkAbsolute ExceptT String (StateT String Identity) String
    forall a. Read a => Parse a
    readParse

    -- | This instance fills in the 'TopLevelModuleName's using 'Nothing'.
    -- Note that these occurrences of 'Nothing' are \"overwritten\" by
    -- 'parseIOTCM'.

    instance Read RangeFile where
        readsPrec :: Int -> ReadS RangeFile
    readsPrec = Parse RangeFile -> Int -> ReadS RangeFile
    forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec (Parse RangeFile -> Int -> ReadS RangeFile)
    -> Parse RangeFile -> Int -> ReadS RangeFile
    forall a b. (a -> b) -> a -> b
    $
          (AbsolutePath -> RangeFile)
    -> Parse AbsolutePath -> Parse RangeFile
    forall a b.
    (a -> b)
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((AbsolutePath -> Maybe TopLevelModuleName -> RangeFile)
    -> Maybe TopLevelModuleName -> AbsolutePath -> RangeFile
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip AbsolutePath -> Maybe TopLevelModuleName -> RangeFile
    mkRangeFile Maybe TopLevelModuleName
    forall a. Maybe a
    Nothing) Parse AbsolutePath
    forall a. Read a => Parse a
    readParse

    instance Read a => Read (Position' a) where
        readsPrec :: Int -> ReadS (Position' a)
    readsPrec = Parse (Position' a) -> Int -> ReadS (Position' a)
    forall a. Parse a -> Int -> String -> [(a, String)]
    parseToReadsPrec (Parse (Position' a) -> Int -> ReadS (Position' a))
    -> Parse (Position' a) -> Int -> ReadS (Position' a)
    forall a b. (a -> b) -> a -> b
    $ do
            String -> ExceptT String (StateT String Identity) ()
    exact String
    "Pn"
            (a -> Word32 -> Word32 -> Word32 -> Position' a)
    -> ExceptT String (StateT String Identity) a
    -> ExceptT String (StateT String Identity) Word32
    -> ExceptT String (StateT String Identity) Word32
    -> ExceptT String (StateT String Identity) Word32
    -> Parse (Position' a)
    forall (m :: * -> *) a1 a2 a3 a4 r.
    Monad m =>
    (a1 -> a2 -> a3 -> a4 -> r) -> m a1 -> m a2 -> m a3 -> m a4 -> m r
    liftM4 a -> Word32 -> Word32 -> Word32 -> Position' a
    forall a. a -> Word32 -> Word32 -> Word32 -> Position' a
    Pn ExceptT String (StateT String Identity) a
    forall a. Read a => Parse a
    readParse ExceptT String (StateT String Identity) Word32
    forall a. Read a => Parse a
    readParse ExceptT String (StateT String Identity) Word32
    forall a. Read a => Parse a
    readParse ExceptT String (StateT String Identity) Word32
    forall a. Read a => Parse a
    readParse

    ---------------------------------------------------------
    -- | Available backends.

    data CompilerBackend = LaTeX | QuickLaTeX | OtherBackend BackendName
        deriving (CompilerBackend -> CompilerBackend -> Bool
    (CompilerBackend -> CompilerBackend -> Bool)
    -> (CompilerBackend -> CompilerBackend -> Bool)
    -> Eq CompilerBackend
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: CompilerBackend -> CompilerBackend -> Bool
    == :: CompilerBackend -> CompilerBackend -> Bool
    $c/= :: CompilerBackend -> CompilerBackend -> Bool
    /= :: CompilerBackend -> CompilerBackend -> Bool
    Eq)

    -- TODO 2021-08-25 get rid of custom Show instance
    instance Show CompilerBackend where
      show :: CompilerBackend -> String
    show = CompilerBackend -> String
    forall a. Pretty a => a -> String
    prettyShow

    instance Pretty CompilerBackend where
      pretty :: CompilerBackend -> Doc
    pretty = \case
        CompilerBackend
    LaTeX          -> Doc
    "LaTeX"
        CompilerBackend
    QuickLaTeX     -> Doc
    "QuickLaTeX"
        OtherBackend BackendName
    s -> BackendName -> Doc
    forall a. Pretty a => a -> Doc
    pretty BackendName
    s

    instance Read CompilerBackend where
      readsPrec :: Int -> ReadS CompilerBackend
    readsPrec Int
    _ String
    s = do
        (t, s) <- ReadS String
    lex String
    s
        let b = case String
    t of
                  String
    "LaTeX"      -> CompilerBackend
    LaTeX
                  String
    "QuickLaTeX" -> CompilerBackend
    QuickLaTeX
                  String
    _            -> BackendName -> CompilerBackend
    OtherBackend (BackendName -> CompilerBackend) -> BackendName -> CompilerBackend
    forall a b. (a -> b) -> a -> b
    $ String -> BackendName
    T.pack String
    t
        return (b, s)

    -- | Ordered ascendingly by degree of normalization.
    data Rewrite =  AsIs | Instantiated | HeadNormal | Simplified | Normalised
        deriving (Int -> Rewrite -> ShowS
    [Rewrite] -> ShowS
    Rewrite -> String
    (Int -> Rewrite -> ShowS)
    -> (Rewrite -> String) -> ([Rewrite] -> ShowS) -> Show Rewrite
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Rewrite -> ShowS
    showsPrec :: Int -> Rewrite -> ShowS
    $cshow :: Rewrite -> String
    show :: Rewrite -> String
    $cshowList :: [Rewrite] -> ShowS
    showList :: [Rewrite] -> ShowS
    Show, ReadPrec [Rewrite]
    ReadPrec Rewrite
    Int -> ReadS Rewrite
    ReadS [Rewrite]
    (Int -> ReadS Rewrite)
    -> ReadS [Rewrite]
    -> ReadPrec Rewrite
    -> ReadPrec [Rewrite]
    -> Read Rewrite
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS Rewrite
    readsPrec :: Int -> ReadS Rewrite
    $creadList :: ReadS [Rewrite]
    readList :: ReadS [Rewrite]
    $creadPrec :: ReadPrec Rewrite
    readPrec :: ReadPrec Rewrite
    $creadListPrec :: ReadPrec [Rewrite]
    readListPrec :: ReadPrec [Rewrite]
    Read, Rewrite -> Rewrite -> Bool
    (Rewrite -> Rewrite -> Bool)
    -> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Rewrite -> Rewrite -> Bool
    == :: Rewrite -> Rewrite -> Bool
    $c/= :: Rewrite -> Rewrite -> Bool
    /= :: Rewrite -> Rewrite -> Bool
    Eq, Eq Rewrite
    Eq Rewrite =>
    (Rewrite -> Rewrite -> Ordering)
    -> (Rewrite -> Rewrite -> Bool)
    -> (Rewrite -> Rewrite -> Bool)
    -> (Rewrite -> Rewrite -> Bool)
    -> (Rewrite -> Rewrite -> Bool)
    -> (Rewrite -> Rewrite -> Rewrite)
    -> (Rewrite -> Rewrite -> Rewrite)
    -> Ord Rewrite
    Rewrite -> Rewrite -> Bool
    Rewrite -> Rewrite -> Ordering
    Rewrite -> Rewrite -> Rewrite
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Rewrite -> Rewrite -> Ordering
    compare :: Rewrite -> Rewrite -> Ordering
    $c< :: Rewrite -> Rewrite -> Bool
    < :: Rewrite -> Rewrite -> Bool
    $c<= :: Rewrite -> Rewrite -> Bool
    <= :: Rewrite -> Rewrite -> Bool
    $c> :: Rewrite -> Rewrite -> Bool
    > :: Rewrite -> Rewrite -> Bool
    $c>= :: Rewrite -> Rewrite -> Bool
    >= :: Rewrite -> Rewrite -> Bool
    $cmax :: Rewrite -> Rewrite -> Rewrite
    max :: Rewrite -> Rewrite -> Rewrite
    $cmin :: Rewrite -> Rewrite -> Rewrite
    min :: Rewrite -> Rewrite -> Rewrite
    Ord)

    data ComputeMode = DefaultCompute | HeadCompute | IgnoreAbstract | UseShowInstance
      deriving (Int -> ComputeMode -> ShowS
    [ComputeMode] -> ShowS
    ComputeMode -> String
    (Int -> ComputeMode -> ShowS)
    -> (ComputeMode -> String)
    -> ([ComputeMode] -> ShowS)
    -> Show ComputeMode
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> ComputeMode -> ShowS
    showsPrec :: Int -> ComputeMode -> ShowS
    $cshow :: ComputeMode -> String
    show :: ComputeMode -> String
    $cshowList :: [ComputeMode] -> ShowS
    showList :: [ComputeMode] -> ShowS
    Show, ReadPrec [ComputeMode]
    ReadPrec ComputeMode
    Int -> ReadS ComputeMode
    ReadS [ComputeMode]
    (Int -> ReadS ComputeMode)
    -> ReadS [ComputeMode]
    -> ReadPrec ComputeMode
    -> ReadPrec [ComputeMode]
    -> Read ComputeMode
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS ComputeMode
    readsPrec :: Int -> ReadS ComputeMode
    $creadList :: ReadS [ComputeMode]
    readList :: ReadS [ComputeMode]
    $creadPrec :: ReadPrec ComputeMode
    readPrec :: ReadPrec ComputeMode
    $creadListPrec :: ReadPrec [ComputeMode]
    readListPrec :: ReadPrec [ComputeMode]
    Read, ComputeMode -> ComputeMode -> Bool
    (ComputeMode -> ComputeMode -> Bool)
    -> (ComputeMode -> ComputeMode -> Bool) -> Eq ComputeMode
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: ComputeMode -> ComputeMode -> Bool
    == :: ComputeMode -> ComputeMode -> Bool
    $c/= :: ComputeMode -> ComputeMode -> Bool
    /= :: ComputeMode -> ComputeMode -> Bool
    Eq)

    data UseForce
      = WithForce     -- ^ Ignore additional checks, like termination/positivity...
      | WithoutForce  -- ^ Don't ignore any checks.
      deriving (UseForce -> UseForce -> Bool
    (UseForce -> UseForce -> Bool)
    -> (UseForce -> UseForce -> Bool) -> Eq UseForce
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: UseForce -> UseForce -> Bool
    == :: UseForce -> UseForce -> Bool
    $c/= :: UseForce -> UseForce -> Bool
    /= :: UseForce -> UseForce -> Bool
    Eq, ReadPrec [UseForce]
    ReadPrec UseForce
    Int -> ReadS UseForce
    ReadS [UseForce]
    (Int -> ReadS UseForce)
    -> ReadS [UseForce]
    -> ReadPrec UseForce
    -> ReadPrec [UseForce]
    -> Read UseForce
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: Int -> ReadS UseForce
    readsPrec :: Int -> ReadS UseForce
    $creadList :: ReadS [UseForce]
    readList :: ReadS [UseForce]
    $creadPrec :: ReadPrec UseForce
    readPrec :: ReadPrec UseForce
    $creadListPrec :: ReadPrec [UseForce]
    readListPrec :: ReadPrec [UseForce]
    Read, Int -> UseForce -> ShowS
    [UseForce] -> ShowS
    UseForce -> String
    (Int -> UseForce -> ShowS)
    -> (UseForce -> String) -> ([UseForce] -> ShowS) -> Show UseForce
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> UseForce -> ShowS
    showsPrec :: Int -> UseForce -> ShowS
    $cshow :: UseForce -> String
    show :: UseForce -> String
    $cshowList :: [UseForce] -> ShowS
    showList :: [UseForce] -> ShowS
    Show)

    data OutputForm_boot tcErr a b = OutputForm Range [ProblemId] Blocker (OutputConstraint_boot tcErr a b)
      deriving ((forall a b.
     (a -> b) -> OutputForm_boot tcErr a a -> OutputForm_boot tcErr a b)
    -> (forall a b.
        a -> OutputForm_boot tcErr a b -> OutputForm_boot tcErr a a)
    -> Functor (OutputForm_boot tcErr a)
    forall a b.
    a -> OutputForm_boot tcErr a b -> OutputForm_boot tcErr a a
    forall a b.
    (a -> b) -> OutputForm_boot tcErr a a -> OutputForm_boot tcErr a b
    forall tcErr a a b.
    a -> OutputForm_boot tcErr a b -> OutputForm_boot tcErr a a
    forall tcErr a a b.
    (a -> b) -> OutputForm_boot tcErr a a -> OutputForm_boot tcErr a b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall tcErr a a b.
    (a -> b) -> OutputForm_boot tcErr a a -> OutputForm_boot tcErr a b
    fmap :: forall a b.
    (a -> b) -> OutputForm_boot tcErr a a -> OutputForm_boot tcErr a b
    $c<$ :: forall tcErr a a b.
    a -> OutputForm_boot tcErr a b -> OutputForm_boot tcErr a a
    <$ :: forall a b.
    a -> OutputForm_boot tcErr a b -> OutputForm_boot tcErr a a
    Functor)

    data OutputConstraint_boot tcErr a b
          = OfType b a | CmpInType Comparison a b b
                       | CmpElim [Polarity] a [b] [b]
          | JustType b | CmpTypes Comparison b b
                       | CmpLevels Comparison b b
                       | CmpTeles Comparison b b
          | JustSort b | CmpSorts Comparison b b
          | Assign b a | TypedAssign b a a | PostponedCheckArgs b [a] a a
          | IsEmptyType a
          | SizeLtSat a
          | FindInstanceOF b a [(a,a,a)]
          | ResolveInstanceOF QName
          | PTSInstance b b
          | PostponedCheckFunDef QName a tcErr
          | CheckLock b b
          | DataSort QName b
          | UsableAtMod Modality b
      deriving ((forall a b.
     (a -> b)
     -> OutputConstraint_boot tcErr a a
     -> OutputConstraint_boot tcErr a b)
    -> (forall a b.
        a
        -> OutputConstraint_boot tcErr a b
        -> OutputConstraint_boot tcErr a a)
    -> Functor (OutputConstraint_boot tcErr a)
    forall a b.
    a
    -> OutputConstraint_boot tcErr a b
    -> OutputConstraint_boot tcErr a a
    forall a b.
    (a -> b)
    -> OutputConstraint_boot tcErr a a
    -> OutputConstraint_boot tcErr a b
    forall tcErr a a b.
    a
    -> OutputConstraint_boot tcErr a b
    -> OutputConstraint_boot tcErr a a
    forall tcErr a a b.
    (a -> b)
    -> OutputConstraint_boot tcErr a a
    -> OutputConstraint_boot tcErr a b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall tcErr a a b.
    (a -> b)
    -> OutputConstraint_boot tcErr a a
    -> OutputConstraint_boot tcErr a b
    fmap :: forall a b.
    (a -> b)
    -> OutputConstraint_boot tcErr a a
    -> OutputConstraint_boot tcErr a b
    $c<$ :: forall tcErr a a b.
    a
    -> OutputConstraint_boot tcErr a b
    -> OutputConstraint_boot tcErr a a
    <$ :: forall a b.
    a
    -> OutputConstraint_boot tcErr a b
    -> OutputConstraint_boot tcErr a a
    Functor)

    -- | A subset of 'OutputConstraint'.

    data OutputConstraint' a b = OfType'
      { forall a b. OutputConstraint' a b -> b
    ofName :: b
      , forall a b. OutputConstraint' a b -> a
    ofExpr :: a
      }

    data OutputContextEntry name ty val
      = ContextVar name ty
      | ContextLet name ty val