Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Interaction.MakeCase

Synopsis

- type CaseContext = Maybe ExtLamInfo
- parseVariables :: QName -> Context -> [AsBinding] -> InteractionId -> Range -> [String] -> TCM [(Int, NameInScope)]
- type ClauseZipper = ([Clause], Clause, [Clause])
- getClauseZipperForIP :: QName -> Int -> TCM (CaseContext, ClauseZipper)
- recheckAbstractClause :: Type -> Maybe Substitution -> SpineClause -> TCM (Clause, Context, [AsBinding])
- makeCase :: InteractionId -> Range -> String -> TCM (QName, CaseContext, [Clause])
- makePatternVarsVisible :: [Nat] -> SplitClause -> SplitClause
- makeRHSEmptyRecord :: RHS -> RHS
- 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 #

parseVariables Source #

Arguments

:: QName | The function name.
-> Context | The context of the RHS of the clause we are splitting.
-> [AsBinding] | The as-bindings 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, Context, [AsBinding]) 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`.

makeRHSEmptyRecord :: RHS -> RHS Source #

If a copattern split yields no clauses, we must be at an empty record type. In this case, replace the rhs by `record{}`

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 #