1.7. 문자, 문자열, 슬라이스🔗

Lean에서 문자열은 유니코드 텍스트를 담습니다. 구체적으로 말하면 문자열은 문자의 시퀀스이며, 각 문자는 유니코드 코드 포인트입니다. 문자열은 큰따옴표로 감싸서 쓰고, 개별 문자는 작은따옴표로 감싸서 씁니다. 문자열의 타입은 String이고 문자의 타입은 Char입니다.

문자열은 ++ 연산자로 이어 붙일 수 있습니다:

"Hello, world"#eval "Hello, " ++ "world"

"Hello, world"

String.push를 사용하면 문자열 끝에 문자를 추가할 수 있습니다:

"Hello!"#eval String.push "Hello" '!'

"Hello!"

이 함수는 구조체 접근자에 쓰이는 점 표기법으로도 호출할 수 있습니다.

"Hello!"#eval "Hello".push '!'

"Hello!"

1.7.1. 슬라이스🔗

문자열은 UTF-8 인코딩으로 표현되며, 바이트 배열과 캐시된 문자 개수가 함께 저장됩니다. 따라서 문자열에서 문자 하나만 제거하더라도 나머지 문자들이 새 문자열로 복사될 수 있습니다.

작은 조합 가능한 조각들로 문자열 처리 코드를 작성할 수 있도록, 많은 문자열 연산은 다른 문자열의 일부 영역인 문자열 슬라이스를 반환합니다. 문자열 슬라이스의 타입은 String.Slice입니다. 슬라이스는 문자열에 대한 참조와 함께 슬라이스의 시작 위치와 끝 위치를 담고 있으며, 여러 슬라이스가 같은 문자열을 공유할 수 있습니다. 문자열의 접두사를 제거하는 것과 같은 연산은 새 문자열을 할당하는 대신 슬라이스를 반환하며, 문자열 API의 상당 부분은 슬라이스에 대해서도 구현되어 있습니다.

슬라이스를 반환하는 연산으로는 문자열의 앞뒤에서 공백, 탭, 줄바꿈, 캐리지 리턴 문자를 제거한 슬라이스를 반환하는 String.trimAscii, 문자열의 시작이나 끝에서 지정한 개수의 문자를 제거하는 String.drop과 String.dropEnd, 그리고 문자열의 시작이나 끝에서 패턴과 일치하는 모든 문자를 각각 제거하는 String.dropWhile과 String.dropEndWhile이 있습니다. 문자열 검색에 사용하는 패턴은 패턴 매칭에 사용하는 패턴과 다릅니다. 문자열 API에서 패턴은 일치시킬 문자나 특정 부분 문자열을 지정하는 함수 인자입니다. 문자열 슬라이스 API에는 슬라이스를 생성하는 모든 문자열 함수도 포함되어 있으므로, 중간 문자열이 복사될 걱정 없이 문자열 조작을 여러 단계에 걸쳐 차례로 작성할 수 있습니다.

이 코드는 중간 문자열을 할당하지 않고 문자열의 앞과 뒤에서 문자를 제거합니다:

"tortoise"#eval (("small tortoiseshell".drop 6).dropEnd 5).copy

"tortoise"

함수 String.Slice.copy는 슬라이스가 가리키는 기반 문자열 영역의 복사본을 반환합니다. 처음 호출하는 String.drop은 슬라이스를 반환하고, String.Slice.dropEnd 호출은 조정된 슬라이스를 반환합니다. 마지막으로 copy를 호출하면 다시 문자열이 만들어집니다.

문자열과 달리 슬라이스는 문자 개수를 캐시하지 않습니다. 문자의 UTF-8 인코딩은 여러 바이트를 차지할 수 있으므로 문자열 슬라이스의 길이를 효율적으로 확인할 방법이 없습니다. 하지만 슬라이스가 비어 있는지는 String.Slice.isEmpty로 확인할 수 있습니다.

1.7.2. 매칭🔗

String.dropWhile나 String.dropEndWhile처럼 문자열의 일부와 매칭하는 함수는 오버로드되어 있습니다. 이러한 함수는 다양한 패턴으로 호출할 수 있으며, 각 패턴은 저마다의 방식으로 부분 문자열과 매칭합니다.

패턴으로 문자를 지정할 수도 있으며, 이 경우 해당 문자가 연속으로 이어진 부분이 제거됩니다:

red admira#eval "red admiral".dropEndWhile 'l'

red admira

출력이 따옴표로 감싸여 있지 않은 것은 문자열 슬라이스이기 때문이며, 문자열 슬라이스는 주변 따옴표 없이 표시됩니다. 패턴은 문자열일 수도 있으며, 이 경우 해당 문자열 전체가 연속으로 반복되는 부분이 제거됩니다:

butterfly#eval "the the butterfly".dropWhile "the "

butterfly

불완전한 매치는 제거되지 않습니다:

grayling#eval ("a gray grayling".drop 2).dropWhile "gray "

grayling

패턴은 true 또는 false를 반환하는 함수일 수도 있습니다. 함수가 false를 반환할 때까지 문자가 제거됩니다. 뒤쪽 공백이 남아 있음을 보이기 위해 슬라이스를 문자열로 변환합니다:

"red "#eval ("red admiral".dropEndWhile Char.isAlpha).copy

"red "

1.7.3. 마주칠 수 있는 메시지🔗

오버로드된 문자열 매칭 함수는 이 책의 뒷부분에서 설명하는 기능, 즉 타입 클래스와 의존 타입을 사용하여 구현됩니다. 특히 Lean의 이러한 기능을 배우기 전에 미리 읽는 법을 익혀 두면 유용한 오류 메시지가 두 가지 있습니다.

패턴 없이 함수를 호출하면 오류가 발생합니다:

#eval don't know how to synthesize implicit argument `ρ`
  @String.dropEndWhile ?m.2 "red admiral"
context:
⊢ Type"red admiral".dropEndWhile

don't know how to synthesize implicit argument `ρ`
  @String.dropEndWhile ?m.2 "red admiral"
context:
⊢ Type

이 오류는 패턴이 주어지지 않았기 때문에 Lean이 어떤 패턴 타입을 사용해야 할지 결정할 수 없다는 뜻입니다. 패턴을 제공하면 이 오류를 해결할 수 있습니다.

유효한 패턴이 아닌 인자로 이 함수들을 호출하면 컴파일 타임 오류가 발생합니다:

#eval failed to synthesize instance of type class
  String.Slice.Pattern.BackwardPattern [12]

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command."12345abcde".dropEndWhile [12]

failed to synthesize instance of type class
  String.Slice.Pattern.BackwardPattern [12]

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

이 오류 메시지는 String.dropEndWhile이 패턴 [12]에 대해 오버로드되어 있지 않다는 뜻입니다. 함수, 문자, 문자열과 같은 의미 있는 패턴을 제공하면 이 오류를 해결할 수 있습니다.