Improve the formatting of [if then else] expressions

3 files changed, 94 insertions, 101 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
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 9075d01d..774b8a1e 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -210,13 +210,12 @@ Definition choose_test_fwd : result unit :=
   z0 <- i32_add z 1 %i32;
   if negb (z0 s= 1 %i32)
   then Fail_
-  else
-    (
-      p <- choose_back i32 true (0 %i32) (0 %i32) z0;
-      let (x, y) := p in
-      if negb (x s= 1 %i32)
-      then Fail_
-      else if negb (y s= 0 %i32) then Fail_ else Return tt )
+  else (
+    p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+    let (x, y) := p in
+    if negb (x s= 1 %i32)
+    then Fail_
+    else if negb (y s= 0 %i32) then Fail_ else Return tt)
   .
 
 (** Unit test for [no_nested_borrows::choose_test] *)
@@ -258,7 +257,7 @@ Fixpoint list_nth_shared_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   | ListCons x tl =>
     if i s= 0 %u32
     then Return x
-    else ( i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t )
+    else (i0 <- u32_sub i 1 %u32; t <- list_nth_shared_fwd T tl i0; Return t)
   | ListNil => Fail_
   end
   .
@@ -269,7 +268,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   | ListCons x tl =>
     if i s= 0 %u32
     then Return x
-    else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t )
+    else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
   | ListNil => Fail_
   end
   .
@@ -281,11 +280,10 @@ Fixpoint list_nth_mut_back
   | ListCons x tl =>
     if i s= 0 %u32
     then Return (ListCons ret tl)
-    else
-      (
-        i0 <- u32_sub i 1 %u32;
-        tl0 <- list_nth_mut_back T tl i0 ret;
-        Return (ListCons x tl0) )
+    else (
+      i0 <- u32_sub i 1 %u32;
+      tl0 <- list_nth_mut_back T tl i0 ret;
+      Return (ListCons x tl0))
   | ListNil => Fail_
   end
   .
@@ -314,39 +312,30 @@ Definition test_list_functions_fwd : result unit :=
   i <- list_length_fwd i32 (ListCons (0 %i32) l1);
   if negb (i s= 3 %u32)
   then Fail_
-  else
-    (
-      i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
-      if negb (i0 s= 0 %i32)
+  else (
+    i0 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (0 %u32);
+    if negb (i0 s= 0 %i32)
+    then Fail_
+    else (
+      i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
+      if negb (i1 s= 1 %i32)
       then Fail_
-      else
-        (
-          i1 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (1 %u32);
-          if negb (i1 s= 1 %i32)
+      else (
+        i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
+        if negb (i2 s= 2 %i32)
+        then Fail_
+        else (
+          ls <- list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3 %i32);
+          i3 <- list_nth_shared_fwd i32 ls (0 %u32);
+          if negb (i3 s= 0 %i32)
           then Fail_
-          else
-            (
-              i2 <- list_nth_shared_fwd i32 (ListCons (0 %i32) l1) (2 %u32);
-              if negb (i2 s= 2 %i32)
-              then Fail_
-              else
-                (
-                  ls <-
-                    list_nth_mut_back i32 (ListCons (0 %i32) l1) (1 %u32) (3
-                      %i32);
-                  i3 <- list_nth_shared_fwd i32 ls (0 %u32);
-                  if negb (i3 s= 0 %i32)
-                  then Fail_
-                  else
-                    (
-                      i4 <- list_nth_shared_fwd i32 ls (1 %u32);
-                      if negb (i4 s= 3 %i32)
-                      then Fail_
-                      else
-                        (
-                          i5 <- list_nth_shared_fwd i32 ls (2 %u32);
-                          if negb (i5 s= 2 %i32) then Fail_ else Return tt ) )
-                  ) ) ) )
+          else (
+            i4 <- list_nth_shared_fwd i32 ls (1 %u32);
+            if negb (i4 s= 3 %i32)
+            then Fail_
+            else (
+              i5 <- list_nth_shared_fwd i32 ls (2 %u32);
+              if negb (i5 s= 2 %i32) then Fail_ else Return tt))))))
   .
 
 (** Unit test for [no_nested_borrows::test_list_functions] *)
@@ -448,34 +437,31 @@ Definition test_constants_fwd : result unit :=
     let (i, _) := p in
     if negb (i s= 1 %u32)
     then Fail_
-    else
-      (
-        swt0 <- new_tuple2_fwd;
-        match swt0 with
-        | mkStruct_with_tuple_t p0 =>
-          let (i0, _) := p0 in
-          if negb (i0 s= 1 %i16)
-          then Fail_
-          else
-            (
-              swt1 <- new_tuple3_fwd;
-              match swt1 with
-              | mkStruct_with_tuple_t p1 =>
-                let (i1, _) := p1 in
-                if negb (i1 s= 1 %u64)
-                then Fail_
-                else
-                  (
-                    swp <- new_pair1_fwd;
-                    match swp with
-                    | mkStruct_with_pair_t p2 =>
-                      match p2 with
-                      | mkPair_t i2 i3 =>
-                        if negb (i2 s= 1 %u32) then Fail_ else Return tt
-                      end
-                    end )
-              end )
-        end )
+    else (
+      swt0 <- new_tuple2_fwd;
+      match swt0 with
+      | mkStruct_with_tuple_t p0 =>
+        let (i0, _) := p0 in
+        if negb (i0 s= 1 %i16)
+        then Fail_
+        else (
+          swt1 <- new_tuple3_fwd;
+          match swt1 with
+          | mkStruct_with_tuple_t p1 =>
+            let (i1, _) := p1 in
+            if negb (i1 s= 1 %u64)
+            then Fail_
+            else (
+              swp <- new_pair1_fwd;
+              match swp with
+              | mkStruct_with_pair_t p2 =>
+                match p2 with
+                | mkPair_t i2 i3 =>
+                  if negb (i2 s= 1 %u32) then Fail_ else Return tt
+                end
+              end)
+          end)
+      end)
   end
   .
 
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index e15e0dc1..25c01d7b 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -34,13 +34,12 @@ Definition test_choose_fwd : result unit :=
   z0 <- i32_add z 1 %i32;
   if negb (z0 s= 1 %i32)
   then Fail_
-  else
-    (
-      p <- choose_back i32 true (0 %i32) (0 %i32) z0;
-      let (x, y) := p in
-      if negb (x s= 1 %i32)
-      then Fail_
-      else if negb (y s= 0 %i32) then Fail_ else Return tt )
+  else (
+    p <- choose_back i32 true (0 %i32) (0 %i32) z0;
+    let (x, y) := p in
+    if negb (x s= 1 %i32)
+    then Fail_
+    else if negb (y s= 0 %i32) then Fail_ else Return tt)
   .
 
 (** Unit test for [paper::test_choose] *)
@@ -61,7 +60,7 @@ Fixpoint list_nth_mut_fwd (T : Type) (l : List_t T) (i : u32) : result T :=
   | ListCons x tl =>
     if i s= 0 %u32
     then Return x
-    else ( i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t )
+    else (i0 <- u32_sub i 1 %u32; t <- list_nth_mut_fwd T tl i0; Return t)
   | ListNil => Fail_
   end
   .
@@ -73,11 +72,10 @@ Fixpoint list_nth_mut_back
   | ListCons x tl =>
     if i s= 0 %u32
     then Return (ListCons ret tl)
-    else
-      (
-        i0 <- u32_sub i 1 %u32;
-        tl0 <- list_nth_mut_back T tl i0 ret;
-        Return (ListCons x tl0) )
+    else (
+      i0 <- u32_sub i 1 %u32;
+      tl0 <- list_nth_mut_back T tl i0 ret;
+      Return (ListCons x tl0))
   | ListNil => Fail_
   end
   .