Add missing import in vscode, fix add missing cases at EOF

TODO.md

@@ -35,7 +35,7 @@
   - [ ] add missing cases should skip indented lines
   - [ ] add missing cases should handle `_::_`
   - [ ] add missing cases should share code between vscode and playground
-  - [ ] "Not in scope" should offer to import
+  - [x] "Not in scope" should offer to import
   - [ ] Case split
 - [ ] Delay checking
   - We have things like `foldr (\ x acc => case x : ...`, where the lambda doesn't have a good type, so we have to be explicit. If we could defer the checking of that expression until more things are solved, we might not need the annotation (e.g. checking the other arguments). Some `case` statements may have a similar situation.
@@ -157,6 +157,7 @@
 
 
 - [ ] warn on unused imports?
+  - Probably have to mark on name lookup, maybe wait until we have query-based
 - [x] redo code to determine base path
 - [x] emit only one branch for default case when splitting inductives
 - [x] save/load results of processing a module

newt-vscode/src/extension.ts

@@ -314,11 +314,36 @@ export function activate(context: vscode.ExtensionContext) {
                 fix.edit = new vscode.WorkspaceEdit();
                 // TODO - we should skip over subsequent lines that are indented more than the current.
                 const insertPos = new vscode.Position(line + 1, 0);
-                fix.edit.insert(document.uri, insertPos, lines.join('\n') + '\n');
+                let text = lines.join('\n') + '\n';
+                if (insertPos.line === document.lineCount) {
+                  text = "\n" + text;
+                }
+                fix.edit.insert(document.uri, insertPos, text);
                 fix.diagnostics = [diagnostic];
                 fix.isPreferred = true;
                 actions.push(fix);
             }
+            m = message.match(/try importing: (.*)/);
+            if (m) {
+              let mods = m[1].split(', ')
+              let insertLine = 0;
+              for (let i = 0; i < document.lineCount; i++) {
+                const line = document.lineAt(i).text;
+                if (/^(import|module)\b/.test(line)) insertLine = i + 1;
+              }
+              const insertPos = new vscode.Position(insertLine, 0);
+              for (let mod of mods) {
+                const fix = new vscode.CodeAction(
+                  `Import ${mod}`,
+                  vscode.CodeActionKind.QuickFix
+                );
+                fix.edit = new vscode.WorkspaceEdit();
+                fix.edit.insert(document.uri, insertPos, `import ${mod}\n`);
+                fix.diagnostics = [diagnostic];
+                // fix.isPreferred = true;  // they're all preferred?
+                actions.push(fix);
+              }
+            }
           }
           return actions;
         }

src/Lib/Elab.newt

@@ -1546,6 +1546,9 @@ infer ctx tm@(RUpdateRec fc _ _) = do
 
 infer ctx (RVar fc nm) = go 0 ctx.types
   where
+    entryNS : TopEntry → String
+    entryNS (MkEntry fc (QN ns _) _ _ _) = joinBy "." ns
+
     go : Int -> List (String × Val)  -> M (Tm × Val)
     go i Nil = do
       top <- getTop
@@ -1554,7 +1557,13 @@ 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 => error fc "\{show nm} not in scope"
+        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}"
     go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty)
       else go (i + 1) xs
 

src/Lib/TopContext.newt

@@ -19,9 +19,14 @@ lookup qn@(QN ns nm) top =
       Just mod => lookupMap' qn mod.modDefs
       Nothing => Nothing
 
+lookupImported : String → TopContext -> List TopEntry
+lookupImported raw top =
+  mapMaybe (flip lookup top) $ (QN top.ns raw) :: map (flip QN raw) top.imported
+
+-- For repl / out of scope errors
 lookupAll : String → TopContext -> List TopEntry
 lookupAll raw top =
-  mapMaybe (flip lookup top) $ (QN top.ns raw) :: map (flip QN raw) top.imported
+  mapMaybe (flip lookup top) $ (QN top.ns raw) :: map (flip QN raw) (map fst $ toList top.modules)
 
 lookupRaw : String -> TopContext -> Maybe TopEntry
 lookupRaw raw top =

src/Main.newt

@@ -2,8 +2,6 @@ module Main
 
 import Prelude
 import Data.List1
-import Data.String
-import Data.IORef
 import Data.SortedMap
 import Lib.Common
 import Lib.Compile
@@ -13,7 +11,6 @@ import Lib.Util
 import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.ProcessDecl
-import Lib.Token
 import Lib.Tokenizer
 import Lib.TopContext
 import Lib.Types