Add new case syntax (#2353)

src/Juvix/Compiler/Concrete/Keywords.hs

@@ -45,6 +45,7 @@ import Juvix.Data.Keyword.All
     kwLet,
     kwMapsTo,
     kwModule,
+    kwOf,
     kwOpen,
     kwOperator,
     kwPipe,
@@ -81,6 +82,7 @@ allKeywords =
     kwLambda,
     kwLet,
     kwModule,
+    kwOf,
     kwOpen,
     kwPipe,
     kwPublic,

src/Juvix/Compiler/Concrete/Language.hs

@@ -1060,6 +1060,7 @@ data Expression
   | ExpressionPostfixApplication PostfixApplication
   | ExpressionList (List 'Scoped)
   | ExpressionCase (Case 'Scoped)
+  | ExpressionNewCase (NewCase 'Scoped)
   | ExpressionLambda (Lambda 'Scoped)
   | ExpressionLet (Let 'Scoped)
   | ExpressionUniverse Universe
@@ -1281,6 +1282,44 @@ 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 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 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 Initializer (s :: Stage) = Initializer
   { _initializerPattern :: PatternParensType s,
     _initializerAssignKw :: Irrelevant KeywordRef,
@@ -1458,6 +1497,7 @@ data ExpressionAtom (s :: Stage)
   | AtomLambda (Lambda s)
   | AtomList (List s)
   | AtomCase (Case s)
+  | AtomNewCase (NewCase s)
   | AtomHole (HoleType s)
   | AtomDoubleBraces (DoubleBracesExpression s)
   | AtomBraces (WithLoc (ExpressionType s))
@@ -1684,6 +1724,8 @@ makeLenses ''PatternInfixApp
 makeLenses ''PatternPostfixApp
 makeLenses ''Case
 makeLenses ''CaseBranch
+makeLenses ''NewCase
+makeLenses ''NewCaseBranch
 makeLenses ''PatternBinding
 makeLenses ''PatternAtoms
 makeLenses ''ExpressionAtoms
@@ -1746,6 +1788,7 @@ instance HasAtomicity Expression where
     ExpressionUniverse {} -> Atom
     ExpressionFunction {} -> Aggregate funFixity
     ExpressionCase c -> atomicity c
+    ExpressionNewCase c -> atomicity c
     ExpressionIterator i -> atomicity i
     ExpressionNamedApplication i -> atomicity i
     ExpressionRecordUpdate {} -> Aggregate updateFixity
@@ -1762,6 +1805,9 @@ instance HasAtomicity (Iterator s) where
 instance HasAtomicity (Case s) where
   atomicity = const Atom
 
+instance HasAtomicity (NewCase s) where
+  atomicity = const Atom
+
 instance HasAtomicity (Let 'Scoped) where
   atomicity l = atomicity (l ^. letExpression)
 
@@ -1854,9 +1900,20 @@ instance HasLoc (Let 'Scoped) where
 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
+    Nothing -> branchLoc
+    Just p -> getLoc p <> branchLoc
+    where
+      branchLoc :: Interval
+      branchLoc = getLocExpressionType (c ^. newCaseBranchExpression)
+
 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 HasLoc (List s) where
   getLoc List {..} = getLoc _listBracketL <> getLoc _listBracketR
 
@@ -1893,6 +1950,7 @@ instance HasLoc Expression where
     ExpressionLambda i -> getLoc i
     ExpressionList l -> getLoc l
     ExpressionCase i -> getLoc i
+    ExpressionNewCase i -> getLoc i
     ExpressionLet i -> getLoc i
     ExpressionUniverse i -> getLoc i
     ExpressionLiteral i -> getLoc i
@@ -2247,6 +2305,7 @@ instance IsApe Expression ApeLeaf where
     ExpressionIdentifier {} -> leaf
     ExpressionList {} -> leaf
     ExpressionCase {} -> leaf
+    ExpressionNewCase {} -> leaf
     ExpressionLambda {} -> leaf
     ExpressionLet {} -> leaf
     ExpressionUniverse {} -> leaf

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

@@ -312,6 +312,7 @@ instance (SingI s) => PrettyPrint (ExpressionAtom s) where
     AtomLambda l -> ppCode l
     AtomLet lb -> ppCode lb
     AtomCase c -> ppCode c
+    AtomNewCase c -> ppCode c
     AtomList l -> ppCode l
     AtomUniverse uni -> ppCode uni
     AtomRecordUpdate u -> ppCode u
@@ -487,11 +488,45 @@ instance (SingI s) => PrettyPrint (Let s) where
         letExpression' = ppExpressionType _letExpression
     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
+    where
+      ppBranches :: NonEmpty (NewCaseBranch s) -> Sem r ()
+      ppBranches = \case
+        b :| [] -> braces (ppCaseBranch True b)
+        _ -> braces (blockIndent (vsepHard (ppCaseBranch False <$> _newCaseBranches)))
+
+      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
+
 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
-        branches' = indent . vsepHard $ fmap ppCode _caseBranches
-    parensIf _caseParens (ppCode _caseKw <+> exp' <> hardline <> branches')
+    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)))
+
+      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))
 
 instance PrettyPrint Universe where
   ppCode Universe {..} = ppCode _universeKw <+?> (noLoc <$> (pretty <$> _universeLevel))
@@ -592,7 +627,13 @@ instance (SingI s) => PrettyPrint (CaseBranch s) where
   ppCode CaseBranch {..} = do
     let pat' = ppPatternParensType _caseBranchPattern
         e' = ppExpressionType _caseBranchExpression
-    ppCode _caseBranchPipe <+> pat' <+> ppCode _caseBranchAssignKw <> oneLineOrNext e'
+    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'
 
 ppBlock :: (PrettyPrint a, Members '[Reader Options, ExactPrint] r, Traversable t) => t a -> Sem r ()
 ppBlock items = vsep (sepEndSemicolon (fmap ppCode items))
@@ -674,6 +715,7 @@ instance PrettyPrint Expression where
     ExpressionLiteral l -> ppCode l
     ExpressionFunction f -> ppCode f
     ExpressionCase c -> ppCode c
+    ExpressionNewCase c -> ppCode c
     ExpressionIterator i -> ppCode i
     ExpressionNamedApplication i -> ppCode i
     ExpressionRecordUpdate i -> ppCode i

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

@@ -1801,6 +1801,21 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do
         ..
       }
 
+checkNewCaseBranch ::
+  forall r.
+  (Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] 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 '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
   Case 'Parsed ->
@@ -1816,6 +1831,21 @@ checkCase Case {..} = do
         _caseParens
       }
 
+checkNewCase ::
+  (Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] 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
+      }
+
 checkLambda ::
   (Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
   Lambda 'Parsed ->
@@ -2012,6 +2042,7 @@ 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
   AtomLet letBlock -> pure . AtomLet <$> checkLet letBlock
   AtomUniverse uni -> return (pure (AtomUniverse uni))
   AtomFunction fun -> pure . AtomFunction <$> checkFunction fun
@@ -2504,6 +2535,7 @@ parseTerm =
       <|> parseFunction
       <|> parseLambda
       <|> parseCase
+      <|> parseNewCase
       <|> parseList
       <|> parseLiteral
       <|> parseLet
@@ -2544,6 +2576,14 @@ 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
+
     parseList :: Parse Expression
     parseList = ExpressionList <$> P.token case_ mempty
       where

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

@@ -611,6 +611,7 @@ expressionAtom =
       <|> AtomIdentifier <$> name
       <|> AtomUniverse <$> universe
       <|> AtomLambda <$> lambda
+      <|> P.try (AtomNewCase <$> newCase)
       <|> AtomCase <$> case_
       <|> AtomFunction <$> function
       <|> AtomLet <$> letBlock
@@ -879,6 +880,21 @@ case_ = do
   let _caseParens = False
   return Case {..}
 
+newCaseBranch :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] 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 '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] 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 {..}
+
 --------------------------------------------------------------------------------
 -- Universe expression
 --------------------------------------------------------------------------------

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

@@ -744,6 +744,7 @@ goExpression = \case
   ExpressionParensIdentifier nt -> return (goIden nt)
   ExpressionApplication a -> Internal.ExpressionApplication <$> goApplication a
   ExpressionCase a -> Internal.ExpressionCase <$> goCase a
+  ExpressionNewCase a -> Internal.ExpressionCase <$> goNewCase a
   ExpressionInfixApplication ia -> Internal.ExpressionApplication <$> goInfix ia
   ExpressionPostfixApplication pa -> Internal.ExpressionApplication <$> goPostfix pa
   ExpressionLiteral l -> return (Internal.ExpressionLiteral (goLiteral l))
@@ -950,6 +951,21 @@ goCase c = do
       _caseBranchExpression <- goExpression (b ^. caseBranchExpression)
       return Internal.CaseBranch {..}
 
+goNewCase :: forall r. (Members '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] 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 '[Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r) => Lambda 'Scoped -> Sem r Internal.Lambda
 goLambda l = do
   clauses' <- mapM goClause (l ^. lambdaClauses)

tests/Internal/positive/Case.juvix

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

tests/positive/Format.juvix

@@ -31,6 +31,33 @@ M;
   axiom , : String → String → String;
 end;
 
+-- case with single branch
+case1 (n : Nat) : Nat := case n of {x := zero};
+
+-- case with multiple branches
+case2 (n : Nat) : Nat :=
+  case n of {
+    | zero := zero
+    | _ := zero
+  };
+
+-- case on nested case
+case3 (n : Nat) : Nat :=
+  case case n of {_ := zero} of {
+    | zero := zero
+    | _ := zero
+  };
+
+-- case on nested case expression
+case4 (n : Nat) : Nat :=
+  case n of {
+    | zero := case n of {x := zero}
+    | _ := zero
+  };
+
+-- -- case with application subject
+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,14 +4,13 @@ import Nat open;
 
 type Unit := unit : Unit;
 
-f : Nat :=
-  case unit
-    | is-zero := zero;
+f : Nat := case unit of {is-zero := zero};
 
 f2 : Nat :=
-  case suc zero
+  case suc zero of {
     | suc is-zero := zero
-    | _ := zero;
+    | _ := zero
+  };
 
 f3 : Nat → Nat
   | (suc is-zero) := is-zero

tests/positive/Internal/Case.juvix

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

tests/positive/Iterators.juvix

@@ -21,6 +21,7 @@ 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
+         case x of {
            | true := y
-           | false := z;
+           | false := z
+         };