datatype Value = Bool(b: bool) | Int(x: int) | Error

datatype Expr =
  | Const(value: Value)
  | Var(name: string)
  | Plus(a: Expr, b: Expr)
  | ITE(cond: Expr, thn: Expr, els: Expr) // `if .. then .. else ..` expressions

type State = map<string, Value>

function Eval(e: Expr, st: State): Value
{
  match e
  case Const(value) => value
  case Var(name) =>
    if name in st then st[name] else Error
  case Plus(a, b) =>
    var aa, bb := Eval(a, st), Eval(b, st);
    match (aa, bb) {
      case (Int(x), Int(y)) => Int(x + y)
      case _ => Error
    }
  case ITE(cond, thn, els) =>
    match Eval(cond, st) {
      case Bool(b) => Eval(if b then thn else els, st)
      case _ => Error
    }
}

// There are two types.
datatype Type = TBool | TInt

// A value is *good* for a given type if the value has that type.
predicate GoodValue(v: Value, ty: Type) {
  || (v.Bool? && ty == TBool)
  || (v.Int? && ty == TInt)
}

// A typing environment is a map from variable names to types.
type Environment = map<string, Type>

// We consider an expression to have a given type only if all its variables are used
// in ways consistent with their types.
predicate HasType(e: Expr, ty: Type, env: Environment) {
  match e
  case Const(value) =>
    GoodValue(value, ty)
  case Var(name) =>
    name in env && env[name] == ty
  case Plus(a, b) =>
    HasType(a, TInt, env) && HasType(b, TInt, env)
  case ITE(cond, thn, els) =>
    HasType(cond, TBool, env) && HasType(thn, ty, env) && HasType(els, ty, env)
}

// 1. Oops. Fix the bug in the `Plus` case of `HasType`!
//
// 2. Now fix this lemma that relates HasType, Eval, and GoodValue.
//    We assume `e` has type `ty` in environment `env`, but that alone does not
//       guarantee `e` evaluates to a good value of type `ty` in state `st`.
//    Dafny should be able to prove your lemma automatically:

lemma WellTypedExpressionEvaluatesToGoodValue(e: Expr, ty: Type, st: State, env: Environment)
  requires HasType(e, ty, env)
  ensures GoodValue(Eval(e, st), ty)
{
}