Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Base

Contents

Orphan instances

Synopsis

data CommandState = CommandState {
- theInteractionPoints :: [InteractionId]
- theCurrentFile :: Maybe (AbsolutePath, ClockTime)
- optionsOnReload :: CommandLineOptions
- oldInteractionScopes :: !OldInteractionScopes
- commandQueue :: !CommandQueue
}
type OldInteractionScopes = Map InteractionId ScopeInfo
initCommandState :: CommandQueue -> CommandState
type CommandM = StateT CommandState TCM
data Command' a
- = Command !a
- | Done
- | Error String
type Command = Command' IOTCM
data CommandQueue = CommandQueue {
- commands :: !(TChan (Integer, Command))
- abort :: !(TVar (Maybe Integer))
}
type Interaction = Interaction' Range
data Interaction' range
- = Cmd_load FilePath [String]
- | Cmd_compile CompilerBackend FilePath [String]
- | Cmd_constraints
- | Cmd_metas
- | 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
- | 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 IOTCM = IOTCM' Range
data IOTCM' range = IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)
data Remove
- = Remove
- | Keep
type Parse a = ExceptT 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
data CompilerBackend
- = LaTeX
- | QuickLaTeX
- | OtherBackend String
data Rewrite
- = AsIs
- | Instantiated
- | HeadNormal
- | Simplified
- | Normalised
data ComputeMode
- = DefaultCompute
- | IgnoreAbstract
- | UseShowInstance
data UseForce
- = WithForce
- | WithoutForce
data OutputForm a b = OutputForm Range [ProblemId] (OutputConstraint a b)
data OutputConstraint a b
- = 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
- | Guard (OutputConstraint a b) ProblemId
- | Assign b a
- | TypedAssign b a a
- | PostponedCheckArgs b [a] a a
- | IsEmptyType a
- | SizeLtSat a
- | FindInstanceOF b a [(a, a)]
- | PTSInstance b b
- | PostponedCheckFunDef QName a
data OutputConstraint' a b = OfType' {
- ofName :: b
- ofExpr :: a
}
data OutputContextEntry name ty val
- = ContextVar name ty
- | ContextLet name ty val

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

Instances details

ToJSON CommandState
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: CommandState -> Value toEncoding :: CommandState -> Encoding toJSONList :: [CommandState] -> Value toEncodingList :: [CommandState] -> Encoding
EncodeTCM CommandState Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: CommandState -> TCM Value Source #

type OldInteractionScopes = Map InteractionId ScopeInfo Source #

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

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

Functor Interaction' Source #
Instance details Defined in Agda.Interaction.Base Methods fmap :: (a -> b) -> Interaction' a -> Interaction' b # (<$) :: a -> Interaction' b -> Interaction' a #
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) #
Read range => Read (Interaction' range) Source #
Instance details 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) Source #
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Interaction' range -> ShowS # show :: Interaction' range -> String # showList :: [Interaction' range] -> ShowS #

type IOTCM = IOTCM' Range Source #

data IOTCM' range Source #

Constructors

IOTCM FilePath HighlightingLevel HighlightingMethod (Interaction' range)

Instances

Instances details

Functor IOTCM' Source #
Instance details Defined in Agda.Interaction.Base Methods fmap :: (a -> b) -> IOTCM' a -> IOTCM' b # (<$) :: a -> IOTCM' b -> IOTCM' a #
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) #
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 Methods readsPrec :: Int -> ReadS Remove # readList :: ReadS [Remove] # readPrec :: ReadPrec Remove # readListPrec :: ReadPrec [Remove] #
Show Remove Source #
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Remove -> ShowS # show :: Remove -> String # showList :: [Remove] -> ShowS #

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.

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

exact :: String -> Parse () Source #

Demand an exact string.

readParse :: Read a => Parse a Source #

parens' :: Parse a -> Parse a Source #

data CompilerBackend Source #

Available backends.

Constructors

LaTeX
QuickLaTeX
OtherBackend String

Instances

Instances details

Eq CompilerBackend Source #
Instance details Defined in Agda.Interaction.Base Methods (==) :: CompilerBackend -> CompilerBackend -> Bool # (/=) :: CompilerBackend -> CompilerBackend -> Bool #
Read CompilerBackend Source #
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS CompilerBackend # readList :: ReadS [CompilerBackend] # readPrec :: ReadPrec CompilerBackend # readListPrec :: ReadPrec [CompilerBackend] #
Show CompilerBackend Source #
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> CompilerBackend -> ShowS # show :: CompilerBackend -> String # showList :: [CompilerBackend] -> ShowS #

data Rewrite Source #

Constructors

AsIs
Instantiated
HeadNormal
Simplified
Normalised

Instances

Instances details

Read Rewrite Source #
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS Rewrite # readList :: ReadS [Rewrite] # readPrec :: ReadPrec Rewrite # readListPrec :: ReadPrec [Rewrite] #
Show Rewrite Source #
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> Rewrite -> ShowS # show :: Rewrite -> String # showList :: [Rewrite] -> ShowS #
ToJSON Rewrite
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: Rewrite -> Value toEncoding :: Rewrite -> Encoding toJSONList :: [Rewrite] -> Value toEncodingList :: [Rewrite] -> Encoding
EncodeTCM Rewrite Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: Rewrite -> TCM Value Source #

data ComputeMode Source #

Constructors

DefaultCompute
IgnoreAbstract
UseShowInstance

Instances

Instances details

Eq ComputeMode Source #
Instance details Defined in Agda.Interaction.Base Methods (==) :: ComputeMode -> ComputeMode -> Bool # (/=) :: ComputeMode -> ComputeMode -> Bool #
Read ComputeMode Source #
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS ComputeMode # readList :: ReadS [ComputeMode] # readPrec :: ReadPrec ComputeMode # readListPrec :: ReadPrec [ComputeMode] #
Show ComputeMode Source #
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> ComputeMode -> ShowS # show :: ComputeMode -> String # showList :: [ComputeMode] -> ShowS #
ToJSON ComputeMode
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: ComputeMode -> Value toEncoding :: ComputeMode -> Encoding toJSONList :: [ComputeMode] -> Value toEncodingList :: [ComputeMode] -> Encoding
EncodeTCM ComputeMode Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: ComputeMode -> TCM Value Source #

data UseForce Source #

Constructors

WithForce	Ignore additional checks, like termination/positivity...
WithoutForce	Don't ignore any checks.

Instances

Instances details

Eq UseForce Source #
Instance details Defined in Agda.Interaction.Base Methods (==) :: UseForce -> UseForce -> Bool # (/=) :: UseForce -> UseForce -> Bool #
Read UseForce Source #
Instance details Defined in Agda.Interaction.Base Methods readsPrec :: Int -> ReadS UseForce # readList :: ReadS [UseForce] # readPrec :: ReadPrec UseForce # readListPrec :: ReadPrec [UseForce] #
Show UseForce Source #
Instance details Defined in Agda.Interaction.Base Methods showsPrec :: Int -> UseForce -> ShowS # show :: UseForce -> String # showList :: [UseForce] -> ShowS #

data OutputForm a b Source #

Constructors

OutputForm Range [ProblemId] (OutputConstraint a b)

Instances

Instances details

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: MonadReify m => ProblemConstraint -> m (Closure (OutputForm Expr Expr)) Source # reifyWhen :: MonadReify m => Bool -> ProblemConstraint -> m (Closure (OutputForm Expr Expr)) Source #
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 #
(Pretty a, Pretty b) => Pretty (OutputForm a b) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputForm a b -> Doc Source # prettyPrec :: Int -> OutputForm a b -> Doc Source # prettyList :: [OutputForm a b] -> Doc Source #
EncodeTCM (OutputForm Expr Expr) Source #
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: OutputForm Expr Expr -> TCM Value Source #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputForm a b -> AbsToCon (OutputForm c d) Source # bindToConcrete :: OutputForm a b -> (OutputForm c d -> AbsToCon b0) -> AbsToCon b0 Source #

data OutputConstraint a b Source #

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
Guard (OutputConstraint a b) ProblemId
Assign b a
TypedAssign b a a
PostponedCheckArgs b [a] a a
IsEmptyType a
SizeLtSat a
FindInstanceOF b a [(a, a)]
PTSInstance b b
PostponedCheckFunDef QName a

Instances

Instances details

Reify Constraint (OutputConstraint Expr Expr) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: MonadReify m => Constraint -> m (OutputConstraint Expr Expr) Source # reifyWhen :: MonadReify m => Bool -> Constraint -> m (OutputConstraint Expr Expr) Source #
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 Methods pretty :: OutputConstraint a b -> Doc Source # prettyPrec :: Int -> OutputConstraint a b -> Doc Source # prettyList :: [OutputConstraint a b] -> Doc Source #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint a b -> AbsToCon (OutputConstraint c d) Source # bindToConcrete :: OutputConstraint a b -> (OutputConstraint c d -> AbsToCon b0) -> AbsToCon b0 Source #

data OutputConstraint' a b Source #

A subset of OutputConstraint.

Constructors

OfType'
Fields ofName :: b ofExpr :: a

Instances

Instances details

(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods pretty :: OutputConstraint' a b -> Doc Source # prettyPrec :: Int -> OutputConstraint' a b -> Doc Source # prettyList :: [OutputConstraint' a b] -> Doc Source #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint' a b) (OutputConstraint' c d) Source #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint' a b -> AbsToCon (OutputConstraint' c d) Source # bindToConcrete :: OutputConstraint' a b -> (OutputConstraint' c d -> AbsToCon b0) -> AbsToCon b0 Source #

data OutputContextEntry name ty val Source #

Constructors

ContextVar name ty
ContextLet name ty val

Orphan instances

Read AbsolutePath Source #
Instance details Methods readsPrec :: Int -> ReadS AbsolutePath # readList :: ReadS [AbsolutePath] # readPrec :: ReadPrec AbsolutePath # readListPrec :: ReadPrec [AbsolutePath] #
Read InteractionId Source #
Instance details Methods readsPrec :: Int -> ReadS InteractionId # readList :: ReadS [InteractionId] # readPrec :: ReadPrec InteractionId # readListPrec :: ReadPrec [InteractionId] #
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 Methods readsPrec :: Int -> ReadS (Range' a) # readList :: ReadS [Range' a] # readPrec :: ReadPrec (Range' a) # readListPrec :: ReadPrec [Range' a] #
Read a => Read (Interval' a) Source #
Instance details Methods readsPrec :: Int -> ReadS (Interval' a) # readList :: ReadS [Interval' a] # readPrec :: ReadPrec (Interval' a) # readListPrec :: ReadPrec [Interval' a] #
Read a => Read (Position' a) Source #
Instance details Methods readsPrec :: Int -> ReadS (Position' a) # readList :: ReadS [Position' a] # readPrec :: ReadPrec (Position' a) # readListPrec :: ReadPrec [Position' a] #