diff options
Diffstat (limited to 'lib/unicode.mli')
| -rw-r--r-- | lib/unicode.mli | 32 |
1 files changed, 23 insertions, 9 deletions
diff --git a/lib/unicode.mli b/lib/unicode.mli index 520203d4..2609e196 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -8,21 +8,35 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol +type status = Letter | IdentPart | Symbol | Unknown -exception Unsupported - -(** Classify a unicode char into 3 classes, or raise [Unsupported] *) +(** Classify a unicode char into 3 classes or unknown. *) val classify : int -> status -(** Check whether a given string be used as a legal identifier. - - [None] means yes - - [Some (b,s)] means no, with explanation [s] and severity [b] *) +(** Return [None] if a given string can be used as a (Coq) identifier. + Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *) val ident_refutation : string -> (bool * string) option -(** First char of a string, converted to lowercase *) +(** First char of a string, converted to lowercase + @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string -(** For extraction, turn a unicode string into an ascii-only one *) +(** Return [true] if all UTF-8 characters in the input string are just plain + ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool + +(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII + characters. The non-ASCII characters are translated to ["_UUxxxx_"] where + {i xxxx} is the Unicode index of the character in hexadecimal (from four + to six hex digits). To avoid potential name clashes, any preexisting + substring ["_UU"] is turned into ["_UUU"]. *) val ascii_of_ident : string -> string + +(** Validate an UTF-8 string *) +val is_utf8 : string -> bool + +(** Return the length of a valid UTF-8 string. *) +val utf8_length : string -> int + +(** Variant of {!String.sub} for UTF-8 strings. *) +val utf8_sub : string -> int -> int -> string |