Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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 Case c Source

Branches in a case tree.




projPatterns :: Bool

We are constructing a record here (copatterns). conBranches lists projections.

conBranches :: Map QName (WithArity c)

Map from constructor (or projection) names to their arity and the case subtree. (Projections have arity 0.)

litBranches :: Map Literal c

Map from literal to case subtree.

catchAllBranch :: Maybe c

(Possibly additional) catch-all clause.

data CompiledClauses Source

Case tree with bodies.


Case Int (Case CompiledClauses)

Case n bs stands for a match on the n-th argument (counting from zero) with bs as the case branches. If the n-th argument is a projection, we have only conBranches with arity 0.

Done [Arg ArgName] Term

Done xs b stands for the body b where the xs contains hiding and name suggestions for the free variables. This is needed to build lambdas on the right hand side for partial applications which can still reduce.


Absurd case.


Show CompiledClauses Source 
Pretty CompiledClauses Source 
KillRange CompiledClauses Source 
Abstract CompiledClauses Source 
Apply CompiledClauses Source 
EmbPrj CompiledClauses Source 
InstantiateFull CompiledClauses Source 
DropArgs CompiledClauses Source

To drop the first n arguments in a compiled clause, we reduce the split argument indices by n and drop n arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.

litCase :: Literal -> c -> Case c Source

projCase :: QName -> c -> Case c Source

catchAll :: c -> Case c Source

hasCatchAll :: CompiledClauses -> Bool Source

Check whether a case tree has a catch-all clause.

Pretty instances.

prettyMap :: (Show k, Pretty v) => Map k v -> [Doc] Source

KillRange instances.