[CakeML] char literals

[Ramana Kumar]

Character literals are just an addition to the REPL parser. All the rest
described below was, I believe, already available.

The REPL supports Char.ord and Char.chr, e.g.:

Char.chr 107;
val it:<char> = #"k"

(The full library available can be gleaned from
https://github.com/CakeML/cakeml/blob/master/semantics/initialProgram.lem)

Also, the translator supports characters, e.g.,:

> val upchr_def = ml_translatorLib.mlDefine`upchr n = CHR (n + (ORD #"A"))`;

WARNING: upchr has a precondition.

|- DeclAssum NONE scratch_decls_2 env tys ∧
   PRECONDITION (upchr_side v1) ⇒
   Eval env (Var (Short "upchr")) ((Eq NUM v1 --> CHAR) upchr)

val upchr_def =
   |- ∀n. upchr n = CHR (n + ORD #"A"):
   thm

In case you're interested, the side condition is:

|- ∀v1. upchr_side v1 ⇔ v1 + 65 < 256

and the code AST:

   Fun "v1"
     (App Chr
        [App (Opn Plus) [Var (Short "v1"); App Ord [Lit (Char #"A")]]])





On 25 August 2015 at 09:46, Konrad Slind <konrad.slind at gmail.com> wrote:

> Would that mean that the translator understands characters (Char.ord and
> Char.chr
> in particular)?
>
> Konrad.
>
>
> On Mon, Aug 24, 2015 at 6:30 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>
>> The version 1 beta of CakeML (available for download from
>> https://cakeml.org) now also supports character literals (thanks to
>> Michael for implementing them, and Yong Kiam for fixing proofs).
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20150825/ae45a284/attachment.html>