Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
AVA
FloVer
Commits
7e46da88
Commit
7e46da88
authored
Sep 20, 2016
by
Heiko Becker
Browse files
Next fix
parent
0fef1430
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/main/scala/daisy/backend/CertificatePhase.scala
View file @
7e46da88
...
...
@@ -25,7 +25,7 @@ object CertificatePhase extends DaisyPhase {
def
writeToFile
(
fileContent
:
String
,
prover
:
String
,
fname
:
String
){
import
java.io.FileWriter
import
java.io.BufferedWriter
val
fileLocation
=
"./output/certificate_"
+
fname
val
fileLocation
=
"./output/certificate_"
+
prg
.
id
+
fname
val
fstream
=
if
(
prover
==
"coq"
)
new
FileWriter
(
fileLocation
+
".v"
)
...
...
@@ -99,7 +99,7 @@ object CertificatePhase extends DaisyPhase {
private
def
coqConstant
(
r
:
RealLiteral
,
id
:
Int
,
reporter
:
Reporter
)
:
(
String
,
String
)
=
r
match
{
case
RealLiteral
(
v
)
=>
val
rationalStr
=
v
.
toString
val
rationalStr
=
v
.
to
Fraction
String
val
coqRational
=
rationalStr
.
replace
(
'/'
,
'#'
)
val
theValue
=
s
"Definition cst$id :Q := ${coqRational}.\n"
val
theExpr
=
s
"Definition ExpCst$id :exp Q := Const cst$id.\n"
...
...
@@ -109,7 +109,7 @@ object CertificatePhase extends DaisyPhase {
private
def
holConstant
(
r
:
RealLiteral
,
id
:
Int
,
reporter
:
Reporter
)
:
(
String
,
String
)
=
r
match
{
case
RealLiteral
(
v
)
=>
val
rationalStr
=
v
.
toString
val
rationalStr
=
v
.
to
Fraction
String
val
holRational
=
rationalStr
.
replace
(
"("
,
"(&"
)
val
theValue
=
s
"let cst$id = define `cst$id:real = ${holRational}`;;\n"
val
theExpr
=
s
"let ExpCst$id = define `ExpCst$id:(real)exp = Const cst$id`;;\n"
...
...
@@ -125,7 +125,7 @@ object CertificatePhase extends DaisyPhase {
(
"Definition Sub"
+
nameLHS
+
nameRHS
+
s
" :exp Q := Binop Sub $nameLHS $nameRHS.\n"
,
"Sub"
+
nameLHS
+
nameRHS
)
case
x
@
Times
(
lhs
,
rhs
)
=>
(
"Definition Mul"
+
nameLHS
+
nameRHS
+
s
" :exp Q := Binop Mult $nameLHS $nameRHS.\n"
,
(
"Definition Mul
t
"
+
nameLHS
+
nameRHS
+
s
" :exp Q := Binop Mult $nameLHS $nameRHS.\n"
,
"Mult"
+
nameLHS
+
nameRHS
)
case
x
@
_
=>
reporter
.
fatalError
(
"Unsupported value"
)
...
...
@@ -140,8 +140,8 @@ object CertificatePhase extends DaisyPhase {
(
"let Sub"
+
nameLHS
+
nameRHS
+
" = define `Sub"
+
nameLHS
+
nameRHS
+
s
":(real)exp = Binop Sub $nameLHS $nameRHS`;;\n"
,
"Sub"
+
nameLHS
+
nameRHS
)
case
x
@
Times
(
lhs
,
rhs
)
=>
(
"let Mul"
+
nameLHS
+
nameRHS
+
" = define `Mul"
+
nameLHS
+
nameRHS
+
s
":(real)exp = Binop Mult $nameLHS $nameRHS`;;\n"
,
"Mul"
+
nameLHS
+
nameRHS
)
(
"let Mul
t
"
+
nameLHS
+
nameRHS
+
" = define `Mul"
+
nameLHS
+
nameRHS
+
s
":(real)exp = Binop Mult $nameLHS $nameRHS`;;\n"
,
"Mul
t
"
+
nameLHS
+
nameRHS
)
case
x
@
_
=>
reporter
.
fatalError
(
"Unsupported value"
)
}
...
...
@@ -218,7 +218,7 @@ object CertificatePhase extends DaisyPhase {
(
definition
,
name
)
case
x
@
_
=>
reporter
.
fatalError
(
"Unsupported operation"
)
reporter
.
fatalError
(
s
"Unsupported operation"
)
}
...
...
@@ -226,16 +226,16 @@ object CertificatePhase extends DaisyPhase {
private
def
coqInterval
(
intv
:
(
Rational
,
Rational
))
:
String
=
intv
match
{
case
(
lowerBound
,
upperBound
)
=>
val
lowerBoundCoq
=
lowerBound
.
toString
.
replace
(
'/'
,
'#'
)
val
upperBoundCoq
=
upperBound
.
toString
.
replace
(
'/'
,
'#'
)
val
lowerBoundCoq
=
lowerBound
.
to
Fraction
String
.
replace
(
'/'
,
'#'
)
val
upperBoundCoq
=
upperBound
.
to
Fraction
String
.
replace
(
'/'
,
'#'
)
"( "
+
lowerBoundCoq
+
", "
+
upperBoundCoq
+
")"
}
private
def
holInterval
(
intv
:
(
Rational
,
Rational
))
:
String
=
intv
match
{
case
(
lowerBound
,
upperBound
)
=>
val
lowerBoundHol
=
lowerBound
.
toString
.
replace
(
"("
,
"(&"
)
val
upperBoundHol
=
upperBound
.
toString
.
replace
(
"("
,
"(&"
)
val
lowerBoundHol
=
lowerBound
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
val
upperBoundHol
=
upperBound
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
"( "
+
lowerBoundHol
+
", "
+
upperBoundHol
+
")"
}
...
...
@@ -283,14 +283,14 @@ object CertificatePhase extends DaisyPhase {
e
match
{
case
x
@
Variable
(
id
)
=>
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"/"
,
"#"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"/"
,
"#"
)
"if exp_eq_bool 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
.
toString
.
replace
(
"/"
,
"#"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"/"
,
"#"
)
"if exp_eq_bool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
...
...
@@ -299,7 +299,7 @@ object CertificatePhase extends DaisyPhase {
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"/"
,
"#"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"/"
,
"#"
)
"if exp_eq_bool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -308,7 +308,7 @@ object CertificatePhase extends DaisyPhase {
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"/"
,
"#"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"/"
,
"#"
)
"if exp_eq_bool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -317,7 +317,7 @@ object CertificatePhase extends DaisyPhase {
val
lFun
=
coqAbsEnv
(
lhs
,
cont
)
val
rFun
=
coqAbsEnv
(
rhs
,
lFun
)
val
intvE
=
coqInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"/"
,
"#"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"/"
,
"#"
)
"if exp_eq_bool e "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -334,14 +334,14 @@ object CertificatePhase extends DaisyPhase {
e
match
{
case
x
@
Variable
(
id
)
=>
val
intvE
=
holInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"("
,
"(&"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
case
x
@
RealLiteral
(
r
)
=>
val
intvE
=
holInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"("
,
"(&"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
cont
...
...
@@ -350,7 +350,7 @@ object CertificatePhase extends DaisyPhase {
val
lFun
=
holAbsEnv
(
lhs
,
cont
)
val
rFun
=
holAbsEnv
(
rhs
,
lFun
)
val
intvE
=
holInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"("
,
"(&"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -359,7 +359,7 @@ object CertificatePhase extends DaisyPhase {
val
lFun
=
holAbsEnv
(
lhs
,
cont
)
val
rFun
=
holAbsEnv
(
rhs
,
lFun
)
val
intvE
=
holInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"("
,
"(&"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
@@ -368,7 +368,7 @@ object CertificatePhase extends DaisyPhase {
val
lFun
=
holAbsEnv
(
lhs
,
cont
)
val
rFun
=
holAbsEnv
(
rhs
,
lFun
)
val
intvE
=
holInterval
((
x
.
interval
.
xlo
,
x
.
interval
.
xhi
))
val
errE
=
x
.
absError
.
toString
.
replace
(
"("
,
"(&"
)
val
errE
=
x
.
absError
.
to
Fraction
String
.
replace
(
"("
,
"(&"
)
"if e = "
+
nameE
+
" then ("
+
intvE
+
","
+
errE
+
")\n"
+
" else "
+
rFun
...
...
src/main/scala/daisy/utils/Rational.scala
View file @
7e46da88
...
...
@@ -412,7 +412,7 @@ class Rational private(val n: BigInt, val d: BigInt) extends ScalaNumber with Sc
def
toFractionString
:
String
=
"(%s)/(%s)"
.
format
(
n
.
toString
,
d
.
toString
)
override
def
toString
:
String
=
toFractionString
override
def
toString
:
String
=
niceDoubleString
(
this
.
toDouble
)
def
integerPart
:
Int
=
doubleValue
.
toInt
def
longPart
:
Long
=
doubleValue
.
toLong
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment