STLC-like interpreted language in Lean 4

STLCBool.lean

import Batteries.Data.RBMap

inductive BinOp where
| add | sub | mul | div
deriving Repr, Ord

-- Abstrct Syntax Tree
inductive Expr where
| bool (value : Bool)
| num (value : Int)
| var (name : String)
| if_ (cond : Expr) (conseq : Expr) (alt : Expr)
| let_ (name : String) (value : Expr) (body : Expr)
| binop (op : BinOp) (lhs : Expr) (rhs : Expr)
| read
deriving Repr, Ord

abbrev Context := Batteries.RBMap String Expr compare

namespace Expr

partial def interpret (expr : Expr) (ctx : Context) : IO Expr :=
  match expr with
  | t@(num _) | t@(bool _) => pure t
  | var name =>
    match ctx.find? name with
    | none => throw (IO.userError s!"unbound variable: '{name}'")
    | some value => value.interpret ctx
  | let_ name value body => body.interpret (ctx.insert name value)
  | read => do
    let stdin ← IO.getStdin
    let n ← stdin.getLine
    pure (num n.toInt!)
  | if_ cond conseq alt => do
    let cond' ← cond.interpret ctx
    match cond' with
    | bool p => if p then conseq.interpret ctx else alt.interpret ctx
    | t => throw (IO.userError s!"type error: expected 'bool', got '{repr t}'")
  | binop op lhs rhs =>
    match op with
    | .add => do
      let lr ← lhs.interpret ctx
      let rr ← rhs.interpret ctx
      match (lr, rr) with
      | (num l, num r) => pure (num (l + r))
      | t => throw (IO.userError s!"type error: expected '(num, num)', got '{repr t}'")
    | .sub => do
      let lr ← lhs.interpret ctx
      let rr ← rhs.interpret ctx
      match (lr, rr) with
      | (num l, num r) => pure (num (l - r))
      | t => throw (IO.userError s!"type error: expected '(num, num)', got '{repr t}'")
    | .mul => do
      let lr ← lhs.interpret ctx
      let rr ← rhs.interpret ctx
      match (lr, rr) with
      | (num l, num r) => pure (num (l * r))
      | t => throw (IO.userError s!"type error: expected '(num, num)', got '{repr t}'")
    | .div => do
      let lr ← lhs.interpret ctx
      let rr ← rhs.interpret ctx
      match (lr, rr) with
      | (num l, num r) => pure (num (l / r))
      | t => throw (IO.userError s!"type error: expected '(num, num)', got '{repr t}'")

open BinOp in
def program : Expr := (binop add (num 41) (num 1))

#eval program.interpret .empty

open BinOp in
def programWithVars : Expr := (let_ "x" (num 4) (binop div (var "x") (num 2)))

#eval programWithVars.interpret .empty

open BinOp in
def programWithBranches : Expr :=
  let_ "x" (num 2)
    (let_ "pred" (bool true)
      (if_ (var "pred") (binop add (var "x") (num 1)) (var "x")))

#eval programWithBranches.interpret .empty

end Expr