其他 JSON 操作🔗

派生实例虽然方便，但现实中的 JSON 常常需要手动控制序列化、默认值以及各种变换。

1. 字段重命名（手写实例）🔗

如果你的 JSON 使用 snake_case 而你的 Lean 代码使用 camelCase，你可以手动实现 ToJson 和 FromJson 实例。

Lean 中的 instance 关键字用于为一个类型类（type class）提供实现。这里，ToJson 和 FromJson 是类型类，定义了一个类型应如何与 Json 相互转换。通过手动定义这些实例，你可以完全控制映射过程，从而弥合不同命名约定或数据结构之间的差异。

structure Person where
  firstName : String
  lastName  : String
deriving Repr

instance : ToJson Person where
  toJson p := json% {
    "first_name": $(p.firstName),
    "last_name": $(p.lastName)
  }

instance : FromJson Person where
  fromJson? j := do
    let first ← j.getObjValAs? String "first_name"
    let last  ← j.getObjValAs? String "last_name"
    return { firstName := first, lastName := last }

{"last_name": "Lovelace", "first_name": "Ada"}#eval toJson 
  ({ firstName := "Ada", lastName := "Lovelace" : Person })
Except.ok { firstName := "Ada", lastName := "Lovelace" }#eval (fromJson? (json% { "first_name": "Ada", 
    "last_name": "Lovelace" }) : Except String Person)

2. 处理默认值🔗

你可以使用 Json.getObjValAs?，在某个键缺失或不是期望类型时提供一个回退值。

def getPort (j : Json) (defaultPort : Nat := 8080) : Nat :=
  match j.getObjValAs? Nat "port" with
  | .ok n => n
  | .error _ => defaultPort

3000#eval getPort (json% { "host": "localhost", "port": 3000 })
8080#eval getPort (json% { "host": "localhost" })