[Agda] Agda bug

[Carlos Camarao]

On Thu, Nov 7, 2013 at 2:30 PM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

    On 2013-11-07 13:43, Carlos Camarao wrote:

        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.

    I've modified the text on the wiki:

      "The search carries on until either a (not necessarily unique)
      solution is found, ..."

    If Agda's unifier instantiates a meta-variable with a non-unique
    solution, then this is a bug. However, C-c C-a is allowed to find
    non-unique solutions.

Thanks a lot.

I'd suggest to include a -u "parameter", to allow a unique solution to be
searched.
And also perhaps highlight the issue by modifying the wiki, right at the
1st paragraph,
as follows:

===================
Auto

Agda supports (since version 2.2.6) command ‘Auto’, that performs a
search for a type inhabitant, which is then used to fill a hole.

The existence of a unique type inhabitant can be specified,
via parameter -u (read about parameters below).

Auto can be used as an aid when interactively ...

Usage
...
Here follows a list of the different modes and parameters.
...
Listing and selecting solutions

By default, Auto replaces the hole with the first solution found.

Parameter -u can change this behavior: it indicates that the hole should
be replaced only if a unique solution exists.

The list of the ten (at most) first solutions encountered can be
included by using flag -l.

A particular solution can be selected by writing -s <n>, ...

===================

        On Wed, Nov 6, 2013 at 5:18 PM, Wolfram Kahl
             <kahl at cas.mcmaster.ca <mailto:kahl at cas.mcmaster.ca>>
             wrote: 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...

    The name .proj₁ does not refer to Data.Product.proj₁. I think it
    refers to the underscore in "just (s , _ , p₁)".

Yes. I think it is a little bug, or a strange behaviour.

I replaced the case-of by:

 case mgu2 (Var v) (Con c) of λ
   { nothing → nothing ;
     (just (s , p , p₁)) → just (s , comm_unif2' p , {!!})
   }

Thanks, cheers,

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