| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.MakeCase
Synopsis
- type CaseContext = Maybe ExtLamInfo
- parseVariables :: QName -> Telescope -> InteractionId -> Range -> [String] -> TCM [(Int, NameInScope)]
- type ClauseZipper = ([Clause], Clause, [Clause])
- getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
- recheckAbstractClause :: Type -> Maybe Substitution -> SpineClause -> TCM Clause
- makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [Clause])
- makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause
- makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
- makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
- anyEllipsisVar :: QName -> SpineClause -> [Name] -> TCM Bool
Documentation
type CaseContext = Maybe ExtLamInfo Source #
Arguments
| :: QName | The function name. |
| -> Telescope | The telescope of the clause we are splitting. |
| -> InteractionId | The hole of this function we are working on. |
| -> Range | The range of this hole. |
| -> [String] | The words the user entered in this hole (variable names). |
| -> TCM [(Int, NameInScope)] | The computed de Bruijn indices of the variables to split on, with information about whether each variable is in scope. |
Parse variables (visible or hidden), returning their de Bruijn indices.
Used in makeCase.
type ClauseZipper = ([Clause], Clause, [Clause]) Source #
Lookup the clause for an interaction point in the signature. Returns the CaseContext, the previous clauses, the clause itself, and a list of the remaining ones.
getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper) Source #
recheckAbstractClause :: Type -> Maybe Substitution -> SpineClause -> TCM Clause Source #
makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [Clause]) Source #
Entry point for case splitting tactic.
makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause Source #
Make the given pattern variables visible by marking their origin as
CaseSplit and pattern origin as PatOSplit in the SplitClause.
makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause Source #
Make clause with no rhs (because of absurd match).
makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause Source #
Make a clause with a question mark as rhs.
anyEllipsisVar :: QName -> SpineClause -> [Name] -> TCM Bool Source #