From 370fc8e0aa527dfa78d9b5e7657591a2d1dd13e5 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Wed, 27 Nov 2024 09:57:22 -0800 Subject: [PATCH] Add filenames to FC, relocate errors from other files in playground/vscode --- TODO.md | 2 +- newt-vscode/src/extension.ts | 10 +++++-- playground/src/main.ts | 12 ++++++-- src/Lib/Common.idr | 38 +++++++++++++++++-------- src/Lib/Parser/Impl.idr | 55 +++++++++++++++++++----------------- src/Lib/ProcessDecl.idr | 6 ++-- src/Lib/Tokenizer.idr | 6 ++-- src/Lib/Types.idr | 2 +- src/Main.idr | 12 ++++---- 9 files changed, 86 insertions(+), 57 deletions(-) diff --git a/TODO.md b/TODO.md index 900704b..99e350f 100644 --- a/TODO.md +++ b/TODO.md @@ -1,7 +1,7 @@ ## TODO -- [ ] add filenames to FC +- [x] add filenames to FC - [x] maybe use backtick for javascript so we don't highlight strings as JS - [ ] add namespaces - [x] dead code elimination diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 450d8ba..4037f91 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -36,11 +36,15 @@ export function activate(context: vscode.ExtensionContext) { for (let i = 0; i < lines.length; i++) { const line = lines[i]; - const match = line.match(/(INFO|ERROR) at \((\d+), (\d+)\):\s*(.*)/); + const match = line.match(/(INFO|ERROR) at (.*):\((\d+), (\d+)\):\s*(.*)/); if (match) { - let [_full, kind, line, column, message] = match; + let [_full, kind, file, line, column, message] = match; + // FIXME - check filename against current + console.log('********', file, fileName); + let lnum = Number(line); let cnum = Number(column); + if (file !== fileName) { lnum = cnum = 0; } let start = new vscode.Position(lnum, cnum); // we don't have the full range, so grab the surrounding word let end = new vscode.Position(lnum, cnum+1); @@ -58,7 +62,7 @@ export function activate(context: vscode.ExtensionContext) { } const severity = kind === 'ERROR' ? vscode.DiagnosticSeverity.Error : vscode.DiagnosticSeverity.Information; const diag = new vscode.Diagnostic(range, message, severity); - diagnostics.push(diag); + if (kind === 'ERROR' || lnum > 0) { diagnostics.push(diag); } } } diagnosticCollection.set(vscode.Uri.file(fileName), diagnostics); diff --git a/playground/src/main.ts b/playground/src/main.ts index d76dcc0..527a048 100644 --- a/playground/src/main.ts +++ b/playground/src/main.ts @@ -292,13 +292,19 @@ const processOutput = ( let model = editor.getModel()!; let markers: monaco.editor.IMarkerData[] = []; let lines = output.split("\n"); + let m = lines[0].match(/.*Process (.*)/) + let fn = '' + if (m) fn = m[1] for (let i = 0; i < lines.length; i++) { const line = lines[i]; - const match = line.match(/(INFO|ERROR) at \((\d+), (\d+)\):\s*(.*)/); + const match = line.match(/(INFO|ERROR) at (.*):\((\d+), (\d+)\):\s*(.*)/); if (match) { - let [_full, kind, line, col, message] = match; + let [_full, kind, file, line, col, message] = match; let lineNumber = +line + 1; let column = +col + 1; + if (fn && file !== fn) { + lineNumber = column = 0 + } let start = { column, lineNumber }; // we don't have the full range, so grab the surrounding word let endColumn = column + 1; @@ -316,7 +322,7 @@ const processOutput = ( kind === "ERROR" ? monaco.MarkerSeverity.Error : monaco.MarkerSeverity.Info; - + if (kind === 'ERROR' || lineNumber) markers.push({ severity, message, diff --git a/src/Lib/Common.idr b/src/Lib/Common.idr index 02b8082..da9121c 100644 --- a/src/Lib/Common.idr +++ b/src/Lib/Common.idr @@ -3,10 +3,20 @@ module Lib.Common import Data.String import public Data.SortedMap --- I was going to use a record, but we're peeling this off of bounds at the moment. + public export -FC : Type -FC = (Int,Int) +record FC where + constructor MkFC + file : String + start : (Int,Int) + +export +(.line) : FC -> Int +fc.line = fst fc.start + +export +(.col) : FC -> Int +fc.col = snd fc.start public export interface HasFC a where @@ -16,7 +26,7 @@ interface HasFC a where export emptyFC : FC -emptyFC = (0,0) +emptyFC = MkFC "" (0,0) -- Error of a parse public export @@ -25,25 +35,29 @@ data Error | Postpone FC Nat String %name Error err +export +Show FC where + show fc = "\{fc.file}:\{show fc.start}" + public export showError : String -> Error -> String -showError src (E (line, col) msg) = "ERROR at \{show (line,col)}: \{msg}\n" ++ go 0 (lines src) +showError src (E fc msg) = "ERROR at \{show fc}: \{msg}\n" ++ go 0 (lines src) where go : Int -> List String -> String go l [] = "" go l (x :: xs) = - if l == line then - " \{x}\n \{replicate (cast col) ' '}^\n" - else if line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs + if l == fc.line then + " \{x}\n \{replicate (cast fc.col) ' '}^\n" + else if fc.line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs else go (l + 1) xs -showError src (Postpone (line, col) ix msg) = "ERROR at \{show (line,col)}: Postpone \{show ix} \{msg}\n" ++ go 0 (lines src) +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 [] = "" go l (x :: xs) = - if l == line then - " \{x}\n \{replicate (cast col) ' '}^\n" - else if line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs + if l == fc.line then + " \{x}\n \{replicate (cast fc.col) ' '}^\n" + else if fc.line - 3 < l then " " ++ x ++ "\n" ++ go (l + 1) xs else go (l + 1) xs public export diff --git a/src/Lib/Parser/Impl.idr b/src/Lib/Parser/Impl.idr index 63dc0bd..db58b87 100644 --- a/src/Lib/Parser/Impl.idr +++ b/src/Lib/Parser/Impl.idr @@ -41,21 +41,22 @@ export runP : Parser a -> TokenList -> Bool -> Operators -> FC -> Result a runP (P f) = f -error : TokenList -> String -> Error -error [] msg = E emptyFC msg -error ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (line, col) msg +-- FIXME no filename, also half the time it is pointing at the token after the error +error : String -> TokenList -> String -> Error +error fn [] msg = E (MkFC fn (0,0)) msg +error fn ((MkBounded val isIrrelevant (MkBounds line col _ _)) :: _) msg = E (MkFC fn (line,col)) msg export -parse : Parser a -> TokenList -> Either Error a -parse pa toks = case runP pa toks False empty (-1,-1) of +parse : String -> Parser a -> TokenList -> Either Error a +parse fn pa toks = case runP pa toks False empty (MkFC fn (-1,-1)) of Fail fatal err toks com ops => Left err OK a [] _ _ => Right a - OK a ts _ _ => Left (error ts "Extra toks") + OK a ts _ _ => Left (error fn ts "Extra toks") ||| Intended for parsing a top level declaration export -partialParse : Parser a -> Operators -> TokenList -> Either Error (a, Operators, TokenList) -partialParse pa ops toks = case runP pa toks False ops (0,0) of +partialParse : String -> Parser a -> Operators -> TokenList -> Either Error (a, Operators, TokenList) +partialParse fn pa ops toks = case runP pa toks False ops (MkFC fn (0,0)) of Fail fatal err toks com ops => Left err OK a ts _ ops => Right (a,ops,ts) @@ -69,11 +70,11 @@ try (P pa) = P $ \toks,com,ops,col => case pa toks com ops col of export fail : String -> Parser a -fail msg = P $ \toks,com,ops,col => Fail False (error toks msg) toks com ops +fail msg = P $ \toks,com,ops,col => Fail False (error col.file toks msg) toks com ops export fatal : String -> Parser a -fatal msg = P $ \toks,com,ops,col => Fail True (error toks msg) toks com ops +fatal msg = P $ \toks,com,ops,col => Fail True (error col.file toks msg) toks com ops export getOps : Parser (Operators) @@ -125,8 +126,8 @@ Monad Parser where pred : (BTok -> Bool) -> String -> Parser String pred f msg = P $ \toks,com,ops,col => case toks of - (t :: ts) => if f t then OK (value t) ts True ops else Fail False (error toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops - [] => Fail False (error toks "\{msg} at EOF") toks com ops + (t :: ts) => if f t then OK (value t) ts True ops else Fail False (error col.file toks "\{msg} at \{show $ kind t}:\{value t}") toks com ops + [] => Fail False (error col.file toks "\{msg} at EOF") toks com ops export commit : Parser () @@ -141,31 +142,33 @@ mutual export getPos : Parser FC -getPos = P $ \toks,com, ops, (l,c) => case toks of +getPos = P $ \toks, com, ops, indent => case toks of [] => OK emptyFC toks com ops - (t :: ts) => OK (start t) toks com ops + (t :: ts) => OK (MkFC indent.file (start t)) toks com ops ||| Start an indented block and run parser in it export startBlock : Parser a -> Parser a -startBlock (P p) = P $ \toks,com,ops,(l,c) => case toks of - [] => p toks com ops (l,c) +startBlock (P p) = P $ \toks,com,ops,indent => case toks of + [] => p toks com ops indent (t :: _) => -- If next token is at or before the current level, we've got an empty block let (tl,tc) = start t - in p toks com ops (tl,ifThenElse (tc <= c) (c + 1) tc) + (MkFC file (line,col)) = indent + in p toks com ops (MkFC file (tl, ifThenElse (tc <= col) (col + 1) tc)) ||| Assert that parser starts at our current column by ||| checking column and then updating line to match the current export sameLevel : Parser a -> Parser a -sameLevel (P p) = P $ \toks,com,ops,(l,c) => case toks of - [] => p toks com ops (l,c) +sameLevel (P p) = P $ \toks,com,ops,indent => case toks of + [] => p toks com ops indent (t :: _) => let (tl,tc) = start t - in if tc == c then p toks com ops (tl, c) - else if c < tc then Fail False (error toks "unexpected indent") toks com ops - else Fail False (error toks "unexpected indent") toks com ops + (MkFC file (line,col)) = indent + in if tc == col then p toks com ops ({start := (tl, col)} indent) + else if col < tc then Fail False (error file toks "unexpected indent") toks com ops + else Fail False (error file toks "unexpected indent") toks com ops export someSame : Parser a -> Parser (List a) @@ -178,12 +181,12 @@ manySame pa = many $ sameLevel pa ||| check indent on next token and run parser export indented : Parser a -> Parser a -indented (P p) = P $ \toks,com,ops,(l,c) => case toks of - [] => p toks com ops (l,c) +indented (P p) = P $ \toks,com,ops,indent => case toks of + [] => p toks com ops indent (t::_) => let (tl,tc) = start t - in if tc > c || tl == l then p toks com ops (l,c) - else Fail False (error toks "unexpected outdent") toks com ops + in if tc > indent.col || tl == indent.line then p toks com ops indent + else Fail False (error indent.file toks "unexpected outdent") toks com ops ||| expect token of given kind export diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index dab1dc8..a0c5891 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -143,7 +143,7 @@ logMetas mstart = do env <- dumpEnv ctx let msg = "\{env} -----------\n \{pprint names ty'}" info fc "User Hole\n\{msg}" - (Unsolved (l,c) k ctx ty kind cons) => do + (Unsolved fc k ctx ty kind cons) => do tm <- quote ctx.lvl !(forceMeta ty) -- Now that we're collecting errors, maybe we simply check at the end -- TODO - log constraints? @@ -151,7 +151,7 @@ logMetas mstart = do let msg = "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints" msgs <- for cons $ \ (MkMc fc env sp val) => do pure " * (m\{show k} (\{unwords $ map show $ sp <>> []}) =?= \{show val}" - addError $ E (l,c) $ unlines ([msg] ++ msgs) + addError $ E fc $ unlines ([msg] ++ msgs) export @@ -409,7 +409,7 @@ processDecl (Data fc nm ty cons) = do for_ names $ \ nm' => do setDef nm' fc dty (DCon (getArity dty) nm) pure names - _ => throwError $ E (0,0) "expected constructor declaration" + decl => throwError $ E (getFC decl) "expected constructor declaration" putStrLn "setDef \{nm} TCon \{show $ join cnames}" updateDef nm fc tyty (TCon (join cnames)) -- logMetas mstart diff --git a/src/Lib/Tokenizer.idr b/src/Lib/Tokenizer.idr index bc692bb..1c27908 100644 --- a/src/Lib/Tokenizer.idr +++ b/src/Lib/Tokenizer.idr @@ -90,8 +90,8 @@ notSpace (MkBounded (Tok Space _) _ _) = False notSpace _ = True export -tokenise : String -> Either Error (List BTok) -tokenise s = case lex rawTokens s of +tokenise : String -> String -> Either Error (List BTok) +tokenise fn s = case lex rawTokens s of (toks, EndInput, l, c, what) => Right (filter notSpace toks) - (toks, reason, l, c, what) => Left (E (l,c) "\{show reason}") + (toks, reason, l, c, what) => Left (E (MkFC fn (l,c)) "\{show reason}") diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index e58ef85..19dd91a 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -512,7 +512,7 @@ error fc msg = throwError $ E fc msg export error' : String -> M a -error' msg = throwError $ E (0,0) msg +error' msg = throwError $ E emptyFC msg export freshMeta : Context -> FC -> Val -> MetaKind -> M Tm diff --git a/src/Main.idr b/src/Main.idr index 28ff79e..a29d127 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -61,10 +61,10 @@ processModule base stk name = do let fn = if base == "" then name ++ ".newt" else base ++ "/" ++ name ++ ".newt" Right src <- readFile $ fn | Left err => fail (show err) - let Right toks = tokenise src + let Right toks = tokenise fn src | Left err => fail (showError src err) - let Right ((nameFC, modName), ops, toks) := partialParse parseModHeader top.ops toks + let Right ((nameFC, modName), ops, toks) := partialParse fn parseModHeader top.ops toks | Left err => fail (showError src err) @@ -72,7 +72,7 @@ processModule base stk name = do let True = name == modName | _ => fail "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}" - let Right (imports, ops, toks) := partialParse parseImports ops toks + let Right (imports, ops, toks) := partialParse fn parseImports ops toks | Left err => fail (showError src err) for_ imports $ \ (MkImport fc name') => do @@ -83,12 +83,14 @@ processModule base stk name = do top <- get mc <- readIORef top.metas + -- REVIEW suppressing unsolved and solved metas from previous files + -- I may want to know about (or fail early on) unsolved let mstart = length mc.metas - let Right (decls, ops, toks) := partialParse (manySame parseDecl) top.ops toks + let Right (decls, ops, toks) := partialParse fn (manySame parseDecl) top.ops toks | Left err => fail (showError src err) let [] := toks | (x :: xs) => - fail (showError src (E (startBounds x.bounds) "extra toks")) -- FIXME FC from xs + fail (showError src (E (MkFC fn (startBounds x.bounds)) "extra toks")) modify { ops := ops } putStrLn "process Decls"