From 69a7b6bed8f4c98aa7d8309c72a2415ef246c60a Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 23 Feb 2026 20:48:25 -0800 Subject: [PATCH] Fix LSP slowness, improve error messages --- src/Commands.newt | 31 ++++++++++++++++++------------- src/LSP.newt | 3 ++- src/Lib/Elab.newt | 6 +++--- src/Lib/Eval.newt | 18 ++++-------------- tests/aside/InferIssue.newt | 11 +++++++++++ 5 files changed, 38 insertions(+), 31 deletions(-) create mode 100644 tests/aside/InferIssue.newt diff --git a/src/Commands.newt b/src/Commands.newt index 97e38d5..e32f5de 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -26,17 +26,18 @@ decomposeName fn = else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc) -switchModule : FileSource → String → M ModContext +switchModule : FileSource → String → M (Maybe ModContext) switchModule repo modns = do - mod <- processModule emptyFC repo Nil modns + top <- getTop + let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing modifyTop [ currentMod := mod; ops := mod.modOps ] - pure mod + pure $ Just mod -- The cheap version of type at point, find the token, lookup in global context -- Later we will either get good FC for entries or scan them all and build a cache. getHoverInfo : FileSource → String → Int → Int → M (Maybe (String × FC)) getHoverInfo repo modns row col = do - mod <- switchModule repo modns + Just mod <- switchModule repo modns | _ => pure Nothing top <- getTop -- Find the token at the point @@ -72,12 +73,15 @@ applyDCon (QN _ nm, _, tm) = go (Lin :< nm) tm go acc (Pi _ _ _ _ _ u) = go acc u go acc _ = acc <>> Nil +data Flavor = EqSplit | FatArrowSplit | MonadSplit + -- Not quite right, we also need to check for let... -- But it's a first pass -splitEquals : SnocList Char → List Char → (Bool × String × String) -splitEquals acc Nil = (True, pack (acc <>> Nil), "") -splitEquals acc xs@('=' :: _) = (True, pack (acc <>> Nil), pack xs) -splitEquals acc xs@('<' :: '-' :: _) = (False, pack (acc <>> Nil), pack xs) +splitEquals : SnocList Char → List Char → (Flavor × String × String) +splitEquals acc Nil = (EqSplit, pack (acc <>> Nil), "") +splitEquals acc xs@('=' :: '>' :: _) = (FatArrowSplit, pack (acc <>> Nil), pack xs) +splitEquals acc xs@('=' :: _) = (EqSplit, pack (acc <>> Nil), pack xs) +splitEquals acc xs@('<' :: '-' :: _) = (MonadSplit, pack (acc <>> Nil), pack xs) splitEquals acc (x :: xs) = splitEquals (acc :< x) xs needParens : SnocList Char → List Char → Bool @@ -115,7 +119,7 @@ makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do let cs = unpack line let head = take (cast sc) cs let tail = drop (S $ cast (ec - 1)) cs - let (isEq, before, after) = splitEquals Lin tail + let (splitKind, before, after) = splitEquals Lin tail let np = needParens (Lin <>< head) tail let cons = map (addParens np ∘ resugarOper) cons let phead = pack head @@ -126,9 +130,10 @@ makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do let phead = pack head let fc' = MkFC uri (MkBounds (sr + 1) 0 (sr + 1) 0) let srest = - if isEq - then joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest - else joinBy "" $ map (\ap => " | \{pack head}\{ap}\{before}=> ?\n") rest + case splitKind of + EqSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest + FatArrowSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "=> ?\n") rest + MonadSplit => joinBy "" $ map (\ap => " | \{pack head}\{ap}\{before}=> ?\n") rest putStrLn "Split \{show line} HD '\{show head}' TL '\{show tail}'" putStrLn srest @@ -212,7 +217,7 @@ introActions _ = pure Nil getActions : FileSource → String → Int → Int → M (List CodeAction) getActions repo modns row col = do - mod <- switchModule repo modns + Just mod <- switchModule repo modns | _ => pure Nil top <- getTop let infos = filter (posInFC row col ∘ getFC) top.currentMod.modInfos putStrLn "Filter got \{show $ length' infos}" diff --git a/src/LSP.newt b/src/LSP.newt index b1263d8..88a7ef8 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -199,7 +199,8 @@ checkFile fn = unsafePerformIO $ do else pure MkUnit (Right (top, json)) <- (do putStrLn "processModule" - _ <- switchModule lspFileSource modName + mod <- processModule emptyFC lspFileSource Nil modName + modifyTop [ currentMod := mod; ops := mod.modOps ] -- pull out errors and infos top <- getTop diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index cdeaef3..fcd2279 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -1503,7 +1503,7 @@ check ctx tm ty = do (tm, ty@(VPi fc nm' Implicit rig a b)) => do let names = map fst ctx.types - debug $ \ _ => "XXX edge case add implicit lambda {\{nm'} : \{show a}} to \{show tm} " + debug $ \ _ => "elab.insert: Add implicit lambda {\{nm'} : \{show a}} to \{show tm} " let var = VVar fc (length' ctx.env) Lin ty' <- b $$ var debugM $ do @@ -1513,12 +1513,12 @@ check ctx tm ty = do pure $ Lam (getFC tm) nm' Implicit rig sc (tm, ty@(VPi fc nm' Auto rig a b)) => do - debug $ \ _ => "XXX edge case add auto lambda {\{nm'} : \{show a}} to \{show tm} " + debug $ \ _ => "elab.insert: Add auto lambda {\{nm'} : \{show a}} to \{show tm}" let var = VVar fc (length' ctx.env) Lin ty' <- b $$ var debugM $ do pty' <- prvalCtx {{(extend ctx nm' a)}} ty' - pure "XXX ty' is \{pty'}" + pure "elab.insert: ty' is \{pty'}" sc <- check (extend ctx nm' a) tm ty' pure $ Lam (getFC tm) nm' Auto rig sc diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt index 9e9b009..f15360e 100644 --- a/src/Lib/Eval.newt +++ b/src/Lib/Eval.newt @@ -268,28 +268,18 @@ prvalCtx {{ctx}} v = do tm <- quote ctx.lvl v pure $ render 90 $ pprint (map fst ctx.types) tm --- REVIEW - might be easier if we inserted the meta without a bunch of explicit App --- I believe Kovacs is doing that. --- we need to walk the whole thing --- meta in Tm have a bunch of args, which should be the relevant --- parts of the scope. So, meta has a bunch of lambdas, we've got a bunch of --- args and we need to beta reduce, which seems like a lot of work for nothing --- Could we put the "good bits" of the Meta in there and write it to Bnd directly --- off of scope? I guess this might get dicey when a meta is another meta applied --- to something. +-- 'zonk' is substituting metas _and_ doing inlining --- ok, so we're doing something that looks lot like eval, having to collect args, --- pull the def, and apply spine. Eval is trying for WHNF, so it doesn't walk the --- whole thing. (We'd like to insert metas inside lambdas.) +-- It is a flavor of eval, maybe we could combine them with some flags +-- to control what gets reduced. zonk : TopContext -> Int -> Env -> Tm -> M Tm zonkBind : TopContext -> Int -> Env -> Tm -> M Tm zonkBind top l env tm = zonk top (1 + l) (VVar (getFC tm) l Lin :: env) tm --- I don't know if app needs an FC... - +-- REVIEW FC might be dicey here appSpine : Tm -> List Tm -> Tm appSpine t Nil = t appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs diff --git a/tests/aside/InferIssue.newt b/tests/aside/InferIssue.newt new file mode 100644 index 0000000..3d39251 --- /dev/null +++ b/tests/aside/InferIssue.newt @@ -0,0 +1,11 @@ +module InferIssue + +-- inline prelude to reduce log size +infixr 8 _×_ +infixr 2 _,_ +data a × b = (a,b) +data Nat = Z | S Nat + +-- unification error because meta isn't solved yet +foo : Nat → (Nat × (Nat → Nat)) +foo x = (Z , (\ x => 10))