Merge pull request #1676 from GaloisInc/T1663-roundAway-reference-eval

Fix `roundAway` implementation in reference evaluator
GaloisInc · Jun 1, 2024 · 22d3277 · 22d3277
2 parents 3ff9a82 + f380e10
commit 22d3277
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 1 deletion.
diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs
@@ -726,7 +726,7 @@ by corresponding type classes:
 >                      (eitherToE . FP.floatToInteger "trunc" FP.ToZero))
 >
 >   , "roundAway"  ~> unary (roundUnary roundAwayRat
->                      (eitherToE . FP.floatToInteger "roundAway" FP.Away))
+>                      (eitherToE . FP.floatToInteger "roundAway" FP.NearAway))
 >
 >   , "roundToEven"~> unary (roundUnary round
 >                      (eitherToE . FP.floatToInteger "roundToEven" FP.NearEven))

diff --git a/tests/issues/issue1663.icry b/tests/issues/issue1663.icry
@@ -0,0 +1,12 @@
+:module Float
+let x = 3.5 : Float32
+:eval floor x
+floor x
+:eval ceiling x
+ceiling x
+:eval trunc x
+trunc x
+:eval roundToEven x
+roundToEven x
+:eval roundAway x
+roundAway x
diff --git a/tests/issues/issue1663.icry.stdout b/tests/issues/issue1663.icry.stdout
@@ -0,0 +1,13 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Float
+3
+3
+4
+4
+3
+3
+4
+4
+4
+4