2.4. 실습 예제: `cat`🔗

표준 유닉스 유틸리티인 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은 그 함수가 종료한다는 증명을 요구하지 않습니다. 반면, 부분 함수는 정확성 증명에도 훨씬 적합하지 않은데, 이는 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)을 포함하고 있습니다. Lean은 프로세스 내에서 이러한 표준 POSIX 스트림을 교체할 수 있도록 허용하는데, 이는 사용자 정의 IO.FS.Stream을 작성하여 프로그램의 출력을 문자열로 캡처하는 것과 같은 작업을 더 쉽게 만들어 주기 때문에, 이것들은 일반적인 정의가 아니라 IO 액션입니다.

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

if 표현식이 dump에서와 같이 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🔗

마지막 단계는 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🔗