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

Safe Haskell | None

Agda.Interaction.InteractionTop

Synopsis

- data CommandState = CommandState {
  - theInteractionPoints :: [InteractionId]
  - theCurrentFile :: Maybe (AbsolutePath, ClockTime)
  - optionsOnReload :: CommandLineOptions
  }
- initCommandState :: CommandState
- newtype CommandM a = CommandM {
  - unCommandM :: StateT CommandState TCM a
  }
- runCommandM :: CommandM a -> CommandState -> TCM (a, CommandState)
- liftCommandM :: TCM a -> CommandM a
- revLift :: MonadState st m => (forall c. m c -> st -> k (c, st)) -> (forall b. k b -> m b) -> (forall x. (m a -> k x) -> k x) -> m a
- commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a
- runSafeTCM :: TCM a -> TCState -> IO (a, TCState)
- liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a
- putResponse :: Response -> CommandM ()
- runInteraction :: IOTCM -> CommandM ()
- data Interaction
  - = Cmd_load FilePath [FilePath]
  - | Cmd_compile Backend FilePath [FilePath]
  - | Cmd_constraints
  - | Cmd_metas
  - | Cmd_show_module_contents_toplevel String
  - | Cmd_solveAll
  - | Cmd_infer_toplevel Rewrite String
  - | Cmd_compute_toplevel Bool String
  - | Cmd_load_highlighting_info FilePath
  - | ShowImplicitArgs Bool
  - | ToggleImplicitArgs
  - | Cmd_give InteractionId Range String
  - | Cmd_refine InteractionId Range String
  - | Cmd_intro Bool InteractionId Range String
  - | Cmd_refine_or_intro Bool InteractionId Range String
  - | Cmd_auto InteractionId Range String
  - | Cmd_context Rewrite InteractionId Range String
  - | Cmd_infer Rewrite InteractionId Range String
  - | Cmd_goal_type Rewrite InteractionId Range String
  - | Cmd_goal_type_context Rewrite InteractionId Range String
  - | Cmd_goal_type_context_infer Rewrite InteractionId Range String
  - | Cmd_show_module_contents InteractionId Range String
  - | Cmd_make_case InteractionId Range String
  - | Cmd_compute Bool InteractionId Range String
- data IOTCM = IOTCM FilePath HighlightingLevel HighlightingMethod Interaction
- type Parse a = ErrorT 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
- independent :: Interaction -> Bool
- interpret :: Interaction -> CommandM ()
- type GoalCommand = InteractionId -> Range -> String -> Interaction
- cmd_load' :: FilePath -> [FilePath] -> Bool -> ((Interface, Maybe Warnings) -> CommandM ()) -> CommandM ()
- data Backend
  - = MAlonzo
  - | Epic
  - | JS
- give_gen :: InteractionId -> Range -> String -> (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> CommandM ()
- give_gen' :: (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> InteractionId -> Range -> String -> CommandM ()
- sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
- prettyContext :: Rewrite -> Bool -> InteractionId -> TCM Doc
- cmd_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> t -> t1 -> CommandM ()
- showModuleContents :: Range -> String -> CommandM ()
- setCommandLineOptions' :: CommandLineOptions -> CommandM ()
- status :: CommandM Status
- displayStatus :: CommandM ()
- display_info :: DisplayInfo -> CommandM ()
- takenNameStr :: TCM [String]
- refreshStr :: [String] -> String -> ([String], String)
- nameModifiers :: [[Char]]
- class LowerMeta a where
  - lowerMeta :: a -> a
- preMeta :: Expr
- preUscore :: Expr
- parseAndDoAtToplevel :: (Expr -> TCM Expr) -> (Doc -> DisplayInfo) -> String -> CommandM ()
- tellToUpdateHighlighting :: Maybe (HighlightingInfo, ModuleToSource) -> IO [Response]
- tellEmacsToJumpToError :: Range -> [Response]

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

optionsOnReload :: CommandLineOptions

  Reset the options on each reload to these.

Instances

MonadState CommandState CommandM |

initCommandState :: CommandState

Initial auxiliary interaction state

newtype CommandM a

Monad for computing answers to interactive commands.

`CommandM` is `TCM` extended with state `CommandState`.

`StateT` is in a newtype wrapper because we would like to prevent the accidental use of `lift`. Instead of `lift` one can use `liftCommandM`, see below.

Constructors

CommandM |

Fields

unCommandM :: StateT CommandState TCM a

Instances

Monad CommandM |
Functor CommandM |
MonadIO CommandM |
MonadError TCErr CommandM |
MonadState CommandState CommandM |

runCommandM :: CommandM a -> CommandState -> TCM (a, CommandState)

Wrapped `runStateT` for `CommandM`.

liftCommandM :: TCM a -> CommandM a

lift a TCM action to CommandM.

`liftCommandM` is a customized form of `lift` for `StateT`. At the end of the lifted action `stInteractionOutputCallback` is set to its original value because the value is lost during the execution of some TCM actions.

revLift

Arguments

:: MonadState st m |
=> (forall c. m c -> st -> k (c, st)) | run
-> (forall b. k b -> m b) | lift
-> (forall x. (m a -> k x) -> k x) |
-> m a | reverse lift in double negative position

Build an opposite action to `lift` for state monads.

commandMToIO :: (forall x. (CommandM a -> IO x) -> IO x) -> CommandM a

Opposite of `liftIO` for `CommandM`. Use only if main errors are already catched.

runSafeTCM :: TCM a -> TCState -> IO (a, TCState)

`runSafeTCM` runs a safe `TMC` action (a `TCM` action which cannot fail)

liftCommandMT :: (forall a. TCM a -> TCM a) -> CommandM a -> CommandM a

Lift a TCM action transformer to a CommandM action transformer.

putResponse :: Response -> CommandM ()

Put a response by the callback function given by `stInteractionOutputCallback`.

runInteraction :: IOTCM -> CommandM ()

Run an `IOTCM` value, catch the exceptions, emit output

If an error happens the state of `CommandM` does not change, but stPersistent may change (which contains successfully loaded interfaces for example).

data Interaction

An interactive computation.

Constructors

Cmd_load FilePath [FilePath] | `cmd_load m includes` loads the module in file `m`, using `includes` as the include directories.
Cmd_compile Backend FilePath [FilePath] | `cmd_compile b m includes` compiles the module in file `m` using the backend `b`, using `includes` as the include directories.
Cmd_constraints |
Cmd_metas | Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead.
Cmd_show_module_contents_toplevel String | Shows all the top-level names in the given module, along with their types. Uses the top-level scope.
Cmd_solveAll |
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 Bool 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.

ShowImplicitArgs Bool | Tells Agda whether or not to show implicit arguments.
ToggleImplicitArgs | Toggle display of implicit arguments.
Cmd_give 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_auto InteractionId Range String |
Cmd_context Rewrite InteractionId Range String |
Cmd_infer Rewrite InteractionId Range String |
Cmd_goal_type Rewrite InteractionId Range String |
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_show_module_contents 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 Bool InteractionId Range String |

Instances

Read Interaction |

data IOTCM

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod Interaction |

Instances

Read IOTCM |

type Parse a = ErrorT 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

independent :: Interaction -> Bool

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

interpret :: Interaction -> CommandM ()

Interpret an interaction

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

cmd_load'

Arguments

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

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

Instances

Read Backend |
Show Backend |

give_gen :: InteractionId -> Range -> String -> (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> CommandM ()

give_gen' :: (InteractionId -> Maybe Range -> Expr -> TCMT IO (Expr, [InteractionId])) -> (Range -> String -> Expr -> GiveResult) -> InteractionId -> Range -> String -> CommandM ()

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_goal_type_context_and :: Doc -> Rewrite -> InteractionId -> t -> t1 -> CommandM ()

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

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

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

setCommandLineOptions' :: CommandLineOptions -> CommandM ()

Sets the command line options and updates the status information.

status :: CommandM Status

Computes some status information.

displayStatus :: CommandM ()

Displays/updates status information.

display_info :: DisplayInfo -> CommandM ()

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

takenNameStr :: TCM [String]

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

nameModifiers :: [[Char]]

class LowerMeta a where

Methods

lowerMeta :: a -> a

Instances

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

preMeta :: Expr

preUscore :: Expr

parseAndDoAtToplevel

Arguments

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

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.

tellToUpdateHighlighting :: Maybe (HighlightingInfo, ModuleToSource) -> IO [Response]

Tell to highlight the code using the given highlighting info (unless it is `Nothing`).

tellEmacsToJumpToError :: Range -> [Response]

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