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

Safe HaskellNone
LanguageHaskell2010

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.

updateInPatterns Source #

Arguments

:: [Dom Type]

the types of the old pattern variables, relative to the new telescope

-> [NamedArg Pattern]

old in patterns

-> [Arg DeBruijnPattern]

patterns to be substituted, living in the new telescope

-> TCM ([NamedArg Pattern], [DotPatternInst]) 

Update the in patterns according to the given substitution, collecting new dot pattern instantiations in the process.

isSolvedProblem :: Problem -> Bool Source #

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

noShadowingOfConstructors Source #

Arguments

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

type Projectn = (ProjOrigin, QName) Source #

Temporary data structure for checkLeftoverPatterns

checkLeftoverDotPatterns Source #

Arguments

:: [NamedArg Pattern]

Leftover patterns after splitting is completed

-> [Int]

De Bruijn indices of leftover variable patterns computed by splitting

-> [Dom Type]

Types of leftover patterns

-> [DotPatternInst]

Instantiations computed by unifier

-> TCM () 

Checks whether the dot patterns left over after splitting can be covered by shuffling around the dots from implicit positions. Returns the updated user patterns (without dot patterns).

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

Bind the variables in a left hand side and check that Hiding of the patterns matches the hiding info in the type.

Precondition: the patterns should all be VarP, WildP, or AbsurdP 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

data LHSResult Source #

Result of checking the LHS of a clause.

Constructors

LHSResult 

Fields

  • lhsParameters :: Nat

    The number of original module parameters. These are present in the the patterns.

  • lhsVarTele :: Telescope

    Δ : The types of the pattern variables, in internal dependency order. Corresponds to clauseTel.

  • lhsPatterns :: [NamedArg DeBruijnPattern]

    The patterns in internal syntax.

  • lhsBodyType :: Arg Type

    The type of the body. Is if Γ is defined. Irrelevant to indicate the rhs must be checked in irrelevant mode.

  • lhsPatSubst :: Substitution

    Substitution version of lhsPatterns, only up to the first projection pattern. Δ |- lhsPatSubst : Γ. Where Γ is the argument telescope of the function. This is used to update inherited dot patterns in with-function clauses.

  • lhsAsBindings :: [AsBinding]

    As-bindings from the left-hand side. Return instead of bound since we want them in where's and right-hand sides, but not in with-clauses (Issue 2303).

checkLeftHandSide Source #

Arguments

:: 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 Substitution

Module parameter substitution from with-abstraction.

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

checkLHS Source #

Arguments

:: Maybe QName

The name of the definition we are checking.

-> LHSState

The current state.

-> TCM LHSState

The final state after all splitting is completed

The loop (tail-recursive): split at a variable in the problem until problem is solved

noPatternMatchingOnCodata :: [NamedArg DeBruijnPattern] -> TCM () Source #

Ensures that we are not performing pattern matching on codata.