Commit cd4f5b9f authored by Heiko Becker's avatar Heiko Becker
Browse files

Accidentally pushed output...

parent 4ba5b551
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../
OPTIONS = QUIT_ON_FAILURE
open CertificateCheckerTheory;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((1657)/(5))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val PlusExpCst1ExpVaru = Define `PlusExpCst1ExpVaru:(real exp) = Binop Plus ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = PlusExpCst1ExpVaru then (( (1157)/(5), (2157)/(5)),(7771411516990528329)/(81129638414606681695789005144064))
else if e = ExpVaru then (( (-100)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (1657)/(5), (1657)/(5)),(1657)/(45035996273704960))
else ((0,1),1)`;
EVAL ``CertificateChecker PlusExpCst1ExpVaru absenv thePrecondition``;
\ No newline at end of file
open CertificateCheckerTheory;
open simpLib realTheory realLib RealArith;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((1657)/(5))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val DivExpCst1ExpVaru = Define `DivExpCst1ExpVaru:(real exp) = Binop Div ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (1)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = DivExpCst1ExpVaru then (( (1657)/(500), (1657)/(5)),(1543838985824032326958855430137511160223694676240661)/(411376139330292376153508977546804877224608665699390244473798656))
else if e = ExpVaru then (( (1)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (1657)/(5), (1657)/(5)),(1657)/(45035996273704960))
else ((0,1),1)`;
val test = EVAL ``CertificateChecker DivExpCst1ExpVaru absenv thePrecondition``;
open CertificateCheckerTheory;
open simpLib realTheory realLib RealArith;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((100)/(1))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val MultExpCst1ExpVaru = Define `MultExpCst1ExpVaru:(real exp) = Binop Mult ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = MultExpCst1ExpVaru then (( (-10000)/(1), (10000)/(1)),(152118072027387545068102987284480625)/(45671926166590716193865151022383844364247891968))
else if e = ExpVaru then (( (-100)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (100)/(1), (100)/(1)),(25)/(2251799813685248))
else ((0,1),1)`;
val _ = store_thm ("ErrorBoundSound",
``CertificateChecker MultExpCst1ExpVaru absenv thePrecondition``,
EVAL_TAC);
\ No newline at end of file
open CertificateCheckerTheory;
val ExpCst1 = Define `ExpCst1:(real exp) = Const ((1657)/(5))`;
val ExpVaru = Define `ExpVaru:(real exp) = Param 1`;
val SubExpCst1ExpVaru = Define `SubExpCst1ExpVaru:(real exp) = Binop Sub ExpCst1 ExpVaru`;;
val thePrecondition_def = Define `
thePrecondition (n:num) =
if n = 1 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_def = Define `absenv:analysisResult =
\e.
if e = SubExpCst1ExpVaru then (( (1157)/(5), (2157)/(5)),(7771411516990528329)/(81129638414606681695789005144064))
else if e = ExpVaru then (( (-100)/(1), (100)/(1)),(25)/(2251799813685248))
else if e = ExpCst1 then (( (1657)/(5), (1657)/(5)),(1657)/(45035996273704960))
else ((0,1),1)`;
EVAL ``CertificateChecker SubExpCst1ExpVaru absenv thePrecondition``;
\ No newline at end of file
......@@ -19,7 +19,7 @@ object Main {
val optionPrintToughSMTCalls = FlagOptionDef("print-tough-smt-calls",
"If enabled, will print those SMT queries to file which take longer.")
val optionValidators = ChoiceOptionDef("certificate", "Wether to certify and which theorem prover to use",Set("coq","hol"),"coq")
val optionValidators = ChoiceOptionDef("certificate", "Wether to certify and which theorem prover to use",Set("coq","hol-light","hol4"),"coq")
val globalOptions: Set[CmdLineOptionDef[Any]] = Set(
FlagOptionDef("help", "Show this message."),
......
......@@ -29,7 +29,10 @@ object CertificatePhase extends DaisyPhase {
if (prover == "coq")
"./coq/output/certificate_" + prg.id + "_" + fname + ".v"
else
"./hol/output/certificate_" + prg.id + "_" + fname + ".hl"
if (prover == "hol4")
"./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)
......@@ -57,12 +60,12 @@ object CertificatePhase extends DaisyPhase {
val functionCall = getComputeExpr(lastGenName,analysisResultName,functionName,prv)
//val functionCall = getAllComputeExps(theBody.get, analysisResultName, functionName, prv)
//compose the strings
val textWithoutFCall = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n" + analysisResultText
val textWithoutFCall = prelude + "\n\n" + theDefinitions + "\n\n" + thePreconditionFunction + "\n\n" + analysisResultText
val certificateText =
if (prv == "coq")
textWithoutFCall + "\n\n" + functionCall
if (prv == "hol-light")
textWithoutFCall + "\n\n" + "let theRewrites = [thePrecondition;absenv;" + holLightExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
else
textWithoutFCall + "\n\n" + "let theRewrites = [thePrecondition;absenv;" + holExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
textWithoutFCall + "\n\n" + functionCall
//write to the output file
writeToFile(certificateText,prv,fnc.id.toString)
......@@ -76,7 +79,6 @@ object CertificatePhase extends DaisyPhase {
//obtain analysis result from ctx?
//generate abstract environment for analysis result
(ctx, prg)
}
......@@ -86,6 +88,8 @@ object CertificatePhase extends DaisyPhase {
private def getPrelude(prover:String) :String=
if (prover == "coq")
"Require Import Daisy.CertificateChecker."
else if (prover == "hol4")
"open CertificateCheckerTheory;\nopen simpLib realTheory realLib RealArith;"
else
"needs \"CertificateChecker.hl\";;\nneeds \"Infra/convs.hl\";;"
......@@ -95,10 +99,16 @@ object CertificatePhase extends DaisyPhase {
(theExpr,s"ExpVar$vname")
}
private def holVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
private def hol4Variable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theExpr = s"val ExpVar$vname = Define `ExpVar$vname:(real exp) = Param $id`;\n"
(theExpr, s"ExpVar$vname")
}
private def holLightVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theExpr = s"let ExpVar$vname = define `ExpVar$vname:(real)exp = Param $id`;;\n"
( theExpr, s"ExpVar$vname")
(theExpr, s"ExpVar$vname")
}
private def coqConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
......@@ -110,13 +120,21 @@ object CertificatePhase extends DaisyPhase {
(theExpr, s"ExpCst$id")
}
private def holConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
private def hol4Constant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
r match {
case RealLiteral(v) =>
val rationalStr = v.toFractionString
val theExpr = s"val ExpCst$id = Define `ExpCst$id:(real exp) = Const ($rationalStr)`;\n"
(theExpr, s"ExpCst$id")
}
private def holLightConstant(r:RealLiteral, id:Int, reporter:Reporter) :(String, String) =
r match {
case RealLiteral(v) =>
val rationalStr = v.toFractionString
val ratTmp = rationalStr.replace("(","(&")
val holRational = ratTmp.replace("&-","-- &")
val theExpr = s"let ExpCst$id = define `ExpCst$id:(real)exp = Const ($holRational)`;;\n"
val holLightRational = ratTmp.replace("&-","-- &")
val theExpr = s"let ExpCst$id = define `ExpCst$id:(real)exp = Const ($holLightRational)`;;\n"
(theExpr, s"ExpCst$id")
}
......@@ -138,7 +156,25 @@ object CertificatePhase extends DaisyPhase {
reporter.fatalError("Unsupported value")
}
private def holBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
private def hol4BinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
e match {
case x @ Plus(lhs, rhs) =>
("val Plus"+ nameLHS + nameRHS + " = Define `Plus"+ nameLHS + nameRHS + s":(real exp) = Binop Plus $nameLHS $nameRHS`;;\n",
"Plus"+ nameLHS + nameRHS)
case x @ Minus(lhs, rhs) =>
("val Sub"+ nameLHS + nameRHS + " = Define `Sub"+ nameLHS + nameRHS + s":(real exp) = Binop Sub $nameLHS $nameRHS`;;\n",
"Sub"+ nameLHS + nameRHS)
case x @ Times(lhs, rhs) =>
("val Mult"+ nameLHS + nameRHS + " = Define `Mult"+ nameLHS + nameRHS + s":(real exp) = Binop Mult $nameLHS $nameRHS`;;\n",
"Mult"+ nameLHS + nameRHS)
case x @ Division(lhs, rhs) =>
("val Div"+ nameLHS + nameRHS + " = Define `Div"+ nameLHS + nameRHS + s":(real exp) = Binop Div $nameLHS $nameRHS`;;\n",
"Div"+ nameLHS + nameRHS)
case x @ _ =>
reporter.fatalError("Unsupported value")
}
private def holLightBinOp (e: Expr, nameLHS:String, nameRHS:String, reporter:Reporter) :(String, String) =
e match {
case x @ Plus(lhs, rhs) =>
("let Plus"+ nameLHS + nameRHS + " = define `Plus"+ nameLHS + nameRHS + s":(real)exp = Binop Plus $nameLHS $nameRHS`;;\n",
......@@ -170,8 +206,10 @@ object CertificatePhase extends DaisyPhase {
val (definition, name) =
if (prv == "coq"){
coqVariable (id,varId,reporter)
}else{
holVariable (id,varId,reporter)
}else if (prv == "hol4"){
hol4Variable (id, varId, reporter)
}else {
holLightVariable (id,varId,reporter)
}
expressionNames += (e -> name)
(definition,name)
......@@ -181,8 +219,10 @@ object CertificatePhase extends DaisyPhase {
val (definition, name) =
if (prv == "coq")
coqConstant (x,nextConstantId(),reporter)
else if (prv == "hol4")
hol4Constant (x, nextConstantId(), reporter)
else
holConstant (x,nextConstantId(),reporter)
holLightConstant (x,nextConstantId(),reporter)
expressionNames += (e -> name)
(definition,name)
......@@ -193,8 +233,11 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else if (prv == "hol4") {
val (binOpDef, binOpName) = hol4BinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
val (binOpDef, binOpName) = holLightBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
......@@ -207,8 +250,11 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else if (prv == "hol4") {
val (binOpDef, binOpName) = hol4BinOp (e, lhsName, rhsName, reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
val (binOpDef, binOpName) = holLightBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
......@@ -221,8 +267,11 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else if (prv == "hol4") {
val (binOpDef, binOpName) = hol4BinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
val (binOpDef, binOpName) = holLightBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
......@@ -235,8 +284,11 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else if (prv == "hol4") {
val (binOpDef, binOpName) = hol4BinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
val (binOpDef, binOpName) = holLightBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
......@@ -256,7 +308,13 @@ object CertificatePhase extends DaisyPhase {
"( " + lowerBoundCoq + ", " + upperBoundCoq + ")"
}
private def holInterval(intv:(Rational,Rational)) :String =
private def hol4Interval(intv:(Rational,Rational)) :String =
intv match {
case (lowerBound, upperBound) =>
"( " + lowerBound.toFractionString + ", " + upperBound.toFractionString + ")"
}
private def holLightInterval(intv:(Rational,Rational)) :String =
intv match {
case (lowerBound, upperBound) =>
val loTmp = lowerBound.toFractionString.replace("(","(&")
......@@ -279,12 +337,23 @@ object CertificatePhase extends DaisyPhase {
(theFunction, "thePrecondition")
}
private def holPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
private def hol4Precondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "val thePrecondition_def = Define ` \n thePrecondition (n:num) = \n"
for ((id,intv) <- ranges) {
val ivHolLight = hol4Interval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHolLight + " else "
}
theFunction += "(0,1)`;"
(theFunction, "thePrecondition")
}
private def holLightPrecondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "let thePrecondition = define ` \n thePrecondition (n:num) = \n"
for ((id,intv) <- ranges) {
val ivHol = holInterval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHol + " else "
val ivHolLight = holLightInterval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHolLight + " else "
}
theFunction += "(&0,&1)`;;"
(theFunction, "thePrecondition")
......@@ -298,8 +367,10 @@ object CertificatePhase extends DaisyPhase {
}
if (prv == "coq"){
coqPrecondition(ranges)
}else if (prv == "hol4"){
hol4Precondition(ranges)
}else {
holPrecondition(ranges)
holLightPrecondition(ranges)
}
}
......@@ -362,56 +433,116 @@ object CertificatePhase extends DaisyPhase {
}
}
private def holAbsEnv (e:Expr, cont:String) :String =
private def hol4AbsEnv (e:Expr, cont:String) :String =
{
//must be set TODO:Assert?
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val intvE = hol4Interval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.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
"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
"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
"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
"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
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ _ =>
"" //TODO Can this happen?
}
}
private def holLightAbsEnv (e:Expr, 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("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ RealLiteral(r) =>
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + cont
case x @ Plus(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Minus(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Times(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
" else " + rFun
case x @ Division(lhs, rhs) =>
val lFun = holAbsEnv (lhs, cont)
val rFun = holAbsEnv (rhs, lFun)
val intvE = holInterval((x.interval.xlo,x.interval.xhi))
val lFun = holLightAbsEnv (lhs, cont)
val rFun = holLightAbsEnv (rhs, lFun)
val intvE = holLightInterval((x.interval.xlo,x.interval.xhi))
val errE = x.absError.toFractionString.replace("(","(&")
"if e = " + nameE +
" then (" + intvE + "," + errE + ")\n" +
......@@ -426,13 +557,21 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq")
("Definition absenv :analysisResult := \nfun (e:exp Q) =>\n"+ coqAbsEnv(e, "((0#1,0#1),0#1)") + ".",
"absenv")
else if (prv == "hol4")
("val absenv_def = Define `absenv:analysisResult = \n\\e. \n" + hol4AbsEnv(e, "((0,1),1)") + "`;",
"absenv")
else
("let absenv = define `absenv:analysisResult = \n\\e. \n" + holAbsEnv(e, "((&0,&1),&1)") + "`;;",
("let absenv = define `absenv:analysisResult = \n\\e. \n" + holLightAbsEnv(e, "((&0,&1),&1)") + "`;;",
"absenv")
private def getComputeExpr (lastGenName:String, analysisResultName:String,precondName:String, prover:String) :String=
if (prover == "coq")
"Eval compute in CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "."
"Theorem ErrorBoundSound :\n CertificateChecker " + lastGenName + " " +
analysisResultName + " " + precondName + " = true.\n" +
"Proof.\n cbv; auto.\nQed."
else if (prover == "hol4")
"val _ = store_thm (\"ErrorBoundSound\",\n ``CertificateChecker " +
lastGenName + " " + analysisResultName + " " + precondName + " = T``,\n EVAL_TAC);"
else
"DAISY_CONV CertificateChecker thePrecondition theRewrites `CertificateChecker " + lastGenName + " " + analysisResultName + " " + precondName + "`;;"
......@@ -470,7 +609,7 @@ object CertificatePhase extends DaisyPhase {
"DAISY_CONV CertificateChecker thePrecondition theRewrites `CertificateChecker " + nameE + " " + analysisResultName + " " + precondName + "`;;"
}
private def holExpList (e:Expr) :String =
private def holLightExpList (e:Expr) :String =
{
val nameE = expressionNames(e)
e match {
......@@ -480,23 +619,23 @@ object CertificatePhase extends DaisyPhase {
nameE
case x @ Plus(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
holLightExpList (lhs) + "; " +
holLightExpList (rhs) + "; " +
nameE
case x @ Minus(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
holLightExpList (lhs) + "; " +
holLightExpList (rhs) + "; " +
nameE
case x @ Times(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
holLightExpList (lhs) + "; " +
holLightExpList (rhs) + "; " +
nameE
case x @ Division(lhs, rhs) =>
holExpList (lhs) + "; " +
holExpList (rhs) + "; " +
holLightExpList (lhs) + "; " +
holLightExpList (rhs) + "; " +
nameE
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