Agda.TypeChecking.CompiledClause.Compile

Documentation

compileClauses

Arguments

:: Maybe (QName, Type)

Translate record patterns and coverage check with given type?

-> [Clause]

-> TCM CompiledClauses

Process function clauses into case tree. This involves: 1. Coverage checking, generating a split tree. 2. Translation of lhs record patterns into rhs uses of projection. Update the split tree. 3. Generating a case tree from the split tree. Phases 1. and 2. are skipped if Nothing.

type Cl = ([Arg Pattern], ClauseBody)

type Cls = [Cl]

compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses

compile :: Cls -> CompiledClauses

nextSplit :: Cls -> Maybe Int

Get the index of the next argument we need to split on. This the number of the first pattern that does a match in the first clause.

isVar :: Pattern -> Bool

Is this a variable pattern?

splitOn :: Bool -> Int -> Cls -> Case Cls

splitOn single n cs will force expansion of catch-alls if single.

splitC :: Int -> Cl -> Case Cl

expandCatchAlls :: Bool -> Int -> Cls -> Cls

Expand catch-alls that appear before actual matches.

Example:

   true  y
   x     false
   false y

will expand the catch-all x to false.

Catch-alls need also to be expanded if they come before/after a record pattern, otherwise we get into trouble when we want to eliminate splits on records later.

substBody :: Int -> Int -> Term -> ClauseBody -> ClauseBody