Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Base

Synopsis

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.

initCommandState :: CommandQueue -> CommandState Source #

Initial auxiliary interaction state

type CommandM = StateT CommandState TCM Source #

Monad for computing answers to interactive commands.

CommandM is TCM extended with state CommandState.

data CurrentFile Source #

Information about the current main module.

Constructors

CurrentFile 

Fields

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 #

show :: Command' a -> String #

showList :: [Command' a] -> ShowS #

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

Instances details
Foldable Interaction' Source # 
Instance details

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' Source # 
Instance details

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' Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

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

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

Read range => Read (Interaction' range) Source # 
Instance details

Defined in Agda.Interaction.Base

Show range => Show (Interaction' range) Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

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

show :: Interaction' range -> String #

showList :: [Interaction' range] -> ShowS #

data IOTCM' range Source #

Instances

Instances details
Foldable IOTCM' Source # 
Instance details

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' Source # 
Instance details

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' Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

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

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

Read range => Read (IOTCM' range) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Interaction.Base

Methods

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

show :: IOTCM' range -> String #

showList :: [IOTCM' range] -> ShowS #

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

Show Remove Source # 
Instance details

Defined in Agda.Interaction.Base

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.

exact :: String -> Parse () Source #

Demand an exact string.

data Rewrite Source #

Ordered ascendingly by degree of normalization.

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

Show UseForce Source # 
Instance details

Defined in Agda.Interaction.Base

Eq UseForce Source # 
Instance details

Defined in Agda.Interaction.Base

data OutputForm a b Source #

Instances

Instances details
Functor (OutputForm a) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Interaction.JSONTop

(Pretty a, Pretty b) => Pretty (OutputForm a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a, ToConcrete b) => ToConcrete (OutputForm a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputForm a b) 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 #

type ConOfAbs (OutputForm a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data OutputConstraint a b Source #

Instances

Instances details
Functor (OutputConstraint a) Source # 
Instance details

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) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

(ToConcrete a, ToConcrete b) => ToConcrete (OutputConstraint a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

Associated Types

type ConOfAbs (OutputConstraint a b) Source #

type ConOfAbs (OutputConstraint a b) Source # 
Instance details

Defined in Agda.Interaction.BasicOps

data OutputConstraint' a b Source #

A subset of OutputConstraint.

Constructors

OfType' 

Fields

data OutputContextEntry name ty val Source #

Constructors

ContextVar name ty 
ContextLet name ty val 

Orphan instances

Read InteractionId Source # 
Instance details

Read RangeFile Source #

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

Instance details

Read AbsolutePath Source # 
Instance details

Read a => Read (Interval' a) Source # 
Instance details

Read a => Read (Position' a) Source # 
Instance details

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