diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/constant_fold.ml | 1 | ||||
| -rw-r--r-- | src/sail_lib.ml | 37 | ||||
| -rw-r--r-- | src/value.ml | 44 |
3 files changed, 70 insertions, 12 deletions
diff --git a/src/constant_fold.ml b/src/constant_fold.ml index b86f4ea5..9e474912 100644 --- a/src/constant_fold.ml +++ b/src/constant_fold.ml @@ -96,6 +96,7 @@ let safe_primops = "print_bits"; "print_int"; "print_string"; + "print_real"; "prerr_bits"; "prerr_int"; "prerr_string"; diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 620df900..7bb176c5 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -578,20 +578,21 @@ 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 real_to_string x = +let string_of_real 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 print_real (str, r) = print_endline (str ^ string_of_real r) +let prerr_real (str, r) = prerr_endline (str ^ string_of_real 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) *) +let round_down x = Rational.floor x +let round_up x = Rational.ceiling x let quotient_real (x, y) = Rational.div x y -let mult_real (x, y) = Rational.mul x y (* Num.mult_num x y *) -let real_power (x, y) = failwith "real_power" (* Num.power_num x (Num.num_of_big_int y) *) +let div_real (x, y) = Rational.div x y +let mult_real (x, y) = Rational.mul x y +let real_power (x, y) = failwith "real_power" let int_power (x, y) = Big_int.pow_int x (Big_int.to_int y) let add_real (x, y) = Rational.add x y let sub_real (x, y) = Rational.sub x y @@ -599,10 +600,26 @@ 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) + let precision = 30 in + let s = Big_int.sqrt (Rational.num x) in + if Big_int.equal (Rational.den x) (Big_int.of_int 1) && Big_int.equal (Big_int.mul s s) (Rational.num x) then + to_real s else - failwith "sqrt" + let p = ref (to_real (Big_int.sqrt (Big_int.div (Rational.num x) (Rational.den x)))) in + let n = ref (Rational.of_int 0) in + let convergence = ref (Rational.div (Rational.of_int 1) (Rational.of_big_int (Big_int.pow_int_positive 10 precision))) in + let quit_loop = ref false in + while not !quit_loop do + n := Rational.div (Rational.add !p (Rational.div x !p)) (Rational.of_int 2); + + if Rational.lt (Rational.abs (Rational.sub !p !n)) !convergence then + quit_loop := true + else + p := !n + done; + !n + +let random_real () = Rational.div (Rational.of_int (Random.bits ())) (Rational.of_int (Random.bits())) let lt (x, y) = Big_int.less x y let gt (x, y) = Big_int.greater x y diff --git a/src/value.ml b/src/value.ml index 589e956a..a4ce225e 100644 --- a/src/value.ml +++ b/src/value.ml @@ -388,7 +388,7 @@ let rec string_of_value = function | V_unit -> "()" | V_string str -> "\"" ^ str ^ "\"" | V_ref str -> "ref " ^ str - | V_real r -> "REAL" (* No Rational.to_string *) + | V_real r -> Sail_lib.string_of_real r | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")" | V_record record -> "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}" @@ -493,6 +493,18 @@ let value_to_real = function | [v] -> V_real (Sail_lib.to_real (coerce_int v)) | _ -> failwith "value to_real" +let value_print_real = function + | [v1; v2] -> output_endline (coerce_string v1 ^ string_of_value v2); V_unit + | _ -> failwith "value print_real" + +let value_random_real = function + | [_] -> V_real (Sail_lib.random_real ()) + | _ -> failwith "value random_real" + +let value_sqrt_real = function + | [v] -> V_real (Sail_lib.sqrt (coerce_real v)) + | _ -> failwith "value sqrt_real" + let value_quotient_real = function | [v1; v2] -> V_real (Sail_lib.quotient_real (coerce_real v1, coerce_real v2)) | _ -> failwith "value quotient_real" @@ -505,6 +517,26 @@ let value_round_down = function | [v] -> V_int (Sail_lib.round_down (coerce_real v)) | _ -> failwith "value round_down" +let value_add_real = function + | [v1; v2] -> V_real (Sail_lib.add_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value add_real" + +let value_sub_real = function + | [v1; v2] -> V_real (Sail_lib.sub_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value sub_real" + +let value_mult_real = function + | [v1; v2] -> V_real (Sail_lib.mult_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value mult_real" + +let value_div_real = function + | [v1; v2] -> V_real (Sail_lib.div_real (coerce_real v1, coerce_real v2)) + | _ -> failwith "value div_real" + +let value_abs_real = function + | [v] -> V_real (Sail_lib.abs_real (coerce_real v)) + | _ -> failwith "value abs_real" + let value_eq_real = function | [v1; v2] -> V_bool (Sail_lib.eq_real (coerce_real v1, coerce_real v2)) | _ -> failwith "value eq_real" @@ -615,9 +647,17 @@ let primops = ("gt_real", value_gt_real); ("lteq_real", value_lt_real); ("gteq_real", value_gt_real); + ("add_real", value_add_real); + ("sub_real", value_sub_real); + ("mult_real", value_mult_real); ("round_up", value_round_up); ("round_down", value_round_down); - ("quotient_real", value_quotient_real); + ("quotient_real", value_div_real); + ("abs_real", value_abs_real); + ("div_real", value_div_real); + ("sqrt_real", value_sqrt_real); + ("print_real", value_print_real); + ("random_real", value_random_real); ("undefined_unit", fun _ -> V_unit); ("undefined_bit", fun _ -> V_bit Sail_lib.B0); ("undefined_int", fun _ -> V_int Big_int.zero); |