
   0 | module Days.Day5
   1 | 
   2 | import Data.String
   3 | import Data.Nat
   4 | import Data.Maybe
   5 | import Data.List1
   6 | import System
   7 | 
   8 | record Rule where
   9 |   constructor MkRule
  10 |   before, after : Nat
  11 | %name Rule rule
  12 | 
  13 | record Update where
  14 |   constructor MkUpdate
  15 |   pages : List Nat
  16 | %name Update update
  17 | 
  18 | record Input where
  19 |   constructor MkInput
  20 |   rules : List Rule
  21 |   updates : List Update
  22 | %name Input input
  23 | 
  24 | appliesTo : Nat -> Rule -> Bool
  25 | appliesTo k (MkRule before after) =
  26 |   k == before || k == after
  27 | 
  28 | appliesTo' : Nat -> Nat -> Rule -> Bool
  29 | appliesTo' k j (MkRule before after) =
  30 |   (k == before && j == after) || (j == before && k == after)
  31 | 
  32 | Show Input where
  33 |   show input =
  34 |     let rules = unlines . map showRule $ input.rules
  35 |         updates = unlines . map showUpdate $ input.updates
  36 |     in fastConcat [rules, "\n", updates]
  37 |     where
  38 |       showRule : Rule -> String
  39 |       showRule (MkRule before after) =
  40 |         "\{show before}|\{show after}"
  41 |       showUpdate : Update -> String
  42 |       showUpdate (MkUpdate pages) =
  43 |         joinBy "," . map show $ pages
  44 | 
  45 | parseInput : String -> Maybe Input
  46 | parseInput str =
  47 |   let ls = map trim . lines $ str
  48 |   in case forget $ splitOn "" ls of
  49 |     [rules, updates] => do
  50 |       rules <- traverse parseRule rules
  51 |       updates <- traverse parseUpdate updates
  52 |       Just $ MkInput rules updates
  53 |     _ => Nothing
  54 |   where
  55 |     parseRule : String -> Maybe Rule
  56 |     parseRule str =
  57 |       case forget $ split (=='|') str of
  58 |         [before, after] => do
  59 |           before <- parsePositive before
  60 |           after <- parsePositive after
  61 |           Just $ MkRule before after
  62 |         _ => Nothing
  63 |     parseUpdate : String -> Maybe Update
  64 |     parseUpdate str = do
  65 |       pages <- traverse parsePositive . forget . split (==',') $ str
  66 |       Just $ MkUpdate pages
  67 | 
  68 | Cursor : Type -> Type
  69 | Cursor a = (SnocList a, a, List a)
  70 | 
  71 | listToCursor : List a -> Maybe (Cursor a)
  72 | listToCursor [] = Nothing
  73 | listToCursor (x :: xs) = Just (Lin, x, xs)
  74 | 
  75 | rulesHere : List Rule -> Cursor Nat -> Maybe Nat
  76 | rulesHere rules (b, c, a) =
  77 |   let applies = filter (appliesTo c) rules
  78 |   in if (checkBefore applies c b) && (checkAfter applies c a)
  79 |     then Nothing
  80 |     else Just (length b)
  81 |   where
  82 |     checkBefore : List Rule -> Nat -> SnocList Nat -> Bool
  83 |     checkBefore rules k [<] = True
  84 |     checkBefore rules k (sx :< x) =
  85 |       case head' . filter (appliesTo' x k) $ rules of
  86 |         Nothing => checkBefore rules k sx
  87 |         Just (MkRule before after) =>
  88 |           if before == x && after == k
  89 |             then checkBefore rules k sx
  90 |             else False
  91 |     checkAfter : List Rule -> Nat -> List Nat -> Bool
  92 |     checkAfter rules k [] = True
  93 |     checkAfter rules k (x :: xs) =
  94 |       case head' . filter (appliesTo' x k) $ rules of
  95 |         Nothing => checkAfter rules k xs
  96 |         Just (MkRule before after) =>
  97 |           if after == x && before == k
  98 |             then checkAfter rules k xs
  99 |             else False
 100 | 
 101 |  
 102 | -- Return nothing if the update passes the rules, otherwise the index of the offending element
 103 | validateUpdate : List Rule -> Update -> Maybe Nat
 104 | validateUpdate rules (MkUpdate pages) =
 105 |   case listToCursor pages of
 106 |     -- Not 100% how to handle the empty case, but it can't _break_ any rules
 107 |     Nothing => Nothing
 108 |     Just pages => rulesAll rules pages
 109 |   where
 110 |     rulesAll : List Rule -> Cursor Nat -> Maybe Nat
 111 |     rulesAll rules cs@(before, current, []) =
 112 |       rulesHere rules cs
 113 |     rulesAll rules cs@(before, current, (x :: xs)) =
 114 |       case rulesHere rules cs of
 115 |         Nothing => rulesAll rules (before :< current, x, xs)
 116 |         idx => idx
 117 | 
 118 | middlePage : Update -> Nat
 119 | middlePage (MkUpdate pages) =
 120 |   let idx = ((length pages) `divNatNZ` 2) ItIsSucc
 121 |   in indexAlt 0 idx pages
 122 |   where
 123 |     indexAlt : (alt : a) -> (idx : Nat) -> List a -> a
 124 |     indexAlt alt idx [] = alt
 125 |     indexAlt alt 0 (x :: xs) = x
 126 |     indexAlt alt (S k) (x :: xs) = indexAlt alt k xs
 127 | 
 128 | indexes : List a -> List (Nat, a)
 129 | indexes xs = indexes' 0 xs
 130 |   where
 131 |     indexes' : Nat -> List a -> List (Nat, a)
 132 |     indexes' k [] = []
 133 |     indexes' k (x :: xs) = (k, x) :: indexes' (S k) xs
 134 | 
 135 | showBoolList : List Bool -> String
 136 | showBoolList xs =
 137 |   unlines . map (\(i,x) => "\{show (i + 1)}: \{show x}") . indexes $ xs
 138 | 
 139 | removeBadPage : List Rule -> Update -> Maybe (Update, Nat)
 140 | removeBadPage rules update@(MkUpdate pages) =
 141 |   case validateUpdate rules update of
 142 |     Nothing => Nothing
 143 |     Just idx =>
 144 |       case inBounds idx pages of
 145 |         Yes prf =>
 146 |           let page = index idx pages
 147 |               removed = deleteAt idx pages
 148 |           in Just (MkUpdate removed, page)
 149 |         No contra => Nothing
 150 | 
 151 | insertPage : List Rule -> Update -> Nat -> Update
 152 | insertPage rules (MkUpdate []) k = MkUpdate []
 153 | insertPage rules (MkUpdate (x :: xs)) k = insertPage' rules (Lin, x, xs) k
 154 |   where
 155 |     cursorToList : Cursor Nat -> List Nat
 156 |     cursorToList ([<], current, after) = current :: after
 157 |     cursorToList ((sx :< y), current, after) = cursorToList (sx, y, current :: after)
 158 |     cursorToUpdate : Cursor Nat -> Update
 159 |     cursorToUpdate x = MkUpdate (cursorToList x)
 160 |     insertPage' : List Rule -> Cursor Nat -> Nat -> Update
 161 |     insertPage' rules (before, current, []) k =
 162 |       if isNothing $ rulesHere rules (before, k, [current])
 163 |         then cursorToUpdate (before, k, [current])
 164 |         else cursorToUpdate (before, current, [k])
 165 |     insertPage' rules (before, current, (y :: ys)) k =
 166 |       let cs = (before, k, (current :: y ::ys))
 167 |       in if isNothing $ rulesHere rules cs
 168 |         then cursorToUpdate cs
 169 |         else insertPage' rules (before :< current, y, ys) k
 170 | 
 171 | fixUpdate : List Rule -> Update -> Update
 172 | fixUpdate rules update =
 173 |   case removeBadPage rules update of
 174 |     Nothing => update
 175 |     Just (update, page) => fixUpdate rules (insertPage rules update page)
 176 | 
 177 | export
 178 | part1 : String -> IO (String, Input)
 179 | part1 str =
 180 |   case parseInput str of
 181 |     Nothing => do
 182 |       putStrLn "Failed parsing input"
 183 |       exitFailure
 184 |     Just input => do
 185 |       let middles =
 186 |         map middlePage . filter (isNothing . validateUpdate input.rules) $ input.updates
 187 |       pure (show . sum $ middles, input)
 188 | 
 189 | export
 190 | part2 : Input -> String -> IO String
 191 | part2 input _ = do
 192 |   let bad_updates = filter (isJust . validateUpdate input.rules) $ input.updates
 193 |   let fixed_updates = map (fixUpdate input.rules) bad_updates
 194 |   let middles = map middlePage fixed_updates
 195 |   pure . show . sum $ middles
 196 |