From b167a59affdb6428fa0656a092b335a3a6899d56 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 13 Dec 2018 16:20:48 +0000
Subject: Add hooks to call cgen stub file for RISC-V

---
 src/sail_lib.ml | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'src/sail_lib.ml')

diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index a718e6d5..620df900 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -578,8 +578,14 @@ let gteq_real (x, y) = Rational.geq x y
 let to_real x = Rational.of_int (Big_int.to_int x) (* FIXME *)
 let negate_real x = Rational.neg x
 
-let print_real (str, r) = print_string "REAL\n"
-let prerr_real (str, r) = prerr_string "REAL\n"
+let real_to_string x =
+  if Big_int.equal (Rational.den x) (Big_int.of_int 1) then
+    Big_int.to_string (Rational.num x)
+  else
+    Big_int.to_string (Rational.num x) ^ "/" ^ Big_int.to_string (Rational.den x)
+
+let print_real (str, r) = print_endline (str ^ real_to_string r)
+let prerr_real (str, r) = prerr_endline (str ^ real_to_string r)
 
 let round_down x = Rational.floor x (* Num.big_int_of_num (Num.floor_num x) *)
 let round_up x = Rational.ceiling x (* Num.big_int_of_num (Num.ceiling_num x) *)
@@ -592,6 +598,12 @@ let sub_real (x, y) = Rational.sub x y
 
 let abs_real x = Rational.abs x
 
+let sqrt x =
+  if Big_int.equal (Rational.den x) (Big_int.of_int 1) then
+    Big_int.sqrt (Rational.den x)
+  else
+    failwith "sqrt"
+
 let lt (x, y) = Big_int.less x y
 let gt (x, y) = Big_int.greater x y
 let lteq (x, y) = Big_int.less_equal x y
@@ -620,8 +632,7 @@ let real_of_string str =
   | [whole] -> Rational.of_int (int_of_string str)
   | _ -> failwith "invalid real literal"
 
-(* Not a very good sqrt implementation *)
-let sqrt_real x = failwith "sqrt_real" (* real_of_string (string_of_float (sqrt (Num.float_of_num x))) *)
+let sqrt_real x = failwith "sqrt_real"
 
 let print str = Pervasives.print_string str
 
-- 
cgit v1.2.3