
  0 | module Days.Day7
  1 | 
  2 | import Data.String
  3 | import Data.List.Lazy
  4 | import Data.List1
  5 | import System
  6 | 
  7 | record Test where
  8 |   constructor MkTest
  9 |   test_value: Integer
 10 |   numbers: List Integer
 11 | %name Test test
 12 | 
 13 | Show Test where
 14 |   show (MkTest test_value numbers) =
 15 |     let numbers = joinBy " " . map show $ numbers
 16 |     in "\{show test_value}: \{numbers}"
 17 | 
 18 | Operator : Type
 19 | Operator = Integer -> Integer -> Integer
 20 | 
 21 | checkTest : (operators : LazyList Operator) -> Test -> Bool
 22 | checkTest operators (MkTest test_value numbers) =
 23 |   Data.List.Lazy.any (== test_value) $ allCombinations operators (fromList numbers)
 24 |   where
 25 |     allCombinations : (ops : LazyList Operator) -> LazyList Integer -> LazyList Integer
 26 |     allCombinations ops [] = []
 27 |     allCombinations ops (x :: []) = [x]
 28 |     allCombinations ops (x :: y :: xs) = do
 29 |       op <- ops
 30 |       let z = x `op` y
 31 |       if z > test_value
 32 |         then []
 33 |         else allCombinations ops (z :: xs)
 34 | 
 35 | totalPossiblyTrue : (ops : LazyList Operator) -> List Test -> Integer
 36 | totalPossiblyTrue ops tests =
 37 |   sum . map test_value . filter (checkTest ops) $ tests
 38 | 
 39 | parseTest : String -> Maybe Test
 40 | parseTest str =
 41 |   case split (== ':') $ str of
 42 |     (test_value ::: [rest]) => do
 43 |       test_value <- parseInteger test_value
 44 |       numbers <- traverse parseInteger . forget . split (== ' ') . trim $ rest
 45 |       Just $ MkTest test_value numbers
 46 |     _ => Nothing
 47 | 
 48 | parseInput : String -> Maybe (List Test)
 49 | parseInput str =
 50 |   let strs = map trim . lines $ str
 51 |   in traverse parseTest strs
 52 | 
 53 | export
 54 | part1 : String -> IO (String, List Test)
 55 | part1 str = do
 56 |   Just input <- pure $ parseInput str
 57 |     | _ => do
 58 |       putStrLn "Failed parsing input"
 59 |       exitFailure
 60 |   let out = totalPossiblyTrue [(+), (*)] input
 61 |   pure (show out, input)
 62 | 
 63 | export
 64 | part2 : List Test -> String -> IO String
 65 | part2 tests _ = do
 66 |   pure . show . totalPossiblyTrue [(+), (*), concatOp] $ tests
 67 |   where
 68 |     concatOp : Integer -> Integer -> Integer
 69 |     -- TODO: Do this with actual arithmetic and not string operations lol
 70 |     concatOp i j =
 71 |      let k = (show i) ++ (show j)
 72 |      in case parseInteger k of
 73 |        Nothing => assert_total (idris_crash "ummm???")
 74 |        Just x => x
 75 |