Commit 198b3cfc authored by Heiko Becker's avatar Heiko Becker
Browse files

Add precondition construction ans some dummy functions

parent a2d2bb7b
......@@ -6,7 +6,8 @@ import lang.Trees._
import lang.Identifiers._
import lang.NumAnnotation
import utils.Interval._
import utils.Rational._
import utils.Rational
import analysis.SpecsProcessingPhase
object CertificatePhase extends DaisyPhase {
......@@ -17,6 +18,8 @@ object CertificatePhase extends DaisyPhase {
FlagOptionDef("printToFile", "print generated code to file")
)
var identifierNums : Map [Identifier, Int] = Map[Identifier, Int] ()
implicit val debugSection = DebugSectionBackend
def run(ctx: Context, prg: Program): (Context, Program) = {
......@@ -39,14 +42,22 @@ object CertificatePhase extends DaisyPhase {
}
for (fnc <- prg.defs) if (!fnc.precondition.isEmpty && !fnc.body.isEmpty){
reporter.info(s"Generating certificate for $fnc.id}")
reporter.info(s"Generating certificate for ${fnc.id}")
val thePrecondition = fnc.precondition
val theBody = fnc.body
proverToUse match {
case Some(prv) =>
val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
writeToFile(theDefinitions,prv,fnc.id.toString)
thePrecondition match {
case Some (pre) =>
val prelude = getPrelude(prv)
val (thePreconditionFunction, functionName) = getPrecondFunction(pre, reporter, prv)
val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, reporter, prv)
val functionCall = getComputeExpr(lastGenName,analysisResultName)
writeToFile(thePreconditionFunction + "\n" + theDefinitions,prv,fnc.id.toString)
case None => reporter.fatalError ("No Precondition specified")
}
case None => reporter.fatalError ("Failure")
}
......@@ -62,8 +73,61 @@ object CertificatePhase extends DaisyPhase {
private val nextConstantId = { var i = 0; () => { i += 1; i} }
private val nextFreshVariable = { var i = 0; () => { i += 1; i} }
private def getPrelude(prv:String) =
"ABC"
/* TOD: Make these tranlate the rationals to proper rationals in Coq, resp. HOL-Light */
private def coqPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "Definition thePrecondition:precond = fun (n:nat) ->\n"
for ((id,intv) <- ranges) {
intv match {
case (lowerBound, upperBound) =>
val freshBinder = nextFreshVariable()
identifierNums += (id -> freshBinder)
theFunction += "if n =? " + freshBinder + " then ("+lowerBound.toString + ","+upperBound.toString + ") else "
}
}
theFunction += "(0#0,0#0)."
(theFunction, "thePrecondition")
}
private def holPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "let thePrecondition = define ` \n thePrecondition (n:num) = \n"
for ((id,intv) <- ranges) {
intv match {
case (lowerBound, upperBound) =>
val freshBinder = nextFreshVariable()
identifierNums += (id -> freshBinder)
theFunction += "if n = " + freshBinder + " then ("+lowerBound.toString + ","+upperBound.toString + ") else "
}
}
theFunction += "(&0,&0)`;;"
(theFunction, "thePrecondition")
}
private def getPrecondFunction(pre:Expr,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)
}else {
holPrecondition(ranges)
}
}
private def getAbsEnvDef (e:Expr,reporter:Reporter, prv:String) =
("ABC","ABC")
private def getComputeExpr (lastGenName:String, analysisResultName:String) =
"ABC"
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 := Var Q $vname.\n"
(theValue + theExpr,s"ExpVar$vname")
......@@ -71,8 +135,8 @@ object CertificatePhase extends DaisyPhase {
private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theValue = s"let $vname:num = define `$vname = $id`;;\n"
val theExpr = s"let ExpVar$vname = define `ExpVar$vname = Var $vname`;;\n"
val theValue = s"let $vname = define `$vname:num = $id`;;\n"
val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Var $vname`;;\n"
(theValue + theExpr, s"ExpVar$vname")
}
......@@ -96,7 +160,6 @@ object CertificatePhase extends DaisyPhase {
(theValue + theExpr, s"ExpCst$id")
}
/* TODO */
private def coqBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
e match {
case x @ Plus(lhs, rhs) =>
......@@ -109,16 +172,30 @@ object CertificatePhase extends DaisyPhase {
reporter.fatalError("Unsupported value")
}
private def holBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
e match {
case x @ Plus(lhs, rhs) =>
(s"let Plus$nameLHS$nameRHS = define `Plus$nameLHS$nameRHS:(real)exp = Binop Plus $nameLHS $nameRHS`;;\n",
"Plus$nameLHS$nameRHS")
case x @ Minus(lhs, rhs) =>
(s"let Sub$nameLHS$nameRHS = define `Sub$nameLHS$nameRHS:(real)exp = Binop Sub $nameLHS $nameRHS`;;\n",
"Sub$nameLHS$nameRHS")
case x @ Times(lhs, rhs) =>
(s"let Mul$nameLHS$nameRHS = define `Mul$nameLHS$nameRHS:(real)exp = Binop Mult $nameLHS $nameRHS`;;\n",
"Mul$nameLHS$nameRHS")
case x @ _ =>
reporter.fatalError("Unsupported value")
}
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = e match {
case x @ Variable(id) =>
// TODO: Make this use the global variable id map!
if (prv == "coq") {
coqVariable (id,nextFreshVariable(),reporter)
}else {
holVariable (id,nextFreshVariable(),reporter)
}
//print state
//reporter.info(s"$x: ${x.interval},${x.absError}")
case x @ RealLiteral(r) =>
if (prv == "coq") {
......@@ -135,7 +212,8 @@ object CertificatePhase extends DaisyPhase {
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
("A","B")
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
case x @ Minus(lhs, rhs) =>
......@@ -145,7 +223,8 @@ object CertificatePhase extends DaisyPhase {
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
("A","B")
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
case x @ Times(lhs, rhs) =>
......@@ -155,7 +234,8 @@ object CertificatePhase extends DaisyPhase {
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
("A","B")
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
case x @ _ =>
......
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