[Agda] Agda bug

[Carlos Camarao]

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.

    > /home/camarao/agda/bugs/bug5/Unif.agda:96,44-50
    > .proj₁ is not a valid expression.
    > when scope checking .proj₁
    >
    > That is another bug (I think) (if it does not compile, it should have
    > not been inserted). I am using compiler 2.3.0.1.
    The dot is warning you that the following identifier is currently not
in scope ---
    you need to change the code to bring it into scope. Here, add:

    open import Data.Product using (proj₁)

open import Data.Product using (proj₁) is there...

    Hope this helps!

    Wolfram

Thanks a lot.

Cheers,

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