diff --git a/TODO.md b/TODO.md index db61130..f7f7bbe 100644 --- a/TODO.md +++ b/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 diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index a740318..e442686 100644 --- a/newt-vscode/src/extension.ts +++ b/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; } diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index cb4eb9c..6490a05 100644 --- a/src/Lib/Elab.newt +++ b/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 diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt index 79df380..af02699 100644 --- a/src/Lib/TopContext.newt +++ b/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 = diff --git a/src/Main.newt b/src/Main.newt index a6527fc..116f3fb 100644 --- a/src/Main.newt +++ b/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