diff --git a/src/Commands.newt b/src/Commands.newt index a9ff0f1..4527a7b 100644 --- a/src/Commands.newt +++ b/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 diff --git a/src/LSP.newt b/src/LSP.newt index 88a7ef8..985db83 100644 --- a/src/LSP.newt +++ b/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 diff --git a/src/Lib/Common.newt b/src/Lib/Common.newt index 2ae3f0f..6940598 100644 --- a/src/Lib/Common.newt +++ b/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 diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index fcd2279..8e689d9 100644 --- a/src/Lib/Elab.newt +++ b/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 diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index edb4eeb..dd427a4 100644 --- a/src/Lib/Types.newt +++ b/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