Hi,<div><br></div><div>I've read this blogpost</div><div><br></div><div><a href="http://adventuresinmercury.blogspot.com/2011/04/dependent-typing-reversing-non-empty.html">http://adventuresinmercury.blogspot.com/2011/04/dependent-typing-reversing-non-empty.html</a></div>
<div><br></div><div>And thought, I could try to implement smth like even- (odd-) sized list using appropriate modes.</div><div>I tried next:</div><div><br></div><div><div>:- module lists1.</div><div><br></div><div>:- interface.</div>
<div><br></div><div>:- import_module io.</div><div><br></div><div>:- pred main(io::di, io::uo) is det.</div><div><br></div><div>:- implementation.</div><div><br></div><div>:- import_module list.</div><div><br></div><div>%:- inst even_list ---> [] ; [ground|even_list]. % XXX</div>
<div>:- inst even_list ---> [] ; [ground,ground|even_list]. % YYY</div><div><br></div><div>%:- type even_list(T) ---> []; [T,T|even_list(T)].</div><div><br></div><div>%:- pred t(even_list(int)).</div><div>:- pred t(list(int)).</div>
<div>:- mode t(in(even_list)) is semidet.</div><div>t([1,2,3,4]).</div><div><br></div><div>main(!IO) :-</div><div><span class="Apple-tab-span" style="white-space:pre">   </span>L=[1,2,3,4,5,6],</div><div><span class="Apple-tab-span" style="white-space:pre">     </span>%L=[1,2,3,4,5,6,7],</div>
<div><span class="Apple-tab-span" style="white-space:pre">      </span>(<span class="Apple-tab-span" style="white-space:pre">   </span>t(L) -></div><div><span class="Apple-tab-span" style="white-space:pre">           </span>print("1",!IO)</div>
<div><span class="Apple-tab-span" style="white-space:pre">      </span>;</div><div><span class="Apple-tab-span" style="white-space:pre">            </span>print("2",!IO)</div><div><span class="Apple-tab-span" style="white-space:pre">     </span>).</div>
</div><div><br></div><div>But this resulted in</div><div><br></div><div><div>D:\stuff\test\mercury\deptypes>mmc.bat --make lists1</div><div>Making Mercury\int3s\lists1.int3</div><div>Making Mercury\ints\<a href="http://lists1.int">lists1.int</a></div>
<div>Making Mercury\cs\lists1.c</div><div>lists1.m:014: In definition of inst `lists1.even_list'/0:</div><div>lists1.m:014:   error: undefined inst `[|]'/2.</div><div>Error: system command received signal 1.</div>
<div>** Error making `Mercury\cs\lists1.c'.</div></div><div><br></div><div>Note, that if I comment YYY line and uncomment XXX - code compiles well.</div><div>My will is that I could compile code with L=[1,2,3,4,5,6] (even sized list) but not with L=[1,2,3,4,5,6,7] (odd).</div>
<div><br></div><div>Is this possible with mercury?</div><div><br></div><div>Sincerely yours,</div><div>Vladimir.</div>