2.4. Worked Example: `cat`🔗

표준 Unix 유틸리티 cat은 여러 명령줄 옵션 뒤에 0개 이상의 입력 파일을 받는다. 파일이 없거나 파일 중 하나가 대시(-)이면 파일을 읽는 대신 표준 입력을 해당 입력으로 사용한다. 입력 내용은 차례로 표준 출력에 쓴다. 지정한 입력 파일이 없으면 표준 오류에 알리지만 cat은 나머지 입력을 계속 결합한다. 입력 파일 중 하나라도 존재하지 않으면 0이 아닌 종료 코드가 반환된다.

이 절에서는 cat의 단순화된 버전인 feline을 설명한다. 널리 쓰이는 cat과 달리 feline에는 줄 번호 표시, 출력 불가능한 문자 표시, 도움말 출력 같은 기능을 위한 명령줄 옵션이 없다. 또한 터미널 장치에 연결된 표준 입력을 두 번 이상 읽을 수 없다.

이 절에서 최대한 많은 것을 배우려면 직접 따라 하라. 코드 예제를 복사해 붙여 넣어도 되지만 손으로 입력하는 편이 더 좋다. 그러면 코드를 입력하고 실수를 복구하며 컴파일러의 피드백을 해석하는 기계적 과정을 배우기 쉽다.

2.4.1. Getting Started🔗

feline 구현의 첫 단계는 패키지를 만들고 코드를 구성할 방법을 정하는 것이다. 이 프로그램은 매우 단순하므로 모든 코드를 Main.lean에 둔다. 먼저 lake new feline을 실행하라. Lakefile을 편집해 라이브러리를 제거하고 생성된 라이브러리 코드와 Main.lean의 해당 참조를 삭제하라. 그러면 lakefile.toml은 다음을 포함해야 한다.

                File: lakefile.tomlname = "feline"version = "0.1.0"defaultTargets = ["feline"][[lean_exe]]name = "feline"root = "Main"

그리고 Main.lean에는 다음과 같은 내용이 있어야 한다.

File: Main.leandef main : IO Unit := IO.println s!"Hello, cats!"

또는 lake new feline exe를 실행하면 lake가 라이브러리 절이 없는 템플릿을 사용하므로 파일을 편집할 필요가 없다.

lake build를 실행해 코드를 빌드할 수 있는지 확인하라.

2.4.2. Concatenating Streams🔗

프로그램의 기본 뼈대를 빌드했으므로 이제 실제 코드를 입력할 차례다. cat의 제대로 된 구현은 /dev/random 같은 무한 IO 스트림에도 사용할 수 있어야 하므로 출력하기 전에 입력을 메모리에 모두 읽을 수 없다. 또한 한 번에 한 문자씩 처리하면 성능이 답답할 정도로 느려지므로 그렇게 해서는 안 된다. 대신 연속된 데이터 블록을 한꺼번에 읽고 한 블록씩 표준 출력으로 보내는 편이 낫다.

첫 단계는 읽을 블록의 크기를 정하는 것이다. 단순성을 위해 이 구현에서는 보수적으로 20킬로바이트 블록을 사용한다. USize는 C의 size_t와 비슷하며 모든 유효한 배열 크기를 나타낼 만큼 큰 부호 없는 정수 타입이다.

def bufsize : USize := 20 * 1024

2.4.2.1. Streams🔗

feline의 주된 작업은 dump가 수행한다. 입력을 한 블록씩 읽어 표준 출력에 내보내며 입력 끝에 도달할 때까지 계속한다. 입력 끝은 read가 빈 바이트 배열을 반환하는 것으로 나타난다.

partial def dump (stream : IO.FS.Stream) : IO Unit := do
  let buf ← stream.read bufsize
  if buf.isEmpty then
    pure ()
  else
    let stdout ← IO.getStdout
    stdout.write buf
    dump stream

dump 함수는 인수보다 즉시 작아지지 않는 입력에 대해 자신을 재귀적으로 호출하므로 partial로 선언한다. 함수를 partial로 선언하면 Lean은 함수가 종료한다는 증명을 요구하지 않는다. 반면 Lean의 논리에서 무한 루프를 허용하면 건전하지 않은(unsound) 논리가 되므로 partial 함수는 정확성 증명에도 훨씬 덜 적합하다. 그러나 무한 입력(/dev/random 등)은 실제로 종료하지 않으므로 dump가 종료한다는 것을 증명할 방법은 없다. 이런 경우에는 함수를 partial로 선언하는 것 외에 다른 방법이 없다.

IO.FS.Stream 타입은 POSIX 스트림을 나타낸다. 이면에서는 POSIX 스트림 연산마다 필드 하나를 가진 구조체로 표현한다. 각 연산은 해당 연산을 제공하는 IO 동작으로 나타낸다.

structure Stream where
  flush   : IO Unit
  read    : USize → IO ByteArray
  write   : ByteArray → IO Unit
  getLine : IO String
  putStr  : String → IO Unit
  isTty   : BaseIO Bool

BaseIO 타입은 런타임 오류를 배제하는 IO의 변형이다. Lean 컴파일러에는 표준 입력·출력·오류를 나타내는 스트림을 얻는 IO 동작이 있다(예: dump에서 호출하는 IO.getStdout). 이것들이 일반 정의가 아닌 IO 동작인 이유는 Lean이 프로세스에서 표준 POSIX 스트림을 교체할 수 있게 하기 때문이다. 따라서 사용자 정의 IO.FS.Stream을 작성해 프로그램 출력을 문자열로 캡처하기가 쉽다.

dump의 제어 흐름은 본질적으로 while 루프다. dump를 호출했을 때 스트림이 파일 끝에 도달했다면 pure ()가 Unit 생성자를 반환해 함수를 종료한다. 파일 끝에 아직 도달하지 않았다면 한 블록을 읽고 그 내용을 stdout에 쓴 뒤 dump가 자신을 직접 호출한다. stream.read가 파일 끝을 나타내는 빈 바이트 배열을 반환할 때까지 재귀 호출을 계속한다.

dump처럼 do의 문장으로 if 표현식이 나오면 if의 각 분기에 do가 암묵적으로 주어진다. 즉 else 뒤의 단계 시퀀스는 맨 앞에 do가 있는 것처럼 실행할 IO 동작의 시퀀스로 취급한다. if 분기에서 let으로 도입한 이름은 해당 분기에서만 보이고 if 밖에서는 범위에 들어오지 않는다.

재귀 호출이 함수의 마지막 단계이고 결과를 조작하거나 계산하지 않고 직접 반환하므로 dump를 호출해도 스택 공간이 고갈되지 않는다. 이 재귀를 꼬리 재귀라고 하며 이 책의 뒤 절에서 자세히 설명한다. 컴파일된 코드가 상태를 보존할 필요가 없으므로 Lean 컴파일러는 재귀 호출을 점프로 컴파일할 수 있다.

feline이 표준 입력을 표준 출력으로 보내기만 한다면 dump로 충분하다. 하지만 명령줄 인수로 주어진 파일을 열고 내용을 출력할 수도 있어야 한다. 인수가 존재하는 파일 이름이면 fileStream은 파일 내용을 읽는 스트림을 반환한다. 인수가 파일이 아니면 fileStream은 오류를 출력하고 none을 반환한다.

def fileStream (filename : System.FilePath) : IO (Option IO.FS.Stream) := do
  let fileExists ← filename.pathExists
  if not fileExists then
    let stderr ← IO.getStderr
    stderr.putStrLn s!"File not found: {filename}"
    pure none
  else
    let handle ← IO.FS.Handle.mk filename IO.FS.Mode.read
    pure (some (IO.FS.Stream.ofHandle handle))

파일을 스트림으로 여는 데는 두 단계가 필요하다. 먼저 파일을 읽기 모드로 열어 파일 핸들을 만든다. Lean 파일 핸들은 기반 파일 디스크립터를 추적한다. 파일 핸들 값에 대한 참조가 없으면 종료자가 파일 디스크립터를 닫는다. 둘째, IO.FS.Stream.ofHandle을 사용해 파일 핸들에 작동하는 대응 IO 동작으로 Stream 구조체의 각 필드를 채워 파일 핸들에 POSIX 스트림과 같은 인터페이스를 준다.

2.4.2.2. Handling Input🔗

feline의 주 루프는 process라는 또 다른 꼬리 재귀 함수다. 입력 중 하나라도 읽지 못하면 0이 아닌 종료 코드를 반환하도록 process는 프로그램 전체의 현재 종료 코드를 나타내는 exitCode 인수를 받는다. 처리할 입력 파일 리스트도 받는다.

def process (exitCode : UInt32) (args : List String) : IO UInt32 := do
  match args with
  | [] => pure exitCode
  | "-" :: args =>
    let stdin ← IO.getStdin
    dump stdin
    process exitCode args
  | filename :: args =>
    let stream ← fileStream ⟨filename⟩
    match stream with
    | none =>
      process 1 args
    | some stream =>
      dump stream
      process exitCode args

if와 마찬가지로 do의 문장으로 사용한 match의 각 분기에도 자체 do가 암묵적으로 주어진다.

가능성은 세 가지다. 처리할 파일이 더 없으면 process는 오류 코드를 그대로 반환한다. 지정한 파일 이름이 "-"이면 process가 표준 입력 내용을 출력한 뒤 남은 파일 이름을 처리한다. 마지막 가능성은 실제 파일 이름이 지정된 경우다. 이때 fileStream으로 파일을 POSIX 스트림으로 열려고 한다. FilePath가 문자열 하나를 담은 단일 필드 구조체이므로 인수를 ⟨ ... ⟩로 감싼다. 파일을 열 수 없으면 건너뛰고 process의 재귀 호출이 종료 코드를 1로 설정한다. 열 수 있으면 내용을 출력하고 process의 재귀 호출은 종료 코드를 그대로 둔다.

process는 구조적으로 재귀적이므로 partial로 표시할 필요가 없다. 각 재귀 호출에는 입력 리스트의 꼬리가 주어지고 Lean의 모든 리스트는 유한하다. 따라서 process는 비종료를 도입하지 않는다.

2.4.2.3. Main🔗

마지막 단계는 main 동작을 작성하는 것이다. 앞의 예제와 달리 feline의 main은 함수다. Lean에서 main은 세 타입 중 하나를 가질 수 있다.

main : IO Unit은 명령줄 인수를 읽을 수 없고 항상 종료 코드 0으로 성공을 나타내는 프로그램에 해당한다.
main : IO UInt32은 인수 없이 종료 코드를 반환하는 프로그램의 C 언어 int main(void)에 해당한다.
main : List String → IO UInt32은 인수를 받고 성공이나 실패를 알리는 프로그램의 C 언어 int main(int argc, char **argv)에 해당한다.

인수가 없으면 feline은 단일 "-" 인수로 호출한 것처럼 표준 입력을 읽어야 한다. 그렇지 않으면 인수를 차례로 처리해야 한다.

def main (args : List String) : IO UInt32 :=
  match args with
  | [] => process 0 ["-"]
  | _ =>  process 0 args

2.4.3. Meow!🔗

feline이 작동하는지 확인하려면 먼저 lake build로 빌드하라. 먼저 인수 없이 호출했을 때 표준 입력에서 받은 내용을 출력해야 한다. 다음을 확인하라.

$ echo "It works!" | lake exe feline

다음 It works!이 출력된다.

둘째, 파일을 인수로 호출하면 파일을 출력해야 한다. test1.txt 파일에 다음이 들어 있다면

File: test1.txtIt's time to find a warm spot

그리고 test2.txt에는 다음이 들어 있다.

File: test2.txtand curl up!

그러면 다음 명령은

$ lake exe feline test1.txt test2.txt

다음을 출력해야 한다.

It's time to find a warm spot
and curl up!

마지막으로 - 인수를 적절히 처리해야 한다.

$ echo "and purr" | lake exe feline test1.txt - test2.txt

다음 결과를 내야 한다.

It's time to find a warm spot
and purr
and curl up!

2.4.4. Exercise🔗

feline을 사용법 정보도 지원하도록 확장하라. 확장 버전은 명령줄 인수 --help를 받으면 사용 가능한 명령줄 옵션에 대한 문서를 표준 출력에 써야 한다.

2.4. Worked Example: cat🔗