Agda.TypeChecking.Reduce.Fast

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 STRefs. 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 Literals.

Documentation

fastReduce :: Term -> ReduceM (Blocked Term)

The entry point to the reduction machine.

fastNormalise :: Term -> ReduceM Term