Improve the formatting of [if then else] expressions

1 files changed, 24 insertions, 15 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 9aaf753e..13c02bca 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1476,25 +1476,34 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_open_hovbox fmt ctx.indent_incr;
         let then_or_else = if is_then then "then" else "else" in
         F.pp_print_string fmt then_or_else;
-        F.pp_print_space fmt ();
-        (* Open a box for the branch *)
-        F.pp_open_hovbox fmt ctx.indent_incr;
-        (* Print the [begin] if necessary *)
         let parenth = PureUtils.let_group_requires_parentheses e_branch in
-        let left_delim, right_delim =
-          match !backend with FStar -> ("begin", "end") | Coq -> ("(", ")")
-        in
-        if parenth then (
-          F.pp_print_string fmt left_delim;
-          F.pp_print_space fmt ());
+        (* Open a box for the branch - we do this only if it is not a parenthesized
+           group of nested let bindings.
+        *)
+        if not parenth then (
+          F.pp_print_space fmt ();
+          F.pp_open_hovbox fmt ctx.indent_incr);
+        (* Open the parenthesized expression *)
+        (if parenth then
+         match !backend with
+         | FStar ->
+             F.pp_print_space fmt ();
+             F.pp_print_string fmt "begin";
+             F.pp_print_space fmt ()
+         | Coq ->
+             F.pp_print_string fmt " (";
+             F.pp_print_cut fmt ());
         (* Print the branch expression *)
         extract_texpression ctx fmt false e_branch;
-        (* Close the [begin ... end ] *)
-        if parenth then (
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt right_delim);
+        (* Close the parenthesized expression *)
+        (if parenth then
+         match !backend with
+         | FStar ->
+             F.pp_print_space fmt ();
+             F.pp_print_string fmt "end"
+         | Coq -> F.pp_print_string fmt ")");
         (* Close the box for the branch *)
-        F.pp_close_box fmt ();
+        if not parenth then F.pp_close_box fmt ();
         (* Close the box for the then/else+branch *)
         F.pp_close_box fmt ()
       in