From f4d1e863195230b61a1c2322824e27afbb506702 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 29 Dec 2025 10:24:15 -0800 Subject: [PATCH] Optional type annotation on case scrutinee --- TODO.md | 1 + src/Lib/Elab.newt | 17 ++++++++++++----- src/Lib/Parser.newt | 10 +++++----- src/Lib/Syntax.newt | 15 ++++++++------- 4 files changed, 26 insertions(+), 17 deletions(-) diff --git a/TODO.md b/TODO.md index bd7d75c..3f4b785 100644 --- a/TODO.md +++ b/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) diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 1933442..4e253e8 100644 --- a/src/Lib/Elab.newt +++ b/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 - (sc, scty) <- infer ctx rsc + (RCase fc rsc mty alts, ty) => do + (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}" diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index 1ceb773..22018bd 100644 --- a/src/Lib/Parser.newt +++ b/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 diff --git a/src/Lib/Syntax.newt b/src/Lib/Syntax.newt index 396f9c7..c351a57 100644 --- a/src/Lib/Syntax.newt +++ b/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 "}"