Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

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) |
Abstract a => Abstract (WithArity a) |
Apply a => Apply (WithArity a) |
InstantiateFull a => InstantiateFull (WithArity a) |
EmbPrj a => EmbPrj (WithArity a) |

data Case c

Constructors

Branches |

Fields

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

Instances

Functor Case |
Typeable1 Case |
Foldable Case |
Traversable Case |
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) |
InstantiateFull a => InstantiateFull (Case a) |
EmbPrj a => EmbPrj (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

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 |

emptyBranches :: Case c

litCase :: Literal -> c -> Case c

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

catchAll :: c -> Case c