9.5. ファイル・ファイルハンドラ・ストリーム（Files, File Handles, and Streams）

Lean はサポート対象のすべてのプラットフォームに対して一貫したファイルシステム API を提供します。以下がカギとなるコンセプトです：

ファイル （file）

ファイルとはオペレーティングシステムが提供する抽象化で、ディレクトリとして階層的に編成された永続的に保存されるデータへのランダムアクセスを提供します。

ディレクトリ （directory）

ディレクトリは フォルダ （folder）としても知られ、ファイルや他のディレクトリを含むことができます。基本的に、ディレクトリはその中に含まれるファイルやディレクトリに名前をマッピングします。

ファイルハンドラ （file handler）

ファイルハンドラ（ Handle ）は読み書きのどちらか、もしくは両方のためにオープンされたファイルへの抽象的な参照です。ファイルハンドラはファイルの特定の場所を指すカーソルと共に、読み書きのどちらか、もしくは両方が許可されているかどうかを決定するモードを保持します。ファイルハンドラからの読み込みやファイルハンドラへの書き込みによってカーソルが進められます。ファイルハンドラは バッファ される可能性があります。これはファイルハンドラからの読み込みが永続データの現在の内容を返さない可能性およびファイルハンドラへの書き込みが直ちに反映されない可能性があることを意味します。

パス

ファイルは主に パス （path、 System.FilePath ）を介してアクセスされます。パスはディレクトリ名の列で、ファイル名で終わる可能性があります。パスは名前を区切り文字 現在のプラットフォームでの区切り文字は System.FilePath.pathSeparators にリストされています。 で区切られた文字列として表現されます。

パスの詳細はプラットフォームに固有です。 絶対パス （absolute path）は ルートディレクトリ （root directory）から始まります；いくつかのオペレーティングシステムでは単一のルートを持ちますが、それ以外では複数のルートディレクトリを持つ可能性があります。相対パスはルートディレクトリから始まらず、他のディレクトリを始点とする必要があります。ディレクトリに加えて、パスは特別なディレクトリ名 . を含むことができます。これは見つかったディレクトリを指します。また .. はパス内の前のディレクトリを指します。

ファイル名、またパスはファイルの種類を識別する1つ以上の 拡張子 （extension）で終わることがあります。拡張子は System.FilePath.extSeparator 文字で区切られます。一部のプラットフォームでは、実行ファイルは特別な拡張子（ System.FilePath.exeExtension ）を持ちます。

ストリーム （stream）

ストリームはファイルをより高度に抽象化したもので、追加機能を提供しつつファイルの詳細を隠します。 ファイルハンドラ は基本的にオペレーティングシステムの表現の薄いラッパーですが、ストリームは Lean では IO.FS.Stream という構造体として実装されています。ストリームは Lean 上で実装されているため、ユーザコードは追加のストリームを作成することができ、標準ライブラリで提供されるストリームとシームレスに併用することができます。

9.5.1. 低レベルのファイル API（Low-Level File API）

最も低いレベルでは、ファイルは Handle.mk を使って明示的にオープンされます。ハンドラオブジェクトへの最後の参照が削除されると、ファイルはクローズされます。ファイルハンドラを閉じる明示的な方法は、そのハンドラへの参照がないことを確認する以外に存在しません。

🔗opaque
IO.FS.Handle : Type
🔗opaque
IO.FS.Handle.mk (fn : System.FilePath)
    (mode : IO.FS.Mode) : IO IO.FS.Handle
🔗inductive type
IO.FS.Mode : Type

The mode of a file handle (i.e., a set of open flags and an fdopen mode).

All modes do not translate line endings (i.e., O_BINARY on Windows) and are not inherited across process creation (i.e., O_NOINHERIT on Windows, O_CLOEXEC elsewhere).

References:

Constructors

read : IO.FS.Mode

File opened for reading. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.

  • open flags: O_RDONLY

  • fdopen mode: r

write : IO.FS.Mode

File opened for writing. On open, truncate an existing file to zero length or create a new file. The stream is positioned at the beginning of the file.

  • open flags: O_WRONLY | O_CREAT | O_TRUNC

  • fdopen mode: w

writeNew : IO.FS.Mode

New file opened for writing. On open, create a new file with the stream positioned at the start. Errors if the file already exists.

  • open flags: O_WRONLY | O_CREAT | O_TRUNC | O_EXCL

  • fdopen mode: w

readWrite : IO.FS.Mode

File opened for reading and writing. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.

  • open flags: O_RDWR

  • fdopen mode: r+

append : IO.FS.Mode

File opened for writing. On open, create a new file if it does not exist. The stream is positioned at the end of the file.

  • open flags: O_WRONLY | O_CREAT | O_APPEND

  • fdopen mode: a

🔗opaque
IO.FS.Handle.read (h : IO.FS.Handle)
    (bytes : USize) : IO ByteArray

Read up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

🔗def
IO.FS.Handle.readToEnd (h : IO.FS.Handle)
    : IO String
🔗def
IO.FS.Handle.readBinToEnd (h : IO.FS.Handle)
    : IO ByteArray
🔗def
IO.FS.Handle.readBinToEndInto (h : IO.FS.Handle)
    (buf : ByteArray) : IO ByteArray
🔗opaque
IO.FS.Handle.getLine (h : IO.FS.Handle)
    : IO String

Read text up to (including) the next line break from the handle. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

🔗opaque
IO.FS.Handle.write (h : IO.FS.Handle)
    (buffer : ByteArray) : IO Unit
🔗opaque
IO.FS.Handle.putStr (h : IO.FS.Handle)
    (s : String) : IO Unit
🔗def
IO.FS.Handle.putStrLn (h : IO.FS.Handle)
    (s : String) : IO Unit
🔗opaque
IO.FS.Handle.flush (h : IO.FS.Handle) : IO Unit
🔗opaque
IO.FS.Handle.rewind (h : IO.FS.Handle) : IO Unit

Rewinds the read/write cursor to the beginning of the handle.

🔗opaque
IO.FS.Handle.truncate (h : IO.FS.Handle)
    : IO Unit

Truncates the handle to the read/write cursor.

Does not automatically flush. Usually this is fine because the read/write cursor includes buffered writes. However, the combination of buffered writes, then rewind, then truncate, then close may lead to a file with content. If unsure, flush before truncating.

🔗opaque
IO.FS.Handle.isTty (h : IO.FS.Handle)
    : BaseIO Bool

Returns true if a handle refers to a Windows console or Unix terminal.

🔗opaque
IO.FS.Handle.lock (h : IO.FS.Handle)
  (exclusive : Bool := true) : IO Unit

Acquires an exclusive or shared lock on the handle. Will block to wait for the lock if necessary.

NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

🔗opaque
IO.FS.Handle.tryLock (h : IO.FS.Handle)
  (exclusive : Bool := true) : IO Bool

Tries to acquire an exclusive or shared lock on the handle. Will NOT block for the lock, but instead return false.

NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

🔗opaque
IO.FS.Handle.unlock (h : IO.FS.Handle) : IO Unit

Releases any previously acquired lock on the handle. Will succeed even if no lock has been acquired.

1つのファイルと複数のハンドラ

このプログラムには同じファイルに対する2つのハンドラがあります。ファイル I/O はハンドラごとに独立してバッファされることがあるため、バッファをファイルの実際の内容と同期させる必要がある場合は Handle.flush を呼び出す必要があります。ここでは2つのハンドラは一方のハンドラが他方のハンドラより1バイト先になるようにファイル内をロックステップで進みます。最初のハンドラは 'A' の出現回数を数えるために使われ、2番目のハンドラは 'A' を '!' に置き換えるために使われます。2番目のハンドラは write モードではなく readWrite モードで開かれています。これは write モードで既存のファイルを開くと空のファイルに置き換わるからです。今回の場合、バッファは実行中にフラッシュされる必要はありません。なぜなら変更はファイルの再読み込みされない部分に対してのみ行われるものの、書き出しハンドラはループが完了したらフラッシュしなければならないからです。

open IO.FS (Handle) def main : IO Unit := do IO.println s!"Starting contents: '{(← IO.FS.readFile "data").trim}'" let h ← Handle.mk "data" .read let h' ← Handle.mk "data" .readWrite h'.rewind let mut count := 0 let mut buf : ByteArray ← h.read 1 while ok : buf.size = 1 do if Char.ofUInt8 buf[0] == 'A' then count := count + 1 h'.write (ByteArray.empty.push '!'.toUInt8) else h'.write buf buf ← h.read 1 h'.flush IO.println s!"Count: {count}" IO.println s!"Contents: '{(← IO.FS.readFile "data").trim}'"

このファイルに対して実行すると：

Input: dataAABAABCDAB

プログラムは以下を出力します：

stdoutStarting contents: 'AABAABCDAB'Count: 5Contents: '!!B!!BCD!B'

その後、ファイル内容は以下のようになります：

Output: data!!B!!BCD!B

9.5.2. ストリーム（Streams）

🔗structure
IO.FS.Stream : Type

A pure-Lean abstraction of POSIX streams. We use Streams for the standard streams stdin/stdout/stderr so we can capture output of #eval commands into memory.

Constructor

IO.FS.Stream.mk

Fields

flush : IO Unit
read : USize → IO ByteArray

Read up to the given number of bytes from the stream. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.

write : ByteArray → IO Unit
getLine : IO String

Read text up to (including) the next line break from the stream. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.

putStr : String → IO Unit
isTty : BaseIO Bool

Returns true if a stream refers to a Windows console or Unix terminal.

🔗def
IO.FS.withIsolatedStreams.{u_1}
  {m : Type → Type u_1} {α : Type} [Monad m]
  [MonadFinally m] [MonadLiftT BaseIO m]
  (x : m α) (isolateStderr : Bool := true) :
  m (String × α)

Run action with stdin emptied and stdout+stderr captured into a String.

🔗def
IO.FS.Stream.ofBuffer
    (r : IO.Ref IO.FS.Stream.Buffer)
    : IO.FS.Stream
🔗def
IO.FS.Stream.ofHandle (h : IO.FS.Handle)
    : IO.FS.Stream
🔗def
IO.FS.Stream.putStrLn (strm : IO.FS.Stream)
    (s : String) : IO Unit
🔗structure
IO.FS.Stream.Buffer : Type

Constructor

IO.FS.Stream.Buffer.mk

Fields

data : ByteArray
pos : Nat
🔗def
IO.FS.Stream.Buffer.data
    (self : IO.FS.Stream.Buffer) : ByteArray
🔗def
IO.FS.Stream.Buffer.pos
    (self : IO.FS.Stream.Buffer) : Nat

9.5.3. パス（Paths）

パスは文字列として表現されます。ディレクトリの区切り文字としてスラッシュ（/）を使う場合もあれば、バックスラッシュ（\）を使う場合もあります。大文字小文字を区別する場合もあれば区別しない場合もあります。ファイル名を表現するために異なる Unicode エンコーディングや正規形が使われるかもしれず、プラットフォームによってはファイル名を文字列ではなくバイト列とみなすものもあります。あるシステムでは 絶対パス を表す文字列が別のシステムでは有効なパスではないこともあります。

複数のシステムで可能な限り互換性のある Lean コードを書くには、生の文字列操作の代わりに Lean のパス操作プリミティブを使用すると便利です。 System.FilePath.join のような補助関数は絶対パスのプラットフォーム固有の規則を考慮し、 System.FilePath.pathSeparator は現在のプラットフォームに適切なパス区切り文字を保持し、 System.FilePath.exeExtension は実行ファイルに必要な拡張子を保持します。これらの規則をハードコードすることは避けてください。

FilePath の Div 型クラスのインスタンスがあり、スラッシュ演算子を使ってパスを連結することができます。

🔗structure
System.FilePath : Type

Constructor

System.FilePath.mk

Fields

toString : String
🔗def
System.mkFilePath (parts : List String)
    : System.FilePath
🔗def
System.FilePath.join (p sub : System.FilePath)
    : System.FilePath
🔗def
System.FilePath.normalize (p : System.FilePath)
    : System.FilePath
🔗def
System.FilePath.isAbsolute (p : System.FilePath)
    : Bool
🔗def
System.FilePath.isRelative (p : System.FilePath)
    : Bool
🔗def
System.FilePath.parent (p : System.FilePath)
    : Option System.FilePath
🔗def
System.FilePath.components (p : System.FilePath)
    : List String
🔗def
System.FilePath.fileName (p : System.FilePath)
    : Option String
🔗def
System.FilePath.fileStem (p : System.FilePath)
    : Option String

Extracts the stem (non-extension) part of p.fileName.

🔗def
System.FilePath.extension (p : System.FilePath)
    : Option String
🔗def
System.FilePath.addExtension
    (p : System.FilePath) (ext : String)
    : System.FilePath

Appends the extension ext to a path p.

ext should not contain a leading ., as this function adds one. If ext is the empty string, no . is added.

Unlike System.FilePath.withExtension, this does not remove any existing extension.

🔗def
System.FilePath.withExtension
    (p : System.FilePath) (ext : String)
    : System.FilePath

Replace the current extension in a path p with ext.

ext should not contain a ., as this function adds one. If ext is the empty string, no . is added.

🔗def
System.FilePath.withFileName
    (p : System.FilePath) (fname : String)
    : System.FilePath
🔗def
System.FilePath.pathSeparator : Char

The character that separates directories. In the case where more than one character is possible, pathSeparator is the 'ideal' one.

🔗def
System.FilePath.pathSeparators : List Char

The list of all possible separators.

🔗def
System.FilePath.extSeparator : Char

File extension character

🔗def
System.FilePath.exeExtension : String

9.5.4. ファイルシステムの対話（Interacting with the Filesystem）

パスに対するいくつかの操作はファイルシステムを参照します。

🔗structure
IO.FS.Metadata : Type

Constructor

IO.FS.Metadata.mk

Fields

accessed : IO.FS.SystemTime
modified : IO.FS.SystemTime
byteSize : UInt64
type : IO.FS.FileType
🔗opaque
System.FilePath.metadata
    : System.FilePath → IO IO.FS.Metadata
🔗def
System.FilePath.pathExists (p : System.FilePath)
    : BaseIO Bool
🔗def
System.FilePath.isDir (p : System.FilePath)
    : BaseIO Bool
🔗structure
IO.FS.DirEntry : Type

Constructor

IO.FS.DirEntry.mk

Fields

root : System.FilePath
fileName : String
🔗def
IO.FS.DirEntry.path (entry : IO.FS.DirEntry)
    : System.FilePath
🔗opaque
System.FilePath.readDir
    : System.FilePath →
      IO (Array IO.FS.DirEntry)
🔗def
System.FilePath.walkDir (p : System.FilePath)
  (enter : System.FilePath → IO Bool := fun x =>
    pure true) :
  IO (Array System.FilePath)

Return all filesystem entries of a preorder traversal of all directories satisfying enter, starting at p. Symbolic links are visited as well by default.

🔗structure
IO.FileRight : Type

Constructor

IO.FileRight.mk

Fields

user : IO.AccessRight
group : IO.AccessRight
other : IO.AccessRight
🔗def
IO.FileRight.flags (acc : IO.FileRight) : UInt32
🔗def
IO.setAccessRights (filename : System.FilePath)
    (mode : IO.FileRight) : IO Unit
🔗opaque
IO.FS.removeFile (fname : System.FilePath)
    : IO Unit
🔗opaque
IO.FS.rename (old new : System.FilePath)
    : IO Unit

Moves a file or directory old to the new location new.

This function coincides with the POSIX rename function, see there for more information.

🔗opaque
IO.FS.removeDir : System.FilePath → IO Unit

Remove given directory. Fails if not empty; see also IO.FS.removeDirAll.

🔗def
IO.FS.lines (fname : System.FilePath)
    : IO (Array String)
🔗def
IO.FS.withTempFile.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT IO m]
    (f : IO.FS.Handle → System.FilePath → m α)
    : m α

Like createTempFile, but also takes care of removing the file after usage.

🔗opaque
IO.FS.createDirAll (p : System.FilePath)
    : IO Unit

Create given path and all missing parents as directories.

🔗def
IO.FS.writeBinFile (fname : System.FilePath)
    (content : ByteArray) : IO Unit
🔗def
IO.FS.withFile {α : Type} (fn : System.FilePath)
    (mode : IO.FS.Mode)
    (f : IO.FS.Handle → IO α) : IO α
🔗opaque
IO.FS.removeDirAll (p : System.FilePath)
    : IO Unit

Fully remove given directory by deleting all contained files and directories in an unspecified order. Fails if any contained entry cannot be deleted or was newly created during execution.

🔗opaque
IO.FS.createTempFile
    : IO (IO.FS.Handle × System.FilePath)

Creates a temporary file in the most secure manner possible. There are no race conditions in the file’s creation. The file is readable and writable only by the creating user ID. Additionally on UNIX style platforms the file is executable by nobody. The function returns both a Handle to the already opened file as well as its FilePath.

Note that it is the caller's job to remove the file after use.

🔗def
IO.FS.readFile (fname : System.FilePath)
    : IO String
🔗opaque
IO.FS.realPath (fname : System.FilePath)
    : IO System.FilePath

Resolves a pathname to an absolute pathname with no '.', '..', or symbolic links.

This function coincides with the POSIX realpath function, see there for more information.

🔗def
IO.FS.writeFile (fname : System.FilePath)
    (content : String) : IO Unit
🔗def
IO.FS.readBinFile (fname : System.FilePath)
    : IO ByteArray
🔗opaque
IO.FS.createDir : System.FilePath → IO Unit

9.5.5. 標準 I/O（Standard I/O）🔗

Unix から派生した、または Unix に影響を受けたオペレーティングシステムでは、各プロセスで利用可能な3つのストリームに 標準入力 （standard input）・ 標準出力 （standard output）・ 標準エラー （standard エラー）の名前がついています。一般的に、プログラムは標準入力から読み、標準出力に通常の出力を書き、標準エラーにエラーメッセージを書き込むことが期待されています。デフォルトでは、標準入力はコンソールからの入力を受け取り、標準出力と標準エラーに出力を行いますが、3つともパイプやファイルにリダイレクトされることが多いです。

Lean はオペレーティングシステムの標準 I/O 機能への直接アクセスを提供するのではなく、 Stream でラップしています。さらに、 IO モナドはそれらを置き換えたり、ローカルでオーバーライドするための特別なサポートを含んでいます。この特別なレベルのインダイレクトにより、Lean プログラム内で入出力をリダイレクトすることが可能になります。

🔗opaque
IO.getStdin : BaseIO IO.FS.Stream
標準入力からの読み取り

この例では、 IO.getStdin と IO.getStdout がそれぞれ現在の標準入力と標準出力を取得するために使用されています。これらは読み込みと書き込みが可能です。

def main : IO Unit := do let stdin ← IO.getStdin let stdout ← IO.getStdout stdout.putStrLn "Who is it?" let name ← stdin.getLine stdout.putStr "Hello, " stdout.putStrLn name

以下の標準入力に対して：

stdinLean user

標準出力は以下のようになります：

stdoutWho is it?Hello, Lean user
🔗opaque
IO.setStdin : IO.FS.Stream → BaseIO IO.FS.Stream

Replaces the stdin stream of the current thread and returns its previous value.

🔗def
IO.withStdin.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT BaseIO m] (h : IO.FS.Stream)
    (x : m α) : m α
🔗opaque
IO.getStdout : BaseIO IO.FS.Stream
🔗opaque
IO.setStdout
    : IO.FS.Stream → BaseIO IO.FS.Stream

Replaces the stdout stream of the current thread and returns its previous value.

🔗def
IO.withStdout.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT BaseIO m] (h : IO.FS.Stream)
    (x : m α) : m α
🔗opaque
IO.getStderr : BaseIO IO.FS.Stream
🔗opaque
IO.setStderr
    : IO.FS.Stream → BaseIO IO.FS.Stream

Replaces the stderr stream of the current thread and returns its previous value.

🔗def
IO.withStderr.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT BaseIO m] (h : IO.FS.Stream)
    (x : m α) : m α
🔗def
IO.FS.withIsolatedStreams.{u_1}
  {m : Type → Type u_1} {α : Type} [Monad m]
  [MonadFinally m] [MonadLiftT BaseIO m]
  (x : m α) (isolateStderr : Bool := true) :
  m (String × α)

Run action with stdin emptied and stdout+stderr captured into a String.

標準 I/O から文字列へのリダイレクトdef countdown : Nat → IO Unit | 0 => IO.println "Blastoff!" | n + 1 => do IO.println s!"{n + 1}" countdown n def runCountdown : IO String := do let (output, ()) ← IO.FS.withIsolatedStreams (countdown 10) return output "10\n9\n8\n7\n6\n5\n4\n3\n2\n1\nBlastoff!\n"#eval runCountdown

countdown を実行すると、出力を含む文字列が得られます：

"10\n9\n8\n7\n6\n5\n4\n3\n2\n1\nBlastoff!\n"

9.5.6. ファイルとディレクトリ（Files and Directories）

🔗opaque
IO.currentDir : IO System.FilePath
🔗opaque
IO.appPath : IO System.FilePath
🔗def
IO.appDir : IO System.FilePath