From 3cc3801f4ddac8e735f79e70f03d0314eb2f80b4 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 23 Feb 2026 13:16:06 -0800 Subject: [PATCH] Add "intro" to LSP, improve error locations --- src/Commands.newt | 57 ++++++++++++++++++++++++++++++++++++++++++--- src/LSP.newt | 5 ++++ src/Lib/Elab.newt | 17 +++++++------- src/Lib/Parser.newt | 21 ++++++++++------- 4 files changed, 79 insertions(+), 21 deletions(-) diff --git a/src/Commands.newt b/src/Commands.newt index cc3dd78..97e38d5 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -61,6 +61,7 @@ data FileEdit = MkEdit FC String data CodeAction = CaseSplitAction (List FileEdit) | AddMissingAction (List FileEdit) + | Intro String FileEdit applyDCon : QName × Int × Tm → List String @@ -163,13 +164,63 @@ posInFC : Int → Int → FC → Bool -- FIXME ec + 1 again... posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (sc <= col && col <= ec + 1) +getHole : ModContext → Int → Int → Maybe MetaEntry +getHole mod row col = + find isUserMeta $ listValues mod.modMetaCtx.metas + where + isUserMeta : MetaEntry → Bool + isUserMeta (Unsolved fc _ _ _ User _) = posInFC row col fc + isUserMeta _ = False + +introActions : Maybe MetaEntry → M (List CodeAction) +introActions (Just $ Unsolved fc qn ctx vty User constraints) = + catchError (do + -- Are there ever any constraints? + top <- getTop + vty <- forceMeta vty + putStrLn "intros for \{show vty}" + case vty of + VPi _ nm Explicit _ a b => do + let str = "(\\ \{nm} => ?)" + pure $ Intro str (MkEdit fc str) :: Nil + _ => do + -- Prelude.Nat not a vref? + -- also need to handle pi types + cons <- getConstructors ctx fc vty + putStrLn "constructors \{show cons}" + pure $ map makeEdit cons + ) $ \ err => do + putStrLn "Got error in introActions:" + putStrLn $ showError "" err + pure Nil + where + + introDCon : QName × Int × Tm → List String + introDCon (QN _ nm, _, tm) = go (Lin :< nm) tm + where + go : SnocList String → Tm → List String + go acc (Pi _ nm Explicit _ _ u) = go (acc :< "?") u + go acc (Pi _ _ _ _ _ u) = go acc u + go acc _ = acc <>> Nil + + makeEdit : (QName × Int × Tm) → CodeAction + makeEdit con@(QN _ nm, _, _) = + let str = unwords $ resugarOper $ introDCon con + in Intro str $ MkEdit fc $ str + +introActions _ = pure Nil + getActions : FileSource → String → Int → Int → M (List CodeAction) getActions repo modns row col = do mod <- switchModule repo modns top <- getTop - let xx = filter (posInFC row col ∘ getFC) top.currentMod.modInfos - putStrLn "Filter got \{show $ length' xx}" - go Nil $ xx + let infos = filter (posInFC row col ∘ getFC) top.currentMod.modInfos + putStrLn "Filter got \{show $ length' infos}" + actions <- go Nil $ infos + let hole = getHole mod row col + putStrLn "Hole \{debugStr hole}" + intros <- introActions $ getHole mod row col + pure $ actions ++ intros where getAction : EditorInfo → M (Maybe CodeAction) getAction (CaseSplit fc ctx nm scty) = getCaseSplit row col fc ctx nm scty diff --git a/src/LSP.newt b/src/LSP.newt index dc0d0c7..b1263d8 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -143,6 +143,11 @@ codeActionInfo uri line col = unsafePerformIO $ do $ ("title", JsonStr "Case split") :: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits)) :: Nil + actionToJson (Intro name edit) = + JsonObj + $ ("title", JsonStr "Intro \{name}") + :: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil)) + :: Nil actionToJson (AddMissingAction edits) = JsonObj $ ("title", JsonStr "Add missing cases") diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 5a9b844..cdeaef3 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -999,13 +999,12 @@ mkPat (tm, icit) = do pure $ PatCon (getFC tm) icit name bpat Nothing -- This fires when a global is shadowed by a pattern var -- Just _ => error (getFC tm) "\{show nm} is not a data constructor" - _ => case b of - -- TODO maybe check case? - Nil => - if isUpperName nm + _ => if isUpperName nm + -- This is not entirely accurate - it could be a function def then error (getFC tm) "\{nm} not in scope" - else pure $ PatVar fc icit nm - _ => error (getFC tm) "patvar applied to args" + else case b of + Nil => pure $ PatVar fc icit nm + _ => error (getFC tm) "patvar applied to args" ((RImplicit fc), Nil) => pure $ PatWild fc icit ((RImplicit fc), _) => error fc "implicit pat can't be applied to arguments" ((RLit fc lit), Nil) => pure $ PatLit fc lit @@ -1486,9 +1485,10 @@ check ctx tm ty = do pure $ Lam fc nm' icit rig sc else error fc "Icity issue checking \{show t} at \{show ty}" - (t@(RLam _ (BI fc nm icit quant) tm), ty) => do + (t@(RLam fc (BI _ nm icit quant) tm), ty) => do pty <- prvalCtx ty - error fc "Expected \{pty}, got pi type" + -- TODO I'm hitting this with an unsolved meta + error fc "Expected \{pty}, got a function" (RLet fc nm ty v sc, rty) => do ty' <- check ctx ty (VU emptyFC) @@ -1513,7 +1513,6 @@ check ctx tm ty = do pure $ Lam (getFC tm) nm' Implicit rig sc (tm, ty@(VPi fc nm' Auto rig a b)) => do - let names = map fst ctx.types debug $ \ _ => "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} " let var = VVar fc (length' ctx.env) Lin ty' <- b $$ var diff --git a/src/Lib/Parser.newt b/src/Lib/Parser.newt index a211f1e..2769192 100644 --- a/src/Lib/Parser.newt +++ b/src/Lib/Parser.newt @@ -311,14 +311,16 @@ pLamArg = impArg <|> autoArg <|> expArg lamExpr : Parser Raw lamExpr = do pos <- getPos - keyword "\\" <|> keyword "λ" - args <- some $ addPos pLamArg - keyword "=>" - scope <- typeExpr - pure $ foldr mkLam scope args + (fc, args, scope) <- withFC $ do + keyword "\\" <|> keyword "λ" + args <- some $ addPos pLamArg + keyword "=>" + scope <- typeExpr + pure (args, scope) + pure $ foldr (mkLam fc) scope args where - mkLam : FC × Icit × Name × Maybe Raw → Raw → Raw - mkLam (fc, icit, name, ty) sc = RLam fc (BI fc name icit Many) sc + mkLam : FC → FC × Icit × Name × Maybe Raw → Raw → Raw + mkLam fc (nfc, icit, name, ty) sc = RLam fc (BI nfc name icit Many) sc caseAlt : Parser RCaseAlt @@ -566,10 +568,11 @@ parseDef = do nm <- getName t Just _ <- optional $ keyword "=" -- impossible clause + -- TODO we should require outdent | Nothing => pure $ FunDef fc nm ((t,Nothing) :: Nil) + -- TODO could we recover and keep the LHS? body <- typeExpr - wfc <- getPos - w <- optional $ do + (wfc, w) <- withFC $ optional $ do keyword "where" startBlock $ manySame $ (parseSig <|> parseDef) let body = maybe body (\ decls => RWhere wfc decls body) w