Compare commits

..

No commits in common. "d68664a356a994a0e17386ef7182d99a7498109e" and "dd61600c49bf2d32830c93bbe62169bb0fbf801f" have entirely different histories.

2 changed files with 0 additions and 285 deletions

View File

@ -1,230 +0,0 @@
import Data.Vect
import Data.List1
import Data.SnocList
import Data.String
import Data.Fin
import System.File.ReadWrite
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 : Integer
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 : Integer
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 . parsePositive . pack . dropWhile (not . isDigit) . unpack $ 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 Integer
| Add Integer
| 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)
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 = snoc items item
newMonkey = MkMonkey id (S item_count) newItems operation test inspected
newMonkeys = replaceAt idx newMonkey monkeys
in MkMonkeys newMonkeys
turn : (calmOp : Item -> Item) -> Monkeys c -> Fin c -> Monkeys c
turn calmOp 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 = calmOp 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} -> (calmOp : Item -> Item) -> Monkeys c -> Monkeys c
round {c} calmOp input =
let indexes = allFins' c
in foldl (turn calmOp) input indexes
rounds : {c: Nat} -> (d: Nat) -> (calmOp : Item -> Item) -> Monkeys c -> Vect d (Monkeys c)
rounds 0 calmOp x = []
rounds (S k) calmOp x =
let newMonkeys = round calmOp x
in newMonkeys :: rounds k calmOp newMonkeys
part1 : {c : Nat} -> Monkeys c -> Nat
part1 x =
let rounds = rounds 20 calmItem x
lastRound = last rounds
in foldl (*) 1 . take 2 . reverse . sort . toList . map inspected . monkeys $ lastRound
part2 : {c : Nat} -> Monkeys c -> Nat
part2 x =
let multiple = product . map divisible_by . map test . monkeys $ x
rounds = rounds 10000 (\(MkItem x) => MkItem (x `mod` multiple)) 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
putStr "Part 1: "
printLn (part1 monkeys)
putStr "Part 2: "
printLn (part2 monkeys)

View File

@ -1,55 +0,0 @@
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