[CakeML] cakeML wish list

[Freek Wiedijk]

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