[Agda] Bounties for Agda features

[Andreas Abel]

On 07.05.12 7:06 PM, Daniel Peebles wrote:
> *Come up with a neat solution to control depth of evaluation locally*
>
> See http://code.google.com/p/agda/issues/detail?id=433
>
> I see this mostly as an ease-of-use feature, but it might also help
> performance. Basically, often you really don't want terms to normalize
> fully in your goals or context. Some of my proofs have goals whose
> normal forms are thousands (literally) of lines long, so the goal output
> becomes effectively unusable.
>
> Most of the time, I want to work at a higher level of abstraction than
> individual recursively defined functions, and I've already proved simple
> lemmas about them. In those cases, I don't want simple definitions to
> normalize past a certain point, and want to prove things about the
> higher-level expressions.
>
> For example, when I'm writing simple proofs about the algebraic
> properties of operations on the naturals, I might want my definitions to
> normalize, but other times I might not. For example, (1 + x) + ((1 + y)
> * (1 + z)) will normalize to the horrible suc (x + suc (z + y * suc z)).
> If I have a proof about the original form, it takes a lot of squinting
> to realize that the normal form applies to it.

Well, a simple heuristics would be to only unfold definitions when 
making progress, where progress means that a constructor-pattern matched 
and an equation fired.

Unfortunately, that would still destroy your beautiful 1 + x.

However,  Data.List's

   any p xs

would not be unfolded to

   foldr _v_ false (map p xs).

Which would already be something.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/