<div dir="ltr"><div><div>Thanks Konrad.<br><br></div>Does your translation work with the latest version of the CakeML translator?<br></div><br>I tried following your approach and still run into a failed translation. (I rewrote DIV2 away rather than translating it, but I don't think that should be the cause of the problem..)<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 15 April 2016 at 13:42, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Looking a bit more at this ... the reason we take <div>the last conjunct of mergesortN_def is because all </div><div>the ones before that are subsumed in the last one. </div><div>Maybe the redundancy is confusing the translator.</div><span class="HOEnZb"><font color="#888888"><div><br></div><div>Konrad.</div><div><br></div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 14, 2016 at 10:34 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">What is called in my development (this is used in the regexp compiler).<div><br></div><div> val thms = <div>List.map translate </div><div> [mergesortTheory.sort2_def,</div><div> mergesortTheory.sort3_def, </div><div> mergesortTheory.merge_def,</div><div> arithmeticTheory.DIV2_def,</div><div> listTheory.DROP_def,</div><div> last(CONJUNCTS mergesortTheory.mergesortN_def),</div><div> mergesortTheory.mergesort_def];</div><div><br></div><div><br></div><div><br></div><div> </div></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Apr 14, 2016 at 10:13 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">This sounds familiar. I got mergesortN to translate.<div>Might have had to fix the translator in order to make it go through.</div><div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div>On Thu, Apr 14, 2016 at 9:44 PM, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div dir="ltr"><div><div><div><div>Hi,<br><br></div>I am trying to use the CakeML translator to translate mergesort from HOL's mergesortTheory. The main function to translate is mergesortN_def, printed below. But the translator fails. Why? I translated sort2 and sort3 and DROP already, so I don't think they are the problem.<br><br>val it =<br> |- (∀l R. mergesortN R 0 l = []) ∧<br> (∀x l R. mergesortN R 1 (x::l) = [x]) ∧<br> (∀R. mergesortN R 1 [] = []) ∧<br> (∀y x l R. mergesortN R 2 (x::y::l) = sort2 R x y) ∧<br> (∀x R. mergesortN R 2 [x] = [x]) ∧ (∀R. mergesortN R 2 [] = []) ∧<br> (∀z y x l R. mergesortN R 3 (x::y::z::l) = sort3 R x y z) ∧<br> (∀y x R. mergesortN R 3 [x; y] = sort2 R x y) ∧<br> (∀x R. mergesortN R 3 [x] = [x]) ∧ (∀R. mergesortN R 3 [] = []) ∧<br> ∀v4 l R.<br> mergesortN R v4 l =<br> if v4 = 0 then []<br> else if v4 = 1 then case l of [] => [] | x::l' => [x]<br> else if v4 = 2 then<br> case l of [] => [] | [x'] => [x'] | x'::y::l'' => sort2 R x' y<br> else if v4 = 3 then<br> case l of<br> [] => []<br> | [x''] => [x'']<br> | [x''; y'] => sort2 R x'' y'<br> | x''::y'::z::l''' => sort3 R x'' y' z<br> else<br> (let len1 = v4 DIV 2<br> in<br> merge R (mergesortN R (v4 DIV 2) l)<br> (mergesortN R (v4 − len1) (DROP len1 l))):<br> thm<br><br>Translating mergesortn<br>metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+0+0+0+0!<br>metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+0+0+0+0!<br>metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+0+0+0+0!<br>Failed translation: mergesortN<br>Exception- HOL_ERR {message = "no solution found", origin_function = "FOL_FIND", origin_structure = "folTools"} raised<br><br></div>I to looks like there's a lot of pattern matching in the definition. What is the status of HOL issue #285 (<a href="https://github.com/HOL-Theorem-Prover/HOL/issues/285" target="_blank">https://github.com/HOL-Theorem-Prover/HOL/issues/285</a>)? I think that might be able to help.<br><br></div>Looking forward to your reply,<br></div>Ramana<br></div>
<br></div></div>_______________________________________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org" target="_blank">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/listinfo/users</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>