Commit b7f792ff authored by Heiko Becker's avatar Heiko Becker
Browse files

One file <=> One certificate, minor beautifications of certificates

parent a3a54a0f
......@@ -24,23 +24,30 @@ object CertificatePhase extends DaisyPhase {
val errorMap = ctx.resultAbsoluteErrors
val rangeMap = ctx.resultRealRanges
def writeToFile (fileContent:String, prover:String, fname:String){
def writeToFile (fileContent:String, prover:String){
import java.io.FileWriter
import java.io.BufferedWriter
val fileLocation =
if (prover == "coq")
"./coq/output/certificate_" + prg.id + "_" + fname + ".v"
"./coq/output/certificate_" + prg.id + ".v"
else
if (prover == "hol4")
"./hol4/output/certificate_" + prg.id + "_" + fname + "Script.sml"
"./hol4/output/certificate_" + prg.id + "Script.sml"
else
"./hol-light/output/certificate_" + prg.id + "_" + fname + ".hl"
"./hol-light/output/certificate_" + prg.id + ".hl"
val fstream = new FileWriter(fileLocation)
val out = new BufferedWriter(fstream)
out.write(fileContent)
out.close
}
var fullCertificate = "";
//First write the imports
val prelude = getPrelude(prover.get, "certificate_" + prg.id)
fullCertificate += prelude + "\n\n";
for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){
reporter.info(s"Generating certificate for ${fnc.id}")
val thePrecondition = fnc.precondition
......@@ -53,19 +60,19 @@ object CertificatePhase extends DaisyPhase {
case Some(prv) =>
thePrecondition match {
case Some (pre) =>
//First write the imports
val prelude = getPrelude(prv, "certificate_" + prg.id + "_" + fnc.id.toString)
//the definitions for the whole expression
val (theDefinitions, lastGenName) = getCmd(theBody.get,reporter,prv)
//generate the precondition
val (thePreconditionFunction, functionName) = getPrecondFunction(pre, reporter, prv)
val (thePreconditionFunction, functionName) =
getPrecondFunction(pre, fnc.id.toString, reporter, prv)
//the analysis result function
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, errorMap, rangeMap, prv)
val (analysisResultText, analysisResultName) =
getAbsEnvDef(theBody.get, errorMap, rangeMap, fnc.id.toString, prv)
//generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,fnc.id.toString,prv)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
//compose the strings
val textWithoutFCall = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n\n" + analysisResultText
val textWithoutFCall = theDefinitions + "\n\n" + thePreconditionFunction + "\n\n" + analysisResultText
val certificateText =
if (prv == "hol-light")
textWithoutFCall + "\n\n" + "let theRewrites = [thePrecondition;absenv;" + holLightExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
......@@ -74,13 +81,16 @@ object CertificatePhase extends DaisyPhase {
else
textWithoutFCall + "\n\n" + functionCall
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
//append the output to the global string
fullCertificate = fullCertificate + "\n\n\n" + certificateText
case None => reporter.fatalError ("No Precondition specified.")
}
case None => reporter.fatalError ("No theorem prover specified.")
}
}
//end iteration, write certificate
writeToFile(fullCertificate,prover.get)
(ctx, prg)
}
......@@ -98,13 +108,13 @@ object CertificatePhase extends DaisyPhase {
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theExpr = s"Definition ExpVar$vname :exp Q := Param Q $id.\n"
val theExpr = s"Definition ExpVar$vname :exp Q := Var Q $id.\n"
(theExpr,s"ExpVar$vname")
}
private def hol4Variable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theExpr = s"val ExpVar$vname = Define `ExpVar$vname:(real exp) = Param $id`;\n"
val theExpr = s"val ExpVar$vname = Define `ExpVar$vname:(real exp) = Var $id`;\n"
(theExpr, s"ExpVar$vname")
}
......@@ -368,9 +378,9 @@ object CertificatePhase extends DaisyPhase {
"(" + lo + ", " + hi + ")"
}
private def coqPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
private def coqPrecondition (ranges:Map [Identifier, (Rational, Rational)],fName:String) :(String, String) =
{
var theFunction = "Definition thePrecondition:precond := fun (n:nat) =>\n"
var theFunction = s"Definition thePrecondition_${fName}:precond := fun (n:nat) =>\n"
for ((id,intv) <- ranges) {
val ivCoq = coqInterval (intv)
//variable must already have a binder here!
......@@ -378,21 +388,21 @@ object CertificatePhase extends DaisyPhase {
theFunction += "if n =? " + identifierNums(id) + " then "+ ivCoq + " else "
}
theFunction += "(0#1,0#1)."
(theFunction, "thePrecondition")
(theFunction, s"thePrecondition_${fName}")
}
private def hol4Precondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
private def hol4Precondition (ranges:Map [Identifier, (Rational, Rational)],fName:String) :(String, String) =
{
var theFunction = "val thePrecondition_def = Define ` \n thePrecondition (n:num):interval = \n"
var theFunction = s"val thePrecondition_${fName}_def = Define ` \n thePrecondition${fName} (n:num):interval = \n"
for ((id,intv) <- ranges) {
val ivHolLight = hol4Interval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHolLight + " else "
}
theFunction += "(0,1)`;"
(theFunction, "thePrecondition")
(theFunction, s"thePrecondition${fName}")
}
private def holLightPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
private def holLightPrecondition (ranges:Map [Identifier, (Rational, Rational)],fName:String) :(String, String) =
{
var theFunction = "let thePrecondition = define ` \n thePrecondition (n:num) = \n"
for ((id,intv) <- ranges) {
......@@ -403,18 +413,18 @@ object CertificatePhase extends DaisyPhase {
(theFunction, "thePrecondition")
}
private def getPrecondFunction(pre:Expr,reporter:Reporter,prv:String) :(String,String) =
private def getPrecondFunction(pre:Expr,fName:String,reporter:Reporter,prv:String) :(String,String) =
{
val (ranges, errors) = daisy.analysis.SpecsProcessingPhase.extractPreCondition(pre)
if (! errors.isEmpty){
reporter.fatalError("Errors on inputs are currently unsupported")
}
if (prv == "coq"){
coqPrecondition(ranges)
coqPrecondition(ranges,fName)
}else if (prv == "hol4"){
hol4Precondition(ranges)
hol4Precondition(ranges,fName)
}else {
holLightPrecondition(ranges)
holLightPrecondition(ranges,fName)
}
}
......@@ -452,7 +462,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
......@@ -462,7 +472,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
......@@ -472,7 +482,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Division(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, errorMap, rangeMap, cont)
......@@ -482,7 +492,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( expEqBool e " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Let (y,exp, g) =>
val expFun = coqAbsEnv (exp, errorMap, rangeMap, cont)
......@@ -493,7 +503,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
s"( expEqBool e Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
cont)
gFun)
case x @ _ =>
"" //TODO Can this happen?
......@@ -529,7 +539,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Minus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
......@@ -539,7 +549,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
lFun)
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
......@@ -549,7 +559,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Division(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
......@@ -559,7 +569,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
cont)
rFun)
case x @ Let (y,exp, g) =>
val expFun = coqAbsEnv (exp, errorMap, rangeMap, cont)
......@@ -570,7 +580,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
s"( e = Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
cont)
gFun)
case x @ _ =>
"" //TODO Can this happen?
......@@ -637,27 +647,27 @@ object CertificatePhase extends DaisyPhase {
}
}
private def getAbsEnvDef (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], prv:String) :(String,String)=
private def getAbsEnvDef (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], fName:String, prv:String) :(String,String)=
if (prv == "coq")
("Definition absenv :analysisResult := \nfun (e:exp Q) =>\n" +
(s"Definition absenv_${fName} :analysisResult := \nfun (e:exp Q) =>\n" +
coqAbsEnv(e, errorMap, rangeMap, "((0#1,0#1),0#1)") + ".",
"absenv")
s"absenv_${fName}")
else if (prv == "hol4")
("val absenv_def = Define `\n absenv:analysisResult = \n\\e. \n" +
(s"val absenv_${fName}_def = Define `\n absenv_${fName}:analysisResult = \n\\e. \n" +
hol4AbsEnv(e, errorMap, rangeMap, "((0,1),1)") + "`;",
"absenv")
s"absenv_${fName}")
else
("let absenv = define `absenv:analysisResult = \n\\e. \n" +
holLightAbsEnv(e, errorMap, rangeMap, "((&0,&1),&1)") + "`;;",
"absenv")
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, prover:String) :String=
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, fName:String, prover:String) :String=
if (prover == "coq")
"Theorem ErrorBoundSound :\n CertificateCheckerCmd " + lastGenName + " " +
s"Theorem ErrorBound_${fName}_Sound :\n CertificateCheckerCmd " + lastGenName + " " +
analysisResultName + " " + precondName + " = true.\n" +
"Proof.\n cbv; auto.\nQed."
else if (prover == "hol4")
"val _ = store_thm (\"ErrorBoundSound\",\n ``CertificateCheckerCmd " +
"val _ = store_thm (\"ErrorBound_${fName}_Sound\",\n ``CertificateCheckerCmd " +
lastGenName + " " + analysisResultName + " " + precondName + " = T``,\n EVAL_TAC);"
else
"DAISY_CONV CertificateChecker thePrecondition theRewrites `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
......
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