Fix case formatting (#2387)

* Closes #2361 * Aligns `case` and `let`
anoma · Sep 26, 2023 · 019579b · 019579b
1 parent e509a6e
commit 019579b
Show file tree

Hide file tree

Showing 13 changed files with 81 additions and 62 deletions.
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -486,17 +486,17 @@ instance (SingI s) => PrettyPrint (Let s) where
   ppCode Let {..} = do
     let letFunDefs' = blockIndent (ppBlock _letFunDefs)
         letExpression' = ppExpressionType _letExpression
-    ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'
+    align $ ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'
 
 instance (SingI s) => PrettyPrint (NewCase s) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => NewCase s -> Sem r ()
   ppCode NewCase {..} = do
     let exp' = ppExpressionType _newCaseExpression
-    ppCode _newCaseKw <+> exp' <+> ppCode _newCaseOfKw <+> ppBranches _newCaseBranches
+    align $ ppCode _newCaseKw <> oneLineOrNextBlock exp' <> ppCode _newCaseOfKw <+> ppBranches _newCaseBranches
     where
       ppBranches :: NonEmpty (NewCaseBranch s) -> Sem r ()
       ppBranches = \case
-        b :| [] -> braces (ppCaseBranch True b)
+        b :| [] -> oneLineOrNextBraces (ppCaseBranch True b)
         _ -> braces (blockIndent (vsepHard (ppCaseBranch False <$> _newCaseBranches)))
 
       ppCaseBranch :: Bool -> NewCaseBranch s -> Sem r ()

diff --git a/src/Juvix/Data/Effect/ExactPrint.hs b/src/Juvix/Data/Effect/ExactPrint.hs
@@ -149,6 +149,12 @@ oneLineOrNextNoIndent = region P.oneLineOrNextNoIndent
 oneLineOrNext :: (Members '[ExactPrint] r) => Sem r () -> Sem r ()
 oneLineOrNext = region P.oneLineOrNext
 
+oneLineOrNextBlock :: (Members '[ExactPrint] r) => Sem r () -> Sem r ()
+oneLineOrNextBlock = region P.oneLineOrNextBlock
+
+oneLineOrNextBraces :: (Members '[ExactPrint] r) => Sem r () -> Sem r ()
+oneLineOrNextBraces = region P.oneLineOrNextBraces
+
 nextLine :: (Members '[ExactPrint] r) => Sem r () -> Sem r ()
 nextLine = region P.nextLine
 

diff --git a/src/Juvix/Prelude/Pretty.hs b/src/Juvix/Prelude/Pretty.hs
@@ -172,6 +172,12 @@ oneLineOrNext x = PP.group (flatAlt (line <> indent' x) (space <> x))
 oneLineOrNextNoIndent :: Doc ann -> Doc ann
 oneLineOrNextNoIndent x = PP.group (flatAlt (line <> x) (space <> x))
 
+oneLineOrNextBlock :: Doc ann -> Doc ann
+oneLineOrNextBlock x = PP.group (flatAlt (line <> indent' x <> line) (space <> x <> space))
+
+oneLineOrNextBraces :: Doc ann -> Doc ann
+oneLineOrNextBraces x = PP.group (flatAlt (lbrace <> line <> indent' x <> line <> rbrace) (lbrace <> x <> rbrace))
+
 nextLine :: Doc ann -> Doc ann
 nextLine x = PP.group (line <> x)
 

diff --git a/tests/Compilation/positive/test037.juvix b/tests/Compilation/positive/test037.juvix
@@ -4,17 +4,19 @@ module test037;
 import Stdlib.Prelude open;
 
 f (l : List ((Nat → Nat) → Nat → Nat)) : Nat :=
-  (case l
-      | x :: _ := x
-      | nil := id)
+  case l of {
+    | x :: _ := x
+    | nil := id
+  }
     (let
       y : Nat → Nat := id;
     in (let
-        z : (Nat → Nat) → Nat → Nat := id;
-      in (case l
-          | _ :: _ := id
-          | _ := id)
-        z)
+         z : (Nat → Nat) → Nat → Nat := id;
+       in case l of {
+            | _ :: _ := id
+            | _ := id
+          }
+         z)
       y)
     7;
 

diff --git a/tests/Compilation/positive/test038.juvix b/tests/Compilation/positive/test038.juvix
@@ -5,8 +5,8 @@ import Stdlib.Prelude open;
 
 main : IO :=
   printNatLn
-    (case 1, 2
+    case 1, 2 of {
       | suc _, zero := 0
       | suc _, suc x := x
-      | _ := 19);
-
+      | _ := 19
+    };
diff --git a/tests/Compilation/positive/test060.juvix b/tests/Compilation/positive/test060.juvix
@@ -19,7 +19,7 @@ type Pair (A B : Type) :=
 mf : Pair (Pair Bool (List Nat)) (List Nat) → Bool
   | mkPair@{fst := mkPair@{fst; snd := nil};
            snd := zero :: _} := fst
-  | _ := false;
+  | x := case x of {_ := false};
 
 main : Triple Nat Nat Nat :=
   let

diff --git a/tests/VampIR/positive/Compilation/test006.juvix b/tests/VampIR/positive/Compilation/test006.juvix
@@ -19,11 +19,11 @@ boolToNat : Bool -> Nat
 main : Nat -> Nat -> Nat
   | x y :=
     boolToNat
-      $ case opt3
-        (natToBool x)
-        λ {x y := if y false x}
-        (natToBool y)
-        | opt0 := false
-        | opt1 b := b
-        | opt2 b f := f b
-        | opt3 b1 f b2 := f b1 b2;
+      $ case
+          opt3 (natToBool x) λ {x y := if y false x} (natToBool y)
+        of {
+          | opt0 := false
+          | opt1 b := b
+          | opt2 b f := f b
+          | opt3 b1 f b2 := f b1 b2
+        };
diff --git a/tests/VampIR/positive/Compilation/test007.juvix b/tests/VampIR/positive/Compilation/test007.juvix
@@ -8,20 +8,19 @@ main : Nat -> Nat -> Nat
     let
       x : Nat := a;
     in let
-      x1 :
-        Nat :=
-          x
-            + let
-              x2 : Nat := 2;
-            in x2;
-    in let
-      x3 : Nat := x1 * x1;
-    in let
-      y : Nat := x3 + b;
-    in -- 11
-    let
-      z : Nat := x3 + y;
-    in -- 20
-      x
-      + y
-      + z;
+         x1 : Nat :=
+           x
+             + let
+                 x2 : Nat := 2;
+               in x2;
+       in let
+            x3 : Nat := x1 * x1;
+          in let
+               y : Nat := x3 + b;
+             in -- 11
+                let
+                  z : Nat := x3 + y;
+                in -- 20
+                  x
+                  + y
+                  + z;
diff --git a/tests/VampIR/positive/Compilation/test009.juvix b/tests/VampIR/positive/Compilation/test009.juvix
@@ -5,17 +5,19 @@ import Stdlib.Prelude open;
 
 f : Nat -> ((Nat -> Nat) -> Nat -> Nat) × Nat → Nat
   | a l :=
-    (case l
-        | x, zero := x
-        | _ := id)
+    case l of {
+      | x, zero := x
+      | _ := id
+    }
       (let
         y : Nat → Nat := id;
       in (let
-          z : (Nat → Nat) → Nat → Nat := id;
-        in (case l
-            | _, zero := id
-            | _ := id)
-          z)
+           z : (Nat → Nat) → Nat → Nat := id;
+         in case l of {
+              | _, zero := id
+              | _ := id
+            }
+           z)
         y)
       a;
 

diff --git a/tests/VampIR/positive/Compilation/test017.juvix b/tests/VampIR/positive/Compilation/test017.juvix
@@ -7,25 +7,27 @@ import Stdlib.Data.Nat.Ord open;
 {-# unroll: 11 #-}
 terminating
 f : Nat → Nat
-
   | x :=
-    case x
+    case x of {
       | zero := 1
-      | suc y := 2 * x + g y;
+      | suc y := 2 * x + g y
+    };
 
 terminating
 g : Nat → Nat
   | x :=
-    case x
+    case x of {
       | zero := 1
-      | suc y := x + h y;
+      | suc y := x + h y
+    };
 
 terminating
 h : Nat → Nat
   | x :=
-    case x
+    case x of {
       | zero := 1
-      | suc y := x * f y;
+      | suc y := x * f y
+    };
 
 main : Nat → Nat
   | x := f x + f (2 * x);
diff --git a/tests/VampIR/positive/Compilation/test019.juvix b/tests/VampIR/positive/Compilation/test019.juvix
@@ -5,6 +5,7 @@ import Stdlib.Prelude open;
 
 main : Nat -> Nat -> Nat
   | x y :=
-    case tail (id (x :: y :: nil))
+    case tail (id (x :: y :: nil)) of {
       | nil := 0
-      | h :: _ := h;
+      | h :: _ := h
+    };
diff --git a/tests/VampIR/positive/Compilation/test023.juvix b/tests/VampIR/positive/Compilation/test023.juvix
@@ -6,5 +6,6 @@ import Stdlib.Data.Nat.Ord open;
 
 main : Nat → Nat → Nat
   | x y :=
-    case λ {z := if (x == z) (x, 0) (x, z)} (y + x)
-      | a, b := a + b;
+    case λ {z := if (x == z) (x, 0) (x, z)} (y + x) of {
+      a, b := a + b
+    };
diff --git a/tests/positive/Internal/Case.juvix b/tests/positive/Internal/Case.juvix
@@ -33,9 +33,9 @@ appIf : {A : Type} → Bool → (A → A) → A → A
 appIf2 : {A : Type} → Bool → (A → A) → A → A
   | b f a :=
     case b of {
-        | true := f
-        | false := id
-      }
+      | true := f
+      | false := id
+    }
       a;
 
 nestedCase1 : {A : Type} → Bool → (A → A) → A → A