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

namespace Demo

// ═════════════════════════════════════════════════════════════════════════════
// A tiny stack machine — the smallest thing that is honestly a "virtual machine".
//
// A program is a list of instructions; execution is a loop that walks them, each
// one pushing to or popping from an operand stack. This is how real bytecode VMs
// (the CLR's own, the JVM, CPython, Lua) work underneath — just with more opcodes.
//
// The instruction set is a `choice` (a value tagged union): some variants carry a
// payload (`push` carries the integer to push), most carry none (`add`, `dup`, …).
// Executing one instruction is a `match` over the variant — the canonical use of a
// sum type. The operand stack is a `List<int>` used as a LIFO: `Add` is push,
// `xs[xs.Count - 1]` is peek, `RemoveAt(xs.Count - 1)` is pop — a `List<T>` from the
// BCL, called directly. Anything that can fail (popping an empty stack, dividing by
// zero, leaving the wrong number of results) is a `Result`, threaded with `?`.
// ═════════════════════════════════════════════════════════════════════════════

// The instruction set. `push` is the only variant with a payload.
choice Op {
    push(value: int)
    add
    sub
    mul
    div
    dup        // duplicate the top of the stack
    swap       // exchange the top two
}

// Pop the top of the stack, or fail on underflow. Takes `*List<int>`... actually a
// `List<int>` is already a reference type, so it is passed and mutated directly — no
// pointer needed. Returns the popped value (or an error), leaving the list shorter.
func pop(stack: List<int>) -> Result<int, string> {
    if stack.Count == 0 {
        return error("stack underflow")
    }
    let top = stack[stack.Count - 1]
    stack.RemoveAt(stack.Count - 1)
    return ok(top)
}

// Execute one instruction against the stack. `match` covers every variant, so the
// dispatch is exhaustive; each arm either pushes, or pops its operands (with `?`
// propagating an underflow) and pushes the result. Single-payload `push` binds its
// value transparently — `n` IS the int.
func step(stack: List<int>, op: Op) -> Result<int, string> {
    match op {
        .push(n) { stack.Add(n) }
        .add {
            let b = pop(stack)?
            let a = pop(stack)?
            stack.Add(a + b)
        }
        .sub {
            let b = pop(stack)?
            let a = pop(stack)?
            stack.Add(a - b)
        }
        .mul {
            let b = pop(stack)?
            let a = pop(stack)?
            stack.Add(a * b)
        }
        .div {
            let b = pop(stack)?
            let a = pop(stack)?
            if b == 0 {
                return error("division by zero")
            }
            stack.Add(a / b)
        }
        .dup {
            let top = pop(stack)?
            stack.Add(top)
            stack.Add(top)
        }
        .swap {
            let b = pop(stack)?
            let a = pop(stack)?
            stack.Add(b)
            stack.Add(a)
        }
    }
    return ok(0)        // step's value is unused; it reports success or the error
}

// Run a whole program: step through every instruction, then require exactly one value
// left on the stack — that's the result. Too many or too few is a program error, not a
// silent answer.
func run(program: List<Op>) -> Result<int, string> {
    let stack = List<int>()
    var i = 0
    while i < program.Count {
        step(stack, program[i])?      // propagate the first runtime error
        i += 1
    }
    if stack.Count != 1 {
        return error("program left {stack.Count} values on the stack, expected 1")
    }
    return ok(stack[0])
}

// Build and run:  (2 + 3) * (10 - 6)  ==  5 * 4  ==  20
//   push 2, push 3, add        → stack [5]
//   push 10, push 6, sub       → stack [5, 4]
//   mul                        → stack [20]
// The entry point lives on a `ref data Program` — the OO "an object IS the application"
// shape, the class-style alternative to a bare top-level `func main`. A `main` method on
// a `ref data Program` IS the program's entry point; the compiler constructs the program
// (`Program()`) and calls `.main()`, so no separate launcher function is needed.
ref data Program {
    func main() -> int {
        let program = List<Op>()
        program.Add(Op.push(2))
        program.Add(Op.push(3))
        program.Add(Op.add())
        program.Add(Op.push(10))
        program.Add(Op.push(6))
        program.Add(Op.sub())
        program.Add(Op.mul())

        let r = run(program)
        return r.IsOk ? r.Value : -1      // 20
    }
}