From 3227bffaa6ca4a9df6fedd046b03fe792acd8808 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Fri, 6 Dec 2024 09:34:49 -0800 Subject: [PATCH] Day6 --- TODO.md | 8 ++- aoc2024/Day6.newt | 132 +++++++++++++++++++++++++++++++++++++++++ aoc2024/SortedMap.newt | 19 +++++- aoc2024/day6/eg.txt | 11 ++++ newt/Prelude.newt | 8 ++- src/Lib/Elab.idr | 1 + 6 files changed, 175 insertions(+), 4 deletions(-) create mode 100644 aoc2024/Day6.newt create mode 100644 aoc2024/day6/eg.txt diff --git a/TODO.md b/TODO.md index d44be56..09fdf46 100644 --- a/TODO.md +++ b/TODO.md @@ -1,10 +1,14 @@ ## TODO +- [ ] SortedMap.newt issue in `where` - [x] fix "insufficient patterns", wire in M or Either String +- [ ] Matching _,_ when Maybe is expected should be an error +- [ ] error for repeated names on LHS - [ ] typeclass dependencies - - need to flag internal functions to not search (or flag functions for search) - - don't search instances that are currently being defined + - need to flag internal functions to not search (or flag functions for search). I need to decide on syntax for this. + - don't search functions that are currently being defined. This is subtle... We do want to recurse in bind, we don't want to do that for the isEq function. Maybe something idris like. +- [ ] default implementations (use them if nothing is defined, where do we store them?) e.g. Ord compare, <, etc in Idris - [ ] syntax for negative integers - [x] Put worker in iframe on safari - [ ] Warnings or errors for missing definitions diff --git a/aoc2024/Day6.newt b/aoc2024/Day6.newt new file mode 100644 index 0000000..c0bbd38 --- /dev/null +++ b/aoc2024/Day6.newt @@ -0,0 +1,132 @@ +module Day6 + +import Prelude +import Node +import Aoc +import SortedMap + +Point : U +Point = Int × Int + +instance Eq Point where + (a,b) == (c,d) = a == c && b == d + +instance Ord Point where + (a,b) < (c,d) = a < c || a == c && b < d + +Grid : U +Grid = SortedMap Point Char + +loadData : String → Grid +loadData text = go (unpack text) 0 0 EmptyMap + where + go : List Char → Int → Int → SortedMap Point Char → SortedMap Point Char + go Nil r c map = map + go ('\n' :: cs) r c map = go cs (r + 1) 0 map + go (x :: xs) r c map = go xs r (c + 1) $ updateMap (r,c) x map + +data Dir : U where North East South West : Dir + +instance Show Dir where + show North = "N" + show East = "E" + show South = "S" + show West = "W" + +instance Ord Dir where + a < b = show a < show b + +instance Eq (Point × Dir) where + (a,b) == (c,d) = a == c && show b == show d + +instance Ord (Point × Dir) where + (a,b) < (c,d) = + if a < c then True + else if a /= c then False + else b < d + +Done : U +Done = SortedMap (Point × Dir) Unit + +turn : Dir → Dir +turn North = East +turn East = South +turn South = West +turn West = North + +instance Cast Dir Char where + cast North = '^' + cast East = '>' + cast South = 'v' + cast West = '<' + +step : Dir → Point → Point +step North (r, c) = (r - 1, c) +step East (r, c) = (r, c + 1) +step South (r, c) = (r + 1, c) +step West (r, c) = (r, c - 1) + +bad : Point → Bool +bad (x,y) = x < 0 || y < 0 + +-- third is +walk : Dir → Point → Grid → Grid +walk dir pos grid = + let grid = updateMap pos 'X' grid in + let pos' = step dir pos in + case lookupMap pos' grid of + Just (_, '#') => walk (turn dir) pos grid + Nothing => grid + _ => walk dir pos' grid + +checkLoop : Grid → Done → Dir → Point → Bool +checkLoop grid done dir pos = + let (Nothing) = lookupMap (pos,dir) done | _ => True in + let done = updateMap (pos, dir) MkUnit done + pos' = step dir pos + in case lookupMap pos' grid of + Nothing => False + Just (_, '#') => checkLoop grid done (turn dir) pos + Just _ => checkLoop grid done dir pos' + +part2 : Dir → Point → Grid → Done → List Point → List Point +part2 dir pos grid done sol = + let done = updateMap (pos, dir) MkUnit done + grid = updateMap pos 'X' grid + turnDir = turn dir + turnPos = step turnDir pos + pos' = step dir pos in + case lookupMap pos' grid of + Nothing => sol + Just (_, '#') => part2 (turn dir) pos grid done sol + Just (_, 'X') => part2 dir pos' grid done sol + Just (_, '.') => if checkLoop (updateMap pos' '#' grid) done turnDir pos + then part2 dir pos' grid done (pos' :: sol) + else part2 dir pos' grid done sol + Just x => part2 (trace ("WAT " ++ debugStr x) dir) pos' grid done sol + +lookupV : ∀ a. Char → List (a × Char) → Maybe a +lookupV _ Nil = Nothing +lookupV needle ((k,v) :: rest) = + if v == needle then Just k else lookupV needle rest + +run : String -> IO Unit +run fn = do + putStrLn fn + text <- readFile fn + let grid = loadData text + let (Just pos) = lookupV '^' (toList grid) | _ => putStrLn "no guard" + let grid' = walk North pos grid + let xs = filter (\ x => 'X' == snd x) $ toList grid' + let part1 = length xs + putStrLn $ "part1 " ++ show part1 + + let cands = part2 North pos grid EmptyMap Nil + -- debugLog $ length cands -- turns out nub isn't needed for these cases, but we'll leave it in + putStrLn $ "part2 " ++ show (length $ ordNub cands) + printLn $ length $ toList grid + +main : IO Unit +main = do + run "aoc2024/day6/eg.txt" + run "aoc2024/day6/input.txt" diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt index bf9968f..88f7abf 100644 --- a/aoc2024/SortedMap.newt +++ b/aoc2024/SortedMap.newt @@ -1,5 +1,7 @@ module SortedMap +import Prelude + data T23 : Nat -> U -> U -> U where Leaf : ∀ k v. k -> v -> T23 Z k v Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v @@ -41,7 +43,6 @@ insertT23 key value (Node3 t1 k1 t2 k2 t3) = Left t3' => Left (Node3 t1 k1 t2 k2 t3') Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c) --- There is no empty tree23? data SortedMap : U -> U -> U where EmptyMap : ∀ k v. SortedMap k v MapOf : ∀ k v h. T23 h k v -> SortedMap k v @@ -56,3 +57,19 @@ updateMap k v (MapOf map) = case insertT23 k v map of Left map' => MapOf map' Right (a, b, c) => MapOf (Node2 a b c) +-- FIXME this doesn't work in a `where` because the erased args are un-erased +toList' : ∀ k v h. T23 h k v → List (k × v) → List (k × v) +toList' (Leaf k v) acc = (k, v) :: acc +toList' (Node2 t1 k1 t2) acc = toList' t2 (toList' t1 acc) +toList' (Node3 t1 k1 t2 k2 t3) acc = toList' t3 $ toList' t2 $ toList' t1 acc + +toList : ∀ k v. SortedMap k v → List (k × v) +toList {k} {v} (MapOf smap) = reverse $ toList' smap Nil + -- FIXME erasure checking false positive - maybe because I'm not handling the top level args yet + -- where + -- foo : ∀ k v h. T23 h k v → List (k × v) → List (k × v) + -- foo (Leaf k v) acc = (k, v) :: acc + -- foo (Node2 t1 k1 t2) acc = foo t2 (foo t1 acc) + -- foo (Node3 t1 k1 t2 k2 t3) acc = foo t3 $ foo t2 $ foo t1 acc +toList _ = Nil + diff --git a/aoc2024/day6/eg.txt b/aoc2024/day6/eg.txt new file mode 100644 index 0000000..fe5e49f --- /dev/null +++ b/aoc2024/day6/eg.txt @@ -0,0 +1,11 @@ +....#..... +.........# +.......... +..#....... +.......#.. +.......... +.#..^..... +........#. +#......... +......#... + diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 95ec484..c8ddff1 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -220,6 +220,8 @@ instance Concat String where pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False` +pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? True : False` + instance Eq Int where a == b = jsEq a b @@ -357,7 +359,7 @@ instance Show Int where pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` -pfunc unpack : String -> List Char +pfunc unpack uses (Nil _::_) : String -> List Char := `(s) => { let acc = Nil(Char) for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc) @@ -376,6 +378,7 @@ pfunc pack : List Char → String := `(cs) => { pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { const go = (obj) => { + if (obj === undefined) return "_" if (obj?.tag === '_::_' || obj?.tag === 'Nil') { let stuff = listToArray(undefined,obj) return '['+(stuff.map(go).join(', '))+']' @@ -675,3 +678,6 @@ ordNub {a} {{ordA}} xs = go $ qsort _<_ xs ite : ∀ a. Bool → a → a → a ite c t e = if c then t else e + +instance Ord String where + a < b = jsLT a b diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index aeb31af..9f8f1b0 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -652,6 +652,7 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do then case y of PatVar _ _ s => pure $ Just $ c :: (xs ++ acc) PatWild _ _ => pure $ Just $ c :: (xs ++ acc) + -- FIXME why don't we hit this ('x' for Just x) PatLit fc lit => error fc "Literal \{show lit} in constructor split" PatCon _ _ str ys => if str == dcName then pure $ Just $ !(makeConstr vars ys) ++ xs ++ acc