[Agda] Devel: How to get back normalisation instead of simplification?

[Guillaume Brunerie]

You can use the prefix C-u C-u to get full normalisation.

Do you really need full normalisation or do you think this is a bug in
the simplification algorithm?
(see https://code.google.com/p/agda/issues/detail?id=850 for some
explanations on simplification, in particular it does not work as
expected yet, see comment #10)


>From the release notes:

* Key bindings for controlling simplification/normalisation:

  [TODO: Simplification should be explained somewhere.]

  Commands like "Goal type and context" (C-c C-,) could previously be
  invoked in two ways. By default the output was normalised, but if a
  prefix argument was used (for instance via C-u C-c C-,), then no
  explicit normalisation was performed. Now there are three options:

  * By default (C-c C-,) the output is simplified.

  * If C-u is used exactly once (C-u C-c C-,), then the result is
    neither (explicitly) normalised nor simplified.

  * If C-u is used twice (C-u C-u C-c C-,), then the result is
    normalised.


Guillaume

2013/7/1 Wolfram Kahl <kahl at cas.mcmaster.ca>:
> On Sun, Jun 23, 2013 at 10:28:50PM -0400, Wolfram Kahl wrote:
>> On Sat, Jun 22, 2013 at 08:27:20PM +0200, Andreas Abel wrote:
>> > if you have some large terms in you developments and have not pulled
>> > Agda recently, it might be worth trying.  I have implemented some
>> > performance improvements that are probably noticeable if you use records
>> > a lot.  The relevant patches concern "issue 854".
>> >
>> > James reported a reduction of memory consumption from 12GB to 3GB for
>> > one of his developments.
>> >
>> > In case you see similar improvements, please reply to this message.
>>
>> Wonderful!
>
> ... so I switched to the current development version.
>
> But now the following gets in the way:
>
>  | Mon May 20 06:33:15 EDT 2013  Andreas Abel <andreas.abel at ifi.lmu.de>
>  |   * Switched to simplification (instead of normalisation) in emacs interaction.
>  |   This is for experimentation purposes.
>  |   Key-bindings for full normalisation should also be added.
>
> Since there is already a distinction achieved via C-u
> in the display of goals and context (see
>   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.EmacsModeKeyCombinations
> ), perhaps it would be natural to expand on that,
> making that distinction ternary instead of the current binary,
> by adding simplified version via a special C-u prefix?
>
> (In Emacs , C-u in general serves to pass a |just| argument of type
>  |Maybe Integer| to the following command;
>  just C-u without a numeric argument seems to pass |just 4|).
>
> Otherwise, is there a simple way to switch back to full normalisation
> as one of the options?
>
>
> Wolfram
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda