| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.MakeCase
Synopsis
- type CaseContext = Maybe ExtLamInfo
- data SplitAction
- splitActionToEither3 :: SplitAction -> Either3 Name Int Int
- parseVariables :: QName -> Context -> [AsBinding] -> InteractionId -> Range -> [String] -> TCM [SplitAction]
- 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 :: [Name] -> [Nat] -> SplitClause -> SplitClause
- makeRHSEmptyRecord :: RHS -> RHS
- makeAbsurdClause :: QName -> ExpandedEllipsis -> SplitClause -> TCM Clause
- filterOutGeneralizedVarPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
- makeNamedArgUserWritten :: NamedArg a -> NamedArg a
- isGeneralizedVarName :: PatVarName -> Bool
- makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause
- anyEllipsisVar :: QName -> SpineClause -> [Name] -> TCM Bool
Documentation
type CaseContext = Maybe ExtLamInfo Source #
data SplitAction Source #
For the names the user enters for case-splitting, there can be different actions depending on what the name resolved to.
Constructors
| RevealDotPattern Name | De Bruijn index of a pattern variable bound to a value, turn into dot pattern. |
| RevealHiddenVariable Int | De Bruijn index of a hidden argument, make this argument visible. |
| SplitOnVariable Int | De Bruijn index of an unconstrained pattern variable, split on it. |
Instances
| Show SplitAction Source # | |
Defined in Agda.Interaction.MakeCase Methods showsPrec :: Int -> SplitAction -> ShowS # show :: SplitAction -> String # showList :: [SplitAction] -> ShowS # | |
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 [SplitAction] | The computed de Bruijn indices of the variables and the inferred action. |
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 :: [Name] -> [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).
filterOutGeneralizedVarPatterns :: [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern] Source #
Drop hidden patterns introduced by generalization with an unparsable name. If we drop one, we need to make the next non-dropped hidden pattern named.
makeNamedArgUserWritten :: NamedArg a -> NamedArg a Source #
isGeneralizedVarName :: PatVarName -> Bool Source #
Unparseable variable names are those that contain a ..
makeAbstractClause :: QName -> RHS -> ExpandedEllipsis -> SplitClause -> TCM Clause Source #
Make a clause with a question mark as rhs.
anyEllipsisVar :: QName -> SpineClause -> [Name] -> TCM Bool Source #