<div dir="ltr"><div>Thanks, Sergei. Even if the use of postulate is not enough to allow me to <br>advance in this particular case, your help is greatly appreciated <br>(I will consider using postulate from now on).<br></div>
<div><br>Cheers,<br><br>Carlos<br><div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Nov 7, 2013 at 9:39 AM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br>


<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div><div>On Wed, 2013-11-06 at 15:14 -0200, Carlos Camarao wrote:<br>
&gt; I am trying to write in Agda the simplest piece of code I can for<br>
&gt; proving soundness and completeness of a most general unification<br>
&gt; function; I think this is a good, instructive example of a problem<br>
&gt; that<br>
&gt; should have a simple but non-structurally recursive solution.<br>
&gt;<br>
&gt; In Unif.agda (all Agda files are annexed) I restricted the problem<br>
&gt; first to a function, mgu2, that is supposed to give the most general<br>
&gt; unifier of only two simple types, if it exists, together with the<br>
&gt; proofs that they are the least unifiers. Types are in Ty.agda and<br>
&gt; substitutions in Subst_list.agda.<br>
&gt;<br>
&gt; When Unif.agda is compiled (question marks are used in places to be<br>
&gt; filled latter), the compiler inserts holes, starting with { }₀ (do<br>
&gt; this, if you want, after copying all agda files into a subdirectory).<br>
&gt; When the cursor is placed inside { }₀, and Cntrl-c Cntrl-a is typed<br>
&gt; (meaning &#39;try to automatically fill the hole yourself if you can&#39;),<br>
&gt; the compiler inserts &quot;nothing&quot; in the place of { }₀.<br>
&gt;<br>
&gt; That is a bug (I think).<br>
&gt;<br>
&gt; Furthermore, if I delete the inserted &quot;nothing&quot; and insert &quot;just ?&quot;<br>
&gt; the program is accepted by the compiler. The compiler replaces &quot;?&quot; by<br>
&gt; &quot;{ }₀&quot;:<br>
&gt; an inconsistency, since &quot;nothing&quot; was considered before the<br>
&gt; only possibility (&quot;just ?&quot; should thus not be accepted).<br>
&gt;<br>
&gt; Trying to continue, if the &quot;case-of&quot; piece of code below is inserted<br>
&gt; (instead of a question mark):<br>
&gt;<br>
&gt;    case mgu2 (Var v) (Con c) of λ<br>
&gt;      { nothing → nothing ;<br>
&gt;        (just (s , _ , p₁)) → just ?<br>
&gt;<br>
&gt; then the compiler again replaces the question mark inside the case-of<br>
&gt; by a hole, say { }₀ (it becomes { }₀ by loading the file, i.e. by<br>
&gt; typing<br>
&gt; Cntrl-c Cntrl-l). By refining { }₀ (by typing Cntrl-c Cntrol-r), it<br>
&gt; becomes:<br>
&gt;<br>
&gt;    case mgu2 (Var v) (Con c) of λ<br>
&gt;      { nothing → nothing ;<br>
&gt;        (just (s , _ , p₁)) → just ({ }₀ , { }₁)<br>
&gt;<br>
&gt; Now, if I type Cntrl-c Cntrl-a inside the new hole { }₀,<br>
&gt; created by the compiler, the case-of becomes:<br>
&gt;<br>
&gt;    case mgu2 (Var v) (Con c) of λ<br>
&gt;      { nothing → nothing ;<br>
&gt;        (just (s , _ , p₁)) → just (proj₁ (p₁ .proj₁) , {!!}₁)<br>
&gt;<br>
&gt; But this code, inserted by the compiler itself, does not<br>
&gt; compile: typing Cntrl-c Cntrl-l gives the error message:<br>
&gt;<br>
<br>
</div></div>So far, my impression is that using interactive help with holes of {?}<br>
and such, cannot give an essential help in developing a program.<br>
<br>
(Though, I am a newbie, I may mistake).<br>
<br>
Instead, I proceed this way:<br>
<br>
    ... → just v1   where<br>
                    postulate v1 : Foo<br>
<br>
and set for  Foo  the type which I guess is needed.<br>
If the type checker rejects this, I try to improve Foo.<br>
After Foo is done, I remove `postulate&#39;, and start with defining<br>
v1 = ...<br>
After everything is checked, I remove some declarations like  v1 : Foo<br>
-- the ones that do not essentially help with readability.<br>
<br>
The idea is that if I do not know where and what is the error, I split<br>
the code into the type declaration for its parts. Then, run the checker<br>
by  C-c C-l,  and split each part further -- until I find which type<br>
needs improvement.<br>
<br>
Regards,<br>
<br>
-------<br>
Sergei<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
</blockquote></div><br></div></div></div></div>