diff --git a/aoc2024/Day14.newt b/aoc2024/Day14.newt index b0f4717..751c3e1 100644 --- a/aoc2024/Day14.newt +++ b/aoc2024/Day14.newt @@ -92,18 +92,18 @@ run fn w h = do | Left msg => putStrLn $ "Parse Error " ++ msg | Right (robots, rest) => putStrLn $ "stuck at¬" ++ pack rest let result = map (move w h 100) robots - -- debugLog result + -- printLn result let q1 = count quad1 result let q2 = count quad2 result let q3 = count quad3 result let q4 = count quad4 result - debugLog (q1,q2,q3,q4) + printLn (q1,q2,q3,q4) let p1 = q1 * q2 * q3 * q4 putStrLn $ "part1 " ++ show p1 printLn $ count (\ x => True) robots let scores = collect robots 0 Nil let stuff = qsort (\ a b => snd a < snd b) $ collect robots 0 Nil - -- debugLog stuff + -- printLn stuff dump robots stuff 1 where dump : List Robot → List (Int × Int) → Int → IO Unit diff --git a/aoc2024/Day14.newt.golden b/aoc2024/Day14.newt.golden index 9e331e0..f5b6449 100644 --- a/aoc2024/Day14.newt.golden +++ b/aoc2024/Day14.newt.golden @@ -1,5 +1,5 @@ aoc2024/day14/input.txt -(121, 119, 119, 132) +(121, (119, (119, 132))) part1 226179492 500 7502 diff --git a/aoc2024/Day15.newt b/aoc2024/Day15.newt index 48c3864..7f358f5 100644 --- a/aoc2024/Day15.newt +++ b/aoc2024/Day15.newt @@ -94,12 +94,12 @@ run fn = do putStrLn fn text <- readFile fn let (Right (grid,steps)) = parseFile text | Left err => putStrLn $ "Error " ++ err - let ((start,_) :: Nil) = filter ((_==_ '@') ∘ snd) $ toList grid | x => debugLog x + let ((start,_) :: Nil) = filter ((_==_ '@') ∘ snd) $ toList grid | x => printLn x let (grid', end) = foldl step (grid, start) steps let p1 = foldl _+_ 0 $ map (gps ∘ fst) $ filter (_==_ 'O' ∘ snd) $ toList grid' putStrLn $ "part1 " ++ show p1 let grid2 = mkPart2 grid - let ((start,_) :: Nil) = filter ((_==_ '@') ∘ snd) $ toList grid2 | x => debugLog x + let ((start,_) :: Nil) = filter ((_==_ '@') ∘ snd) $ toList grid2 | x => printLn x let (grid2', end) = foldl step (grid2, start) steps let p2 = foldl _+_ 0 $ map (gps ∘ fst) $ filter (_==_ '[' ∘ snd) $ toList grid2' putStrLn $ "part2 " ++ show p2 diff --git a/aoc2024/Day18.newt b/aoc2024/Day18.newt index 7cdedb4..6d27906 100644 --- a/aoc2024/Day18.newt +++ b/aoc2024/Day18.newt @@ -94,7 +94,7 @@ run fn size time = do | Right (_, cs) => putStrLn $ "extra: " ++ pack cs let p1map = step EmptyMap points time let p1 = minPath p1map size - debugLog $ length $ toList p1map + printLn $ length $ toList p1map putStrLn $ "part1 " ++ show p1 let p2map = step2 EmptyMap points 0 let p2 = part2 p2map size diff --git a/aoc2024/Day21.newt b/aoc2024/Day21.newt index 806e4ce..6ba07b1 100644 --- a/aoc2024/Day21.newt +++ b/aoc2024/Day21.newt @@ -123,7 +123,7 @@ run fn = do -- the space is illegal spot let numpad = fromList $ filter (not ∘ _==_ ' ' ∘ fst) $ gridPoints "789\n456\n123\n 0A" - debugLog $ toList numpad + printLn $ toList numpad let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing let robn = makeKeypad 2 rob1 diff --git a/aoc2024/Day21.newt.golden b/aoc2024/Day21.newt.golden index 2742e34..e740b44 100644 --- a/aoc2024/Day21.newt.golden +++ b/aoc2024/Day21.newt.golden @@ -1,8 +1,8 @@ aoc2024/day21/eg.txt -[("0", 3, 1), ("1", 2, 0), ("2", 2, 1), ("3", 2, 2), ("4", 1, 0), ("5", 1, 1), ("6", 1, 2), ("7", 0, 0), ("8", 0, 1), ("9", 0, 2), ("A", 3, 2)] +(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2)) part1 126384 part2 154115708116294 aoc2024/day21/input.txt -[("0", 3, 1), ("1", 2, 0), ("2", 2, 1), ("3", 2, 2), ("4", 1, 0), ("5", 1, 1), ("6", 1, 2), ("7", 0, 0), ("8", 0, 1), ("9", 0, 2), ("A", 3, 2)] +(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2)) part1 248108 part2 303836969158972 diff --git a/aoc2024/Day21monad.newt b/aoc2024/Day21monad.newt index 6c29817..f6230ad 100644 --- a/aoc2024/Day21monad.newt +++ b/aoc2024/Day21monad.newt @@ -158,7 +158,7 @@ run fn = do -- the space is illegal spot let numpad = fromList $ filter (not ∘ _==_ ' ' ∘ fst) $ gridPoints "789\n456\n123\n 0A" - debugLog $ toList numpad + printLn $ toList numpad let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing let robn = makeKeypad 2 rob1 diff --git a/aoc2024/Day21monad.newt.golden b/aoc2024/Day21monad.newt.golden index 2742e34..e740b44 100644 --- a/aoc2024/Day21monad.newt.golden +++ b/aoc2024/Day21monad.newt.golden @@ -1,8 +1,8 @@ aoc2024/day21/eg.txt -[("0", 3, 1), ("1", 2, 0), ("2", 2, 1), ("3", 2, 2), ("4", 1, 0), ("5", 1, 1), ("6", 1, 2), ("7", 0, 0), ("8", 0, 1), ("9", 0, 2), ("A", 3, 2)] +(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2)) part1 126384 part2 154115708116294 aoc2024/day21/input.txt -[("0", 3, 1), ("1", 2, 0), ("2", 2, 1), ("3", 2, 2), ("4", 1, 0), ("5", 1, 1), ("6", 1, 2), ("7", 0, 0), ("8", 0, 1), ("9", 0, 2), ("A", 3, 2)] +(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2)) part1 248108 part2 303836969158972 diff --git a/aoc2024/Day25.newt b/aoc2024/Day25.newt index a4860c3..0884724 100644 --- a/aoc2024/Day25.newt +++ b/aoc2024/Day25.newt @@ -57,7 +57,7 @@ run fn = do text <- readFile fn let chunks = parseFile text let (locks,keys) = splitKeys chunks Nil Nil - debugLog (length locks, length keys) + printLn (length locks, length keys) let p1 = foldl _+_ 0 $ map (\ l => foldl _+_ 0 $ map (check l) keys) locks putStrLn $ "part1 " ++ show p1 diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index f4e52b4..f47624b 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -444,8 +444,9 @@ processData ns fc nm ty cons = do unifyCatch fc (mkCtx fc) tyty' type' Just _ => error fc "\{show nm} already declared" Nothing => setDef (QN ns nm) fc tyty Axiom Nil - entries <- join <$> (for (enumerate cons) $ \x => case x of - (ix, TypeSig fc names tm) => do + -- check cons, return list of type,con + allCons <- join <$> (for cons $ \x => case x of + (TypeSig fc names tm) => do traverse (checkAlreadyDef fc) names debug $ \ _ => "check dcon \{show names} \{show tm}" dty <- check (mkCtx fc) tm (VU fc) @@ -460,11 +461,12 @@ processData ns fc nm ty cons = do | (tm, _) => error (getFC tm) "expected \{nm} got \{render 90 $ pprint tnames tm}" when (hn /= QN ns nm) $ \ _ => error (getFC codomain) "Constructor codomain is \{render 90 $ pprint tnames codomain} rather than \{nm}" - pure $ map (\ nm' => (MkEntry fc (QN ns nm') dty (DCon ix NormalCon (getArity dty) hn) Nil)) names - (_,decl) => throwError $ E (getFC decl) "expected constructor declaration") + pure $ map (_,_ dty) names + decl => throwError $ E (getFC decl) "expected constructor declaration") -- type level autos like _++_ solveAutos - let entries = populateConInfo entries + + let entries = populateConInfo $ map makeConEntry $ enumerate allCons for entries $ \case (MkEntry name fc dty def flags) => setDef fc name dty def flags let cnames = map (\x => x.name) entries @@ -472,6 +474,9 @@ processData ns fc nm ty cons = do let arity = cast $ piArity tyty updateDef (QN ns nm) fc tyty (TCon arity cnames) where + makeConEntry : (Nat × Tm × String) → TopEntry + makeConEntry (ix, dty, nm') = MkEntry fc (QN ns nm') dty (DCon ix NormalCon (getArity dty) (QN ns nm)) Nil + binderName : Binder → Name binderName (MkBinder _ nm _ _ _) = nm