
  0 | module Days.Day2
  1 | 
  2 | import Data.String
  3 | import Data.List1
  4 | import Data.Vect
  5 | import Data.Fin
  6 | import System
  7 | 
  8 | parseReport : String -> Maybe (List Integer)
  9 | parseReport = traverse parseInteger . forget . split (== ' ')
 10 | 
 11 | parseReports : String -> Maybe (List (List Integer))
 12 | parseReports = traverse parseReport . lines
 13 | 
 14 | ordered : (pred : a -> a -> Bool) -> List a -> Bool
 15 | ordered pred [] = True
 16 | ordered pred (x :: []) = True
 17 | ordered pred (x :: (y :: xs)) =
 18 |   if x `pred` y
 19 |   then ordered pred (y :: xs)
 20 |   else False
 21 | 
 22 | maxStep : List Integer -> Integer
 23 | maxStep is = maxStep' is 0
 24 |   where
 25 |    maxStep' : (xs : List Integer) -> (acc : Integer) -> Integer
 26 |    maxStep' [] acc = acc
 27 |    maxStep' (x :: []) acc = acc
 28 |    maxStep' (x :: (y :: xs)) acc =
 29 |      let step = abs $ y - x
 30 |          next_acc = if step > acc then step else acc
 31 |      in maxStep' (y :: xs) next_acc
 32 | 
 33 | safeReport : (report : List Integer) -> Bool
 34 | safeReport report =
 35 |   if (ordered (<) report) || (ordered (>) report)
 36 |   -- Cases where maxStep is less than one should be excluded by both of the
 37 |   -- predicates above being inequalities
 38 |   then maxStep report <= 3
 39 |   else False
 40 | 
 41 | deletions : List a -> List (List a)
 42 | deletions xs =
 43 |   let len = length xs
 44 |   in case toVect len xs of
 45 |     Nothing => [] -- Shouldn't happen
 46 |     Just xs =>
 47 |       case len of
 48 |         0 => []
 49 |         (S k) =>
 50 |           let idxs = Data.Fin.List.allFins (S k)
 51 |               vects = map (\i => deleteAt i xs) idxs
 52 |           in map toList vects
 53 | 
 54 | safeWithDeletion : (report : List Integer) -> Bool
 55 | safeWithDeletion report =
 56 |   safeReport report || any safeReport (deletions report)
 57 | 
 58 | export
 59 | part1 : String -> IO (String, List (List Integer))
 60 | part1 str =
 61 |   case parseReports str of
 62 |     Nothing => do
 63 |       putStrLn "Error parsing puzzle input"
 64 |       exitFailure
 65 |     Just reports =>
 66 |       pure (show $ count safeReport reports, reports)
 67 | 
 68 | export
 69 | part2 : (reports : List (List Integer)) -> String -> IO String
 70 | part2 reports _ =
 71 |   pure . show $ count safeWithDeletion reports
 72 |