Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Base

Contents

- Orphan instances

Synopsis

- data CommandState = CommandState {
  - theInteractionPoints :: [InteractionId]
  - theCurrentFile :: Maybe CurrentFile
  - optionsOnReload :: CommandLineOptions
  - oldInteractionScopes :: !OldInteractionScopes
  - commandQueue :: !CommandQueue
  }
- type OldInteractionScopes = Map InteractionId ScopeInfo
- initCommandState :: CommandQueue -> CommandState
- data CurrentFile = CurrentFile {
  - currentFilePath :: AbsolutePath
  - currentFileModule :: TopLevelModuleName
  - currentFileArgs :: [String]
  - currentFileStamp :: ClockTime
  }
- type CommandM' = StateT CommandState
- data Command' a
  - = Command !a
  - | Done
  - | Error String
- type Command = Command' IOTCM
- type IOTCM = Maybe TopLevelModuleName -> IOTCM' Range
- data CommandQueue = CommandQueue {
  - commands :: !(TChan (Integer, Command))
  - abort :: !(TVar (Maybe Integer))
  }
- type Interaction = Interaction' Range
- data Interaction' range
  - = Cmd_load FilePath [String]
  - | Cmd_constraints
  - | Cmd_metas Rewrite
  - | Cmd_load_no_metas FilePath
  - | Cmd_show_module_contents_toplevel Rewrite String
  - | Cmd_search_about_toplevel Rewrite String
  - | Cmd_solveAll Rewrite
  - | Cmd_solveOne Rewrite InteractionId range String
  - | Cmd_autoOne Rewrite InteractionId range String
  - | Cmd_autoAll Rewrite
  - | Cmd_infer_toplevel Rewrite String
  - | Cmd_compute_toplevel ComputeMode String
  - | Cmd_compile CompilerBackend FilePath [String]
  - | Cmd_backend_top CompilerBackend String
  - | Cmd_backend_hole InteractionId range String CompilerBackend String
  - | Cmd_load_highlighting_info FilePath
  - | Cmd_tokenHighlighting FilePath Remove
  - | Cmd_highlight InteractionId range String
  - | ShowImplicitArgs Bool
  - | ToggleImplicitArgs
  - | ShowIrrelevantArgs Bool
  - | ToggleIrrelevantArgs
  - | 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
  - | Cmd_elaborate_give Rewrite InteractionId range String
  - | Cmd_goal_type_context Rewrite InteractionId range String
  - | Cmd_goal_type_context_infer Rewrite InteractionId range String
  - | Cmd_goal_type_context_check Rewrite InteractionId range String
  - | 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
  - | Cmd_show_version
  - | Cmd_abort
  - | Cmd_exit
- data IOTCM' range = IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)
- data Remove
  - = Remove
  - | Keep
- parseIOTCM :: String -> Either String IOTCM
- type Parse a = ExceptT String (StateT String Identity) a
- readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a
- parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)]
- exact :: String -> Parse ()
- readParse :: Read a => Parse a
- parens' :: Parse a -> Parse a
- data CompilerBackend
  - = LaTeX
  - | QuickLaTeX
  - | OtherBackend BackendName
- data Rewrite
  - = AsIs
  - | Instantiated
  - | HeadNormal
  - | Simplified
  - | Normalised
- data ComputeMode
  - = DefaultCompute
  - | HeadCompute
  - | IgnoreAbstract
  - | UseShowInstance
- data UseForce
  - = WithForce
  - | WithoutForce
- data OutputForm_boot tcErr a b = OutputForm Range [ProblemId] Blocker (OutputConstraint_boot tcErr a b)
- data OutputConstraint_boot tcErr a b
  - = OfType b a
  - | CmpInType Comparison a b b
  - | CmpElim [Polarity] a [b] [b]
  - | JustType b
  - | CmpTypes Comparison b b
  - | CmpLevels Comparison b b
  - | CmpTeles Comparison b b
  - | JustSort b
  - | CmpSorts Comparison b b
  - | Assign b a
  - | TypedAssign b a a
  - | PostponedCheckArgs b [a] a a
  - | IsEmptyType a
  - | SizeLtSat a
  - | FindInstanceOF b a [(a, a, a)]
  - | ResolveInstanceOF QName
  - | PTSInstance b b
  - | PostponedCheckFunDef QName a tcErr
  - | CheckLock b b
  - | DataSort QName b
  - | UsableAtMod Modality b
- data OutputConstraint' a b = OfType' {
  - ofName :: b
  - ofExpr :: a
  }
- data OutputContextEntry name ty val
  - = ContextVar name ty
  - | ContextLet name ty val

# Documentation

data CommandState Source #

Auxiliary state of an interactive computation.

Constructors

CommandState |

Fields

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

- theCurrentFile :: Maybe CurrentFile

  The file which the state applies to. Only stored if the module was successfully type checked (potentially with warnings).

- optionsOnReload :: CommandLineOptions

  Reset the options on each reload to these.

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

- commandQueue :: !CommandQueue

  The command queue.

  This queue should only be manipulated by `initialiseCommandQueue` and `maybeAbort`.

#### Instances

Instances details

EncodeTCM CommandState Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: CommandState -> TCM Value Source #
ToJSON CommandState Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: CommandState -> Value Source # toEncoding :: CommandState -> Encoding Source # toJSONList :: [CommandState] -> Value Source # toEncodingList :: [CommandState] -> Encoding Source # omitField :: CommandState -> Bool Source #

type OldInteractionScopes = Map InteractionId ScopeInfo Source #

initCommandState :: CommandQueue -> CommandState Source #

Initial auxiliary interaction state

data CurrentFile Source #

Information about the current main module.

Constructors

CurrentFile |

Fields

- currentFilePath :: AbsolutePath

  The file currently loaded into interaction.

- currentFileModule :: TopLevelModuleName

  The top-level module name of the currently loaded file.

- currentFileArgs :: [String]

  The arguments to Agda used for loading the file.

- currentFileStamp :: ClockTime

  The modification time stamp of the file when it was loaded.

#### Instances

Instances details

EncodeTCM CurrentFile Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: CurrentFile -> TCM Value Source #
ToJSON CurrentFile Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: CurrentFile -> Value Source # toEncoding :: CurrentFile -> Encoding Source # toJSONList :: [CurrentFile] -> Value Source # toEncodingList :: [CurrentFile] -> Encoding Source # omitField :: CurrentFile -> Bool Source #
Show CurrentFile Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> CurrentFile -> ShowS Source # show :: CurrentFile -> String Source # showList :: [CurrentFile] -> ShowS Source #

type CommandM' = StateT CommandState Source #

data Command' a Source #

A generalised command type.

Constructors

Command !a | A command.
Done | Stop processing commands.
Error String | An error message for a command that could not be parsed.

#### Instances

Instances details

Show a => Show (Command' a) Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Command' a -> ShowS Source # show :: Command' a -> String Source # showList :: [Command' a] -> ShowS Source #

type Command = Command' IOTCM Source #

IOTCM commands.

type IOTCM = Maybe TopLevelModuleName -> IOTCM' Range Source #

IOTCM commands.

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

data CommandQueue Source #

Command queues.

Constructors

CommandQueue |

Fields

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

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

type Interaction = Interaction' Range Source #

An interactive computation.

data Interaction' range Source #

Constructors

Cmd_load FilePath [String] | `cmd_load m argv` loads the module in file `m`, using `argv` as the command-line options.
Cmd_constraints |
Cmd_metas Rewrite | Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead.
Cmd_load_no_metas FilePath | Load a file and fail if there are any unsolved meta-variables. By default no output is generated if the command is successful. (This command was previously used in Agda's installation script (Setup.hs)).
Cmd_show_module_contents_toplevel Rewrite String | Shows all the top-level names in the given module, along with their types. Uses the top-level scope.
Cmd_search_about_toplevel Rewrite String | Shows all the top-level names in scope which mention all the given identifiers in their type.
Cmd_solveAll Rewrite | Solve (all goals / the goal at point) whose values are determined by the constraints.
Cmd_solveOne Rewrite InteractionId range String |
Cmd_autoOne Rewrite InteractionId range String | Solve (all goals / the goal at point) by using Mimer proof search.
Cmd_autoAll Rewrite |
Cmd_infer_toplevel Rewrite String | Parse the given expression (as if it were defined at the top-level of the current module) and infer its type.
Cmd_compute_toplevel ComputeMode 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_compile CompilerBackend 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_backend_top | Custom top-level command for backends.

Fields

- CompilerBackend

  which backend

- String

  arbitrary user payload

Cmd_backend_hole | Custom hole-level command for backends.

Fields

- InteractionId

  the hole's ID

- range

  range of the hole

- String

  text inside the hole

- CompilerBackend

  which backend

- String

  arbitrary payload

Cmd_load_highlighting_info FilePath

`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_tokenHighlighting FilePath Remove

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_highlight InteractionId range String | Tells Agda to compute highlighting information for the expression just spliced into an interaction point.
ShowImplicitArgs Bool | Tells Agda whether or not to show implicit arguments.
ToggleImplicitArgs | Toggle display of implicit arguments.
ShowIrrelevantArgs Bool | Tells Agda whether or not to show irrelevant arguments.
ToggleIrrelevantArgs | Toggle display of irrelevant arguments.
Cmd_give UseForce InteractionId range String | Goal commands If the range is `noRange`, then the string comes from the minibuffer rather than the goal.
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 |
Cmd_elaborate_give Rewrite InteractionId range String | Grabs the current goal's type and checks the expression in the hole against it. Returns the elaborated term.
Cmd_goal_type_context Rewrite InteractionId range String | Displays the current goal and context.
Cmd_goal_type_context_infer Rewrite InteractionId range String | Displays the current goal and context and infers the type of an expression.
Cmd_goal_type_context_check Rewrite InteractionId range String | Grabs the current goal's type and checks the expression in the hole against it.
Cmd_show_module_contents 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_make_case InteractionId range String |
Cmd_compute ComputeMode InteractionId range String |
Cmd_why_in_scope InteractionId range String |
Cmd_why_in_scope_toplevel String |
Cmd_show_version | Displays version of the running Agda
Cmd_abort | Abort the current computation. Does nothing if no computation is in progress.
Cmd_exit | Exit the program.

#### Instances

Instances details

Functor Interaction' Source # |
Instance details Defined in Agda.Interaction.Base Methods fmap :: (a -> b) -> Interaction' a -> Interaction' b Source # (<$) :: a -> Interaction' b -> Interaction' a Source #
Foldable Interaction' Source # |

Instance details

Defined in Agda.Interaction.Base

Methods

fold :: Monoid m => Interaction' m -> m Source #

foldMap :: Monoid m => (a -> m) -> Interaction' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> Interaction' a -> m Source #

foldr :: (a -> b -> b) -> b -> Interaction' a -> b Source #

foldr' :: (a -> b -> b) -> b -> Interaction' a -> b Source #

foldl :: (b -> a -> b) -> b -> Interaction' a -> b Source #

foldl' :: (b -> a -> b) -> b -> Interaction' a -> b Source #

foldr1 :: (a -> a -> a) -> Interaction' a -> a Source #

foldl1 :: (a -> a -> a) -> Interaction' a -> a Source #

toList :: Interaction' a -> [a] Source #

null :: Interaction' a -> Bool Source #

length :: Interaction' a -> Int Source #

elem :: Eq a => a -> Interaction' a -> Bool Source #

maximum :: Ord a => Interaction' a -> a Source #

minimum :: Ord a => Interaction' a -> a Source #

sum :: Num a => Interaction' a -> a Source #

product :: Num a => Interaction' a -> a Source #

Traversable Interaction' Source # |
Instance details Defined in Agda.Interaction.Base Methods traverse :: Applicative f => (a -> f b) -> Interaction' a -> f (Interaction' b) Source # sequenceA :: Applicative f => Interaction' (f a) -> f (Interaction' a) Source # mapM :: Monad m => (a -> m b) -> Interaction' a -> m (Interaction' b) Source # sequence :: Monad m => Interaction' (m a) -> m (Interaction' a) Source #
Read range => Read (Interaction' range) Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS (Interaction' range) Source # readList :: ReadS [Interaction' range] Source # readPrec :: ReadPrec (Interaction' range) Source # readListPrec :: ReadPrec [Interaction' range] Source #
Show range => Show (Interaction' range) Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Interaction' range -> ShowS Source # show :: Interaction' range -> String Source # showList :: [Interaction' range] -> ShowS Source #

data IOTCM' range Source #

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range) |

#### Instances

Instances details

Functor IOTCM' Source # |
Instance details Defined in Agda.Interaction.Base Methods fmap :: (a -> b) -> IOTCM' a -> IOTCM' b Source # (<$) :: a -> IOTCM' b -> IOTCM' a Source #
Foldable IOTCM' Source # |

Instance details

Defined in Agda.Interaction.Base

Methods

fold :: Monoid m => IOTCM' m -> m Source #

foldMap :: Monoid m => (a -> m) -> IOTCM' a -> m Source #

foldMap' :: Monoid m => (a -> m) -> IOTCM' a -> m Source #

foldr :: (a -> b -> b) -> b -> IOTCM' a -> b Source #

foldr' :: (a -> b -> b) -> b -> IOTCM' a -> b Source #

foldl :: (b -> a -> b) -> b -> IOTCM' a -> b Source #

foldl' :: (b -> a -> b) -> b -> IOTCM' a -> b Source #

foldr1 :: (a -> a -> a) -> IOTCM' a -> a Source #

foldl1 :: (a -> a -> a) -> IOTCM' a -> a Source #

toList :: IOTCM' a -> [a] Source #

null :: IOTCM' a -> Bool Source #

length :: IOTCM' a -> Int Source #

elem :: Eq a => a -> IOTCM' a -> Bool Source #

maximum :: Ord a => IOTCM' a -> a Source #

minimum :: Ord a => IOTCM' a -> a Source #

sum :: Num a => IOTCM' a -> a Source #

product :: Num a => IOTCM' a -> a Source #

Traversable IOTCM' Source # |
Instance details Defined in Agda.Interaction.Base Methods traverse :: Applicative f => (a -> f b) -> IOTCM' a -> f (IOTCM' b) Source # sequenceA :: Applicative f => IOTCM' (f a) -> f (IOTCM' a) Source # mapM :: Monad m => (a -> m b) -> IOTCM' a -> m (IOTCM' b) Source # sequence :: Monad m => IOTCM' (m a) -> m (IOTCM' a) Source #
Read range => Read (IOTCM' range) Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS (IOTCM' range) Source # readList :: ReadS [IOTCM' range] Source # readPrec :: ReadPrec (IOTCM' range) Source # readListPrec :: ReadPrec [IOTCM' range] Source #
Show range => Show (IOTCM' range) Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> IOTCM' range -> ShowS Source # show :: IOTCM' range -> String Source # showList :: [IOTCM' range] -> ShowS Source #

data Remove Source #

Used to indicate whether something should be removed or not.

Constructors

Remove |
Keep |

#### Instances

Instances details

Read Remove Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS Remove Source # readList :: ReadS [Remove] Source # readPrec :: ReadPrec Remove Source # readListPrec :: ReadPrec [Remove] Source #
Show Remove Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Remove -> ShowS Source # show :: Remove -> String Source # showList :: [Remove] -> ShowS Source #

parseIOTCM :: String -> Either String IOTCM Source #

An `IOTCM` parser.

If the parse fails, then an error message is returned.

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

The `Parse` monad. `StateT` state holds the remaining input.

readsToParse :: String -> (String -> Maybe (a, String)) -> Parse a Source #

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

parseToReadsPrec :: Parse a -> Int -> String -> [(a, String)] Source #

exact :: String -> Parse () Source #

Demand an exact string.

readParse :: Read a => Parse a Source #

parens' :: Parse a -> Parse a Source #

data CompilerBackend Source #

Available backends.

Constructors

LaTeX |
QuickLaTeX |
OtherBackend BackendName |

#### Instances

Instances details

Pretty CompilerBackend Source # |
Instance details Defined in Agda.Interaction.Base Methods pretty :: CompilerBackend -> Doc Source # prettyPrec :: Int -> CompilerBackend -> Doc Source # prettyList :: [CompilerBackend] -> Doc Source #
Read CompilerBackend Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS CompilerBackend Source # readList :: ReadS [CompilerBackend] Source # readPrec :: ReadPrec CompilerBackend Source # readListPrec :: ReadPrec [CompilerBackend] Source #
Show CompilerBackend Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> CompilerBackend -> ShowS Source # show :: CompilerBackend -> String Source # showList :: [CompilerBackend] -> ShowS Source #
Eq CompilerBackend Source # |
Instance details Defined in Agda.Interaction.Base Methods (==) :: CompilerBackend -> CompilerBackend -> Bool Source # (/=) :: CompilerBackend -> CompilerBackend -> Bool Source #

data Rewrite Source #

Ordered ascendingly by degree of normalization.

Constructors

AsIs |
Instantiated |
HeadNormal |
Simplified |
Normalised |

#### Instances

Instances details

EncodeTCM Rewrite Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Rewrite -> TCM Value Source #
ToJSON Rewrite Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Rewrite -> Value Source # toEncoding :: Rewrite -> Encoding Source # toJSONList :: [Rewrite] -> Value Source # toEncodingList :: [Rewrite] -> Encoding Source # omitField :: Rewrite -> Bool Source #
Read Rewrite Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS Rewrite Source # readList :: ReadS [Rewrite] Source # readPrec :: ReadPrec Rewrite Source # readListPrec :: ReadPrec [Rewrite] Source #
Show Rewrite Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Rewrite -> ShowS Source # show :: Rewrite -> String Source # showList :: [Rewrite] -> ShowS Source #
Eq Rewrite Source # |
Instance details Defined in Agda.Interaction.Base Methods (==) :: Rewrite -> Rewrite -> Bool Source # (/=) :: Rewrite -> Rewrite -> Bool Source #
Ord Rewrite Source # |
Instance details Defined in Agda.Interaction.Base Methods compare :: Rewrite -> Rewrite -> Ordering Source # (<) :: Rewrite -> Rewrite -> Bool Source # (<=) :: Rewrite -> Rewrite -> Bool Source # (>) :: Rewrite -> Rewrite -> Bool Source # (>=) :: Rewrite -> Rewrite -> Bool Source # max :: Rewrite -> Rewrite -> Rewrite Source # min :: Rewrite -> Rewrite -> Rewrite Source #

data ComputeMode Source #

Constructors

DefaultCompute |
HeadCompute |
IgnoreAbstract |
UseShowInstance |

#### Instances

Instances details

EncodeTCM ComputeMode Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ComputeMode -> TCM Value Source #
ToJSON ComputeMode Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: ComputeMode -> Value Source # toEncoding :: ComputeMode -> Encoding Source # toJSONList :: [ComputeMode] -> Value Source # toEncodingList :: [ComputeMode] -> Encoding Source # omitField :: ComputeMode -> Bool Source #
Read ComputeMode Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS ComputeMode Source # readList :: ReadS [ComputeMode] Source # readPrec :: ReadPrec ComputeMode Source # readListPrec :: ReadPrec [ComputeMode] Source #
Show ComputeMode Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> ComputeMode -> ShowS Source # show :: ComputeMode -> String Source # showList :: [ComputeMode] -> ShowS Source #
Eq ComputeMode Source # |
Instance details Defined in Agda.Interaction.Base Methods (==) :: ComputeMode -> ComputeMode -> Bool Source # (/=) :: ComputeMode -> ComputeMode -> Bool Source #

data UseForce Source #

Constructors

WithForce | Ignore additional checks, like termination/positivity...
WithoutForce | Don't ignore any checks.

#### Instances

Instances details

Read UseForce Source # |
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS UseForce Source # readList :: ReadS [UseForce] Source # readPrec :: ReadPrec UseForce Source # readListPrec :: ReadPrec [UseForce] Source #
Show UseForce Source # |
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> UseForce -> ShowS Source # show :: UseForce -> String Source # showList :: [UseForce] -> ShowS Source #
Eq UseForce Source # |
Instance details Defined in Agda.Interaction.Base Methods (==) :: UseForce -> UseForce -> Bool Source # (/=) :: UseForce -> UseForce -> Bool Source #

data OutputForm_boot tcErr a b Source #

Constructors

OutputForm Range [ProblemId] Blocker (OutputConstraint_boot tcErr a b) |

#### Instances

Instances details

EncodeTCM (OutputForm Expr Expr) Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: OutputForm Expr Expr -> TCM Value Source #
(Pretty a, Pretty b) => Pretty (OutputForm a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputForm a b -> Doc Source # prettyPrec :: Int -> OutputForm a b -> Doc Source # prettyList :: [OutputForm a b] -> Doc Source #
(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) Source # |

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b) |
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputForm a b -> m (ConOfAbs (OutputForm a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputForm a b -> (ConOfAbs (OutputForm a b) -> m b0) -> m b0 Source #

(Pretty a, Pretty b) => PrettyTCM (OutputForm a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods prettyTCM :: MonadPretty m => OutputForm a b -> m Doc Source #
Functor (OutputForm_boot tcErr a) Source # |
Instance details Defined in Agda.Interaction.Base Methods fmap :: (a0 -> b) -> OutputForm_boot tcErr a a0 -> OutputForm_boot tcErr a b Source # (<$) :: a0 -> OutputForm_boot tcErr a b -> OutputForm_boot tcErr a a0 Source #
type ConOfAbs (OutputForm a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)

data OutputConstraint_boot tcErr a b Source #

Constructors

OfType b a |
CmpInType Comparison a b b |
CmpElim [Polarity] a [b] [b] |
JustType b |
CmpTypes Comparison b b |
CmpLevels Comparison b b |
CmpTeles Comparison b b |
JustSort b |
CmpSorts Comparison b b |
Assign b a |
TypedAssign b a a |
PostponedCheckArgs b [a] a a |
IsEmptyType a |
SizeLtSat a |
FindInstanceOF b a [(a, a, a)] |
ResolveInstanceOF QName |
PTSInstance b b |
PostponedCheckFunDef QName a tcErr |
CheckLock b b |
DataSort QName b |
UsableAtMod Modality b |

#### Instances

Instances details

(Pretty a, Pretty b) => Pretty (OutputConstraint a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint a b -> Doc Source # prettyPrec :: Int -> OutputConstraint a b -> Doc Source # prettyList :: [OutputConstraint a b] -> Doc Source #
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) Source # |

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b) |
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputConstraint a b -> m (ConOfAbs (OutputConstraint a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> m b0) -> m b0 Source #

Functor (OutputConstraint_boot tcErr a) Source # |
Instance details Defined in Agda.Interaction.Base Methods fmap :: (a0 -> b) -> OutputConstraint_boot tcErr a a0 -> OutputConstraint_boot tcErr a b Source # (<$) :: a0 -> OutputConstraint_boot tcErr a b -> OutputConstraint_boot tcErr a a0 Source #
type ConOfAbs (OutputConstraint a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

data OutputConstraint' a b Source #

A subset of `OutputConstraint`.

Constructors

OfType' |

Fields

- ofName :: b
- ofExpr :: a

#### Instances

Instances details

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint' a b -> Doc Source # prettyPrec :: Int -> OutputConstraint' a b -> Doc Source # prettyList :: [OutputConstraint' a b] -> Doc Source #
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b) Source # |

Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b) |
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)

Methods

toConcrete :: MonadToConcrete m => OutputConstraint' a b -> m (ConOfAbs (OutputConstraint' a b)) Source #

bindToConcrete :: MonadToConcrete m => OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> m b0) -> m b0 Source #

type ConOfAbs (OutputConstraint' a b) Source # |
Instance details Defined in Agda.Interaction.BasicOps type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)

data OutputContextEntry name ty val Source #

Constructors

ContextVar name ty |
ContextLet name ty val |

# Orphan instances

Read InteractionId Source # |
Instance details Methods readsPrec :: Int -> ReadS InteractionId Source # readList :: ReadS [InteractionId] Source # readPrec :: ReadPrec InteractionId Source # readListPrec :: ReadPrec [InteractionId] Source #
Read RangeFile Source # | This instance fills in the `TopLevelModuleName`s using `Nothing`. Note that these occurrences of `Nothing` are "overwritten" by `parseIOTCM`.
Instance details Methods readsPrec :: Int -> ReadS RangeFile Source # readList :: ReadS [RangeFile] Source # readPrec :: ReadPrec RangeFile Source # readListPrec :: ReadPrec [RangeFile] Source #
Read AbsolutePath Source # |
Instance details Methods readsPrec :: Int -> ReadS AbsolutePath Source # readList :: ReadS [AbsolutePath] Source # readPrec :: ReadPrec AbsolutePath Source # readListPrec :: ReadPrec [AbsolutePath] Source #
Read a => Read (Interval' a) Source # |
Instance details Methods readsPrec :: Int -> ReadS (Interval' a) Source # readList :: ReadS [Interval' a] Source # readPrec :: ReadPrec (Interval' a) Source # readListPrec :: ReadPrec [Interval' a] Source #
Read a => Read (Position' a) Source # |
Instance details Methods readsPrec :: Int -> ReadS (Position' a) Source # readList :: ReadS [Position' a] Source # readPrec :: ReadPrec (Position' a) Source # readListPrec :: ReadPrec [Position' a] Source #
Read a => Read (Range' a) Source # | Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.
Instance details Methods readsPrec :: Int -> ReadS (Range' a) Source # readList :: ReadS [Range' a] Source # readPrec :: ReadPrec (Range' a) Source # readListPrec :: ReadPrec [Range' a] Source #