API Json

Small conservative JSON helpers shared by public 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 NN.API.Json.fail {α : Type} (msg : String) : Except String α

Throw an Except String parse error.

def NN.API.Json.expectObjE (ctx : String) (j : Lean.Json) : Except String (Std.TreeMap.Raw String Lean.Json compare)

Parse a JSON value as an object.

def NN.API.Json.expectFieldE (ctx key : String) (j : Lean.Json) : Except String Lean.Json

Extract a required field from a JSON object.

def NN.API.Json.expectStringE (ctx : String) (j : Lean.Json) : Except String String

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

def NN.API.Json.expectNatE (ctx : String) (j : Lean.Json) : Except String Nat

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

def NN.API.Json.expectArrayE (ctx : String) (j : Lean.Json) : Except String (Array Lean.Json)

Require a JSON array and return its entries.

def NN.API.Json.optionalBoolFieldE (ctx key : String) (default : Bool) (j : Lean.Json) : Except String Bool

Parse an optional JSON boolean field with a default.

def NN.API.Json.expectNatArrayE (ctx : String) (j : Lean.Json) : Except String (Array Nat)

Parse a JSON array of natural numbers.

def NN.API.Json.parseFile (path : System.FilePath) : IO Lean.Json

Parse a JSON file from disk.