Safe Haskell	None
Language	Haskell2010

Agda.Interaction.BasicOps

Contents

Orphan instances

Synopsis

parseExpr :: Range -> String -> TCM Expr
parseExprIn :: InteractionId -> Range -> String -> TCM Expr
giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM ()
redoChecks :: Maybe InteractionId -> TCM ()
give :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine :: UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
evalInCurrent :: Expr -> TCM Expr
evalInMeta :: InteractionId -> Expr -> TCM Expr
data Rewrite
- = AsIs
- | Instantiated
- | HeadNormal
- | Simplified
- | Normalised
normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
data ComputeMode
- = DefaultCompute
- | IgnoreAbstract
- | UseShowInstance
computeIgnoreAbstract :: ComputeMode -> Bool
computeWrapInput :: ComputeMode -> String -> String
showComputed :: ComputeMode -> Expr -> TCM Doc
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
- | FindInScopeOF b a [(a, a)]
- | PTSInstance b b
data OutputConstraint' a b = OfType' {
- ofName :: b
- ofExpr :: a
}
outputFormId :: OutputForm a b -> b
reifyElimToExpr :: Elim -> TCM Expr
showComparison :: Comparison -> String
getConstraints :: TCM [OutputForm Expr Expr]
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)]
typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta)
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId)
typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta]
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr)
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name]
typeInCurrent :: Rewrite -> Expr -> TCM Expr
typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr
withInteractionId :: InteractionId -> TCM a -> TCM a
withMetaId :: MetaId -> TCM a -> TCM a
introTactic :: Bool -> InteractionId -> TCM [String]
atTopLevel :: TCM a -> TCM a
parseName :: Range -> String -> TCM QName
isQName :: Expr -> Maybe QName
moduleContents :: Rewrite -> Range -> String -> TCM ([Name], [(Name, Type)])
getRecordContents :: Rewrite -> Expr -> TCM ([Name], [(Name, Type)])
getModuleContents :: Rewrite -> QName -> TCM ([Name], [(Name, Type)])
whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])

Documentation

parseExpr :: Range -> String -> TCM Expr #

Parses an expression.

parseExprIn :: InteractionId -> Range -> String -> TCM Expr #

giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM () #

redoChecks :: Maybe InteractionId -> TCM () #

After a give, redo termination etc. checks for function which was complemented.

give #

Arguments

:: UseForce	Skip safety checks?
-> InteractionId	Hole.
-> Maybe Range
-> Expr	The expression to give.
-> TCM Expr	If successful, the very expression is returned unchanged.

Try to fill hole by expression.

Returns the given expression unchanged (for convenient generalization to refine).

refine #

Arguments

:: UseForce	Skip safety checks when giving?
-> InteractionId	Hole.
-> Maybe Range
-> Expr	The expression to refine the hole with.
-> TCM Expr	The successfully given expression.

Try to refine hole by expression e.

This amounts to successively try to give e, e ?, e ? ?, ... Returns the successfully given expression.

evalInCurrent :: Expr -> TCM Expr #

Evaluate the given expression in the current environment

evalInMeta :: InteractionId -> Expr -> TCM Expr #

data Rewrite #

Modifier for interactive commands, specifying the amount of normalization in the output.

Constructors

AsIs
Instantiated
HeadNormal
Simplified
Normalised

Instances

Read Rewrite #
Instance details Defined in Agda.Interaction.BasicOps Methods readsPrec :: Int -> ReadS Rewrite # readList :: ReadS [Rewrite] # readPrec :: ReadPrec Rewrite # readListPrec :: ReadPrec [Rewrite] #
Show Rewrite #
Instance details Defined in Agda.Interaction.BasicOps Methods showsPrec :: Int -> Rewrite -> ShowS # show :: Rewrite -> String # showList :: [Rewrite] -> ShowS #

normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t #

data ComputeMode #

Modifier for the interactive computation command, specifying the mode of computation and result display.

Constructors

DefaultCompute
IgnoreAbstract
UseShowInstance

Instances

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

computeIgnoreAbstract :: ComputeMode -> Bool #

computeWrapInput :: ComputeMode -> String -> String #

showComputed :: ComputeMode -> Expr -> TCM Doc #

data UseForce #

Modifier for interactive commands, specifying whether safety checks should be ignored.

Constructors

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

Instances

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

data OutputForm a b #

Constructors

OutputForm Range [ProblemId] (OutputConstraint a b)

Instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) #
Functor (OutputForm a) #
Instance details Defined in Agda.Interaction.BasicOps Methods fmap :: (a0 -> b) -> OutputForm a a0 -> OutputForm a b # (<$) :: a0 -> OutputForm a b -> OutputForm a a0 #
(Show a, Show b) => Show (OutputForm a b) #
Instance details Defined in Agda.Interaction.BasicOps Methods showsPrec :: Int -> OutputForm a b -> ShowS # show :: OutputForm a b -> String # showList :: [OutputForm a b] -> ShowS #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputForm a b -> AbsToCon (OutputForm c d) # bindToConcrete :: OutputForm a b -> (OutputForm c d -> AbsToCon b0) -> AbsToCon b0 #

data OutputConstraint a b #

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
FindInScopeOF b a [(a, a)]
PTSInstance b b

Instances

Reify Constraint (OutputConstraint Expr Expr) #
Instance details Defined in Agda.Interaction.BasicOps Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) #
Functor (OutputConstraint a) #
Instance details Defined in Agda.Interaction.BasicOps Methods fmap :: (a0 -> b) -> OutputConstraint a a0 -> OutputConstraint a b # (<$) :: a0 -> OutputConstraint a b -> OutputConstraint a a0 #
(Show a, Show b) => Show (OutputConstraint a b) #
Instance details Defined in Agda.Interaction.BasicOps Methods showsPrec :: Int -> OutputConstraint a b -> ShowS # show :: OutputConstraint a b -> String # showList :: [OutputConstraint a b] -> ShowS #
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputConstraint a b) (OutputConstraint c d) #
Instance details Defined in Agda.Interaction.BasicOps Methods toConcrete :: OutputConstraint a b -> AbsToCon (OutputConstraint c d) # bindToConcrete :: OutputConstraint a b -> (OutputConstraint c d -> AbsToCon b0) -> AbsToCon b0 #

data OutputConstraint' a b #

A subset of OutputConstraint.

Constructors

OfType'
Fields ofName :: b ofExpr :: a

Instances

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

outputFormId :: OutputForm a b -> b #

reifyElimToExpr :: Elim -> TCM Expr #

showComparison :: Comparison -> String #

getConstraints :: TCM [OutputForm Expr Expr] #

getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)] #

getSolvedInteractionPoints True returns all solutions, even if just solved by another, non-interaction meta.

getSolvedInteractionPoints False only returns metas that are solved by a non-meta.

typeOfMetaMI :: Rewrite -> MetaId -> TCM (OutputConstraint Expr NamedMeta) #

typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId) #

typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId) #

typesOfVisibleMetas :: Rewrite -> TCM [OutputConstraint Expr InteractionId] #

typesOfHiddenMetas :: Rewrite -> TCM [OutputConstraint Expr NamedMeta] #

metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr) #

contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name] #

typeInCurrent :: Rewrite -> Expr -> TCM Expr #

Returns the type of the expression in the current environment We wake up irrelevant variables just in case the user want to invoke that command in an irrelevant context.

typeInMeta :: InteractionId -> Rewrite -> Expr -> TCM Expr #

withInteractionId :: InteractionId -> TCM a -> TCM a #

withMetaId :: MetaId -> TCM a -> TCM a #

introTactic :: Bool -> InteractionId -> TCM [String] #

atTopLevel :: TCM a -> TCM a #

Runs the given computation as if in an anonymous goal at the end of the top-level module.

Sets up current module, scope, and context.

parseName :: Range -> String -> TCM QName #

Parse a name.

isQName :: Expr -> Maybe QName #

Check whether an expression is a (qualified) identifier.

moduleContents #

Arguments

:: Rewrite	How should the types be presented?
-> Range	The range of the next argument.
-> String	The module name.
-> TCM ([Name], [(Name, Type)])	Module names, names paired up with corresponding types.

Returns the contents of the given module or record.

getRecordContents #

Arguments

:: Rewrite	Amount of normalization in types.
-> Expr	Expression presumably of record type.
-> TCM ([Name], [(Name, Type)])	Module names, names paired up with corresponding types.

Returns the contents of the given record identifier.

getModuleContents #

Arguments

:: Rewrite	Amount of normalization in types.
-> QName	Module name.
-> TCM ([Name], [(Name, Type)])	Module names, names paired up with corresponding types.

Returns the contents of the given module.

whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule]) #

Orphan instances

Reify ProblemConstraint (Closure (OutputForm Expr Expr)) #
Instance details Methods reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) #
Reify Constraint (OutputConstraint Expr Expr) #
Instance details Methods reify :: Constraint -> TCM (OutputConstraint Expr Expr) # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) #