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

namespace Demo

// ═════════════════════════════════════════════════════════════════════════════
// Value vs. shared — the heart of E#'s memory model, and what `new` is for.
//
// A `data` type is a VALUE, like an int. Assigning it COPIES; two variables holding a
// `data` never affect each other. That is the default, and it is usually what you
// want — no spooky action at a distance.
//
// Sometimes you need the opposite: several places that read and write ONE shared
// piece of state (a counter threaded through a computation, a node in a linked
// structure). For that you put the `data` on the heap with `new`, which yields a
// POINTER, written `*T`. Everyone holding the `*T` sees the same mutations.
//
//   `new Counter { ... }`   →   allocate on the heap, hand back a `*Counter`
//   `c: *Counter`           →   a pointer; `c.total` reads/writes the shared cell
//   `let alias = c`         →   copies the POINTER, not the counter — same object
//
// `new` is exactly "put this value on the heap and give me a pointer to it". It is
// the one allocation expression in the language and the only way to mint a fresh `*T`.
// ═════════════════════════════════════════════════════════════════════════════

// A plain value `data`: a running tally. No `init` block — value types are built with
// a composite literal that names each field (`Counter { total: 0, steps: 0 }`).
data Counter {
    var total: int
    var steps: int
}

// `bump` takes a POINTER (`*Counter`), so it mutates the caller's counter in place.
// A pointer parameter stays a free function (only a direct-value receiver like
// `func f(c: Counter)` would become the method `c.f()`).
func bump(c: *Counter, amount: int) {
    c.total += amount
    c.steps += 1
}

// Had this taken a value `Counter` instead of `*Counter`, `add` would receive its own
// COPY and the caller would never see the change. The pointer is what makes the
// sharing real.
// Optional: You can annotate return type as void if you prefer visibility.
func addAll(c: *Counter, xs: List<int>) -> void {
    for x in xs {
        bump(c, x)
    }
}

func main() -> int {
    // `new` allocates the counter on the heap and returns a *Counter. `tally` and
    // `alias` are then two NAMES for the SAME heap counter.
    var tally: *Counter = new Counter { total: 0, steps: 0 }
    let alias = tally

    let xs = List<int>()
    xs.Add(5)
    xs.Add(7)
    xs.Add(3)

    addAll(tally, xs)      // through the pointer: total = 15, steps = 3
    bump(alias, 100)       // through the OTHER name — same object: total = 115, steps = 4

    // The writes via `alias` are visible through `tally` — both point at one heap cell.
    // Read the shared fields back through the pointer (auto-deref): total = 115, steps = 4.
    return tally.total + tally.steps    // 119
}