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

Safe Haskell | None

Agda.TypeChecking.CompiledClause.Compile

Synopsis

- compileClauses :: Maybe (QName, Type) -> [Clause] -> TCM CompiledClauses
- type Cl = ([Arg Pattern], ClauseBody)
- type Cls = [Cl]
- compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses
- compile :: Cls -> CompiledClauses
- nextSplit :: Cls -> Maybe Int
- splitOn :: Int -> Cls -> Case Cls
- splitC :: Int -> Cl -> Case Cl
- expandCatchAlls :: Int -> Cls -> Cls
- substBody :: Int -> Int -> Term -> ClauseBody -> ClauseBody

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

splitOn :: Int -> Cls -> Case Cls

splitC :: Int -> Cl -> Case Cl

expandCatchAlls :: Int -> Cls -> Cls

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