From e39651489951ffe1aba0c944d3031dd6735bfd7d Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 21 Dec 2024 14:29:46 -0800 Subject: [PATCH] day21 --- TODO.md | 3 + aoc2024/Day21.newt | 143 ++++++++++++++++++++++ aoc2024/day21/eg.txt | 5 + newt-vscode/.eslintrc.json | 4 +- newt-vscode/src/extension.ts | 38 +++--- newt-vscode/syntaxes/newt.tmLanguage.json | 2 +- playground/samples/aoc2024/Day21.newt | 1 + playground/samples/aoc2024/day21 | 1 + playground/src/monarch.ts | 1 + 9 files changed, 176 insertions(+), 22 deletions(-) create mode 100644 aoc2024/Day21.newt create mode 100644 aoc2024/day21/eg.txt create mode 120000 playground/samples/aoc2024/Day21.newt create mode 120000 playground/samples/aoc2024/day21 diff --git a/TODO.md b/TODO.md index d9edfc5..6e0f470 100644 --- a/TODO.md +++ b/TODO.md @@ -6,6 +6,8 @@ More comments in code! This is getting big enough that I need to re-find my bear - [ ] editor - idnent newline on let with no in - [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 - [ ] 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 @@ -14,6 +16,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] Matching _,_ when Maybe is expected should be an error - [ ] There are issues with matching inside do blocks, I think we need to guess scrutinee? I could imagine constraining metas too (e.g. if Just ... at ?m123 then ?m123 =?= Maybe ?m456) - Also, the root cause is tough to track down if there is a type error (this happens with `do` in Idris, too). + - Part of it is the auto solutions are getting discarded because of an unrelated unification failure. Either auto shouldn't go as deep or should run earlier. Forgetting that lookupMap returns a (k,v) pair is a good example. - [ ] error for non-linear pattern - [ ] typeclass dependencies - need to flag internal functions to not search (or flag functions for search). I need to decide on syntax for this. diff --git a/aoc2024/Day21.newt b/aoc2024/Day21.newt new file mode 100644 index 0000000..1a8b335 --- /dev/null +++ b/aoc2024/Day21.newt @@ -0,0 +1,143 @@ +module Day21 + +import Prelude +import Node +import Aoc +import SortedMap +import Parser + +min : Int → Int → Int +min a b = if a < b then a else b + +gridPoints : String → List (Char × Int × Int) +gridPoints text = go 0 0 (unpack text) Nil + where + -- might as well be tail recursive + go : Int → Int → List Char → List (Char × Int × Int) → List (Char × Int × Int) + go row col Nil points = points + go row col ('\n' :: cs) points = go (row + 1) 0 cs points + go row col (c :: cs) points = go row (col + 1) cs ((c,row,col) :: points) + +data Dir : U where North East South West : Dir + +dirs : List Dir +dirs = (North :: South :: East :: West :: Nil) + +move : Point → Dir → Point +move (r, c) North = (r - 1, c) +move (r, c) East = (r, c + 1) +move (r, c) South = (r + 1, c) +move (r, c) West = (r, c - 1) + +Costs : U +Costs = SortedMap (Point × Point) Int + +-- linked list of keypads +record Keypad where + constructor KP + name : String + start : Point + interdit : Point + costs : Costs -- cache of costs + next : Maybe Keypad + +getPaths : Point → Point → Point → List (List Dir) +getPaths interdit pt@(a,b) to@(c,d) = + if pt == to then Nil :: Nil else + if pt == interdit then Nil else + join $ map check dirs + where + check : Dir → List (List Dir) + check North = if c < a then map (_::_ North) $ getPaths interdit (move pt North) (c,d) else Nil + check South = if a < c then map (_::_ South) $ getPaths interdit (move pt South) (c,d) else Nil + check East = if b < d then map (_::_ East) $ getPaths interdit (move pt East) (c,d) else Nil + check West = if d < b then map (_::_ West) $ getPaths interdit (move pt West) (c,d) else Nil + +updateCost : Point × Point → Int → Keypad → Keypad +updateCost path cost (KP n s i c nxt) = (KP n s i (updateMap path cost c) nxt) + +keyPos : Dir → Point +keyPos North = (0,1) +keyPos South = (1,1) +keyPos East = (1,2) +keyPos West = (1,0) + +-- cost to run a path in a keypad +pathCost : Point → Point → Keypad → Keypad × Int + +-- cost of sequence of points (run in parent keypad) +-- for numpad, we pick points from the map, for the rest map keyPos ... +seqCost : Point → List Point → Keypad × Int → Keypad × Int +seqCost cur Nil (kp, cost) = (kp, cost) +seqCost cur (pt :: pts) (kp, cost) = + let (kp, cost') = pathCost cur pt kp in + let x = cost' in + seqCost pt pts (kp, cost + cost') + +-- cost of best path from -> to in kp +pathCost from to kp = do + case lookupMap (from, to) (costs kp) of + Just (_, cost) => (kp, cost) + Nothing => + let (path :: paths) = getPaths (interdit kp) from to | _ => ? in + case kp of + (KP n s i c Nothing) => (kp, 1) + (KP n s i c (Just kp')) => + let (kp', cost) = mincost path paths kp' in + let kp = KP n s i c (Just kp') in + (updateCost (from,to) cost kp, cost) + where + xlate : List Dir → Point -> List Point + xlate Nil a = a :: Nil + xlate (d :: ds) a = keyPos d :: xlate ds a + + mincost : List Dir → List (List Dir) → Keypad → Keypad × Int + mincost path paths kp = + let (kp', cost) = seqCost (0,2) (xlate path $ start kp) (kp, 0) in + case paths of + Nil => (kp', cost) + (path :: paths) => let (kp', cost') = mincost path paths kp' in (kp', min cost cost') + +fromList : ∀ k v. {{Ord k}} {{Eq k}} → List (k × v) → SortedMap k v +fromList xs = foldMap (\ a b => b) EmptyMap xs + +getNum : String → Int +getNum str = case number (unpack str) of + Right (n, _) => n + _ => 0 + +runOne : Keypad → SortedMap Char Point → String → Int × Int +runOne kp numpad str = + let pts = map snd $ mapMaybe (flip lookupMap numpad) $ unpack str in + let res = seqCost (3,2) pts (kp, 0) in + (getNum str, snd res) + +makeKeypad : Int → Keypad -> Keypad +makeKeypad 0 kp = kp +makeKeypad n kp = makeKeypad (n - 1) $ KP (show n) (0,2) (0,0) EmptyMap (Just kp) + +run : String -> IO Unit +run fn = do + putStrLn fn + text <- readFile fn + let codes = split (trim text) "\n" + + -- the space is illegal spot + let numpad = fromList $ filter (not ∘ _==_ ' ' ∘ fst) $ gridPoints "789\n456\n123\n 0A" + + let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing + let robn = makeKeypad 2 rob1 + let kp = KP "kp" (3,2) (3,0) EmptyMap (Just robn) + let p1 = foldl _+_ 0 $ map (uncurry _*_ ∘ runOne kp numpad) codes + putStrLn $ "part1 " ++ show p1 + + let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing + let robn = makeKeypad 25 rob1 + let kp = KP "kp" (3,2) (3,0) EmptyMap (Just robn) + let p2 = foldl _+_ 0 $ map (uncurry _*_ ∘ runOne kp numpad) codes + putStrLn $ "part2 " ++ show p2 + +main : IO Unit +main = do + run "aoc2024/day21/eg.txt" + run "aoc2024/day21/input.txt" diff --git a/aoc2024/day21/eg.txt b/aoc2024/day21/eg.txt new file mode 100644 index 0000000..4cf0c29 --- /dev/null +++ b/aoc2024/day21/eg.txt @@ -0,0 +1,5 @@ +029A +980A +179A +456A +379A diff --git a/newt-vscode/.eslintrc.json b/newt-vscode/.eslintrc.json index 86c86f3..d327f1b 100644 --- a/newt-vscode/.eslintrc.json +++ b/newt-vscode/.eslintrc.json @@ -17,7 +17,7 @@ } ], "@typescript-eslint/semi": "warn", - "curly": "warn", + "curly": ["warn", "multi"], "eqeqeq": "warn", "no-throw-literal": "warn", "semi": "off" @@ -27,4 +27,4 @@ "dist", "**/*.d.ts" ] -} \ No newline at end of file +} diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index d06b55c..0e1d6dd 100644 --- a/newt-vscode/src/extension.ts +++ b/newt-vscode/src/extension.ts @@ -37,9 +37,9 @@ export function activate(context: vscode.ExtensionContext) { { cwd, maxBuffer: 1024 * 1024 * 10 }, (err, stdout, _stderr) => { // I think I ignored 1 here because I wanted failure to launch - if (err && err.code !== 1) { + if (err && err.code !== 1) vscode.window.showErrorMessage(`newt error: ${err}`); - } + // extract errors and messages from stdout const lines = stdout.split("\n"); @@ -79,9 +79,9 @@ export function activate(context: vscode.ExtensionContext) { let lnum = Number(line); let cnum = Number(column); - if (file !== fileName) { + 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); @@ -92,17 +92,17 @@ export function activate(context: vscode.ExtensionContext) { // anything indented // Context:, or Goal: are part of PRINTME // unexpected / expecting appear in parse errors - while (lines[i + 1]?.match(/^( )/)) { + while (lines[i + 1]?.match(/^( )/)) message += "\n" + lines[++i]; - } + const severity = kind === "ERROR" ? vscode.DiagnosticSeverity.Error : vscode.DiagnosticSeverity.Information; const diag = new vscode.Diagnostic(range, message, severity); - if (kind === "ERROR" || lnum > 0) { + if (kind === "ERROR" || lnum > 0) diagnostics.push(diag); - } + } } diagnosticCollection.set(vscode.Uri.file(fileName), diagnostics); @@ -116,9 +116,9 @@ export function activate(context: vscode.ExtensionContext) { const editor = vscode.window.activeTextEditor; if (editor) { const document = editor.document; - if (document.fileName.endsWith(".newt")) { + if (document.fileName.endsWith(".newt")) checkDocument(document); - } + } } ); @@ -164,25 +164,25 @@ export function activate(context: vscode.ExtensionContext) { } } ) - ) + ); context.subscriptions.push(runPiForall); vscode.workspace.onDidSaveTextDocument((document) => { - if (document.fileName.endsWith(".newt")) { + if (document.fileName.endsWith(".newt")) vscode.commands.executeCommand("newt-vscode.check"); - } + }); vscode.workspace.onDidOpenTextDocument((document) => { - if (document.fileName.endsWith(".newt")) { + if (document.fileName.endsWith(".newt")) vscode.commands.executeCommand("newt-vscode.check"); - } + }); - for (let document of vscode.workspace.textDocuments) { - if (document.fileName.endsWith(".newt")) { + for (let document of vscode.workspace.textDocuments) + if (document.fileName.endsWith(".newt")) checkDocument(document); - } - } + + context.subscriptions.push(diagnosticCollection); } diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index f0d17ee..d662f61 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/newt-vscode/syntaxes/newt.tmLanguage.json @@ -16,7 +16,7 @@ }, { "name": "keyword.newt", - "match": "\\b(λ|=>|<-|->|→|:=|\\$|data|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" + "match": "\\b(λ|=>|<-|->|→|:=|\\$|data|record|where|do|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b" }, { "name": "string.js", diff --git a/playground/samples/aoc2024/Day21.newt b/playground/samples/aoc2024/Day21.newt new file mode 120000 index 0000000..ead4a42 --- /dev/null +++ b/playground/samples/aoc2024/Day21.newt @@ -0,0 +1 @@ +../../../aoc2024/Day21.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/day21 b/playground/samples/aoc2024/day21 new file mode 120000 index 0000000..0693fca --- /dev/null +++ b/playground/samples/aoc2024/day21 @@ -0,0 +1 @@ +../../../aoc2024/day21 \ No newline at end of file diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts index e5ece23..9f27735 100644 --- a/playground/src/monarch.ts +++ b/playground/src/monarch.ts @@ -68,6 +68,7 @@ export let newtTokens: monaco.languages.IMonarchLanguage = { "in", "where", "case", + "record", "of", "data", "forall",