From 6cd20c1106819f6dd331ff7e9e2125022e430e38 Mon Sep 17 00:00:00 2001
From: Sylvain <dailler@adacore.com>
Date: Thu, 22 Aug 2019 13:44:39 +0200
Subject: [PATCH] why3execute: Adding experimental version of exp and log

---
 bench/interp/real.mlw       | 13 +++++++++++++
 src/mlw/big_real.ml         | 18 +++++++++++++++++-
 src/mlw/big_real.mli        |  2 ++
 src/mlw/pinterp.ml          |  6 ++++++
 src/util/mlmpfr_dummy.ml    |  3 +++
 src/util/mlmpfr_wrapper.mli |  2 ++
 stdlib/real.mlw             |  4 ++--
 7 files changed, 45 insertions(+), 3 deletions(-)

diff --git a/bench/interp/real.mlw b/bench/interp/real.mlw
index 5cc155011..fad34c4f0 100644
--- a/bench/interp/real.mlw
+++ b/bench/interp/real.mlw
@@ -3,6 +3,7 @@ module R
   use real.Real
   use ref.Ref
   use real.Square
+  use real.ExpLog
 
   exception BenchFailure
 
@@ -23,6 +24,18 @@ module R
     let y : real = 1.0 / x in
     (x, y, 3.0 * y)
 
+  let test_exp () =
+    let x: real = 1.0 in
+    exp x
+
+  let test_log () =
+    let x: real = 1.0 in
+    log x
+
+  let test_exp_log () =
+    let x: real = 42.0 in
+    exp (log x), log x, exp x
+
   let bench1 ()
     (* Tries to calculate sqrt(2) *)
     diverges
diff --git a/src/mlw/big_real.ml b/src/mlw/big_real.ml
index b3fd4f133..79549ec8e 100644
--- a/src/mlw/big_real.ml
+++ b/src/mlw/big_real.ml
@@ -134,7 +134,7 @@ let div x y =
 
 let sqrt (xmin, xmax) =
   set_exponents ();
-  let prec = get_prec() in
+  let prec = get_prec () in
   let zero = get_zero () in
   if lessequal_p zero xmin then
     let res_min = sqrt ~rnd:Toward_Minus_Infinity ~prec xmin in
@@ -143,6 +143,22 @@ let sqrt (xmin, xmax) =
   else
     raise Undetermined
 
+let exp (xmin, xmax) =
+  set_exponents ();
+  let prec = get_prec () in
+  (exp ~rnd:Toward_Minus_Infinity ~prec xmin,
+   exp ~rnd:Toward_Plus_Infinity ~prec xmax)
+
+let log (xmin, xmax) =
+  set_exponents ();
+  let prec = get_prec () in
+  let zero = get_zero () in
+  if lessequal_p zero xmin then
+    (log ~rnd:Toward_Minus_Infinity ~prec xmin,
+     log ~rnd:Toward_Plus_Infinity ~prec xmax)
+  else
+    raise Undetermined
+
 let real_from_str s =
   let prec = get_prec () in
   let n1 = make_from_str ~prec ~base:10 ~rnd:Toward_Minus_Infinity s in
diff --git a/src/mlw/big_real.mli b/src/mlw/big_real.mli
index f6b1ad8b0..c267882ec 100644
--- a/src/mlw/big_real.mli
+++ b/src/mlw/big_real.mli
@@ -17,6 +17,8 @@ val add: real -> real -> real
 val mul: real -> real -> real
 val div: real -> real -> real
 val sqrt: real -> real
+val exp: real -> real
+val log: real -> real
 
 (* Real comparisons *)
 val eq: real -> real -> bool
diff --git a/src/mlw/pinterp.ml b/src/mlw/pinterp.ml
index ec7018b4f..881037ddc 100644
--- a/src/mlw/pinterp.ml
+++ b/src/mlw/pinterp.ml
@@ -486,10 +486,16 @@ let built_in_modules =
     ["pi", eval_real Modeconst (Big_real.pi());
     ]
   in
+  let real_exp_log =
+    ["real"], "ExpLog", [],
+    ["exp", eval_real Mode1r Big_real.exp;
+     "log", eval_real Mode1r Big_real.log]
+  in
   bool_module :: (int_modules @ [array_module;
                                  real_module;
                                  real_square_module;
                                  real_trigo_module;
+                                 real_exp_log;
                                  mode_module;
                                  float_modules 32 ~prec:24 "Float32";
                                  float_modules 64 ~prec:53 "Float64";])
diff --git a/src/util/mlmpfr_dummy.ml b/src/util/mlmpfr_dummy.ml
index 772daa065..ddd932a0d 100644
--- a/src/util/mlmpfr_dummy.ml
+++ b/src/util/mlmpfr_dummy.ml
@@ -28,6 +28,9 @@ let sub ?rnd:_ ?prec:_ _ _ = raise Not_Implemented
 let abs ?rnd:_ ?prec:_ _ = raise Not_Implemented
 let fma ?rnd:_ ?prec:_ _ _ _ = raise Not_Implemented
 let rint ?rnd:_ ?prec:_ _ = raise Not_Implemented
+let exp ?rnd:_ ?prec:_ _ = raise Not_Implemented
+let log ?rnd:_ ?prec:_ _ = raise Not_Implemented
+
 
 let min ?rnd:_ ?prec:_ _ _ = raise Not_Implemented
 let max ?rnd:_ ?prec:_ _ _ = raise Not_Implemented
diff --git a/src/util/mlmpfr_wrapper.mli b/src/util/mlmpfr_wrapper.mli
index 28c6ecfaa..a954cfe14 100644
--- a/src/util/mlmpfr_wrapper.mli
+++ b/src/util/mlmpfr_wrapper.mli
@@ -36,6 +36,8 @@ val sub: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float -> mpfr_float
 val abs: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
 val fma: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float -> mpfr_float -> mpfr_float
 val rint: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
+val exp : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
+val log : ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float
 
 
 val min: ?rnd:mpfr_rnd_t -> ?prec:int -> mpfr_float -> mpfr_float -> mpfr_float
diff --git a/stdlib/real.mlw b/stdlib/real.mlw
index bcfa9504e..1f0757658 100644
--- a/stdlib/real.mlw
+++ b/stdlib/real.mlw
@@ -228,13 +228,13 @@ module ExpLog
 
   use Real
 
-  function exp real : real
+  val function exp real : real
   axiom Exp_zero : exp(0.0) = 1.0
   axiom Exp_sum : forall x y:real. exp (x+y) = exp x * exp y
 
   constant e : real = exp 1.0
 
-  function log real : real
+  val function log real : real
   axiom Log_one : log 1.0 = 0.0
   axiom Log_mul :
     forall x y:real. x > 0.0 /\ y > 0.0 -> log (x*y) = log x + log y
-- 
GitLab