Optional type annotation on case scrutinee

TODO.md

@@ -1,6 +1,7 @@
 
 ## TODO
 
+- [x] add optional types to case `case xxx : Maybe Int of ...`
 - [ ] "Expected keyword" at `\ a ->` should be error at the `->`
 - [x] Show Either
 - [ ] `local` for `where`-like `let` clauses? (I want a `where` that closes over more stuff)

src/Lib/Elab.newt

@@ -1358,7 +1358,7 @@ undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
     Just _ => do
       let nm = "$sc"
       xs' <- undo fc xs
-      rest <- pure $ RCase fc (RVar fc nm) (MkAlt left (Just xs') :: Nil)
+      rest <- pure $ RCase fc (RVar fc nm) Nothing (MkAlt left (Just xs') :: Nil)
       pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
         (RLam fc (BI fc nm Explicit Many) rest) Explicit
     Nothing => do
@@ -1368,7 +1368,7 @@ undo prev ((DoArrow fc left@(RVar fc' nm) right Nil) :: xs) = do
 undo prev ((DoArrow fc left right alts) :: xs) = do
   let nm = "$sc"
   xs' <- undo fc xs
-  rest <- pure $ RCase fc (RVar fc nm) (MkAlt left (Just xs') :: alts)
+  rest <- pure $ RCase fc (RVar fc nm) Nothing (MkAlt left (Just xs') :: alts)
   pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
     (RLam fc (BI fc nm Explicit Many) rest) Explicit
 
@@ -1426,13 +1426,20 @@ check ctx tm ty = do
     (RUpdateRec fc clauses arg, ty) => updateRec ctx fc clauses arg ty
     (RWhere fc decls body, ty) => checkWhere ctx (collectDecl decls) body ty
     (RIf fc a b c, ty) =>
-      let tm' = RCase fc a ( MkAlt (RVar (getFC b) "True") (Just b) :: MkAlt (RVar (getFC c) "False") (Just c)  :: Nil) in
+      -- REVIEW maybe stuff Bool in here?
+      let tm' = RCase fc a Nothing (MkAlt (RVar (getFC b) "True") (Just b) :: MkAlt (RVar (getFC c) "False") (Just c)  :: Nil) in
       check ctx tm' ty
     (RDo fc stmts, ty) => do
       stmts' <- undo fc stmts
       check ctx stmts' ty
-    (RCase fc rsc alts, ty) => do
+    (RCase fc rsc mty alts, ty) => do
-      (sc, scty) <- infer ctx rsc
+      (sc, scty) <- case mty of
+        Nothing => infer ctx rsc
+        Just ty => do
+          scty <- check ctx ty (VU emptyFC)
+          vscty <- eval ctx.env scty
+          sc <- check ctx rsc vscty
+          pure (sc, vscty)
       scty <- forceMeta scty
       debug $ \ _ => "SCTM \{rpprint (names ctx) sc}"
       debug $ \ _ => "SCTY \{show scty}"

src/Lib/Parser.newt

@@ -273,7 +273,6 @@ letExpr = do
     letAssign = do
       fc <- getPos
       name <- ident
-      -- TODO type assertion
       ty <- optional (keyword ":" *> typeExpr)
       keyword "="
       t <- typeExpr
@@ -329,16 +328,17 @@ caseExpr = do
   fc <- getPos
   keyword "case"
   sc <- term
+  ty <- optional (keyword ":" *> typeExpr)
   keyword "of"
   alts <- startBlock $ someSame $ caseAlt
-  pure $ RCase fc sc alts
+  pure $ RCase fc sc ty alts
 
 caseLamExpr : Parser Raw
 caseLamExpr = do
   fc <- getPos
   try ((keyword "\\" <|> keyword "λ") *> keyword "case")
   alts <- startBlock $ someSame $ caseAlt
-  pure $ RLam fc (BI fc "$case" Explicit Many) $ RCase fc (RVar fc "$case") alts
+  pure $ RLam fc (BI fc "$case" Explicit Many) $ RCase fc (RVar fc "$case") Nothing alts
 
 doExpr : Parser Raw
 doStmt : Parser DoStmt
@@ -355,7 +355,7 @@ caseLet = do
   alts <- startBlock $ manySame $ symbol "|" *> caseAlt
   keyword "in"
   body <- term
-  pure $ RCase fc sc (MkAlt pat (Just body) :: alts)
+  pure $ RCase fc sc Nothing (MkAlt pat (Just body) :: alts)
 
 doCaseLet : Parser DoStmt
 doCaseLet = do
@@ -370,7 +370,7 @@ doCaseLet = do
   alts <- startBlock $ manySame $ symbol "|" *> caseAlt
   bodyFC <- getPos
   body <- RDo <$> getPos <*> someSame doStmt
-  pure $ DoExpr fc (RCase fc sc (MkAlt pat (Just body) :: alts))
+  pure $ DoExpr fc (RCase fc sc Nothing (MkAlt pat (Just body) :: alts))
 
 doArrow : Parser DoStmt
 doArrow = do

src/Lib/Syntax.newt

@@ -45,7 +45,7 @@ data Raw : U where
   RLet : (fc : FC) -> (nm : Name) -> (ty : Raw) -> (v : Raw) -> (sc : Raw) -> Raw
   RAnn : (fc : FC) -> (tm : Raw) -> (ty : Raw) -> Raw
   RLit : (fc : FC) -> Literal -> Raw
-  RCase : (fc : FC) -> (scrut : Raw) -> (alts : List RCaseAlt) -> Raw
+  RCase : (fc : FC) -> (scrut : Raw) -> (mty : Maybe Raw) -> (alts : List RCaseAlt) -> Raw
   RImplicit : (fc : FC) -> Raw
   RHole : (fc : FC) -> Raw
   RDo : (fc : FC) -> List DoStmt -> Raw
@@ -65,7 +65,7 @@ instance HasFC Raw where
   getFC (RLet fc nm ty v sc) = fc
   getFC (RAnn fc tm ty) = fc
   getFC (RLit fc y) = fc
-  getFC (RCase fc scrut alts) = fc
+  getFC (RCase fc scrut mty alts) = fc
   getFC (RImplicit fc) = fc
   getFC (RHole fc) = fc
   getFC (RDo fc stmts) = fc
@@ -171,7 +171,8 @@ instance Show Raw where
   show (RPi _ bi y z) = foo ( "Pi" :: show bi :: show y :: show z :: Nil)
   show (RApp _ x y z) = foo ( "App" :: show x :: show y :: show z :: Nil)
   show (RLam _ bi y) = foo ( "Lam" :: show bi :: show y :: Nil)
-  show (RCase _ x xs) = foo ( "Case" :: show x :: show xs :: Nil)
+  show (RCase _ x Nothing xs) = foo ( "Case" :: show x :: " of " :: show xs :: Nil)
+  show (RCase _ x (Just ty) xs) = foo ( "Case" :: show x :: " : " :: show ty :: " of " :: show xs :: Nil)
   show (RDo _ stmts) = foo ( "DO" :: "FIXME" :: Nil)
   show (RU _) = "U"
   show (RIf _ x y z) = foo ( "If" :: show x :: show y :: show z :: Nil)
@@ -224,15 +225,15 @@ instance Pretty Raw where
           <+> text "=" <+> asDoc p v
           <+/> text "in" <+> asDoc p scope
     -- does this exist?
-    asDoc p (RAnn _ x y) = text "TODO - RAnn"
+    asDoc p (RAnn _ x y) = text "TODO - Pretty RAnn"
     asDoc p (RLit _ lit) = pretty lit
-    asDoc p (RCase _ x xs) = text "TODO - RCase"
+    asDoc p (RCase _ x _ xs) = text "TODO - Pretty RCase"
     asDoc p (RImplicit _) = text "_"
     asDoc p (RImpossible _) = text "()"
     asDoc p (RHole _) = text "?"
-    asDoc p (RDo _ stmts) = text "TODO - RDo"
+    asDoc p (RDo _ stmts) = text "TODO - Pretty RDo"
     asDoc p (RIf _ x y z) = par p 0 $ text "if" <+> asDoc 0 x <+/> text "then" <+> asDoc 0 y <+/> text "else" <+> asDoc 0 z
-    asDoc p (RWhere _ dd b) = text "TODO pretty where"
+    asDoc p (RWhere _ dd b) = text "TODO pretty RWhere"
     asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")"
     asDoc p (RUpdateRec _ clauses tm) = text "{" <+> text "TODO RUpdateRec" <+> text "}"