Formatter improvements (#3194)

1. Closes #3192. The first pipe is ensured in a multi-clause lambda.
3. Bugfix: Pragmas are now properly printed for deriving statements.
Previously they were never printed.
4. Record types are always declared in a new line, even if they have a
single constructor and fit in a line. I think this change improves
readability.
   ```
   -- before
   type Eq A := mkEq@{builtin isEqual eq : A -> A -> Bool};
  
   -- after
   type Eq A :=
     mkEq@{
       builtin isEqual
       eq : A -> A -> Bool;
     };
   ```
5. I've formatted the stdlib
(anoma/juvix-stdlib#150).
6. I've refactored some code related to adding the first pipe so that it
is reused for cases, lambdas and types.
7. Now `ConstructorDef` has a proper `PrettyCode` instance and does not
need to be passed a bool indicating whether it is the only constructor
in a definition.

examples/demo/Demo.juvix

@@ -18,7 +18,9 @@ log2 (n : Nat) : Nat :=
     | else := log2 (div n 2) + 1;
 
 type Tree (A : Type) :=
-  | leaf@{element : A}
+  | leaf@{
+      element : A;
+    }
   | node@{
       element : A;
       left : Tree A;

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -7,7 +7,10 @@ import Logic.Symbol open public;
 import Logic.Extra open;
 
 --- A 3x3 grid of ;Square;s
-type Board := mkBoard@{squares : List (List Square)};
+type Board :=
+  mkBoard@{
+    squares : List (List Square);
+  };
 
 --- Returns the list of numbers corresponding to the empty ;Square;s
 possibleMoves : (list : List Square) -> List Nat

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -7,9 +7,13 @@ import Logic.Extra open;
 --- A square is each of the holes in a board
 type Square :=
   | --- An empty square has a ;Nat; that uniquely identifies it
-    empty@{id : Nat}
+    empty@{
+      id : Nat;
+    }
   | --- An occupied square has a ;Symbol; in it
-    occupied@{player : Symbol};
+    occupied@{
+      player : Symbol;
+    };
 
 instance
 eqSquareI : Eq Square :=

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

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

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

@@ -3000,6 +3000,7 @@ makeLenses ''MarkdownInfo
 makeLenses ''Deriving
 
 makePrisms ''NamedArgumentNew
+makePrisms ''ConstructorRhs
 makePrisms ''FunctionDefNameParsed
 
 functionDefLhs :: FunctionDef s -> FunctionLhs s
@@ -3154,6 +3155,35 @@ instance HasLoc ScopedIden where
 instance (SingI s) => HasLoc (InductiveParameters s) where
   getLoc i = getLocSymbolType (i ^. inductiveParametersNames . _head1) <>? (getLocExpressionType <$> (i ^? inductiveParametersRhs . _Just . inductiveParametersType))
 
+getLocTypeSig :: (SingI s) => TypeSig s -> Maybe Interval
+getLocTypeSig TypeSig {..} =
+  (getLocSpan <$> nonEmpty _typeSigArgs)
+    ?<>? (getLocExpressionType <$> _typeSigRetType)
+
+instance HasLoc (RhsRecord s) where
+  getLoc RhsRecord {..} =
+    let (kat, kl, kr) = _rhsRecordDelim ^. unIrrelevant
+     in (getLoc <$> kat) ?<> getLoc kl <> getLoc kr
+
+instance (SingI s) => HasLoc (RhsGadt s) where
+  getLoc RhsGadt {..} = fromJust (getLocTypeSig _rhsGadtTypeSig)
+
+getLocRhsAdt :: (SingI s) => RhsAdt s -> Maybe Interval
+getLocRhsAdt RhsAdt {..} = getLocSpan' getLocExpressionType <$> nonEmpty _rhsAdtArguments
+
+getLocConstructorRhs :: (SingI s) => ConstructorRhs s -> Maybe Interval
+getLocConstructorRhs = \case
+  ConstructorRhsGadt a -> Just (getLoc a)
+  ConstructorRhsAdt a -> getLocRhsAdt a
+  ConstructorRhsRecord a -> Just (getLoc a)
+
+instance (SingI s) => HasLoc (ConstructorDef s) where
+  getLoc ConstructorDef {..} =
+    (getLoc <$> (_constructorPipe ^. unIrrelevant))
+      ?<> ( getLocSymbolType _constructorName
+              <>? getLocConstructorRhs _constructorRhs
+          )
+
 instance HasLoc (InductiveDef s) where
   getLoc i = (getLoc <$> i ^. inductivePositive) ?<> getLoc (i ^. inductiveKw)
 
@@ -3602,11 +3632,6 @@ data ApeLeaf
   | ApeLeafPatternArg PatternArg
   | ApeLeafAtom (AnyStage ExpressionAtom)
 
-_ConstructorRhsRecord :: Traversal' (ConstructorRhs s) (RhsRecord s)
-_ConstructorRhsRecord f rhs = case rhs of
-  ConstructorRhsRecord r -> ConstructorRhsRecord <$> f r
-  _ -> pure rhs
-
 _DefinitionSyntax :: Traversal' (Definition s) (SyntaxDef s)
 _DefinitionSyntax f x = case x of
   DefinitionSyntax r -> DefinitionSyntax <$> f r

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

@@ -677,36 +677,33 @@ ppCaseBranch :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) =
 ppCaseBranch isTop CaseBranch {..} = do
   let pat' = ppPatternParensType _caseBranchPattern
       rhs' = ppCaseBranchRhs isTop _caseBranchRhs
-  pat' <+> rhs'
+      pipe' = ppCode <$> (_caseBranchPipe ^. unIrrelevant)
+  pipe' <?+> pat' <+> rhs'
 
 ppCase :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Case s -> Sem r ()
-ppCase isTop Case {..} = do
-  let exp' = ppExpressionType _caseExpression
-  align $ ppCode _caseKw <> oneLineOrNextBlock exp' <> ppCode _caseOfKw <> ppBranches _caseBranches
+ppCase isTop c = do
+  let exp' = ppExpressionType (c ^. caseExpression)
+
+  align $ ppCode (c ^. caseKw) <> oneLineOrNextBlock exp' <> ppCode (c ^. caseOfKw) <> ppBranches branches'
   where
+    branches' = insertFirstPipe1 (caseBranchPipe . unIrrelevant) (c ^. caseBranches)
+
     ppBranches :: NonEmpty (CaseBranch s) -> Sem r ()
     ppBranches = \case
       b :| [] -> case isTop of
-        Top -> oneLineOrNext (ppCaseBranch' True Top b)
-        NotTop -> space <> oneLineOrNextBraces (ppCaseBranch' True NotTop b)
+        Top -> oneLineOrNext (ppCaseBranch' Top b)
+        NotTop -> space <> oneLineOrNextBraces (ppCaseBranch' NotTop b)
       _ -> case isTop of
         Top -> do
           let brs =
-                vsepHard (ppCaseBranch' False NotTop <$> NonEmpty.init _caseBranches)
+                vsepHard (ppCaseBranch' NotTop <$> NonEmpty.init branches')
                   <> hardline
-                  <> ppCaseBranch' False Top (NonEmpty.last _caseBranches)
+                  <> ppCaseBranch' Top (NonEmpty.last branches')
           hardline <> indent brs
-        NotTop -> space <> braces (blockIndent (vsepHard (ppCaseBranch' False NotTop <$> _caseBranches)))
-
-    ppCaseBranch' :: Bool -> IsTop -> CaseBranch s -> Sem r ()
-    ppCaseBranch' singleBranch lastTopBranch b = pipeHelper <?+> ppCaseBranch lastTopBranch b
-      where
-        pipeHelper :: Maybe (Sem r ())
-        pipeHelper
-          | singleBranch = Nothing
-          | otherwise = Just $ case b ^. caseBranchPipe . unIrrelevant of
-              Just p -> ppCode p
-              Nothing -> ppCode Kw.kwPipe
+        NotTop -> space <> braces (blockIndent (vsepHard (ppCaseBranch' NotTop <$> branches')))
+
+    ppCaseBranch' :: IsTop -> CaseBranch s -> Sem r ()
+    ppCaseBranch' lastTopBranch b = ppCaseBranch lastTopBranch b
 
 instance (SingI s) => PrettyPrint (IfBranch s 'BranchIfBool) where
   ppCode IfBranch {..} = do
@@ -863,11 +860,20 @@ instance (SingI s) => PrettyPrint (Lambda s) where
   ppCode Lambda {..} = do
     let lambdaKw' = ppCode _lambdaKw
         braces' = uncurry enclose (over both ppCode (_lambdaBraces ^. unIrrelevant))
-        lambdaClauses' = braces' $ case _lambdaClauses of
+        lambdaClauses' = braces' $ case insertFirstPipe1 (lambdaPipe . unIrrelevant) _lambdaClauses of
           s :| [] -> ppCode s
-          _ -> blockIndent (vsepHard (ppCode <$> _lambdaClauses))
+          clauses' -> blockIndent (vsepHard (ppCode <$> clauses'))
     lambdaKw' <> lambdaClauses'
 
+-- | Inserts a pipe to the first element when it is not already there and the
+-- list has more than one element
+insertFirstPipe1 :: (HasLoc a) => Lens' a (Maybe KeywordRef) -> NonEmpty a -> NonEmpty a
+insertFirstPipe1 pipekw l = case l of
+  _ :| [] -> l
+  a :| as ->
+    let p = run (runReader (getLoc a) (Gen.kw Kw.kwPipe))
+     in over pipekw (<|> Just p) a :| as
+
 instance PrettyPrint Precedence where
   ppCode = \case
     PrecArrow -> noLoc (pretty ("-ω" :: Text))
@@ -1144,7 +1150,8 @@ instance (SingI s) => PrettyPrint (SigArg s) where
 
 instance (SingI s) => PrettyPrint (Deriving s) where
   ppCode Deriving {..} =
-    ppCode _derivingKw
+    (ppCode <$> _derivingPragmas)
+      ?<> ppCode _derivingKw
       <+> ppCode _derivingFunLhs
 
 instance (SingI s) => PrettyPrint (TypeSig s) where
@@ -1447,8 +1454,7 @@ instance (SingI s) => PrettyPrint (RhsRecord s) where
   ppCode RhsRecord {..} = do
     let Irrelevant (_, l, r) = _rhsRecordDelim
         fields'
-          | [] <- _rhsRecordStatements = mempty
-          | [f] <- _rhsRecordStatements = ppCode f
+          | null _rhsRecordStatements = mempty
           | otherwise = ppBlock _rhsRecordStatements
     ppCode kwAt <> ppCode l <> fields' <> ppCode r
 
@@ -1462,36 +1468,30 @@ instance (SingI s) => PrettyPrint (ConstructorRhs s) where
     ConstructorRhsRecord r -> ppCode r
     ConstructorRhsAdt r -> ppCode r
 
-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 {} -> mempty
-          ConstructorRhsRecord {} -> mempty
-          ConstructorRhsAdt a
-            | null (a ^. rhsAdtArguments) -> mempty
-            | otherwise -> space
-
-    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
+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
+        pipe = ppCode <$> (_constructorPipe ^. unIrrelevant)
+
+        nestCond :: Sem r () -> Sem r ()
+        nestCond x = case _constructorPipe ^. unIrrelevant of
+          Just p -> printCommentsUntil (getLoc p) >> nest x
+          Nothing -> x
+    nestCond (pipe <?+> doc' ?<> pragmas' ?<> constructorName' <> constructorRhs')
+    where
+      constructorRhsHelper :: ConstructorRhs s -> Sem r ()
+      constructorRhsHelper r = spaceMay <> ppCode r
+        where
+          spaceMay = case r of
+            ConstructorRhsGadt {} -> mempty
+            ConstructorRhsRecord {} -> mempty
+            ConstructorRhsAdt a
+              | null (a ^. rhsAdtArguments) -> mempty
+              | otherwise -> space
 
 ppInductiveSignature :: (SingI s) => PrettyPrinting (InductiveDef s)
 ppInductiveSignature InductiveDef {..} = do
@@ -1518,7 +1518,7 @@ instance (SingI s) => PrettyPrint (InductiveDef s) where
   ppCode d@InductiveDef {..} = do
     let doc' = ppCode <$> _inductiveDoc
         pragmas' = ppCode <$> _inductivePragmas
-        constrs' = ppConstructorBlock _inductiveConstructors
+        constrs' = ppConstructorBlock (insertFirstPipe1 (constructorPipe . unIrrelevant) _inductiveConstructors)
         sig' = ppInductiveSignature d
     doc'
       ?<> pragmas'
@@ -1528,8 +1528,9 @@ instance (SingI s) => PrettyPrint (InductiveDef s) where
     where
       ppConstructorBlock :: NonEmpty (ConstructorDef s) -> Sem r ()
       ppConstructorBlock = \case
-        c :| [] -> oneLineOrNext (ppConstructorDef True c)
-        cs -> line <> indent (vsep (ppConstructorDef False <$> cs))
+        c :| []
+          | not (has (constructorRhs . _ConstructorRhsRecord . rhsRecordStatements . each) c) -> oneLineOrNext (ppCode c)
+        cs -> hardline <> indent (vsep (ppCode <$> cs))
 
 instance (SingI s) => PrettyPrint (ProjectionDef s) where
   ppCode ProjectionDef {..} =

src/Juvix/Data/Loc.hs

@@ -103,7 +103,10 @@ instance HasLoc Interval where
 
 -- | The items are assumed to be in order with respect to their location.
 getLocSpan :: (HasLoc t) => NonEmpty t -> Interval
-getLocSpan l = getLoc (head l) <> getLoc (last l)
+getLocSpan = getLocSpan' getLoc
+
+getLocSpan' :: (t -> Interval) -> NonEmpty t -> Interval
+getLocSpan' gl l = gl (head l) <> gl (last l)
 
 -- | Assumes the file is the same
 instance Semigroup Interval where

tests/positive/Format.juvix

@@ -53,7 +53,7 @@ case4 (n : Nat) : Nat :=
     | zero := case n of {x := zero}
     | _ := zero;
 
--- -- case with application subject
+-- case with application subject
 case5 (n : Nat) : Nat := case id n of x := zero;
 
 -- qualified commas
@@ -274,7 +274,8 @@ module Comments;
   type color : Type :=
     -- comment before pipe
     | black : color
-    | white : color
+    | --- documentation for white
+      white : color
     | red : color
     -- comment before pipe
     | blue : color;
@@ -309,7 +310,10 @@ module Traits;
   import Stdlib.Prelude open hiding {Show; mkShow; module Show};
 
   trait
-  type Show A := mkShow@{show : A → String};
+  type Show A :=
+    mkShow@{
+      show : A → String;
+    };
 
   instance
   showStringI : Show String :=
@@ -396,6 +400,18 @@ module RecordFieldPragmas;
     };
 end;
 
+module MultiConstructorRecord;
+  type Tree (A : Type) :=
+    | leaf@{
+        element : A;
+      }
+    | node@{
+        element : A;
+        left : Tree A;
+        right : Tree A;
+      };
+end;
+
 longLongLongArg : Int := 0;
 
 longLongLongListArg : List Int := [];

tests/positive/InstanceImport/M.juvix

@@ -1,7 +1,10 @@
 module M;
 
 trait
-type T A := mkT@{pp : A → A};
+type T A :=
+  mkT@{
+    pp : A → A;
+  };
 
 type Unit := unit;
 

tests/positive/Internal/Positivity2/main.juvix

@@ -53,8 +53,13 @@ module E6;
     | zero
     | suc Nat;
 
-  type Box := mkBox@{unbox : Nat};
+  type Box :=
+    mkBox@{
+      unbox : Nat;
+    };
 
   type Foldable :=
-    mkFoldable@{for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B};
+    mkFoldable@{
+      for : {B : Type} -> (B -> Nat -> B) -> B -> Box -> B;
+    };
 end;

tests/positive/RecordProjectionSignature.juvix

@@ -3,7 +3,10 @@ module RecordProjectionSignature;
 import Stdlib.Data.Nat open;
 
 trait
-type R A := mkR@{fun : (n : A) -> A};
+type R A :=
+  mkR@{
+    fun : (n : A) -> A;
+  };
 
 f {{R Nat}} : Nat :=
   R.fun@{

tests/positive/Termination/issue2414.juvix

@@ -3,7 +3,10 @@ module issue2414;
 import Stdlib.Prelude open;
 
 trait
-type T := mkT@{tt : T};
+type T :=
+  mkT@{
+    tt : T;
+  };
 
 f {{T}} : Nat → Nat
   | zero := zero