7 | import Control.Eff.Except
11 | ParseError : Type -> Type
12 | ParseError = ExceptL "parse" String
14 | data ModInt : Integer -> Type where
15 | MkMod : (0 modulus : Integer) -> (val : Integer) -> ModInt modulus
17 | toFin : {modulus : Integer} -> ModInt modulus -> Fin (integerToNat modulus)
18 | toFin (MkMod modulus val) =
19 | case integerToFin val (integerToNat modulus) of
20 | Nothing => assert_total (idris_crash "wat")
23 | inner : ModInt x -> Integer
24 | inner (MkMod x val) = val
26 | {modulus : Integer} -> Num (ModInt modulus) where
27 | (+) (MkMod _ val_x) (MkMod _ val_y) =
28 | MkMod _ ((val_x + val_y) `mod` modulus)
29 | (*) (MkMod _ val_x) (MkMod _ val_y) =
30 | MkMod _ ((val_x * val_y) `mod` modulus)
31 | fromInteger x = MkMod _ (x `mod` modulus)
33 | {modulus : Integer} -> Neg (ModInt modulus) where
34 | (-) (MkMod _ x) (MkMod _ y) = MkMod _ ((x - y) `mod` modulus)
35 | negate (MkMod _ val) = MkMod _ ((negate val) `mod` modulus)
37 | Show (ModInt modulus) where
38 | show (MkMod _ x) = show x
40 | ModPair : (x, y : Integer) -> Type
41 | ModPair x y = (ModInt x, ModInt y)
43 | record Robot (x_mod, y_mod : Integer) where
45 | position : ModPair x_mod y_mod
46 | velocity : (Integer, Integer)
49 | advanceRobot : {x, y : Integer} -> Robot x y -> Robot x y
50 | advanceRobot (MkRobot (x', y') (dx, dy)) =
51 | let (x', y') = (x' + (fromInteger dx), y' + (fromInteger dy))
52 | in MkRobot (x', y') (dx, dy)
56 | x_mod, y_mod : Integer
57 | robots : List (Robot x_mod y_mod)
60 | advanceInput : Input -> Input
61 | advanceInput (MkInput x_mod y_mod robots) =
62 | MkInput x_mod y_mod (map advanceRobot robots)
64 | overlapping : Input -> Nat
65 | overlapping (MkInput x_mod y_mod robots) =
66 | let robots' = nubBy roboeq robots
67 | in length robots `minus` length robots'
69 | roboeq : (Robot x_mod y_mod) -> (Robot x_mod y_mod) -> Bool
71 | let (x, y) = (inner . fst $
rob.position, inner . snd $
rob.position)
72 | (x', y') = (inner . fst $
rob1.position, inner . snd $
rob1.position)
73 | in x == x' && y == y'
75 | G : Nat -> Nat -> Type
76 | G rows cols = Vect rows (Vect cols Nat)
79 | show (MkInput x_mod y_mod robots) =
80 | let grid : G (integerToNat y_mod) (integerToNat x_mod) =
81 | replicate _ (replicate _ 0)
82 | f : G (integerToNat y_mod) (integerToNat x_mod)
83 | -> Robot x_mod y_mod
84 | -> G (integerToNat y_mod) (integerToNat x_mod)
85 | f xs (MkRobot (x, y) vel) =
86 | let (x, y) = (toFin x, toFin y)
87 | in updateAt y (updateAt x S) xs
88 | natToStr : Nat -> String
90 | natToStr (S k) = show (S k)
91 | in joinBy "\n" . toList . map (joinBy " " . toList . map natToStr) . foldl f grid $
robots
93 | parseRobot : Has ParseError fs =>
94 | {x, y: Integer} -> (input : String) -> Eff fs (Robot x y)
95 | parseRobot input = do
96 | pos ::: vel :: [] <- pure . split (== ' ') . trim $
input
97 | | _ => throwAt "parse" "Too many components"
98 | let pos = strSubstr 2 (strLength pos - 1) . trim $
pos
99 | let vel = strSubstr 2 (strLength vel - 1) . trim $
vel
100 | pos_x ::: pos_y :: [] <- pure . split (== ',') $
pos
101 | | _ => throwAt "parse" "Too many position components"
102 | vel_x ::: vel_y :: [] <- pure . split (== ',') $
vel
103 | | _ => throwAt "parse" "Too many velocity components"
104 | [pos_x, pos_y, vel_x, vel_y] <-
105 | noteAt "parse" "Parsing integers" $
106 | traverse parseInteger (the (Vect _ _) [pos_x, pos_y, vel_x, vel_y])
107 | pure $
MkRobot (fromInteger pos_x, fromInteger pos_y) (vel_x, vel_y)
109 | parseInput : Has ParseError fs => (x_mod, y_mod : Integer) -> (input : String) -> Eff fs Input
110 | parseInput x_mod y_mod input = do
111 | let input = lines . trim $
input
112 | robots <- traverse parseRobot input
113 | pure $
MkInput x_mod y_mod robots
116 | part1 : String -> Eff [IO, Except String] (Integer, Input)
118 | input <- tagAt "parse" $
parseInput 101 103 str
119 | let MkInput x_mod y_mod robots = doTimes advanceInput 100 $
input
120 | let a = filter (f (<) (<)) robots
121 | let b = filter (f (<) (>)) robots
122 | let c = filter (f (>) (<)) robots
123 | let d = filter (f (>) (>)) robots
124 | let t = length a * length b * length c * length d
125 | pure (natToInteger t, input)
127 | f : (cmp1, cmp2 : Integer -> Integer -> Bool) -> Robot a b -> Bool
128 | f cmp1 cmp2 robot =
129 | ((inner . fst $
robot.position) `cmp1` 50) && ((inner . snd $
robot.position) `cmp2` 51)
132 | part2 : Input -> Eff [IO, Except String] Integer
135 | ((i, overlapping, step) :: steps) <-
136 | pure . filter ((== (the Nat 0)) . fst . snd) . zip (lazyRange max) . map (\x => (overlapping x, x)). lazyTimes max advanceInput $
input
137 | | _ => throw "No steps, somehow"