Idris/advent
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: Idris:ed3d8a86cac30561e16c5d68f5342fc47e8e7b30
Branches Tags
Idris:trunk
Idris:develop
Idris:wat
..
compare: Idris:ca07f2995e9ee56d99a102c437f59bca5e01bed2
Branches Tags
Idris:trunk
Idris:develop
Idris:wat

No commits in common. "ed3d8a86cac30561e16c5d68f5342fc47e8e7b30" and "ca07f2995e9ee56d99a102c437f59bca5e01bed2" have entirely different histories.
ed3d8a86ca ... ca07f2995e

4 changed files with 0 additions and 345 deletions
Show stats Expand all files Collapse all files

1
README.md
View file

@ -37,4 +37,3 @@ solution.
- [Day 6](src/Years/Y2015/Day6.md) - [Day 6](src/Years/Y2015/Day6.md)
- [Day 7](src/Years/Y2015/Day7.md) - [Day 7](src/Years/Y2015/Day7.md)
- [Day 8](src/Years/Y2015/Day8.md) - [Day 8](src/Years/Y2015/Day8.md)
- [Day 9](src/Years/Y2015/Day9.md)

43
src/Util.md
View file

@ -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 mapLeft f (Right x) = Right x
``` ```
## List
<!-- idris
namespace 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 ## Vectors
Define some operations for pairs of numbers, treating them roughly like vectors Define some operations for pairs of numbers, treating them roughly like vectors

7
src/Years/Y2015.md
View file

@ -15,7 +15,6 @@ import Years.Y2015.Day5
import Years.Y2015.Day6 import Years.Y2015.Day6
import Years.Y2015.Day7 import Years.Y2015.Day7
import Years.Y2015.Day8 import Years.Y2015.Day8
import Years.Y2015.Day9
--> -->
# Days # Days
@ -74,12 +73,6 @@ y2015 = MkYear 2015 [
, day8 , day8
``` ```
## [Day 9](Y2015/Day9.md)
```idris
, day9
```
```idris ```idris
] ]
``` ```

294
src/Years/Y2015/Day9.md
View file

@ -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
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, 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
```
<!-- idris
public export
day9 : Day
day9 = Both 9 part1 part2
-->