Commit 3af79fbd authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove superfluous parentheses around some patterns in Coq printer.

parent 4f4532e0
......@@ -652,8 +652,7 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
(~ (is_positive x) ->
(t'isFinite x) /\
((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%R))
| (ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE) =>
is_infinite x
| ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE => is_infinite x
end.
(* Why3 assumption *)
......
......@@ -660,8 +660,7 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
(t'isFinite x) /\
((t'real x) =
(-(9007199254740991 * 19958403095347198116563727130368385660674512604354575415025472424372118918689640657849579654926357010893424468441924952439724379883935936607391717982848314203200056729510856765175377214443629871826533567445439239933308104551208703888888552684480441575071209068757560416423584952303440099278848)%R)%R))
| (ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE) =>
is_infinite x
| ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE => is_infinite x
end.
(* Why3 assumption *)
......
......@@ -1889,8 +1889,7 @@ Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
| ieee_float.RoundingMode.RTZ =>
((is_positive x) -> (is_finite x) /\ ((to_real x) = max_real)) /\
(~ (is_positive x) -> (is_finite x) /\ ((to_real x) = (-max_real)%R))
| (ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE) =>
is_infinite x
| ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE => is_infinite x
end.
(* Why3 assumption *)
......
......@@ -200,27 +200,28 @@ let unambig_fs fs =
let lparen_r fmt () = fprintf fmt "@[<1>("
let rparen_r fmt () = fprintf fmt ")@]"
let print_paren_r fmt x =
print_list_delim ~start:lparen_r ~stop:rparen_r ~sep:comma fmt x
let print_paren_r f =
print_list_delim ~start:lparen_r ~stop:rparen_r ~sep:comma f
let arrow fmt () = fprintf fmt " ->@ "
let print_arrow_list fmt x = print_list_suf arrow fmt x
let rec print_pat info fmt p = match p.pat_node with
let rec print_pattern info fmt p = print_pat false info fmt p
and print_pat op info fmt p = match p.pat_node with
| Pwild -> fprintf fmt "_"
| Pvar v -> print_vs fmt v
| Pas (p,v) ->
fprintf fmt "(%a as %a)" (print_pat info) p print_vs v
fprintf fmt (protect_on op "%a as %a") (print_pat true info) p print_vs v
| Por (p,q) ->
fprintf fmt "(%a|%a)" (print_pat info) p (print_pat info) q
fprintf fmt (protect_on op "%a|%a") (print_pat true info) p (print_pat true info) q
| Papp (cs,pl) when is_fs_tuple cs ->
fprintf fmt "%a" (print_paren_r (print_pat info)) pl
print_paren_r (print_pat false info) fmt pl
| Papp (cs,pl) ->
begin match query_syntax info.info_syn cs.ls_name with
| Some s -> syntax_arguments s (print_pat info) fmt pl
| _ when pl = [] -> (print_ls_real info) fmt cs
| _ -> fprintf fmt "@[<1>(%a@ %a)@]"
(print_ls_real info) cs (print_list space (print_pat info)) pl
| Some s -> syntax_arguments s (print_pat true info) fmt pl
| _ when pl = [] -> print_ls_real info fmt cs
| _ -> fprintf fmt (protect_on op "%a@ %a")
(print_ls_real info) cs (print_list space (print_pat true info)) pl
end
let print_vsty info fmt v =
......@@ -343,7 +344,7 @@ and print_tnode ?(boxed=false) opl opr info fmt t = match t.t_node with
and print_tbranch info fmt br =
let p,t = t_open_branch br in
fprintf fmt "@[<4>| %a =>@ %a@]"
(print_pat info) p (print_term info) t;
(print_pattern info) p (print_term info) t;
Svs.iter forget_var p.pat_vars
(** Declarations *)
......
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