Day 8

aoc2025/Day8.newt

@@ -0,0 +1,102 @@
+module Day8
+
+import Prelude
+import Node
+import Aoc
+import Data.SortedMap
+
+XYZ : U
+XYZ = (Int × Int × Int)
+
+-- don't need sqrt for sorting
+dist2 : XYZ → XYZ → Int
+dist2 (a,(b,c)) (d,(e,f)) = (a - d)*(a - d) + (b - e)*(b - e) + (c - f) * (c - f)
+
+parseLine : String → XYZ
+parseLine line =
+  let (x :: y :: z :: Nil) = split line "," | _ => fatalError "parseLine"
+  in (stringToInt x,(stringToInt y, stringToInt z))
+
+parse : String → List XYZ
+parse text = map parseLine $ split (trim text) "\n"
+
+-- List distances between pairs of points
+dists : List XYZ → List (Int × XYZ × XYZ)
+dists pts = go pts Nil
+  where
+    pairs : XYZ → List XYZ  → List (Int × XYZ × XYZ) → List (Int × XYZ × XYZ)
+    pairs pt Nil acc = acc
+    pairs a (b :: pts) acc = pairs a pts ((dist2 a b, a, b) :: acc)
+
+    go : List XYZ → List (Int × XYZ × XYZ) → List (Int × XYZ × XYZ)
+    go Nil acc = acc
+    go (pt :: pts) acc = go pts (pairs pt pts acc)
+
+lookup : ∀ a b. {{Eq a}} → a → List (a × b) → Maybe b
+lookup key Nil = Nothing
+lookup key ((a,b) :: rest) = if a == key then Just b else lookup key rest
+
+part1 : List XYZ → List (Int × XYZ × XYZ) → Int → Int
+part1 pts pairs count =
+  -- node -> component
+  let g = map (\ a => (a, a)) pts in
+  let node2id = merge g (cast count) pairs in
+  let id2nodes = foldl addNode emptyMap $ map swap node2id in
+  let stuff = take (cast 3) $ qsort _>_ $ map fst $ map getSize $ toList id2nodes in
+  foldl _*_ 1 stuff
+  where
+    getSize : XYZ × List XYZ → Int × XYZ
+    getSize (id,pts) = (length' pts, id)
+
+    addNode : SortedMap XYZ (List XYZ) → XYZ × XYZ → SortedMap XYZ (List XYZ)
+    addNode g (a,b) = updateMap a (b :: fromMaybe Nil (lookupMap' a g)) g
+
+    rename : XYZ → XYZ → XYZ × XYZ → XYZ × XYZ
+    rename a b (c,d) = if d == a then (c,b) else (c,d)
+
+    merge : List (XYZ × XYZ) → Nat → List (Int × XYZ × XYZ) → List (XYZ × XYZ)
+    merge g Z _ = g
+    merge g (S k) ((_, (a,b)) :: rest) =
+      let (Just a') = lookup a g | _ => fatalError "No \{show a}" in
+      let (Just b') = lookup b g | _ => fatalError "No \{show b}" in
+      if a' /= b'
+        then merge (map (rename a' b') g) k rest
+        else merge g k rest
+    merge g (S k) Nil = fatalError "too few points"
+
+part2 : List XYZ → List (Int × XYZ × XYZ) → Int
+part2 pts pairs = merge (map (\ a => (a, a)) pts) pairs
+  where
+    rename : XYZ → XYZ → XYZ × XYZ → XYZ × XYZ
+    rename a b (c,d) = if d == a then (c,b) else (c,d)
+
+    connected : List (XYZ × XYZ) → Bool
+    connected (a :: b :: rest) = if snd a == snd b then connected (a :: rest) else False
+    connected _ = True
+
+    merge : List (XYZ × XYZ) → List (Int × XYZ × XYZ) → Int
+    merge g ((_, (a,b)) :: rest) =
+      let (Just a') = lookup a g | _ => fatalError "No \{show a}" in
+      let (Just b') = lookup b g | _ => fatalError "No \{show b}" in
+      if a' == b'
+        then merge g rest
+        else let g = map (rename a' b') g in
+          if connected g
+            then fst a * fst b
+            else merge g rest
+    merge g Nil = fatalError "too few points"
+
+
+run : String -> Int → IO Unit
+run fn cnt = do
+  putStrLn fn
+  text <- readFile fn
+  let points = parse text
+  let pairs = qsort _<_ $ dists points
+  putStrLn $ "part1 " ++ show (part1 points pairs cnt)
+  putStrLn $ "part2 " ++ show (part2 points pairs)
+
+main : IO Unit
+main = do
+  run "aoc2025/day8/eg.txt" 10
+  run "aoc2025/day8/input.txt" 1000

aoc2025/day8/eg.txt

@@ -0,0 +1,20 @@
+162,817,812
+57,618,57
+906,360,560
+592,479,940
+352,342,300
+466,668,158
+542,29,236
+431,825,988
+739,650,466
+52,470,668
+216,146,977
+819,987,18
+117,168,530
+805,96,715
+346,949,466
+970,615,88
+941,993,340
+862,61,35
+984,92,344
+425,690,689

src/Prelude.newt

@@ -353,9 +353,14 @@ instance Monad IO where
 
 bindList : ∀ a b. List a → (a → List b) → List b
 
+-- Tail recursive, but may be hard to write proofs?
 instance ∀ a. Concat (List a) where
-  Nil ++ ys = ys
+  xs ++ ys = go (reverse xs) ys
-  (x :: xs) ++ ys = x :: (xs ++ ys)
+    where
+      go : ∀ a. List a → List a → List a
+      go Nil ys = ys
+      go (x :: xs) ys = go xs (x :: ys)
+
 
 instance Monad List where
   pure a = a :: Nil