import action for out of scope names, start introducing error types

src/Commands.newt

@@ -63,6 +63,7 @@ data CodeAction
   = CaseSplitAction (List FileEdit)
   | AddMissingAction (List FileEdit)
   | Intro String FileEdit
+  | ImportAction String FileEdit
 
 
 applyDCon : QName × Int × Tm → List String
@@ -210,7 +211,6 @@ introActions (Just $ Unsolved fc qn ctx vty User constraints) =
       putStrLn $ showError "" err
       pure Nil
   where
-
     introDCon : QName × Int × Tm → List String
     introDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
       where
@@ -226,6 +226,26 @@ introActions (Just $ Unsolved fc qn ctx vty User constraints) =
 
 introActions _ = pure Nil
 
+errorActions : Int → Int → Error → M (List CodeAction)
+errorActions row col err = do
+  let (ENotFound fc nm) = err | _ => pure Nil
+  let (True) = posInFC row col fc | _ => pure Nil
+  top <- getTop
+  let mods = map (\e => e.name.qns) $ lookupAll nm top
+  case mods of
+    Nil => pure Nil
+    _ => do
+      top <- getTop
+      let row = getInsertRow 0 1 $ split top.currentMod.modSource "\n"
+      let fc = MkFC fc.file (MkBounds row 0 row 0)
+      pure $ map (\nm => ImportAction nm (MkEdit fc "import \{nm}\n")) mods
+  where
+    getInsertRow : Int → Int → List String → Int
+    getInsertRow row cur Nil = row
+    getInsertRow row cur (l :: ls) =
+      let row =  ite (isPrefixOf "module" l || isPrefixOf "import" l) cur row
+      in getInsertRow row (cur + 1) ls
+
 getActions : FileSource → String → Int → Int → M (List CodeAction)
 getActions repo modns row col = do
   Just mod <- switchModule repo modns | _ => pure Nil
@@ -236,7 +256,8 @@ getActions repo modns row col = do
   let hole = getHole mod row col
   putStrLn "Hole \{debugStr hole}"
   intros <- introActions $ getHole mod row col
-  pure $ actions ++ intros
+  eactions <- join <$> traverse (errorActions row col) mod.modErrors
+  pure $ actions ++ intros ++ eactions
   where
     getAction : EditorInfo → M (Maybe CodeAction)
     getAction (CaseSplit fc ctx nm scty) = getCaseSplit row col fc ctx nm scty

src/LSP.newt

@@ -13,8 +13,6 @@ import Data.SortedMap
 import Data.IORef
 import Node
 import Commands
-import Data.List1
-import Lib.Prettier
 import Lib.ProcessDecl
 
 pfunc js_castArray : Array JSObject → JSObject := `x => x`
@@ -148,6 +146,11 @@ codeActionInfo uri line col = unsafePerformIO $ do
         $ ("title", JsonStr "Intro \{name}")
         :: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil))
         :: Nil
+    actionToJson (ImportAction name edit) =
+      JsonObj
+        $ ("title", JsonStr "Import \{name}")
+        :: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil))
+        :: Nil
     actionToJson (AddMissingAction edits) =
       JsonObj
         $ ("title", JsonStr "Add missing cases")
@@ -155,11 +158,11 @@ codeActionInfo uri line col = unsafePerformIO $ do
         :: Nil
 
 errorToDiag : Error -> Json
-errorToDiag (E fc msg) =
+errorToDiag err =
   JsonObj
     $  ("severity", JsonInt 1)
-    :: ("range", fcToRange fc)
-    :: ("message", JsonStr msg)
+    :: ("range", fcToRange (getFC err))
+    :: ("message", JsonStr (errorMsg err))
     :: ("source", JsonStr "newt") -- what is this key for?
     :: Nil
 -- These shouldn't escape

src/Lib/Common.newt

@@ -142,11 +142,10 @@ emptyFC' : String → FC
 emptyFC' fn = MkFC fn (MkBounds 0 0 0 0)
 
 -- Using a String instead of List String for the module shaved about 16% of compile time...
-data QName : U where
-  QN : String -> String -> QName
-
-.baseName : QName → String
-(QN _ name).baseName = name
+record QName where
+  constructor QN
+  qns : String
+  baseName : String
 
 instance Eq QName where
   -- `if` gets us short circuit behavior, idris has a lazy `&&`
@@ -159,34 +158,39 @@ instance Show QName where
 instance Ord QName where
   compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns'
 
+-- I'll want to get Context / Val in some of these
+-- and a pretty printer in the monad
 data Error
   = E FC String
+  | ENotFound FC String
   | Postpone FC QName String
 
 instance Show FC where
   show (MkFC file (MkBounds l c el ec)) = "\{file}:\{show $ l + 1}:\{show $ c + 1}--\{show $ el + 1}:\{show $ ec + 1}"
 
-showError : String -> Error -> String
-showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src)
+instance HasFC Error where
+  getFC (E x str) = x
+  getFC (ENotFound x _) = x
+  getFC (Postpone x k str) = x
+
+errorMsg : Error -> String
+errorMsg (E x str) = str
+errorMsg (ENotFound x nm) = "\{nm} not in scope"
+errorMsg (Postpone x k str) = str
+
+showError : (src : String) -> Error -> String
+showError src err =
+  let fc = getFC err
+  in "ERROR at \{show $ getFC err}: \{errorMsg err}\n" ++ go fc 0 (lines src)
   where
-    go : Int -> List String -> String
-    go l Nil = ""
-    go l (x :: xs) =
+    go : FC → Int → List String → String
+    go fc l Nil = ""
+    go fc l (x :: xs) =
       if l == fcLine fc then
         let width = fc.bnds.endCol - fc.bnds.startCol in
         "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}\{replicate (cast width) '^'}\n"
-      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
-      else go (l + 1) xs
-showError src (Postpone fc ix msg) = "ERROR at \{show fc}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src)
-  where
-    go : Int -> List String -> String
-    go l Nil = ""
-    go l (x :: xs) =
-      if l == fcLine fc then
-        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}^\n"
-      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go (l + 1) xs
-      else go (l + 1) xs
-
+      else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go fc (l + 1) xs
+      else go fc (l + 1) xs
 
 data Fixity = InfixL | InfixR | Infix
 

src/Lib/Elab.newt

@@ -1535,9 +1535,6 @@ infer ctx tm@(RUpdateRec fc _ _) = error fc "I can't infer record updates"
 
 infer ctx (RVar fc nm) = go 0 ctx.types
   where
-    entryNS : TopEntry → String
-    entryNS (MkEntry fc (QN ns _) _ _ _) = ns
-
     go : Int -> List (String × Val)  -> M (Tm × Val)
     go i Nil = do
       top <- getTop
@@ -1546,13 +1543,8 @@ infer ctx (RVar fc nm) = go 0 ctx.types
           debug $ \ _ => "lookup \{show name} as \{show def}"
           vty <- eval Nil ty
           pure (Ref fc name, vty)
-        Nothing => do
-          let mods = map entryNS $ lookupAll nm top
-          let extra = case mods of
-            Nil => ""
-            -- For the benefit of the editor, but only sees transitive modules
-            _ => ", try importing: \{joinBy ", " mods}"
-          error fc "\{show nm} not in scope\{extra}"
+        -- Can we soften this without introducing a meta?
+        Nothing => throwError $ ENotFound fc nm
     go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty)
       else go (i + 1) xs
 

src/Lib/Types.newt

@@ -570,13 +570,6 @@ debugM x = logM 2 x
 instance Show Context where
   show ctx = "Context \{show $ map fst $ ctx.types}"
 
-errorMsg : Error -> String
-errorMsg (E x str) = str
-errorMsg (Postpone x k str) = str
-
-instance HasFC Error where
-  getFC (E x str) = x
-  getFC (Postpone x k str) = x
 
 error : ∀ a. FC -> String -> M a
 error fc msg = throwError $ E fc msg