Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Rules.LHS

Synopsis

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

Arguments

:: (Maybe r -> Call)	Trace, e.g., `CheckPatternShadowing clause`
-> Problem
-> TCM ()

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. Precondition: the patterns should all be VarP, WildP, or ImplicitP and the telescope should have the same size as the pattern list. There could also be ConPs resulting from eta expanded implicit record patterns.

bindAsPatterns :: [AsBinding] -> TCM a -> TCM a Source

Bind as patterns

checkLeftHandSide Source

Arguments

:: (Maybe r -> Call)	Trace, e.g. `CheckPatternShadowing clause`
-> Maybe QName	The name of the definition we are checking.
-> [NamedArg Pattern]	The patterns.
-> Type	The expected type `a = Γ → b`.
-> (Maybe Telescope -> Telescope -> Substitution -> [ArgName] -> [NamedArg Pattern] -> Arg Type -> Permutation -> 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.

noPatternMatchingOnCodata :: [NamedArg Pattern] -> TCM () Source