Agda.TypeChecking.CompiledClause

Documentation

type :-> key value = Map key value

data WithArity c

Constructors

WithArity

Fields

arity :: Int

content :: c

Instances

Functor WithArity

Typeable1 WithArity

Foldable WithArity

Traversable WithArity

Monoid c => Monoid (WithArity c)

Pretty a => Pretty (WithArity a)

KillRange c => KillRange (WithArity c)

Abstract a => Abstract (WithArity a)

Apply a => Apply (WithArity a)

EmbPrj a => EmbPrj (WithArity a)

InstantiateFull a => InstantiateFull (WithArity a)

data Case c

Branches in a case tree.

Constructors

Branches

Fields

conBranches :: QName :-> WithArity c

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

litBranches :: Literal :-> c

Map from literal to case subtree.

catchAllBranch :: Maybe c

(Possibly additional) catch-all clause.

Instances

Functor Case

Typeable1 Case

Foldable Case

Traversable Case

Pretty a => Show (Case a)

Monoid m => Monoid (Case m)

Pretty a => Pretty (Case a)

KillRange c => KillRange (Case c)

Abstract a => Abstract (Case a)

Apply a => Apply (Case a)

EmbPrj a => EmbPrj (Case a)

InstantiateFull a => InstantiateFull (Case a)

data CompiledClauses

Case tree with bodies.

Constructors

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.

Fail

Absurd case.

Instances

Show CompiledClauses

Typeable CompiledClauses

Pretty CompiledClauses

KillRange CompiledClauses

Abstract CompiledClauses

Apply CompiledClauses

EmbPrj 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

emptyBranches :: Case c

litCase :: Literal -> c -> Case c

conCase :: QName -> WithArity c -> Case c

catchAll :: c -> Case c

Pretty instances.

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