
  0 | module Days.Day10
  1 | 
  2 | import Data.String
  3 | import System
  4 | 
  5 | import Util
  6 | 
  7 | directions : LazyList (Integer, Integer)
  8 | directions =
  9 |   [ (-1, 0) -- Up
 10 |   , (1, 0)  -- Down
 11 |   , (0, -1) -- Left
 12 |   , (0, 1)  -- Right
 13 |   ]
 14 | 
 15 | record Input where
 16 |   constructor MkInput
 17 |   rows, cols : Nat
 18 |   grid : Grid rows cols Nat
 19 | %name Input input
 20 | 
 21 | Show Input where
 22 |   show (MkInput rows cols grid) =
 23 |     unlines . toList . map (joinBy "" . toList . map show) $ grid
 24 | 
 25 | parseInput : String -> Maybe Input
 26 | parseInput str = do
 27 |   (rows ** cols ** grid) <- stringTo2D str
 28 |   grid <- traverse id . map (traverse parsePositive . map singleton) $ grid
 29 |   pure $ MkInput rows cols grid
 30 | 
 31 | trailheads : (input : Input) -> LazyList (Coord input.rows input.cols)
 32 | trailheads input =
 33 |   map fst . filter ((== (the Nat 0)) . snd) . flat $ input.grid
 34 | 
 35 | accessibleEnds : (input : Input) -> (start : Coord input.rows input.cols)
 36 |                -> LazyList (Coord input.rows input.cols)
 37 | accessibleEnds input start = do
 38 |   let canidates = mapMaybe (step start) directions
 39 |   let current = start `index` input.grid
 40 |   next_pos <- canidates
 41 |   let next = next_pos `index` input.grid
 42 |   if next == current + 1
 43 |     then if next == 9
 44 |       then [next_pos]
 45 |       else accessibleEnds input next_pos
 46 |     else []
 47 | 
 48 | trailheadScore : (input : Input) -> Coord input.rows input.cols -> Nat
 49 | trailheadScore input start = length . nub . toList . accessibleEnds input $ start
 50 | 
 51 | accessibleTrails : (input : Input) -> (start : Coord input.rows input.cols)
 52 |                  -> LazyList (List (Coord input.rows input.cols))
 53 | accessibleTrails input start = do
 54 |   let canidates = mapMaybe (step start) directions
 55 |   let current = start `index` input.grid
 56 |   next_pos <- canidates
 57 |   let next = next_pos `index` input.grid
 58 |   if next == current + 1
 59 |     then if next == 9
 60 |       then [[start, next_pos]]
 61 |       else do
 62 |         rest <- accessibleTrails input next_pos
 63 |         [(start :: rest)]
 64 |     else []
 65 | 
 66 | trailheadRating : (input : Input) -> Coord input.rows input.cols -> Nat
 67 | trailheadRating input start =
 68 |   length . nub . toList . accessibleTrails input $ start
 69 | 
 70 | export
 71 | part1 : String -> IO (String, Input)
 72 | part1 str = do
 73 |   Just input <- pure $ parseInput str
 74 |     | _ => exitFailure
 75 |   let trailhead_scores = map (trailheadScore input) $ trailheads input
 76 |   pure $ (show . sum $ trailhead_scores, input)
 77 | 
 78 | export
 79 | part2 : Input -> String -> IO String
 80 | part2 input str = do
 81 |   let accessible_trails = map (trailheadRating input) $ trailheads input
 82 |   pure . show . sum  $ accessible_trails
 83 |