ATS の文字列はC言語と同じ方法で表現されています。 それは NULL 文字で終端される非 NULL 文字群が隣接して保存された列で、その長さはその列の中の非 NULL 文字の数です。 慣習的に、このような文字列をしばしばC言語スタイル文字列と呼びます。 また安全に処理することが困難であるために悪評が高いことでも知られています (この文字列の誤用に起因する多くのバグと欠陥が明確に物語っています)。 実際のところ、私の知るかぎり ATS はC言語スタイルの文字列に対する安全な処理を完全にサポートするはじめての実用的なプログラミング言語です。 ATS では、 string は種 (int) -> type の型コンストラクタです。 静的な整数 n が与えられた時、 string(n) は長さ n の文字列の型です。 string は長さが指定されていない文字列の非依存型をも参照していることに注意してください。 この非依存型は次に定義する型 String と基本的に同等です:
次の2つの関数は与えられた文字列を走査する用途に一般に使われます:// fun string_is_atend {n:int}{i:nat | i <= n} (str: string (n), i: size_t (i)): bool (i==n) // end of [string_is_atend] // fun string_isnot_atend {n:int}{i:nat | i <= n} (str: string (n), i: size_t (i)): bool (i < n) // end of [string_isnot_atend] //
fun string_length {n:nat} ( str: string (n) ) : size_t (n) = let fun loop {i:nat | i <= n} .<n-i>. (str: string n, i: size_t i): size_t (n) = if string_isnot_atend (str, i) then loop (str, succ(i)) else i // end of [loop] in loop (str, i2sz(0)) end // end of [string_length]
次の2つの関数は文字列に保存されている文字へのアクセスと変更を表わします:
// typedef charNZ = [c:int | c != 0] char(c) // fun string_get_at {n:int}{i:nat | i < n}(str: string n, i: size_t i): charNZ overload [] with string_get_at // fun string_set_char_at {n:int}{i:nat | i < n}(str: string n, i: size_t i, c: charNZ): void overload [] with string_set_char_at //
// typedef sizeLt (n:int) = [i:nat | i < n] size_t (i) // fun string_find{n:nat} ( str: string n, c0: char ) : Option (sizeLt n) = let typedef res = sizeLt (n) fun loop{i:nat | i <= n} ( str: string n, c0: char, i: size_t i ) : Option (res) = ( if string_isnot_atend (str, i) then if (c0 = str[i]) then Some{res}(i) else loop (str, c0, succ(i)) else None () // end of [if] ) (* end of [loop] *) in loop (str, c0, i2sz(0)) end // end of [string_find] //
string_find の実装にはいくらか非効率な部分があります: 最初に string_isnot_atend 呼び出して、与えられた位置 i は 文字列 str の長さより短かいかどうか検査されます。 そしてもし短かければ string_get_at を呼び出して、 文字列の当該位置に保存されている文字を取り出します。 これら2つの関数呼び出しを次の実装のように1つにまとめましょう:
// // This implementation does the same as [string_find] // but should be more efficient. // fun string_find2{n:nat} ( str: string n, c0: char ) : Option (sizeLt n) = let // fun loop{i:nat | i <= n} ( str: string n , c0: char, i: size_t i ) : Option (sizeLt n) = let typedef res = sizeLt (n) val c = string_test_at (str, i) in if c != '\000' then ( if (c0 = c) then Some{res}(i) else loop(str, c0, succ(i)) // end of [if] ) else None((*void*)) // end of [if] end // end of [loop] // in loop (str, c0, i2sz(0)) end // end of [string_find2]
fun string_test_at {n:int}{i:nat | i <= n} ( str: string (n), i: size_t (i) ) : [c:char | (c != NUL && i < n) || (c == NUL && i >= n)] char c // end of [string_test_at]
文字列を安全に効率的に取り扱うことは、プログラミング言語のデザインにおいて厄介事の一つです。 またプログラミング言語に関する大量の情報が、文字列の取り扱いに関することであることもしばしばです。 ATS では、線形型を使ってC言語スタイル文字列を適切に処理することができます。 このトピックはこの本の別の章で紹介します。