From 23a95f70f560f8cc352e3d8df2d8884a54faa081 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 28 Dec 2024 16:02:31 -0800 Subject: [PATCH] add `\case` sugar and editor support. fix symlink --- TODO.md | 13 ++++--- aoc2024/Day20b.newt.golden | 8 ----- aoc2024/Parser.newt | 4 +-- aoc2024/SortedMap.newt | 1 + newt-vscode/language-configuration.json | 2 +- newt-vscode/src/extension.ts | 45 +++++++++---------------- playground/src/monarch.ts | 8 +---- src/Lib/Elab.idr | 2 +- src/Lib/Parser.idr | 12 +++++-- 9 files changed, 40 insertions(+), 55 deletions(-) delete mode 100644 aoc2024/Day20b.newt.golden create mode 120000 aoc2024/SortedMap.newt diff --git a/TODO.md b/TODO.md index d18d1f5..ca1777c 100644 --- a/TODO.md +++ b/TODO.md @@ -5,14 +5,14 @@ More comments in code! This is getting big enough that I need to re-find my bear - [ ] tokenizer - [ ] string interpolation -- [ ] pattern matching lambda - - I kept wanting this in AoC and use it a lot in the newt code + - [ ] editor - indent newline on let with no in - I've seen this done in vi for Idris, but it seems non-trivial in vscode. - [x] Move on to next decl in case of error - [x] for parse error, seek to col 0 token and process next decl - [ ] record initialization sugar, e.g. `{ x := 1, y := 2 }` - [ ] record update sugar, syntax TBD + - I think I'm going to hold off on this for now as it requires the type to elaborate. This ends up at the head of an app, which typically is inferred. We'd need a special case somewhere that infers its argument instead. - [ ] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality) - [ ] Keep a `compare` function on `SortedMap` (like lean) - [x] keymap for monaco @@ -128,7 +128,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] there is some zero argument application in generated code - [x] get equality.newt to work - [x] broken again because I added J, probably need to constrain scrutinee to value -- [ ] Bad FC for missing case in where clause (probably from ctx) +- [x] Bad FC for missing case in where clause (probably from ctx) - [x] inline metas. Maybe zonk after TC/elab - [x] implicit patterns - [x] operators @@ -137,7 +137,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] matching on operators - [x] top level - [x] case statements -- [ ] Lean / Agda ⟨ ⟩ (does agda do this or just lean?) +- [ ] Lean ⟨ ⟩ anonymous constructors - [ ] Lean-like .map, etc? (resolve name in namespace of target type, etc) - [x] autos / typeclass resolution - [x] very primitive version in place, not higher order, search at end @@ -167,6 +167,11 @@ More comments in code! This is getting big enough that I need to re-find my bear - [ ] magic newtype? (drop them in codegen) - [x] vscode: syntax highlighting for String - [ ] add `pop` or variant of `pfunc` that maps to an operator, giving the js operator and precedence on RHS +- [ ] consider moving caselet, etc. desugaring out of the parser +- [ ] pattern matching lambda + - I kept wanting this in AoC and use it a lot in the newt code + - This conflicts with current code (unused?) that allows telescope information in lambdas + - For now, I'll implement `\case` ### Parsing diff --git a/aoc2024/Day20b.newt.golden b/aoc2024/Day20b.newt.golden deleted file mode 100644 index 7ceaa6f..0000000 --- a/aoc2024/Day20b.newt.golden +++ /dev/null @@ -1,8 +0,0 @@ -aoc2024/day20/eg.txt -base 84 -part1 1 -part2 285 -aoc2024/day20/input.txt -base 9440 -part1 1332 -part2 987695 diff --git a/aoc2024/Parser.newt b/aoc2024/Parser.newt index 9ea8b51..48dd81b 100644 --- a/aoc2024/Parser.newt +++ b/aoc2024/Parser.newt @@ -30,12 +30,12 @@ fail msg = \ cs => Left msg -- TODO, case builder isn't expanding Parser Unit to count lambdas eof : Parser Unit -eof = \ cs => case cs of +eof = \case Nil => Right (MkUnit, Nil) _ => Left "expected eof" satisfy : (Char → Bool) → Parser Char -satisfy pred = λ cs => case cs of +satisfy pred = \case Nil => Left "unexpected EOF" (c :: cs) => if pred c then Right (c, cs) else Left ("did not expect " ++ show c) diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt new file mode 120000 index 0000000..ef4aa42 --- /dev/null +++ b/aoc2024/SortedMap.newt @@ -0,0 +1 @@ +../newt/SortedMap.newt \ No newline at end of file diff --git a/newt-vscode/language-configuration.json b/newt-vscode/language-configuration.json index 1a5c092..5fa3abb 100644 --- a/newt-vscode/language-configuration.json +++ b/newt-vscode/language-configuration.json @@ -33,7 +33,7 @@ ], "onEnterRules": [ { - "beforeText": "\\b(where|of)$", + "beforeText": "\\b(where|of|case)$", "action": { "indent": "indent" } }, { diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 0e1d6dd..737e9fb 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -40,7 +40,6 @@ export function activate(context: vscode.ExtensionContext) { if (err && err.code !== 1) vscode.window.showErrorMessage(`newt error: ${err}`); - // extract errors and messages from stdout const lines = stdout.split("\n"); const diagnostics: vscode.Diagnostic[] = []; @@ -70,17 +69,13 @@ export function activate(context: vscode.ExtensionContext) { console.log("top data", topData); } const match = line.match( - /(INFO|ERROR) at (.*):\((\d+), (\d+)\):\s*(.*)/ + /(INFO|WARN|ERROR) at (.*):\((\d+), (\d+)\):\s*(.*)/ ); if (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; + 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 @@ -88,21 +83,17 @@ export function activate(context: vscode.ExtensionContext) { let range = document.getWordRangeAtPosition(start) ?? new vscode.Range(start, end); - // heuristics to grab the entire message: - // anything indented - // Context:, or Goal: are part of PRINTME - // unexpected / expecting appear in parse errors - while (lines[i + 1]?.match(/^( )/)) - message += "\n" + lines[++i]; + // anything indented after the ERROR/INFO line are part of + // the message + while (lines[i + 1]?.match(/^( )/)) message += "\n" + lines[++i]; - const severity = - kind === "ERROR" - ? vscode.DiagnosticSeverity.Error - : vscode.DiagnosticSeverity.Information; + let severity; + + if (kind === "ERROR") severity = vscode.DiagnosticSeverity.Error; + else if (kind === "WARN") severity = vscode.DiagnosticSeverity.Warning; + else severity = vscode.DiagnosticSeverity.Information; const diag = new vscode.Diagnostic(range, message, severity); - if (kind === "ERROR" || lnum > 0) - diagnostics.push(diag); - + if (kind === "ERROR" || lnum > 0) diagnostics.push(diag); } } diagnosticCollection.set(vscode.Uri.file(fileName), diagnostics); @@ -116,9 +107,7 @@ export function activate(context: vscode.ExtensionContext) { const editor = vscode.window.activeTextEditor; if (editor) { const document = editor.document; - if (document.fileName.endsWith(".newt")) - checkDocument(document); - + if (document.fileName.endsWith(".newt")) checkDocument(document); } } ); @@ -148,7 +137,7 @@ export function activate(context: vscode.ExtensionContext) { context.subscriptions.push( vscode.languages.registerHoverProvider( - {language: 'newt'}, + { language: "newt" }, { provideHover(document, position, token) { if (!topData) return null; @@ -161,7 +150,7 @@ export function activate(context: vscode.ExtensionContext) { return null; } return new vscode.Hover(`${entry.name} : ${entry.type}`); - } + }, } ) ); @@ -171,17 +160,13 @@ export function activate(context: vscode.ExtensionContext) { vscode.workspace.onDidSaveTextDocument((document) => { if (document.fileName.endsWith(".newt")) vscode.commands.executeCommand("newt-vscode.check"); - }); vscode.workspace.onDidOpenTextDocument((document) => { if (document.fileName.endsWith(".newt")) vscode.commands.executeCommand("newt-vscode.check"); - }); for (let document of vscode.workspace.textDocuments) - if (document.fileName.endsWith(".newt")) - checkDocument(document); - + if (document.fileName.endsWith(".newt")) checkDocument(document); context.subscriptions.push(diagnosticCollection); } diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts index ab72fd6..12b83e5 100644 --- a/playground/src/monarch.ts +++ b/playground/src/monarch.ts @@ -40,13 +40,7 @@ export let newtConfig: monaco.languages.LanguageConfiguration = { }, }, { - beforeText: /\bwhere$/, - action: { - indentAction: monaco.languages.IndentAction.Indent, - }, - }, - { - beforeText: /\bof$/, + beforeText: /\b(where|of|case)$/, action: { indentAction: monaco.languages.IndentAction.Indent, }, diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 90ecc4f..6bd86ce 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -789,7 +789,7 @@ checkWhere ctx decls body ty = do -- context could hold a Name -> Val (not Tm because levels) to help with that -- e.g. "go" -> (VApp ... (VApp (VRef "ns.go") ...) -- But I'll attempt letrec first - tm <- buildTree ctx' (MkProb clauses' vty) + tm <- buildTree ({ fc := defFC} ctx') (MkProb clauses' vty) vtm <- eval ctx'.env CBN tm -- Should we run the rest with the definition in place? -- I'm wondering if switching from bind to define will mess with metas diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 900f3cd..f19a881 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -165,7 +165,8 @@ parseOp = do pure res - +-- TODO case let? We see to only have it for `do` +-- try (keyword "let" >> sym "(") export letExpr : Parser Raw @@ -221,6 +222,13 @@ caseExpr = do alts <- startBlock $ someSame $ caseAlt pure $ RCase fc sc alts +caseLamExpr : Parser Raw +caseLamExpr = do + fc <- getPos + try ((keyword "\\" <|> keyword "λ") *> keyword "case") + alts <- startBlock $ someSame $ caseAlt + pure $ RLam fc (BI fc "$case" Explicit Many) $ RCase fc (RVar fc "$case") alts + doExpr : Parser Raw doStmt : Parser DoStmt @@ -247,7 +255,6 @@ doCaseLet = do pat <- typeExpr sym ")" keyword "=" - -- arrow <- (False <$ keyword "=" <|> True <$ keyword "<-") sc <- typeExpr alts <- startBlock $ manySame $ sym "|" *> caseAlt bodyFC <- getPos @@ -287,6 +294,7 @@ term' : Parser Raw term' = caseExpr <|> caseLet <|> letExpr + <|> caseLamExpr <|> lamExpr <|> doExpr <|> ifThenElse