// Here are the same definitions we saw in the reading:

datatype Expr =
  | Const(value: int)
  | Var(name: string)
  | Plus(a: Expr, b: Expr)

type State = map<string, int>

// Let's try a different approach to handling expressions that
// refer to variables not defined in the state...

// The value of an Expr might be an int or it might be an *error*...
datatype Value = Int(value: int) | Error

function Eval(e: Expr, st: State): Value
{
  match e
  case Const(value) => Int(value)
  case Var(name) =>
    if name in st then
      Int(st[name])
    else // ... and evaluating an undefined variable is an error!
      Error
  case Plus(a, b) =>
    var avalue, bvalue := Eval(a, st), Eval(b, st);
    // 1. Complete the definition of Eval for Plus:
    ???
}

function FreeVars(e: Expr): set<string> {
  match e
  case Const(_) => {}
  case Var(name) => {name}
  case Plus(a, b) => FreeVars(a) + FreeVars(b)
}

// 2. State a useful lemma relating FreeVars, Eval, and errors.
//    Dafny should prove it automatically:
lemma SomethingSomethingEvalSomethingSomething(e: Expr, st: State)
  requires true
  ensures false
{
}