Optional braces in case syntax (#2778)

* Closes #2769 
* Removes old case syntax
* Pretty printing doesn't print braces in `case` if the `case` is a
"top" expression in a definition.

src/Juvix/Compiler/Concrete/Language.hs

@@ -1281,7 +1281,6 @@ data Expression
   | ExpressionList (List 'Scoped)
   | ExpressionCase (Case 'Scoped)
   | ExpressionIf (If 'Scoped)
-  | ExpressionNewCase (NewCase 'Scoped)
   | ExpressionLambda (Lambda 'Scoped)
   | ExpressionLet (Let 'Scoped)
   | ExpressionUniverse Universe
@@ -1514,7 +1513,7 @@ deriving stock instance Ord (Let 'Parsed)
 deriving stock instance Ord (Let 'Scoped)
 
 data CaseBranch (s :: Stage) = CaseBranch
-  { _caseBranchPipe :: Irrelevant KeywordRef,
+  { _caseBranchPipe :: Irrelevant (Maybe KeywordRef),
     _caseBranchAssignKw :: Irrelevant KeywordRef,
     _caseBranchPattern :: PatternParensType s,
     _caseBranchExpression :: ExpressionType s
@@ -1539,9 +1538,7 @@ deriving stock instance Ord (CaseBranch 'Scoped)
 
 data Case (s :: Stage) = Case
   { _caseKw :: KeywordRef,
-    -- | Due to limitations of the pretty printing algorithm, we store whether
-    -- the `case` was surrounded by parentheses in the code.
-    _caseParens :: Bool,
+    _caseOfKw :: KeywordRef,
     _caseExpression :: ExpressionType s,
     _caseBranches :: NonEmpty (CaseBranch s)
   }
@@ -1563,54 +1560,6 @@ deriving stock instance Ord (Case 'Parsed)
 
 deriving stock instance Ord (Case 'Scoped)
 
-data NewCaseBranch (s :: Stage) = NewCaseBranch
-  { _newCaseBranchPipe :: Irrelevant (Maybe KeywordRef),
-    _newCaseBranchAssignKw :: Irrelevant KeywordRef,
-    _newCaseBranchPattern :: PatternParensType s,
-    _newCaseBranchExpression :: ExpressionType s
-  }
-  deriving stock (Generic)
-
-instance Serialize (NewCaseBranch 'Scoped)
-
-instance Serialize (NewCaseBranch 'Parsed)
-
-deriving stock instance Show (NewCaseBranch 'Parsed)
-
-deriving stock instance Show (NewCaseBranch 'Scoped)
-
-deriving stock instance Eq (NewCaseBranch 'Parsed)
-
-deriving stock instance Eq (NewCaseBranch 'Scoped)
-
-deriving stock instance Ord (NewCaseBranch 'Parsed)
-
-deriving stock instance Ord (NewCaseBranch 'Scoped)
-
-data NewCase (s :: Stage) = NewCase
-  { _newCaseKw :: KeywordRef,
-    _newCaseOfKw :: KeywordRef,
-    _newCaseExpression :: ExpressionType s,
-    _newCaseBranches :: NonEmpty (NewCaseBranch s)
-  }
-  deriving stock (Generic)
-
-instance Serialize (NewCase 'Scoped)
-
-instance Serialize (NewCase 'Parsed)
-
-deriving stock instance Show (NewCase 'Parsed)
-
-deriving stock instance Show (NewCase 'Scoped)
-
-deriving stock instance Eq (NewCase 'Parsed)
-
-deriving stock instance Eq (NewCase 'Scoped)
-
-deriving stock instance Ord (NewCase 'Parsed)
-
-deriving stock instance Ord (NewCase 'Scoped)
-
 data IfBranch (s :: Stage) = IfBranch
   { _ifBranchPipe :: Irrelevant KeywordRef,
     _ifBranchAssignKw :: Irrelevant KeywordRef,
@@ -1967,7 +1916,6 @@ data ExpressionAtom (s :: Stage)
   | AtomLambda (Lambda s)
   | AtomList (List s)
   | AtomCase (Case s)
-  | AtomNewCase (NewCase s)
   | AtomIf (If s)
   | AtomHole (HoleType s)
   | AtomInstanceHole (HoleType s)
@@ -2227,8 +2175,6 @@ makeLenses ''PatternInfixApp
 makeLenses ''PatternPostfixApp
 makeLenses ''Case
 makeLenses ''CaseBranch
-makeLenses ''NewCase
-makeLenses ''NewCaseBranch
 makeLenses ''If
 makeLenses ''IfBranch
 makeLenses ''IfBranchElse
@@ -2327,7 +2273,6 @@ instance HasAtomicity Expression where
     ExpressionUniverse {} -> Atom
     ExpressionFunction {} -> Aggregate funFixity
     ExpressionCase c -> atomicity c
-    ExpressionNewCase c -> atomicity c
     ExpressionIf x -> atomicity x
     ExpressionIterator i -> atomicity i
     ExpressionNamedApplication i -> atomicity i
@@ -2346,9 +2291,6 @@ instance HasAtomicity (Iterator s) where
 instance HasAtomicity (Case s) where
   atomicity = const Atom
 
-instance HasAtomicity (NewCase s) where
-  atomicity = const Atom
-
 instance HasAtomicity (If s) where
   atomicity = const Atom
 
@@ -2438,15 +2380,12 @@ instance HasLoc (Let 'Scoped) where
   getLoc l = getLoc (l ^. letKw) <> getLoc (l ^. letExpression)
 
 instance (SingI s) => HasLoc (CaseBranch s) where
-  getLoc c = getLoc (c ^. caseBranchPipe) <> getLocExpressionType (c ^. caseBranchExpression)
-
-instance (SingI s) => HasLoc (NewCaseBranch s) where
-  getLoc c = case c ^. newCaseBranchPipe . unIrrelevant of
+  getLoc c = case c ^. caseBranchPipe . unIrrelevant of
     Nothing -> branchLoc
     Just p -> getLoc p <> branchLoc
     where
       branchLoc :: Interval
-      branchLoc = getLocExpressionType (c ^. newCaseBranchExpression)
+      branchLoc = getLocExpressionType (c ^. caseBranchExpression)
 
 instance (SingI s) => HasLoc (IfBranch s) where
   getLoc c = getLoc (c ^. ifBranchPipe) <> getLocExpressionType (c ^. ifBranchExpression)
@@ -2457,9 +2396,6 @@ instance (SingI s) => HasLoc (IfBranchElse s) where
 instance (SingI s) => HasLoc (Case s) where
   getLoc c = getLoc (c ^. caseKw) <> getLoc (c ^. caseBranches . to last)
 
-instance (SingI s) => HasLoc (NewCase s) where
-  getLoc c = getLoc (c ^. newCaseKw) <> getLoc (c ^. newCaseBranches . to last)
-
 instance (SingI s) => HasLoc (If s) where
   getLoc c = getLoc (c ^. ifKw) <> getLoc (c ^. ifBranchElse)
 
@@ -2502,7 +2438,6 @@ instance HasLoc Expression where
     ExpressionLambda i -> getLoc i
     ExpressionList l -> getLoc l
     ExpressionCase i -> getLoc i
-    ExpressionNewCase i -> getLoc i
     ExpressionIf x -> getLoc x
     ExpressionLet i -> getLoc i
     ExpressionUniverse i -> getLoc i
@@ -2873,7 +2808,6 @@ instance IsApe Expression ApeLeaf where
     ExpressionIdentifier {} -> leaf
     ExpressionList {} -> leaf
     ExpressionCase {} -> leaf
-    ExpressionNewCase {} -> leaf
     ExpressionIf {} -> leaf
     ExpressionLambda {} -> leaf
     ExpressionLet {} -> leaf

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

@@ -31,6 +31,16 @@ import Juvix.Prelude hiding ((<+>), (<+?>), (<?+>), (?<>))
 import Juvix.Prelude.Pretty (annotate, pretty)
 import Juvix.Prelude.Pretty qualified as P
 
+--- An expression is `Top` if it is:
+--- * immediately at the top of a function (clause) body (including in let
+---   bindings) or a lambda body
+--- * immediately inside parens or braces
+--- * the body of a `Top` let expression,
+--- * the body of a `Top` iterator,
+--- * the else branch body of a `Top` if expression,
+--- * the last branch body of a `Top` case expresssion.
+data IsTop = Top | NotTop
+
 type PrettyPrinting a = forall r. (Members '[ExactPrint, Reader Options] r) => a -> Sem r ()
 
 class PrettyPrint a where
@@ -119,6 +129,16 @@ ppExpressionType = case sing :: SStage s of
   SParsed -> ppCode
   SScoped -> ppCode
 
+ppTopExpressionType :: forall s. (SingI s) => PrettyPrinting (ExpressionType s)
+ppTopExpressionType e = case sing :: SStage s of
+  SParsed -> ppCode e
+  SScoped -> case e of
+    ExpressionLet l -> ppLet Top l
+    ExpressionCase c -> ppCase Top c
+    ExpressionIf i -> ppIf Top i
+    ExpressionIterator i -> ppIterator Top i
+    _ -> ppCode e
+
 ppExpressionAtomType :: forall s. (SingI s) => PrettyPrinting (ExpressionType s)
 ppExpressionAtomType = case sing :: SStage s of
   SParsed -> ppCodeAtom
@@ -244,19 +264,18 @@ instance (SingI s) => PrettyPrint (Range s) where
         e = ppExpressionType _rangeExpression
     n <+> ppCode _rangeInKw <+> e
 
-instance (SingI s) => PrettyPrint (Iterator s) where
-  ppCode Iterator {..} = do
-    let n = ppIdentifierType _iteratorName
-        is = ppCode <$> _iteratorInitializers
-        rngs = ppCode <$> _iteratorRanges
-        is' = parens . hsepSemicolon <$> nonEmpty is
-        rngs' = parens . hsepSemicolon <$> nonEmpty rngs
-        b = ppExpressionType _iteratorBody
-        b'
-          | _iteratorBodyBraces = braces (oneLineOrNextNoIndent b)
-          | otherwise = line <> b
-    parensIf _iteratorParens $
-      hang (n <+?> is' <+?> rngs' <> b')
+ppIterator :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Iterator s -> Sem r ()
+ppIterator isTop Iterator {..} = do
+  let n = ppIdentifierType _iteratorName
+      is = ppCode <$> _iteratorInitializers
+      rngs = ppCode <$> _iteratorRanges
+      is' = parens . hsepSemicolon <$> nonEmpty is
+      rngs' = parens . hsepSemicolon <$> nonEmpty rngs
+      b
+        | _iteratorBodyBraces = braces (oneLineOrNextNoIndent (ppTopExpressionType _iteratorBody))
+        | otherwise = line <> ppMaybeTopExpression isTop _iteratorBody
+  parensIf _iteratorParens $
+    hang (n <+?> is' <+?> rngs' <> b)
 
 instance PrettyPrint S.AName where
   ppCode n = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.anameVerbatim)))
@@ -336,28 +355,27 @@ instance (SingI s) => PrettyPrint (RecordUpdate s) where
 instance (SingI s) => PrettyPrint (DoubleBracesExpression s) where
   ppCode DoubleBracesExpression {..} = do
     let (l, r) = _doubleBracesDelims ^. unIrrelevant
-    ppCode l <> ppExpressionType _doubleBracesExpression <> ppCode r
+    ppCode l <> ppTopExpressionType _doubleBracesExpression <> ppCode r
 
 instance (SingI s) => PrettyPrint (ExpressionAtom s) where
   ppCode = \case
     AtomIdentifier n -> ppIdentifierType n
     AtomLambda l -> ppCode l
-    AtomLet lb -> ppCode lb
-    AtomCase c -> ppCode c
-    AtomNewCase c -> ppCode c
-    AtomIf c -> ppCode c
+    AtomLet lb -> ppLet NotTop lb
+    AtomCase c -> ppCase NotTop c
+    AtomIf c -> ppIf NotTop c
     AtomList l -> ppCode l
     AtomUniverse uni -> ppCode uni
     AtomRecordUpdate u -> ppCode u
     AtomFunction fun -> ppCode fun
     AtomLiteral lit -> ppCode lit
     AtomFunArrow a -> ppCode a
-    AtomParens e -> parens (ppExpressionType e)
+    AtomParens e -> parens (ppTopExpressionType e)
     AtomDoubleBraces e -> ppCode e
-    AtomBraces e -> braces (ppExpressionType (e ^. withLocParam))
+    AtomBraces e -> braces (ppTopExpressionType (e ^. withLocParam))
     AtomHole w -> ppHoleType w
     AtomInstanceHole w -> ppHoleType w
-    AtomIterator i -> ppCode i
+    AtomIterator i -> ppIterator NotTop i
     AtomNamedApplication i -> ppCode i
     AtomNamedApplicationNew i -> ppCode i
 
@@ -493,7 +511,7 @@ ppLiteral = \case
 instance (SingI s) => PrettyPrint (LambdaClause s) where
   ppCode LambdaClause {..} = do
     let lambdaParameters' = hsep (ppPatternAtom <$> _lambdaParameters)
-        lambdaBody' = ppExpressionType _lambdaBody
+        lambdaBody' = ppTopExpressionType _lambdaBody
         lambdaPipe' = ppCode <$> _lambdaPipe ^. unIrrelevant
     lambdaPipe' <?+> lambdaParameters' <+> ppCode _lambdaAssignKw <> oneLineOrNext lambdaBody'
 
@@ -503,68 +521,78 @@ instance (SingI s) => PrettyPrint (LetStatement s) where
     LetAliasDef f -> ppCode f
     LetOpen f -> ppCode f
 
-instance (SingI s) => PrettyPrint (Let s) where
-  ppCode Let {..} = do
-    let letFunDefs' = blockIndent (ppBlock _letFunDefs)
-        letExpression' = ppExpressionType _letExpression
-    align $ ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'
+ppMaybeTopExpression :: (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> ExpressionType s -> Sem r ()
+ppMaybeTopExpression isTop e = case isTop of
+  Top -> ppTopExpressionType e
+  NotTop -> ppExpressionType e
 
-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
-    align $ ppCode _newCaseKw <> oneLineOrNextBlock exp' <> ppCode _newCaseOfKw <+> ppBranches _newCaseBranches
-    where
-      ppBranches :: NonEmpty (NewCaseBranch s) -> Sem r ()
-      ppBranches = \case
-        b :| [] -> oneLineOrNextBraces (ppCaseBranch True b)
-        _ -> braces (blockIndent (vsepHard (ppCaseBranch False <$> _newCaseBranches)))
+ppLet :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> Let s -> Sem r ()
+ppLet isTop Let {..} = do
+  let letFunDefs' = blockIndent (ppBlock _letFunDefs)
+      letExpression' = ppMaybeTopExpression isTop _letExpression
+  align $ ppCode _letKw <> letFunDefs' <> ppCode _letInKw <+> letExpression'
 
-      ppCaseBranch :: Bool -> NewCaseBranch s -> Sem r ()
-      ppCaseBranch singleBranch b = pipeHelper <?+> ppCode b
-        where
-          pipeHelper :: Maybe (Sem r ())
-          pipeHelper
-            | singleBranch = Nothing
-            | otherwise = Just $ case b ^. newCaseBranchPipe . unIrrelevant of
-                Just p -> ppCode p
-                Nothing -> ppCode Kw.kwPipe
+ppCaseBranch :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> CaseBranch s -> Sem r ()
+ppCaseBranch isTop CaseBranch {..} = do
+  let pat' = ppPatternParensType _caseBranchPattern
+      e' = ppMaybeTopExpression isTop _caseBranchExpression
+  pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e'
 
-instance (SingI s) => PrettyPrint (Case s) where
-  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Case s -> Sem r ()
-  ppCode Case {..} = do
-    let exp' = ppExpressionType _caseExpression
-    ppCode _caseKw <+> exp' <+> ppCode Kw.kwOf <+> ppBranches _caseBranches
-    where
-      ppBranches :: NonEmpty (CaseBranch s) -> Sem r ()
-      ppBranches = \case
-        b :| [] -> braces (ppCaseBranch True b)
-        _ -> braces (blockIndent (vsepHard (ppCaseBranch False <$> _caseBranches)))
+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
+  where
+    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)
+      _ -> case isTop of
+        Top -> do
+          let brs =
+                vsepHard (ppCaseBranch' False NotTop <$> NonEmpty.init _caseBranches)
+                  <> hardline
+                  <> ppCaseBranch' False Top (NonEmpty.last _caseBranches)
+          hardline <> indent brs
+        NotTop -> space <> braces (blockIndent (vsepHard (ppCaseBranch' False NotTop <$> _caseBranches)))
 
-      ppCaseBranch :: Bool -> CaseBranch s -> Sem r ()
-      ppCaseBranch singleBranch b = pipeHelper <?+> ppCode b
-        where
-          pipeHelper :: Maybe (Sem r ())
-          pipeHelper
-            | singleBranch = Nothing
-            | otherwise = Just (ppCode (b ^. caseBranchPipe . unIrrelevant))
+    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
 
-instance (SingI s) => PrettyPrint (If s) where
-  ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => If s -> Sem r ()
-  ppCode If {..} = do
-    ppCode _ifKw <+> hardline <> indent (vsepHard (ppIfBranch <$> _ifBranches) <> hardline <> ppIfBranchElse _ifBranchElse)
-    where
-      ppIfBranch :: IfBranch s -> Sem r ()
-      ppIfBranch b = pipeHelper <+> ppCode b
-        where
-          pipeHelper :: Sem r ()
-          pipeHelper = ppCode (b ^. ifBranchPipe . unIrrelevant)
+instance (SingI s) => PrettyPrint (IfBranch s) where
+  ppCode IfBranch {..} = do
+    let cond' = ppExpressionType _ifBranchCondition
+        e' = ppExpressionType _ifBranchExpression
+    cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e'
 
-      ppIfBranchElse :: IfBranchElse s -> Sem r ()
-      ppIfBranchElse b = pipeHelper <+> ppCode b
-        where
-          pipeHelper :: Sem r ()
-          pipeHelper = ppCode (b ^. ifBranchElsePipe . unIrrelevant)
+ppIfBranchElse :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> IfBranchElse s -> Sem r ()
+ppIfBranchElse isTop IfBranchElse {..} = do
+  let e' = ppMaybeTopExpression isTop _ifBranchElseExpression
+  ppCode _ifBranchElseKw <+> ppCode _ifBranchElseAssignKw <> oneLineOrNext e'
+
+ppIf :: forall r s. (Members '[ExactPrint, Reader Options] r, SingI s) => IsTop -> If s -> Sem r ()
+ppIf isTop If {..} = do
+  ppCode _ifKw <+> hardline <> indent (vsepHard (ppIfBranch <$> _ifBranches) <> hardline <> ppIfBranchElse' _ifBranchElse)
+  where
+    ppIfBranch :: IfBranch s -> Sem r ()
+    ppIfBranch b = pipeHelper <+> ppCode b
+      where
+        pipeHelper :: Sem r ()
+        pipeHelper = ppCode (b ^. ifBranchPipe . unIrrelevant)
+
+    ppIfBranchElse' :: IfBranchElse s -> Sem r ()
+    ppIfBranchElse' b = pipeHelper <+> ppIfBranchElse isTop b
+      where
+        pipeHelper :: Sem r ()
+        pipeHelper = ppCode (b ^. ifBranchElsePipe . unIrrelevant)
 
 instance PrettyPrint Universe where
   ppCode Universe {..} = ppCode _universeKw <+?> (noLoc . pretty <$> _universeLevel)
@@ -661,29 +689,6 @@ ppLRExpression associates fixlr e =
     (atomParens associates (atomicity e) fixlr)
     (ppCode e)
 
-instance (SingI s) => PrettyPrint (CaseBranch s) where
-  ppCode CaseBranch {..} = do
-    let pat' = ppPatternParensType _caseBranchPattern
-        e' = ppExpressionType _caseBranchExpression
-    pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e'
-
-instance (SingI s) => PrettyPrint (NewCaseBranch s) where
-  ppCode NewCaseBranch {..} = do
-    let pat' = ppPatternParensType _newCaseBranchPattern
-        e' = ppExpressionType _newCaseBranchExpression
-    pat' <+> ppCode _newCaseBranchAssignKw <> oneLineOrNext e'
-
-instance (SingI s) => PrettyPrint (IfBranch s) where
-  ppCode IfBranch {..} = do
-    let cond' = ppExpressionType _ifBranchCondition
-        e' = ppExpressionType _ifBranchExpression
-    cond' <+> ppCode _ifBranchAssignKw <> oneLineOrNext e'
-
-instance (SingI s) => PrettyPrint (IfBranchElse s) where
-  ppCode IfBranchElse {..} = do
-    let e' = ppExpressionType _ifBranchElseExpression
-    ppCode _ifBranchElseKw <+> ppCode _ifBranchElseAssignKw <> oneLineOrNext e'
-
 ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
 ppBlock items = vsep (sepEndSemicolon (fmap ppCode items))
 
@@ -813,14 +818,13 @@ instance PrettyPrint Expression where
     ExpressionInfixApplication a -> ppCode a
     ExpressionPostfixApplication a -> ppCode a
     ExpressionLambda l -> ppCode l
-    ExpressionLet lb -> ppCode lb
+    ExpressionLet lb -> ppLet NotTop lb
     ExpressionUniverse u -> ppCode u
     ExpressionLiteral l -> ppCode l
     ExpressionFunction f -> ppCode f
-    ExpressionCase c -> ppCode c
-    ExpressionNewCase c -> ppCode c
-    ExpressionIf c -> ppCode c
-    ExpressionIterator i -> ppCode i
+    ExpressionCase c -> ppCase NotTop c
+    ExpressionIf c -> ppIf NotTop c
+    ExpressionIterator i -> ppIterator NotTop i
     ExpressionNamedApplication i -> ppCode i
     ExpressionNamedApplicationNew i -> ppCode i
     ExpressionRecordUpdate i -> ppCode i
@@ -927,7 +931,7 @@ instance (SingI s) => PrettyPrint (FunctionClause s) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => FunctionClause s -> Sem r ()
   ppCode FunctionClause {..} = do
     let pats' = hsep (ppPatternAtomType <$> _clausenPatterns)
-        e' = ppExpressionType _clausenBody
+        e' = ppTopExpressionType _clausenBody
     ppCode _clausenPipeKw <+> pats' <+> ppCode _clausenAssignKw <> oneLineOrNext e'
 
 instance (SingI s) => PrettyPrint (Argument s) where
@@ -983,7 +987,7 @@ instance (SingI s) => PrettyPrint (FunctionDef s) where
         pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas
         sig' = ppFunctionSignature fun
         body' = case _signBody of
-          SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppExpressionType e)
+          SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppTopExpressionType e)
           SigBodyClauses k -> line <> indent (vsep (ppCode <$> k))
     doc'
       ?<> pragmas'

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -1984,21 +1984,6 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do
         ..
       }
 
-checkNewCaseBranch ::
-  forall r.
-  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) =>
-  NewCaseBranch 'Parsed ->
-  Sem r (NewCaseBranch 'Scoped)
-checkNewCaseBranch NewCaseBranch {..} = withLocalScope $ do
-  pattern' <- checkParsePatternAtoms _newCaseBranchPattern
-  expression' <- (checkParseExpressionAtoms _newCaseBranchExpression)
-  return $
-    NewCaseBranch
-      { _newCaseBranchPattern = pattern',
-        _newCaseBranchExpression = expression',
-        ..
-      }
-
 checkCase ::
   (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) =>
   Case 'Parsed ->
@@ -2011,22 +1996,7 @@ checkCase Case {..} = do
       { _caseExpression = caseExpression',
         _caseBranches = caseBranches',
         _caseKw,
-        _caseParens
-      }
-
-checkNewCase ::
-  (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader EntryPoint] r) =>
-  NewCase 'Parsed ->
-  Sem r (NewCase 'Scoped)
-checkNewCase NewCase {..} = do
-  caseBranches' <- mapM checkNewCaseBranch _newCaseBranches
-  caseExpression' <- checkParseExpressionAtoms _newCaseExpression
-  return $
-    NewCase
-      { _newCaseExpression = caseExpression',
-        _newCaseBranches = caseBranches',
-        _newCaseKw,
-        _newCaseOfKw
+        _caseOfKw
       }
 
 checkIfBranch ::
@@ -2281,7 +2251,6 @@ checkExpressionAtom e = case e of
   AtomIdentifier n -> pure . AtomIdentifier <$> checkScopedIden n
   AtomLambda lam -> pure . AtomLambda <$> checkLambda lam
   AtomCase c -> pure . AtomCase <$> checkCase c
-  AtomNewCase c -> pure . AtomNewCase <$> checkNewCase c
   AtomIf c -> pure . AtomIf <$> checkIf c
   AtomLet letBlock -> pure . AtomLet <$> checkLet letBlock
   AtomUniverse uni -> return (pure (AtomUniverse uni))
@@ -2525,7 +2494,6 @@ checkParens e@(ExpressionAtoms as _) = case as of
       let scopedIdenNoFix = over scopedIdenSrcName (set S.nameFixity Nothing) scopedId
       return (ExpressionParensIdentifier scopedIdenNoFix)
     AtomIterator i -> ExpressionIterator . set iteratorParens True <$> checkIterator i
-    AtomCase c -> ExpressionCase . set caseParens True <$> checkCase c
     AtomRecordUpdate u -> ExpressionParensRecordUpdate . ParensRecordUpdate <$> checkRecordUpdate u
     _ -> checkParseExpressionAtoms e
   _ -> checkParseExpressionAtoms e
@@ -2823,7 +2791,6 @@ parseTerm =
     <|> parseFunction
     <|> parseLambda
     <|> parseCase
-    <|> parseNewCase
     <|> parseIf
     <|> parseList
     <|> parseLiteral
@@ -2874,14 +2841,6 @@ parseTerm =
           AtomCase l -> Just l
           _ -> Nothing
 
-    parseNewCase :: Parse Expression
-    parseNewCase = ExpressionNewCase <$> P.token case_ mempty
-      where
-        case_ :: ExpressionAtom 'Scoped -> Maybe (NewCase 'Scoped)
-        case_ s = case s of
-          AtomNewCase l -> Just l
-          _ -> Nothing
-
     parseIf :: Parse Expression
     parseIf = ExpressionIf <$> P.token if_ mempty
       where

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

@@ -830,7 +830,6 @@ expressionAtom =
       <|> AtomIdentifier <$> name
       <|> AtomUniverse <$> universe
       <|> AtomLambda <$> lambda
-      <|> P.try (AtomNewCase <$> newCase)
       <|> AtomCase <$> case_
       <|> AtomFunction <$> function
       <|> AtomLet <$> letBlock
@@ -1114,37 +1113,21 @@ letBlock = do
   _letExpression <- parseExpressionAtoms
   return Let {..}
 
-caseBranch :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (CaseBranch 'Parsed)
-caseBranch = do
-  _caseBranchPipe <- Irrelevant <$> kw kwPipe
+caseBranch :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (CaseBranch 'Parsed)
+caseBranch _caseBranchPipe = do
   _caseBranchPattern <- parsePatternAtoms
   _caseBranchAssignKw <- Irrelevant <$> kw kwAssign
   _caseBranchExpression <- parseExpressionAtoms
   return CaseBranch {..}
 
-case_ :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Case 'Parsed)
-case_ = do
+case_ :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (Case 'Parsed)
+case_ = P.label "case" $ do
   _caseKw <- kw kwCase
   _caseExpression <- parseExpressionAtoms
-  _caseBranches <- some1 caseBranch
-  let _caseParens = False
+  _caseOfKw <- kw kwOf
+  _caseBranches <- braces (pipeSep1 caseBranch) <|> pipeSep1 caseBranch
   return Case {..}
 
-newCaseBranch :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (NewCaseBranch 'Parsed)
-newCaseBranch _newCaseBranchPipe = do
-  _newCaseBranchPattern <- parsePatternAtoms
-  _newCaseBranchAssignKw <- Irrelevant <$> kw kwAssign
-  _newCaseBranchExpression <- parseExpressionAtoms
-  return NewCaseBranch {..}
-
-newCase :: forall r. (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => ParsecS r (NewCase 'Parsed)
-newCase = P.label "new case" $ do
-  _newCaseKw <- kw kwCase
-  _newCaseExpression <- parseExpressionAtoms
-  _newCaseOfKw <- kw kwOf
-  _newCaseBranches <- braces (pipeSep1 newCaseBranch)
-  return NewCase {..}
-
 ifBranch' :: (Members '[ParserResultBuilder, PragmasStash, JudocStash] r) => Irrelevant KeywordRef -> ParsecS r (IfBranch 'Parsed)
 ifBranch' _ifBranchPipe = do
   _ifBranchCondition <- parseExpressionAtoms

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -720,7 +720,6 @@ goExpression = \case
   ExpressionParensIdentifier nt -> return (goIden nt)
   ExpressionApplication a -> goApplication a
   ExpressionCase a -> Internal.ExpressionCase <$> goCase a
-  ExpressionNewCase a -> Internal.ExpressionCase <$> goNewCase a
   ExpressionIf a -> goIf a
   ExpressionInfixApplication ia -> Internal.ExpressionApplication <$> goInfix ia
   ExpressionPostfixApplication pa -> Internal.ExpressionApplication <$> goPostfix pa
@@ -1054,7 +1053,7 @@ goCase :: forall r. (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Err
 goCase c = do
   _caseExpression <- goExpression (c ^. caseExpression)
   _caseBranches <- mapM goBranch (c ^. caseBranches)
-  let _caseParens = c ^. caseParens
+  let _caseParens = False
       _caseExpressionType :: Maybe Internal.Expression = Nothing
       _caseExpressionWholeType :: Maybe Internal.Expression = Nothing
   return Internal.Case {..}
@@ -1065,21 +1064,6 @@ goCase c = do
       _caseBranchExpression <- goExpression (b ^. caseBranchExpression)
       return Internal.CaseBranch {..}
 
-goNewCase :: forall r. (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => NewCase 'Scoped -> Sem r Internal.Case
-goNewCase c = do
-  _caseExpression <- goExpression (c ^. newCaseExpression)
-  _caseBranches <- mapM goBranch (c ^. newCaseBranches)
-  let _caseParens = False
-      _caseExpressionType :: Maybe Internal.Expression = Nothing
-      _caseExpressionWholeType :: Maybe Internal.Expression = Nothing
-  return Internal.Case {..}
-  where
-    goBranch :: NewCaseBranch 'Scoped -> Sem r Internal.CaseBranch
-    goBranch b = do
-      _caseBranchPattern <- goPatternArg (b ^. newCaseBranchPattern)
-      _caseBranchExpression <- goExpression (b ^. newCaseBranchExpression)
-      return Internal.CaseBranch {..}
-
 goLambda :: forall r. (Members '[Reader DefaultArgsStack, Builtins, NameIdGen, Error ScoperError, Reader Pragmas, Reader S.InfoTable] r) => Lambda 'Scoped -> Sem r Internal.Lambda
 goLambda l = do
   clauses' <- mapM goClause (l ^. lambdaClauses)

tests/Anoma/Compilation/positive/test026.juvix

@@ -18,58 +18,51 @@ last {A} : List A -> Maybe A
 
 front : {A : Type} → Queue A → Maybe A
   | q :=
-    case qfst q of {
+    case qfst q of
       | nil := last (qsnd q)
-      | x :: _ := just x
-    };
+      | x :: _ := just x;
 
 drop_front : {A : Type} → Queue A → Queue A
   | {A} q :=
     let
       q' : Queue A := queue (tail (qfst q)) (qsnd q);
-    in case qfst q' of {
+    in case qfst q' of
          | nil := queue (reverse (qsnd q')) nil
-         | _ := q'
-       };
+         | _ := q';
 
 pop_front {A} : Queue A -> Maybe (A × Queue A)
   | (queue xs ys) :=
-    case xs of {
+    case xs of
       | h :: t := just (h, queue t ys)
       | [] :=
-        case reverse ys of {
+        case reverse ys of
           | h :: t := just (h, queue t [])
-          | [] := nothing
-        }
-    };
+          | [] := nothing;
 
 push_back : {A : Type} → Queue A → A → Queue A
   | q x :=
-    case qfst q of {
+    case qfst q of
       | nil := queue (x :: nil) (qsnd q)
-      | q' := queue q' (x :: qsnd q)
-    };
+      | q' := queue q' (x :: qsnd q);
 
 is_empty : {A : Type} → Queue A → Bool
   | q :=
-    case qfst q of {
+    case qfst q of
       | nil :=
         case qsnd q of {
           | nil := true
           | _ := false
         }
-      | _ := false
-    };
+      | _ := false;
 
 empty : {A : Type} → Queue A := queue nil nil;
 
 terminating
 g : List Nat → Queue Nat → List Nat
   | acc q :=
-    case pop_front q of {
+    case pop_front q of
       | nothing := acc
-      | just (h, q') := g (h :: acc) q'
-    };
+      | just (h, q') := g (h :: acc) q';
 
 f : Nat → Queue Nat → List Nat
   | zero q := g nil q

tests/Anoma/Compilation/positive/test028.juvix

@@ -13,8 +13,8 @@ force : (Unit → Stream) → Stream
 terminating
 sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
   | p s unit :=
-    case force s
-      | cons h t :=
+    case force s of
+      cons h t :=
         if (p h) (cons h (sfilter p t)) (force (sfilter p t));
 
 shead : Stream → Nat
@@ -37,8 +37,8 @@ indivisible : Nat → Nat → Bool
 terminating
 eratostenes : (Unit → Stream) → Unit → Stream
   | s unit :=
-    case force s
-      | cons n t :=
+    case force s of
+      cons n t :=
         cons n (eratostenes (sfilter (indivisible n) t));
 
 primes : Unit → Stream := eratostenes (numbers 2);

tests/Anoma/Compilation/positive/test035.juvix

@@ -25,13 +25,12 @@ terminating
 f : Tree → Nat
   | leaf := 1
   | (node l r) :=
-    case g l, g r of {
+    case g l, g r of
       | leaf, leaf := 3
       | node l r, leaf := mod ((f l + f r) * 2) 20000
       | node l1 r1, node l2 r2 :=
         mod ((f l1 + f r1) * (f l2 + f r2)) 20000
-      | _, node l r := mod (f l + f r) 20000
-    };
+      | _, node l r := mod (f l + f r) 20000;
 
 g : Tree → Tree
   | leaf := leaf

tests/Anoma/Compilation/positive/test038.juvix

@@ -4,8 +4,7 @@ module test038;
 import Stdlib.Prelude open;
 
 main : Nat :=
-  case 1, 2 of {
+  case 1, 2 of
     | suc _, zero := 0
     | suc _, suc x := x
-    | _ := 19
-  };
+    | _ := 19;

tests/Anoma/Compilation/positive/test052.juvix

@@ -148,9 +148,8 @@ res : Either Error Val := eval (double+1 # num 7);
 -- TODO: Use Partial or failwith in left branches when anoma backend supports
 -- strings
 main : List Nat :=
-  case res >>= getNat of {
+  case res >>= getNat of
     | left (ScopeError n ctx) := []
     | left (ExpectedNat e) := []
     | left ExpectedLambda := []
-    | right r := [r]
-  };
+    | right r := [r];

tests/Anoma/Compilation/positive/test057.juvix

@@ -5,7 +5,7 @@ import Stdlib.Prelude open;
 
 myfun : {A : Type} -> (A -> A -> A) -> A -> List A -> A
   | f x xs :=
-    case x :: xs
+    case x :: xs of
       | nil := x
       | y :: nil := y
       | y :: z :: _ := f y z;

tests/Casm/Compilation/positive/test024.juvix

@@ -27,13 +27,13 @@ f : Tree → Nat
       terminating
       a :
         Nat :=
-          case l
+          case l of
             | leaf := 1
             | node l r := f l + f r;
       terminating
       b :
         Nat :=
-          case r
+          case r of
             | node l r := f l + f r
             | _ := 2;
     in a * b;

tests/Casm/Compilation/positive/test026.juvix

@@ -3,8 +3,7 @@ module test026;
 
 import Stdlib.Prelude open;
 
-type Queue (A : Type) :=
-  | queue : List A → List A → Queue A;
+type Queue (A : Type) := queue : List A → List A → Queue A;
 
 qfst : {A : Type} → Queue A → List A
   | (queue x _) := x;
@@ -19,23 +18,24 @@ pop_front : {A : Type} → Queue A → Queue A
   | {A} q :=
     let
       q' : Queue A := queue (tail (qfst q)) (qsnd q);
-    in case qfst q'
-      | nil := queue (reverse (qsnd q')) nil
-      | _ := q';
+    in case qfst q' of
+         | nil := queue (reverse (qsnd q')) nil
+         | _ := q';
 
 push_back : {A : Type} → Queue A → A → Queue A
   | q x :=
-    case qfst q
+    case qfst q of
       | nil := queue (x :: nil) (qsnd q)
       | q' := queue q' (x :: qsnd q);
 
 is_empty : {A : Type} → Queue A → Bool
   | q :=
-    case qfst q
+    case qfst q of
       | nil :=
-        (case qsnd q
+        case qsnd q of {
           | nil := true
-          | _ := false)
+          | _ := false
+        }
       | _ := false;
 
 empty : {A : Type} → Queue A := queue nil nil;
@@ -45,8 +45,6 @@ g {{Partial}} : List Nat → Queue Nat → List Nat
   | acc q :=
     if (is_empty q) acc (g (front q :: acc) (pop_front q));
 
--- TODO: remove `terminating` after fixing https://github.com/anoma/juvix/issues/2414
-terminating
 f {{Partial}} : Nat → Queue Nat → List Nat
   | zero q := g nil q
   | n@(suc n') q := f n' (push_back q n);
@@ -55,4 +53,4 @@ sum : List Nat → Nat
   | nil := 0
   | (h :: t) := h + sum t;
 
-main : Nat := sum (runPartial (λ {{{_}} := f 100 empty}));
+main : Nat := sum (runPartial λ {{{_}} := f 100 empty});

tests/Casm/Compilation/positive/test057.juvix

@@ -5,7 +5,7 @@ import Stdlib.Prelude open;
 
 myfun : {A : Type} -> (A -> A -> A) -> A -> List A -> A
   | f x xs :=
-    case x :: xs
+    case x :: xs of
       | nil := x
       | y :: nil := y
       | y :: z :: _ := f y z;

tests/Compilation/negative/test002.juvix

@@ -4,7 +4,7 @@ module test002;
 import Stdlib.Prelude open;
 
 f (x : List Nat) : Nat :=
-  case x
+  case x of
     | nil := 0
     | x :: y :: _ := x + y;
 

tests/Compilation/positive/test012.juvix

@@ -14,12 +14,9 @@ gen : Nat → Tree
   | zero := leaf
   | n :=
     if
-      (mod n 3 == 0)
-      (node1 (gen (sub n 1)))
-      (if
-        (mod n 3 == 1)
-        (node2 (gen (sub n 1)) (gen (sub n 1)))
-        (node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1))));
+      | mod n 3 == 0 := node1 (gen (sub n 1))
+      | mod n 3 == 1 := node2 (gen (sub n 1)) (gen (sub n 1))
+      | else := node3 (gen (sub n 1)) (gen (sub n 1)) (gen (sub n 1));
 
 preorder : Tree → IO
   | leaf := printNat 0

tests/Compilation/positive/test015.juvix

@@ -5,25 +5,34 @@ import Stdlib.Prelude open;
 
 terminating
 f : Nat → Nat → Nat
-| x :=
-    let g (y : Nat) : Nat := x + y in
-    if (x == 0)
-       (f 10)
-       (if (x < 10)
-           λ{y := g (f (sub x 1) y)}
-           g);
+  | x :=
+    let
+      g (y : Nat) : Nat := x + y;
+    in if
+      | x == 0 := f 10
+      | else := if (x < 10) λ {y := g (f (sub x 1) y)} g;
 
 g (x : Nat) (h : Nat → Nat) : Nat := x + h x;
 
 terminating
 h : Nat → Nat
-| zero := 0
-| (suc x) := g x h;
+  | zero := 0
+  | (suc x) := g x h;
 
 main : IO :=
-    printNatLn (f 100 500) >> -- 600
-    printNatLn (f 5 0) >> -- 25
-    printNatLn (f 5 5) >> -- 30
-    printNatLn (h 10) >> -- 45
-    printNatLn (g 10 h) >> -- 55
-    printNatLn (g 3 (f 10));
+  printNatLn (f 100 500)
+    >> -- 600
+      printNatLn
+      (f 5 0)
+    >> -- 25
+      printNatLn
+      (f 5 5)
+    >> -- 30
+      printNatLn
+      (h 10)
+    >> -- 45
+      printNatLn
+      (g 10 h)
+    >> -- 55
+      printNatLn
+      (g 3 (f 10));

tests/Compilation/positive/test021.juvix

@@ -7,12 +7,9 @@ terminating
 power' : Nat → Nat → Nat → Nat
   | acc a b :=
     if
-      (b == 0)
-      acc
-      (if
-        (mod b 2 == 0)
-        (power' acc (a * a) (div b 2))
-        (power' (acc * a) (a * a) (div b 2)));
+      | b == 0 := acc
+      | mod b 2 == 0 := power' acc (a * a) (div b 2)
+      | else := power' (acc * a) (a * a) (div b 2);
 
 power : Nat → Nat → Nat := power' 1;
 
@@ -20,4 +17,3 @@ main : IO :=
   printNatLn (power 2 3)
     >> printNatLn (power 3 7)
     >> printNatLn (power 5 11);
-

tests/Compilation/positive/test024.juvix

@@ -13,7 +13,6 @@ gen : Nat → Tree
   | (suc (suc n')) := node (gen n') (gen (suc n'));
 
 g : Tree → Tree
-  
   | leaf := leaf
   | (node l r) := if (isNode l) r (node r l);
 
@@ -25,17 +24,15 @@ f : Tree → Nat
       l : Tree := g l';
       r : Tree := g r';
       terminating
-      a :
-        Nat :=
-          case l
-            | leaf := 1
-            | node l r := f l + f r;
+      a : Nat :=
+        case l of
+          | leaf := 1
+          | node l r := f l + f r;
       terminating
-      b :
-        Nat :=
-          case r
-            | node l r := f l + f r
-            | _ := 2;
+      b : Nat :=
+        case r of
+          | node l r := f l + f r
+          | _ := 2;
     in a * b;
 
 isNode : Tree → Bool
@@ -43,4 +40,3 @@ isNode : Tree → Bool
   | leaf := false;
 
 main : IO := printNatLn (f (gen 10));
-

tests/Compilation/positive/test025.juvix

@@ -6,7 +6,10 @@ import Stdlib.Prelude open;
 terminating
 gcd : Nat → Nat → Nat
   | a b :=
-    if (a > b) (gcd b a) (if (a == 0) b (gcd (mod b a) a));
+    if
+      | a > b := gcd b a
+      | a == 0 := b
+      | else := gcd (mod b a) a;
 
 main : IO :=
   printNatLn (gcd (3 * 7 * 2) (7 * 2 * 11))

tests/Compilation/positive/test026.juvix

@@ -3,8 +3,7 @@ module test026;
 
 import Stdlib.Prelude open;
 
-type Queue (A : Type) :=
-  | queue : List A → List A → Queue A;
+type Queue (A : Type) := queue : List A → List A → Queue A;
 
 qfst : {A : Type} → Queue A → List A
   | (queue x _) := x;
@@ -19,23 +18,24 @@ pop_front : {A : Type} → Queue A → Queue A
   | {A} q :=
     let
       q' : Queue A := queue (tail (qfst q)) (qsnd q);
-    in case qfst q'
-      | nil := queue (reverse (qsnd q')) nil
-      | _ := q';
+    in case qfst q' of
+         | nil := queue (reverse (qsnd q')) nil
+         | _ := q';
 
 push_back : {A : Type} → Queue A → A → Queue A
   | q x :=
-    case qfst q
+    case qfst q of
       | nil := queue (x :: nil) (qsnd q)
       | q' := queue q' (x :: qsnd q);
 
 is_empty : {A : Type} → Queue A → Bool
   | q :=
-    case qfst q
+    case qfst q of
       | nil :=
-        (case qsnd q
+        case qsnd q of {
           | nil := true
-          | _ := false)
+          | _ := false
+        }
       | _ := false;
 
 empty : {A : Type} → Queue A := queue nil nil;
@@ -45,8 +45,6 @@ g {{Partial}} : List Nat → Queue Nat → List Nat
   | acc q :=
     if (is_empty q) acc (g (front q :: acc) (pop_front q));
 
--- TODO: remove `terminating` after fixing https://github.com/anoma/juvix/issues/2414
-terminating
 f {{Partial}} : Nat → Queue Nat → List Nat
   | zero q := g nil q
   | n@(suc n') q := f n' (push_back q n);
@@ -56,6 +54,6 @@ printListNatLn : List Nat → IO
   | (h :: t) :=
     printNat h >> printString " :: " >> printListNatLn t;
 
-main : IO := printListNatLn (runPartial (λ {{{_}} := f 100 empty}));
+main : IO :=
+  printListNatLn (runPartial λ {{{_}} := f 100 empty});
 -- list of numbers from 1 to 100
-

tests/Compilation/positive/test028.juvix

@@ -3,8 +3,7 @@ module test028;
 
 import Stdlib.Prelude open;
 
-type Stream :=
-  | cons : Nat → (Unit → Stream) → Stream;
+type Stream := cons : Nat → (Unit → Stream) → Stream;
 
 force : (Unit → Stream) → Stream
   | f := f unit;
@@ -12,8 +11,8 @@ force : (Unit → Stream) → Stream
 terminating
 sfilter : (Nat → Bool) → (Unit → Stream) → Unit → Stream
   | p s unit :=
-    case force s
-      | cons h t :=
+    case force s of
+      cons h t :=
         if (p h) (cons h (sfilter p t)) (force (sfilter p t));
 
 shead : Stream → Nat
@@ -36,8 +35,8 @@ indivisible : Nat → Nat → Bool
 terminating
 eratostenes : (Unit → Stream) → Unit → Stream
   | s unit :=
-    case force s
-      | cons n t :=
+    case force s of
+      cons n t :=
         cons n (eratostenes (sfilter (indivisible n) t));
 
 primes : Unit → Stream := eratostenes (numbers 2);
@@ -47,4 +46,3 @@ main : IO :=
     >> printNatLn (snth 50 primes)
     >> printNatLn (snth 100 primes)
     >> printNatLn (snth 200 primes);
-

tests/Compilation/positive/test029.juvix

@@ -15,4 +15,3 @@ main : IO :=
     >> printNatLn (ack 2 7)
     >> printNatLn (ack 2 13)
     >> printNatLn (ack 3 7);
-

tests/Compilation/positive/test032.juvix

@@ -7,8 +7,7 @@ split : {A : Type} → Nat → List A → List A × List A
   | zero xs := nil, xs
   | (suc n) nil := nil, nil
   | (suc n) (x :: xs) :=
-    case split n xs
-      | l1, l2 := x :: l1, l2;
+    case split n xs of l1, l2 := x :: l1, l2;
 
 terminating
 merge' : List Nat → List Nat → List Nat
@@ -23,10 +22,10 @@ sort : List Nat → List Nat
     let
       n : Nat := length xs;
     in if
-      (n <= 1)
-      xs
-      (case split (div n 2) xs
-        | l1, l2 := merge' (sort l1) (sort l2));
+      | n <= 1 := xs
+      | else :=
+        case split (div n 2) xs of
+          l1, l2 := merge' (sort l1) (sort l2);
 
 terminating
 uniq : List Nat → List Nat

tests/Compilation/positive/test035.juvix

@@ -24,7 +24,7 @@ terminating
 f : Tree → Nat
   | leaf := 1
   | (node l r) :=
-    case g l, g r
+    case g l, g r of
       | leaf, leaf := 3
       | node l r, leaf := mod ((f l + f r) * 2) 20000
       | node l1 r1, node l2 r2 :=

tests/Compilation/positive/test037.juvix

@@ -12,10 +12,9 @@ f (l : List ((Nat → Nat) → Nat → Nat)) : Nat :=
       y : Nat → Nat := id;
     in (let
          z : (Nat → Nat) → Nat → Nat := id;
-       in case l of {
+       in case l of
             | _ :: _ := id
             | _ := id
-          }
          z)
       y)
     7;

tests/Compilation/positive/test052.juvix

@@ -180,7 +180,7 @@ double+1 : Expr := Λ (compose # +1 # double # ! 0);
 res : Either Error Val := eval (double+1 # num 7);
 
 main : IO :=
-  case res
+  case res of
     | left (ScopeError n ctx) :=
       printStringLn
         ("ScopeError: "

tests/Compilation/positive/test057.juvix

@@ -5,7 +5,7 @@ import Stdlib.Prelude open;
 
 myfun : {A : Type} -> (A -> A -> A) -> A -> List A -> A
   | f x xs :=
-    case x :: xs
+    case x :: xs of
       | nil := x
       | y :: nil := y
       | y :: z :: _ := f y z;

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
-  | x := case x of {_ := false};
+  | x := case x of _ := false;
 
 main : Triple Nat Nat Nat :=
   let
@@ -32,14 +32,15 @@ main : Triple Nat Nat Nat :=
     f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
       (@Triple{fst := fst * 10});
   in if
-    (mf
-      mkPair@{
-        fst := mkPair true nil;
-        snd := 0 :: nil
-      })
-    (f p')
-    mkTriple@{
-      fst := 0;
-      thd := 0;
-      snd := 0
-    };
+    | mf
+        mkPair@{
+          fst := mkPair true nil;
+          snd := 0 :: nil
+        } :=
+      (f p')
+    | else :=
+      mkTriple@{
+        fst := 0;
+        thd := 0;
+        snd := 0
+      };

tests/Compilation/positive/test064.juvix

@@ -36,7 +36,6 @@ even' : Nat -> Bool := even;
 
 main : Nat :=
   sum 3
-    + case even' 6 || g true || h true of {
+    + case even' 6 || g true || h true of
         | true := if (g false) (f 1 2 + sum 7 + j 0) 0
-        | false := f (3 + 4) (f 0 8) + loop
-      };
+        | false := f (3 + 4) (f 0 8) + loop;

tests/Geb/positive/Compilation/test007.juvix

@@ -10,6 +10,6 @@ type Box :=
   | box : Box2 -> Box;
 
 main : Nat :=
-  case box (box2 3 5)
-    | box (box2 x y) := x + y;
+  case box (box2 3 5) of
+    box (box2 x y) := x + y;
 -- result: 8

tests/Geb/positive/Compilation/test008.juvix

@@ -10,7 +10,7 @@ type enum :=
   | opt3 : Bool -> (Bool -> Bool -> Bool) -> Bool -> enum;
 
 main : Bool :=
-  case opt3 true λ {x y := if y false x} false
+  case opt3 true λ {x y := if y false x} false of
     | opt0 := false
     | opt1 b := b
     | opt2 b f := f b

tests/Geb/positive/Compilation/test011.juvix

@@ -17,14 +17,14 @@ id''' : ((Nat → Nat) → Nat → Nat) → (Nat → Nat) → Nat → Nat
 
 f : Pair → Nat
   | l :=
-    (case l
+    (case l of
         | pair x zero := x
         | _ := id'')
       (let
         y : Nat → Nat := id';
       in (let
           z : (Nat → Nat) → Nat → Nat := id'';
-        in (case l
+        in (case l of
             | pair _ zero := id'''
             | _ := id''')
           z)

tests/Geb/positive/Compilation/test027.juvix

@@ -7,7 +7,7 @@ type Pair :=
   | pair : Nat -> Nat -> Pair;
 
 main : Nat :=
-  case pair 1 2
+  case pair 1 2 of
     | pair (suc _) zero := 0
     | pair (suc _) (suc x) := x
     | _ := 19;

tests/Internal/positive/Case.juvix

@@ -4,18 +4,16 @@ import Stdlib.Prelude open;
 
 not' : Bool → Bool
   | b :=
-    case b of {
+    case b of
       | true := false
-      | false := true
-    };
+      | false := true;
 
 terminating
 andList : List Bool → Bool
   | l :=
-    case l of {
+    case l of
       | nil := true
-      | x :: xs := x && andList xs
-    };
+      | x :: xs := x && andList xs;
 
 main : IO :=
   printBoolLn (not' false)

tests/VampIR/positive/Compilation/test005.juvix

@@ -11,6 +11,6 @@ type Box :=
 
 main : Nat -> Nat -> Nat
   | x y :=
-    case box (box2 x y)
+    case box (box2 x y) of
       | box (box2 x y) := x + y;
 -- result: 8

tests/VampIR/positive/Compilation/test017.juvix

@@ -7,26 +7,23 @@ import Stdlib.Prelude open;
 terminating
 f : Nat → Nat
   | x :=
-    case x of {
+    case x of
       | zero := 1
-      | suc y := 2 * x + g y
-    };
+      | suc y := 2 * x + g y;
 
 terminating
 g : Nat → Nat
   | x :=
-    case x of {
+    case x of
       | zero := 1
-      | suc y := x + h y
-    };
+      | suc y := x + h y;
 
 terminating
 h : Nat → Nat
   | x :=
-    case x of {
+    case x of
       | zero := 1
-      | suc y := x * f y
-    };
+      | suc y := x * f y;
 
 main : Nat → Nat
   | x := f x + f (2 * x);

tests/VampIR/positive/Compilation/test018.juvix

@@ -10,9 +10,8 @@ pow : Nat -> Nat
 hash' : Nat -> Nat -> Nat
   | (suc n@(suc (suc m))) x :=
     if
-      (x < pow n)
-      (hash' n x)
-      (mod (div (x * x) (pow m)) (pow 6))
+      | x < pow n := hash' n x
+      | else := mod (div (x * x) (pow m)) (pow 6)
   | _ x := x * x;
 
 hash : Nat -> Nat := hash' 16;

tests/VampIR/positive/Compilation/test019.juvix

@@ -3,9 +3,7 @@ module test019;
 
 import Stdlib.Prelude open;
 
-main : Nat -> Nat -> Nat
-  | x y :=
-    case tail (id (x :: y :: nil)) of {
-      | nil := 0
-      | h :: _ := h
-    };
+main (x y : Nat) : Nat :=
+  case tail (id (x :: y :: nil)) of
+    | nil := 0
+    | h :: _ := h;

tests/VampIR/positive/Compilation/test021.juvix

@@ -9,12 +9,9 @@ power : Nat → Nat → Nat :=
     terminating
     power' (acc a b : Nat) : Nat :=
       if
-        (b == 0)
-        acc
-        (if
-          (mod b 2 == 0)
-          (power' acc (a * a) (div b 2))
-          (power' (acc * a) (a * a) (div b 2)));
+        | b == 0 := acc
+        | mod b 2 == 0 := power' acc (a * a) (div b 2)
+        | else := power' (acc * a) (a * a) (div b 2);
   in power' 1;
 
 main : Nat -> Nat -> Nat := power;

tests/VampIR/positive/Compilation/test023.juvix

@@ -3,8 +3,6 @@ module test023;
 
 import Stdlib.Prelude open;
 
-main : Nat → Nat → Nat
-  | x y :=
-    case λ {z := if (x == z) (x, 0) (x, z)} (y + x) of {
-      a, b := a + b
-    };
+main (x y : Nat) : Nat :=
+    case λ {z := if (x == z) (x, 0) (x, z)} (y + x) of
+      a, b := a + b;

tests/negative/issue1337/DoubleBraces.juvix

@@ -4,4 +4,4 @@ type Nat :=
   | O : Nat
   | S : Nat -> Nat;
 
-fun (n : Nat) : Nat := case n of {S {{y}} := O};
+fun (n : Nat) : Nat := case n of S {{y}} := O;

tests/positive/Alias.juvix

@@ -20,10 +20,9 @@ not2 (b : Boolean) : Boolean :=
   let
     syntax alias yes := ⊤;
     syntax alias no := ⊥;
-  in case b of {
+  in case b of
        | no := yes
-       | yes := no
-     };
+       | yes := no;
 
 module ExportAlias;
   syntax alias Binary := Bool;

tests/positive/AliasRecordConstructor.juvix

@@ -12,7 +12,7 @@ t : T :=
   };
 
 t1 : T -> A
- | mkT'@{ field := x } := x;
+  | mkT'@{field := x} := x;
 
 syntax iterator it {init := 0; range := 1};
 it : (A → A) → T → A

tests/positive/Format.juvix

@@ -30,31 +30,28 @@ M;
 end;
 
 -- case with single branch
-case1 (n : Nat) : Nat := case n of {x := zero};
+case1 (n : Nat) : Nat := case n of x := zero;
 
 -- case with multiple branches
 case2 (n : Nat) : Nat :=
-  case n of {
+  case n of
     | zero := zero
-    | _ := zero
-  };
+    | _ := zero;
 
 -- case on nested case
 case3 (n : Nat) : Nat :=
-  case case n of {_ := zero} of {
+  case case n of {_ := zero} of
     | zero := zero
-    | _ := zero
-  };
+    | _ := zero;
 
 -- case on nested case expression
 case4 (n : Nat) : Nat :=
-  case n of {
+  case n of
     | zero := case n of {x := zero}
-    | _ := zero
-  };
+    | _ := zero;
 
 -- -- case with application subject
-case5 (n : Nat) : Nat := case id n of {x := zero};
+case5 (n : Nat) : Nat := case id n of x := zero;
 
 -- qualified commas
 t4 : String := "a" M., "b" M., "c" M., "d";

tests/positive/ImportShadow/Main.juvix

@@ -4,13 +4,12 @@ import Nat open;
 
 type Unit := unit : Unit;
 
-f : Nat := case unit of {is-zero := zero};
+f : Nat := case unit of is-zero := zero;
 
 f2 : Nat :=
-  case suc zero of {
+  case suc zero of
     | suc is-zero := zero
-    | _ := zero
-  };
+    | _ := zero;
 
 f3 : Nat → Nat
   | (suc is-zero) := is-zero

tests/positive/ImportShadow/Nat.juvix

@@ -10,7 +10,6 @@ type Nat :=
 
 is-zero : Nat → Bool
   | n :=
-    case n of {
+    case n of
       | zero := true
-      | suc _ := false
-    };
+      | suc _ := false;

tests/positive/InstanceImport/Main.juvix

@@ -10,4 +10,4 @@ type Bool :=
 instance
 boolI : T Bool := mkT λ {x := x};
 
-main : Bool := case T.pp unit of {unit := T.pp true};
+main : Bool := case T.pp unit of unit := T.pp true;

tests/positive/Internal/Case.juvix

@@ -4,31 +4,27 @@ import Stdlib.Prelude open;
 
 isZero : Nat → Bool
   | n :=
-    case n of {
+    case n of
       | zero := true
-      | k@(suc _) := false
-    };
+      | k@(suc _) := false;
 
 id' : Bool → {A : Type} → A → A
   | b :=
-    case b of {
+    case b of
       | true := id
-      | false := id
-    };
+      | false := id;
 
 pred : Nat → Nat
   | n :=
-    case n of {
+    case n of
       | zero := zero
-      | suc n := n
-    };
+      | suc n := n;
 
 appIf : {A : Type} → Bool → (A → A) → A → A
   | b f :=
-    case b of {
+    case b of
       | true := f
-      | false := id
-    };
+      | false := id;
 
 appIf2 : {A : Type} → Bool → (A → A) → A → A
   | b f a :=
@@ -40,7 +36,6 @@ appIf2 : {A : Type} → Bool → (A → A) → A → A
 
 nestedCase1 : {A : Type} → Bool → (A → A) → A → A
   | b f :=
-    case b of {
+    case b of
       | true := case b of {_ := id}
-      | false := id
-    };
+      | false := id;

tests/positive/Iterators.juvix

@@ -19,7 +19,6 @@ main : Bool :=
     z : Bool := false;
   in itconst (a := true; b := false) (c in false; d in false)
        for (x := true) (y in false)
-         case x of {
+         case x of
            | true := y
-           | false := z
-         };
+           | false := z;

tests/positive/LetShadow.juvix

@@ -7,9 +7,8 @@ type Nat :=
 type Unit := unit : Unit;
 
 t : Nat :=
-  case unit of {
+  case unit of
     x :=
       let
         x : Nat := suc zero;
-      in x
-  };
+      in x;

tests/positive/NestedPatterns.juvix

@@ -9,7 +9,6 @@ toList : {A : Type} -> MyList A -> List A
 
 f : MyList Nat -> Nat
   | xs :=
-    case toList xs of {
+    case toList xs of
       | suc n :: nil := n
-      | _ := zero
-    };
+      | _ := zero;

tests/positive/Traits2.juvix

@@ -79,7 +79,7 @@ import Stdlib.Data.Product open;
   {{Semigroup A}}
   {B C : Type}
   : A × B -> (B -> A × C) -> A × C
-  | (a, b) f := case f b of {a', b' := a <> a', b'};
+  | (a, b) f := case f b of a', b' := a <> a', b';
 
 instance
 ×-Monad