Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



type :-> key value = Map key valueSource

data Case c Source




conBranches :: QName :-> WithArity c

Map from constructor names to their arity and the case subtree

litBranches :: Literal :-> c

Map from literal to case subtree

catchAllBranch :: Maybe c

(Possibly additional) catch-all clause

data CompiledClauses Source


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.

Done [Arg String] 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 
Typeable CompiledClauses 
Pretty CompiledClauses 
Abstract CompiledClauses 
Apply CompiledClauses 
DropArgs CompiledClauses

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.

InstantiateFull CompiledClauses 
EmbPrj CompiledClauses