diff --git a/src/options.ml b/src/options.ml index 1eca8d39cacb7dfd35704a1dd7832a05cb0d8fde..4ab3b3f6e04c02619f2ee1c285d472e1f06b5960 100755 --- a/src/options.ml +++ b/src/options.ml @@ -32,7 +32,7 @@ let lusi = ref false let print_reuse = ref false let const_unfold = ref false let mpfr = ref false -let mpfr_prec = ref 0 +let mpfr_prec = ref 100 let print_dec_types = ref false let traces = ref false diff --git a/src/options_management.ml b/src/options_management.ml index 1a052fb40376f66e9e758e756805f1910d10adfd..bdda79c77f7d6dbbea3fb4bd2b63dc2ba7ba6612 100644 --- a/src/options_management.ml +++ b/src/options_management.ml @@ -66,11 +66,20 @@ let set_mpfr prec = if prec > 0 then ( mpfr := true; mpfr_prec := prec; + real_type := "mpfr"; (* salsa_enabled := false; (* We deactivate salsa *) TODO *) ) else failwith "mpfr requires a positive integer" +let set_real_type s = + match s with + "mpfr" -> ( + mpfr := true; + real_type := "mpfr"; + ) + | _ -> real_type := s + let set_backend s = output := s; Backends.setup () @@ -113,7 +122,7 @@ let lustrec_options = "-c++" , Arg.Set cpp , "c++ backend"; "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")"; - "-real", Arg.Set_string real_type, "specifies the real type (default=\"double\" without mpfr option)"; + "-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)"; "-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)"; "-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code";