Improve formatting of single-constructor types and records (#2342)

- Closes #2331.

The rules implemented in this pr are as follows.
1. If a type definition has only one constructor, no pipe is added. The
constructor is printed in the same line if it fits.
2. If a constructor is a record with a single field, the field is
printed in the same line if it fits. If the constructor has multiple
fields, they are printed aligned and indented after a line break.

Examples:
```
type T := constructT : T;

type T-wrapper := mkWrapper {unwrap : T};

type EnumRecord :=
  | --- doc for C1
    C1 {
      c1a : T;
      c1b : T
    }
  | C2 {
      c2a : T;
      c2b : T
    };
```

examples/milestone/Bank/Bank.juvix

@@ -22,8 +22,8 @@ axiom eqField : Field -> Field -> Bool;
 
 module Token;
   type Token :=
-    | --- Arguments are: owner, gates, amount.
-      mkToken : Address -> Nat -> Nat -> Token;
+    --- Arguments are: owner, gates, amount.
+    mkToken : Address -> Nat -> Nat -> Token;
 
   --- Retrieves the owner from a ;Token;
   getOwner : Token -> Address

examples/milestone/Hanoi/Hanoi.juvix

@@ -44,8 +44,7 @@ showPeg : Peg → String
   | right := "right";
 
 --- A Move represents a move between pegs
-type Move :=
-  | move : Peg → Peg → Move;
+type Move := move : Peg → Peg → Move;
 
 showMove : Move → String
   | (move from to) :=

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -7,8 +7,7 @@ import Logic.Symbol open public;
 import Logic.Extra open;
 
 --- A 3x3 grid of ;Square;s
-type Board :=
-  | board : List (List Square) → Board;
+type Board := board : List (List Square) → Board;
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
 possibleMoves : List Square → List Nat

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -13,7 +13,7 @@ type Error :=
     terminate : String → Error;
 
 type GameState :=
-  | state : Board → Symbol → Error → GameState;
+  state : Board → Symbol → Error → GameState;
 
 --- Textual representation of a ;GameState;
 showGameState : GameState → String

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -556,7 +556,7 @@ goConstructors cc = do
 
         srcPart :: Sem r Html
         srcPart = do
-          sig' <- ppCodeHtml defaultOptions (set constructorDoc Nothing c)
+          sig' <- ppHelper (ppConstructorDef False (set constructorDoc Nothing c))
           return
             $ td
               ! Attr.class_ "src"

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -712,7 +712,7 @@ instance (SingI s) => PrettyPrint (JudocLine s) where
 
 instance (SingI s) => PrettyPrint (Judoc s) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Judoc s -> Sem r ()
-  ppCode (Judoc groups) = ppGroups groups <> line
+  ppCode (Judoc groups) = ppGroups groups <> hardline
     where
       ppGroups :: NonEmpty (JudocGroup s) -> Sem r ()
       ppGroups = \case
@@ -992,13 +992,13 @@ instance (SingI s) => PrettyPrint (RhsRecord s) where
         fields'
           | null (_rhsRecordFields ^. _tail1) = ppCode (_rhsRecordFields ^. _head1)
           | otherwise =
-              line
+              hardline
                 <> indent
                   ( sequenceWith
                       (semicolon >> line)
                       (ppCode <$> _rhsRecordFields)
                   )
-                <> line
+                <> hardline
     ppCode l <> fields' <> ppCode r
 
 instance (SingI s) => PrettyPrint (RhsAdt s) where
@@ -1011,30 +1011,36 @@ instance (SingI s) => PrettyPrint (ConstructorRhs s) where
     ConstructorRhsRecord r -> ppCode r
     ConstructorRhsAdt r -> ppCode r
 
-instance (SingI s) => PrettyPrint (ConstructorDef s) where
-  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => ConstructorDef s -> Sem r ()
-  ppCode ConstructorDef {..} = do
-    let constructorName' = annDef _constructorName (ppSymbolType _constructorName)
-        constructorRhs' = constructorRhsHelper _constructorRhs
-        doc' = ppCode <$> _constructorDoc
-        pragmas' = ppCode <$> _constructorPragmas
-    pipeHelper <+> nest (doc' ?<> pragmas' ?<> constructorName' <> constructorRhs')
-    where
-      constructorRhsHelper :: ConstructorRhs s -> Sem r ()
-      constructorRhsHelper r = spaceMay <> ppCode r
-        where
-          spaceMay = case r of
-            ConstructorRhsGadt {} -> space
-            ConstructorRhsRecord {} -> space
-            ConstructorRhsAdt a
-              | null (a ^. rhsAdtArguments) -> mempty
-              | otherwise -> space
+ppConstructorDef :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => Bool -> ConstructorDef s -> Sem r ()
+ppConstructorDef singleConstructor ConstructorDef {..} = do
+  let constructorName' = annDef _constructorName (ppSymbolType _constructorName)
+      constructorRhs' = constructorRhsHelper _constructorRhs
+      doc' = ppCode <$> _constructorDoc
+      pragmas' = ppCode <$> _constructorPragmas
+  pipeHelper <?+> nestHelper (doc' ?<> pragmas' ?<> constructorName' <> constructorRhs')
+  where
+    constructorRhsHelper :: ConstructorRhs s -> Sem r ()
+    constructorRhsHelper r = spaceMay <> ppCode r
+      where
+        spaceMay = case r of
+          ConstructorRhsGadt {} -> space
+          ConstructorRhsRecord {} -> space
+          ConstructorRhsAdt a
+            | null (a ^. rhsAdtArguments) -> mempty
+            | otherwise -> space
 
-      -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted
-      pipeHelper :: Sem r ()
-      pipeHelper = case _constructorPipe ^. unIrrelevant of
-        Just p -> ppCode p
-        Nothing -> ppCode Kw.kwPipe
+    nestHelper :: Sem r () -> Sem r ()
+    nestHelper
+      | singleConstructor = id
+      | otherwise = nest
+
+    -- we use this helper so that comments appear before the first optional pipe if the pipe was omitted
+    pipeHelper :: Maybe (Sem r ())
+    pipeHelper
+      | singleConstructor = Nothing
+      | otherwise = Just $ case _constructorPipe ^. unIrrelevant of
+          Just p -> ppCode p
+          Nothing -> ppCode Kw.kwPipe
 
 ppInductiveSignature :: (SingI s) => PrettyPrinting (InductiveDef s)
 ppInductiveSignature InductiveDef {..} = do
@@ -1065,11 +1071,12 @@ instance (SingI s) => PrettyPrint (InductiveDef s) where
       ?<> pragmas'
       ?<> sig'
       <+> ppCode _inductiveAssignKw
-        <> line
-        <> indent constrs'
+        <> constrs'
     where
       ppConstructorBlock :: NonEmpty (ConstructorDef s) -> Sem r ()
-      ppConstructorBlock cs = vsep (ppCode <$> cs)
+      ppConstructorBlock = \case
+        c :| [] -> oneLineOrNext (ppConstructorDef True c)
+        cs -> line <> indent (vsep (ppConstructorDef False <$> cs))
 
 instance (SingI s) => PrettyPrint (ProjectionDef s) where
   ppCode ProjectionDef {..} =

src/Juvix/Data/Effect/ExactPrint.hs

@@ -79,6 +79,9 @@ align = region P.align
 indent :: (Members '[ExactPrint] r) => Sem r () -> Sem r ()
 indent = region (P.indent 2)
 
+softline :: (Members '[ExactPrint] r) => Sem r ()
+softline = noLoc P.softline
+
 line :: (Members '[ExactPrint] r) => Sem r ()
 line = noLoc P.line
 

test/Format.hs

@@ -69,5 +69,9 @@ tests =
   [ posTest
       "Format"
       $(mkRelDir ".")
+      $(mkRelFile "Format.juvix"),
+    posTest
+      "Records"
+      $(mkRelDir ".")
       $(mkRelFile "Format.juvix")
   ]

tests/positive/Adt.juvix

@@ -4,8 +4,7 @@ type Bool :=
   | true
   | false;
 
-type Pair (A B : Type) :=
-  | mkPair A B;
+type Pair (A B : Type) := mkPair A B;
 
 type Nat :=
   | zero

tests/positive/Format.juvix

@@ -145,8 +145,7 @@ exampleFunction2
       + undefined};
 
 positive
-type T0 (A : Type) :=
-  | c0 : (A -> T0 A) -> T0 A;
+type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
 
 -- Single Lambda clause
 idLambda : {A : Type} -> A -> A := λ {x := x};
@@ -166,8 +165,7 @@ f : Nat -> Nat :=
 module Patterns;
   syntax operator × functor;
   syntax operator , pair;
-  type × (A : Type) (B : Type) :=
-    | , : A → B → A × B;
+  type × (A : Type) (B : Type) := , : A → B → A × B;
 
   f : Nat × Nat × Nat × Nat -> Nat
     | (a, b, c, d) := a;
@@ -236,8 +234,7 @@ module Comments;
   {-- before first f
   f; f};
 
-  type list (A : Type) : Type :=
-    | cons A (list A);
+  type list (A : Type) : Type := cons A (list A);
 end;
 
 -- Comment at the end of a module

tests/positive/ImportShadow/Main.juvix

@@ -2,8 +2,7 @@ module Main;
 
 import Nat open;
 
-type Unit :=
-  | unit : Unit;
+type Unit := unit : Unit;
 
 f : Nat :=
   case unit

tests/positive/Imports/A.juvix

@@ -5,8 +5,7 @@ syntax fixity i3 {arity: binary};
 module M;
   module N;
     syntax operator t i3;
-    type T :=
-      | t : T;
+    type T := t : T;
   end;
 
   syntax fixity add {arity: binary, assoc: right, below: [i3]};

tests/positive/Inductive.juvix

@@ -1,4 +1,3 @@
 module Inductive;
 
-type T :=
-  | t : T;
+type T := t : T;

tests/positive/InductivePipes.juvix

@@ -1,7 +1,6 @@
 module InductivePipes;
 
-type T :=
-  | t : T;
+type T := t : T;
 
 type T2 :=
   | t1 : T2

tests/positive/Judoc.juvix

@@ -6,8 +6,8 @@ axiom b : Type;
 
 --- document type
 type T :=
-  | --- document constructor
-    t : T;
+  --- document constructor
+  t : T;
 
 --- blah ;id A; and ;A A id T A id; this is another ;id
   id

tests/positive/MultiParams.juvix

@@ -1,7 +1,6 @@
 module MultiParams;
 
-type Multi (A B C : Type) :=
-  | mult : Multi A B C;
+type Multi (A B C : Type) := mult : Multi A B C;
 
 f : {A B : Type} → (C : Type) → {D E F : Type} → Type → Type
   | C _ := C;

tests/positive/QualifiedConstructor/M.juvix

@@ -8,8 +8,7 @@ open O;
 
 module N;
   module O;
-    type T :=
-      | A : T;
+    type T := A : T;
   end;
 end;
 

tests/positive/Records.juvix

@@ -1,19 +1,22 @@
 module Records;
 
-type T :=
-  | constructT : T;
+type T := constructT : T;
+
+type T-wrapper := mkWrapper {unwrap : T};
 
 type Pair (A B : Type) :=
-  | mkPair {
-      fst : A;
-      snd : B
-    };
+  --- creates a pair
+  mkPair {
+    fst : A;
+    snd : B
+  };
 
 p1 : Pair T T :=
   mkPair (fst := constructT; snd := constructT);
 
 type EnumRecord :=
-  | C1 {
+  | --- doc for C1
+    C1 {
       c1a : T;
       c1b : T
     }
@@ -27,8 +30,7 @@ p2 : Pair EnumRecord EnumRecord :=
     (fst := C1 (c1a := constructT; c1b := constructT);
     snd := C2 (c2a := constructT; c2b := constructT));
 
-type newtype :=
-  | mknewtype {f : T};
+type newtype := mknewtype {f : T};
 
 p3 : Pair T T -> T := Pair.fst;
 
@@ -42,5 +44,5 @@ type Bool :=
 
 module Update;
   f {A B : Type} (p : Pair A B) : Pair Bool B :=
-    p @Pair{fst := true};
+    p@Pair{fst := true};
 end;

tests/positive/StdlibList/Data/Product.juvix

@@ -3,5 +3,4 @@ module Data.Product;
 syntax fixity prod {arity: binary};
 
 syntax operator × prod;
-type × (a : Type) (b : Type) :=
-  | , : a → b → a × b;
+type × (a : Type) (b : Type) := , : a → b → a × b;