1.7. Characters, Strings, and Slices🔗

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. Slices🔗

문자열은 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. Matching🔗

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. Messages You May Meet🔗

오버로드된 문자열 매칭 함수는 책 뒤에서 설명할 타입 클래스와 종속 타입 기능으로 구현한다. 이러한 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] 패턴에 대해 오버로드되지 않았다는 뜻이다. 함수·문자·문자열처럼 의미 있는 패턴을 제공하면 고칠 수 있다.