Commit 375ca08b authored by ='s avatar =

Removing the use of nextFreshVariableIdentifier, we are now using the globalId...

Removing the use of nextFreshVariableIdentifier, we are now using the globalId of the Identifier object.
parent dbd5e2eb
......@@ -115,7 +115,6 @@ 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(prover:String, fname:String) :String=
if (prover == "coq")
......@@ -137,27 +136,26 @@ object CertificatePhase extends DaisyPhase {
}
}
private def coqVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
private def coqVariable(vname:Identifier, reporter:Reporter) :(String, String) =
{
//FIXME: Ugly Hack to get disjoint names for multiple function encodings with same variable names:
val freshId = nextFreshVariable()
val theExpr = s"Definition ExpVar$vname$freshId :exp Q := Var Q $id.\n"
(theExpr,s"ExpVar$vname$freshId")
val name = s"ExpVar$vname${vname.globalId}"
val theExpr = s"Definition $name :exp Q := Var Q ${vname.globalId}.\n"
(theExpr,name)
}
private def hol4Variable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
private def hol4Variable(vname:Identifier, reporter:Reporter) :(String, String) =
{
//FIXME: Ugly Hack to get disjoint names for multiple function encodings with same variable names:
val freshId = nextFreshVariable()
val theExpr = s"val ExpVar$vname${freshId}_def = Define `ExpVar$vname$freshId:(real exp) = Var $id`;\n"
(theExpr, s"ExpVar$vname$freshId")
val name = s"ExpVar$vname${vname.globalId}"
val theExpr = s"val ${name}_def = Define `$name:(real exp) = Var ${vname.globalId}`;\n"
(theExpr, name)
}
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")
}
private def holLightVariable(vname:Identifier, reporter:Reporter) :(String, String) =
{
val name = s"ExpVar$vname"
val theExpr = s"let $name = define `$name:(real)exp = Param ${vname.globalId}`;;\n"
(theExpr, s"ExpVar$vname")
}
private def coqConstant(r:RealLiteral, id:Int, precision:Precision, reporter:Reporter) :(String, String) =
r match {
......@@ -270,15 +268,14 @@ object CertificatePhase extends DaisyPhase {
if (identifierNums.contains(id)){
("",expressionNames(e))
}else{
val varId = nextFreshVariable()
identifierNums += (id -> varId)
identifierNums += (id -> id.globalId)
val (definition, name) =
if (prv == "coq"){
coqVariable (id, varId, reporter)
coqVariable (id, reporter)
}else if (prv == "hol4"){
hol4Variable (id, varId, reporter)
hol4Variable (id, reporter)
}else {
holLightVariable (id,varId,reporter)
holLightVariable (id, reporter)
}
expressionNames += (e -> name)
(definition,name)
......@@ -401,13 +398,13 @@ object CertificatePhase extends DaisyPhase {
//first compute expression AST
val (expDef, expName) = getValues (exp, precision, constPrecision, reporter,prv)
//now allocate a new variable
val varId = nextFreshVariable()
val varId = x.globalId
identifierNums += (x -> varId)
val (varDef, varName) =
if (prv == "coq"){
coqVariable (x, varId, reporter)
coqVariable (x, reporter)
}else{
hol4Variable (x, varId, reporter)
hol4Variable (x, reporter)
}
expressionNames += (Variable(x) -> varName)
//now recursively compute the command
......
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