Safe Haskell | None |
---|---|
Language | Haskell98 |
- flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars
- class IsFlexiblePattern a where
- maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind
- isFlexiblePattern :: a -> TCM Bool
- dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst]
- instantiatePattern :: Substitution -> Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
- instantiatePattern' :: Substitution -> Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
- isSolvedProblem :: Problem -> Bool
- noShadowingOfConstructors :: Call -> Problem -> TCM ()
- checkDotPattern :: DotPatternInst -> TCM ()
- bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- data LHSResult = LHSResult {}
- checkLeftHandSide :: Call -> Maybe QName -> [NamedArg Pattern] -> Type -> (LHSResult -> TCM a) -> TCM a
- checkLHS :: Maybe QName -> LHSState -> TCM LHSState
- noPatternMatchingOnCodata :: [NamedArg Pattern] -> TCM ()
Documentation
flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars Source
Compute the set of flexible patterns in a list of patterns. The result is the deBruijn indices of the flexible patterns.
class IsFlexiblePattern a where Source
A pattern is flexible if it is dotted or implicit, or a record pattern with only flexible subpatterns.
maybeFlexiblePattern :: a -> MaybeT TCM FlexibleVarKind Source
isFlexiblePattern :: a -> TCM Bool Source
IsFlexiblePattern Pattern Source | |
IsFlexiblePattern a => IsFlexiblePattern [a] Source | Lists of flexible patterns are |
IsFlexiblePattern (Pattern' a) Source | |
IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source | |
IsFlexiblePattern a => IsFlexiblePattern (Arg c a) Source |
dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst] Source
Compute the dot pattern instantiations.
:: Substitution | Partial substitution for the pattern variables, given in order of the clause telescope, (not in the order of occurrence in the patterns). |
-> Permutation | Map from the pattern variables to the telescope variables. |
-> [NamedArg Pattern] | Input patterns. |
-> [NamedArg Pattern] | Output patterns, with some |
In an internal pattern, replace some pattern variables by dot patterns, according to the given substitution.
:: Substitution | Partial substitution for the pattern variables, given in order of the clause telescope, (not in the order of occurrence in the patterns). |
-> Permutation | Map from the pattern variables to the telescope variables. |
-> [NamedArg Pattern] | Input patterns. |
-> [NamedArg Pattern] | Output patterns, with some |
In an internal pattern, replace some pattern variables by dot patterns, according to the given substitution.
isSolvedProblem :: Problem -> Bool Source
Check if a problem is solved. That is, if the patterns are all variables.
noShadowingOfConstructors Source
For each user-defined pattern variable in the Problem
, check
that the corresponding data type (if any) does not contain a
constructor of the same name (which is not in scope); this
"shadowing" could indicate an error, and is not allowed.
Precondition: The problem has to be solved.
checkDotPattern :: DotPatternInst -> TCM () Source
Check that a dot pattern matches it's instantiation.
bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a Source
Bind the variables in a left hand side and check that Hiding
of
the patterns matches the hiding info in the type.
Precondition: the patterns should
all be VarP
, WildP
, or AbsurdP
and the
telescope should have the same size as the pattern list.
There could also be ConP
s resulting from eta expanded implicit record
patterns.
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a Source
Bind as patterns
Result of checking the LHS of a clause.
LHSResult | |
|
:: Call | Trace, e.g. |
-> Maybe QName | The name of the definition we are checking. |
-> [NamedArg Pattern] | The patterns. |
-> Type | The expected type |
-> (LHSResult -> TCM a) | Continuation. |
-> TCM a |
Check a LHS. Main function.
checkLeftHandSide a ps a ret
checks that user patterns ps
eliminate
the type a
of the defined function, and calls continuation ret
if successful.
:: Maybe QName | The name of the definition we are checking. |
-> LHSState | The current state. |
-> TCM LHSState | The final state after all splitting is completed |
The loop (tail-recursive): split at a variable in the problem until problem is solved
noPatternMatchingOnCodata :: [NamedArg Pattern] -> TCM () Source
Ensures that we are not performing pattern matching on codata.