Agda-2.2.10: A dependently typed functional programming language and proof assistant
Source code
Contents
Index
Agda.TypeChecking.CompiledClause
Synopsis
type
:->
key value =
Map
key value
data
Case
c =
Branches
{
conBranches
::
QName
:->
c
litBranches
::
Literal
:->
c
catchAllBranch
::
Maybe
c
}
data
CompiledClauses
=
Case
Int
(
Case
CompiledClauses
)
|
Done
Int
Term
|
Fail
compileClauses
:: [
Clauses
] ->
CompiledClauses
type
Cl
= ([
Arg
Pattern
],
ClauseBody
)
type
Cls
= [
Cl
]
compile
::
Cls
->
CompiledClauses
nextSplit
::
Cls
->
Maybe
Int
splitOn
::
Int
->
Cls
->
Case
Cls
splitC
::
Int
->
Cl
->
Case
Cl
Documentation
type
:->
key value =
Map
key value
Source
data
Case
c
Source
Constructors
Branches
conBranches
::
QName
:->
c
litBranches
::
Literal
:->
c
catchAllBranch
::
Maybe
c
data
CompiledClauses
Source
Constructors
Case
Int
(
Case
CompiledClauses
)
Done
Int
Term
Fail
compileClauses
:: [
Clauses
] ->
CompiledClauses
Source
Note that it is the
translated
clauses which are compiled, not the original ones.
type
Cl
= ([
Arg
Pattern
],
ClauseBody
)
Source
type
Cls
= [
Cl
]
Source
compile
::
Cls
->
CompiledClauses
Source
nextSplit
::
Cls
->
Maybe
Int
Source
splitOn
::
Int
->
Cls
->
Case
Cls
Source
splitC
::
Int
->
Cl
->
Case
Cl
Source
Produced by
Haddock
version 2.6.1