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' {}
- data OutputContextEntry name ty val
- = ContextVar name ty
- | ContextLet name ty val
- outputFormId :: OutputForm a b -> b
- reifyElimToExpr :: MonadReify m => Elim -> m Expr
- prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr]
- getConstraints :: TCM [OutputForm Expr Expr]
- getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr]
- stripConstraintPids :: Constraints -> Constraints
- getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr]
- getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' Expr]
- getGoals :: TCM Goals
- getWarningsAndNonFatalErrors :: TCM WarningsAndNonFatalErrors
- getResponseContext :: Rewrite -> InteractionId -> TCM [ResponseContextEntry]
- 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 [ResponseContextEntry]
- 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.
Instances
Read Rewrite Source # | |
Show Rewrite Source # | |
ToJSON Rewrite | |
Defined in Agda.Interaction.JSONTop toEncoding :: Rewrite -> Encoding toJSONList :: [Rewrite] -> Value toEncodingList :: [Rewrite] -> Encoding | |
EncodeTCM Rewrite Source # | |
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 # | |
ToJSON ComputeMode | |
Defined in Agda.Interaction.JSONTop toJSON :: ComputeMode -> Value toEncoding :: ComputeMode -> Encoding toJSONList :: [ComputeMode] -> Value toEncodingList :: [ComputeMode] -> Encoding | |
EncodeTCM ComputeMode Source # | |
Defined in Agda.Interaction.JSONTop encodeTCM :: ComputeMode -> TCM Value Source # |
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
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 # |
data OutputContextEntry name ty val Source #
ContextVar name ty | |
ContextLet name ty val |
outputFormId :: OutputForm a b -> b Source #
reifyElimToExpr :: MonadReify m => Elim -> m Expr Source #
prettyConstraints :: [Closure Constraint] -> TCM [OutputForm Expr Expr] Source #
getConstraints :: TCM [OutputForm Expr Expr] Source #
getConstraintsMentioning :: Rewrite -> MetaId -> TCM [OutputForm Expr Expr] Source #
getConstraints' :: (ProblemConstraint -> TCM ProblemConstraint) -> (ProblemConstraint -> Bool) -> TCM [OutputForm Expr Expr] Source #
getIPBoundary :: Rewrite -> InteractionId -> TCM [IPBoundary' Expr] Source #
:: Rewrite | Normalise? |
-> InteractionId | |
-> TCM [ResponseContextEntry] |
Collecting the context of the given meta-variable.
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 #
Create type of application of new helper function that would solve the goal.
contextOfMeta :: InteractionId -> Rewrite -> TCM [ResponseContextEntry] Source #
Gives a list of names and corresponding types. This list includes not only the local variables in scope, but also the let-bindings.
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 #