Commit 12dd5cf1 authored by Heiko Becker's avatar Heiko Becker

Remove getOrElse by simplifyung computation

parent f5e323af
......@@ -442,158 +442,168 @@ object CertificatePhase extends DaisyPhase {
"else " + elseC
private def coqAbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
//FIXME: Only happens for let Bindings!
val nameE = expressionNames.getOrElse(e,"FOO")
e match {
case x @ Variable(id) =>
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ RealLiteral(r) =>
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Plus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Division(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Let (y,exp, g) =>
val expFun = coqAbsEnv (exp, errorMap, rangeMap, cont)
val gFun = coqAbsEnv (g, errorMap, rangeMap, expFun)
val intvY = coqInterval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable (y)).toFractionString.replace("/","#")
val nameY = expressionNames(Variable(y))
conditional (
s"( expEqBool e (Var Q ${identifierNums(y)}) )",
"(" + intvY + ", " + errY + ")",
gFun)
case x @ _ =>
"" //TODO Can this happen?
}
{
// Let bindings do not have names, so these are a special case here:
e match {
case x @ Let (y,exp, g) =>
val expFun = coqAbsEnv (exp, errorMap, rangeMap, cont)
val gFun = coqAbsEnv (g, errorMap, rangeMap, expFun)
val intvY = coqInterval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable (y)).toFractionString.replace("/","#")
val nameY = expressionNames(Variable(y))
conditional (
s"( expEqBool e (Var Q ${identifierNums(y)}) )",
"(" + intvY + ", " + errY + ")",
gFun)
case x @ _ =>
val nameE = expressionNames.get(e)
e match {
case x @ Variable(id) =>
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ RealLiteral(r) =>
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Plus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Division(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = coqAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ _ =>
"" //TODO Can this happen?
}
}
}
private def hol4AbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
// see coqAbsenv
val nameE = expressionNames.getOrElse(e,"FOO")
e match {
case x @ Variable(id) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ RealLiteral(r) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Plus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Minus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
lFun)
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Division(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Let (y,exp, g) =>
val expFun = hol4AbsEnv (exp, errorMap, rangeMap, cont)
val gFun = hol4AbsEnv (g, errorMap, rangeMap, expFun)
val intvY = hol4Interval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable (y)).toFractionString
val nameY = expressionNames(Variable(y))
conditional (
s"( e = Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
gFun)
private def hol4AbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
e match {
case x @ _ =>
"" //TODO Can this happen?
}
case x @ Let (y,exp, g) =>
val expFun = hol4AbsEnv (exp, errorMap, rangeMap, cont)
val gFun = hol4AbsEnv (g, errorMap, rangeMap, expFun)
val intvY = hol4Interval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable (y)).toFractionString
val nameY = expressionNames(Variable(y))
conditional (
s"( e = Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
gFun)
case x @ _ =>
val nameE = expressionNames.get(e)
e match {
case x @ Variable(id) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ RealLiteral(r) =>
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
case x @ Plus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Minus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
lFun)
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ Division(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = hol4AbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
rFun)
case x @ _ =>
"" //TODO Can this happen?
}
}
}
private def holLightAbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment