Commit ef97348d authored by Raphaël Monat's avatar Raphaël Monat
Browse files

to debug on BallBeam, --randomMP

parent 40475da3
......@@ -253,7 +253,7 @@ object CertificatePhase extends DaisyPhase {
private def hol4Downcast(nameOp: String, prec: Precision): (String, String) = {
val name = s"Downcast${precisionToString(prec)}$nameOp"
(s"val $name = Define `$name : reql exp = Downcast ${precisionToString(prec)} $nameOp`;;\n", name)
(s"val $name = Define `$name : real exp = Downcast ${precisionToString(prec)} $nameOp`;;\n", name)
}
......@@ -629,10 +629,10 @@ object CertificatePhase extends DaisyPhase {
val expFun = hol4AbsEnv (exp, errorMap, rangeMap, precisions, cont)
val gFun = hol4AbsEnv (g, errorMap, rangeMap, precisions, expFun)
val intvY = hol4Interval((rangeMap(Variable(y)).xlo, rangeMap(Variable(y)).xhi))
val errY = errorMap(Variable(y)).toFractionString.replace("/", "#")
val errY = errorMap(Variable(y)).toFractionString
val nameY = expressionNames(Variable(y))
conditional (
s"( e = Var Q ${identifierNums(y)} )",
s"( e = Var ${identifierNums(y)} )",
"(" + intvY + ", " + errY + ")",
gFun)
......
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