[CakeML] char literals

Konrad Slind konrad.slind at gmail.com
Tue Aug 25 15:29:57 UTC 2015


Thanks! I had for some reason thought that they weren't supported.

Konrad.


On Mon, Aug 24, 2015 at 11:07 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> 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/8025a92a/attachment.html>


More information about the Users mailing list