Agda: Support step-by-step evaluation

[mdimjasevic]

Agda does not feature a step-by-step expression evaluation. This is a useful feature in aiding the understanding of code, in debugging and probably in other situations. C-c C-n in Emacs runs the command agda2-compute-normalised-maybe-toplevel, but this gives the final result only. As @jespercockx pointed it out, one's "best bet is to put {-# OPTIONS -v tc.reduce.fast:110 #-} which will print the steps of the AAM (Agda Abstract Machine) but the output is not very user-friendly."

@jespercockx said in Agda's #general Slack channel:

Alternatively we could add a separate function to unfold a term by one step. Currently we have the functions reduce, normalise, simplify, instantiate, and instantiateFull, we could add unfold. We could even avoid code duplication by making the (non-AAM version of) reduce make use of unfold. We could then have an emacs command that prints out the next N unfoldings of the given term.

He continued with:

I think the first step would be to look at the Reduce class in https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Reduce.hs and try to define a variant of it that avoids the recursive calls. This will probably involve some judgement calls as to what exactly constitutes a "single unfolding step". If this works out well, we could in a next phase try to implement Reduce in terms of this new single-step unfolding (but I wouldn't focus on that until we know it works well).

and this:

Some functions in there such as unfoldDefinitionE already take a continuation as an argument, so it should be possible to reuse them for single-step unfolding without too much hasstle.

I'm opening this issue with the aim of discussing implementation details and concerns of this feature to be added to Agda.

[mdimjasevic]

You can find my latest progress on implementing the feature at https://github.com/mdimjasevic/agda/tree/issue4747.

[nad]

Have you made any progress on this?

[mdimjasevic]

@nad , unfortunately I have not.