diff --git a/include/mpfr_lustre.c b/include/mpfr_lustre.c index bea22e579fbc4d89533f675dfa932d0631b7692a..b8f427b2949c42ad3472df4856efea45490d73a2 100644 --- a/include/mpfr_lustre.c +++ b/include/mpfr_lustre.c @@ -101,6 +101,54 @@ void MPFRint_to_real_step (int i, mpfr_t out) { mpfr_set_si(out, i, MPFR_RNDN); } + +void MPFRreal_to_int_step (mpfr_t in1, int *out) +{ + *out = mpfr_get_sj (in1, MPFR_RNDN); +} + +void MPFRFloor (mpfr_t in1, int *out) +{ + mpfr_t tmp; + int prec; + mpfr_init (tmp); // would be better to avoid local init + prec = mpfr_get_prec (in1); + mpfr_set_prec(tmp, prec); + + mpfr_floor(tmp, in1); + *out = mpfr_get_sj (tmp, MPFR_RNDN); + + mpfr_clear(tmp); +} + +void MPFRCeiling (mpfr_t in1, int *out) +{ + mpfr_t tmp; + int prec; + mpfr_init (tmp); // would be better to avoid local init + prec = mpfr_get_prec (in1); + mpfr_set_prec(tmp, prec); + + mpfr_ceil(tmp, in1); + *out = mpfr_get_sj (tmp, MPFR_RNDN); + + mpfr_clear(tmp); +} + +void MPFRRound (mpfr_t in1, int *out) +{ + mpfr_t tmp; + int prec; + mpfr_init (tmp); // would be better to avoid local init + prec = mpfr_get_prec (in1); + mpfr_set_prec(tmp, prec); + + mpfr_round(tmp, in1); + *out = mpfr_get_sj (tmp, MPFR_RNDN); + + mpfr_clear(tmp); +} + // functions of lustrec_math void MPFRacos_step (mpfr_t i, mpfr_t out diff --git a/include/mpfr_lustre.lusi b/include/mpfr_lustre.lusi index 801d53af29c699e534b8a5b1873a6f877cf7fb41..6e7f0f9be51bdb482618ab87f64f6f2fcae42e54 100644 --- a/include/mpfr_lustre.lusi +++ b/include/mpfr_lustre.lusi @@ -22,6 +22,10 @@ function MPFRNeq(i1, i2: real) returns (out: bool); -- Functions already available in conv function MPFRint_to_real (x: int) returns (y: real); +function MPFRreal_to_int (in1: real) returns (out: int); +function MPFRFloor (in1: real) returns (out: int); +function MPFRCeiling (in1: real) returns (out: int); +function MPFRRound (in1: real) returns (out: int); -- Functions already available in lustrec_math diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml index 9536034dde77636d4a3db4acb818c7be19361b65..462de54dd05a246e2a4677231526db488b550017 100644 --- a/src/backends/C/c_backend_common.ml +++ b/src/backends/C/c_backend_common.ml @@ -723,13 +723,16 @@ let print_put_var fmt file_suffix name var_type var_id = pp_file fmt "i" var_id ) else if Types.is_real_type unclocked_t then - let _ = - if !Options.mpfr then - fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@ " name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double - else - fprintf fmt "_put_double(\"%s\", %s, %i);@ " name var_id !Options.print_prec_double - in - pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", " ^ var_id) + + if !Options.mpfr then ( + fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s), %i);@ " name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double; + pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", mpfr_get_d(" ^ var_id ^ ", MPFR_RNDN)") + ) + else ( + fprintf fmt "_put_double(\"%s\", %s, %i);@ " name var_id !Options.print_prec_double; + pp_file fmt ".*f" ((string_of_int !Options.print_prec_double) ^ ", " ^ var_id) + ) + else (Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false) diff --git a/src/plugins/mpfr/mpfr.ml b/src/plugins/mpfr/mpfr.ml index 76ea13bf6f97927f520bfa4de2775f202e932f60..0f43e6d772e84b34753c6b0ea98b2271951f8908 100644 --- a/src/plugins/mpfr/mpfr.ml +++ b/src/plugins/mpfr/mpfr.ml @@ -16,6 +16,8 @@ open Corelang open Normalization open Machine_code_common +let report = Log.report ~plugin:"MPFR" + let mpfr_module = mktop (Open(false, "mpfr_lustre")) let cpt_fresh = ref 0 @@ -99,6 +101,14 @@ let base_inject_op id = | "!=" -> "MPFRNeq" (* Conv functions *) | "int_to_real" -> "MPFRint_to_real" + | "real_to_int" -> "MPFRreal_to_int" + | "_floor" -> "MPFRfloor" + | "_ceil" -> "MPFRceil" + | "_round" -> "MPFRround" + | "_Floor" -> "MPFRFloor" + | "_Ceiling" -> "MPFRCeiling" + | "_Round" -> "MPFRRound" + (* Math library functions *) | "acos" -> "MPFRacos" | "acosh" -> "MPFRacosh" @@ -128,7 +138,7 @@ let base_inject_op id = | _ -> raise Not_found let inject_op id = - Format.eprintf "trying to inject mpfr into function %s@." id; + report ~level:3 (fun fmt -> Format.fprintf fmt "trying to inject mpfr into function %s@." id); try base_inject_op id with Not_found -> id