LARA

Evaluating Postfix and its Correctness

sealed abstract class Expr
case class Var(varID: String) extends Expr
case class IntLiteral(value: Int) extends Expr
case class Plus(lhs: Expr, rhs: Expr) extends Expr
case class Times(lhs: Expr, rhs: Expr) extends Expr
 
sealed abstract class Token
case class ID(str : String) extends Token
case class Const(c : Int) extends Token
case class Add extends Token
case class Mul extends Token
 
object Print {
  def postfix(e : Expr) : List[Token] = e match {
    case Var(id)        => List(ID(id))
    case IntLiteral(c)  => List(Const(c))
    case Plus(lhs,rhs)  => postfix(lhs) ::: postfix(rhs) ::: List(Add())
    case Times(lhs,rhs) => postfix(lhs) ::: postfix(rhs) ::: List(Mul())
  }
}
object Eval {
  // recursive interpretation of expression
  def infix(env : Map[String,Int], expr : Expr) : Int = expr match {
    case Var(id)       => env(id)
    case IntLiteral(v) => v
    case Plus(e1,e2)   => infix(env,e1) + infix(env,e2)
    case Times(e1,e2)  => infix(env,e1) * infix(env,e2)
  }
 
  // non-recursive evaluation of postfix expression
  def postfix(env   : Map[String,Int],
              pexpr : Array[Token]) : Int = {
    var stack : Array[Int] = new Array[Int](512)
    var top : Int = 0
    var pos : Int = 0
 
    while (pos < pexpr.length) {
      pexpr(pos) match {
	case ID(v) => 
	  top = top + 1
	  stack(top) = env(v)
	case Const(c) =>
	  top = top + 1
	  stack(top) = c
	case Add() =>
	  stack(top - 1) = stack(top - 1) + stack(top)
	  top = top - 1
	case Mul() =>
	  stack(top - 1) = stack(top - 1) * stack(top)
	  top = top - 1
      }
      pos = pos + 1
    }
    return stack(top)
  }
}
object Test {
  def main(args : Array[String]) = {
    val expr = Plus(Var("x"),Times(Var("y"),Var("z")))
    val env = Map("x"->3, "y"->4, "z"->5)
    println("env = " + env)
    val resInterpreted = Eval.infix(env,expr)    
    println("resInterpreted = " + resInterpreted)
 
    val pexpr : Array[Token] = Print.postfix(expr).toArray
    println("postfix: " + (pexpr.toList))
    val resCompiled = Eval.postfix(env,pexpr)
    println("resCompiled = " + resCompiled)
 
    val theoremHolds = 
      (Eval.postfix(env,Print.postfix(expr).toArray) == 
       Eval.infix(env,expr))
 
    println("theoremHolds (for this case) = " + theoremHolds)
  }
}