diff --git a/LANGUAGE.md b/LANGUAGE.md index 48f2b64..721a7cf 100644 --- a/LANGUAGE.md +++ b/LANGUAGE.md @@ -556,6 +556,39 @@ use "stdlib/math.goth" | `canvas.goth` | Canvas/graphics operations | | `tui.goth` | Terminal UI operations | | `random.goth` | Seeded PRNG (xorshift64) with state-passing pattern | +| `crypto.goth` | SHA-256, MD5, BLAKE3, Base64 encode/decode | +| `json.goth` | JSON parser/serializer (`parseJson`, `toJson`, accessors) | + +### JSON + +The `json.goth` module provides a pure Goth JSON parser and serializer. JSON values are represented as tagged 2-tuples `⟨tag, payload⟩` where the tag discriminates the type: + +```goth +use "stdlib/json.goth" + +╭─ main : () → String +╰─ let r = parseJson "{\"name\":\"Goth\",\"version\":1}" + in if r.0 then toJson r.1 else "error: " ⧺ r.2 +``` + +| Function | Signature | Description | +|----------|-----------|-------------| +| `jsonNull` | `() → Json` | Construct null (tag 0) | +| `jsonBool` | `Bool → Json` | Construct boolean (tag 1) | +| `jsonNum` | `F64 → Json` | Construct number (tag 2) | +| `jsonStr` | `String → Json` | Construct string (tag 3) | +| `jsonArr` | `[n]Json → Json` | Construct array (tag 4) | +| `jsonObj` | `[n]⟨String, Json⟩ → Json` | Construct object (tag 5) | +| `parseJson` | `String → ⟨Bool, Json, String⟩` | Parse JSON string; `⟨⊤, val, ""⟩` or `⟨⊥, 0, errMsg⟩` | +| `toJson` | `Json → String` | Serialize to compact JSON | +| `jsonGet` | `String → Json → ⟨Bool, Json⟩` | Lookup key in object | +| `jsonIndex` | `ℤ → Json → ⟨Bool, Json⟩` | Index into array | +| `jsonKeys` | `Json → [n]String` | Object keys | +| `jsonValues` | `Json → [n]Json` | Object values | +| `jsonLen` | `Json → ℤ` | Array/object length | +| `jsonType` | `Json → String` | Type name string | +| `isNull`, `isBool`, `isNum`, `isStr`, `isArr`, `isObj` | `Json → Bool` | Type predicates | +| `asBool`, `asNum`, `asStr`, `asArr`, `asObj` | `Json → α` | Payload extractors (unsafe) | ### Random Number Generation diff --git a/docs/CLAUDE-SKILLS.md b/docs/CLAUDE-SKILLS.md index 6c9952d..73ea4bc 100644 --- a/docs/CLAUDE-SKILLS.md +++ b/docs/CLAUDE-SKILLS.md @@ -1,5 +1,7 @@ # Claude Skills: Working with Goth +> **Version:** 2026-02-02T14:47:26Z + This guide describes how Claude (or other LLMs) can effectively generate and modify Goth code using the AST-first workflow. ## Overview @@ -643,6 +645,276 @@ use "stdlib/crypto.goth" - De Bruijn index tracking is critical in hash compression loops — annotate every `let` with a comment showing the current index state (e.g., `# ₀=ki ₁=roundIdx ₂=st ₃=schedule`) - Use `fold` over `iota N` for round-based processing; inside the fold lambda, `₁` = accumulator, `₀` = round index +## Standard Library: JSON + +The `stdlib/json.goth` module provides a pure-Goth JSON parser and serializer. JSON values are represented as tagged 2-tuples `⟨tag, payload⟩` where the integer tag discriminates the type. Import with `use "stdlib/json.goth"`. + +**Key design pattern:** JSON values use integer-tagged tuples rather than algebraic data types (Goth's `enum` constructors are not yet wired into the evaluator). Use constructors to build values and predicates/extractors to inspect them. The parser returns a Result triple `⟨Bool, Json, String⟩` following the `result.goth` convention. + +**Value representation:** + +| Tag | JSON type | Constructor | Payload | +|-----|-----------|-------------|---------| +| 0 | null | `jsonNull ⟨⟩` | `0` (unused) | +| 1 | boolean | `jsonBool ⊤` | `Bool` | +| 2 | number | `jsonNum 3.14` | `F64` | +| 3 | string | `jsonStr "hi"` | `String` | +| 4 | array | `jsonArr [...]` | `[n]Json` | +| 5 | object | `jsonObj [⟨"k", v⟩]` | `[n]⟨String, Json⟩` | + +**Parse and extract fields:** + +```goth +use "stdlib/json.goth" + +╭─ main : () → String +╰─ let r = parseJson "{\"name\":\"Goth\",\"version\":1}" + in if ¬(r.0) then "error: " ⧺ r.2 + else let json = r.1 + in let name = jsonGet "name" json + in if name.0 then asStr name.1 else "unknown" +``` + +**Build and serialize:** + +```goth +use "stdlib/json.goth" + +╭─ main : () → String +╰─ let obj = jsonObj [ + ⟨"x", jsonNum 1.0⟩, + ⟨"y", jsonArr [jsonBool ⊤, jsonNull ⟨⟩]⟩ + ] + in toJson obj +# {"x":1,"y":[true,null]} +``` + +**Roundtrip (parse → serialize → re-parse → compare):** + +```goth +use "stdlib/json.goth" + +╭─ main : () → String +╰─ let input = "{\"a\":1,\"b\":[2,3],\"c\":{\"d\":true}}" + in let r1 = parseJson input + in if ¬(r1.0) then "parse error" + else let s1 = toJson r1.1 + in let r2 = parseJson s1 + in if ¬(r2.0) then "re-parse error" + else if strEq s1 (toJson r2.1) then "PASS" else "FAIL" +``` + +**Public functions:** + +| Function | Signature | Description | +|----------|-----------|-------------| +| `jsonNull` | `() → Json` | Construct null | +| `jsonBool` | `Bool → Json` | Construct boolean | +| `jsonNum` | `F64 → Json` | Construct number | +| `jsonStr` | `String → Json` | Construct string | +| `jsonArr` | `[n]Json → Json` | Construct array | +| `jsonObj` | `[n]⟨String, Json⟩ → Json` | Construct object | +| `parseJson` | `String → ⟨Bool, Json, String⟩` | Parse JSON; `⟨⊤, val, ""⟩` or `⟨⊥, 0, errMsg⟩` | +| `toJson` | `Json → String` | Serialize to compact JSON | +| `showJson` | `Json → String` | Alias for `toJson` | +| `jsonGet` | `String → Json → ⟨Bool, Json⟩` | Lookup key in object (Option) | +| `jsonIndex` | `ℤ → Json → ⟨Bool, Json⟩` | Index into array (Option) | +| `jsonKeys` | `Json → [n]String` | Object keys | +| `jsonValues` | `Json → [n]Json` | Object values | +| `jsonLen` | `Json → ℤ` | Array/object length | +| `jsonType` | `Json → String` | `"null"`, `"bool"`, `"number"`, `"string"`, `"array"`, `"object"` | +| `isNull` | `Json → Bool` | Tag = 0 | +| `isBool` | `Json → Bool` | Tag = 1 | +| `isNum` | `Json → Bool` | Tag = 2 | +| `isStr` | `Json → Bool` | Tag = 3 | +| `isArr` | `Json → Bool` | Tag = 4 | +| `isObj` | `Json → Bool` | Tag = 5 | +| `asBool` | `Json → Bool` | Extract boolean payload (unsafe) | +| `asNum` | `Json → F64` | Extract number payload (unsafe) | +| `asStr` | `Json → String` | Extract string payload (unsafe) | +| `asArr` | `Json → [n]Json` | Extract array payload (unsafe) | +| `asObj` | `Json → [n]⟨String, Json⟩` | Extract object entries (unsafe) | + +**Implementation notes for LLMs:** +- JSON values are just `⟨Int, payload⟩` tuples — check tag with `.0`, extract with `.1` +- `jsonGet` and `jsonIndex` return Option tuples `⟨Bool, Json⟩` — check `.0` before accessing `.1` +- The parser uses recursive descent with position threading: each internal parser function takes `[n]Char → ℤ → ⟨Bool, value, ℤ⟩` (chars, position → ok?, value, new position) +- De Bruijn indices in the parser go deep — the code annotates every `let` with an index comment (e.g., `# ₀=p1 ₁=acc ₂=pos ₃=chars`) +- Chained field access like `x.1.1` does **not** work — the parser reads `.1.1` as the float literal `1.1`. Use a helper function or intermediate `let` to access nested tuple fields +- The `fromChars` primitive is needed for building strings from char arrays (e.g., in the string parser and number parser) +- `⧺` on arrays appends (snoc): `acc ⧺ [elem]` builds arrays element by element during parsing +- `escapeJsonStr` handles `"`, `\`, `\n`, `\t`, `\r`; `\uXXXX` escapes are replaced with `?` +- Number serialization uses Goth's `toString` — formatting may differ from strict JSON (e.g., `1.0` renders as `1`) + +## Complex Numbers + +Goth has first-class complex number support. Complex values are `Value::Complex(re, im)` internally, with type annotation `ℂ` or `Complex`. + +**Literal syntax:** + +```goth +3 + 4𝕚 # Complex(3, 4) — Unicode imaginary unit U+1D55A +3 + 4i # Same — ASCII fallback +𝕚 # Complex(0, 1) — standalone imaginary unit +5𝕚 # Complex(0, 5) +``` + +**Auto-promotion chain:** `ℤ → F → ℂ → ℍ`. When one operand is Complex, the other is promoted automatically. + +**Arithmetic:** All standard operators work: `+`, `-`, `×`, `/`, `^`. Multiplication uses the standard formula `(a+bi)(c+di) = (ac-bd) + (ad+bc)i`. + +**Math functions extended to complex:** + +| Function | Complex behavior | +|----------|-----------------| +| `sqrt` | Polar-form square root; `√(0 - 4)` → `2𝕚` | +| `exp` | `e^(a+bi) = e^a(cos b + i sin b)` — Euler's formula | +| `ln` | `ln|z| + i·arg(z)` | +| `sin` | `sin(a)cosh(b) + i·cos(a)sinh(b)` | +| `cos` | `cos(a)cosh(b) - i·sin(a)sinh(b)` | +| `abs` | Returns `F64`: modulus `√(re² + im²)` | + +> `tan`, `asin`, `acos`, `atan`, `sinh`, `cosh`, `tanh` are **not** extended to complex — they accept real arguments only. + +**Decomposition primitives:** + +| Primitive | Signature | Description | +|-----------|-----------|-------------| +| `re` | `ℂ → F` | Real part (`re(3+4𝕚) = 3`) | +| `im` | `ℂ → F` | Imaginary part (`im(3+4𝕚) = 4`) | +| `conj` | `ℂ → ℂ` | Conjugate (`conj(3+4𝕚) = 3-4𝕚`) | +| `arg` | `ℂ → F` | Argument in radians (`arg(𝕚) = π/2`) | + +For plain real numbers, `re` returns the value, `im` returns `0.0`, `conj` returns the value unchanged. + +**Examples:** + +```goth +exp(π × 𝕚) + 1 # ≈ 0 (Euler's identity) +√(0 - 4) # 2𝕚 +(3 + 4𝕚) × (1 + 2𝕚) # -5+10𝕚 +abs(3 + 4𝕚) # 5.0 +``` + +**Display format:** `3 + 4𝕚`, `3 - 4𝕚`, `5𝕚` (pure imaginary), `3` (pure real). Zero displays as `0`. + +## Quaternions + +Goth supports quaternion arithmetic with the Hamilton product. Quaternion values are `Value::Quaternion(w, i, j, k)` with type annotation `ℍ` or `Quaternion`. + +**Literal syntax:** + +```goth +𝕚 # Quaternion(0,1,0,0) — also Complex if no j/k context +𝕛 # Quaternion(0,0,1,0) — Unicode U+1D55B +𝕜 # Quaternion(0,0,0,1) — Unicode U+1D55C +3𝕛 # Quaternion(0,0,3,0) +1 + 2𝕚 + 3𝕛 + 4𝕜 # Quaternion(1,2,3,4) +``` + +ASCII fallbacks: `j`, `k` (e.g., `3j`, `4k`). + +**Arithmetic:** `+`, `-`, `×`, `/`, negation. Multiplication is the **non-commutative** Hamilton product: + +| Rule | Result | +|------|--------| +| `𝕚 × 𝕛` | `𝕜` | +| `𝕛 × 𝕜` | `𝕚` | +| `𝕜 × 𝕚` | `𝕛` | +| `𝕛 × 𝕚` | `-𝕜` | +| `𝕚 × 𝕛 × 𝕜` | `-1` | + +Division: `a / b = a × conj(b) / |b|²`. + +**Decomposition:** + +| Primitive | Quaternion behavior | +|-----------|-------------------| +| `re` | Returns `F64`: the scalar (w) component | +| `im` | Returns `⟨F, F, F⟩`: the (i, j, k) components as a 3-tuple | +| `conj` | Returns `ℍ`: `(w, -i, -j, -k)` | +| `abs` | Returns `F64`: norm `√(w² + i² + j² + k²)` | + +> Quaternion `exp`, `ln`, `sqrt`, `pow`, `sin`, `cos` are **not** implemented — only basic arithmetic, `abs`, `conj`, `re`, `im`. + +**Example:** + +```goth +# Hamilton's identity +╭─ main : I64 → ℍ +│ ⊨ re(₀) = 0.0 - 1.0 +╰─ 𝕚 × 𝕛 × 𝕜 +``` + +## Linear Algebra + +Goth provides built-in linear algebra primitives operating on rank-2 tensors (matrices) and rank-1 tensors (vectors). + +### Core Operations + +| Name | Signature | Description | +|------|-----------|-------------| +| `·`, `dot` | `[n]F64 → [n]F64 → F64` | Dot product | +| `norm` | `[n]F64 → F64` | Euclidean (L2) norm | +| `matmul` | `[m n]F64 → [n p]F64 → [m p]F64` | Matrix multiplication (inner dims must match) | +| `⍉`, `transpose` | `[m n]α → [n m]α` | Matrix transpose | + +### Matrix Utilities + +| Name | Signature | Description | +|------|-----------|-------------| +| `trace`, `tr` | `[n n]F64 → F64` | Sum of diagonal elements | +| `det` | `[n n]F64 → F64` | Determinant (LU decomposition) | +| `inv` | `[n n]F64 → [n n]F64` | Matrix inverse (errors on singular) | +| `diag` | `[n]F64 → [n n]F64` | Vector → diagonal matrix | +| `diag` | `[n n]F64 → [n]F64` | Matrix → diagonal vector | +| `eye` | `ℤ → [n n]F64` | Identity matrix of size n | + +`diag` is dual-mode: rank-1 input builds a diagonal matrix, rank-2 input extracts the diagonal. + +### Eigenvalue / Eigenvector + +| Name | Signature | Description | +|------|-----------|-------------| +| `eig` | `[n n]F64 → [n]F64\|[n]ℂ` | Eigenvalues | +| `eigvecs` | `[n n]F64 → ⟨[n]α, [n n]α⟩` | Eigenvalues + eigenvector matrix | + +**Algorithm:** Hessenberg reduction via Householder similarity transforms, then QR iteration with Wilkinson shifts and Givens rotations. Max iterations: `100 × n`. + +**Return type:** If all eigenvalues are real (imaginary part < 1e-12), returns Float tensors. If any are complex, returns tensors with Complex values. Eigenvalues sorted by real part descending. + +`eigvecs` returns `⟨eigenvalues, eigenvector_matrix⟩` where columns of the matrix are eigenvectors. Eigenvectors computed via inverse iteration (real eigenvalues) or 2n×2n real embedding for complex pairs. + +### Linear System Solvers + +| Name | Signature | Description | +|------|-----------|-------------| +| `solve` | `[n n]F64 → [n]F64 → [n]F64` | Solve Ax = b (LU, default) | +| `solveWith` | `[n n]F64 → [n]F64 → String → [n]F64` | Solve with method choice | + +`solveWith` methods: +- `"lu"` — Doolittle LU with partial pivoting (same as `solve`) +- `"qr"` — Householder QR; handles overdetermined (least-squares) systems where m ≥ n + +**Examples:** + +```goth +solve [[2,1],[5,3]] [4,7] # [5, -6] +solveWith [[1,1],[1,2],[1,3]] [1,2,2] "qr" # least-squares +det [[6,1,1],[4,0-2,5],[2,8,7]] # -306 +eig [[2,1],[1,2]] # [3, 1] +eig [[0,0-1],[1,0]] # [0+1𝕚, 0-1𝕚] +eigvecs (diag [5,3]) # ⟨[5, 3], [[1,0],[0,1]]⟩ +inv [[1,2],[3,4]] # [[-2, 1], [1.5, -0.5]] +``` + +**Implementation notes for LLMs:** +- All matrix operations require rank-2 tensors; pass `[[1,2],[3,4]]` not `[1,2,3,4]` +- `outer` and `inner` are declared in the PrimFn enum but **not implemented** — they produce a runtime "not implemented" error +- Singularity threshold is `1e-12` for inverse, `1e-15` for LU pivot +- Negative literal syntax quirk: Goth parses `0-2` as subtraction; `-2` in a matrix literal may be parsed as unary negation depending on context, so `0-2` is safest in array literals +- `diag` auto-detects rank: `diag [1,2,3]` builds a 3×3 diagonal matrix; `diag [[1,0],[0,2]]` extracts `[1,2]` + ## Goth Syntax ↔ JSON | Goth Syntax | JSON AST | diff --git a/stdlib/json.goth b/stdlib/json.goth new file mode 100644 index 0000000..e1afb1c --- /dev/null +++ b/stdlib/json.goth @@ -0,0 +1,341 @@ +# Goth Standard Library - JSON Parser and Serializer +# Pure Goth implementation of a JSON parser and serializer. +# +# Usage: +# use "stdlib/json.goth" +# let result = parseJson "{\"name\":\"goth\",\"version\":1}" +# in if result.0 then toJson result.1 else "parse error: " ⧺ result.2 +# +# JSON values are represented as tagged 2-tuples ⟨tag, payload⟩: +# Tag Type Payload +# 0 null 0 +# 1 bool Bool +# 2 number F64 +# 3 string String +# 4 array [n]Json +# 5 object [n]⟨String, Json⟩ + +# ============ Constructors ============ + +# Create a JSON null +╭─ jsonNull : ⟨⟩ → ⟨ℤ, ℤ⟩ +╰─ ⟨0, 0⟩ + +# Create a JSON boolean +╭─ jsonBool : Bool → ⟨ℤ, Bool⟩ +╰─ ⟨1, ₀⟩ + +# Create a JSON number +╭─ jsonNum : F → ⟨ℤ, F⟩ +╰─ ⟨2, ₀⟩ + +# Create a JSON string +╭─ jsonStr : String → ⟨ℤ, String⟩ +╰─ ⟨3, ₀⟩ + +# Create a JSON array +╭─ jsonArr : [n]α → ⟨ℤ, [n]α⟩ +╰─ ⟨4, ₀⟩ + +# Create a JSON object from key-value pairs +╭─ jsonObj : [n]⟨String, α⟩ → ⟨ℤ, [n]⟨String, α⟩⟩ +╰─ ⟨5, ₀⟩ + +# ============ Type Predicates ============ + +╭─ isNull : ⟨ℤ, α⟩ → Bool +╰─ ₀.0 = 0 + +╭─ isBool : ⟨ℤ, α⟩ → Bool +╰─ ₀.0 = 1 + +╭─ isNum : ⟨ℤ, α⟩ → Bool +╰─ ₀.0 = 2 + +╭─ isStr : ⟨ℤ, α⟩ → Bool +╰─ ₀.0 = 3 + +╭─ isArr : ⟨ℤ, α⟩ → Bool +╰─ ₀.0 = 4 + +╭─ isObj : ⟨ℤ, α⟩ → Bool +╰─ ₀.0 = 5 + +# ============ Extractors ============ + +# Get payload (unsafe — caller must check tag first) +╭─ asBool : ⟨ℤ, α⟩ → Bool +╰─ ₀.1 + +╭─ asNum : ⟨ℤ, α⟩ → F +╰─ ₀.1 + +╭─ asStr : ⟨ℤ, α⟩ → String +╰─ ₀.1 + +╭─ asArr : ⟨ℤ, α⟩ → [n]α +╰─ ₀.1 + +╭─ asObj : ⟨ℤ, α⟩ → [n]⟨String, α⟩ +╰─ ₀.1 + +# ============ Type Name ============ + +╭─ jsonType : ⟨ℤ, α⟩ → String +╰─ if ₀.0 = 0 then "null" + else if ₀.0 = 1 then "bool" + else if ₀.0 = 2 then "number" + else if ₀.0 = 3 then "string" + else if ₀.0 = 4 then "array" + else if ₀.0 = 5 then "object" + else "unknown" + +# ============ Object/Array Access ============ + +# Lookup key in JSON object → Option ⟨Bool, Json⟩ +╭─ jsonGet : String → ⟨ℤ, α⟩ → ⟨Bool, α⟩ +╰─ if ₀.0 ≠ 5 then ⟨⊥, 0⟩ + else let entries = ₀.1 + # ₀=entries ₁=json ₂=key + in let matches = iota (len ₀) ▸ λ→ strEq ₁[₀].0 ₃ + # ₀=matches ₁=entries ₂=json ₃=key + in if len ₀ > 0 then ⟨⊤, ₁[₀[0]].1⟩ else ⟨⊥, 0⟩ + +# Index into JSON array → Option ⟨Bool, Json⟩ +╭─ jsonIndex : ℤ → ⟨ℤ, α⟩ → ⟨Bool, α⟩ +╰─ if ₀.0 ≠ 4 then ⟨⊥, 0⟩ + else let elems = ₀.1 + # ₀=elems ₁=json ₂=idx + in if ₂ ≥ 0 ∧ ₂ < len ₀ then ⟨⊤, ₀[₂]⟩ else ⟨⊥, 0⟩ + +# Get all keys from a JSON object +╭─ jsonKeys : ⟨ℤ, α⟩ → [n]String +╰─ if ₀.0 ≠ 5 then [] + else ₀.1 ↦ λ→ ₀.0 + +# Get all values from a JSON object +╭─ jsonValues : ⟨ℤ, α⟩ → [n]α +╰─ if ₀.0 ≠ 5 then [] + else ₀.1 ↦ λ→ ₀.1 + +# Length of array or object +╭─ jsonLen : ⟨ℤ, α⟩ → ℤ +╰─ if ₀.0 = 4 ∨ ₀.0 = 5 then len ₀.1 else 0 + +# ============ Serializer ============ + +# Escape special characters in a string for JSON output +╭─ escapeJsonStr : String → String +╰─ let cs = chars ₀ + in ⌿ (λ→ λ→ + # ₁=acc ₀=ch + if ₀ = '"' then ₁ ⧺ "\\\"" + else if ₀ = '\\' then ₁ ⧺ "\\\\" + else if ₀ = '\n' then ₁ ⧺ "\\n" + else if ₀ = '\t' then ₁ ⧺ "\\t" + else if ₀ = '\r' then ₁ ⧺ "\\r" + else ₁ ⧺ (fromChars [₀]) + ) "" cs + +# Serialize a JSON value to a compact string +╭─ toJson : ⟨ℤ, α⟩ → String +╰─ if ₀.0 = 0 then "null" + else if ₀.0 = 1 then if ₀.1 then "true" else "false" + else if ₀.0 = 2 then toString ₀.1 + else if ₀.0 = 3 then "\"" ⧺ escapeJsonStr ₀.1 ⧺ "\"" + else if ₀.0 = 4 then + let elems = ₀.1 + in if len ₀ = 0 then "[]" + else "[" ⧺ ⌿ (λ→ λ→ + # ₁=acc ₀=elem + if ₁ = "" then toJson ₀ + else ₁ ⧺ "," ⧺ toJson ₀ + ) "" ₀ ⧺ "]" + else if ₀.0 = 5 then + let entries = ₀.1 + in if len ₀ = 0 then "{}" + else "{" ⧺ ⌿ (λ→ λ→ + # ₁=acc ₀=kv + let kvStr = "\"" ⧺ escapeJsonStr ₀.0 ⧺ "\":" ⧺ toJson ₀.1 + # ₀=kvStr ₁=kv ₂=acc + in if ₂ = "" then ₀ + else ₂ ⧺ "," ⧺ ₀ + ) "" ₀ ⧺ "}" + else "null" + +# Alias +╭─ showJson : ⟨ℤ, α⟩ → String +╰─ toJson ₀ + +# ============ Parser Internals ============ + +# Skip whitespace characters starting at position +# Returns new position after whitespace +╭─ pSkipWS : [n]Char → ℤ → ℤ +╰─ if ₀ ≥ len ₁ then ₀ + else if ₁[₀] = ' ' ∨ ₁[₀] = '\t' ∨ ₁[₀] = '\n' ∨ ₁[₀] = '\r' + then pSkipWS ₁ (₀ + 1) + else ₀ + +# Parse a JSON string literal (opening " already peeked but not consumed) +# ₁=chars ₀=pos (pointing at opening ") +# Returns ⟨Bool, ⟨ℤ, String⟩, ℤ⟩ +╭─ pStringInner : [n]Char → ℤ → [m]Char → ⟨Bool, α, ℤ⟩ +╰─ # ₂=chars ₁=pos ₀=acc (accumulated chars) + if ₁ ≥ len ₂ then ⟨⊥, 0, ₁⟩ + else if ₂[₁] = '"' then ⟨⊤, jsonStr (fromChars ₀), ₁ + 1⟩ + else if ₂[₁] = '\\' then + if ₁ + 1 ≥ len ₂ then ⟨⊥, 0, ₁⟩ + else if ₂[₁ + 1] = '"' then pStringInner ₂ (₁ + 2) (₀ ⧺ ['"']) + else if ₂[₁ + 1] = '\\' then pStringInner ₂ (₁ + 2) (₀ ⧺ ['\\']) + else if ₂[₁ + 1] = '/' then pStringInner ₂ (₁ + 2) (₀ ⧺ ['/']) + else if ₂[₁ + 1] = 'n' then pStringInner ₂ (₁ + 2) (₀ ⧺ ['\n']) + else if ₂[₁ + 1] = 't' then pStringInner ₂ (₁ + 2) (₀ ⧺ ['\t']) + else if ₂[₁ + 1] = 'r' then pStringInner ₂ (₁ + 2) (₀ ⧺ ['\r']) + else if ₂[₁ + 1] = 'b' then pStringInner ₂ (₁ + 2) (₀ ⧺ [' ']) + else if ₂[₁ + 1] = 'f' then pStringInner ₂ (₁ + 2) (₀ ⧺ [' ']) + else if ₂[₁ + 1] = 'u' then pStringInner ₂ (₁ + 6) (₀ ⧺ ['?']) + else pStringInner ₂ (₁ + 2) (₀ ⧺ [₂[₁ + 1]]) + else pStringInner ₂ (₁ + 1) (₀ ⧺ [₂[₁]]) + +╭─ pString : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ pStringInner ₁ (₀ + 1) [] + +# Collect number characters (digits, '.', '-', '+', 'e', 'E') +╭─ pNumChars : [n]Char → ℤ → ℤ +╰─ if ₀ ≥ len ₁ then ₀ + else if (₁[₀] ≥ '0' ∧ ₁[₀] ≤ '9') ∨ ₁[₀] = '.' ∨ ₁[₀] = '-' ∨ ₁[₀] = '+' ∨ ₁[₀] = 'e' ∨ ₁[₀] = 'E' + then pNumChars ₁ (₀ + 1) + else ₀ + +╭─ pNumber : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ let endPos = pNumChars ₁ ₀ + # ₀=endPos ₁=startPos ₂=chars + in if ₀ = ₁ then ⟨⊥, 0, ₁⟩ + else let numStr = fromChars (take (₀ - ₁) (drop ₁ ₂)) + # ₀=numStr ₁=endPos ₂=startPos ₃=chars + in ⟨⊤, jsonNum (parseFloat ₀), ₁⟩ + +# Parse "true" +╭─ pTrue : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ if ₀ + 4 > len ₁ then ⟨⊥, 0, ₀⟩ + else if ₁[₀] = 't' ∧ ₁[₀ + 1] = 'r' ∧ ₁[₀ + 2] = 'u' ∧ ₁[₀ + 3] = 'e' + then ⟨⊤, jsonBool ⊤, ₀ + 4⟩ + else ⟨⊥, 0, ₀⟩ + +# Parse "false" +╭─ pFalse : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ if ₀ + 5 > len ₁ then ⟨⊥, 0, ₀⟩ + else if ₁[₀] = 'f' ∧ ₁[₀ + 1] = 'a' ∧ ₁[₀ + 2] = 'l' ∧ ₁[₀ + 3] = 's' ∧ ₁[₀ + 4] = 'e' + then ⟨⊤, jsonBool ⊥, ₀ + 5⟩ + else ⟨⊥, 0, ₀⟩ + +# Parse "null" +╭─ pNull : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ if ₀ + 4 > len ₁ then ⟨⊥, 0, ₀⟩ + else if ₁[₀] = 'n' ∧ ₁[₀ + 1] = 'u' ∧ ₁[₀ + 2] = 'l' ∧ ₁[₀ + 3] = 'l' + then ⟨⊤, jsonNull ⟨⟩, ₀ + 4⟩ + else ⟨⊥, 0, ₀⟩ + +# Parse array elements after '[' and optional whitespace +# ₂=chars ₁=pos ₀=acc (accumulated elements) +╭─ pArrayElems : [n]Char → ℤ → [m]α → ⟨Bool, α, ℤ⟩ +╰─ let r = pValue ₂ ₁ + # ₀=r ₁=acc ₂=pos ₃=chars + in if ¬(₀.0) then ⟨⊥, 0, ₀.2⟩ + else let newAcc = ₁ ⧺ [₀.1] + # ₀=newAcc ₁=r ₂=acc ₃=pos ₄=chars + in let p2 = pSkipWS ₄ ₁.2 + # ₀=p2 ₁=newAcc ₂=r ₃=acc ₄=pos ₅=chars + in if ₀ ≥ len ₅ then ⟨⊥, 0, ₀⟩ + else if ₅[₀] = ']' then ⟨⊤, jsonArr ₁, ₀ + 1⟩ + else if ₅[₀] = ',' then pArrayElems ₅ (pSkipWS ₅ (₀ + 1)) ₁ + else ⟨⊥, 0, ₀⟩ + +# Parse a JSON array +╭─ pArray : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ let p1 = pSkipWS ₁ (₀ + 1) + # ₀=p1 ₁=startPos ₂=chars + in if ₀ ≥ len ₂ then ⟨⊥, 0, ₀⟩ + else if ₂[₀] = ']' then ⟨⊤, jsonArr [], ₀ + 1⟩ + else pArrayElems ₂ ₀ [] + +# Helper: extract the string payload from a jsonStr value +╭─ getStrPayload : ⟨ℤ, α⟩ → String +╰─ ₀.1 + +# Helper: parse one object entry (key:value), return ⟨ok, ⟨keyStr, val⟩, newPos⟩ +# ₁=chars ₀=pos (pointing at the key's opening ") +╭─ pOneEntry : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ let keyRes = pString ₁ ₀ + # ₀=keyRes ₁=pos ₂=chars + in if ¬(₀.0) then ⟨⊥, 0, ₀.2⟩ + else let keyStr = getStrPayload ₀.1 + # ₀=keyStr ₁=keyRes ₂=pos ₃=chars + in let p2 = pSkipWS ₃ ₁.2 + # ₀=p2 ₁=keyStr ₂=keyRes ₃=pos ₄=chars + in if ₀ ≥ len ₄ then ⟨⊥, 0, ₀⟩ + else if ₄[₀] ≠ ':' then ⟨⊥, 0, ₀⟩ + else let p3 = pSkipWS ₄ (₀ + 1) + # ₀=p3 ₁=p2 ₂=keyStr ₃=keyRes ₄=pos ₅=chars + in let valRes = pValue ₅ ₀ + # ₀=valRes ₁=p3 ₂=p2 ₃=keyStr + in if ¬(₀.0) then ⟨⊥, 0, ₀.2⟩ + else ⟨⊤, ⟨₃, ₀.1⟩, ₀.2⟩ + +# Parse object key-value pairs after '{' +# ₂=chars ₁=pos ₀=acc (accumulated key-value pairs) +╭─ pObjectEntries : [n]Char → ℤ → [m]α → ⟨Bool, α, ℤ⟩ +╰─ let p1 = pSkipWS ₂ ₁ + # ₀=p1 ₁=acc ₂=pos ₃=chars + in if ₀ ≥ len ₃ then ⟨⊥, 0, ₀⟩ + else if ₃[₀] ≠ '"' then ⟨⊥, 0, ₀⟩ + else let entryRes = pOneEntry ₃ ₀ + # ₀=entryRes ₁=p1 ₂=acc ₃=pos ₄=chars + in if ¬(₀.0) then ⟨⊥, 0, ₀.2⟩ + else let newAcc = ₂ ⧺ [₀.1] + # ₀=newAcc ₁=entryRes ₂=p1 ₃=acc ₄=pos ₅=chars + in let p4 = pSkipWS ₅ ₁.2 + # ₀=p4 ₁=newAcc ₂=entryRes ₃=p1 ₄=acc ₅=pos ₆=chars + in if ₀ ≥ len ₆ then ⟨⊥, 0, ₀⟩ + else if ₆[₀] = '}' then ⟨⊤, jsonObj ₁, ₀ + 1⟩ + else if ₆[₀] = ',' then pObjectEntries ₆ (₀ + 1) ₁ + else ⟨⊥, 0, ₀⟩ + +# Parse a JSON object +╭─ pObject : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ let p1 = pSkipWS ₁ (₀ + 1) + # ₀=p1 ₁=startPos ₂=chars + in if ₀ ≥ len ₂ then ⟨⊥, 0, ₀⟩ + else if ₂[₀] = '}' then ⟨⊤, jsonObj [], ₀ + 1⟩ + else pObjectEntries ₂ ₀ [] + +# Top-level value parser: skip ws, peek, dispatch +╭─ pValue : [n]Char → ℤ → ⟨Bool, α, ℤ⟩ +╰─ let p = pSkipWS ₁ ₀ + # ₀=p ₁=startPos ₂=chars + in if ₀ ≥ len ₂ then ⟨⊥, 0, ₀⟩ + else if ₂[₀] = '"' then pString ₂ ₀ + else if ₂[₀] = 't' then pTrue ₂ ₀ + else if ₂[₀] = 'f' then pFalse ₂ ₀ + else if ₂[₀] = 'n' then pNull ₂ ₀ + else if ₂[₀] = '[' then pArray ₂ ₀ + else if ₂[₀] = '{' then pObject ₂ ₀ + else if (₂[₀] ≥ '0' ∧ ₂[₀] ≤ '9') ∨ ₂[₀] = '-' + then pNumber ₂ ₀ + else ⟨⊥, 0, ₀⟩ + +# ============ Public Parser API ============ + +# Parse a JSON string → Result ⟨Bool, Json, String⟩ +# Success: ⟨⊤, jsonValue, ""⟩ +# Failure: ⟨⊥, 0, errorMessage⟩ +╭─ parseJson : String → ⟨Bool, α, String⟩ +╰─ let cs = chars ₀ + in let result = pValue cs 0 + # ₀=result ₁=cs ₂=input + in if ¬(₀.0) then ⟨⊥, 0, "parse error at position " ⧺ toString ₀.2⟩ + else let finalPos = pSkipWS ₁ ₀.2 + # ₀=finalPos ₁=result ₂=cs ₃=input + in if ₀ < len ₂ then ⟨⊥, 0, "trailing content at position " ⧺ toString ₀⟩ + else ⟨⊤, ₁.1, ""⟩