[Agda] Agda bug

[Carlos Camarao]

Thanks, Sergei. Even if the use of postulate is not enough to allow me to
advance in this particular case, your help is greatly appreciated
(I will consider using postulate from now on).

Cheers,

Carlos

On Thu, Nov 7, 2013 at 9:39 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Wed, 2013-11-06 at 15:14 -0200, Carlos Camarao wrote:
> > I am trying to write in Agda the simplest piece of code I can for
> > proving soundness and completeness of a most general unification
> > function; I think this is a good, instructive example of a problem
> > that
> > should have a simple but non-structurally recursive solution.
> >
> > In Unif.agda (all Agda files are annexed) I restricted the problem
> > first to a function, mgu2, that is supposed to give the most general
> > unifier of only two simple types, if it exists, together with the
> > proofs that they are the least unifiers. Types are in Ty.agda and
> > substitutions in Subst_list.agda.
> >
> > When Unif.agda is compiled (question marks are used in places to be
> > filled latter), the compiler inserts holes, starting with { }₀ (do
> > this, if you want, after copying all agda files into a subdirectory).
> > 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).
> >
> > Trying to continue, if the "case-of" piece of code below is inserted
> > (instead of a question mark):
> >
> >    case mgu2 (Var v) (Con c) of λ
> >      { nothing → nothing ;
> >        (just (s , _ , p₁)) → just ?
> >
> > then the compiler again replaces the question mark inside the case-of
> > by a hole, say { }₀ (it becomes { }₀ by loading the file, i.e. by
> > typing
> > Cntrl-c Cntrl-l). By refining { }₀ (by typing Cntrl-c Cntrol-r), it
> > becomes:
> >
> >    case mgu2 (Var v) (Con c) of λ
> >      { nothing → nothing ;
> >        (just (s , _ , p₁)) → just ({ }₀ , { }₁)
> >
> > Now, if I type Cntrl-c Cntrl-a inside the new hole { }₀,
> > created by the compiler, the case-of becomes:
> >
> >    case mgu2 (Var v) (Con c) of λ
> >      { nothing → nothing ;
> >        (just (s , _ , p₁)) → just (proj₁ (p₁ .proj₁) , {!!}₁)
> >
> > But this code, inserted by the compiler itself, does not
> > compile: typing Cntrl-c Cntrl-l gives the error message:
> >
>
> So far, my impression is that using interactive help with holes of {?}
> and such, cannot give an essential help in developing a program.
>
> (Though, I am a newbie, I may mistake).
>
> Instead, I proceed this way:
>
>     ... → just v1   where
>                     postulate v1 : Foo
>
> and set for  Foo  the type which I guess is needed.
> If the type checker rejects this, I try to improve Foo.
> After Foo is done, I remove `postulate', and start with defining
> v1 = ...
> After everything is checked, I remove some declarations like  v1 : Foo
> -- the ones that do not essentially help with readability.
>
> The idea is that if I do not know where and what is the error, I split
> the code into the type declaration for its parts. Then, run the checker
> by  C-c C-l,  and split each part further -- until I find which type
> needs improvement.
>
> Regards,
>
> -------
> Sergei
>
>
>
>
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131107/732f3118/attachment.html