<div dir="ltr"><div><div>I would vote for immutable strings. That way HOL Light constants<br></div>couldn't have their names (perhaps maliciously) changed after<br>declaration.<br><br></div>Konrad.<br><br></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Mon, Feb 3, 2014 at 9:28 AM, Freek Wiedijk <span dir="ltr"><<a href="mailto:freek@cs.ru.nl" target="_blank">freek@cs.ru.nl</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hi Ramana,<br>
<div class="im"><br>
>For strings, are characters also required as a primitive type? String<br>
>comparisons? Should they be Unicode strings? I imagine an initial<br>
>version might implement strings as int arrays (or int vectors) and<br>
>support literals, size, maybe concat.<br>
<br>
</div>If I look at the HOL Light code base, what I see there is<br>
things like...<br>
<br>
String.get                      : string -> int -> char<br>
String.length                   : string -> int<br>
String.make                     : int -> char -> string<br>
<br>
Char.chr                        : int -> char<br>
Char.code                       : char -> int<br>
Num.num_of_string               : string -> Num.num<br>
Num.string_of_num               : Num.num -> string<br>
Pervasives.int_of_string        : string -> int<br>
Pervasives.string_of_float      : float -> string<br>
Pervasives.string_of_int        : int -> string<br>
Pervasives.( ^ )                : string -> string -> string<br>
String.escaped                  : string -> string<br>
String.sub                      : string -> int -> int -> string<br>
<br>
(plus i/o and formatter functions)<br>
<br>
... but many of those can be programmed given the others,<br>
I guess.<br>
<br>
I don't think I "need" unicode.  I also don't think having<br>
"char" be a synonym for "int" would really be a problem.<br>
In which case Char.chr and Char.code would just be the<br>
identity.<br>
<br>
Having "string" be a synonym of "int array" would be<br>
perfectly fine too for me too.  As long as you give me nice<br>
syntax for string literals (both on input and output)!<br>
<br>
Then only the array counterparts to the first three<br>
operations (suprisingly "String.set" doesn't seem to be used)<br>
(well, and maybe (^) for efficiency, although I'm not sure<br>
it would make a big difference) would be perfect.  I guess.<br>
<br>
So, if you want a specific wish: arrays + string literal<br>
syntax please! :-)<br>
<br>
(Or maybe vectors instead of arrays?  Apparently I don't<br>
seem to need updates.)<br>
<span class="HOEnZb"><font color="#888888"><br>
Freek<br>
</font></span></blockquote></div><br></div>