diff --git a/README.md b/README.md index 3ca6197..f40d0a7 100644 --- a/README.md +++ b/README.md @@ -37,4 +37,3 @@ 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) diff --git a/src/Util.md b/src/Util.md index 836a4cd..92b301a 100644 --- a/src/Util.md +++ b/src/Util.md @@ -31,49 +31,6 @@ Applies a function to the contents of a `Left` if the value of the given mapLeft f (Right x) = Right x ``` -## List - - - -### contains - -Returns `True` if the list contains the given value - -```idris -export -contains : Eq a => a -> List a -> Bool -contains x [] = False -contains x (y :: xs) = - if x == y - then True - else contains x xs -``` - -### rotations - -Provides all the 'rotations' of a list. - -Example: - -``` -rotations [1, 2, 3] == [[1, 2, 3], [3, 1, 2], [2, 3, 1]] -``` - -```idris -export -rotations : List a -> List (List a) -rotations xs = rotations' (length xs) xs [] - where - rotations' : Nat -> List a -> (acc : List (List a)) -> List (List a) - rotations' 0 xs acc = acc - rotations' (S k) [] acc = acc - rotations' (S k) (x :: xs) acc = - let next = xs ++ [x] - in rotations' k next (next :: acc) -``` - ## Vectors Define some operations for pairs of numbers, treating them roughly like vectors diff --git a/src/Years/Y2015.md b/src/Years/Y2015.md index 0225c82..d3be367 100644 --- a/src/Years/Y2015.md +++ b/src/Years/Y2015.md @@ -15,7 +15,6 @@ import Years.Y2015.Day5 import Years.Y2015.Day6 import Years.Y2015.Day7 import Years.Y2015.Day8 -import Years.Y2015.Day9 --> # Days @@ -74,12 +73,6 @@ y2015 = MkYear 2015 [ , day8 ``` -## [Day 9](Y2015/Day9.md) - -```idris - , day9 -``` - ```idris ] ``` diff --git a/src/Years/Y2015/Day9.md b/src/Years/Y2015/Day9.md deleted file mode 100644 index 8abf4b2..0000000 --- a/src/Years/Y2015/Day9.md +++ /dev/null @@ -1,294 +0,0 @@ -# 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 -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) -``` - - - -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, Integer)) -> Eff fs (List Location, Integer) -shortestPath paths = do - shortest paths 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) -``` - -Calculate the longest path from a list of paths by recursively comparing -lengths. - -```idris -longestPath : Has (Reader DistanceMap) fs => Has (Except String) fs => - (paths : List (List Location, Integer)) -> Eff fs (List Location, Integer) -longestPath paths = do - longest paths Nothing - where - longest : List (a, Integer) -> (acc : Maybe (a, Integer)) - -> Eff fs (a, Integer) - longest [] acc = note "No paths" acc - longest (x :: xs) acc = - case acc of - Nothing => longest xs (Just x) - Just y => - if (snd x) > (snd y) - then longest xs (Just x) - else longest 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, (DistanceMap, List (List Location, 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" - distances <- traverse pathLen paths - let pairs = zip paths distances - (path, len) <- shortestPath pairs - info "Shortest Path: \{show path} \{show len}" - pure (len, (distance_map, pairs)) -``` - -### Part 2 - -Feed the locations back into a longest path function - -```idris -part2 : (DistanceMap, List (List Location, Integer)) - -> Eff (PartEff String) Integer -part2 (distance_map, pairs) = do - runReader distance_map {fs = Reader DistanceMap :: PartEff String} $ do - (path, len) <- longestPath pairs - info "Longest Path: \{show path} \{show len}" - pure len -``` - -