{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DataKinds #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use camelCase" #-}

module Cornelis.Types.Agda where

import           Cornelis.Offsets
import           Data.Aeson (ToJSON, FromJSON)
import           Data.Foldable (toList)
import           Data.Sequence
import qualified Data.Sequence as Seq
import           Data.Text (Text)
import qualified Data.Text as T
import           GHC.Generics
import           GHC.Show (showSpace)

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, Int -> Rewrite
Rewrite -> Int
Rewrite -> [Rewrite]
Rewrite -> Rewrite
Rewrite -> Rewrite -> [Rewrite]
Rewrite -> Rewrite -> Rewrite -> [Rewrite]
(Rewrite -> Rewrite)
-> (Rewrite -> Rewrite)
-> (Int -> Rewrite)
-> (Rewrite -> Int)
-> (Rewrite -> [Rewrite])
-> (Rewrite -> Rewrite -> [Rewrite])
-> (Rewrite -> Rewrite -> [Rewrite])
-> (Rewrite -> Rewrite -> Rewrite -> [Rewrite])
-> Enum Rewrite
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Rewrite -> Rewrite
succ :: Rewrite -> Rewrite
$cpred :: Rewrite -> Rewrite
pred :: Rewrite -> Rewrite
$ctoEnum :: Int -> Rewrite
toEnum :: Int -> Rewrite
$cfromEnum :: Rewrite -> Int
fromEnum :: Rewrite -> Int
$cenumFrom :: Rewrite -> [Rewrite]
enumFrom :: Rewrite -> [Rewrite]
$cenumFromThen :: Rewrite -> Rewrite -> [Rewrite]
enumFromThen :: Rewrite -> Rewrite -> [Rewrite]
$cenumFromTo :: Rewrite -> Rewrite -> [Rewrite]
enumFromTo :: Rewrite -> Rewrite -> [Rewrite]
$cenumFromThenTo :: Rewrite -> Rewrite -> Rewrite -> [Rewrite]
enumFromThenTo :: Rewrite -> Rewrite -> Rewrite -> [Rewrite]
Enum, Rewrite
Rewrite -> Rewrite -> Bounded Rewrite
forall a. a -> a -> Bounded a
$cminBound :: Rewrite
minBound :: Rewrite
$cmaxBound :: Rewrite
maxBound :: Rewrite
Bounded)


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, Eq ComputeMode
Eq ComputeMode =>
(ComputeMode -> ComputeMode -> Ordering)
-> (ComputeMode -> ComputeMode -> Bool)
-> (ComputeMode -> ComputeMode -> Bool)
-> (ComputeMode -> ComputeMode -> Bool)
-> (ComputeMode -> ComputeMode -> Bool)
-> (ComputeMode -> ComputeMode -> ComputeMode)
-> (ComputeMode -> ComputeMode -> ComputeMode)
-> Ord ComputeMode
ComputeMode -> ComputeMode -> Bool
ComputeMode -> ComputeMode -> Ordering
ComputeMode -> ComputeMode -> ComputeMode
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 :: ComputeMode -> ComputeMode -> Ordering
compare :: ComputeMode -> ComputeMode -> Ordering
$c< :: ComputeMode -> ComputeMode -> Bool
< :: ComputeMode -> ComputeMode -> Bool
$c<= :: ComputeMode -> ComputeMode -> Bool
<= :: ComputeMode -> ComputeMode -> Bool
$c> :: ComputeMode -> ComputeMode -> Bool
> :: ComputeMode -> ComputeMode -> Bool
$c>= :: ComputeMode -> ComputeMode -> Bool
>= :: ComputeMode -> ComputeMode -> Bool
$cmax :: ComputeMode -> ComputeMode -> ComputeMode
max :: ComputeMode -> ComputeMode -> ComputeMode
$cmin :: ComputeMode -> ComputeMode -> ComputeMode
min :: ComputeMode -> ComputeMode -> ComputeMode
Ord, Int -> ComputeMode
ComputeMode -> Int
ComputeMode -> [ComputeMode]
ComputeMode -> ComputeMode
ComputeMode -> ComputeMode -> [ComputeMode]
ComputeMode -> ComputeMode -> ComputeMode -> [ComputeMode]
(ComputeMode -> ComputeMode)
-> (ComputeMode -> ComputeMode)
-> (Int -> ComputeMode)
-> (ComputeMode -> Int)
-> (ComputeMode -> [ComputeMode])
-> (ComputeMode -> ComputeMode -> [ComputeMode])
-> (ComputeMode -> ComputeMode -> [ComputeMode])
-> (ComputeMode -> ComputeMode -> ComputeMode -> [ComputeMode])
-> Enum ComputeMode
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ComputeMode -> ComputeMode
succ :: ComputeMode -> ComputeMode
$cpred :: ComputeMode -> ComputeMode
pred :: ComputeMode -> ComputeMode
$ctoEnum :: Int -> ComputeMode
toEnum :: Int -> ComputeMode
$cfromEnum :: ComputeMode -> Int
fromEnum :: ComputeMode -> Int
$cenumFrom :: ComputeMode -> [ComputeMode]
enumFrom :: ComputeMode -> [ComputeMode]
$cenumFromThen :: ComputeMode -> ComputeMode -> [ComputeMode]
enumFromThen :: ComputeMode -> ComputeMode -> [ComputeMode]
$cenumFromTo :: ComputeMode -> ComputeMode -> [ComputeMode]
enumFromTo :: ComputeMode -> ComputeMode -> [ComputeMode]
$cenumFromThenTo :: ComputeMode -> ComputeMode -> ComputeMode -> [ComputeMode]
enumFromThenTo :: ComputeMode -> ComputeMode -> ComputeMode -> [ComputeMode]
Enum, ComputeMode
ComputeMode -> ComputeMode -> Bounded ComputeMode
forall a. a -> a -> Bounded a
$cminBound :: ComputeMode
minBound :: ComputeMode
$cmaxBound :: ComputeMode
maxBound :: ComputeMode
Bounded)

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)


newtype InteractionId = InteractionId { InteractionId -> Int
interactionId :: Int }
  deriving newtype
           ( InteractionId -> InteractionId -> Bool
(InteractionId -> InteractionId -> Bool)
-> (InteractionId -> InteractionId -> Bool) -> Eq InteractionId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: InteractionId -> InteractionId -> Bool
== :: InteractionId -> InteractionId -> Bool
$c/= :: InteractionId -> InteractionId -> Bool
/= :: InteractionId -> InteractionId -> Bool
Eq
           , Eq InteractionId
Eq InteractionId =>
(InteractionId -> InteractionId -> Ordering)
-> (InteractionId -> InteractionId -> Bool)
-> (InteractionId -> InteractionId -> Bool)
-> (InteractionId -> InteractionId -> Bool)
-> (InteractionId -> InteractionId -> Bool)
-> (InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId -> InteractionId)
-> Ord InteractionId
InteractionId -> InteractionId -> Bool
InteractionId -> InteractionId -> Ordering
InteractionId -> InteractionId -> InteractionId
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 :: InteractionId -> InteractionId -> Ordering
compare :: InteractionId -> InteractionId -> Ordering
$c< :: InteractionId -> InteractionId -> Bool
< :: InteractionId -> InteractionId -> Bool
$c<= :: InteractionId -> InteractionId -> Bool
<= :: InteractionId -> InteractionId -> Bool
$c> :: InteractionId -> InteractionId -> Bool
> :: InteractionId -> InteractionId -> Bool
$c>= :: InteractionId -> InteractionId -> Bool
>= :: InteractionId -> InteractionId -> Bool
$cmax :: InteractionId -> InteractionId -> InteractionId
max :: InteractionId -> InteractionId -> InteractionId
$cmin :: InteractionId -> InteractionId -> InteractionId
min :: InteractionId -> InteractionId -> InteractionId
Ord
           , Int -> InteractionId -> ShowS
[InteractionId] -> ShowS
InteractionId -> String
(Int -> InteractionId -> ShowS)
-> (InteractionId -> String)
-> ([InteractionId] -> ShowS)
-> Show InteractionId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> InteractionId -> ShowS
showsPrec :: Int -> InteractionId -> ShowS
$cshow :: InteractionId -> String
show :: InteractionId -> String
$cshowList :: [InteractionId] -> ShowS
showList :: [InteractionId] -> ShowS
Show
           , ReadPrec [InteractionId]
ReadPrec InteractionId
Int -> ReadS InteractionId
ReadS [InteractionId]
(Int -> ReadS InteractionId)
-> ReadS [InteractionId]
-> ReadPrec InteractionId
-> ReadPrec [InteractionId]
-> Read InteractionId
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS InteractionId
readsPrec :: Int -> ReadS InteractionId
$creadList :: ReadS [InteractionId]
readList :: ReadS [InteractionId]
$creadPrec :: ReadPrec InteractionId
readPrec :: ReadPrec InteractionId
$creadListPrec :: ReadPrec [InteractionId]
readListPrec :: ReadPrec [InteractionId]
Read
           , Integer -> InteractionId
InteractionId -> InteractionId
InteractionId -> InteractionId -> InteractionId
(InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId)
-> (InteractionId -> InteractionId)
-> (InteractionId -> InteractionId)
-> (Integer -> InteractionId)
-> Num InteractionId
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: InteractionId -> InteractionId -> InteractionId
+ :: InteractionId -> InteractionId -> InteractionId
$c- :: InteractionId -> InteractionId -> InteractionId
- :: InteractionId -> InteractionId -> InteractionId
$c* :: InteractionId -> InteractionId -> InteractionId
* :: InteractionId -> InteractionId -> InteractionId
$cnegate :: InteractionId -> InteractionId
negate :: InteractionId -> InteractionId
$cabs :: InteractionId -> InteractionId
abs :: InteractionId -> InteractionId
$csignum :: InteractionId -> InteractionId
signum :: InteractionId -> InteractionId
$cfromInteger :: Integer -> InteractionId
fromInteger :: Integer -> InteractionId
Num
           , Enum InteractionId
Real InteractionId
(Real InteractionId, Enum InteractionId) =>
(InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId -> InteractionId)
-> (InteractionId -> InteractionId -> InteractionId)
-> (InteractionId
    -> InteractionId -> (InteractionId, InteractionId))
-> (InteractionId
    -> InteractionId -> (InteractionId, InteractionId))
-> (InteractionId -> Integer)
-> Integral InteractionId
InteractionId -> Integer
InteractionId -> InteractionId -> (InteractionId, InteractionId)
InteractionId -> InteractionId -> InteractionId
forall a.
(Real a, Enum a) =>
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
$cquot :: InteractionId -> InteractionId -> InteractionId
quot :: InteractionId -> InteractionId -> InteractionId
$crem :: InteractionId -> InteractionId -> InteractionId
rem :: InteractionId -> InteractionId -> InteractionId
$cdiv :: InteractionId -> InteractionId -> InteractionId
div :: InteractionId -> InteractionId -> InteractionId
$cmod :: InteractionId -> InteractionId -> InteractionId
mod :: InteractionId -> InteractionId -> InteractionId
$cquotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId)
quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId)
$cdivMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId)
divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId)
$ctoInteger :: InteractionId -> Integer
toInteger :: InteractionId -> Integer
Integral
           , Num InteractionId
Ord InteractionId
(Num InteractionId, Ord InteractionId) =>
(InteractionId -> Rational) -> Real InteractionId
InteractionId -> Rational
forall a. (Num a, Ord a) => (a -> Rational) -> Real a
$ctoRational :: InteractionId -> Rational
toRational :: InteractionId -> Rational
Real
           , Int -> InteractionId
InteractionId -> Int
InteractionId -> [InteractionId]
InteractionId -> InteractionId
InteractionId -> InteractionId -> [InteractionId]
InteractionId -> InteractionId -> InteractionId -> [InteractionId]
(InteractionId -> InteractionId)
-> (InteractionId -> InteractionId)
-> (Int -> InteractionId)
-> (InteractionId -> Int)
-> (InteractionId -> [InteractionId])
-> (InteractionId -> InteractionId -> [InteractionId])
-> (InteractionId -> InteractionId -> [InteractionId])
-> (InteractionId
    -> InteractionId -> InteractionId -> [InteractionId])
-> Enum InteractionId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: InteractionId -> InteractionId
succ :: InteractionId -> InteractionId
$cpred :: InteractionId -> InteractionId
pred :: InteractionId -> InteractionId
$ctoEnum :: Int -> InteractionId
toEnum :: Int -> InteractionId
$cfromEnum :: InteractionId -> Int
fromEnum :: InteractionId -> Int
$cenumFrom :: InteractionId -> [InteractionId]
enumFrom :: InteractionId -> [InteractionId]
$cenumFromThen :: InteractionId -> InteractionId -> [InteractionId]
enumFromThen :: InteractionId -> InteractionId -> [InteractionId]
$cenumFromTo :: InteractionId -> InteractionId -> [InteractionId]
enumFromTo :: InteractionId -> InteractionId -> [InteractionId]
$cenumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId]
enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId]
Enum
           , [InteractionId] -> Value
[InteractionId] -> Encoding
InteractionId -> Bool
InteractionId -> Value
InteractionId -> Encoding
(InteractionId -> Value)
-> (InteractionId -> Encoding)
-> ([InteractionId] -> Value)
-> ([InteractionId] -> Encoding)
-> (InteractionId -> Bool)
-> ToJSON InteractionId
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: InteractionId -> Value
toJSON :: InteractionId -> Value
$ctoEncoding :: InteractionId -> Encoding
toEncoding :: InteractionId -> Encoding
$ctoJSONList :: [InteractionId] -> Value
toJSONList :: [InteractionId] -> Value
$ctoEncodingList :: [InteractionId] -> Encoding
toEncodingList :: [InteractionId] -> Encoding
$comitField :: InteractionId -> Bool
omitField :: InteractionId -> Bool
ToJSON
           , Maybe InteractionId
Value -> Parser [InteractionId]
Value -> Parser InteractionId
(Value -> Parser InteractionId)
-> (Value -> Parser [InteractionId])
-> Maybe InteractionId
-> FromJSON InteractionId
forall a.
(Value -> Parser a)
-> (Value -> Parser [a]) -> Maybe a -> FromJSON a
$cparseJSON :: Value -> Parser InteractionId
parseJSON :: Value -> Parser InteractionId
$cparseJSONList :: Value -> Parser [InteractionId]
parseJSONList :: Value -> Parser [InteractionId]
$comittedField :: Maybe InteractionId
omittedField :: Maybe InteractionId
FromJSON
           )


-- | IOTCM commands.

type Command = Command' IOTCM

type IntervalWithoutFile = AgdaInterval

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

data Range' a
  = NoRange
  | Range !a (Seq IntervalWithoutFile)
  deriving
    (Range' a -> Range' a -> Bool
(Range' a -> Range' a -> Bool)
-> (Range' a -> Range' a -> Bool) -> Eq (Range' a)
forall a. Eq a => Range' a -> Range' a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Range' a -> Range' a -> Bool
== :: Range' a -> Range' a -> Bool
$c/= :: forall a. Eq a => Range' a -> Range' a -> Bool
/= :: Range' a -> Range' a -> Bool
Eq, Eq (Range' a)
Eq (Range' a) =>
(Range' a -> Range' a -> Ordering)
-> (Range' a -> Range' a -> Bool)
-> (Range' a -> Range' a -> Bool)
-> (Range' a -> Range' a -> Bool)
-> (Range' a -> Range' a -> Bool)
-> (Range' a -> Range' a -> Range' a)
-> (Range' a -> Range' a -> Range' a)
-> Ord (Range' a)
Range' a -> Range' a -> Bool
Range' a -> Range' a -> Ordering
Range' a -> Range' a -> Range' a
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
forall a. Ord a => Eq (Range' a)
forall a. Ord a => Range' a -> Range' a -> Bool
forall a. Ord a => Range' a -> Range' a -> Ordering
forall a. Ord a => Range' a -> Range' a -> Range' a
$ccompare :: forall a. Ord a => Range' a -> Range' a -> Ordering
compare :: Range' a -> Range' a -> Ordering
$c< :: forall a. Ord a => Range' a -> Range' a -> Bool
< :: Range' a -> Range' a -> Bool
$c<= :: forall a. Ord a => Range' a -> Range' a -> Bool
<= :: Range' a -> Range' a -> Bool
$c> :: forall a. Ord a => Range' a -> Range' a -> Bool
> :: Range' a -> Range' a -> Bool
$c>= :: forall a. Ord a => Range' a -> Range' a -> Bool
>= :: Range' a -> Range' a -> Bool
$cmax :: forall a. Ord a => Range' a -> Range' a -> Range' a
max :: Range' a -> Range' a -> Range' a
$cmin :: forall a. Ord a => Range' a -> Range' a -> Range' a
min :: Range' a -> Range' a -> Range' a
Ord, (forall a b. (a -> b) -> Range' a -> Range' b)
-> (forall a b. a -> Range' b -> Range' a) -> Functor Range'
forall a b. a -> Range' b -> Range' a
forall a b. (a -> b) -> Range' a -> Range' 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) -> Range' a -> Range' b
fmap :: forall a b. (a -> b) -> Range' a -> Range' b
$c<$ :: forall a b. a -> Range' b -> Range' a
<$ :: forall a b. a -> Range' b -> Range' a
Functor, (forall m. Monoid m => Range' m -> m)
-> (forall m a. Monoid m => (a -> m) -> Range' a -> m)
-> (forall m a. Monoid m => (a -> m) -> Range' a -> m)
-> (forall a b. (a -> b -> b) -> b -> Range' a -> b)
-> (forall a b. (a -> b -> b) -> b -> Range' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Range' a -> b)
-> (forall b a. (b -> a -> b) -> b -> Range' a -> b)
-> (forall a. (a -> a -> a) -> Range' a -> a)
-> (forall a. (a -> a -> a) -> Range' a -> a)
-> (forall a. Range' a -> [a])
-> (forall a. Range' a -> Bool)
-> (forall a. Range' a -> Int)
-> (forall a. Eq a => a -> Range' a -> Bool)
-> (forall a. Ord a => Range' a -> a)
-> (forall a. Ord a => Range' a -> a)
-> (forall a. Num a => Range' a -> a)
-> (forall a. Num a => Range' a -> a)
-> Foldable Range'
forall a. Eq a => a -> Range' a -> Bool
forall a. Num a => Range' a -> a
forall a. Ord a => Range' a -> a
forall m. Monoid m => Range' m -> m
forall a. Range' a -> Bool
forall a. Range' a -> Int
forall a. Range' a -> [a]
forall a. (a -> a -> a) -> Range' a -> a
forall m a. Monoid m => (a -> m) -> Range' a -> m
forall b a. (b -> a -> b) -> b -> Range' a -> b
forall a b. (a -> b -> b) -> b -> Range' 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 => Range' m -> m
fold :: forall m. Monoid m => Range' m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Range' a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Range' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Range' a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Range' a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Range' a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Range' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Range' a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Range' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Range' a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Range' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Range' a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Range' a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Range' a -> a
foldr1 :: forall a. (a -> a -> a) -> Range' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Range' a -> a
foldl1 :: forall a. (a -> a -> a) -> Range' a -> a
$ctoList :: forall a. Range' a -> [a]
toList :: forall a. Range' a -> [a]
$cnull :: forall a. Range' a -> Bool
null :: forall a. Range' a -> Bool
$clength :: forall a. Range' a -> Int
length :: forall a. Range' a -> Int
$celem :: forall a. Eq a => a -> Range' a -> Bool
elem :: forall a. Eq a => a -> Range' a -> Bool
$cmaximum :: forall a. Ord a => Range' a -> a
maximum :: forall a. Ord a => Range' a -> a
$cminimum :: forall a. Ord a => Range' a -> a
minimum :: forall a. Ord a => Range' a -> a
$csum :: forall a. Num a => Range' a -> a
sum :: forall a. Num a => Range' a -> a
$cproduct :: forall a. Num a => Range' a -> a
product :: forall a. Num a => Range' a -> a
Foldable, Functor Range'
Foldable Range'
(Functor Range', Foldable Range') =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Range' a -> f (Range' b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Range' (f a) -> f (Range' a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Range' a -> m (Range' b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Range' (m a) -> m (Range' a))
-> Traversable Range'
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 => Range' (m a) -> m (Range' a)
forall (f :: * -> *) a.
Applicative f =>
Range' (f a) -> f (Range' a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Range' a -> m (Range' b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Range' a -> f (Range' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Range' a -> f (Range' b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Range' a -> f (Range' b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Range' (f a) -> f (Range' a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Range' (f a) -> f (Range' a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Range' a -> m (Range' b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Range' a -> m (Range' b)
$csequence :: forall (m :: * -> *) a. Monad m => Range' (m a) -> m (Range' a)
sequence :: forall (m :: * -> *) a. Monad m => Range' (m a) -> m (Range' a)
Traversable, (forall x. Range' a -> Rep (Range' a) x)
-> (forall x. Rep (Range' a) x -> Range' a) -> Generic (Range' a)
forall x. Rep (Range' a) x -> Range' a
forall x. Range' a -> Rep (Range' a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Range' a) x -> Range' a
forall a x. Range' a -> Rep (Range' a) x
$cfrom :: forall a x. Range' a -> Rep (Range' a) x
from :: forall x. Range' a -> Rep (Range' a) x
$cto :: forall a x. Rep (Range' a) x -> Range' a
to :: forall x. Rep (Range' a) x -> Range' a
Generic)

instance Show a =>
         Show (Range' a) where
  showsPrec :: Int -> Range' a -> ShowS
showsPrec Int
_ Range' a
NoRange
    = String -> ShowS
showString String
"noRange"
  showsPrec
    Int
a_a1hOk
    (Cornelis.Types.Agda.Range a
b1_a1hOl Seq IntervalWithoutFile
b2_a1hOm)
    = Bool -> ShowS -> ShowS
showParen
        (Int
a_a1hOk Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11)
        (ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
           (String -> ShowS
showString String
"intervalsToRange ")
           (ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
              (Int -> a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 a
b1_a1hOl)
              (ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
                 ShowS
showSpace (Int -> [IntervalWithoutFile] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 ([IntervalWithoutFile] -> ShowS) -> [IntervalWithoutFile] -> ShowS
forall a b. (a -> b) -> a -> b
$ Seq IntervalWithoutFile -> [IntervalWithoutFile]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq IntervalWithoutFile
b2_a1hOm))))

type SrcFile = Maybe AbsolutePath

newtype AbsolutePath = AbsolutePath { AbsolutePath -> String
textPath :: String }
  deriving (AbsolutePath -> AbsolutePath -> Bool
(AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool) -> Eq AbsolutePath
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbsolutePath -> AbsolutePath -> Bool
== :: AbsolutePath -> AbsolutePath -> Bool
$c/= :: AbsolutePath -> AbsolutePath -> Bool
/= :: AbsolutePath -> AbsolutePath -> Bool
Eq, Eq AbsolutePath
Eq AbsolutePath =>
(AbsolutePath -> AbsolutePath -> Ordering)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> Bool)
-> (AbsolutePath -> AbsolutePath -> AbsolutePath)
-> (AbsolutePath -> AbsolutePath -> AbsolutePath)
-> Ord AbsolutePath
AbsolutePath -> AbsolutePath -> Bool
AbsolutePath -> AbsolutePath -> Ordering
AbsolutePath -> AbsolutePath -> AbsolutePath
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 :: AbsolutePath -> AbsolutePath -> Ordering
compare :: AbsolutePath -> AbsolutePath -> Ordering
$c< :: AbsolutePath -> AbsolutePath -> Bool
< :: AbsolutePath -> AbsolutePath -> Bool
$c<= :: AbsolutePath -> AbsolutePath -> Bool
<= :: AbsolutePath -> AbsolutePath -> Bool
$c> :: AbsolutePath -> AbsolutePath -> Bool
> :: AbsolutePath -> AbsolutePath -> Bool
$c>= :: AbsolutePath -> AbsolutePath -> Bool
>= :: AbsolutePath -> AbsolutePath -> Bool
$cmax :: AbsolutePath -> AbsolutePath -> AbsolutePath
max :: AbsolutePath -> AbsolutePath -> AbsolutePath
$cmin :: AbsolutePath -> AbsolutePath -> AbsolutePath
min :: AbsolutePath -> AbsolutePath -> AbsolutePath
Ord)

instance Show AbsolutePath where
  showsPrec :: Int -> AbsolutePath -> ShowS
showsPrec Int
n (AbsolutePath String
p) =
    Bool -> ShowS -> ShowS
showParen (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"mkAbsolute " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 String
p



type Range = Range' SrcFile

type IOTCM = IOTCM' Range
data IOTCM' range
    = IOTCM
        Text
         -- -^ 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)




data Interaction' range
    -- | @cmd_load m argv@ loads the module in file @m@, using
    -- @argv@ as the command-line options.
  = Cmd_load            Text [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
$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)

type Interaction = Interaction' Range

data HighlightingLevel
  = None
  | NonInteractive
  | Interactive
    -- ^ This includes both non-interactive highlighting and
    -- interactive highlighting of the expression that is currently
    -- being type-checked.
    deriving (HighlightingLevel -> HighlightingLevel -> Bool
(HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> Eq HighlightingLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HighlightingLevel -> HighlightingLevel -> Bool
== :: HighlightingLevel -> HighlightingLevel -> Bool
$c/= :: HighlightingLevel -> HighlightingLevel -> Bool
/= :: HighlightingLevel -> HighlightingLevel -> Bool
Eq, Eq HighlightingLevel
Eq HighlightingLevel =>
(HighlightingLevel -> HighlightingLevel -> Ordering)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> Bool)
-> (HighlightingLevel -> HighlightingLevel -> HighlightingLevel)
-> (HighlightingLevel -> HighlightingLevel -> HighlightingLevel)
-> Ord HighlightingLevel
HighlightingLevel -> HighlightingLevel -> Bool
HighlightingLevel -> HighlightingLevel -> Ordering
HighlightingLevel -> HighlightingLevel -> HighlightingLevel
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 :: HighlightingLevel -> HighlightingLevel -> Ordering
compare :: HighlightingLevel -> HighlightingLevel -> Ordering
$c< :: HighlightingLevel -> HighlightingLevel -> Bool
< :: HighlightingLevel -> HighlightingLevel -> Bool
$c<= :: HighlightingLevel -> HighlightingLevel -> Bool
<= :: HighlightingLevel -> HighlightingLevel -> Bool
$c> :: HighlightingLevel -> HighlightingLevel -> Bool
> :: HighlightingLevel -> HighlightingLevel -> Bool
$c>= :: HighlightingLevel -> HighlightingLevel -> Bool
>= :: HighlightingLevel -> HighlightingLevel -> Bool
$cmax :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
max :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
$cmin :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
min :: HighlightingLevel -> HighlightingLevel -> HighlightingLevel
Ord, Int -> HighlightingLevel -> ShowS
[HighlightingLevel] -> ShowS
HighlightingLevel -> String
(Int -> HighlightingLevel -> ShowS)
-> (HighlightingLevel -> String)
-> ([HighlightingLevel] -> ShowS)
-> Show HighlightingLevel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HighlightingLevel -> ShowS
showsPrec :: Int -> HighlightingLevel -> ShowS
$cshow :: HighlightingLevel -> String
show :: HighlightingLevel -> String
$cshowList :: [HighlightingLevel] -> ShowS
showList :: [HighlightingLevel] -> ShowS
Show, ReadPrec [HighlightingLevel]
ReadPrec HighlightingLevel
Int -> ReadS HighlightingLevel
ReadS [HighlightingLevel]
(Int -> ReadS HighlightingLevel)
-> ReadS [HighlightingLevel]
-> ReadPrec HighlightingLevel
-> ReadPrec [HighlightingLevel]
-> Read HighlightingLevel
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HighlightingLevel
readsPrec :: Int -> ReadS HighlightingLevel
$creadList :: ReadS [HighlightingLevel]
readList :: ReadS [HighlightingLevel]
$creadPrec :: ReadPrec HighlightingLevel
readPrec :: ReadPrec HighlightingLevel
$creadListPrec :: ReadPrec [HighlightingLevel]
readListPrec :: ReadPrec [HighlightingLevel]
Read, (forall x. HighlightingLevel -> Rep HighlightingLevel x)
-> (forall x. Rep HighlightingLevel x -> HighlightingLevel)
-> Generic HighlightingLevel
forall x. Rep HighlightingLevel x -> HighlightingLevel
forall x. HighlightingLevel -> Rep HighlightingLevel x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HighlightingLevel -> Rep HighlightingLevel x
from :: forall x. HighlightingLevel -> Rep HighlightingLevel x
$cto :: forall x. Rep HighlightingLevel x -> HighlightingLevel
to :: forall x. Rep HighlightingLevel x -> HighlightingLevel
Generic)

data HighlightingMethod
  = Direct
    -- ^ Via stdout.
  | Indirect
    -- ^ Both via files and via stdout.
    deriving (HighlightingMethod -> HighlightingMethod -> Bool
(HighlightingMethod -> HighlightingMethod -> Bool)
-> (HighlightingMethod -> HighlightingMethod -> Bool)
-> Eq HighlightingMethod
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HighlightingMethod -> HighlightingMethod -> Bool
== :: HighlightingMethod -> HighlightingMethod -> Bool
$c/= :: HighlightingMethod -> HighlightingMethod -> Bool
/= :: HighlightingMethod -> HighlightingMethod -> Bool
Eq, Int -> HighlightingMethod -> ShowS
[HighlightingMethod] -> ShowS
HighlightingMethod -> String
(Int -> HighlightingMethod -> ShowS)
-> (HighlightingMethod -> String)
-> ([HighlightingMethod] -> ShowS)
-> Show HighlightingMethod
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HighlightingMethod -> ShowS
showsPrec :: Int -> HighlightingMethod -> ShowS
$cshow :: HighlightingMethod -> String
show :: HighlightingMethod -> String
$cshowList :: [HighlightingMethod] -> ShowS
showList :: [HighlightingMethod] -> ShowS
Show, ReadPrec [HighlightingMethod]
ReadPrec HighlightingMethod
Int -> ReadS HighlightingMethod
ReadS [HighlightingMethod]
(Int -> ReadS HighlightingMethod)
-> ReadS [HighlightingMethod]
-> ReadPrec HighlightingMethod
-> ReadPrec [HighlightingMethod]
-> Read HighlightingMethod
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HighlightingMethod
readsPrec :: Int -> ReadS HighlightingMethod
$creadList :: ReadS [HighlightingMethod]
readList :: ReadS [HighlightingMethod]
$creadPrec :: ReadPrec HighlightingMethod
readPrec :: ReadPrec HighlightingMethod
$creadListPrec :: ReadPrec [HighlightingMethod]
readListPrec :: ReadPrec [HighlightingMethod]
Read, (forall x. HighlightingMethod -> Rep HighlightingMethod x)
-> (forall x. Rep HighlightingMethod x -> HighlightingMethod)
-> Generic HighlightingMethod
forall x. Rep HighlightingMethod x -> HighlightingMethod
forall x. HighlightingMethod -> Rep HighlightingMethod x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. HighlightingMethod -> Rep HighlightingMethod x
from :: forall x. HighlightingMethod -> Rep HighlightingMethod x
$cto :: forall x. Rep HighlightingMethod x -> HighlightingMethod
to :: forall x. Rep HighlightingMethod x -> HighlightingMethod
Generic)


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)

noRange :: Range' a
noRange :: forall a. Range' a
noRange = Range' a
forall a. Range' a
NoRange


-- | Converts a file name and an interval to a range.
intervalToRange :: a -> IntervalWithoutFile -> Range' a
intervalToRange :: forall a. a -> IntervalWithoutFile -> Range' a
intervalToRange a
f IntervalWithoutFile
i = a -> Seq IntervalWithoutFile -> Range' a
forall a. a -> Seq IntervalWithoutFile -> Range' a
Range a
f (IntervalWithoutFile -> Seq IntervalWithoutFile
forall a. a -> Seq a
Seq.singleton IntervalWithoutFile
i)


-- | Turns a file name plus a list of intervals into a range.
--
-- Precondition: 'consecutiveAndSeparated'.
intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a
intervalsToRange :: forall a. a -> [IntervalWithoutFile] -> Range' a
intervalsToRange a
_ [] = Range' a
forall a. Range' a
NoRange
intervalsToRange a
f [IntervalWithoutFile]
is = a -> Seq IntervalWithoutFile -> Range' a
forall a. a -> Seq IntervalWithoutFile -> Range' a
Range a
f ([IntervalWithoutFile] -> Seq IntervalWithoutFile
forall a. [a] -> Seq a
Seq.fromList [IntervalWithoutFile]
is)

mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range
mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range
mkAbsPathRnage = SrcFile -> IntervalWithoutFile -> Range
forall a. a -> IntervalWithoutFile -> Range' a
intervalToRange (SrcFile -> IntervalWithoutFile -> Range)
-> (Text -> SrcFile) -> Text -> IntervalWithoutFile -> Range
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> SrcFile
forall a. a -> Maybe a
Just (AbsolutePath -> SrcFile)
-> (Text -> AbsolutePath) -> Text -> SrcFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> AbsolutePath
AbsolutePath (String -> AbsolutePath)
-> (Text -> String) -> Text -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack