Commit dd47e465 authored by Heiko Becker's avatar Heiko Becker

Simplify abstract environment generation and fix bug that would omit parts,...

Simplify abstract environment generation and fix bug that would omit parts, when a unary operator is encountered
parent 3c56e1a6
......@@ -73,7 +73,7 @@ object CertificatePhase extends DaisyPhase {
getPrecondFunction(pre, fnc.id.toString, reporter, prv)
//the analysis result function
val (analysisResultText, analysisResultName) =
getAbsEnvDef(theBody.get, errorMap, rangeMap, fnc.id.toString, prv)
getAbsEnvDef(theBody.get, errorMap, rangeMap, fnc.id.toString, prv, reporter)
//generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,fnc.id.toString,prv)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
......@@ -469,13 +469,13 @@ object CertificatePhase extends DaisyPhase {
"then " + thenC + "\n" +
"else " + elseC
private def coqAbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
private def coqAbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String, reporter:Reporter) :String =
{
// 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 expFun = coqAbsEnv (exp, errorMap, rangeMap, cont, reporter)
val gFun = coqAbsEnv (g, errorMap, rangeMap, expFun, reporter)
val intvY = coqInterval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable (y)).toFractionString.replace("/","#")
val nameY = expressionNames(Variable(y))
......@@ -488,76 +488,52 @@ object CertificatePhase extends DaisyPhase {
val nameE = expressionNames(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)
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
case x @ _ =>
"" //TODO Can this happen?
val continuation =
e match {
case x @ Variable(id) => cont
case x @ RealLiteral(r) => cont
case x @ Plus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont, reporter)
coqAbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont, reporter)
coqAbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont, reporter)
coqAbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ Division(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont, reporter)
coqAbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ UMinus(e) =>
coqAbsEnv (e, errorMap, rangeMap, cont, reporter)
case x @ _ =>
reporter.fatalError(s"Unsupported operation $e")
}
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
continuation)
}
}
private def hol4AbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
private def hol4AbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String, reporter:Reporter) :String =
{
e match {
case x @ Let (y,exp, g) =>
val expFun = hol4AbsEnv (exp, errorMap, rangeMap, cont)
val gFun = hol4AbsEnv (g, errorMap, rangeMap, expFun)
val expFun = hol4AbsEnv (exp, errorMap, rangeMap, cont, reporter)
val gFun = hol4AbsEnv (g, errorMap, rangeMap, expFun, reporter)
val intvY = hol4Interval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable (y)).toFractionString
val nameY = expressionNames(Variable(y))
......@@ -570,66 +546,41 @@ object CertificatePhase extends DaisyPhase {
val nameE = expressionNames(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 + ")",
rFun)
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)
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
val continuation =
e match {
case x @ Variable(id) => cont
case x @ RealLiteral(r) => cont
case x @ Plus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont, reporter)
hol4AbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ Minus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont, reporter)
hol4AbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont, reporter)
hol4AbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ Division(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont, reporter)
hol4AbsEnv (rhs, errorMap, rangeMap, lFun, reporter)
case x @ UMinus(e) =>
hol4AbsEnv (e, errorMap, rangeMap, cont, reporter)
case x @ _ =>
"" //TODO Can this happen?
reporter.fatalError(s"Unsupported operation $e")
}
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
continuation)
}
}
......@@ -693,14 +644,14 @@ object CertificatePhase extends DaisyPhase {
}
}
private def getAbsEnvDef (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], fName:String, prv:String) :(String,String)=
private def getAbsEnvDef (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], fName:String, prv:String, reporter:Reporter) :(String,String)=
if (prv == "coq")
(s"Definition absenv_${fName} :analysisResult := \nfun (e:exp Q) =>\n" +
coqAbsEnv(e, errorMap, rangeMap, "((0#1,0#1),0#1)") + ".",
coqAbsEnv(e, errorMap, rangeMap, "((0#1,0#1),0#1)", reporter) + ".",
s"absenv_${fName}")
else if (prv == "hol4")
(s"val absenv_${fName}_def = Define `\n absenv_${fName}:analysisResult = \n\\e. \n" +
hol4AbsEnv(e, errorMap, rangeMap, "((0,1),1)") + "`;",
hol4AbsEnv(e, errorMap, rangeMap, "((0,1),1)", reporter) + "`;",
s"absenv_${fName}")
else
("let absenv = define `absenv:analysisResult = \n\\e. \n" +
......
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