Agda.TypeChecking.CompiledClause

Documentation

type :-> key value = Map key value

data Case c

Constructors

Branches

Fields

conBranches :: QName :-> c

litBranches :: Literal :-> c

catchAllBranch :: Maybe c

Instances

Functor Case

Typeable1 Case

Data c => Data (Case c)

Pretty a => Show (Case a)

Monoid m => Monoid (Case m)

Pretty a => Pretty (Case a)

Abstract a => Abstract (Case a)

Apply a => Apply (Case a)

EmbPrj a => EmbPrj (Case a)

InstantiateFull a => InstantiateFull (Case a)

data CompiledClauses

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.

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.

Fail

Absurd case.

Instances

Data CompiledClauses

Show CompiledClauses

Typeable CompiledClauses

Pretty CompiledClauses

Abstract CompiledClauses

Apply CompiledClauses

EmbPrj CompiledClauses

InstantiateFull CompiledClauses

litCase :: Literal -> c -> Case c

conCase :: QName -> c -> Case c

catchAll :: c -> Case c