diff --git a/Makefile b/Makefile index 4bebee9..bf6fa85 100644 --- a/Makefile +++ b/Makefile @@ -67,7 +67,7 @@ lsp.js: ${SRCS} newt-vscode-lsp/src/newt.js: lsp.js .PHONY echo "import fs from 'fs'\nlet mods = { fs }\nlet require = key => mods[key]\n" > $@ # HACK - perl -p -e "s/(const LSP_(?:updateFile|checkFile|hoverInfo))/export \$$1/" lsp.js >> $@ + perl -p -e "s/(const LSP_(?:updateFile|checkFile|hoverInfo|codeActionInfo))/export \$$1/" lsp.js >> $@ newt-vscode-lsp/dist/lsp.js: newt-vscode-lsp/src/lsp.ts newt-vscode-lsp/src/newt.js (cd newt-vscode-lsp && node esbuild.js) diff --git a/README.md b/README.md index 4c80e8b..65f544e 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,7 @@ The `Makefile` will build builds `./newt.js`. There is a bootstrap version of ne Newt can also be built by running `node bootstrap/newt.js src/Main.newt -o newt.js`. -The source for the vscode extension is found in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output format is in flux. +The source for the vscode extension is found in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `newt.js` to exist in the workspace. And `make test` will run a few black box tests. The tests have an expected succesful output in a `.golden` file or expected failure output in a `.fail` file. ## Playground diff --git a/newt-vscode-lsp/src/extension.ts b/newt-vscode-lsp/src/extension.ts index a95a7f7..836476a 100644 --- a/newt-vscode-lsp/src/extension.ts +++ b/newt-vscode-lsp/src/extension.ts @@ -90,86 +90,6 @@ export function activate(context: vscode.ExtensionContext) { } } }); - - // HACK Temporarily copied from non-LSP version, until code actions are implemented - context.subscriptions.push( - vscode.languages.registerCodeActionsProvider( - { language: "newt" }, - { - provideCodeActions(document, range, context, token) { - const actions: vscode.CodeAction[] = []; - for (const diagnostic of context.diagnostics) { - let {message,range} = diagnostic; - let m = message.match(/missing cases: \[(.*)\]/); - if (m) { - // A lot of this logic would also apply to case split. - let cons = m[1].split(', '); - let line = range.start.line; - let lineText = document.lineAt(line).text; - // this isn't going to work for let. - // and I think I relaxed the indent for `|` - const indent = getIndent(lineText) - let m2 = lineText.match(/(.*=>?)/); - if (!m2) continue; - let s = range.start.character; - let e = range.end.character; - let a = lineText.slice(0,s); - let b = lineText.slice(e,m2[0].length); - let parens = a.endsWith('(') && b.startsWith(')'); - let lines = cons.map(con => - !parens && con.includes('_') - ? `${a}(${con})${b} ?` - : `${a}${con}${b} ?`); - const fix = new vscode.CodeAction( - "Add missing cases", - vscode.CodeActionKind.QuickFix - ); - fix.edit = new vscode.WorkspaceEdit(); - // skip indented lines - while (1) { - line = line + 1 - lineText = document.lineAt(line).text - if (!lineText.trim() || getIndent(lineText) <= indent) break - } - const insertPos = new vscode.Position(line, 0); - 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; - } - } - ) - ); - return; - } export function deactivate() { diff --git a/newt-vscode-lsp/src/lsp.ts b/newt-vscode-lsp/src/lsp.ts index e901884..5158443 100644 --- a/newt-vscode-lsp/src/lsp.ts +++ b/newt-vscode-lsp/src/lsp.ts @@ -5,7 +5,7 @@ * vscode LSP server module. */ -import { LSP_checkFile, LSP_updateFile, LSP_hoverInfo } from './newt.js' +import { LSP_checkFile, LSP_updateFile, LSP_hoverInfo, LSP_codeActionInfo } from './newt.js' import { createConnection, @@ -105,14 +105,21 @@ connection.onDefinition((params): Location | null => { return value.location }) +connection.onCodeAction(({textDocument, range}) => { + let actions = LSP_codeActionInfo(textDocument.uri, range.start.line, range.start.character); + console.log('ACTIONS is ', JSON.stringify(actions,null,' ')) + return actions +}) + connection.onInitialize((_params: InitializeParams): InitializeResult => ({ capabilities: { textDocumentSync: TextDocumentSyncKind.Incremental, hoverProvider: true, definitionProvider: true, + codeActionProvider: true, }, })); documents.listen(connection); connection.listen(); -console.log('STARTED') \ No newline at end of file +console.log('STARTED') diff --git a/newt-vscode-lsp/src/newt.d.ts b/newt-vscode-lsp/src/newt.d.ts index 7298051..d22a4b5 100644 --- a/newt-vscode-lsp/src/newt.d.ts +++ b/newt-vscode-lsp/src/newt.d.ts @@ -1,4 +1,4 @@ -import { Diagnostic, Location } from "vscode-languageserver"; +import { CodeAction, Diagnostic, Location } from "vscode-languageserver"; export function LSP_updateFile(name: string, content: string): (eta: any) => any; export function LSP_checkFile(name: string): Diagnostic[]; @@ -7,3 +7,4 @@ interface HoverResult { location: Location } export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult|null; +export function LSP_codeActionInfo(name: string, row: number, col: number): CodeAction[]|null; diff --git a/newt-vscode/README.md b/newt-vscode/README.md index 074076c..16d45bd 100644 --- a/newt-vscode/README.md +++ b/newt-vscode/README.md @@ -1,3 +1,3 @@ # newt-vscode README -newt extension for vscode +newt extension for vscode. This is the older, non-LSP one that runs the compiler one-shot and scrapes the result. Use newt-vscode-lsp instead. diff --git a/src/Commands.newt b/src/Commands.newt index df4dfb3..c395901 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -10,6 +10,9 @@ import Data.List1 import Lib.Tokenizer import Lib.Token import Lib.Elab +import Data.String +import Lib.Eval +import Data.SortedMap -- For now we cheat and assume capitalized directories are a module component decomposeName : String → String × String @@ -31,7 +34,8 @@ getHoverInfo repo modns row col = do mod <- processModule emptyFC repo Nil modns -- not necessarily loaded into top... (Maybe push this down into that branch of processModule) - modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps ] + -- FIXME - fragile - this is why we don't want this stuff directly in TopContext + modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps; infos := mod.modInfos] top <- getTop -- Find the token at the point @@ -50,3 +54,117 @@ getHoverInfo repo modns row col = do getTok (tok :: toks) = if tok.bounds.startCol <= col && (col <= tok.bounds.endCol) then Just $ value tok else getTok toks + +data FileEdit = MkEdit FC String +data CodeAction + = CaseSplitAction (List FileEdit) + | AddMissingAction (List FileEdit) + + +applyDCon : QName × Int × Tm → List String +applyDCon (QN _ nm, _, tm) = go (Lin :< nm) tm + where + go : SnocList String → Tm → List String + go acc (Pi _ nm Explicit _ _ u) = go (acc :< nm) u + go acc (Pi _ _ _ _ _ u) = go acc u + go acc _ = acc <>> Nil + +-- Not quite right, we also need to check for let... +-- But it's a first pass +splitEquals : SnocList Char → List Char → (Bool × String × String) +splitEquals acc Nil = (True, pack (acc <>> Nil), "") +splitEquals acc xs@('=' :: _) = (True, pack (acc <>> Nil), pack xs) +splitEquals acc xs@('<' :: '-' :: _) = (False, pack (acc <>> Nil), pack xs) +splitEquals acc (x :: xs) = splitEquals (acc :< x) xs + +needParens : SnocList Char → List Char → Bool +needParens (xs :< ' ') ys = needParens xs ys +needParens xs (' ' :: ys) = needParens xs ys +needParens (xs :< '(') (')' :: ys) = False +needParens _ _ = True + +addParens : Bool → List String → String +addParens _ (x :: Nil) = x +addParens False s = unwords s +addParens True s = "(\{unwords s})" + +-- REVIEW - maybe pass in QName and use applyDCon in here, especially if we want to get better names? +makeEdits : FC → List QName → Bool → M (List FileEdit) +makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do + cons <- map applyDCon <$> traverse lookupDCon names + top <- getTop + let (Just mod) = lookupMap' top.ns top.modules | _ => pure Nil + let lines = split mod.modSource "\n" + let (Just line) = getAt' sr lines | _ => pure Nil + let cs = unpack line + let head = take (cast sc) cs + let tail = drop (S $ cast ec) cs + let (isEq, before, after) = splitEquals Lin tail + let np = needParens (Lin <>< head) tail + let cons = map (addParens np) cons + let phead = pack head + + -- No init or first :: rest for add missing case + let (edits, rest) = doFirst inPlace cons + + let phead = pack head + let fc' = MkFC uri (MkBounds (sr + 1) 0 (sr + 1) 0) + let srest = + if isEq + then joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest + else joinBy "" $ map (\ap => " | \{pack head}\{ap}\{before}=> ?\n") rest + + putStrLn "Split \{show line} HD '\{show head}' TL '\{show tail}'" + putStrLn srest + let edits = MkEdit fc' (srest) :: edits + putStrLn "edits \{debugStr edits}" + pure edits + where + doFirst : Bool → List String → (List FileEdit × List String) + doFirst True (first :: rest) = (MkEdit fc first :: Nil, rest) + doFirst _ cons = (Nil, cons) + +addMissingCases : Int → Int → FC → Context → List QName → M (Maybe CodeAction) +addMissingCases _ _ fc@(MkFC uri (MkBounds sr sc er ec)) ctx names = do + top <- getTop + edits <- makeEdits fc names False + putStrLn "Add Missing \{show fc} \{show names}" + pure $ Just $ AddMissingAction edits + +getCaseSplit : Int → Int → FC → Context → String → Val → M (Maybe CodeAction) +getCaseSplit row col fc@(MkFC uri (MkBounds sr sc er ec)) ctx nm scty = do + top <- getTop + -- It's getting vars for the type + scty <- unlet ctx.env scty + cons <- getConstructors ctx fc scty + ty <- quote (length' ctx.env) scty + cons <- filterM (checkCase ctx nm scty) cons + let names = map fst cons + edits <- makeEdits fc names True + pure $ Just $ CaseSplitAction edits + +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) + +getActions : FileSource → String → Int → Int → M (List CodeAction) +getActions repo modns row col = do + mod <- processModule emptyFC repo Nil modns + -- not necessarily loaded into top... (Maybe push this down into that branch of processModule) + modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps; infos := mod.modInfos] + top <- getTop + let xx = filter (posInFC row col ∘ getFC) top.infos + putStrLn "Filter got \{show $ length' xx}" + go Nil $ xx + where + getAction : EditorInfo → M (Maybe CodeAction) + getAction (CaseSplit fc ctx nm scty) = getCaseSplit row col fc ctx nm scty + getAction (MissingCases fc ctx names) = addMissingCases row col fc ctx names + + go : List CodeAction → List EditorInfo → M (List CodeAction) + go acc Nil = pure acc + go acc (x :: xs) = do + Right (Just res) <- tryError $ getAction x + | _ => go acc xs + go (res :: acc) xs + diff --git a/src/LSP.newt b/src/LSP.newt index a8f9526..3cf0998 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -81,9 +81,14 @@ updateFile fn src = unsafePerformIO $ do modifyIORef state [ topContext := ctx ] +-- FIXME - this is an issue - FC doesn't distinguish empty and length 1. +-- Need to put the +1 on FC itself. fcToRange : FC → Json fcToRange (MkFC uri (MkBounds sr sc er ec)) = - JsonObj $ ("start", mkPosition sr sc) :: ("end", mkPosition er (ec + 1)) :: Nil + if sc == 0 && ec == 0 + -- For the insert position in edits + then JsonObj $ ("start", mkPosition sr sc) :: ("end", mkPosition er (ec)) :: Nil + else JsonObj $ ("start", mkPosition sr sc) :: ("end", mkPosition er (ec + 1)) :: Nil where mkPosition : Int → Int → Json mkPosition l c = JsonObj $ ("line", JsonInt l) :: ("character", JsonInt c) :: Nil @@ -96,6 +101,7 @@ hoverInfo uri line col = unsafePerformIO $ do if (st.baseDir /= base) then resetState base else pure MkUnit + st <- readIORef state -- We're proactively running check if there is no module information, make sure we save it Right (top, Just (msg, fc)) <- (getHoverInfo lspFileSource modns line col).runM st.topContext | Right (top, _) => do @@ -109,6 +115,45 @@ hoverInfo uri line col = unsafePerformIO $ do let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil +codeActionInfo : String → Int → Int → JSObject +codeActionInfo uri line col = unsafePerformIO $ do + let (base,modns) = decomposeName uri + putStrLn "Action \{uri} base \{base} mod \{modns}" + st <- readIORef state + if (st.baseDir /= base) then resetState base else pure MkUnit + st <- readIORef state + Right (top, actions) <- (do + actions <- getActions lspFileSource modns line col + putStrLn "\{show $ length' actions} actions" + pure actions).runM st.topContext + | Left err => do + putStrLn $ showError "" err + pure js_null + modifyIORef state $ [ topContext := top ] + pure $ jsonToJObject $ JsonArray $ map actionToJson actions + where + single : String → Json → Json + single k v = JsonObj $ (k,v) :: Nil + + editToJson : FileEdit → Json + editToJson (MkEdit fc text) = + JsonObj + $ ("range", fcToRange fc) + :: ("newText", JsonStr text) + :: Nil + + actionToJson : CodeAction → Json + actionToJson (CaseSplitAction edits) = + JsonObj + $ ("title", JsonStr "Case split") + :: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits)) + :: Nil + actionToJson (AddMissingAction edits) = + JsonObj + $ ("title", JsonStr "Add missing cases") + :: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits)) + :: Nil + errorToDiag : Error -> Json errorToDiag (E fc msg) = JsonObj @@ -173,4 +218,5 @@ checkFile fn = unsafePerformIO $ do -- This seems like a hack, but it works. -- Dummy main function with references to force functions into ouput file. -- but we don't get `export` on it.. -pfunc main uses (updateFile checkFile hoverInfo) : IO Unit := `() => {}` +-- #export updateFile checkFile hoverInfo +pfunc main uses (updateFile checkFile hoverInfo codeActionInfo) : IO Unit := `() => {}` diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index e61f17f..55a1350 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -245,8 +245,6 @@ solveAutos = do res <- trySolveAuto e if res then pure True else run es --- We need to switch to SortedMap here - updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit updateMeta ix f = do top <- getTop @@ -713,6 +711,14 @@ findSplit (x@(PC nm (PatCon _ _ _ _ _) _) :: xs) = Just x findSplit (x@(PC nm (PatLit _ val) _) :: xs) = Just x findSplit (x :: xs) = findSplit xs +lookupDCon : QName -> M (QName × Int × Tm) +lookupDCon nm = do + top <- getTop + case lookup nm top of + (Just (MkEntry _ name type (DCon _ _ k str) _)) => pure (name, length' k, type) + Just _ => error emptyFC "Internal Error: \{show nm} is not a DCon" + Nothing => error emptyFC "Internal Error: DCon \{show nm} not found" + -- Get the constructors for a type getConstructors : Context -> FC -> Val -> M (List (QName × Int × Tm)) getConstructors ctx scfc (VRef fc nm _) = do @@ -725,13 +731,7 @@ getConstructors ctx scfc (VRef fc nm _) = do case lookup nm top of (Just (MkEntry _ name type (TCon _ names) _)) => pure names _ => error scfc "Not a type constructor: \{show nm}" - lookupDCon : QName -> M (QName × Int × Tm) - lookupDCon nm = do - top <- getTop - case lookup nm top of - (Just (MkEntry _ name type (DCon _ _ k str) _)) => pure (name, length' k, type) - Just _ => error fc "Internal Error: \{show nm} is not a DCon" - Nothing => error fc "Internal Error: DCon \{show nm} not found" + getConstructors ctx scfc tm = do tms <- vprint ctx tm error scfc "Can't split - not VRef: \{tms}" @@ -1088,9 +1088,15 @@ checkDone fc ctx Nil (Just body) ty = do got <- check ctx body ty debug $ \ _ => "DONE<- got \{rpprint (names ctx) got}" pure got -checkDone fc ctx (PC x (PatWild _ _) scty :: xs) body ty = checkDone fc ctx xs body ty -checkDone fc ctx (PC nm (PatVar _ _ nm') scty :: xs) body ty = - let ctx = MkCtx ctx.lvl ctx.env (rename ctx.types) ctx.bds ctx.ctxFC in +checkDone fc ctx (PC x (PatWild pvfc icit) scty :: xs) body ty = do + -- sometimes have the same FC as real arguments + when (icit == Explicit) $ \ _ => addInfo $ CaseSplit pvfc ctx "_" scty + checkDone fc ctx xs body ty +checkDone fc ctx (PC nm (PatVar pvfc _ nm') scty :: xs) body ty = do + -- TIME 5.50 -> 5.62 (we can flag this if it's an issue) + addInfo $ CaseSplit pvfc ctx nm' scty + + let ctx = MkCtx ctx.lvl ctx.env (rename ctx.types) ctx.bds ctx.ctxFC checkDone fc ctx xs body ty where rename : List (String × Val) -> List (String × Val) @@ -1182,26 +1188,13 @@ buildLitCase ctx prob fc scnm scty lit = do buildDefault : Context → Problem → FC → String → List QName → M CaseAlt buildDefault ctx prob fc scnm missing = do let defclauses = filter (isDefaultCase scnm) prob.clauses - -- HACK - For missing cases, we leave enough details in the error message to enable - -- the editor to add them - -- We can't do this precisely without a better pretty printer. - when (length' defclauses == 0) $ \ _ => do - missing <- traverse applied missing - error fc "missing cases: \{show missing}" - CaseDefault <$> buildTree ctx (MkProb defclauses prob.ty) - where - -- apply a dcon to _ for each explicit argument - applied : QName → M String - applied qn = do - top <- getTop - case lookup qn top of - Just (MkEntry _ _ ty (DCon _ _ _ _) _) => pure $ go qn.baseName ty - _ => pure qn.baseName - where - go : String → Tm → String - go acc (Pi _ nm Explicit _ _ t) = go "\{acc} \{nm}" t - go acc (Pi _ _ _ _ _ t) = go acc t - go acc _ = acc + case defclauses of + Nil => do + addInfo $ MissingCases fc ctx missing + addError $ E fc "missing cases: \{show missing}" + hole <- freshMeta ctx fc prob.ty ErrorHole + pure $ CaseDefault hole + _ => CaseDefault <$> buildTree ctx (MkProb defclauses prob.ty) buildLitCases : Context -> Problem -> FC -> String -> Val -> M (List CaseAlt) buildLitCases ctx prob fc scnm scty = do @@ -1543,17 +1536,7 @@ check ctx tm ty = do unifyCatch (getFC tm) ctx ty' ty pure tm' --- We assume the types are the same here, which looses some flexibility --- This does not work because the meta is unsolved when `updateRecord` tries to do --- its thing. We would need to defer elab to get this to work - insert placeholder --- and solve it later. -infer ctx tm@(RUpdateRec fc _ _) = do - error fc "I can't infer record updates" - -- mvar <- freshMeta ctx fc (VU emptyFC) Normal - -- a <- eval ctx.env mvar - -- let ty = VPi fc ":ins" Explicit Many a (MkClosure ctx.env mvar) - -- tm <- check ctx tm ty - -- pure (tm, ty) +infer ctx tm@(RUpdateRec fc _ _) = error fc "I can't infer record updates" infer ctx (RVar fc nm) = go 0 ctx.types where @@ -1601,7 +1584,7 @@ infer ctx (RApp fc t u icit) = do -- If it's not a VPi, try to unify it with a VPi -- TODO test case to cover this. tty => do - debug $ \ _ => "unify PI for \{show tty}" + debug $ \ _ => "unify PI for \{show tty} at \{show $ getFC tty}" a <- freshMeta ctx fc (VU emptyFC) Normal >>= eval ctx.env b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) fc (VU emptyFC) Normal -- FIXME - I had to guess Many here. What are the side effects? diff --git a/src/Lib/Erasure.newt b/src/Lib/Erasure.newt index b234091..d531806 100644 --- a/src/Lib/Erasure.newt +++ b/src/Lib/Erasure.newt @@ -96,7 +96,7 @@ erase env t sp = case t of (Bnd fc k) => do case getAt (cast k) env of Nothing => error fc "bad index \{show k}" - Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here - see Elab.lookupName)" + Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" Just (nm, Many, ty) => eraseSpine env t sp ty (UU fc) => eraseSpine env t sp (Just $ UU fc) (Lit fc lit) => eraseSpine env t sp Nothing diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index be32dc5..f2aa001 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -21,7 +21,7 @@ addPrimitives = do processDecl primNS (PType emptyFC "Char" Nothing) setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil top <- getTop - let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil top.errors + let mod = MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil top.errors Nil let modules = updateMap primNS mod top.modules -- TODO - do we clear this? Try just modules := modules, but wait until this refactor is done. modifyTop [ modules := modules @@ -106,11 +106,12 @@ processModule importFC repo stk modns = do top <- getTop let freshMC = MC emptyMap Nil 0 CheckAll -- NOW Print and drop errors here - -- set imported, mod, freshMC, ops before processing + -- clear per module fields before processing this module modifyTop [ imported := imported ; hints := emptyMap ; ns := modns ; defs := emptyMap + ; infos := Nil ; metaCtx := freshMC ; ops := ops ] @@ -124,7 +125,7 @@ processModule importFC repo stk modns = do -- update modules with result, leave the rest of context in case this is top file top <- getTop - let mod = MkModCtx src top.defs top.metaCtx top.ops imported top.errors + let mod = MkModCtx src top.defs top.metaCtx top.ops imported top.errors top.infos let modules = updateMap modns mod top.modules modifyTop [modules := modules] @@ -159,5 +160,4 @@ invalidateModule modname = do go deps (name :: names) = do modifyTop [modules $= deleteMap name] let ds = fromMaybe Nil $ lookupMap' name deps - putStrLn "Chase \{name} → \{show ds}" go deps $ ds ++ names diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt index 55e9ea9..358f96d 100644 --- a/src/Lib/TopContext.newt +++ b/src/Lib/TopContext.newt @@ -47,7 +47,7 @@ instance Show TopContext where show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.defs}]" emptyTop : TopContext -emptyTop = MkTop emptyMap Nil emptyMap "" emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap +emptyTop = MkTop emptyMap Nil emptyMap Nil "" emptyMap (MC emptyMap Nil 0 CheckAll) 0 Nil emptyMap setFlag : QName → FC → EFlag → M Unit @@ -94,4 +94,9 @@ addHint qn = do addError : Error -> M Unit addError err = do top <- getTop - modifyTop [ errors $= _::_ err ] + modifyTop [ errors $= (err ::) ] + +addInfo : EditorInfo → M Unit +addInfo info = do + top <- getTop + modifyTop [ infos $= (info ::)] diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 26fa98b..3e324a4 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -294,17 +294,19 @@ showClosure (MkClosure xs t) = "(%cl [\{show $ length xs} env] \{show t})" Context : U -data MetaKind = Normal | User | AutoSolve +data MetaKind = Normal | User | AutoSolve | ErrorHole instance Show MetaKind where show Normal = "Normal" show User = "User" show AutoSolve = "Auto" + show ErrorHole = "ErrorHole" instance Eq MetaKind where Normal == Normal = True User == User = True AutoSolve == AutoSolve = True + ErrorHole == ErrorHole = True _ == _ = False -- constrain meta applied to val to be a val @@ -394,6 +396,11 @@ record TopEntry where instance Show TopEntry where show (MkEntry fc name type def flags) = "\{show name} : \{show type} := \{show def} \{show flags}" +data EditorInfo + = CaseSplit FC Context String Val + -- Not sure we need Context here? + | MissingCases FC Context (List QName) + record ModContext where constructor MkModCtx modSource : String @@ -404,6 +411,7 @@ record ModContext where ctxOps : Operators modDeps : List String modErrors : List Error + modInfos : List EditorInfo -- Top level context. -- Most of the reason this is separate is to have a different type @@ -414,17 +422,25 @@ record ModContext where -- A placeholder while walking through dependencies of a module emptyModCtx : String → ModContext -emptyModCtx csum = MkModCtx csum emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil Nil +emptyModCtx source = MkModCtx source emptyMap (MC emptyMap Nil 0 NoCheck) emptyMap Nil Nil Nil HintTable : U HintTable = SortedMap QName (List (QName × Tm)) + +-- DERIVE - HasFC would be an example of a user-defined derived +instance HasFC EditorInfo where + getFC (CaseSplit fc _ _ _) = fc + getFC (MissingCases fc _ _) = fc + + record TopContext where constructor MkTop modules : SortedMap String ModContext imported : List String -- TCon name → function name × type hints : HintTable + infos : List EditorInfo -- current module ns : String