Commit 85891e72 authored by François Bobot's avatar François Bobot

gappa : rounding modes, Single.round, Double.round are syntax.

parent 247960c9
......@@ -141,6 +141,8 @@ end
theory floating_point.Single
syntax logic round "rnd_ieee32_%1(%2)"
prelude "@rnd_ieee32_ne=float<ieee_32,ne>;"
prelude "@rnd_ieee32_zr=float<ieee_32,zr>;"
prelude "@rnd_ieee32_up=float<ieee_32,up>;"
......@@ -151,6 +153,8 @@ end
theory floating_point.Double
syntax logic round "rnd_ieee64_%1(%2)"
prelude "@rnd_ieee64_ne=float<ieee_64,ne>;"
prelude "@rnd_ieee64_zr=float<ieee_64,zr>;"
prelude "@rnd_ieee64_up=float<ieee_64,up>;"
......@@ -159,6 +163,15 @@ theory floating_point.Double
end
theory floating_point.Rounding
syntax logic NearestTiesToEven "ne"
syntax logic ToZero "zr"
syntax logic Up "up"
syntax logic Down "dn"
syntax logic NearTiesToAway "na"
end
(*
Local Variables:
mode: why
......
......@@ -34,13 +34,10 @@ open Task
type info = {
info_symbols : Sid.t;
info_ops_of_rel : (bool * string * string) Mls.t;
rounding_modes : string Mls.t;
info_syn : string Mid.t;
info_rem : Sid.t;
}
let round_single = ref ps_equ
let round_double = ref ps_equ
let int_minus = ref ps_equ
let real_minus = ref ps_equ
......@@ -51,7 +48,6 @@ let find_th env file th =
let get_info =
let arith_symbols = ref None in
let ops_of_rels = ref Mls.empty in
let modes = ref Mls.empty in
let _inline = ref Sls.empty in
fun env task ->
let syn = get_syntax_map task in
......@@ -70,27 +66,16 @@ let get_info =
let real_ge = find_real "infix >=" in
let real_lt = find_real "infix <" in
let real_gt = find_real "infix >" in
let find_rounding_theory = find_th env "floating_point" "Rounding" in
let round_ne = find_rounding_theory "NearestTiesToEven" in
let round_zr = find_rounding_theory "ToZero" in
let round_up = find_rounding_theory "Up" in
let round_dn = find_rounding_theory "Down" in
let round_na = find_rounding_theory "NearTiesToAway" in
let find_single_theory = find_th env "floating_point" "Single" in
round_single := find_single_theory "round";
let find_double_theory = find_th env "floating_point" "Double" in
round_double := find_double_theory "round";
(*
let no_overflow_single = find_single_theory "no_overflow" in
*)
(* sets of known symbols *)
let l = Mid.fold (fun id _ -> Sid.add id) syn Sid.empty in
let l = Mid.map (Util.const ()) syn in
let l =
List.fold_right (fun ls -> Sid.add ls.ls_name)
[ps_equ;
int_le; int_ge; int_lt; int_gt;
real_le; real_ge; real_lt; real_gt;
!round_single; !round_double;
] l
in
arith_symbols := Some l;
......@@ -107,16 +92,6 @@ let get_info =
real_lt,false,">=","<=" ;
real_gt,false,"<=",">=" ;
];
modes :=
List.fold_left
(fun acc (ls,s) -> Mls.add ls s acc)
Mls.empty
[ round_ne, "ne" ;
round_zr, "zr" ;
round_up, "up" ;
round_dn, "dn" ;
round_na, "na" ;
];
(*
inline :=
List.fold_left
......@@ -131,7 +106,6 @@ let get_info =
{
info_symbols = l;
info_ops_of_rel = !ops_of_rels;
rounding_modes = !modes;
info_syn = syn;
info_rem = get_remove_set task;
}
......@@ -165,26 +139,18 @@ let constant_value t =
(* terms *)
let get_mode info m =
match m.t_node with
| Tapp(ls,[]) ->
begin try Mls.find ls info.rounding_modes
with Not_found -> assert false
end
| _ -> assert false
let rec print_term info fmt t =
let term = print_term info in
match t.t_node with
| Tconst c ->
Pretty.print_const fmt c
| Tvar { vs_name = id }
| Tapp ( { ls_name = id } ,[] ) ->
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp (ls, [m;t]) when ls_equal ls !round_single ->
fprintf fmt "rnd_ieee32_%s(%a)" (get_mode info m) term t
| Tapp (ls, [m;t]) when ls_equal ls !round_double ->
fprintf fmt "rnd_ieee64_%s(%a)" (get_mode info m) term t
| Tapp ( { ls_name = id } ,[] ) ->
begin match query_syntax info.info_syn id with
| Some s -> syntax_arguments s term fmt []
| None -> print_ident fmt id
end
| Tapp (ls, tl) ->
begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s term fmt tl
......@@ -209,7 +175,10 @@ let rec print_fmla info fmt f =
let fmla = print_fmla info in
match f.f_node with
| Fapp ({ ls_name = id }, []) ->
print_ident fmt id
begin match query_syntax info.info_syn id with
| Some s -> syntax_arguments s term fmt []
| None -> print_ident fmt id
end
| Fapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
(* TODO: distinguish between type of t1 and t2
the following is OK only for real of integer
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment