<div dir="ltr">Hi Yong Kiam,<div><br></div><div>To get the asts printed, Magnus advised invoking</div><div><br></div><div> ml_translatorLib.print_asts := true</div><div><br></div><div>in my Script file, after I had made all the definitions and before export_theory().</div><div><br></div><div>Will this still work?</div><div><br></div><div>Thanks,</div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Aug 12, 2015 at 10:11 AM, Yong Kiam Tan <span dir="ltr"><<a href="mailto:tanyongkiam@gmail.com" target="_blank">tanyongkiam@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"><div>Hi Konrad,<br></div><div><br></div><div>I'm not sure how exactly you are printing the declarations, I have added semicolons for each declaration in the pretty printer now but the way I used to print them from HOL was to print the whole thing as a list of decls (so the semicolons get automatically added after each decl).</div><div><br></div><div>For reference, my printing code was something like:</div><div>val _ = enable_astPP();</div><div>val _ = set_trace "pp_avoids_symbol_merges" 0;</div><div><br></div><div>val _ = finalise_translation();</div><div>val decls = get_decls() in print(term_to_string decls) end; </div><div><br></div><div>(I guess this now needs to change to print each decl separately instead of just as a list).</div><div><br></div><div>Let me know if the latest update to astPP doesn't work for you (I could probably help if you sent me the declarations you wanted printed as well since I think those got lost in the email).</div><div><br></div><div> </div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Wed, Aug 12, 2015 at 5:47 AM, 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 class="h5"><div dir="ltr"><div><div>(I actually think these emails should be on the CakeML Users mailing list - redirecting there.)<br><br></div>Konrad, I think you're right that astPP should add semicolons, since CakeML expects them. I'll add an issue for this. (<a href="https://github.com/CakeML/cakeml/issues/54" target="_blank">https://github.com/CakeML/cakeml/issues/54</a>)<br><br></div>You're also right that it probably doesn't do anything special regarding vectors at the moment. But what should it do? (I.e., what's going wrong with them?)<br></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 12 August 2015 at 02:16, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Got the wrong email address for Yong Kiam. This time with his gmail address.<div><div><br><div class="gmail_quote">On Tue, 11 Aug 2015 at 18:12, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I think Yong Kiam and Ramana ought to be included in these emails. I've included them. -- Magnus<br><div class="gmail_quote">On Tue, 11 Aug 2015 at 18:03, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">.... having some trouble expressing myself: print_ast prints out everything fine, but<div>the generated syntax isn't accepted by the cakeml REPL.</div></div><div dir="ltr"><div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 11, 2015 at 10:53 AM, 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">print_asts works pretty well, but doesn't get all the way through the file.<div>Quick comments:</div><div><br></div><div>1. cakeml repl demands semicolon to terminate declaration. But print_ast doesn't</div><div> add these.</div><div><br></div><div>2. print_asts may not know about Vector and operations on it.</div><span><font color="#888888"><div><br></div><div>Konrad.</div><div><br></div></font></span></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 11, 2015 at 9:09 AM, 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">Thanks!<div><br></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Aug 11, 2015 at 9:06 AM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Yes, the translator can be made to print concrete syntax. The printer isn't 100 % reliable (bug reports are appreciated). To print concrete syntax, write<br><br>val _ = (print_asts := true)<br><br>in your script file where the translation happens. Running Holmake should produce some sml files with the concrete syntax.<br><br>I'm not at a computer at the moment so can't try this at the moment...<br><br>Cheers,<br>Magnus<div><div><br><div class="gmail_quote">On Tue, 11 Aug 2015 at 15:58, Konrad Slind <<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div> My message was a bit terse. To build the example:</div><div><br></div><div>1. update <cakeml>/translator/{ml_translatorScript.sml,ml_translatorLib.sml} </div><div> with the attached files. Note that these new versions will build okasaki-examples</div><div> and other-examples directories.</div><div>2. Put all the other files in a new directory foo</div><div>3. Invoke Holmake regexpTheory.uo</div><div><br></div><div>Now a question: using the translator I think I have built up an internal environment</div><div>of cakeML ASTs corresponding to the original HOL definitions. Does cakeML </div><div>provide a way to get these ASTs printed out in cakeML concrete syntax?</div><div><br></div><div>Thanks,</div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote"></div></div><div class="gmail_extra"><div class="gmail_quote">On Mon, Aug 10, 2015 at 6:11 PM, Konrad Slind <span dir="ltr"><<a href="mailto:konrad.slind@gmail.com" target="_blank">konrad.slind@gmail.com</a>></span> wrote:<br></div></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi all,<div><br></div><div> I got the regexp matcher to finally get through the translator. In order to do </div><div>this, I had to do some revision to the definitions, and I also had to fix a </div><div>problem with "v" in ml_translatorLib.sml and ml_translatorScript.sml. </div><div>All this should be in the attached files.</div><div><br></div><div>Some notes on what I learned are in trans.notes.txt.</div><div><br></div><div>The problem with v: some code in the translator depends on this name. But if the</div><div>definition to be translated also has a variable named "v" problems occur. I worked</div><div>around this by changing the translator to use "_v" in various places, and also</div><div>changing the use of "v" in some definitions in ml_translatorScript.sml.</div><div><br></div><div>I am still puzzled that mergesort_def won't translate, but I've swapped that out</div><div>in favour of QSORT, which translates with no problem.</div><div><br></div><div>Cheers,</div><div>Konrad.</div><div><br></div></div>
</blockquote></div></div></blockquote></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>
</blockquote></div></blockquote></div>
</div></div></blockquote></div><br></div>
</div></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>