<div dir="ltr">Thanks! I had for some reason thought that they weren't supported.<div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Aug 24, 2015 at 11:07 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><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>Character literals are just an addition to the REPL parser. All the rest described below was, I believe, already available.<br></div><div><br>The REPL supports Char.ord and Char.chr, e.g.:<br><br>Char.chr 107;<br>val it:<char> = #"k"<br><br></div>(The full library available can be gleaned from <a href="https://github.com/CakeML/cakeml/blob/master/semantics/initialProgram.lem" target="_blank">https://github.com/CakeML/cakeml/blob/master/semantics/initialProgram.lem</a>)<br><br></div>Also, the translator supports characters, e.g.,:<br><br>> val upchr_def = ml_translatorLib.mlDefine`upchr n = CHR (n + (ORD #"A"))`;<br><br>WARNING: upchr has a precondition.<br><br>|- DeclAssum NONE scratch_decls_2 env tys ∧<br>   PRECONDITION (upchr_side v1) ⇒<br>   Eval env (Var (Short "upchr")) ((Eq NUM v1 --> CHAR) upchr)<br><br>val upchr_def =<br>   |- ∀n. upchr n = CHR (n + ORD #"A"):<br>   thm<br><br>In case you're interested, the side condition is:<br><br>|- ∀v1. upchr_side v1 ⇔ v1 + 65 < 256<br><br></div>and the code AST:<br><br>   Fun "v1"<br>     (App Chr<br>        [App (Opn Plus) [Var (Short "v1"); App Ord [Lit (Char #"A")]]])<br><br><br><div><br><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 25 August 2015 at 09:46, 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">Would that mean that the translator understands characters (Char.ord and Char.chr<div>in particular)?</div><div><br></div><div>Konrad.</div><div><br></div></div><div class="gmail_extra"><br><div class="gmail_quote"><span>On Mon, Aug 24, 2015 at 6:30 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></span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span><div dir="ltr">The version 1 beta of CakeML (available for download from <a href="https://cakeml.org" target="_blank">https://cakeml.org</a>) now also supports character literals (thanks to Michael for implementing them, and Yong Kiam for fixing proofs).<br></div>
<br></span>_______________________________________________<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>