Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data Rewrite
- data ComputeMode
- data UseForce
- newtype InteractionId = InteractionId {
- interactionId :: Int
- type Command = Command' IOTCM
- type IntervalWithoutFile = AgdaInterval
- data Command' a
- data Range' a
- = NoRange
- | Range !a (Seq IntervalWithoutFile)
- type SrcFile = Maybe AbsolutePath
- newtype AbsolutePath = AbsolutePath {}
- type Range = Range' SrcFile
- type IOTCM = IOTCM' Range
- data IOTCM' range = IOTCM Text HighlightingLevel HighlightingMethod (Interaction' range)
- data Interaction' range
- = Cmd_load Text [String]
- | Cmd_constraints
- | Cmd_metas Rewrite
- | Cmd_show_module_contents_toplevel Rewrite String
- | Cmd_search_about_toplevel Rewrite String
- | Cmd_solveAll Rewrite
- | Cmd_solveOne Rewrite InteractionId range String
- | Cmd_autoOne InteractionId range String
- | Cmd_autoAll
- | Cmd_infer_toplevel Rewrite String
- | Cmd_compute_toplevel ComputeMode String
- | Cmd_load_highlighting_info FilePath
- | Cmd_tokenHighlighting FilePath Remove
- | Cmd_highlight InteractionId range String
- | ShowImplicitArgs Bool
- | ToggleImplicitArgs
- | ShowIrrelevantArgs Bool
- | ToggleIrrelevantArgs
- | Cmd_give UseForce InteractionId range String
- | 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
- | Cmd_goal_type_context Rewrite InteractionId range String
- | Cmd_goal_type_context_infer Rewrite InteractionId range String
- | Cmd_goal_type_context_check Rewrite InteractionId range String
- | Cmd_show_module_contents Rewrite InteractionId range String
- | 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
- | Cmd_abort
- | Cmd_exit
- type Interaction = Interaction' Range
- data HighlightingLevel
- data HighlightingMethod
- data Remove
- noRange :: Range' a
- intervalToRange :: a -> IntervalWithoutFile -> Range' a
- intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a
- mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range
Documentation
Instances
Bounded Rewrite Source # | |
Enum Rewrite Source # | |
Read Rewrite Source # | |
Show Rewrite Source # | |
Eq Rewrite Source # | |
Ord Rewrite Source # | |
data ComputeMode Source #
Instances
WithForce | Ignore additional checks, like termination/positivity... |
WithoutForce | Don't ignore any checks. |
newtype InteractionId Source #
Instances
type IntervalWithoutFile = AgdaInterval Source #
Instances
type SrcFile = Maybe AbsolutePath Source #
newtype AbsolutePath Source #
Instances
Show AbsolutePath Source # | |
Defined in Cornelis.Types.Agda showsPrec :: Int -> AbsolutePath -> ShowS # show :: AbsolutePath -> String # showList :: [AbsolutePath] -> ShowS # | |
Eq AbsolutePath Source # | |
Defined in Cornelis.Types.Agda (==) :: AbsolutePath -> AbsolutePath -> Bool # (/=) :: AbsolutePath -> AbsolutePath -> Bool # | |
Ord AbsolutePath Source # | |
Defined in Cornelis.Types.Agda compare :: AbsolutePath -> AbsolutePath -> Ordering # (<) :: AbsolutePath -> AbsolutePath -> Bool # (<=) :: AbsolutePath -> AbsolutePath -> Bool # (>) :: AbsolutePath -> AbsolutePath -> Bool # (>=) :: AbsolutePath -> AbsolutePath -> Bool # max :: AbsolutePath -> AbsolutePath -> AbsolutePath # min :: AbsolutePath -> AbsolutePath -> AbsolutePath # |
Instances
Foldable IOTCM' Source # | |
Defined in Cornelis.Types.Agda 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 # elem :: Eq a => a -> IOTCM' a -> Bool # maximum :: Ord a => IOTCM' a -> a # minimum :: Ord a => IOTCM' a -> a # | |
Traversable IOTCM' Source # | |
Functor IOTCM' Source # | |
Read range => Read (IOTCM' range) Source # | |
Show range => Show (IOTCM' range) Source # | |
data Interaction' range Source #
Cmd_load Text [String] |
|
Cmd_constraints | |
Cmd_metas Rewrite | Show unsolved metas. If there are no unsolved metas but unsolved constraints show those instead. |
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 |
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 |
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 |
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
type Interaction = Interaction' Range Source #
data HighlightingLevel Source #
None | |
NonInteractive | |
Interactive | This includes both non-interactive highlighting and interactive highlighting of the expression that is currently being type-checked. |
Instances
data HighlightingMethod Source #
Instances
Generic HighlightingMethod Source # | |
Defined in Cornelis.Types.Agda type Rep HighlightingMethod :: Type -> Type # from :: HighlightingMethod -> Rep HighlightingMethod x # to :: Rep HighlightingMethod x -> HighlightingMethod # | |
Read HighlightingMethod Source # | |
Defined in Cornelis.Types.Agda | |
Show HighlightingMethod Source # | |
Defined in Cornelis.Types.Agda showsPrec :: Int -> HighlightingMethod -> ShowS # show :: HighlightingMethod -> String # showList :: [HighlightingMethod] -> ShowS # | |
Eq HighlightingMethod Source # | |
Defined in Cornelis.Types.Agda (==) :: HighlightingMethod -> HighlightingMethod -> Bool # (/=) :: HighlightingMethod -> HighlightingMethod -> Bool # | |
type Rep HighlightingMethod Source # | |
intervalToRange :: a -> IntervalWithoutFile -> Range' a Source #
Converts a file name and an interval to a range.
intervalsToRange :: a -> [IntervalWithoutFile] -> Range' a Source #
Turns a file name plus a list of intervals into a range.
Precondition: consecutiveAndSeparated
.
mkAbsPathRnage :: Text -> IntervalWithoutFile -> Range Source #