// E# — a verified example from the E# language corpus (CLR language; .es, not ECMAScript).
// provenance: json.es   topic: choice   status: verified
// hand-authored, idiomatic E# — verified through the E# compiler

namespace Demo

using "System.Text"                    // StringBuilder

// ═════════════════════════════════════════════════════════════════════════════
// A JSON value, modeled and serialized. The shape of JSON is a recursive sum type —
// a value is null, a bool, a number, a string, an array OF values, or an object whose
// fields hold values — so it is a `ref choice`: an identity-carrying tagged union whose
// cases can recurse through each other (an array holds a `List<Json>`, and so on).
//
// `stringify` is the whole point: one `match` over the six cases, each arm building its
// own text, the array/object arms recursing back into `stringify`. This is the canonical
// "interpreter over an AST" shape — `match` for dispatch, recursion for structure, a
// `StringBuilder` for the O(n) join, string interpolation for the leaves.
// ═════════════════════════════════════════════════════════════════════════════

// One key/value entry of an object. A plain value `data` — copied by value, no identity.
data Field {
    key: string
    value: Json
}

// The recursive value type. `ref choice` = abstract base + one sealed subclass per case;
// the cases reference `Json` (and `List<Json>`) freely because each case is a real class.
ref choice Json {
    jnull
    jbool(value: bool)
    jnum(value: double)
    jstr(value: string)
    jarr(items: List<Json>)
    jobj(fields: List<Field>)
}

// Serialize any value to its JSON text. Exhaustive `match` — every case is handled, so
// the compiler needs no trailing fallback. Each single-payload case binds its payload
// *transparently*: in `.jbool(b)` the name `b` IS the bool, in `.jarr(items)` `items` IS
// the `List<Json>` — the case view unwraps to the payload value (and `b.value` /
// `items.Count` still work). The array/object arms walk their collection and recurse.
//
// The transparent binding is pure SUGAR. A single-payload arm `.jbool(b) { … b … }` is
// exactly the case view `.jbool(c) { … c.value … }` with the projection elided — both
// lower to the identical IL (cast to the variant subclass, then load the one payload
// field). So `.jbool(b)` and `.jbool(c)` + `c.value` are interchangeable; the bare name
// is just the common case spelled shorter. (A multi-payload case has no single value to
// unwrap to, so it keeps the explicit view: `.jobj(c)` then `c.fields`.)
func stringify(j: Json) -> string {
    match j {
        .jnull       { return "null" }
        .jbool(b)    { return b ? "true" : "false" }
        .jnum(n)     { return "{n}" }
        .jstr(s)     { return "\"{s}\"" }
        .jarr(items) {
            let sb = StringBuilder()
            sb.Append("[")
            var i = 0
            while i < items.Count {
                if i > 0 { sb.Append(",") }
                sb.Append(stringify(items[i]))       // recurse into each element
                i += 1
            }
            sb.Append("]")
            return sb.ToString()
        }
        .jobj(fields) {
            let sb = StringBuilder()
            sb.Append("{")
            var i = 0
            while i < fields.Count {
                let f = fields[i]
                if i > 0 { sb.Append(",") }
                sb.Append("\"{f.key}\":")
                sb.Append(stringify(f.value))        // recurse into each value
                i += 1
            }
            sb.Append("}")
            return sb.ToString()
        }
    }
}

// Build a small document and render it:  {"name":"ada","tags":["math","engine"],"active":true}
func main() -> string {
    let tags = List<Json>()
    tags.Add(Json.jstr("math"))
    tags.Add(Json.jstr("engine"))

    let fields = List<Field>()
    fields.Add(Field { key: "name", value: Json.jstr("ada") })
    fields.Add(Field { key: "tags", value: Json.jarr(tags) })
    fields.Add(Field { key: "active", value: Json.jbool(true) })

    return stringify(Json.jobj(fields))
}