读取与写入 JSON 文件🔗

贡献者：Anirudh Gupta, subfish-zhou, swarnava1207

本节讲述如何与文件系统交互来读写 JSON 数据。关于如何构造或操作 JSON 对象本身的细节，参见创建 JSON 对象。

如何读取 JSON 文件🔗

要读取一个 JSON 文件，你可以使用 Lean 中的 Lean.Json 模块。用 IO.FS.readFile 把文件作为字符串读取，然后用 Lean.Json.parse 解析它：

def readJsonFile (path : System.FilePath) : IO Json := do
  let content ← IO.FS.readFile path
  match Json.parse content with
  | Except.ok json => return json
  | Except.error err =>
    throw <| IO.userError
      s!"Failed to parse JSON from {path}: {err}"

如何写入 JSON 文件🔗

要把 JSON 数据写入文件，你首先要把 Json 对象转换为字符串。你可以用 toString 得到紧凑表示，或用 .pretty 得到格式化的版本。

def writeJsonToFile (path : System.FilePath) (data : Json)
  : IO Unit := do IO.FS.writeFile path (data.pretty)

如果你需要更多控制，比如设置缩进级别，可以给 .pretty 方法传一个参数：

def writeJsonIndented (path : System.FilePath) (data : Json)
  : IO Unit := do  IO.FS.writeFile path (data.pretty 2)
  -- .pretty(2) formats the JSON with an indent of 2 spaces