[Agda] Agda bug

[Ulf Norell]

On Thu, Nov 7, 2013 at 1:43 PM, Carlos Camarao <carlos.camarao at gmail.com>wrote:

> On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl <kahl at cas.mcmaster.ca> wrote:
>
>     Carlos,
>
>     On Wed, Nov 06, 2013 at 03:14:57PM -0200, Carlos Camarao wrote:
>       When the cursor is placed inside { }₀, and Cntrl-c Cntrl-a is typed
>     > (meaning 'try to automatically fill the hole yourself if you can'),
>     > the compiler inserts "nothing" in the place of { }₀.
>     >
>     > That is a bug (I think).
>     >
>     > Furthermore, if I delete the inserted "nothing" and insert "just ?"
>     > the program is accepted by the compiler. The compiler replaces "?"
> by "{
>     > }₀":
>     > an inconsistency, since "nothing" was considered before the
>     > only possibility ("just ?" should thus not be accepted).
>
>     "nothing" was considered not as the ``only possibility'',
>     but as the ``first possibility that worked''.
>
>     To see all possibilities that are considered to work,
>     insert ``-l'' into the whole before hitting C-c C-a.
>
> Ok. Thanks.
>
> I'd expect (and suggest) a different behavior: that by default (that
> is, if nothing, i.e. no "-l", is inserted) auto would only fill a hole
> if a unique solution was found; the behavior of inserting the first
> found solution (or of showing all found solutions) should have to be
> explicitly indicated.
>
> The documentation (from
> http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Auto) is not
> very clear about auto's behavior:
>
> "Search parameters are given by entering them into the hole before
> invocation. Giving no arguments is fine and results in a search with
> default parameters. The search carries on until either a solution is
> found, the search space is fully (and unsuccessfully) explored or it
> times out (5 seconds by default). Here follows a list of the different
> modes and parameters. ..."
>
> I had not read this, but even if I had, I could interpret "a solution"
> (in "The search carries on until either a solution..." above) as
> "a unique solution": I think this is what auto should do unless
> otherwise explicitly indicated.
>

There are a few problems with this approach:
- It would mean auto could only be used in cases where the search space
  can be exhaustively explored in a short time. You wouldn't want auto to
  spend a lot of time just to make sure that the solution it found right
away
  is the unique one.
- Often you don't care about having a unique solution. For example, if you
  want it to prove some simple lemma any proof would do.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131107/00ef8956/attachment.html