Commit 996cbd49 authored by Heiko Becker's avatar Heiko Becker

Fix some bugs, add more verbose debug testing of certificates

parent 491610b9
(* First unfold all! definitions to the definitions known to the kernel
then remove all! conditionals using the conditional rewriting conversion
then get rid of all conditionals using NUM_REDUCE_CONV (TODO: What about equivalence of constants?)
then remove all let bindings
then simplify projections
then finally evaluate all rational functions until you arrive at true or false
*)
let Checker_Rewrites =
[CertificateChecker;validIntervalbounds; validErrorbound;
maxAbsFun; isSupersetInterval; multInterval; subtractInterval;
addInterval; absIntvUpd; min4; max4; machineEpsilon; IVlo; IVhi];;
let DistinctnessAndInjectivity = [distinctness "exp"; injectivity "exp"; distinctness "binop"];;
let DAISY_CONV theRewrites term =
let allRewrites = List.concat [Checker_Rewrites; theRewrites; DistinctnessAndInjectivity] in
let unfolded_defs = REWRITE_CONV allRewrites term in
let no_conditionals = CONV_RULE CONDS_ELIM_CONV unfolded_defs in
let evaluated_conditions =
CONV_RULE
(REPEATC
(CHANGED_CONV
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV NUM_REDUCE_CONV THENC TRY_CONV REAL_RAT_RED_CONV))))) no_conditionals in
let no_lets = CONV_RULE ((REPEATC (CHANGED_CONV (ONCE_DEPTH_CONV let_CONV))) THENC SIMP_CONV[FST;SND]) evaluated_conditions in
CONV_RULE
(REPEATC
(CHANGED_CONV
(ONCE_DEPTH_CONV
(CHANGED_CONV
(TRY_CONV REAL_RAT_ABS_CONV
THENC TRY_CONV REAL_RAT_MAX_CONV
THENC TRY_CONV REAL_RAT_MIN_CONV
THENC TRY_CONV REAL_RAT_RED_CONV
)
)
)
)
) no_lets;;
......@@ -54,9 +54,16 @@ object CertificatePhase extends DaisyPhase {
//the analysis result function
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, prv)
//generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
//val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
//compose the strings
val certificateText = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n" + analysisResultText + "\n\n" + functionCall
val textWithoutFCall = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n" + analysisResultText
val certificateText =
if (prv == "coq")
textWithoutFCall + "\n\n" + functionCall
else
textWithoutFCall + "let theRewrites = [thePrecondition;absenv;" + holExpList(theBody.get) + "];;" + "\n" + functionCall
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
case None => reporter.fatalError ("No Precondition specified")
......@@ -80,20 +87,18 @@ object CertificatePhase extends DaisyPhase {
if (prover == "coq")
"Require Import Daisy.CertificateChecker."
else
"needs \"CertificateChecker.hl\";;"
"needs \"CertificateChecker.hl\";;\nneeds \"Infra/convs.hl\";;"
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theValue = s"Definition $vname :nat := $id.\n"
val theExpr = s"Definition ExpVar$vname :exp Q := Param Q $vname.\n"
(theValue + theExpr,s"ExpVar$vname")
val theExpr = s"Definition ExpVar$vname :exp Q := Param Q $id.\n"
(theExpr,s"ExpVar$vname")
}
private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theValue = s"let $vname = define `$vname:num = $id`;;\n"
val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Param $vname`;;\n"
(theValue + theExpr, s"ExpVar$vname")
val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Param $id`;;\n"
( theExpr, s"ExpVar$vname")
}
private def coqConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
......@@ -101,19 +106,18 @@ object CertificatePhase extends DaisyPhase {
case RealLiteral(v) =>
val rationalStr = v.toFractionString
val coqRational = rationalStr.replace('/','#')
val theValue = s"Definition cst$id :Q := ${coqRational}.\n"
val theExpr = s"Definition ExpCst$id :exp Q := Const cst$id.\n"
(theValue + theExpr, s"ExpCst$id")
val theExpr = s"Definition ExpCst$id :exp Q := Const ($coqRational).\n"
(theExpr, s"ExpCst$id")
}
private def holConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
r match {
case RealLiteral(v) =>
val rationalStr = v.toFractionString
val holRational = rationalStr.replace("(","(&")
val theValue = s"let cst$id = define `cst$id:real = ${holRational}`;;\n"
val theExpr = s"let ExpCst$id = define `ExpCst$id:(real)exp = Const cst$id`;;\n"
(theValue + theExpr, s"ExpCst$id")
val ratTmp = rationalStr.replace("(","(&")
val holRational = ratTmp.replace("&-","-- &")
val theExpr = s"let ExpCst$id = define `ExpCst$id:(real)exp = Const ($holRational)`;;\n"
(theExpr, s"ExpCst$id")
}
private def coqBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
......@@ -140,7 +144,7 @@ object CertificatePhase extends DaisyPhase {
("let Sub"+ nameLHS + nameRHS + " = define `Sub"+ nameLHS + nameRHS + s":(real)exp = Binop Sub $nameLHS $nameRHS`;;\n",
"Sub"+ nameLHS + nameRHS)
case x @ Times(lhs, rhs) =>
("let Mult"+ nameLHS + nameRHS + " = define `Mul"+ nameLHS + nameRHS + s":(real)exp = Binop Mult $nameLHS $nameRHS`;;\n",
("let Mult"+ nameLHS + nameRHS + " = define `Mult"+ nameLHS + nameRHS + s":(real)exp = Binop Mult $nameLHS $nameRHS`;;\n",
"Mult"+ nameLHS + nameRHS)
case x @ _ =>
reporter.fatalError("Unsupported value")
......@@ -234,9 +238,11 @@ object CertificatePhase extends DaisyPhase {
private def holInterval(intv:(Rational,Rational)) :String =
intv match {
case (lowerBound, upperBound) =>
val lowerBoundHol = lowerBound.toFractionString.replace("(","(&")
val upperBoundHol = upperBound.toFractionString.replace("(","(&")
"( " + lowerBoundHol + ", " + upperBoundHol + ")"
val loTmp = lowerBound.toFractionString.replace("(","(&")
val hiTmp = upperBound.toFractionString.replace("(","(&")
val lo = loTmp.replace("&-","-- &")
val hi = hiTmp.replace("&-", "-- &")
"(" + lo + ", " + hi + ")"
}
private def coqPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
......@@ -380,15 +386,79 @@ object CertificatePhase extends DaisyPhase {
private def getAbsEnvDef (e:Expr, prv:String) :(String,String)=
if (prv == "coq")
("Definition absenv :analysisResult := fun (e:exp Q) =>\n"+ coqAbsEnv(e, "((0#1,0#1),0#1)") + ".",
("Definition absenv :analysisResult := \nfun (e:exp Q) =>\n"+ coqAbsEnv(e, "((0#1,0#1),0#1)") + ".",
"absenv")
else
("let absenv = define `absenv:analysisResult = \n" + holAbsEnv(e, "((&0,&1),&1)") + "`;;",
("let absenv = define `absenv:analysisResult = \n\\e. \n" + holAbsEnv(e, "((&0,&1),&1)") + "`;;",
"absenv")
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, prover:String) :String=
if (prover == "coq")
"Eval compute in CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "."
else
"DEPTH_CONV `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
"DAISY_CONV theRewrites `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
private def getAllComputeExps (e:Expr, analysisResultName:String,precondName:String, prover:String) :String=
{
val nameE = expressionNames(e)
if (prover == "coq"){
e match {
case x @ Variable(id) =>
"Eval compute in CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + ".\n"
case x @ RealLiteral(r) =>
"Eval compute in CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + ".\n"
case x @ Plus(lhs, rhs) =>
getAllComputeExps (lhs, analysisResultName, precondName, prover) +
getAllComputeExps (rhs, analysisResultName, precondName, prover) +
"Eval compute in CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + ".\n"
case x @ Minus(lhs, rhs) =>
getAllComputeExps (lhs, analysisResultName, precondName, prover) +
getAllComputeExps (rhs, analysisResultName, precondName, prover) +
"Eval compute in CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + ".\n"
case x @ Times(lhs, rhs) =>
getAllComputeExps (lhs, analysisResultName, precondName, prover) +
getAllComputeExps (rhs, analysisResultName, precondName, prover) +
"Eval compute in CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + ".\n"
case x @ _ =>
"" //TODO Can this happen?
}
}
else
"DAISY_CONV theRewrites `CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + "`;;"
}
private def holExpList (e:Expr) :String =
{
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
nameE
case x @ RealLiteral(r) =>
nameE
case x @ Plus(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
nameE
case x @ Minus(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
nameE
case x @ Times(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
nameE
case x @ _ =>
"" //TODO Can this happen?
}
}
}
......@@ -329,7 +329,8 @@ trait ErrorFunctions {
case x @ RealLiteral(r) =>
val range = rangeFromReal(r)
val error = if (isExactInFloats(r) || !trackRoundoffErrs) {
// was: isExactInFloats(r) || !trackRoundoffErrs)
val error = if (!trackRoundoffErrs) {
zeroError
} else {
fromError(uniformPrecision.absRoundoff(r))
......
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