0 | module Days.Day16
  1 |
  2 | import Data.String
  3 | import Data.List.Lazy
  4 | import System
  5 |
  6 | import Control.Eff
  7 | import Control.Eff.Except
  8 | import Control.Eff.Choose
  9 | import Control.Eff.State
 10 |
 11 | import Derive.Prelude
 12 |
 13 | import Util
 14 | import Util.Graph
 15 |
 16 | %language ElabReflection
 17 |
 18 | data ErrorL = LParse | LSolve
 19 |
 20 | Show ErrorL where
 21 |   show LParse = "parsing"
 22 |   show LSolve = "solving"
 23 |
 24 | ParseError : Type -> Type
 25 | ParseError = ExceptL LParse String
 26 |
 27 | SolveError : Type -> Type
 28 | SolveError = ExceptL LSolve String
 29 |
 30 | data Cell = Wall | Start | End | Empty
 31 | %runElab derive "Cell" [Eq]
 32 |
 33 | charToCell : Char -> Cell
 34 | charToCell '#' = Wall
 35 | charToCell 'S' = Start
 36 | charToCell 'E' = End
 37 | charToCell _ = Empty
 38 |
 39 | record Input where
 40 |   constructor MkInput
 41 |   rows, cols : Nat
 42 |   room : Grid rows cols Cell
 43 |
 44 | parseInput : Has ParseError fs => String -> Eff fs Input
 45 | parseInput str = do
 46 |   (rows ** cols ** input) <- noteAt LParse "Error gridfying input" $
 47 |     stringTo2D str
 48 |   let room = map (map charToCell) input
 49 |   pure $ MkInput rows cols room
 50 |
 51 | startPos : (i : Input) -> Maybe (Coord i.rows i.cols)
 52 | startPos i = map fst . head' . filter ((== Start) . snd) . flat $ i.room
 53 |
 54 | endPos : (i : Input) -> Maybe (Coord i.rows i.cols)
 55 | endPos i = map fst . head' . filter ((== End) . snd) . flat $ i.room
 56 |
 57 | NodeWeight : (rows, cols : Nat) -> Type
 58 | NodeWeight rows cols = (Coord rows cols, Direction)
 59 |
 60 | EdgeWeight : Type
 61 | EdgeWeight = Integer
 62 |
 63 | GraphT : (rows, cols : Nat) -> Type
 64 | GraphT rows cols = Graph (Tpe (NodeWeight rows cols) EdgeWeight)
 65 |
 66 | inputToGraph :
 67 |   Has SolveError fs =>
 68 |   (i : Input) -> Eff fs (GraphT i.rows i.cols)
 69 | inputToGraph i = do
 70 |   start <- noteAt LSolve "No Start position" $ startPos i
 71 |   let initialState : GraphT i.rows i.cols = empty
 72 |   let (ids, graph) =
 73 |     extract . runState initialState . runChoose {f = List} $ toGraph (start, Right)
 74 |   pure graph
 75 |   where
 76 |     nextWeights :
 77 |       (i : Input) -> (weight : NodeWeight i.rows i.cols)
 78 |       -> Eff [Choose, (State (GraphT i.rows i.cols))] (NodeWeight i.rows i.cols, Integer)
 79 |     nextWeights i (coord, dir) = do
 80 |       -- Either turn or don't
 81 |       turn <- oneOf $ Nothing :: map Just (turns dir)
 82 |       case turn of
 83 |         Nothing => do
 84 |           Just next <- pure $ step coord (directionToStep dir)
 85 |             | _ => empty
 86 |           case next `index` i.room of
 87 |             Wall => empty
 88 |             _ => pure $ ((next, dir), 1)
 89 |         Just turn => pure $ ((coord, turn), 1000)
 90 |     toGraph :
 91 |       (weight : NodeWeight i.rows i.cols)
 92 |       -> Eff [Choose, (State (GraphT i.rows i.cols))] NodeId
 93 |     toGraph weight = do
 94 |       -- Check to see if the graph already has this node
 95 |       graph <- get
 96 |       Nothing <-
 97 |         pure . head' . filter (\x => Just weight == node_weight x graph) . nodes $  graph
 98 |         | Just id => pure id -- short circut if we have
 99 |       -- Get the id from inserting our node in the graph, update the state, and recurse
100 |       let (id, graph) = insert_node weight graph
101 |       put graph
102 |       -- Select our next weight
103 |       (next_weight, cost) <- nextWeights i weight
104 |       -- Get the id from recursion
105 |       next_id <- toGraph next_weight
106 |       -- Add our edge node
107 |       graph <- get
108 |       put $ insert_edge (id, next_id) cost graph
109 |       -- Return our id
110 |       pure id
111 |
112 | export
113 | part1 : String -> Eff [IO, Except String] (Integer, Input)
114 | part1 str = do
115 |   input <- tagAt LParse $ parseInput str
116 |   graph <- tagAt LSolve $ inputToGraph input
117 |   putStrLn $ "Converted to graph"
118 |   printLn graph
119 |   ?part1_rhs
120 |
121 | export
122 | part2 : Input -> Eff [IO, Except String] Integer
123 |