ModuleAgda-2.7.0.1Haskell2010

Agda.Interaction.Base

20 types
7 values

PackageAgda-2.7.0.1
Exports27
LanguageHaskell2010
LicenceMIT
SourceBase.hs

datadata CommandState

Auxiliary state of an interactive computation.

Constructors

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

Instances2ToJSON, EncodeTCM

ToJSON CommandStateDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
EncodeTCM CommandStateDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan

typetype OldInteractionScopes = Map InteractionId ScopeInfo

valueinitCommandState :: CommandQueue -> CommandState

Initial auxiliary interaction state

datadata CurrentFile

Information about the current main module.

Constructors

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

Instances3Show, ToJSON, EncodeTCM

Show CurrentFileDefined in Agda-2.7.0.1 · Agda.Interaction.Base
ToJSON CurrentFileDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
EncodeTCM CurrentFileDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan

datadata Command' a

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.

Instances1Show

Show a => Show (Command' a)Defined in Agda-2.7.0.1 · Agda.Interaction.Base

typetype Command = Command' IOTCM

IOTCM commands.

typetype IOTCM = Maybe TopLevelModuleName -> IOTCM' Range

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.

datadata CommandQueue

Command queues.

Constructors

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

typetype Interaction = Interaction' Range

An interactive computation.

datadata Interaction' range

Constructors

Cmd_load FilePath [String]
cmd_load m argv loads the module in file m, using argv as the command-line options.
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_constraints
Cmd_metas Rewrite
Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead.
Cmd_no_metas
A command that fails if there are any unsolved meta-variables. By default no output is generated if the command is successful.
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_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.

Instances5Functor, Foldable, Traversable, Read, Show

Functor Interaction'Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Foldable Interaction'Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Traversable Interaction'Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Read range => Read (Interaction' range)Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Show range => Show (Interaction' range)Defined in Agda-2.7.0.1 · Agda.Interaction.Base

datadata IOTCM' range

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)

Instances5Functor, Foldable, Traversable, Read, Show

Functor IOTCM'Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Foldable IOTCM'Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Traversable IOTCM'Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Read range => Read (IOTCM' range)Defined in Agda-2.7.0.1 · Agda.Interaction.Base
Show range => Show (IOTCM' range)Defined in Agda-2.7.0.1 · Agda.Interaction.Base

datadata Remove

Used to indicate whether something should be removed or not.

Remove Keep

Instances2Read, Show

Read RemoveDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Show RemoveDefined in Agda-2.7.0.1 · Agda.Interaction.Base

valueparseIOTCM :: String -> Either String IOTCM

An IOTCM parser.

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

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

The Parse monad. StateT state holds the remaining input.

valuereadsToParse :: String -> (String -> Maybe (a, String)) -> Parse a

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

valueparseToReadsPrec :: Parse a -> Int -> String -> [(a, String)]

valueexact :: String -> Parse ()

Demand an exact string.

valuereadParse :: Read a => Parse a

valueparens' :: Parse a -> Parse a

datadata CompilerBackend

Available backends.

Constructors

LaTeX
QuickLaTeX
OtherBackend String

Instances4Eq, Read, Show, Pretty

Eq CompilerBackendDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Read CompilerBackendDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Show CompilerBackendDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Pretty CompilerBackendDefined in Agda-2.7.0.1 · Agda.Interaction.Base

datadata Rewrite

Ordered ascendingly by degree of normalization.

AsIs Instantiated HeadNormal Simplified Normalised

Instances6Eq, Ord, Read, Show, ToJSON, EncodeTCM

Eq RewriteDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Ord RewriteDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Read RewriteDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Show RewriteDefined in Agda-2.7.0.1 · Agda.Interaction.Base
ToJSON RewriteDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
EncodeTCM RewriteDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan

datadata ComputeMode

DefaultCompute HeadCompute IgnoreAbstract UseShowInstance

Instances5Eq, Read, Show, ToJSON, EncodeTCM

Eq ComputeModeDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Read ComputeModeDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Show ComputeModeDefined in Agda-2.7.0.1 · Agda.Interaction.Base
ToJSON ComputeModeDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
EncodeTCM ComputeModeDefined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan

datadata UseForce

Constructors

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

Instances3Eq, Read, Show

Eq UseForceDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Read UseForceDefined in Agda-2.7.0.1 · Agda.Interaction.Base
Show UseForceDefined in Agda-2.7.0.1 · Agda.Interaction.Base

datadata OutputForm_boot tcErr a b

Constructors

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

Instances6Functor, Pretty, PrettyTCM, ToConcrete, EncodeTCM, ConOfAbs

Functor (OutputForm_boot tcErr a)Defined in Agda-2.7.0.1 · Agda.Interaction.Base
(Pretty a, Pretty b) => Pretty (OutputForm a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
(Pretty a, Pretty b) => PrettyTCM (OutputForm a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
EncodeTCM (OutputForm Expr Expr)Defined in Agda-2.7.0.1 · Agda.Interaction.JSONTop · orphan
type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan

datadata OutputConstraint_boot tcErr a b

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

Instances4Functor, Pretty, ToConcrete, ConOfAbs

Functor (OutputConstraint_boot tcErr a)Defined in Agda-2.7.0.1 · Agda.Interaction.Base
(Pretty a, Pretty b) => Pretty (OutputConstraint a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan

datadata OutputConstraint' a b

A subset of OutputConstraint.

Constructors

OfType'
- ofName :: b
- ofExpr :: a

Instances3Pretty, ToConcrete, ConOfAbs

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan
type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)Defined in Agda-2.7.0.1 · Agda.Interaction.BasicOps · orphan

datadata OutputContextEntry name ty val

Constructors

ContextVar name ty
ContextLet name ty val

Orphan instances

6 instances

Read InteractionId
Read RangeFile
This instance fills in the TopLevelModuleNames using Nothing. Note that these occurrences of Nothing are "overwritten" by parseIOTCM.
Read AbsolutePath
Read a => Read (Interval' a)
Read a => Read (Position' a)
Read a => Read (Range' a)
Note that the grammar implemented by this instance does not necessarily match the current representation of ranges.