Add "intro" to LSP, improve error locations

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

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

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

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