Day 11 Part 1

11/Main.idr

@@ -0,0 +1,269 @@
+import Data.Vect
+import Data.List1
+import Data.SnocList
+import Data.String
+import Data.Fin
+import System.File.ReadWrite
+import Debug.Trace
+
+allFins' : (n : Nat) -> List (Fin n)
+allFins' n = toList (allFins'' n)
+  where
+    allFins'' : (n : Nat) -> SnocList (Fin n)
+    allFins'' 0 = Lin
+    allFins'' 1 = Lin :< FZ
+    allFins'' (S k) = map weaken (allFins'' k) :< last
+
+%default total
+
+data Error =
+  StartingItems String
+  | ParseTest String
+  | ParseOperation String
+  | ParseMonkey String
+  | ParseMonkeys String
+  | BadVect
+
+Show Error where
+  show (StartingItems str) = "StartingItems: " ++ str
+  show (ParseTest str) = "ParseTest: " ++ str
+  show (ParseOperation str) = "ParseOperation: " ++ str
+  show (ParseMonkey str) = "ParseMonkey: " ++ str
+  show (ParseMonkeys str) = "ParseMonkeys: " ++ str
+  show BadVect = "Invalid vector length, somehow"
+
+record Item where
+  constructor MkItem
+  worryLevel : Nat
+
+Show Item where
+  show (MkItem worryLevel) = "(worry: " ++ show worryLevel ++ ")"
+
+-- parse the items line
+parseItems : String -> Either Error (n : Nat ** Vect n Item)
+parseItems str =
+  let numeric = pack . dropWhile (not . isDigit) . unpack $ str
+      numStrings = split (== ',') numeric
+      numbers = traverse parsePositive (forget numStrings)
+  in case numbers of
+       Nothing => Left (StartingItems str)
+       Just numbers =>
+         let items = map MkItem numbers
+             len = length items
+         in case toVect len items of
+              Nothing => Left BadVect
+              Just items => Right (len ** items)
+
+record Test (monkeys : Nat) where
+  constructor MkTest
+  divisible_by : Nat
+  true_monkey : Fin monkeys
+  false_monkey : Fin monkeys
+
+Show (Test monkeys) where
+  show (MkTest divisible_by true_monkey false_monkey) =
+    "if divisible by " ++ show divisible_by ++ " then " ++ show true_monkey ++ " else " ++ show false_monkey
+
+parseTest : {monkeys : Nat } -> Vect 3 String -> Either Error (Test monkeys)
+parseTest {monkeys} input@[line_1, line_2, line_3] =
+  do Just divisible_by <- pure . lineToNat $ line_1
+       | Nothing => Left error
+     Just true_monkey <- pure . (lineToNat >=> finify) $ line_2
+       | Nothing => Left error
+     Just false_monkey <- pure . (lineToNat >=> finify) $ line_3
+       | Nothing => Left error
+     Right (MkTest divisible_by true_monkey false_monkey)
+  where lineToNat : String -> Maybe Nat
+        lineToNat = parsePositive . pack . dropWhile (not . isDigit) . unpack
+        error : Error
+        error = ParseTest (joinBy "\n" (toList input))
+        finify : Nat -> Maybe (Fin monkeys)
+        finify n = natToFin n monkeys
+
+applyTest : Test n -> Item -> Fin n
+applyTest (MkTest divisible_by true_monkey false_monkey) (MkItem worryLevel) =
+  if worryLevel `mod` divisible_by == 0
+    then true_monkey
+    else false_monkey
+
+data Operation =
+  Multiply Nat
+  | Add Nat
+  | MultiplySelf
+
+Show Operation where
+  show (Multiply k) = "old * " ++ show k
+  show (Add k) = "old + " ++ show k
+  show MultiplySelf = "old * old"
+
+parseOperation : String -> Either Error Operation
+parseOperation str =
+  let op = dropWhile (\x => not (x == '+' || x == '*')) . unpack $ str
+  in case op of
+       ('*' :: ' ' :: 'o' :: 'l' :: 'd' :: _) => Right MultiplySelf
+       ('*' :: ' ' :: rest) =>
+         case parsePositive (pack rest) of
+           Nothing => Left (ParseOperation str)
+           Just other => Right (Multiply other)
+       ('+' :: ' ' :: rest) =>
+         case parsePositive (pack rest) of
+           Nothing => Left (ParseOperation str)
+           Just other => Right (Add other)
+       _ => Left (ParseOperation str)
+
+applyOperation : Operation -> Item -> Item
+applyOperation (Multiply k) (MkItem worryLevel) = MkItem (k * worryLevel)
+applyOperation (Add k) (MkItem worryLevel) = MkItem (k + worryLevel)
+applyOperation MultiplySelf (MkItem worryLevel) = MkItem (worryLevel * worryLevel)
+
+calmItem : Item -> Item
+calmItem (MkItem worryLevel) = MkItem (worryLevel `div` 3)
+
+record Monkey (monkeys : Nat) where
+  constructor MkMonkey
+  id : Fin monkeys
+  item_count : Nat
+  items : Vect item_count Item
+  operation : Operation
+  test : Test monkeys
+  inspected : Nat
+
+Show (Monkey monkeys) where
+  show (MkMonkey id item_count items operation test inspected) =
+    "Monkey " ++ show id ++ ":\n" ++
+    "Items(" ++ show item_count ++ "): " ++ show items ++ "\n" ++
+    "Operation: " ++ show operation ++ "\n" ++
+    "Test: " ++ show test ++ "\n" ++
+    "Inspected: " ++ show inspected
+
+parseMonkey : {monkeys : Nat} -> Vect 6 String -> Either Error (Monkey monkeys)
+parseMonkey {monkeys} input@[id, starting_items, op, test_1, test_2, test_3] =
+  let test : Vect 3 String
+      test = [test_1, test_2, test_3]
+  in do Just id <- pure . (parsePositive >=> (\x => natToFin x monkeys)) . pack . filter isDigit . unpack $ id
+          | Nothing => Left error
+        (item_count ** items) <- parseItems starting_items
+        operation <- parseOperation op
+        test <- parseTest test
+        Right (MkMonkey id item_count items operation test 0)
+  where error : Error
+        error = ParseMonkey (joinBy "\n" (toList input))
+
+record Monkeys (count : Nat) where
+  constructor MkMonkeys
+  monkeys : Vect count (Monkey count)
+
+showMonkeys : Monkeys c -> String
+showMonkeys (MkMonkeys monkeys) =
+    show (length monkeys) ++ " Monkeys: \n" ++ joinBy "\n\n" (map show (toList monkeys))
+
+Show (Monkeys c) where
+  show monkeys = showMonkeys monkeys
+
+parseMonkeys : String -> Either Error (n : Nat ** Monkeys n)
+parseMonkeys str =
+  let individuals = forget . split (== "") . map trim . lines $ str
+      vects = traverse (toVect 6) individuals
+  in do Just vects <- pure vects
+          | Nothing => Left (ParseMonkeys str)
+        let count = length vects
+        Just vects <- pure (toVect count vects)
+          | Nothing => Left (ParseMonkeys str)
+        monkeys <- traverse (parseMonkey {monkeys = count}) vects
+        Right (count ** MkMonkeys monkeys)
+
+tag : Show a => String -> a -> a
+tag str = traceValBy (\x => str ++ ": " ++ show x)
+
+appendEnd : a -> Vect n a -> Vect (S n) a
+appendEnd x [] = [x]
+appendEnd x (y :: xs) = y :: appendEnd x xs
+
+throw : Monkeys c -> Item -> Fin c -> Monkeys c
+throw (MkMonkeys monkeys) item idx =
+  let monkey@(MkMonkey id item_count items operation test inspected) = index idx monkeys
+      newItems = appendEnd item items
+      newMonkey = MkMonkey id (S item_count) newItems operation test inspected
+      newMonkeys = replaceAt idx newMonkey monkeys
+  in MkMonkeys newMonkeys
+
+turn : Monkeys c -> Fin c -> Monkeys c
+turn inputMonkeys@(MkMonkeys monkeys) idx =
+  let inputMonkey@(MkMonkey id item_count items operation test inspected) = index idx monkeys
+      (outputMonkey, (MkMonkeys resMonkeys)) = itemsHelper inputMonkey inputMonkeys
+      outputMonkeys = replaceAt idx outputMonkey resMonkeys
+  in MkMonkeys outputMonkeys
+  where itemsHelper : Monkey c -> Monkeys c -> (Monkey c, Monkeys c)
+        itemsHelper monkey@(MkMonkey id 0 [] operation test inspected) y = (monkey, y)
+        itemsHelper monkey@(MkMonkey id (S len) (x :: xs) operation test inspected) y =
+          let operated = applyOperation operation x
+              calmed = calmItem operated
+              throwTo = applyTest test calmed
+              monkeys = throw y calmed throwTo
+          in itemsHelper (assert_smaller monkey (MkMonkey id len xs operation test (S inspected))) monkeys
+
+round : {c : Nat} -> Monkeys c -> Monkeys c
+round {c} input =
+  let indexes = allFins' c
+  in foldl turn input indexes
+
+rounds : {c: Nat} -> (d: Nat) -> Monkeys c -> Vect d (Monkeys c)
+rounds 0 x = []
+rounds (S k) x =
+  let newMonkeys = round x
+  in newMonkeys :: rounds k newMonkeys
+
+simple = """
+  Monkey 0:
+    Starting items: 79, 98
+    Operation: new = old * 19
+    Test: divisible by 23
+      If true: throw to monkey 2
+      If false: throw to monkey 3
+
+  Monkey 1:
+    Starting items: 54, 65, 75, 74
+    Operation: new = old + 6
+    Test: divisible by 19
+      If true: throw to monkey 2
+      If false: throw to monkey 0
+
+  Monkey 2:
+    Starting items: 79, 60, 97
+    Operation: new = old * old
+    Test: divisible by 13
+      If true: throw to monkey 1
+      If false: throw to monkey 3
+
+  Monkey 3:
+    Starting items: 74
+    Operation: new = old + 3
+    Test: divisible by 17
+      If true: throw to monkey 0
+      If false: throw to monkey 1
+  """
+
+testPart1 : IO ()
+testPart1 =
+  do Right (count ** inputMonkeys) <- pure (parseMonkeys simple)
+       | Left err => printLn err
+     let rounds = rounds 20 inputMonkeys
+     let lastRound = last rounds
+     let activity = foldl (*) 1 . take 2 . reverse . sort . toList . map inspected . monkeys $ lastRound
+     printLn activity
+
+part1 : {c : Nat} -> Monkeys c -> Nat
+part1 x =
+  let rounds = rounds 20 x
+      lastRound = last rounds
+  in foldl (*) 1 . take 2 . reverse . sort . toList . map inspected . monkeys $ lastRound
+
+partial main : IO ()
+main =
+  do Right file <- readFile "input"
+       | Left err => printLn err
+     Right (count ** monkeys) <- pure (parseMonkeys file)
+       | Left err => printLn err
+     printLn monkeys
+     putStr "Part 1: "
+     printLn (part1 monkeys)

11/input

@@ -0,0 +1,55 @@
+Monkey 0:
+  Starting items: 75, 63
+  Operation: new = old * 3
+  Test: divisible by 11
+    If true: throw to monkey 7
+    If false: throw to monkey 2
+
+Monkey 1:
+  Starting items: 65, 79, 98, 77, 56, 54, 83, 94
+  Operation: new = old + 3
+  Test: divisible by 2
+    If true: throw to monkey 2
+    If false: throw to monkey 0
+
+Monkey 2:
+  Starting items: 66
+  Operation: new = old + 5
+  Test: divisible by 5
+    If true: throw to monkey 7
+    If false: throw to monkey 5
+
+Monkey 3:
+  Starting items: 51, 89, 90
+  Operation: new = old * 19
+  Test: divisible by 7
+    If true: throw to monkey 6
+    If false: throw to monkey 4
+
+Monkey 4:
+  Starting items: 75, 94, 66, 90, 77, 82, 61
+  Operation: new = old + 1
+  Test: divisible by 17
+    If true: throw to monkey 6
+    If false: throw to monkey 1
+
+Monkey 5:
+  Starting items: 53, 76, 59, 92, 95
+  Operation: new = old + 2
+  Test: divisible by 19
+    If true: throw to monkey 4
+    If false: throw to monkey 3
+
+Monkey 6:
+  Starting items: 81, 61, 75, 89, 70, 92
+  Operation: new = old * old
+  Test: divisible by 3
+    If true: throw to monkey 0
+    If false: throw to monkey 1
+
+Monkey 7:
+  Starting items: 81, 86, 62, 87
+  Operation: new = old + 8
+  Test: divisible by 13
+    If true: throw to monkey 3
+    If false: throw to monkey 5