| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Agda.Interaction.MakeCase
- type CaseContext = Maybe ExtLamInfo
- findClause :: MetaId -> TCM (CaseContext, QName, Clause)
- parseVariables :: InteractionId -> Range -> [String] -> TCM [Int]
- makeCase :: InteractionId -> Range -> String -> TCM (CaseContext, [Clause])
- makeAbsurdClause :: QName -> SplitClause -> TCM Clause
- makeAbstractClause :: QName -> SplitClause -> TCM Clause
- deBruijnIndex :: Expr -> TCM Nat
Documentation
type CaseContext = Maybe ExtLamInfo Source #
findClause :: MetaId -> TCM (CaseContext, QName, Clause) Source #
Find the clause whose right hand side is the given meta BY SEARCHING THE WHOLE SIGNATURE. Returns the original clause, before record patterns have been translated away. Raises an error if there is no matching clause.
Andreas, 2010-09-21: This looks like a SUPER UGLY HACK to me. You are walking through the WHOLE signature to find an information you have thrown away earlier. (shutter with disgust). This code fails for record rhs because they have been eta-expanded, so the MVar is gone.
parseVariables :: InteractionId -> Range -> [String] -> TCM [Int] Source #
Parse variables (visible or hidden), returning their de Bruijn indices.
Used in makeCase.
makeCase :: InteractionId -> Range -> String -> TCM (CaseContext, [Clause]) Source #
Entry point for case splitting tactic.
makeAbsurdClause :: QName -> SplitClause -> TCM Clause Source #
makeAbstractClause :: QName -> SplitClause -> TCM Clause Source #
Make a clause with a question mark as rhs.