Safe Haskell | None |
---|---|
Language | Haskell98 |
- flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars
- dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst]
- instantiatePattern :: Substitution -> Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]
- isSolvedProblem :: Problem -> Bool
- noShadowingOfConstructors :: (Maybe r -> Call) -> Problem -> TCM ()
- checkDotPattern :: DotPatternInst -> TCM ()
- bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- data LHSResult = LHSResult {}
- checkLeftHandSide :: (Maybe r -> 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. A pattern is flexible if it is dotted or implicit.
dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst] Source
Compute the dot pattern instantiations.
instantiatePattern :: Substitution -> Permutation -> [NamedArg Pattern] -> [NamedArg Pattern] Source
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.
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a Source
Bind as patterns
LHSResult | |
|
:: (Maybe r -> 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.