diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sail_lib.ml | 4 | ||||
| -rw-r--r-- | src/value.ml | 6 |
2 files changed, 4 insertions, 6 deletions
diff --git a/src/sail_lib.ml b/src/sail_lib.ml index 7bb176c5..026172ec 100644 --- a/src/sail_lib.ml +++ b/src/sail_lib.ml @@ -599,7 +599,7 @@ let sub_real (x, y) = Rational.sub x y let abs_real x = Rational.abs x -let sqrt x = +let sqrt_real 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 @@ -649,8 +649,6 @@ let real_of_string str = | [whole] -> Rational.of_int (int_of_string str) | _ -> failwith "invalid real literal" -let sqrt_real x = failwith "sqrt_real" - let print str = Pervasives.print_string str let prerr str = Pervasives.prerr_string str diff --git a/src/value.ml b/src/value.ml index a4ce225e..729b3974 100644 --- a/src/value.ml +++ b/src/value.ml @@ -502,7 +502,7 @@ let value_random_real = function | _ -> failwith "value random_real" let value_sqrt_real = function - | [v] -> V_real (Sail_lib.sqrt (coerce_real v)) + | [v] -> V_real (Sail_lib.sqrt_real (coerce_real v)) | _ -> failwith "value sqrt_real" let value_quotient_real = function @@ -645,8 +645,8 @@ let primops = ("eq_real", value_eq_real); ("lt_real", value_lt_real); ("gt_real", value_gt_real); - ("lteq_real", value_lt_real); - ("gteq_real", value_gt_real); + ("lteq_real", value_lteq_real); + ("gteq_real", value_gteq_real); ("add_real", value_add_real); ("sub_real", value_sub_real); ("mult_real", value_mult_real); |