From f9f29cd932ff68f7b7306bff9ada87b0e953e60c Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Mon, 9 Dec 2024 22:43:26 -0800
Subject: [PATCH] Day10

---
 TODO.md               |   1 +
 aoc2024/Day10.newt    | 108 ++++++++++++++++++++++++++++++++++++++++++
 aoc2024/day10/eg.txt  |   4 ++
 aoc2024/day10/eg2.txt |   7 +++
 aoc2024/day10/eg3.txt |   7 +++
 aoc2024/day10/eg4.txt |   7 +++
 aoc2024/day10/eg5.txt |   8 ++++
 src/Lib/Elab.idr      |   9 ++--
 8 files changed, 148 insertions(+), 3 deletions(-)
 create mode 100644 aoc2024/Day10.newt
 create mode 100644 aoc2024/day10/eg.txt
 create mode 100644 aoc2024/day10/eg2.txt
 create mode 100644 aoc2024/day10/eg3.txt
 create mode 100644 aoc2024/day10/eg4.txt
 create mode 100644 aoc2024/day10/eg5.txt

diff --git a/TODO.md b/TODO.md
index 3989919..1765518 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,7 @@
 
 ## TODO
 
+- [ ] keymap for monaco
 - [x] SortedMap.newt issue in `where`
 - [x] fix "insufficient patterns", wire in M or Either String
 - [x] Matching _,_ when Maybe is expected should be an error
diff --git a/aoc2024/Day10.newt b/aoc2024/Day10.newt
new file mode 100644
index 0000000..beaa279
--- /dev/null
+++ b/aoc2024/Day10.newt
@@ -0,0 +1,108 @@
+module Day10
+
+import Prelude
+import Node
+import Aoc
+import SortedMap
+
+-- move to lib
+
+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)
+
+Point : U
+Point = Int × Int
+
+instance Add Point where
+  (a,b) + (c,d) = (a + c, b + d)
+
+instance Sub Point where
+  (a,b) - (c,d) = (a - c, b - d)
+
+instance Ord Point where
+  (a,b) < (c,d) = a < c || a == c && b < d
+
+instance Eq Point where
+  (a,b) == (c,d) = a == c && b == d
+
+swap : ∀ a b. a × b → b × a
+swap (a,b) = (b,a)
+
+const : ∀ a b. a → b → a
+const a b = a
+
+-- TODO add parameter a and pass Char -> a into getGrid
+Grid : U
+Grid = SortedMap Point Int
+
+digitToInt : Char → Int
+digitToInt c = ord c - 48
+
+getGrid : String → Grid
+
+getGrid text = foldl update EmptyMap $ gridPoints text
+  where
+    update : Grid → Char × Point → Grid
+    update grid (c,pt) = updateMap pt (digitToInt c) grid
+
+peers : Point → List Point
+peers pt = map (_+_ pt) ((0, 0 - 1) :: (0,1) :: (0 - 1,0) :: (1,0) :: Nil)
+
+
+paths : Grid → List Point → Int → Int
+paths grid pts ht =
+  if ht == 9 then cast $ length pts else
+  -- Maybe I should nub with a sortedMap
+  let cands = ordNub $ map fst $ filter (_==_ (ht + 1) ∘ snd) $ join $ map getCands pts
+  in paths grid cands (ht + 1)
+  where
+    getCands : Point → List (Point × Int)
+    getCands pt = mapMaybe (\ p => lookupMap p grid) (peers pt)
+
+foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b
+foldMap f m Nil = m
+foldMap f m ((a,b) :: xs) = case lookupMap a m of
+  Nothing => foldMap f (updateMap a b m) xs
+  Just (_, b') => foldMap f (updateMap a (f b' b) m) xs
+
+paths2 : Grid → List (Point × Int) → Int → Int
+paths2 grid pts ht =
+  if ht == 9 then foldl _+_ 0 $ map snd $ pts else
+  let cands = join $ map getCands pts
+      pts' = toList $ foldMap _+_ EmptyMap cands
+  in paths2 grid pts' (ht + 1)
+  where
+    getCands : Point × Int → List (Point × Int)
+    getCands (pt,cnt) =
+      map (\ x => fst x , cnt)
+        $ filter (_==_ (ht + 1) ∘ snd)
+        $ mapMaybe (\ p => lookupMap p grid) (peers pt)
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let grid = getGrid text
+  let starts = filter (_==_ 0 ∘ snd) $ toList grid
+  let all = map (\ pt => paths grid (fst pt :: Nil) 0) starts
+  let part1 = foldl _+_ 0 all
+  putStrLn $ "part1 " ++ show part1
+
+  let all = map (\ pt => paths2 grid ((fst pt, 1) :: Nil) 0) starts
+  let part2 = foldl _+_ 0 all
+  putStrLn $ "part2 " ++ show part2
+
+main : IO Unit
+main = do
+  run "aoc2024/day10/eg.txt"
+  run "aoc2024/day10/eg2.txt"
+  run "aoc2024/day10/eg3.txt"
+  run "aoc2024/day10/eg4.txt"
+  run "aoc2024/day10/eg5.txt"
+  run "aoc2024/day10/input.txt"
diff --git a/aoc2024/day10/eg.txt b/aoc2024/day10/eg.txt
new file mode 100644
index 0000000..a305b9d
--- /dev/null
+++ b/aoc2024/day10/eg.txt
@@ -0,0 +1,4 @@
+0123
+1234
+8765
+9876
diff --git a/aoc2024/day10/eg2.txt b/aoc2024/day10/eg2.txt
new file mode 100644
index 0000000..db56de0
--- /dev/null
+++ b/aoc2024/day10/eg2.txt
@@ -0,0 +1,7 @@
+...0...
+...1...
+...2...
+6543456
+7.....7
+8.....8
+9.....9
diff --git a/aoc2024/day10/eg3.txt b/aoc2024/day10/eg3.txt
new file mode 100644
index 0000000..17655af
--- /dev/null
+++ b/aoc2024/day10/eg3.txt
@@ -0,0 +1,7 @@
+..90..9
+...1.98
+...2..7
+6543456
+765.987
+876....
+987....
diff --git a/aoc2024/day10/eg4.txt b/aoc2024/day10/eg4.txt
new file mode 100644
index 0000000..185787f
--- /dev/null
+++ b/aoc2024/day10/eg4.txt
@@ -0,0 +1,7 @@
+10..9..
+2...8..
+3...7..
+4567654
+...8..3
+...9..2
+.....01
diff --git a/aoc2024/day10/eg5.txt b/aoc2024/day10/eg5.txt
new file mode 100644
index 0000000..cada9b3
--- /dev/null
+++ b/aoc2024/day10/eg5.txt
@@ -0,0 +1,8 @@
+89010123
+78121874
+87430965
+96549874
+45678903
+32019012
+01329801
+10456732
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 2093470..92fef37 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -121,7 +121,7 @@ addConstraint env ix sp tm = do
     (Unsolved pos k a b c cons) => do
       debug "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
       pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons))
-    (Solved _ k tm) => error' "Meta \{show k} already solved"
+    (Solved _ k tm) => error' "Meta \{show k} already solved [addConstraint]"
   pure ()
 
 
@@ -201,7 +201,7 @@ export
 solve : Env -> (k : Nat) -> SnocList Val -> Val -> M  ()
 solve env m sp t = do
   meta@(Unsolved metaFC ix ctx_ ty kind cons) <- lookupMeta m
-    | _ => error (getFC t) "Meta \{show m} already solved!"
+    | _ => error (getFC t) "Meta \{show m} already solved! [solve]"
   debug "SOLVE \{show m} \{show kind} lvl \{show $ length env} sp \{show sp} is \{show t}"
   let size = length $ filter (\x => x == Bound) $ toList ctx_.bds
   debug "\{show m} size is \{show size} sps \{show $ length sp}"
@@ -226,7 +226,7 @@ solve env m sp t = do
 
     updateMeta m $ \case
       (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln
-      (Solved _ k x) => error' "Meta \{show ix} already solved!"
+      (Solved _ k x) => error' "Meta \{show ix} already solved! [solve2]"
     for_ cons $ \case
       MkMc fc env sp rhs => do
         val <- vappSpine soln sp
@@ -238,6 +238,9 @@ solve env m sp t = do
         debug "CONSTRAINT2 m\{show ix} \{show sp} =?= \{show t}"
         addConstraint env m sp t
       err => do
+        -- I get legit errors after stuffing in solution
+        -- report for now, tests aren't hitting this branch
+        throwError err
         debug "CONSTRAINT3 m\{show ix} \{show sp} =?= \{show t}"
         debug "because \{showError "" err}"
         addConstraint env m sp t)