From 0dfa96cb5e852f9b0988cdaac3b10455c483259a Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 29 Dec 2025 10:48:22 -0800 Subject: [PATCH] use new case syntax instead of `the` --- TODO.md | 3 +++ src/Lib/CompileExp.newt | 4 ++-- src/Lib/Elab.newt | 2 +- src/Lib/ProcessDecl.newt | 12 ++++++------ 4 files changed, 12 insertions(+), 9 deletions(-) diff --git a/TODO.md b/TODO.md index 3f4b785..9be6106 100644 --- a/TODO.md +++ b/TODO.md @@ -16,6 +16,9 @@ - [ ] add missing cases should handle `_::_` - [ ] add missing cases should share code between vscode and playground - [ ] "Not in scope" should offer to import +- [ ] Delay checking + - We have things like `foldr (\ x acc => case x : ...`, where the lambda doesn't have a good type, so we have to be explicit. If we could defer the checking of that expression until more things are solved, we might not need the annotation (e.g. checking the other arguments). Some `case` statements may have a similar situation. + - One idea is to throw the checks onto some sort of TODO list and run whatever works. (I think Idris may have a heuristic where it checks arguments backwards in some cases.) - [ ] Dependent records (I guess I missed that bit) - [ ] Arguments on records - [ ] Add sugar for type aliases (maybe infer arguments) diff --git a/src/Lib/CompileExp.newt b/src/Lib/CompileExp.newt index 5e1d100..c078e44 100644 --- a/src/Lib/CompileExp.newt +++ b/src/Lib/CompileExp.newt @@ -120,7 +120,7 @@ compileTerm t@(Ref fc nm@(QN _ tag)) = do defs <- getRef Defs case arity of Nil => - case the (Maybe Def) $ lookupMap' nm defs of + case lookupMap' nm defs : Maybe Def of Just (DCon ix EnumCon _ _) => pure $ CLit $ LInt $ cast ix Just (DCon ix FalseCon _ _) => pure $ CLit $ LBool False Just (DCon ix TrueCon _ _) => pure $ CLit $ LBool True @@ -143,7 +143,7 @@ compileTerm tm@(App _ _ _) = case funArgs tm of arity <- arityForName fc nm let (Nothing) = compilePrimOp (show nm) args' | Just cexp => pure cexp - case the (Maybe Def) $ lookupMap' nm defs of + case lookupMap' nm defs : Maybe Def of Just (DCon _ SuccCon _ _) => applySucc args' _ => apply nm args' arity -- REVIEW maybe we want a different constructor for non-Ref applications? diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 4e253e8..e2d1bb1 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1549,7 +1549,7 @@ infer ctx (RVar fc nm) = go 0 ctx.types infer ctx (RApp fc t u icit) = do -- If the app is explicit, add any necessary metas - (icit, t, tty) <- case the Icit icit of + (icit, t, tty) <- case icit of Explicit => do (t, tty) <- infer ctx t (t, tty) <- insert ctx t tty diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index ebe08b5..7fd7516 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -319,10 +319,10 @@ processInstance ns instfc ty decls = do -- declare individual functions, collect their defs defs <- for conTele $ \case (MkBinder fc nm Explicit rig ty) => do - let ty' = foldr (\ x acc => case the Binder x of (MkBinder fc nm' icit rig ty') => Pi fc nm' icit rig ty' acc) ty tele + let ty' = foldr (\ x acc => case x : Binder of (MkBinder fc nm' icit rig ty') => Pi fc nm' icit rig ty' acc) ty tele let nm' = "\{instname},\{nm}" -- we're working with a Tm, so we define directly instead of processDecl - let (Just (FunDef fc name xs)) = find (\x => case the Decl x of + let (Just (FunDef fc name xs)) = find (\x => case x : Decl of (FunDef y name xs) => name == nm _ => False) decls | _ => error instfc "no definition for \{nm}" @@ -499,9 +499,9 @@ processRecord ns recordFC nm tele cname decls = do let dcName = fromMaybe "Mk\{show nm}" cname let tcType = teleToPi tele (RU recordFC) -- REVIEW - I probably want to stick the telescope in front of the fields - let tail = foldl (\ acc bi => case the (BindInfo × Raw) bi of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele + let tail = foldl (\ acc bi => case bi : BindInfo × Raw of (BI fc nm icit _, _) => RApp fc acc (RVar fc nm) icit) (RVar recordFC nm) tele let dcType = teleToPi (impTele tele) $ - foldr (\ x acc => case the (FC × String × Raw) x of (fc, nm, ty) => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields + foldr (\ x acc => case x : FC × String × Raw of (fc, nm, ty) => RPi fc (BI fc nm Explicit Many) ty acc ) tail fields log 1 $ \ _ => "tcon type \{render 90 $ pretty tcType}" log 1 $ \ _ => "dcon type \{render 90 $ pretty dcType}" @@ -514,11 +514,11 @@ processRecord ns recordFC nm tele cname decls = do -- TODO dependency isn't handled yet -- we'll need to replace stuff like `len` with `len self`. let funType = teleToPi (impTele tele) $ RPi fc (BI fc "_" Explicit Many) tail ty - let autoPat = foldl (\acc x => case the (FC × String × Raw) x of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields + let autoPat = foldl (\acc x => case x : FC × String × Raw of (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar recordFC dcName) fields -- `.fieldName` let pname = "." ++ name - let lhs = foldl (\acc x => case the (BindInfo × Raw) x of (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc pname) tele + let lhs = foldl (\acc x => case x : BindInfo × Raw of (BI fc' nm icit quant, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc pname) tele let lhs = RApp recordFC lhs autoPat Explicit let pdecl = FunDef fc pname ((lhs, (Just $ RVar fc name)) :: Nil) log 1 $ \ _ => "\{pname} : \{render 90 $ pretty funType}"