Commit ef12f888 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into 'certificates'

Make certificate generation compliant with new format in upstream

See merge request !81
parents f5393bb8 31505b03
......@@ -17,7 +17,7 @@ Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Pr
approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv
|approxUpdFree E1 E2 A v1 v2 x fVars dVars:
approxEnv E1 A fVars dVars E2 ->
(Rabs (v1 - v2) <= v1 * Q2R machineEpsilon)%R ->
(Rabs (v1 - v2) <= Rabs v1 * Q2R machineEpsilon)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1) A (NatSet.add x fVars) dVars (updEnv x v2 E2)
|approxUpdBound E1 E2 A v1 v2 x fVars dVars:
......
......@@ -141,7 +141,7 @@ Proof.
apply Rmult_le_compat_r.
{ apply mEps_geq_zero. }
{ rewrite <- maxAbs_impl_RmaxAbs.
apply contained_leq_maxAbs_val.
apply contained_leq_maxAbs.
unfold contained; simpl.
pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf.
rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf.
......
......@@ -12,6 +12,8 @@ import scala.collection.immutable.Seq
import scala.reflect.ClassTag
import lang.Identifiers._
import lang.Trees._
import utils.{Interval, PartialInterval, Rational}
case class Context(
......@@ -28,15 +30,22 @@ case class Context(
// but don't want to pollute the nice and clean trees.
// If these get too many, move to their own "Summary".
// indexed by FunDef.id
inputRanges: Map[Identifier, Map[Identifier, Interval]] = Map(),
inputErrors: Map[Identifier, Map[Identifier, Rational]] = Map(),
specInputRanges: Map[Identifier, Map[Identifier, Interval]] = Map(),
specInputErrors: Map[Identifier, Map[Identifier, Rational]] = Map(),
// for now we only support a single result value, i.e. no tuples
// this map is indexed by fnc.id -> potentially partial interval bound of result
// and similar for the errors
resultRangeBounds: Map[Identifier, PartialInterval] = Map(),
resultErrorBounds: Map[Identifier, Rational] = Map()
//requiredOutputRanges: Map[Identifier, Map[Identifier, PartialInterval]] = Map(),
//requiredOutputErrors: Map[Identifier, Map[Identifier, Rational]] = Map()
specResultRangeBounds: Map[Identifier, PartialInterval] = Map(),
specResultErrorBounds: Map[Identifier, Rational] = Map(),
// the intermediate analysis results, since we rely on having them at hand when
// encoding the analysis result
intermediateAbsoluteErrors: Map[Identifier, Map[Expr, Rational]]= Map(),
intermediateRanges: Map[Identifier, Map[Expr, Interval]] = Map(),
// the analysed/computed roundoff errors for each function
resultAbsoluteErrors: Map[Identifier, Rational] = Map(),
resultRealRanges: Map[Identifier, Interval] = Map()
) {
// on the first creation of a context, we also update the context variable
......
......@@ -50,23 +50,16 @@ object InfoPhase extends DaisyPhase {
reporter.info(fnc.id)
val infoString: String = getLastExpression(fnc.body.get) match {
case x: NumAnnotation if x.hasError =>
val absError = x.absError
val range = x.interval
val relError: Double = if (range.xlo <= zero && zero <= range.xhi) {
Double.NaN
} else {
max(abs(absError / range.xlo), abs(absError / range.xhi)).toDouble
}
s"abs-error: ${x.absError}, range: ${x.interval},\nrel-error: ${relError}"
case x: NumAnnotation =>
"final error: - "
case _ => ""
}
val absError = ctx.resultAbsoluteErrors(fnc.id)
val range = ctx.resultRealRanges(fnc.id)
val relError: Double = if (range.xlo <= zero && zero <= range.xhi) {
Double.NaN
} else {
max(abs(absError / range.xlo), abs(absError / range.xhi)).toDouble
}
val infoString: String =
s"abs-error: ${absError}, real range: ${range},\nrel-error: ${relError}"
reporter.info(infoString)
if (out != null) {
......
......@@ -106,7 +106,7 @@ object DynamicPhase extends DaisyPhase {
val body = fnc.body.get
reporter.info("evaluating " + id + "...")
val inputRanges: Map[Identifier, Interval] = ctx.inputRanges(id).map({
val inputRanges: Map[Identifier, Interval] = ctx.specInputRanges(id).map({
case (id, i) =>
(id, Interval(i.mid - inputRangeFactor * i.radius,
i.mid + inputRangeFactor * i.radius))
......
......@@ -16,7 +16,7 @@ import lang.Identifiers._
Prerequisites:
- SpecsProcessingPhase
*/
object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
object RangeErrorPhase extends DaisyPhase with RoundoffEvaluators with IntervalSubdivision {
override val name = "range-error phase"
override val description = "Computes ranges and absolute errors"
......@@ -37,10 +37,6 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
var reporter: Reporter = null
// Var for error functions
// trackRoundoffErrs and uniformPrecision assigned below in run
attachToTree = true
override def run(ctx: Context, prg: Program): (Context, Program) = {
reporter = ctx.reporter
reporter.info(s"\nStarting $name")
......@@ -56,9 +52,8 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
var errorMethod = "interval"
var trackInitialErrs = true
var trackRoundoffErrs = true
// setting trait variables
trackRoundoffErrs = true
var uniformPrecision: Precision = Float64
// process relevant options
......@@ -97,11 +92,16 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
val fncsToConsider: Seq[String] = functionsToConsider(ctx, prg)
for (fnc <- prg.defs)
if (!fnc.precondition.isEmpty && !fnc.body.isEmpty && fncsToConsider.contains(fnc.id.toString)){
var roundoffErrorMap: Map[Identifier, Map[Expr, Rational]] = Map()
var rangeResMap: Map[Identifier, Map[Expr, Interval]] = Map()
val res: Map[Identifier, (Rational, Interval)] = prg.defs.filter(fnc =>
!fnc.precondition.isEmpty &&
!fnc.body.isEmpty &&
fncsToConsider.contains(fnc.id.toString)).map(fnc => {
reporter.info("analyzing fnc: " + fnc.id)
val inputValMap: Map[Identifier, Interval] = ctx.inputRanges(fnc.id)
val inputValMap: Map[Identifier, Interval] = ctx.specInputRanges(fnc.id)
// If we track both input and roundoff errors, then we pre-compute
// the roundoff errors for those variables that do not have a user-defined
......@@ -109,14 +109,14 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
val inputErrorMap: Map[Identifier, Rational] =
if (trackInitialErrs && trackRoundoffErrs){
val inputErrs = ctx.inputErrors(fnc.id)
val inputErrs = ctx.specInputErrors(fnc.id)
val allIDs = fnc.params.map(_.id).toSet
val missingIDs = allIDs -- inputErrs.keySet
inputErrs ++ missingIDs.map( id => (id -> uniformPrecision.absRoundoff(inputValMap(id))))
} else if(trackInitialErrs) {
val inputErrs = ctx.inputErrors(fnc.id)
val inputErrs = ctx.specInputErrors(fnc.id)
val allIDs = fnc.params.map(_.id).toSet
val missingIDs = allIDs -- inputErrs.keySet
inputErrs ++ missingIDs.map( id => (id -> zero))
......@@ -133,37 +133,46 @@ object RangeErrorPhase extends DaisyPhase with ErrorFunctions {
}
(rangeMethod, errorMethod) match {
val (resError: Rational, resRange: Interval, rangeMap:Map[Expr, Interval], errorMap:Map[Expr, Interval]) = (rangeMethod, errorMethod) match {
case ("interval", "interval") =>
errorIntervalInterval(fnc.body.get, inputValMap, inputErrorMap)
uniformRoundoff_IA_IA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
case ("interval", "affine") =>
errorIntervalAffine(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision)
uniformRoundoff_IA_AA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
case ("affine", "affine") =>
errorAffineAffine(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision)
uniformRoundoff_AA_AA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
case ("smt", "affine") =>
errorSMTAffine(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision)
uniformRoundoff_SMT_AA(fnc.body.get, inputValMap, inputErrorMap, uniformPrecision, trackRoundoffErrs)
// default is to use the method that attaches the info to trees.
case ("subdiv", _) =>
evaluateSubdiv(
fnc.body.get,
val tmp = doIntervalSubdivision( //evaluateSubdiv(
fnc.body.get, lang.TreeOps.freeVariablesOf(fnc.body.get),
inputValMap,
inputErrorMap,
trackRoundoffErrs,
uniformPrecision)
(tmp._2, tmp._1)
case _ =>
reporter.fatalError(s"Your combination of $rangeMethod and $errorMethod" +
"for computing ranges and errors is not supported.")
null
}
}
roundoffErrorMap += (fnc.id -> (errorMap.map(x => x._1 -> x._2.xhi)))
rangeResMap += (fnc.id -> rangeMap)
(fnc.id -> (resError, resRange))
}).toMap
timer.stop
ctx.reporter.info(s"Finished $name")
(ctx, prg)
(ctx.copy(
resultAbsoluteErrors = res.map(x => (x._1 -> x._2._1)),
resultRealRanges = res.map(x => (x._1 -> x._2._2)),
intermediateAbsoluteErrors = roundoffErrorMap,
intermediateRanges = rangeResMap), prg)
}
......
......@@ -70,7 +70,7 @@ object RangePhase extends DaisyPhase {
case "smt" =>
evaluateSMT(fnc.body.get, Map.empty)
case "subdiv" =>
evaluateSubdiv(fnc.body.get, ctx.inputRanges(fnc.id), Map.empty)
evaluateSubdiv(fnc.body.get, ctx.specInputRanges(fnc.id), Map.empty)
}
......
......@@ -121,8 +121,8 @@ object SpecsProcessingPhase extends DaisyPhase {
reporter.debug("range bounds: " + resRanges.mkString("\n"))
reporter.debug("error bounds: " + resErrors.mkString("\n"))
(ctx.copy(inputRanges = allRanges, inputErrors = allErrors,
resultRangeBounds = resRanges, resultErrorBounds = resErrors), prg)
(ctx.copy(specInputRanges = allRanges, specInputErrors = allErrors,
specResultRangeBounds = resRanges, specResultErrorBounds = resErrors), prg)
}
......
......@@ -5,7 +5,7 @@ import daisy.lang.{ScalaPrinter, PrettyPrinter}
import lang.Trees._
import lang.Identifiers._
import lang.NumAnnotation
import utils.Interval._
import utils.Interval
import utils.Rational
import analysis.SpecsProcessingPhase
......@@ -20,7 +20,9 @@ object CertificatePhase extends DaisyPhase {
def run(ctx: Context, prg: Program): (Context, Program) = {
val reporter = ctx.reporter
val proverToUse = ctx.findOption(Main.optionValidators)
val prover = ctx.findOption(Main.optionValidators)
val errorMap = ctx.resultAbsoluteErrors
val rangeMap = ctx.resultRealRanges
def writeToFile (fileContent:String, prover:String, fname:String){
import java.io.FileWriter
......@@ -30,9 +32,9 @@ object CertificatePhase extends DaisyPhase {
"./coq/output/certificate_" + prg.id + "_" + fname + ".v"
else
if (prover == "hol4")
"./hol4/output/certificate_" + prg.id + "_" + fname + "Script.sml"
else
"./hol-light/output/certificate_" + prg.id + "_" + fname + ".hl"
"./hol4/output/certificate_" + prg.id + "_" + fname + "Script.sml"
else
"./hol-light/output/certificate_" + prg.id + "_" + fname + ".hl"
val fstream = new FileWriter(fileLocation)
val out = new BufferedWriter(fstream)
out.write(fileContent)
......@@ -44,7 +46,10 @@ object CertificatePhase extends DaisyPhase {
val thePrecondition = fnc.precondition
val theBody = fnc.body
proverToUse match {
val errorMap = ctx.intermediateAbsoluteErrors.get(fnc.id).get
val rangeMap = ctx.intermediateRanges.get(fnc.id).get
prover match {
case Some(prv) =>
thePrecondition match {
case Some (pre) =>
......@@ -55,7 +60,7 @@ object CertificatePhase extends DaisyPhase {
//generate the precondition
val (thePreconditionFunction, functionName) = getPrecondFunction(pre, reporter, prv)
//the analysis result function
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, prv)
val (analysisResultText, analysisResultName) = getAbsEnvDef(theBody.get, errorMap, rangeMap, prv)
//generate the final evaluation statement
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
......@@ -71,16 +76,11 @@ object CertificatePhase extends DaisyPhase {
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
case None => reporter.fatalError ("No Precondition specified")
case None => reporter.fatalError ("No Precondition specified.")
}
case None => reporter.fatalError ("Failure")
case None => reporter.fatalError ("No theorem prover specified.")
}
}
//generate definitions for "program"
//obtain analysis result from ctx?
//generate abstract environment for analysis result
(ctx, prg)
}
......@@ -377,57 +377,59 @@ object CertificatePhase extends DaisyPhase {
}
}
private def coqAbsEnv (e:Expr, cont:String) :String =
private def coqAbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
//must be set TODO:Assert?
//since we already generated the AST, we can be sure to have generated the name
assert (expressionNames(e) != None)
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("/","#")
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ RealLiteral(r) =>
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("/","#")
val intvE = coqInterval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString.replace("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ Plus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("/","#")
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("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Minus(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("/","#")
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("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Times(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("/","#")
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("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Division(lhs, rhs) =>
val lFun = coqAbsEnv (lhs, cont)
val rFun = coqAbsEnv (rhs, lFun)
val intvE = coqInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("/","#")
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("/","#")
"if expEqBool e " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
......@@ -436,57 +438,57 @@ object CertificatePhase extends DaisyPhase {
}
}
private def hol4AbsEnv (e:Expr, cont:String) :String =
private def hol4AbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
//must be set TODO:Assert?
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ RealLiteral(r) =>
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString
val intvE = hol4Interval((rangeMap(x).xlo,rangeMap(x).xhi))
val errE = errorMap(x).toFractionString
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ Plus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, cont)
val rFun = hol4AbsEnv (rhs, lFun)
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString
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
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Minus(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, cont)
val rFun = hol4AbsEnv (rhs, lFun)
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString
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
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, cont)
val rFun = hol4AbsEnv (rhs, lFun)
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString
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
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Division(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, cont)
val rFun = hol4AbsEnv (rhs, lFun)
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString
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
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
......@@ -496,57 +498,57 @@ object CertificatePhase extends DaisyPhase {
}
}
private def holLightAbsEnv (e:Expr, cont:String) :String =
private def holLightAbsEnv (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], cont:String) :String =
{
//must be set TODO:Assert?
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
val errE = errorMap(x).toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ RealLiteral(r) =>
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
val errE = errorMap(x).toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ Plus(lhs, rhs) =>
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val lFun = holLightAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = holLightAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
val errE = errorMap(x).toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Minus(lhs, rhs) =>
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val lFun = holLightAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = holLightAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
val errE = errorMap(x).toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Times(lhs, rhs) =>
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val lFun = holLightAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = holLightAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
val errE = errorMap(x).toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Division(lhs, rhs) =>
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val lFun = holLightAbsEnv (lhs, errorMap, rangeMap, cont)
val rFun = holLightAbsEnv (rhs, errorMap, rangeMap, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
val errE = errorMap(x).toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
......@@ -556,15 +558,18 @@ object CertificatePhase extends DaisyPhase {
}
}
private def getAbsEnvDef (e:Expr, prv:String) :(String,String)=
private def getAbsEnvDef (e:Expr, errorMap:Map[Expr, Rational], rangeMap:Map[Expr, Interval], prv:String) :(String,String)=
if (prv == "coq")