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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Reduce.Fast

Description

This module implements the Agda Abstract Machine used for compile-time reduction. It's a call-by-need environment machine with an implicit heap maintained using `STRef`s. See the `AM` type below for a description of the machine.

Some other tricks that improves performance:

- Memoise getConstInfo.

A big chunk of the time during reduction is spent looking up definitions in the signature. Any long-running reduction will use only a handful definitions though, so memoising getConstInfo is a big win.

- Optimised case trees.

Since we memoise getConstInfo we can do some preprocessing of the definitions, returning a `CompactDef` instead of a `Definition`. In particular we streamline the case trees used for matching in a few ways:

- Drop constructor arity information.
- Use NameId instead of QName as map keys.
- Special branch for natural number successor.

None of these changes would make sense to incorporate into the actual case trees. The first two loses information that we need in other places and the third would complicate a lot of code working with case trees.

`CompactDef` also has a special representation for built-in/primitive functions that can be implemented as pure functions from `Literal`s.

Synopsis

- fastReduce :: Term -> ReduceM (Blocked Term)
- fastNormalise :: Term -> ReduceM Term

# Documentation

fastReduce :: Term -> ReduceM (Blocked Term) Source #

The entry point to the reduction machine.

fastNormalise :: Term -> ReduceM Term Source #