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

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

namespace Demo

// ═════════════════════════════════════════════════════════════════════════════
// Type narrowing & downcasting — the language form the in-house LSP needs to take an
// open symbol and discriminate it into its concrete kind. The shape is the LSP's own:
// a symbol table over a CLOSED `abstract class` hierarchy (a base you must subclass,
// sealed leaves you instantiate — E#'s base-or-sealed inheritance stance), dispatched
// with an exhaustive `match` type pattern and ZERO downcasts.
//
// `match s { (t: TypeSym) => … (m: MethodSym) => … }` is the whole point: each arm is an
// `isinst` test that binds the narrowed value, and because the hierarchy is closed the
// compiler checks every leaf is handled — add a leaf and every match that forgot it warns.
// A guard (`if m.isStatic`) refines an arm; the `=>` form is the value-producing body.
// ═════════════════════════════════════════════════════════════════════════════

// The closed hierarchy. `abstract class` is a base that must be subclassed; each leaf
// is a plain (sealed) `class`, constructed with its `init` and chaining `: base(...)`.
abstract class Sym {
    name: string
    init(n: string) { self.name = n }
}

class TypeSym : Sym {
    arity: int
    init(n: string, a: int) : base(n) { self.arity = a }
}

class MethodSym : Sym {
    isStatic: bool
    init(n: string, s: bool) : base(n) { self.isStatic = s }
}

class FieldSym : Sym {
    fieldType: string
    init(n: string, t: string) : base(n) { self.fieldType = t }
}

// One hover line per symbol kind — an exhaustive type-pattern match over the closed set.
// No `default`: the compiler knows Sym's leaves are TypeSym / MethodSym / FieldSym, so
// adding a fourth would light up this match. A guarded arm distinguishes static methods.
func (s: Sym) describe() -> string =
    match s {
        (t: TypeSym)                 => "type {t.name}/{t.arity}"
        (m: MethodSym) if m.isStatic => "static {m.name}"
        (m: MethodSym)               => "func {m.name}"
        (f: FieldSym)                => "{f.name}: {f.fieldType}"
    }

// The open-world fallback. When the value is genuinely an open `object` (the BCL boundary
// the LSP can't avoid), `is` / `as` / `as!` carry the narrowing: `is T` tests and
// smart-casts, `as T` yields `T?` and composes with `??`, `as!` asserts and throws.
func openKind(o: object) -> string {
    if o is Sym {
        // smart-cast: `o` is a `Sym` here, no rebind — dispatch through describe's match.
        // `describe` is a value-receiver method (its first parameter is `Sym`), so it is
        // called as a method on the narrowed value.
        return o.describe()
    }
    let n = o as int        // n : int? — the safe cast, composing with ??
    return "raw {n ?? -1}"
}

// The entry point — a `class Program` whose `main` IS the program (the compiler
// constructs it and calls `.main()`). Builds a few symbols and renders them.
class Program {
    func main() -> string {
        let symbols = List<Sym>()
        symbols.Add(TypeSym("Point", 0))
        symbols.Add(MethodSym("origin", true))
        symbols.Add(MethodSym("translate", false))
        symbols.Add(FieldSym("x", "int"))

        let sb = System.Text.StringBuilder()
        var i = 0
        while i < symbols.Count {
            if i > 0 { sb.Append("; ") }
            sb.Append(symbols[i].describe())
            i += 1
        }
        // …and the open-world path over a boxed primitive.
        sb.Append(" | ")
        let boxed: object = 42
        sb.Append(openKind(boxed))
        return sb.ToString()
    }
}