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 userdefined 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 (tailrecursive): 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.