<br><div class="gmail_quote">On Fri, Oct 29, 2010 at 10:36 PM, Alan Jeffrey <span dir="ltr">&lt;<a href="mailto:ajeffrey@bell-labs.com">ajeffrey@bell-labs.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Yay, victory!  Or very close to it...  (# 2 + # 2) now generates:<br>
<br>
MAlonzo.System.IO.Examples.Four.d42 = GHC.Integer.Type.S# 2<br>
MAlonzo.System.IO.Examples.Four.d41 =<br>
  GHC.Integer.plusInteger<br>   MAlonzo.System.IO.Examples.Four.d42<br>
    MAlonzo.System.IO.Examples.Four.d42<br>
<br>
No intermediate conversions, hooray!  The only gotcha is we need a place for the following RULES to live... any chance you could generate them along with the converter functions?<br>
<br>
{-# RULES &quot;i-n-i&quot; forall x . mazNatToInteger (mazIntegerToNat x) = x #-}<br>
{-# RULES &quot;n-i-n&quot; forall x . mazIntegerToNat (mazNatToInteger x) = x #-}<br></blockquote><div><br></div><div>These coercions are now generated together with conversion functions. </div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

The other issue is that at the moment, every module is getting its own mazCoerce function, which means that there&#39;s no way to write coercion-aware FFI libraries (e.g. for stream fusion).  Fixing this would involve generating a tiny run time system, which the compiler is currently avoiding.</blockquote>
<div><br></div><div>I&#39;ve put mazCoerce in its own module MAlonzo.RTE (the other generated modules end up in MAlonzo.Code.*). That way you should be able to write coercion-aware libraries as long as you compile them together with the Agda program. Hopefully that&#39;ll work for now, but eventually I guess we should put it in a cabal package that is installed together with Agda.</div>
<div><br></div><div>/ Ulf</div><div><br></div></div>