Safe Haskell | None |
---|---|
Language | Haskell2010 |
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
- normalForm :: (Reduce t, Simplify t, Normalise t) => Rewrite -> t -> TCM t
- data ComputeMode
- computeIgnoreAbstract :: ComputeMode -> Bool
- computeWrapInput :: ComputeMode -> String -> String
- showComputed :: ComputeMode -> Expr -> TCM Doc
- data UseForce
- 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' {}
- outputFormId :: OutputForm a b -> b
- reifyElimToExpr :: Elim -> TCM Expr
- 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], Telescope, [(Name, Type)])
- getRecordContents :: Rewrite -> Expr -> TCM ([Name], Telescope, [(Name, Type)])
- getModuleContents :: Rewrite -> QName -> TCM ([Name], Telescope, [(Name, Type)])
- whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule])
Documentation
parseExprIn :: InteractionId -> Range -> String -> TCM Expr Source #
redoChecks :: Maybe InteractionId -> TCM () Source #
After a give, redo termination etc. checks for function which was complemented.
:: 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
:: 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.
evalInMeta :: InteractionId -> Expr -> TCM Expr Source #
Modifier for interactive commands, specifying the amount of normalization in the output.
data ComputeMode Source #
Modifier for the interactive computation command, specifying the mode of computation and result display.
Instances
Eq ComputeMode Source # | |
Defined in Agda.Interaction.BasicOps (==) :: ComputeMode -> ComputeMode -> Bool # (/=) :: ComputeMode -> ComputeMode -> Bool # | |
Read ComputeMode Source # | |
Defined in Agda.Interaction.BasicOps readsPrec :: Int -> ReadS ComputeMode # readList :: ReadS [ComputeMode] # readPrec :: ReadPrec ComputeMode # readListPrec :: ReadPrec [ComputeMode] # | |
Show ComputeMode Source # | |
Defined in Agda.Interaction.BasicOps showsPrec :: Int -> ComputeMode -> ShowS # show :: ComputeMode -> String # showList :: [ComputeMode] -> ShowS # |
computeWrapInput :: ComputeMode -> String -> String Source #
showComputed :: ComputeMode -> Expr -> TCM Doc Source #
Modifier for interactive commands, specifying whether safety checks should be ignored.
WithForce | Ignore additional checks, like termination/positivity... |
WithoutForce | Don't ignore any checks. |
data OutputForm a b Source #
OutputForm Range [ProblemId] (OutputConstraint a b) |
Instances
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # | |
Defined in Agda.Interaction.BasicOps reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # | |
Functor (OutputForm a) Source # | |
Defined in Agda.Interaction.BasicOps 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 # | |
Defined in Agda.Interaction.BasicOps pretty :: OutputForm a b -> Doc Source # prettyPrec :: Int -> OutputForm a b -> Doc Source # prettyList :: [OutputForm a b] -> Doc Source # | |
(ToConcrete a c, ToConcrete b d) => ToConcrete (OutputForm a b) (OutputForm c d) Source # | |
Defined in Agda.Interaction.BasicOps 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 #
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
data OutputConstraint' a b Source #
A subset of OutputConstraint
.
Instances
(Pretty a, Pretty b) => Pretty (OutputConstraint' a b) Source # | |
Defined in Agda.Interaction.BasicOps 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 # | |
Defined in Agda.Interaction.BasicOps toConcrete :: OutputConstraint' a b -> AbsToCon (OutputConstraint' c d) Source # bindToConcrete :: OutputConstraint' a b -> (OutputConstraint' c d -> AbsToCon b0) -> AbsToCon b0 Source # |
outputFormId :: OutputForm a b -> b Source #
getConstraints :: TCM [OutputForm Expr Expr] Source #
getSolvedInteractionPoints :: Bool -> Rewrite -> TCM [(InteractionId, MetaId, Expr)] Source #
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) Source #
typeOfMeta :: Rewrite -> InteractionId -> TCM (OutputConstraint Expr InteractionId) Source #
typeOfMeta' :: Rewrite -> (InteractionId, MetaId) -> TCM (OutputConstraint Expr InteractionId) Source #
metaHelperType :: Rewrite -> InteractionId -> Range -> String -> TCM (OutputConstraint' Expr Expr) Source #
contextOfMeta :: InteractionId -> Rewrite -> TCM [OutputConstraint' Expr Name] Source #
typeInCurrent :: Rewrite -> Expr -> TCM Expr Source #
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 Source #
withInteractionId :: InteractionId -> TCM a -> TCM a Source #
introTactic :: Bool -> InteractionId -> TCM [String] Source #
The intro tactic.
Returns the terms (as strings) that can be used to refine the goal. Uses the coverage checker to find out which constructors are possible.
atTopLevel :: TCM a -> TCM a Source #
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.
:: Rewrite | How should the types be presented? |
-> Range | The range of the next argument. |
-> String | The module name. |
-> TCM ([Name], Telescope, [(Name, Type)]) | Module names, context extension needed to print types, names paired up with corresponding types. |
Returns the contents of the given module or record.
:: Rewrite | Amount of normalization in types. |
-> Expr | Expression presumably of record type. |
-> TCM ([Name], Telescope, [(Name, Type)]) | Module names, context extension, names paired up with corresponding types. |
Returns the contents of the given record identifier.
:: Rewrite | Amount of normalization in types. |
-> QName | Module name. |
-> TCM ([Name], Telescope, [(Name, Type)]) | Module names, context extension, names paired up with corresponding types. |
Returns the contents of the given module.
whyInScope :: String -> TCM (Maybe LocalVar, [AbstractName], [AbstractModule]) Source #
Orphan instances
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # | |
reify :: ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # reifyWhen :: Bool -> ProblemConstraint -> TCM (Closure (OutputForm Expr Expr)) Source # | |
Reify Constraint (OutputConstraint Expr Expr) Source # | |
reify :: Constraint -> TCM (OutputConstraint Expr Expr) Source # reifyWhen :: Bool -> Constraint -> TCM (OutputConstraint Expr Expr) Source # |