Allow optional pipe before the first constructor for inductive type declarations

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

@@ -301,9 +301,7 @@ instance SingI s => PrettyCode (InductiveDef s) where
       ppConstructorBlock ::
         NonEmpty (InductiveConstructorDef s) -> Sem r (Doc Ann)
       ppConstructorBlock cs =
-        do
-          concatWith (\x y -> x <> softline <> kwPipe <+> y)
-          <$> mapM ppCode (toList cs)
+        vsep <$> mapM (fmap (kwPipe <+>) . ppCode) (toList cs)
 
 dotted :: Foldable f => f (Doc Ann) -> Doc Ann
 dotted = concatWith (surround kwDot)

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -506,7 +506,9 @@ inductiveDef _inductiveBuiltin = do
       P.<?> "<type annotation e.g. ': Type'>"
   kw kwAssign P.<?> "<assignment symbol ':='>"
   _inductiveConstructors <-
-    P.sepBy1 constructorDef (kw kwPipe) P.<?> "<constructor definition>"
+    optional (kw kwPipe)
+      >> P.sepBy1 constructorDef (kw kwPipe)
+      P.<?> "<constructor definition>"
   return InductiveDef {..}
 
 inductiveParam :: Members '[InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (InductiveParameter 'Parsed)

test/Scope/Positive.hs

@@ -131,6 +131,10 @@ tests =
       "Inductive"
       $(mkRelDir ".")
       $(mkRelFile "Inductive.juvix"),
+    PosTest
+      "Pipes symbol as possible prefix for each data constructor"
+      $(mkRelDir ".")
+      $(mkRelFile "InductivePipes.juvix"),
     PosTest
       "Imports and qualified names"
       $(mkRelDir "Imports")

tests/positive/InductivePipes.juvix

@@ -0,0 +1,9 @@
+module InductivePipes;
+
+  type T := | t : T;
+  type T2 :=
+  | t1 : T2
+  | t2 : T2
+  | t3 : T2;
+
+end ;