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

Safe Haskell | None

Agda.TypeChecking.Rules.LHS

Synopsis

- flexiblePatterns :: [NamedArg Pattern] -> TCM FlexibleVars
- dotPatternInsts :: [NamedArg Pattern] -> Substitution -> [Dom Type] -> TCM [DotPatternInst]
- instantiatePattern :: Substitution -> Permutation -> [Arg Pattern] -> [Arg Pattern]
- isSolvedProblem :: Problem -> Bool
- noShadowingOfConstructors :: (Maybe r -> Call) -> Problem -> TCM ()
- checkDotPattern :: DotPatternInst -> TCM ()
- bindLHSVars :: [NamedArg Pattern] -> Telescope -> TCM a -> TCM a
- bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
- checkLeftHandSide :: (Maybe r -> Call) -> [NamedArg Pattern] -> Type -> (Maybe Telescope -> Telescope -> Substitution -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) -> TCM a
- noPatternMatchingOnCodata :: [Arg Pattern] -> TCM ()

# 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 -> [Arg Pattern] -> [Arg 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`, or `ImplicitP` 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

Bind as patterns

checkLeftHandSide

Arguments

:: (Maybe r -> Call) | Trace, e.g. `CheckPatternShadowing clause`
-> [NamedArg Pattern] | The patterns.
-> Type | The expected type `a = Γ → b`.
-> (Maybe Telescope -> Telescope -> Substitution -> [String] -> [Arg Pattern] -> Type -> Permutation -> TCM a) | Continuation.
-> TCM a |

Check a LHS. Main function.

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