Agda.Interaction.Base

Documentation

data CommandState

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

EncodeTCM CommandState

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: CommandState -> TCM Value

ToJSON CommandState

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: CommandState -> Value

toEncoding :: CommandState -> Encoding

toJSONList :: [CommandState] -> Value

toEncodingList :: [CommandState] -> Encoding

omitField :: CommandState -> Bool

type OldInteractionScopes = Map InteractionId ScopeInfo

initCommandState :: CommandQueue -> CommandState

Initial auxiliary interaction state

type CommandM = StateT CommandState TCM

Monad for computing answers to interactive commands.

CommandM is TCM extended with state CommandState.

data CurrentFile

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

EncodeTCM CurrentFile

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: CurrentFile -> TCM Value

Show CurrentFile

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> CurrentFile -> ShowS

show :: CurrentFile -> String

showList :: [CurrentFile] -> ShowS

ToJSON CurrentFile

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: CurrentFile -> Value

toEncoding :: CurrentFile -> Encoding

toJSONList :: [CurrentFile] -> Value

toEncodingList :: [CurrentFile] -> Encoding

omitField :: CurrentFile -> Bool

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

Instances

Show a => Show (Command' a)

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> Command' a -> ShowS

show :: Command' a -> String

showList :: [Command' a] -> ShowS

type Command = Command' IOTCM

IOTCM commands.

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

data CommandQueue

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

An interactive computation.

data 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 InteractionId range String

Solve (all goals / the goal at point) by using Auto.

Cmd_autoAll

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.

Instances

Foldable Interaction'

Defined in Agda.Interaction.Base

Methods

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

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

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

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

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

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

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

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

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

toList :: Interaction' a -> [a]

null :: Interaction' a -> Bool

length :: Interaction' a -> Int

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

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

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

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

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

Traversable Interaction'

Defined in Agda.Interaction.Base

Methods

traverse :: Applicative f => (a -> f b) -> Interaction' a -> f (Interaction' b)

sequenceA :: Applicative f => Interaction' (f a) -> f (Interaction' a)

mapM :: Monad m => (a -> m b) -> Interaction' a -> m (Interaction' b)

sequence :: Monad m => Interaction' (m a) -> m (Interaction' a)

Functor Interaction'

Defined in Agda.Interaction.Base

Methods

fmap :: (a -> b) -> Interaction' a -> Interaction' b

(<$) :: a -> Interaction' b -> Interaction' a

Read range => Read (Interaction' range)

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (Interaction' range)

readList :: ReadS [Interaction' range]

readPrec :: ReadPrec (Interaction' range)

readListPrec :: ReadPrec [Interaction' range]

Show range => Show (Interaction' range)

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> Interaction' range -> ShowS

show :: Interaction' range -> String

showList :: [Interaction' range] -> ShowS

data IOTCM' range

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)

Instances

Foldable IOTCM'

Defined in Agda.Interaction.Base

Methods

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

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

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

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

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

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

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

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

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

toList :: IOTCM' a -> [a]

null :: IOTCM' a -> Bool

length :: IOTCM' a -> Int

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

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

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

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

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

Traversable IOTCM'

Defined in Agda.Interaction.Base

Methods

traverse :: Applicative f => (a -> f b) -> IOTCM' a -> f (IOTCM' b)

sequenceA :: Applicative f => IOTCM' (f a) -> f (IOTCM' a)

mapM :: Monad m => (a -> m b) -> IOTCM' a -> m (IOTCM' b)

sequence :: Monad m => IOTCM' (m a) -> m (IOTCM' a)

Functor IOTCM'

Defined in Agda.Interaction.Base

Methods

fmap :: (a -> b) -> IOTCM' a -> IOTCM' b

(<$) :: a -> IOTCM' b -> IOTCM' a

Read range => Read (IOTCM' range)

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS (IOTCM' range)

readList :: ReadS [IOTCM' range]

readPrec :: ReadPrec (IOTCM' range)

readListPrec :: ReadPrec [IOTCM' range]

Show range => Show (IOTCM' range)

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> IOTCM' range -> ShowS

show :: IOTCM' range -> String

showList :: [IOTCM' range] -> ShowS

data Remove

Used to indicate whether something should be removed or not.

Constructors

Remove

Keep

Instances

Read Remove

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS Remove

readList :: ReadS [Remove]

readPrec :: ReadPrec Remove

readListPrec :: ReadPrec [Remove]

Show Remove

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> Remove -> ShowS

show :: Remove -> String

showList :: [Remove] -> ShowS

parseIOTCM :: String -> Either String IOTCM

An IOTCM parser.

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

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

The Parse monad. StateT state holds the remaining input.

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

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

exact :: String -> Parse ()

Demand an exact string.

readParse :: Read a => Parse a

parens' :: Parse a -> Parse a

data CompilerBackend

Available backends.

Constructors

LaTeX

QuickLaTeX

OtherBackend String

Instances

Pretty CompilerBackend

Defined in Agda.Interaction.Base

Methods

pretty :: CompilerBackend -> Doc

prettyPrec :: Int -> CompilerBackend -> Doc

prettyList :: [CompilerBackend] -> Doc

Read CompilerBackend

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS CompilerBackend

readList :: ReadS [CompilerBackend]

readPrec :: ReadPrec CompilerBackend

readListPrec :: ReadPrec [CompilerBackend]

Show CompilerBackend

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> CompilerBackend -> ShowS

show :: CompilerBackend -> String

showList :: [CompilerBackend] -> ShowS

Eq CompilerBackend

Defined in Agda.Interaction.Base

Methods

(==) :: CompilerBackend -> CompilerBackend -> Bool

(/=) :: CompilerBackend -> CompilerBackend -> Bool

data Rewrite

Ordered ascendingly by degree of normalization.

Constructors

AsIs

Instantiated

HeadNormal

Simplified

Normalised

Instances

EncodeTCM Rewrite

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: Rewrite -> TCM Value

Read Rewrite

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS Rewrite

readList :: ReadS [Rewrite]

readPrec :: ReadPrec Rewrite

readListPrec :: ReadPrec [Rewrite]

Show Rewrite

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> Rewrite -> ShowS

show :: Rewrite -> String

showList :: [Rewrite] -> ShowS

Eq Rewrite

Defined in Agda.Interaction.Base

Methods

(==) :: Rewrite -> Rewrite -> Bool

(/=) :: Rewrite -> Rewrite -> Bool

Ord Rewrite

Defined in Agda.Interaction.Base

Methods

compare :: Rewrite -> Rewrite -> Ordering

(<) :: Rewrite -> Rewrite -> Bool

(<=) :: Rewrite -> Rewrite -> Bool

(>) :: Rewrite -> Rewrite -> Bool

(>=) :: Rewrite -> Rewrite -> Bool

max :: Rewrite -> Rewrite -> Rewrite

min :: Rewrite -> Rewrite -> Rewrite

ToJSON Rewrite

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: Rewrite -> Value

toEncoding :: Rewrite -> Encoding

toJSONList :: [Rewrite] -> Value

toEncodingList :: [Rewrite] -> Encoding

omitField :: Rewrite -> Bool

data ComputeMode

Constructors

DefaultCompute

HeadCompute

IgnoreAbstract

UseShowInstance

Instances

EncodeTCM ComputeMode

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: ComputeMode -> TCM Value

Read ComputeMode

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS ComputeMode

readList :: ReadS [ComputeMode]

readPrec :: ReadPrec ComputeMode

readListPrec :: ReadPrec [ComputeMode]

Show ComputeMode

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> ComputeMode -> ShowS

show :: ComputeMode -> String

showList :: [ComputeMode] -> ShowS

Eq ComputeMode

Defined in Agda.Interaction.Base

Methods

(==) :: ComputeMode -> ComputeMode -> Bool

(/=) :: ComputeMode -> ComputeMode -> Bool

ToJSON ComputeMode

Defined in Agda.Interaction.JSONTop

Methods

toJSON :: ComputeMode -> Value

toEncoding :: ComputeMode -> Encoding

toJSONList :: [ComputeMode] -> Value

toEncodingList :: [ComputeMode] -> Encoding

omitField :: ComputeMode -> Bool

data UseForce

Constructors

WithForce

Ignore additional checks, like termination/positivity...

WithoutForce

Don't ignore any checks.

Instances

Read UseForce

Defined in Agda.Interaction.Base

Methods

readsPrec :: Int -> ReadS UseForce

readList :: ReadS [UseForce]

readPrec :: ReadPrec UseForce

readListPrec :: ReadPrec [UseForce]

Show UseForce

Defined in Agda.Interaction.Base

Methods

showsPrec :: Int -> UseForce -> ShowS

show :: UseForce -> String

showList :: [UseForce] -> ShowS

Eq UseForce

Defined in Agda.Interaction.Base

Methods

(==) :: UseForce -> UseForce -> Bool

(/=) :: UseForce -> UseForce -> Bool

data OutputForm a b

Constructors

OutputForm Range [ProblemId] Blocker (OutputConstraint a b)

Instances

Functor (OutputForm a)

Defined in Agda.Interaction.Base

Methods

fmap :: (a0 -> b) -> OutputForm a a0 -> OutputForm a b

(<$) :: a0 -> OutputForm a b -> OutputForm a a0

EncodeTCM (OutputForm Expr Expr)

Defined in Agda.Interaction.JSONTop

Methods

encodeTCM :: OutputForm Expr Expr -> TCM Value

(Pretty a, Pretty b) => Pretty (OutputForm a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputForm a b -> Doc

prettyPrec :: Int -> OutputForm a b -> Doc

prettyList :: [OutputForm a b] -> Doc

(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b)

Methods

toConcrete :: OutputForm a b -> AbsToCon (ConOfAbs (OutputForm a b))

bindToConcrete :: OutputForm a b -> (ConOfAbs (OutputForm a b) -> AbsToCon b0) -> AbsToCon b0

(Pretty a, Pretty b) => PrettyTCM (OutputForm a b)

Defined in Agda.Interaction.BasicOps

Methods

prettyTCM :: MonadPretty m => OutputForm a b -> m Doc

type ConOfAbs (OutputForm a b)

Defined in Agda.Interaction.BasicOps

type ConOfAbs (OutputForm a b) = OutputForm (ConOfAbs a) (ConOfAbs b)

data OutputConstraint 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)]

PTSInstance b b

PostponedCheckFunDef QName a TCErr

CheckLock b b

DataSort QName b

UsableAtMod Modality b

Instances

Functor (OutputConstraint a)

Defined in Agda.Interaction.Base

Methods

fmap :: (a0 -> b) -> OutputConstraint a a0 -> OutputConstraint a b

(<$) :: a0 -> OutputConstraint a b -> OutputConstraint a a0

(Pretty a, Pretty b) => Pretty (OutputConstraint a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint a b -> Doc

prettyPrec :: Int -> OutputConstraint a b -> Doc

prettyList :: [OutputConstraint a b] -> Doc

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b)

Methods

toConcrete :: OutputConstraint a b -> AbsToCon (ConOfAbs (OutputConstraint a b))

bindToConcrete :: OutputConstraint a b -> (ConOfAbs (OutputConstraint a b) -> AbsToCon b0) -> AbsToCon b0

type ConOfAbs (OutputConstraint a b)

Defined in Agda.Interaction.BasicOps

type ConOfAbs (OutputConstraint a b) = OutputConstraint (ConOfAbs a) (ConOfAbs b)

data OutputConstraint' a b

A subset of OutputConstraint.

Constructors

OfType'

Fields

• ofName :: b
• ofExpr :: a

Instances

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

Methods

pretty :: OutputConstraint' a b -> Doc

prettyPrec :: Int -> OutputConstraint' a b -> Doc

prettyList :: [OutputConstraint' a b] -> Doc

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint' a b)

Methods

toConcrete :: OutputConstraint' a b -> AbsToCon (ConOfAbs (OutputConstraint' a b))

bindToConcrete :: OutputConstraint' a b -> (ConOfAbs (OutputConstraint' a b) -> AbsToCon b0) -> AbsToCon b0

type ConOfAbs (OutputConstraint' a b)

Defined in Agda.Interaction.BasicOps

type ConOfAbs (OutputConstraint' a b) = OutputConstraint' (ConOfAbs a) (ConOfAbs b)

data OutputContextEntry name ty val

Constructors

ContextVar name ty

ContextLet name ty val

Orphan instances

Read InteractionId

Methods

readsPrec :: Int -> ReadS InteractionId

readList :: ReadS [InteractionId]

readPrec :: ReadPrec InteractionId

readListPrec :: ReadPrec [InteractionId]

Read RangeFile

This instance fills in the TopLevelModuleNames using Nothing. Note that these occurrences of Nothing are "overwritten" by parseIOTCM.

Methods

readsPrec :: Int -> ReadS RangeFile

readList :: ReadS [RangeFile]

readPrec :: ReadPrec RangeFile

readListPrec :: ReadPrec [RangeFile]

Read AbsolutePath

Methods

readsPrec :: Int -> ReadS AbsolutePath

readList :: ReadS [AbsolutePath]

readPrec :: ReadPrec AbsolutePath

readListPrec :: ReadPrec [AbsolutePath]

Read a => Read (Interval' a)

Methods

readsPrec :: Int -> ReadS (Interval' a)

readList :: ReadS [Interval' a]

readPrec :: ReadPrec (Interval' a)

readListPrec :: ReadPrec [Interval' a]

Read a => Read (Position' a)

Methods

readsPrec :: Int -> ReadS (Position' a)

readList :: ReadS [Position' a]

readPrec :: ReadPrec (Position' a)

readListPrec :: ReadPrec [Position' a]

Read a => Read (Range' a)

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

Methods

readsPrec :: Int -> ReadS (Range' a)

readList :: ReadS [Range' a]

readPrec :: ReadPrec (Range' a)

readListPrec :: ReadPrec [Range' a]