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

module Agda.Interaction.Base where

import           Control.Concurrent.STM.TChan
import           Control.Concurrent.STM.TVar
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 {-# SOURCE #-} Agda.TypeChecking.Monad.Base
  (HighlightingLevel, HighlightingMethod, TCM, Comparison, Polarity, TCErr)

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

import           Agda.Interaction.Options     (CommandLineOptions,
                                               defaultOptions)

import           Agda.Utils.FileName          (AbsolutePath, mkAbsolute)
import           Agda.Utils.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
    }

-- | Monad for computing answers to interactive commands.
--
--   'CommandM' is 'TCM' extended with state 'CommandState'.

type CommandM = StateT CommandState TCM

-- | Information about the current main module.
data CurrentFile = CurrentFile
  { CurrentFile -> AbsolutePath
currentFilePath  :: AbsolutePath
      -- ^ The file currently loaded into interaction.
  , 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
showList :: [CurrentFile] -> ShowS
$cshowList :: [CurrentFile] -> ShowS
show :: CurrentFile -> String
$cshow :: CurrentFile -> String
showsPrec :: Int -> CurrentFile -> ShowS
$cshowsPrec :: Int -> CurrentFile -> ShowS
Show)

------------------------------------------------------------------------
-- 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
showList :: [Command' a] -> ShowS
$cshowList :: forall a. Show a => [Command' a] -> ShowS
show :: Command' a -> String
$cshow :: forall a. Show a => Command' a -> String
showsPrec :: Int -> Command' a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Command' a -> ShowS
Show

-- | IOTCM commands.

type Command = Command' IOTCM

-- | 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_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]

  | Cmd_constraints

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

    -- | 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 Auto.
  | Cmd_autoOne            InteractionId range String
  | Cmd_autoAll

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

    ------------------------------------------------------------------------
    -- 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
showList :: [Interaction' range] -> ShowS
$cshowList :: forall range. Show range => [Interaction' range] -> ShowS
show :: Interaction' range -> String
$cshow :: forall range. Show range => Interaction' range -> String
showsPrec :: Int -> Interaction' range -> ShowS
$cshowsPrec :: forall range. Show range => Int -> 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
readListPrec :: ReadPrec [Interaction' range]
$creadListPrec :: forall range. Read range => ReadPrec [Interaction' range]
readPrec :: ReadPrec (Interaction' range)
$creadPrec :: forall range. Read range => ReadPrec (Interaction' range)
readList :: ReadS [Interaction' range]
$creadList :: forall range. Read range => ReadS [Interaction' range]
readsPrec :: Int -> ReadS (Interaction' range)
$creadsPrec :: forall range. Read range => Int -> ReadS (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
<$ :: forall a b. a -> Interaction' b -> Interaction' a
$c<$ :: forall a b. a -> Interaction' b -> Interaction' a
fmap :: forall a b. (a -> b) -> Interaction' a -> Interaction' b
$cfmap :: forall a b. (a -> b) -> Interaction' a -> Interaction' b
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
product :: forall a. Num a => Interaction' a -> a
$cproduct :: forall a. Num a => Interaction' a -> a
sum :: forall a. Num a => Interaction' a -> a
$csum :: forall a. Num a => Interaction' a -> a
minimum :: forall a. Ord a => Interaction' a -> a
$cminimum :: forall a. Ord a => Interaction' a -> a
maximum :: forall a. Ord a => Interaction' a -> a
$cmaximum :: forall a. Ord a => Interaction' a -> a
elem :: forall a. Eq a => a -> Interaction' a -> Bool
$celem :: forall a. Eq a => a -> Interaction' a -> Bool
length :: forall a. Interaction' a -> Int
$clength :: forall a. Interaction' a -> Int
null :: forall a. Interaction' a -> Bool
$cnull :: forall a. Interaction' a -> Bool
toList :: forall a. Interaction' a -> [a]
$ctoList :: forall a. Interaction' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Interaction' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Interaction' a -> a
foldr1 :: forall a. (a -> a -> a) -> Interaction' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Interaction' a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> Interaction' a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Interaction' a -> m
fold :: forall m. Monoid m => Interaction' m -> m
$cfold :: forall m. Monoid m => Interaction' m -> m
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)
sequence :: forall (m :: * -> *) a.
Monad m =>
Interaction' (m a) -> m (Interaction' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
Interaction' (m a) -> m (Interaction' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Interaction' a -> m (Interaction' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Interaction' a -> m (Interaction' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Interaction' (f a) -> f (Interaction' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Interaction' (f a) -> f (Interaction' a)
traverse :: 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)
Traversable)

type IOTCM = IOTCM' Range
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
showList :: [IOTCM' range] -> ShowS
$cshowList :: forall range. Show range => [IOTCM' range] -> ShowS
show :: IOTCM' range -> String
$cshow :: forall range. Show range => IOTCM' range -> String
showsPrec :: Int -> IOTCM' range -> ShowS
$cshowsPrec :: forall range. Show range => Int -> 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
readListPrec :: ReadPrec [IOTCM' range]
$creadListPrec :: forall range. Read range => ReadPrec [IOTCM' range]
readPrec :: ReadPrec (IOTCM' range)
$creadPrec :: forall range. Read range => ReadPrec (IOTCM' range)
readList :: ReadS [IOTCM' range]
$creadList :: forall range. Read range => ReadS [IOTCM' range]
readsPrec :: Int -> ReadS (IOTCM' range)
$creadsPrec :: forall range. Read range => Int -> ReadS (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
<$ :: forall a b. a -> IOTCM' b -> IOTCM' a
$c<$ :: forall a b. a -> IOTCM' b -> IOTCM' a
fmap :: forall a b. (a -> b) -> IOTCM' a -> IOTCM' b
$cfmap :: forall a b. (a -> b) -> IOTCM' a -> IOTCM' b
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
product :: forall a. Num a => IOTCM' a -> a
$cproduct :: forall a. Num a => IOTCM' a -> a
sum :: forall a. Num a => IOTCM' a -> a
$csum :: forall a. Num a => IOTCM' a -> a
minimum :: forall a. Ord a => IOTCM' a -> a
$cminimum :: forall a. Ord a => IOTCM' a -> a
maximum :: forall a. Ord a => IOTCM' a -> a
$cmaximum :: forall a. Ord a => IOTCM' a -> a
elem :: forall a. Eq a => a -> IOTCM' a -> Bool
$celem :: forall a. Eq a => a -> IOTCM' a -> Bool
length :: forall a. IOTCM' a -> Int
$clength :: forall a. IOTCM' a -> Int
null :: forall a. IOTCM' a -> Bool
$cnull :: forall a. IOTCM' a -> Bool
toList :: forall a. IOTCM' a -> [a]
$ctoList :: forall a. IOTCM' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
foldr1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> IOTCM' a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> IOTCM' a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> IOTCM' a -> m
fold :: forall m. Monoid m => IOTCM' m -> m
$cfold :: forall m. Monoid m => IOTCM' m -> m
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)
sequence :: forall (m :: * -> *) a. Monad m => IOTCM' (m a) -> m (IOTCM' a)
$csequence :: forall (m :: * -> *) a. Monad m => IOTCM' (m a) -> m (IOTCM' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> IOTCM' a -> m (IOTCM' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> IOTCM' a -> m (IOTCM' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
IOTCM' (f a) -> f (IOTCM' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
IOTCM' (f a) -> f (IOTCM' a)
traverse :: 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)
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
showList :: [Remove] -> ShowS
$cshowList :: [Remove] -> ShowS
show :: Remove -> String
$cshow :: Remove -> String
showsPrec :: Int -> Remove -> ShowS
$cshowsPrec :: Int -> 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
readListPrec :: ReadPrec [Remove]
$creadListPrec :: ReadPrec [Remove]
readPrec :: ReadPrec Remove
$creadPrec :: ReadPrec Remove
readList :: ReadS [Remove]
$creadList :: ReadS [Remove]
readsPrec :: Int -> ReadS Remove
$creadsPrec :: Int -> ReadS Remove
Read)




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


-- | 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
  String
st <- StateT String Identity String
-> ExceptT String (StateT String Identity) String
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 String -> Maybe (a, String)
f String
st of
    Maybe (a, String)
Nothing -> String -> Parse 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 (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 -> Parse 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 (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
"("
    a
x <- Parse a
p
    String -> ExceptT String (StateT String Identity) ()
exact String
")"
    a -> Parse a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
  Parse a -> Parse a -> Parse 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 (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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Range' a -> Parse (Range' 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"
        (Position' a -> Position' a -> Interval' a)
-> ExceptT String (StateT String Identity) (Position' a)
-> ExceptT String (StateT String Identity) (Position' a)
-> Parse (Interval' a)
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Position' a -> Position' a -> Interval' a
forall a. Position' a -> Position' a -> Interval' a
Interval ExceptT String (StateT String Identity) (Position' a)
forall a. Read a => Parse a
readParse ExceptT String (StateT String Identity) (Position' a)
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 (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

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 -> Int32 -> Int32 -> Int32 -> Position' a)
-> ExceptT String (StateT String Identity) a
-> ExceptT String (StateT String Identity) Int32
-> ExceptT String (StateT String Identity) Int32
-> ExceptT String (StateT String Identity) Int32
-> 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 -> Int32 -> Int32 -> Int32 -> Position' a
forall a. a -> Int32 -> Int32 -> Int32 -> Position' a
Pn ExceptT String (StateT String Identity) a
forall a. Read a => Parse a
readParse ExceptT String (StateT String Identity) Int32
forall a. Read a => Parse a
readParse ExceptT String (StateT String Identity) Int32
forall a. Read a => Parse a
readParse ExceptT String (StateT String Identity) Int32
forall a. Read a => Parse a
readParse

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

data CompilerBackend = LaTeX | QuickLaTeX | OtherBackend String
    deriving (CompilerBackend -> CompilerBackend -> Bool
(CompilerBackend -> CompilerBackend -> Bool)
-> (CompilerBackend -> CompilerBackend -> Bool)
-> Eq CompilerBackend
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CompilerBackend -> CompilerBackend -> Bool
$c/= :: CompilerBackend -> CompilerBackend -> Bool
== :: CompilerBackend -> CompilerBackend -> Bool
$c== :: 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 String
s -> String -> Doc
text String
s

instance Read CompilerBackend where
  readsPrec :: Int -> ReadS CompilerBackend
readsPrec Int
_ String
s = do
    (String
t, String
s) <- ReadS String
lex String
s
    let b :: CompilerBackend
b = case String
t of
              String
"LaTeX"      -> CompilerBackend
LaTeX
              String
"QuickLaTeX" -> CompilerBackend
QuickLaTeX
              String
_            -> String -> CompilerBackend
OtherBackend String
t
    (CompilerBackend, String) -> [(CompilerBackend, String)]
forall (m :: * -> *) a. Monad m => a -> m a
return (CompilerBackend
b, String
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
showList :: [Rewrite] -> ShowS
$cshowList :: [Rewrite] -> ShowS
show :: Rewrite -> String
$cshow :: Rewrite -> String
showsPrec :: Int -> Rewrite -> ShowS
$cshowsPrec :: Int -> 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
readListPrec :: ReadPrec [Rewrite]
$creadListPrec :: ReadPrec [Rewrite]
readPrec :: ReadPrec Rewrite
$creadPrec :: ReadPrec Rewrite
readList :: ReadS [Rewrite]
$creadList :: ReadS [Rewrite]
readsPrec :: Int -> ReadS Rewrite
$creadsPrec :: Int -> ReadS Rewrite
Read, Rewrite -> Rewrite -> Bool
(Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c== :: 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
min :: Rewrite -> Rewrite -> Rewrite
$cmin :: Rewrite -> Rewrite -> Rewrite
max :: Rewrite -> Rewrite -> Rewrite
$cmax :: Rewrite -> Rewrite -> Rewrite
>= :: Rewrite -> Rewrite -> Bool
$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
compare :: Rewrite -> Rewrite -> Ordering
$ccompare :: Rewrite -> Rewrite -> Ordering
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
showList :: [ComputeMode] -> ShowS
$cshowList :: [ComputeMode] -> ShowS
show :: ComputeMode -> String
$cshow :: ComputeMode -> String
showsPrec :: Int -> ComputeMode -> ShowS
$cshowsPrec :: Int -> 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
readListPrec :: ReadPrec [ComputeMode]
$creadListPrec :: ReadPrec [ComputeMode]
readPrec :: ReadPrec ComputeMode
$creadPrec :: ReadPrec ComputeMode
readList :: ReadS [ComputeMode]
$creadList :: ReadS [ComputeMode]
readsPrec :: Int -> ReadS ComputeMode
$creadsPrec :: Int -> ReadS ComputeMode
Read, ComputeMode -> ComputeMode -> Bool
(ComputeMode -> ComputeMode -> Bool)
-> (ComputeMode -> ComputeMode -> Bool) -> Eq ComputeMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ComputeMode -> ComputeMode -> Bool
$c/= :: ComputeMode -> ComputeMode -> Bool
== :: ComputeMode -> ComputeMode -> Bool
$c== :: 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
/= :: UseForce -> UseForce -> Bool
$c/= :: UseForce -> UseForce -> Bool
== :: UseForce -> UseForce -> Bool
$c== :: 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
readListPrec :: ReadPrec [UseForce]
$creadListPrec :: ReadPrec [UseForce]
readPrec :: ReadPrec UseForce
$creadPrec :: ReadPrec UseForce
readList :: ReadS [UseForce]
$creadList :: ReadS [UseForce]
readsPrec :: Int -> ReadS UseForce
$creadsPrec :: Int -> ReadS 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
showList :: [UseForce] -> ShowS
$cshowList :: [UseForce] -> ShowS
show :: UseForce -> String
$cshow :: UseForce -> String
showsPrec :: Int -> UseForce -> ShowS
$cshowsPrec :: Int -> UseForce -> ShowS
Show)

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

data OutputConstraint 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)]
      | PTSInstance b b
      | PostponedCheckFunDef QName a TCErr
      | CheckLock b b
      | UsableAtMod Modality b
  deriving ((forall a b.
 (a -> b) -> OutputConstraint a a -> OutputConstraint a b)
-> (forall a b. a -> OutputConstraint a b -> OutputConstraint a a)
-> Functor (OutputConstraint a)
forall a b. a -> OutputConstraint a b -> OutputConstraint a a
forall a b.
(a -> b) -> OutputConstraint a a -> OutputConstraint a b
forall a a b. a -> OutputConstraint a b -> OutputConstraint a a
forall a a b.
(a -> b) -> OutputConstraint a a -> OutputConstraint a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> OutputConstraint a b -> OutputConstraint a a
$c<$ :: forall a a b. a -> OutputConstraint a b -> OutputConstraint a a
fmap :: forall a b.
(a -> b) -> OutputConstraint a a -> OutputConstraint a b
$cfmap :: forall a a b.
(a -> b) -> OutputConstraint a a -> OutputConstraint a b
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