Fix bug in SpecsPhase that did not use mixed-precision assignments

src/main/scala/daisy/analysis/SpecsProcessingPhase.scala

@@ -110,11 +110,14 @@ object SpecsProcessingPhase extends DaisyPhase with PrecisionsParser {
           // the roundoff errors for those variables that do not have a user-defined
           // error, in order to keep correlations.
           allErrors += (fnc.id -> (
+            {
+            val precisionMap = inputPrecision.get(fnc.id).get
             if (trackInitialErrs && trackRoundoffErrs){
 
               val allIDs = fnc.params.map(_.id).toSet
               val missingIDs = allIDs -- errors.keySet
-              errors ++ missingIDs.map(id => (id -> defaultPrecision.absRoundoff(allRanges(fnc.id)(id))))
+              errors ++ missingIDs.map(id =>
+                (id -> (precisionMap.get(id).get).absRoundoff(allRanges(fnc.id)(id))))
 
             } else if (trackInitialErrs) {
 
@@ -132,7 +135,9 @@ object SpecsProcessingPhase extends DaisyPhase with PrecisionsParser {
               val allIDs = fnc.params.map(_.id)
               allIDs.map(id => (id -> Rational.zero)).toMap
 
-            }))
+            }
+            }
+          ))
           addConds match {
             case Seq() => additionalConst += (fnc.id -> BooleanLiteral(true)) // no additional constraints
             case Seq(x) => additionalConst += (fnc.id -> x)

src/main/scala/daisy/backend/CertificatePhase.scala

@@ -81,9 +81,7 @@ object CertificatePhase extends DaisyPhase {
       //first retrieve the values
       //these should be defined, otherwise the generation will fail
       val thePrecondition = fnc.precondition.get
-      reporter.info(s"${fnc.body.get}")
       val theBody = (changeType (fnc.body.get, precisionMap))._1
-      reporter.info(s"$theBody")
       val errorMap = ctx.intermediateAbsErrors.get(fnc.id).get
       val rangeMap = ctx.intermediateRanges.get(fnc.id).get
 
@@ -153,14 +151,14 @@ object CertificatePhase extends DaisyPhase {
 
   private def coqVariable(vname: Identifier): (String, String) =
   {
-    val name = s"ExpVar$vname${vname.globalId}"
+    val name = s"$vname${vname.globalId}"
     val theExpr = s"Definition $name :exp Q := Var Q ${vname.globalId}.\n"
     (theExpr, name)
   }
 
   private def hol4Variable(vname: Identifier): (String, String) =
   {
-    val name = s"ExpVar$vname${vname.globalId}"
+    val name = s"$vname${vname.globalId}"
     val theExpr = s"val ${name}_def = Define `$name:(real exp) = Var ${vname.globalId}`;\n"
     (theExpr, name)
   }
@@ -173,8 +171,9 @@ object CertificatePhase extends DaisyPhase {
         val prec = precisionToString(precision)
         val rationalStr = v.toFractionString
         val coqRational = rationalStr.replace('/', '#')
-        val theExpr = s"Definition ExpCst$id$freshId :exp Q := Const $prec ($coqRational).\n"
-        (theExpr, s"ExpCst$id$freshId")
+        val name = s"C$id$freshId"
+        val theExpr = s"Definition $name :exp Q := Const $prec ($coqRational).\n"
+        (theExpr, name)
     }
 
   private def hol4Constant(r: RealLiteral, id: Int, precision: Precision): (String, String) =
@@ -184,26 +183,30 @@ object CertificatePhase extends DaisyPhase {
         val freshId = nextConstantId()
         val prec = precisionToString(precision)
         val rationalStr = v.toFractionString
-        val theExpr = s"val ExpCst$id${freshId}_def = Define `ExpCst$id$freshId:(real exp) = Const $prec ($rationalStr)`;\n"
-        (theExpr, s"ExpCst$id$freshId")
+        val name = s"C$id$freshId"
+        val theExpr = s"val ${name}_def = Define `$name:(real exp) = Const $prec ($rationalStr)`;\n"
+        (theExpr, name)
     }
 
   private def coqBinOp (e: Expr, nameLHS: String, nameRHS: String): (String, String) =
-    e match {
-      case x @ Plus(lhs, rhs) =>
-        ("Definition Plus"+ nameLHS + nameRHS + s" :exp Q := Binop Plus $nameLHS $nameRHS.\n",
-          "Plus"+ nameLHS + nameRHS)
-       case x @ Minus(lhs, rhs) =>
-        ("Definition Sub"+ nameLHS + nameRHS + s" :exp Q := Binop Sub $nameLHS $nameRHS.\n",
-          "Sub"+ nameLHS + nameRHS)
-       case x @ Times(lhs, rhs) =>
-        ("Definition Mult"+ nameLHS + nameRHS + s" :exp Q := Binop Mult $nameLHS $nameRHS.\n",
-          "Mult"+ nameLHS + nameRHS)
-      case x @ Division(lhs, rhs) =>
-        ("Definition Div"+ nameLHS + nameRHS + s" :exp Q := Binop Div $nameLHS $nameRHS.\n",
-          "Div"+ nameLHS + nameRHS)
-       case x @ _ =>
-       reporter.fatalError("Unsupported value")
+    {
+      val name = s"e${nextConstantId()}"
+      e match {
+        case x @ Plus(lhs, rhs) =>
+          (s"Definition $name :exp Q := Binop Plus $nameLHS $nameRHS.\n",
+            name)
+        case x @ Minus(lhs, rhs) =>
+          (s"Definition $name :exp Q := Binop Sub $nameLHS $nameRHS.\n",
+            name)
+        case x @ Times(lhs, rhs) =>
+          (s"Definition $name :exp Q := Binop Mult $nameLHS $nameRHS.\n",
+            name)
+        case x @ Division(lhs, rhs) =>
+          (s"Definition $name :exp Q := Binop Div $nameLHS $nameRHS.\n",
+            name)
+        case x @ _ =>
+          reporter.fatalError("Unsupported value")
+      }
     }
 
     private def hol4BinOp (e: Expr, nameLHS: String, nameRHS: String): (String, String) =
@@ -724,12 +727,12 @@ object CertificatePhase extends DaisyPhase {
 
   private def getAbsEnvDef(e: Expr, errorMap: Map[Expr, Rational], rangeMap: Map[Expr, Interval], precision: Map[Identifier, Precision], fName: String, prv: String): (String, String)=
     if (prv == "coq")
-      (s"Definition absenv_${fName} :analysisResult := \n" +
+      (s"Definition absenv_${fName} :analysisResult := Eval compute in\n" +
         coqAbsEnv(e, errorMap, rangeMap, precision, "DaisyMap.empty (intv * error)") + ".",
         s"absenv_${fName}")
     else if (prv == "hol4")
-      (s"val absenv_${fName}_def = Define `\n  absenv_${fName}:analysisResult = \n" +
-        hol4AbsEnv(e, errorMap, rangeMap, precision, "DaisyMap_empty") + "`;",
+      (s"val absenv_${fName}_def = RIGHT_CONV_RULE EVAL (Define `\n  absenv_${fName}:analysisResult = \n" +
+        hol4AbsEnv(e, errorMap, rangeMap, precision, "DaisyMapTree_empty") + "`);",
         s"absenv_${fName}")
     else
       ("ABS " + binaryAbsEnv(e, errorMap, rangeMap, reporter), "")

src/main/scala/daisy/tools/RoundoffEvaluators.scala

@@ -4,6 +4,7 @@ package daisy
 package tools
 
 import lang.Trees._
+import lang.Types._
 import lang.Identifiers._
 import FinitePrecision._
 import Rational._
@@ -386,11 +387,10 @@ trait RoundoffEvaluators extends RangeEvaluators {
         val (valueError, valuePrec) = eval(value)
 
         val idPrec = precision(id)
-        val idType = id.getType
         val error = if (idPrec < valuePrec) { // we need to cast down
           val valueRange = range(value)
           val err = computeNewError(valueRange, valueError, idPrec)
-          intermediateErrors.put(Downcast(value,idType),err)
+          intermediateErrors.put(Downcast(value,FinitePrecisionType(idPrec)),err)
           err
         } else {
           (valueError,valuePrec)
@@ -402,7 +402,7 @@ trait RoundoffEvaluators extends RangeEvaluators {
 
       case _ => throw new Exception("Not supported")
 
-    })
+      })
     val (resError, _) = eval(expr)
     (resError, intermediateErrors.mapValues(_._1).toMap)
   }