Year 2015 Day 9 Part 1

2025-01-17 22:20:51 -05:00 · 2025-01-17 22:20:51 -05:00 · c46d3d911b
parent 8cd56f32ab
commit c46d3d911b
3 changed files with 266 additions and 0 deletions
--- a/README.md
+++ b/README.md
@ -37,3 +37,4 @@ solution.
  - [Day 6](src/Years/Y2015/Day6.md)
  - [Day 7](src/Years/Y2015/Day7.md)
  - [Day 8](src/Years/Y2015/Day8.md)
  - [Day 9](src/Years/Y2015/Day9.md)
--- a/src/Years/Y2015.md
+++ b/src/Years/Y2015.md
@ -15,6 +15,7 @@ import Years.Y2015.Day5
 import Years.Y2015.Day6
 import Years.Y2015.Day7
 import Years.Y2015.Day8
 import Years.Y2015.Day9
 -->
 # Days
@ -73,6 +74,12 @@ y2015 = MkYear 2015 [
  , day8
 ```
 ## [Day 9](Y2015/Day9.md)
 ```idris
  , day9
 ```
 ```idris
  ]
 ```
--- a/src/Years/Y2015/Day9.md
+++ b/src/Years/Y2015/Day9.md
@ -0,0 +1,258 @@
 # Year 2016 Day 9
 This day provides our first example of a graph traversal problem. We'll use a
 `Choose` based effectful breath first search to identify all the possible paths
 meeting the problem criteria, and then figure out the length in a separate step.
 This isn't a particularly efficient solution, but its good enough for this small
 problem size.
 <!-- idris
 module Years.Y2015.Day9
 import Control.Eff
 import Runner
 -->
 ```idris
 import Data.String
 import Data.List1
 import Data.Vect
 import Data.List.Lazy
 import Data.SortedMap
 import Data.SortedSet
 import Util
 ```
 ## Parsing and data structures
 ### Parsing
 Define a location pair as a collection of two locations and a distance between
 them (as this graph is undirected), as well as some type aliases, a `contains`
 method to test if a pair covers a given location, and implement `Foldable` for
 the type to get access to the standard library utility methods.
 `DistanceMap` serves as a slightly fancy adjacency list for our graph
 representation. We'll load this into a `Reader` effect to avoid having to pass
 it around as an explicit argument to every function later on once it's been
 computed.
 ```idris
 Location : Type
 Location = String
 Distance : Type
 Distance = Integer
 record LocationPair (l : Type) where
  constructor MkLP
  locations : Vect 2 l
  distance : Integer
 %name LocationPair lp, mp, np, op
 contains : Eq l => l -> LocationPair l -> Bool
 contains x lp = 
  case find (== x) lp.locations of
    Nothing => False
    Just _ => True
 Foldable LocationPair where
  foldl f acc lp = foldl f acc lp.locations
  foldr f acc lp = foldr f acc lp.locations
  toList lp = toList lp.locations
 LP : Type
 LP = LocationPair Location
 DistanceMap : Type
 DistanceMap = SortedMap Location (List LP)
 ```
 <!-- idris
 Show l => Show (LocationPair l) where
  show (MkLP [x, y] distance) = "\{show x} <-> \{show y}: \{show distance}"
 -->
 Perform simple, pattern matching based parsing of a location pair.
 ```idris
 parseLocationPair : Has (Except String) fs =>
  String -> Eff fs LP
 parseLocationPair str = do
  from ::: ["to", to, "=", dist] <- pure $ split (== ' ') str
    | _ => throw "Badly formatted input string: \{str}"
  dist <- note "Bad distance: \{dist}" $ parsePositive dist
  pure $ MkLP [from, to] dist
 ```
 Convert a list of pairs to a `DistanceMap`, a mapping from a location to all the
 location pairs that cover it. To keep this function readable, we do this inside
 an inner function with the `State DistanceMap` effect.
 Since the inner function is recursive, instead of extracting the result after
 running the state effect, we lift it into an unconstrained `fs` so we can borrow
 the stack-saftey from our runner's top level `runEff`.
 ```idris
 pairsToMap : List LP -> Eff fs DistanceMap
 pairsToMap lps = do
  (_, out) <- lift . runState empty $ insertPairs lps
  pure out
  where
    insertLoc : LP -> (loc : Fin 2) -> Eff [State DistanceMap] ()
    insertLoc lp loc = do
      let loc = (index loc lp.locations)
      list <- map (lookup loc) get
      case list of
        Nothing => modify $ insert loc [lp]
        Just xs => modify $ insert loc (lp :: xs)
    insertPair : LP -> Eff [State DistanceMap] ()
    insertPair lp = traverse_ (insertLoc lp) (the (List _) [0, 1])
    insertPairs : List LP -> Eff [State DistanceMap] ()
    insertPairs lps = traverse_ insertPair lps
 ```
 ## Solver functions
 Generate all the possible paths originating from `current` with length `depth`,
 which is set to the number of locations in the calling function to provide the
 "visits each node once" property.
 The `path` argument accumulates the path taken by this particular branch of the
 breadth first search. It is accumulated in reverse order, but this doesn't
 really matter as this graph is undirected.
 We use the `Choose` effect to explore every possible link connecting to the
 current node, after filtering the possible links for ones that satisfy the
 problem constraints.
 ```idris
 paths : Has (Reader DistanceMap) fs => Has Choose fs => Has Logger fs =>
  (path : List Location) 
  -> (depth : Nat)
  -> (current : Location)
  -> Eff fs (List Location)
 paths path 0 current = empty
 paths path 1 current = 
  if contains current path
    then empty
    else pure $ current :: path
 paths path (S depth') current = do
  debug "Paths from \{current} at \{show (S depth')} having visited \{show path}"
  -- If we are in the path list, we have revisited this node, bail
  False <- pure $ contains current path
    | _ => empty
  -- Update our path list to contain ourself
  let path = current :: path
  -- Find our next possible steps, bailing out if there are none
  Just nexts <- map (lookup current) ask
    | _ => do empty
  -- Convert it to a list of locations
  let nexts = concat . map toList $ nexts
  -- Filter out any that are already in the path, this would be covered by the
  -- check at the start of this function, but this cleans up the logs
  let nexts = filter (not . (flip contains) path) nexts
  -- Select our next node
  next <- oneOf nexts
  paths path depth' next
 ```
 Calculate all the possible paths that satisfy the problem constraints.
 As a minor optimization, we only explore the paths leading out of a single
 arbitrary location to start with, and then take advantage of a symmetry of the
 problem, collecting all the "rotations" of each output path to cheaply calculate
 all the paths that take all the same steps as our "seed" path, but have
 different starting and ending locations.
 ```idris
 allPaths : 
  Has (Reader DistanceMap) fs => Has Logger fs => Has (Except String) fs =>
  Eff fs $ SortedSet (List Location)
 allPaths = do
  locs <- map keys ask
  first <- note "No locations" $ head' locs
  paths <- lift . runChoose {f = LazyList} $ 
    paths [] (length locs) first {fs = [Choose, Reader _, Logger]}
  pure $ buildSet paths empty
  where
    insertPaths : List (List Location) -> (acc : SortedSet (List Location)) 
      -> SortedSet (List Location)
    insertPaths [] acc = acc
    insertPaths (x :: xs) acc = insertPaths xs (insert x acc)
    buildSet : LazyList (List Location) -> (acc : SortedSet (List Location))
      -> SortedSet (List Location)
    buildSet [] acc = acc
    buildSet (x :: xs) acc = 
      let rots = rotations x
      in buildSet xs (insertPaths rots acc) 
 ```
 Calculate the length of a path by recursively destructuring the list and looking
 up each pair of locations in our `DistanceMap`.
 ```idris
 pathLen : Has (Reader DistanceMap) fs => Has (Except String) fs =>
  (path : List Location) -> Eff fs Integer
 pathLen [] = pure 0
 pathLen (x :: []) = pure 0
 pathLen (x :: (y :: xs)) = do
  lps <- map (lookup x) ask >>= note "Not found in distance map: \{x}"
  lp <- note "Pair not found \{x} \{y}" $ 
    find (\l => contains x l && contains y l) lps
  map (lp.distance +) $ pathLen (y :: xs)
 ```
 Calculate the shortest path from a list of paths by recursively comparing
 lengths.
 ```idris
 shortestPath : Has (Reader DistanceMap) fs => Has (Except String) fs =>
  (paths : List (List Location)) -> Eff fs (List Location, Integer)
 shortestPath paths = do
  lens <- traverse pathLen paths
  let pairs = zip paths lens
  shortest pairs Nothing
  where
    shortest : List (a, Integer) -> (acc : Maybe (a, Integer)) 
      -> Eff fs (a, Integer)
    shortest [] acc = note "No paths" acc
    shortest (x :: xs) acc = 
      case acc of
        Nothing => shortest xs (Just x)
        Just y => 
          if (snd x) < (snd y)
            then shortest xs (Just x)
            else shortest xs (Just y)
 ```
 ## Part Functions
 ### Part 1
 Parse our locations, turn them into a `DistanceMap`, load that into our reader,
 generate our paths, then find the one with the shortest length.
 ```idris
 part1 : Eff (PartEff String) (Integer, ())
 part1 = do
  locations <- map lines (askAt "input") >>= traverse parseLocationPair
  info "Locations: \{show locations}"
  distance_map <- pairsToMap locations
  info "Distance map: \{show distance_map}"
  runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do
  paths <- map Prelude.toList allPaths
  trace "Paths: \{show paths}"
  info "Found \{show $ length paths} paths"
  (path, len) <- shortestPath paths
  info "Shortest Path: \{show path} \{show len}"
  pure (len, ())
 ```
 <!-- idris
 public export
 day9 : Day
 day9 = First 9 part1
 -->