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

Agda.Interaction.GhciTop

Synopsis

- data State = State {
  - theTCState :: TCState
  - theInteractionPoints :: [InteractionId]
  - theCurrentFile :: Maybe (AbsolutePath, ClockTime)
  }
- initState :: State
- theState :: IORef State
- data Independence
  - = Independent (Maybe [FilePath])
  - | Dependent
- data Interaction = Interaction {
  - independence :: Independence
  - command :: TCM (Maybe ModuleName)
  }
- isIndependent :: Interaction -> Bool
- ioTCM_ :: TCM a -> IO a
- ioTCM :: FilePath -> Maybe FilePath -> Interaction -> IO ()
- cmd_load :: FilePath -> [FilePath] -> Interaction
- cmd_load' :: FilePath -> [FilePath] -> Bool -> ((Interface, Maybe Warnings) -> TCM ()) -> Interaction
- data Backend
  - = MAlonzo
  - | Epic
- cmd_compile :: Backend -> FilePath -> [FilePath] -> Interaction
- cmd_constraints :: Interaction
- cmd_metas :: Interaction
- type GoalCommand = InteractionId -> Range -> String -> Interaction
- cmd_give :: GoalCommand
- cmd_refine :: GoalCommand
- cmd_intro :: GoalCommand
- cmd_refine_or_intro :: GoalCommand
- cmd_auto :: GoalCommand
- sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
- prettyContext :: Rewrite -> Bool -> InteractionId -> TCM Doc
- cmd_context :: Rewrite -> GoalCommand
- cmd_infer :: Rewrite -> GoalCommand
- cmd_goal_type :: Rewrite -> GoalCommand
- cmd_goal_type_context :: Rewrite -> GoalCommand
- cmd_goal_type_context_infer :: Rewrite -> GoalCommand
- showModuleContents :: Range -> String -> TCM ()
- cmd_show_module_contents :: GoalCommand
- cmd_show_module_contents_toplevel :: String -> Interaction
- setCommandLineOptions :: CommandLineOptions -> TCM ()
- data Status = Status {
  - sShowImplicitArguments :: Bool
  - sChecked :: Bool
  }
- status :: TCM Status
- showStatus :: Status -> String
- displayStatus :: Status -> IO ()
- display_info' :: String -> String -> IO ()
- display_info :: String -> String -> TCM ()
- display_infoD :: String -> Doc -> TCM ()
- response :: Lisp String -> String
- data Lisp a
  - = A a
  - | L [Lisp a]
  - | Q (Lisp a)
  - | Cons (Lisp a) (Lisp a)
- takenNameStr :: TCM [String]
- refreshStr :: [String] -> String -> ([String], String)
- cmd_make_case :: GoalCommand
- cmd_solveAll :: Interaction
- class LowerMeta a where
  - lowerMeta :: a -> a
- cmd_compute :: Bool -> GoalCommand
- parseAndDoAtToplevel :: (Expr -> TCM Expr) -> String -> String -> Interaction
- cmd_infer_toplevel :: Rewrite -> String -> Interaction
- cmd_compute_toplevel :: Bool -> String -> Interaction
- cmd_write_highlighting_info :: FilePath -> FilePath -> Interaction
- tellEmacsToJumpToError :: Range -> IO ()
- showImplicitArgs :: Bool -> Interaction
- toggleImplicitArgs :: Interaction
- errorTitle :: String
- displayErrorAndExit :: Status -> Range -> String -> IO a
- ensureFileLoaded :: AbsolutePath -> TCM ()
- getCurrentFile :: IO FilePath
- makeSilent :: Interaction -> Interaction
- top_command' :: FilePath -> Interaction -> IO ()
- goal_command :: InteractionId -> GoalCommand -> String -> IO ()
- module Agda.TypeChecker
- module Agda.TypeChecking.MetaVars
- module Agda.TypeChecking.Reduce
- module Agda.TypeChecking.Errors
- module Agda.Syntax.Position
- module Agda.Syntax.Parser
- module Agda.Syntax.Scope.Base
- module Agda.Syntax.Scope.Monad
- module Agda.Syntax.Translation.ConcreteToAbstract
- module Agda.Syntax.Translation.AbstractToConcrete
- module Agda.Syntax.Translation.InternalToAbstract
- module Agda.Syntax.Abstract.Name
- module Agda.Interaction.Exceptions
- mkAbsolute :: FilePath -> AbsolutePath

# Documentation

data State

Constructors

State |

Fields

theTCState :: TCState
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 (AbsolutePath, ClockTime)

  The file which the state applies to. Only stored if the module was successfully type checked (potentially with warnings). The `ClockTime` is the modification time stamp of the file when it was last loaded.

initState :: State

theState :: IORef State

data Independence

Can the command run even if the relevant file has not been loaded into the state?

Constructors

Independent (Maybe [FilePath]) | Yes. If the argument is ``Just` is`, then `is` is used as the command's include directories.
Dependent |

data Interaction

An interactive computation.

Is the command independent?

Constructors

Interaction |

Fields

independence :: Independence

  Is the command independent?

command :: TCM (Maybe ModuleName)

  If a module name is returned, then syntax highlighting information will be written for the given module (by `ioTCM`).

isIndependent :: Interaction -> Bool

ioTCM_ :: TCM a -> IO a

Run a TCM computation in the current state. Should only be used for debugging.

ioTCM

Arguments

:: FilePath | The current file. If this file does not match `theCurrentFile`, and the `Interaction` is not "independent", then an error is raised.
-> Maybe FilePath | Syntax highlighting information will be written to this file, if any.
-> Interaction |
-> IO () |

Runs a `TCM` computation. All calls from the Emacs mode should be wrapped in this function.

cmd_load :: FilePath -> [FilePath] -> Interaction

`cmd_load m includes` loads the module in file `m`, using `includes` as the include directories.

cmd_load'

Arguments

:: FilePath |
-> [FilePath] |
-> Bool | Allow unsolved meta-variables?
-> ((Interface, Maybe Warnings) -> TCM ()) |
-> Interaction |

`cmd_load' m includes cmd cmd2` loads the module in file `m`, using `includes` as the include directories.

If type checking completes without any exceptions having been encountered then the command `cmd r` is executed, where `r` is the result of `typeCheck`.

data Backend

Available backends.

Constructors

MAlonzo |
Epic |

cmd_compile :: Backend -> FilePath -> [FilePath] -> Interaction

`cmd_compile b m includes` compiles the module in file `m` using the backend `b`, using `includes` as the include directories.

cmd_constraints :: Interaction

cmd_metas :: Interaction

type GoalCommand = InteractionId -> Range -> String -> Interaction

If the range is `noRange`, then the string comes from the minibuffer rather than the goal.

cmd_give :: GoalCommand

cmd_refine :: GoalCommand

cmd_intro :: GoalCommand

cmd_refine_or_intro :: GoalCommand

cmd_auto :: GoalCommand

sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]

Sorts interaction points based on their ranges.

prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc

Pretty-prints the type of the meta-variable.

prettyContext

Arguments

:: Rewrite | Normalise?
-> Bool | Print the elements in reverse order?
-> InteractionId |
-> TCM Doc |

Pretty-prints the context of the given meta-variable.

cmd_context :: Rewrite -> GoalCommand

cmd_infer :: Rewrite -> GoalCommand

cmd_goal_type :: Rewrite -> GoalCommand

cmd_goal_type_context :: Rewrite -> GoalCommand

Displays the current goal, the given document, and the current context.

Displays the current goal and context.

cmd_goal_type_context_infer :: Rewrite -> GoalCommand

Displays the current goal and context and infers the type of an expression.

showModuleContents :: Range -> String -> TCM ()

Shows all the top-level names in the given module, along with their types.

cmd_show_module_contents :: GoalCommand

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_toplevel :: String -> Interaction

Shows all the top-level names in the given module, along with their types. Uses the top-level scope.

setCommandLineOptions :: CommandLineOptions -> TCM ()

Sets the command line options and updates the status information.

data Status

Status information.

Constructors

Status |

Fields

sShowImplicitArguments :: Bool

  Are implicit arguments displayed?

sChecked :: Bool

  Has the module been successfully type checked?

status :: TCM Status

Computes some status information.

showStatus :: Status -> String

Shows status information.

displayStatus :: Status -> IO ()

Displays/updates status information.

display_info' :: String -> String -> IO ()

`display_info' header content` displays `content` (with header `header`) in some suitable way.

display_info :: String -> String -> TCM ()

`display_info` does what `display_info'` does, but additionally displays some status information (see `status` and `displayStatus`).

display_infoD :: String -> Doc -> TCM ()

Like `display_info`, but takes a `Doc` instead of a `String`.

response :: Lisp String -> String

Formats a response command.

data Lisp a

Constructors

A a |
L [Lisp a] |
Q (Lisp a) |
Cons (Lisp a) (Lisp a) |

Instances

Pretty a => Show (Lisp a) |
Pretty a => Pretty (Lisp a) |

takenNameStr :: TCM [String]

refreshStr :: [String] -> String -> ([String], String)

cmd_make_case :: GoalCommand

cmd_solveAll :: Interaction

class LowerMeta a where

Methods

lowerMeta :: a -> a

Instances

LowerMeta Declaration |
LowerMeta WhereClause |
LowerMeta RHS |
LowerMeta TypedBinding |
LowerMeta TypedBindings |
LowerMeta LamBinding |
LowerMeta Expr |
LowerMeta a => LowerMeta [a] |
LowerMeta a => LowerMeta (Arg a) |
LowerMeta a => LowerMeta (Named name a) |

cmd_compute

Arguments

:: Bool | Ignore abstract?
-> GoalCommand |

parseAndDoAtToplevel

Arguments

:: (Expr -> TCM Expr) | The command to perform.
-> String | The name to use for the buffer displaying the output.
-> String | The expression to parse.
-> Interaction |

Parses and scope checks an expression (using the "inside scope" as the scope), performs the given command with the expression as input, and displays the result.

cmd_infer_toplevel

Arguments

:: Rewrite | Normalise the type?
-> String |
-> Interaction |

Parse the given expression (as if it were defined at the top-level of the current module) and infer its type.

cmd_compute_toplevel

Arguments

:: Bool | Ignore abstract?
-> String |
-> Interaction |

Parse and type check the given expression (as if it were defined at the top-level of the current module) and normalise it.

cmd_write_highlighting_info :: FilePath -> FilePath -> Interaction

`cmd_write_highlighting_info source target` writes syntax highlighting information for the module in `source` into `target`.

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 the representation of "no highlighting information available" is instead written to `target`.

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.

tellEmacsToJumpToError :: Range -> IO ()

Tells the Emacs mode to go to the first error position (if any).

showImplicitArgs

Arguments

:: Bool | Show them?
-> Interaction |

Tells Agda whether or not to show implicit arguments.

toggleImplicitArgs :: Interaction

Toggle display of implicit arguments.

errorTitle :: String

When an error message is displayed the following title should be used, if appropriate.

displayErrorAndExit

Arguments

:: Status | The new status information.
-> Range |
-> String |
-> IO a |

Displays an error, instructs Emacs to jump to the site of the error, and terminates the program. Because this function may switch the focus to another file the status information is also updated.

ensureFileLoaded :: AbsolutePath -> TCM ()

Outermost error handler.

Raises an error if the given file is not the one currently loaded.

getCurrentFile :: IO FilePath

makeSilent :: Interaction -> Interaction

Changes the `Interaction` so that its first action is to turn off all debug messages.

top_command' :: FilePath -> Interaction -> IO ()

goal_command :: InteractionId -> GoalCommand -> String -> IO ()

module Agda.TypeChecker

module Agda.TypeChecking.MetaVars

module Agda.TypeChecking.Reduce

module Agda.TypeChecking.Errors

module Agda.Syntax.Position

module Agda.Syntax.Parser

module Agda.Syntax.Scope.Base

module Agda.Syntax.Scope.Monad

module Agda.Syntax.Translation.ConcreteToAbstract

module Agda.Syntax.Translation.AbstractToConcrete

module Agda.Syntax.Translation.InternalToAbstract

module Agda.Syntax.Abstract.Name

module Agda.Interaction.Exceptions

mkAbsolute :: FilePath -> AbsolutePath

Constructs `AbsolutePath`s.

Precondition: The path must be absolute and valid.