[CakeML] cakeML wish list

[Konrad Slind]

I would vote for immutable strings. That way HOL Light constants
couldn't have their names (perhaps maliciously) changed after
declaration.

Konrad.



On Mon, Feb 3, 2014 at 9:28 AM, Freek Wiedijk <freek at cs.ru.nl> wrote:

> Hi Ramana,
>
> >For strings, are characters also required as a primitive type? String
> >comparisons? Should they be Unicode strings? I imagine an initial
> >version might implement strings as int arrays (or int vectors) and
> >support literals, size, maybe concat.
>
> If I look at the HOL Light code base, what I see there is
> things like...
>
> String.get                      : string -> int -> char
> String.length                   : string -> int
> String.make                     : int -> char -> string
>
> Char.chr                        : int -> char
> Char.code                       : char -> int
> Num.num_of_string               : string -> Num.num
> Num.string_of_num               : Num.num -> string
> Pervasives.int_of_string        : string -> int
> Pervasives.string_of_float      : float -> string
> Pervasives.string_of_int        : int -> string
> Pervasives.( ^ )                : string -> string -> string
> String.escaped                  : string -> string
> String.sub                      : string -> int -> int -> string
>
> (plus i/o and formatter functions)
>
> ... but many of those can be programmed given the others,
> I guess.
>
> I don't think I "need" unicode.  I also don't think having
> "char" be a synonym for "int" would really be a problem.
> In which case Char.chr and Char.code would just be the
> identity.
>
> Having "string" be a synonym of "int array" would be
> perfectly fine too for me too.  As long as you give me nice
> syntax for string literals (both on input and output)!
>
> Then only the array counterparts to the first three
> operations (suprisingly "String.set" doesn't seem to be used)
> (well, and maybe (^) for efficiency, although I'm not sure
> it would make a big difference) would be perfect.  I guess.
>
> So, if you want a specific wish: arrays + string literal
> syntax please! :-)
>
> (Or maybe vectors instead of arrays?  Apparently I don't
> seem to need updates.)
>
> Freek
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140203/b7be6931/attachment.html>