Agda.TypeChecking.Rules.LHS

Documentation

flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars

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]

Compute the dot pattern instantiations.

instantiatePattern :: Substitution -> Permutation -> [NamedArg Pattern] -> [NamedArg Pattern]

isSolvedProblem :: Problem -> Bool

Check if a problem is solved. That is, if the patterns are all variables.

noShadowingOfConstructors

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 ()

Check that a dot pattern matches it's instantiation.

bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a

Bind the variables in a left hand side. Precondition: the patterns should all be VarP, WildP, AbsurdP, 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

Bind as patterns

data LHSResult

Constructors

LHSResult

Fields

lhsPatternTele :: Maybe Telescope

lhsVarTele :: Telescope

lhsSubstitution :: Substitution

σ : The patterns in form of a substitution

lhsVarNames :: [String]

Names for the variables in

lhsPatterns :: [NamedArg Pattern]

The patterns in internal syntax.

lhsBodyType :: Arg Type

The type of the body. Is bσ@ if

lhsPermutation :: Permutation

checkLeftHandSide

Arguments

:: (Maybe r -> Call)

Trace, e.g. CheckPatternShadowing clause

-> Maybe QName

The name of the definition we are checking.

-> [NamedArg Pattern]

The patterns.

-> 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.

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