2.4. 실습 예제: `cat`🔗

표준 Unix 유틸리티인 cat은 여러 명령줄 옵션을 받고, 그 뒤에 0개 이상의 입력 파일을 받습니다. 파일이 하나도 주어지지 않았거나 그중 하나가 대시(-)이면, 파일을 읽는 대신 표준 입력을 해당 입력으로 사용합니다. 입력의 내용은 차례대로 하나씩 표준 출력에 쓰입니다. 지정된 입력 파일이 존재하지 않으면 이 사실을 표준 오류에 기록하지만, cat은 나머지 입력을 계속 이어 붙입니다. 입력 파일 중 하나라도 존재하지 않으면 0이 아닌 종료 코드를 반환합니다.

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

이 절을 최대한 활용하려면 직접 따라 해 보십시오. 코드 예제를 복사해 붙여 넣어도 괜찮지만, 손으로 직접 타입해 입력하는 편이 훨씬 좋습니다. 그렇게 하면 코드를 입력하고, 실수를 바로잡고, 컴파일러의 피드백을 해석하는 기계적인 과정을 더 쉽게 익힐 수 있습니다.

2.4.1. 시작하기🔗

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. 스트림 이어붙이기🔗

이제 프로그램의 기본 골격이 갖추어졌으니, 실제로 코드를 작성할 차례입니다. cat을 제대로 구현하면 /dev/random과 같은 무한 IO 스트림에도 사용할 수 있습니다. 이는 출력하기 전에 입력을 메모리로 모두 읽어 들일 수 없다는 뜻입니다. 또한 한 번에 한 문자씩 처리해서도 안 됩니다. 그렇게 하면 성능이 답답할 만큼 느려지기 때문입니다. 그 대신 연속된 데이터 블록을 한꺼번에 읽어 들이고, 그 데이터를 한 번에 한 블록씩 표준 출력으로 보내는 편이 낫습니다.

첫 번째 단계는 한 번에 얼마나 큰 블록을 읽을지 정하는 것입니다. 단순하게 하기 위해 이 구현에서는 20킬로바이트라는 보수적인 크기의 블록을 사용합니다. USize는 C의 size_t에 해당하며, 유효한 배열 크기를 모두 나타낼 수 있을 만큼 큰 부호 없는 정수 타입입니다.

def bufsize : USize := 20 * 1024

2.4.2.1. 스트림🔗

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은 그 함수가 종료한다는 증명을 요구하지 않습니다. 반면에 partial 함수는 정확성을 증명하기도 훨씬 어렵습니다. Lean의 논리에서 무한 루프를 허용하면 그 논리가 건전하지 않게 되기 때문입니다. 그러나 dump가 종료한다는 것을 증명할 방법은 없습니다. (/dev/random에서 오는 입력과 같은) 무한한 입력이 주어지면 실제로 종료하지 않기 때문입니다. 이와 같은 경우에는 함수를 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에서처럼 if 표현식이 do 안에서 문장으로 쓰이면, 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을 사용하여 파일 핸들에 POSIX 스트림과 동일한 인터페이스를 부여합니다. 이 함수는 Stream 구조체의 각 필드를 파일 핸들에 대해 동작하는 해당 IO 액션으로 채웁니다.

2.4.2.2. 입력 처리🔗

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 액션을 작성하는 것입니다. 이전 예제들과 달리, 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. 야옹!🔗

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. 연습 문제🔗

feline에 사용법 정보를 표시하는 기능을 추가하십시오. 확장된 버전은 사용 가능한 명령줄 옵션에 대한 설명을 표준 출력에 출력하도록 하는 명령줄 인자 --help를 받을 수 있어야 합니다.

2.4. 실습 예제: cat🔗