as per issue https://github.com/agda/agda/issues/426, first cut at tr…

[cartazio]

…ying out enabling lazy evaluation in emacs agda-mode.

The long term solution is probably expose this choice as a cabal level build configure that then uses CPP in this module or something.

opening this PR as a discussion point for ticket #426

[UlfNorell]

The problem with using destructive updates in top-level emacs mode commands is that it has side effects on the state. For instance, if you ask for the normal form of a type and then ask for it non-normalised you'll still get the normal form, since it's been updated destructively.

[cartazio]

Ok. That makes sense. From a user stand point, could that be handled by
having the closure indirection hold both the original expression and the
result? Or by reloading the module of interest ?

On Monday, February 22, 2016, Ulf Norell notifications@github.com wrote:

The problem with using destructive updates in top-level emacs mode
commands is that it has side effects on the state. For instance, if you ask
for the normal form of a type and then ask for it non-normalised you'll
still get the normal form, since it's been updated destructively.

—
Reply to this email directly or view it on GitHub
#1867 (comment).

[UlfNorell]

Keeping the original expression in the indirection could be very expensive, and I'm not sure how much effort would be required to make it work. Reloading the module for every top-level command would be problematic for expensive modules.

In any case, the current --sharing implementation is not how we want to implement call-by-need--it's too brittle and error prone--so we won't spend any time improving it at the moment.