Fix LSP slowness, improve error messages

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 : SnocList Char → List Char → (Flavor × String × String)
-splitEquals acc Nil = (True, pack (acc <>> Nil), "")
+splitEquals acc Nil = (EqSplit, pack (acc <>> Nil), "")
-splitEquals acc xs@('=' :: _) = (True, pack (acc <>> Nil), pack xs)
+splitEquals acc xs@('=' :: '>' :: _) = (FatArrowSplit, pack (acc <>> Nil), pack xs)
-splitEquals acc xs@('<' :: '-' :: _) = (False, 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
+    case splitKind of
-      then joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest
+      EqSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest
-      else joinBy "" $ map (\ap => "  | \{pack head}\{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}"

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

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
 

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
+-- 'zonk' is substituting metas _and_ doing inlining
--- 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.
 
--- ok, so we're doing something that looks lot like eval, having to collect args,
+-- It is a flavor of eval, maybe we could combine them with some flags
--- pull the def, and apply spine. Eval is trying for WHNF, so it doesn't walk the
+-- to control what gets reduced.
--- whole thing. (We'd like to insert metas inside lambdas.)
 
 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

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))