/* Expression compiler correctness.
Viktor Kuncak and Filip Maric
*/
import leon.Utils._
import leon.Annotations._
object ExpressionCompiler {
sealed abstract class Sign
case class NUM(x : Int) extends Sign
case object PLUS extends Sign
sealed abstract class List
case class Cons(head : Sign, tail : List) extends List
case class Nil() extends List
def single(x: Sign) = Cons(x, Nil())
sealed abstract class Expr
case class Num(x: Int) extends Expr
case class Plus(e1: Expr, e2: Expr) extends Expr
def eval(e: Expr) : Int = {
e match {
case Num(x) => x
case Plus(e1, e2) => eval(e1) + eval(e2)
}
}
def postfixAcc(e : Expr, acc : List) : List = {
e match {
case Num(x) => Cons(NUM(x),acc)
case Plus(e1, e2) => postfixAcc(e1, postfixAcc(e2, Cons(PLUS, acc)))
}
}
sealed abstract class Stack
case class Empty extends Stack
case class Push(i: Int, s: Stack) extends Stack
def run(l:List, s: Stack) : Stack = {
l match {
case Nil() => s
case Cons(NUM(x), ss) => run(ss, Push(x, s))
case Cons(PLUS, ss) => s match {
case Push(a, Push(b, s1)) => run(ss, (Push(a + b, s1)))
case _ => Empty()
}
}
}
// note: no 'holds', it would not work directly
def run_lemma(e: Expr, ss: List, stack: Stack) = {
run(postfixAcc(e, ss), stack) == run(ss, Push(eval(e), stack))
}
// we express induction with generalization using appropriate recursion
def run_lemma_induct(e: Expr, ss: List, stack: Stack) : Boolean = {
e match {
case Num(x) => run_lemma(e, ss, stack)
case Plus(e1, e2) => run_lemma(e, ss, stack) &&
run_lemma_induct(e1, postfixAcc(e2, Cons(PLUS, ss)), stack) &&
run_lemma_induct(e2, Cons(PLUS,ss), Push(eval(e1), stack))
}
} holds
// inlining is crucial to knowing that property was proved
// proof hints are expressed as extra conjuncts
def test_run_lemma(e: Expr, ss: List, stack: Stack) = {
run_lemma_induct(e, ss, stack) &&
run(postfixAcc(e, ss), stack) == run(ss, Push(eval(e), stack))
} holds
// thanks to first conjunct, this now works
def thm(e: Expr) = {
test_run_lemma(e,Nil(),Empty()) &&
run(postfixAcc(e, Nil()), Empty()) == Push(eval(e), Empty())
} holds
}