Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 => [(Bool, Arg Pattern)] -> tcm ()
Documentation
data DotPatternInst Source
Constructors
DPI Expr Term Type
data AsBinding Source
Constructors
AsB Name Term Type
flexiblePatterns :: [NamedArg Pattern] -> FlexibleVarsSource
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]Source
Compute the dot pattern instantiations.
instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]Source
isSolvedProblem :: Problem -> BoolSource
Check if a problem is solved. That is, if the patterns are all variables.
noShadowingOfConstructorsSource
:: ClauseThe 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 ConstraintsSource
Check that a dot pattern matches it's instantiation.
bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM aSource
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 aSource
Bind as patterns
useNamesFromPattern :: [NamedArg Pattern] -> Telescope -> TelescopeSource
Rename the variables in a telescope using the names from a given pattern
checkLeftHandSideSource
::
=> ClauseThe patterns.
-> [NamedArg Pattern]The expected type.
-> TypeContinuation.
-> Telescope -> Telescope -> [Term] -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a
-> TCM a
Check a LHS. Main function.
noPatternMatchingOnCodataSource
:: MonadTCM tcm
=> [(Bool, Arg Pattern)]
-> tcm ()
Produced by Haddock version 2.6.0