JSON Parsing

Conservative JSON helpers shared by artifact loaders and verification tools.

The functions here fail fast with contextual messages. This module stays focused: not a schema library, just the common parsing substrate for TorchLean JSON artifacts.

def TorchLean.Json.expectObject (context : String) (value : Lean.Json) : Except String (Std.TreeMap.Raw String Lean.Json compare)

Parse a JSON value as an object.

def TorchLean.Json.expectField (context key : String) (value : Lean.Json) : Except String Lean.Json

Extract a required field from a JSON object.

def TorchLean.Json.expectString (context : String) (value : Lean.Json) : Except String String

Require a JSON string and report context in the error message on mismatch.

def TorchLean.Json.expectNat (context : String) (value : Lean.Json) : Except String Nat

Parse a JSON natural number, accepting either a JSON number or a decimal string.

def TorchLean.Json.expectArray (context : String) (value : Lean.Json) : Except String (Array Lean.Json)

Require a JSON array and return its entries.

def TorchLean.Json.readFile (path : System.FilePath) : IO Lean.Json

Read and parse a JSON file from disk.