From 565dfa92dd005c2839e1401b73d8cb255243adb7 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 11 Dec 2022 05:07:39 -0500 Subject: [PATCH] Day 11 Part 1 --- 11/Main.idr | 269 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 11/input | 55 +++++++++++ 2 files changed, 324 insertions(+) create mode 100644 11/Main.idr create mode 100644 11/input diff --git a/11/Main.idr b/11/Main.idr new file mode 100644 index 0000000..f903991 --- /dev/null +++ b/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) diff --git a/11/input b/11/input new file mode 100644 index 0000000..76ed4aa --- /dev/null +++ b/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