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

namespace Demo

// ═════════════════════════════════════════════════════════════════════════════
// A vending machine — a small stateful protocol, and the one place E# reaches for
// the object world on purpose.
//
// The machine HAS IDENTITY: there is one of it, money accumulates in it, stock
// depletes from it, and every command acts on that same evolving thing. That is the
// definition of `ref data` — a class with reference semantics — as opposed to the
// value `data` used elsewhere in this corpus. Commands arrive as a `choice` (insert a
// coin, buy, cancel) and are dispatched with `match`. Coins are an `enum` with
// explicit denominations, decoded by a second `match`. Anything the user can get
// wrong (too little credit, sold out) is a `Result`, so the caller always gets a
// clear outcome instead of a silent failure.
// ═════════════════════════════════════════════════════════════════════════════

// Coin denominations, in cents. An `enum` emits as a real CLR enum; the explicit
// values are the actual coin worth.
enum Coin {
    nickel  = 5
    dime    = 10
    quarter = 25
}

// Decode a coin to its cent value. `match` over an enum needs the type named so the
// `.nickel` shorthand resolves to `Coin`.
func cents(c: Coin) -> int {
    match (c: Coin) {
        .nickel  { return 5 }
        .dime    { return 10 }
        .quarter { return 25 }
    }
    return 0
}

// The three things a customer can do. A `choice`: `insert` carries which coin; the
// others carry nothing.
choice Command {
    insert(coin: Coin)
    buy
    cancel
}

// The machine itself — a `ref data`, because it has identity and evolving state.
// `var` fields mutate in place; `price` is fixed at construction.
ref data Machine {
    var credit: int
    var stock: int
    let price: int

    init(stock: int, price: int) {
        self.credit = 0
        self.stock = stock
        self.price = price
    }
}

// Apply one command to the machine, mutating it and reporting the outcome. Promoted
// onto `Machine` (first parameter), so the caller writes `machine.apply(cmd)`. Each
// arm reads/writes the shared state through the reference — the changes persist
// across calls because a `ref data` is one object, not a copy.
func apply(m: Machine, cmd: Command) -> Result<string, string> {
    match cmd {
        .insert(coin) {
            m.credit += cents(coin)               // coin IS the Coin (transparent view)
            return ok("credit: {m.credit}c")
        }
        .buy {
            if m.stock == 0 {
                return error("sold out")
            }
            if m.credit < m.price {
                return error("need {m.price - m.credit}c more")
            }
            let change = m.credit - m.price
            m.credit = 0                          // bank the price, return the rest
            m.stock -= 1
            return ok("dispensed — change {change}c, {m.stock} left")
        }
        .cancel {
            let refund = m.credit
            m.credit = 0
            return ok("refunded {refund}c")
        }
    }
}

// A short session against ONE machine: the mutations accumulate because `m` is a
// single identity-bearing object, not re-copied each call. Two quarters + a dime is
// 60c against a 50c price → dispensed with 10c change.
// The application is itself a `ref data` — `Program` OWNS the machine and drives the
// session in `main`. A `main` method on a `ref data Program` IS the program's entry
// point (the class-style alternative to a bare top-level `func main`); the compiler
// constructs the program (`Program()`) and calls `.main()`, so no launcher is needed.
ref data Program {
    func main() -> string {
        let m = Machine(3, 50)                // 3 items, 50c each

        m.apply(Command.insert(Coin.quarter())) // credit 25
        m.apply(Command.insert(Coin.quarter())) // credit 50
        m.apply(Command.insert(Coin.dime()))    // credit 60

        let result = m.apply(Command.buy())     // dispense, 10c change, 2 left
        return result.IsOk ? result.Value : "error: {result.Error}"
    }
}