[Agda] evaluation in compilation

[Nils Anders Danielsson]

On 2012-10-01 12:34, Serge D. Mechveliani wrote:
> Please, how to prevent a compilation time evaluation?

There is no general, simple way to do this. If you can make sure that
the type-checker doesn't need to normalise your definition, and the
type-checker isn't overly "strict", then compile-time evaluation is
hopefully avoided (when the MAlonzo backend is used).

If the type-checker is too "strict", please report this on the bug
tracker.

Maybe we should modify the compiler infrastructure so that the backends
work on code that is closer to what the user wrote. This can perhaps be
accomplished by storing (at most) two copies of each definition, only
one of which is unfolded. I'm not quite sure what to do about
unification, though: should meta-variables also be instantiated in two
different ways?

Does anyone know if this problem has been addressed in the literature?

-- 
/NAD