strings, chars, and OCaml
Note: This related to module string.OCaml in the standard library. May be the module name string.OCaml is not the right one. Any suggestion for a better name is welcome.
Regarding OCaml characters, here is a proposal: in string.OCaml, declare a type char
such as
type char = private { char: string; ) invariant { length char = 1 }
so that we could declare a function
val ([]) (s: string) (i: int63) : char requires { 0 <= i < length s } ensures { result.char = s[i] }
which would be mapped to String.get directly (and not to "String.make 1 (String.get ...)" as it is currently) in the OCaml driver.