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 타입을 가집니다. 슬라이스(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]에 대해 오버로드되지 않았음을 의미합니다. 함수, 문자, 문자열과 같은 의미 있는 패턴을 제공하여 이를 수정할 수 있습니다.