Commit 111d4b3d authored by Heiko Becker's avatar Heiko Becker

Fix bug, that there was no unary negation possible in certificates

parent e4778d81
......@@ -3,6 +3,7 @@ package backend
import daisy.lang.{ScalaPrinter, PrettyPrinter}
import lang.Trees._
import lang.TreeOps
import lang.Identifiers._
import lang.NumAnnotation
import utils.Interval
......@@ -48,11 +49,16 @@ object CertificatePhase extends DaisyPhase {
fullCertificate += prelude + "\n\n";
var size = 0
for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){
reporter.info(s"Generating certificate for ${fnc.id}")
val thePrecondition = fnc.precondition
val theBody = fnc.body
size += TreeOps.size(theBody.get)
val errorMap = ctx.intermediateAbsoluteErrors.get(fnc.id).get
val rangeMap = ctx.intermediateRanges.get(fnc.id).get
......@@ -89,6 +95,8 @@ object CertificatePhase extends DaisyPhase {
case None => reporter.fatalError ("No theorem prover specified.")
}
}
reporter.info(s"Number of operations: $size")
//end iteration, write certificate
writeToFile(fullCertificate,prover.get)
(ctx, prg)
......@@ -213,6 +221,13 @@ object CertificatePhase extends DaisyPhase {
reporter.fatalError("Unsupported value")
}
private def coqUMin (e:Expr, nameOp:String, reporter:Reporter) :(String, String) =
(s"Defintion UMin${nameOp} :exp Q := Unop Neg $nameOp", s"UMin${nameOp}")
private def hol4UMin (e:Expr, nameOp:String, reporter:Reporter) :(String, String) =
(s"val UMin${nameOp} = Define `UMin${nameOp}:(real exp) = Unop Neg ${nameOp}`;",
s"UMin${nameOp}")
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = {
if (expressionNames.contains(e)){
......@@ -318,8 +333,21 @@ object CertificatePhase extends DaisyPhase {
expressionNames += (e -> name)
(definition,name)
case x @ UMinus (exp) =>
val (opDef, opName) = getValues (exp, reporter, prv)
val (defintion, name) =
if (prv == "coq") {
val (unopDef, unopName) = coqUMin (e, opName, reporter)
(opDef + unopDef, unopName)
} else {
val (unopDef, unopName) = hol4UMin (e, opName, reporter)
(opDef + unopDef, unopName)
}
expressionNames += (e -> name)
(defintion, name)
case x @ _ =>
reporter.fatalError(s"Unsupported operation")
reporter.fatalError(s"Unsupported operation $e")
}
}
}
......
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