Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.TypeChecking.CompiledClause
Contents
Description
Case trees.
After coverage checking, pattern matching is translated to case trees, i.e., a tree of successive case splits on one variable at a time.
- data WithArity c = WithArity {}
- data Case c = Branches {
- conBranches :: Map QName (WithArity c)
- litBranches :: Map Literal c
- catchAllBranch :: Maybe c
- data CompiledClauses
- emptyBranches :: Case CompiledClauses
- litCase :: Literal -> c -> Case c
- conCase :: QName -> WithArity c -> Case c
- catchAll :: c -> Case c
- prettyMap :: (Show k, Pretty v) => Map k v -> [Doc]
Documentation
data WithArity c
data Case c
Branches in a case tree.
Constructors
Branches | |
Fields
|
data CompiledClauses
Case tree with bodies.
Constructors
Case Int (Case CompiledClauses) |
|
Done [Arg ArgName] Term |
|
Fail | Absurd case. |
Instances
Show CompiledClauses | |
Pretty CompiledClauses | |
Abstract CompiledClauses | |
Apply CompiledClauses | |
EmbPrj CompiledClauses | |
InstantiateFull CompiledClauses | |
DropArgs CompiledClauses | To drop the first |