Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Rules.LHS

Synopsis

- data DotPatternInst = DPI Expr Term Type
- data AsBinding = AsB Name Term Type
- flexiblePatterns :: [NamedArg Pattern] -> FlexibleVars
- dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Type] -> [DotPatternInst]
- instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]
- isSolvedProblem :: Problem -> Bool
- noShadowingOfConstructors :: Clause -> Problem -> TCM ()
- checkDotPattern :: DotPatternInst -> TCM Constraints
- bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope
- checkLeftHandSide :: Clause -> [NamedArg Pattern] -> Type -> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) -> TCM a
- noPatternMatchingOnCodata :: MonadTCM tcm => [Arg Pattern] -> tcm ()

# Documentation

data DotPatternInst

Constructors

DPI Expr Term Type |

Instances

Subst DotPatternInst |
PrettyTCM DotPatternInst |

data AsBinding

Constructors

AsB Name Term Type |

Instances

Raise AsBinding |
Subst AsBinding |
PrettyTCM AsBinding |

flexiblePatterns :: [NamedArg Pattern] -> 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 -> [Type] -> [DotPatternInst]

Compute the dot pattern instantiations.

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

isSolvedProblem :: Problem -> Bool

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

noShadowingOfConstructors

Arguments

:: Clause | The entire clause (used for error reporting).
-> 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 Constraints

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`, or `ImplicitP` and the telescope should have the same size as the pattern list.

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

Bind as patterns

useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope

Rename the variables in a telescope using the names from a given pattern

checkLeftHandSide

Arguments

:: Clause | The entire clause.
-> [NamedArg Pattern] | The patterns.
-> Type | The expected type.
-> (Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) | Continuation.
-> TCM a |

Check a LHS. Main function.

noPatternMatchingOnCodata :: MonadTCM tcm => [Arg Pattern] -> tcm ()