访问与修改 JSON🔗

从 JSON 读取值🔗

要从 Json 对象读取值，你可以使用像 Json.getObjValAs? 这样的专用辅助函数，它会尝试取出一个值并把它转换为特定的 Lean 类型。

def getAge (j : Json) : Except String Nat :=
  j.getObjValAs? Nat "age"

Except.ok 30#eval getAge (json% { "name": "Alice", "age": 30 })

def getJsonValue (j : Json) (key : String) : Json :=
  let val := j.getObjVal? key
  match val with
  | .ok v => v
  | .error err => panic! s!"Key '{key}' not found: {err}"

7#eval getJsonValue (json% { "name": "Bob", "age": 7 }) "age"

要获取一个 Json 对象中的所有键，你只需对 Json.obj 构造子进行匹配：

def getSortedKeys (j : Json) : List String :=
  match j with
  | .obj m => m.toList.map (·.1) |>.mergeSort
  | _ => []

["apple", "b", "cats"]#eval getSortedKeys (json% { apple: 1, "b": 2, cats: 3 })

对于更复杂的结构，你可以使用 fromJson? 类一次性解码整个对象：

structure JsonUser where
  name : String
  age  : Nat
  isAdmin : Bool
deriving FromJson, ToJson, Inhabited

def getUserName (j : Json) : String :=
  match (fromJson? j : Except String JsonUser) with
  | .ok user => user.name
  | .error err => panic! s!"Failed to decode User: {err}"

"Charlie"#eval getUserName (json% { "name": "Charlie", 
  "age": 25, "isAdmin": false })

修改 JSON 对象🔗

由于 Json 是一个不可变的归纳类型，“修改”它其实是在旧值的基础上创建一个新的 Json 值。

1. 直接操作对象🔗

如果你确知某个 Json 值是一个对象，可以对 Json.obj 进行模式匹配来访问底层的 RBMap。然后你可以使用像 insert 或 erase 这样的方法，并把结果重新包回 Json.obj。

/-- Update or add the 'isAdmin' field -/
def setAdminStatus (j : Json) (status : Bool) : Json :=
  match j with
  | Json.obj kv => Json.obj 
      (kv.insert "isAdmin" (toJson status))
  | _ => j

{"name": "Bob", "isAdmin": true}#eval setAdminStatus (json% { "name": "Bob", 
    "isAdmin": false }) true
{"name": "Charlie", "isAdmin": true}#eval setAdminStatus (json% { "name": "Charlie"}) true

/-- Remove the 'age' field if it exists -/
def stripAge (j : Json) : Json :=
  match j with
  | Json.obj kv => Json.obj (kv.erase "age")
  | _ => j

{"name": "Bob"}#eval stripAge (json% { "name": "Bob", "age": 42 })

2. 解码—修改—编码模式🔗

对于复杂的修改，尤其是涉及嵌套数据或集合的修改，最健壮的做法是把 JSON 解码为一个 Lean 结构体，用 Lean 强大的函数式工具执行更新，然后再重新编码它。

structure Endpoint where
  host : String
  port : Nat
deriving FromJson, ToJson

structure ServerConfig where
  name      : String
  endpoints : List Endpoint
  active    : Bool
  location  : Option String
deriving FromJson, ToJson

/-- Update the port for a specific host 
  and toggle the active status -/
def updateConfig (config : ServerConfig) 
    (targetHost : String) (newPort : Nat) : ServerConfig :=
  let updatedEndpoints := config.endpoints.map fun e =>
    if e.host == targetHost then 
      { e with port := newPort } else e
  { config with endpoints := updatedEndpoints, active 
    := !config.active }

def serverUpdate (j : Json) (target : String)
    (port : Nat) : Except String Json := do
  let config : ServerConfig ← fromJson? j
  return toJson (updateConfig config target port)

/- Example: Updating 'localhost' to port 8080 
  and toggling active to false -/
ok: {"name": "DevServer",
 "location": null,
 "endpoints":
 [{"port": 8080, "host": "localhost"},
  {"port": 443, "host": "api.example.com"}],
 "active": false}#eval serverUpdate (json% {
  "name": "DevServer",
  "active": true,
  "endpoints": [
    { "host": "localhost", "port": 3000 },
    { "host": "api.example.com", "port": 443 }
  ]
}) "localhost" 8080