diff --git a/.gitignore b/.gitignore index dc3cb4d..8e6f4dd 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ build/ /*.js input.txt node_modules +mkday.py diff --git a/aoc2023/Aoc.newt b/aoc2023/Aoc.newt index 8ab948b..7cd501d 100644 --- a/aoc2023/Aoc.newt +++ b/aoc2023/Aoc.newt @@ -29,3 +29,19 @@ indexOf? {a} z xs = go Z z xs go ix z Nil = Nothing go ix z (x :: xs) = if z == x then Just ix else go (S ix) z xs + +-- TODO move to Aoc library +Point : U +Point = Int × Int + +instance Add Point where + (a,b) + (c,d) = (a + c, b + d) + +instance Sub Point where + (a,b) - (c,d) = (a - c, b - d) + +instance Ord Point where + (a,b) < (c,d) = a < c || a == c && b < d + +instance Eq Point where + (a,b) == (c,d) = a == c && b == d diff --git a/aoc2024/Day10.newt b/aoc2024/Day10.newt index fc57034..d3d1d3b 100644 --- a/aoc2024/Day10.newt +++ b/aoc2024/Day10.newt @@ -16,21 +16,6 @@ gridPoints text = go 0 0 (unpack text) Nil go row col ('\n' :: cs) points = go (row + 1) 0 cs points go row col (c :: cs) points = go row (col + 1) cs ((c,row,col) :: points) -Point : U -Point = Int × Int - -instance Add Point where - (a,b) + (c,d) = (a + c, b + d) - -instance Sub Point where - (a,b) - (c,d) = (a - c, b - d) - -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - -- TODO add parameter a and pass Char -> a into getGrid Grid : U Grid = SortedMap Point Int @@ -59,12 +44,6 @@ paths grid pts ht = getCands : Point → List (Point × Int) getCands pt = mapMaybe (\ p => lookupMap p grid) (peers pt) -foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b -foldMap f m Nil = m -foldMap f m ((a,b) :: xs) = case lookupMap a m of - Nothing => foldMap f (updateMap a b m) xs - Just (_, b') => foldMap f (updateMap a (f b' b) m) xs - paths2 : Grid → List (Point × Int) → Int → Int paths2 grid pts ht = if ht == 9 then foldl _+_ 0 $ map snd $ pts else diff --git a/aoc2024/Day11.newt b/aoc2024/Day11.newt index 4277be2..e0a29bc 100644 --- a/aoc2024/Day11.newt +++ b/aoc2024/Day11.newt @@ -14,12 +14,6 @@ pfunc divide uses (_,_) : String → String × String := `(s) => { return _$2C_(undefined, undefined, s.slice(0,l), s.slice(l)) }` -foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b -foldMap f m Nil = m -foldMap f m ((a,b) :: xs) = case lookupMap a m of - Nothing => foldMap f (updateMap a b m) xs - Just (_, b') => foldMap f (updateMap a (f b' b) m) xs - step : List (Int × Int) → List (Int × Int) step = go Nil where diff --git a/aoc2024/Day11b.newt b/aoc2024/Day11b.newt index a5be114..87dc34c 100644 --- a/aoc2024/Day11b.newt +++ b/aoc2024/Day11b.newt @@ -22,12 +22,6 @@ stone num = if num == 0 then Left 1 else go num num 1 else if b < 10 then Left (2024 * num) else go (div53 a 10) (div53 b 100) (mod * 10) -foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b -foldMap f m Nil = m -foldMap f m ((a,b) :: xs) = case lookupMap a m of - Nothing => foldMap f (updateMap a b m) xs - Just (_, b') => foldMap f (updateMap a (f b' b) m) xs - step : List (Int × Int) → List (Int × Int) step xs = go Nil xs where diff --git a/aoc2024/Day12.newt b/aoc2024/Day12.newt index 9982abb..d3d8acb 100644 --- a/aoc2024/Day12.newt +++ b/aoc2024/Day12.newt @@ -16,21 +16,6 @@ gridPoints text = go 0 0 (unpack text) Nil go row col ('\n' :: cs) points = go (row + 1) 0 cs points go row col (c :: cs) points = go row (col + 1) cs ((c,row,col) :: points) -Point : U -Point = Int × Int - -instance Add Point where - (a,b) + (c,d) = (a + c, b + d) - -instance Sub Point where - (a,b) - (c,d) = (a - c, b - d) - -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - -- TODO add parameter a and pass Char -> a into getGrid Grid : U Grid = SortedMap Point Int diff --git a/aoc2024/Day13.newt b/aoc2024/Day13.newt index 0702ade..e0adae9 100644 --- a/aoc2024/Day13.newt +++ b/aoc2024/Day13.newt @@ -5,27 +5,6 @@ import Node import Aoc import Parser - -Point : U -Point = Int × Int - -instance Add Point where - (a,b) + (c,d) = (a + c, b + d) - -instance Sub Point where - (a,b) - (c,d) = (a - c, b - d) - -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - - -token : String → Parser Unit -token str = string str >> ws - - data Machine : U where MkMachine : Point → Point → Point → Machine diff --git a/aoc2024/Day14.newt b/aoc2024/Day14.newt new file mode 100644 index 0000000..b0f4717 --- /dev/null +++ b/aoc2024/Day14.newt @@ -0,0 +1,156 @@ +module Day14 + +import Prelude +import Node +import Aoc +import Parser +import SortedMap + +data Robot : U where + MkBot : Point → Point → Robot + +pint : Parser Int +pint = do + sign <- pure (0 - 1) <* match '-' <|> pure 1 + num <- number + pure $ sign * num + +ppoint : Parser Point +ppoint = _,_ <$> pint <* match ',' <*> pint + +probot : Parser Robot +probot = do + token "p=" + p <- ppoint + ws + token "v=" + v <- ppoint + ws + many (match '\n') + pure $ MkBot p v + +-- TODO make Mod typeclass or something +infixl 7 _%_ +pfunc _%_ : Int → Int → Int := `(x,y) => x % y` + +pmod : Int → Int → Int +pmod a b = + if a < 0 then (a + b * ((0 - a / b) + 1)) % b else a % b + +move : Int → Int → Int → Robot → Point +move w h time (MkBot (x,y) (dx,dy)) = + -- no HMul yet + -- let (x',y') = trace "to" $ (x,y) + (time * dx, time * dy) in + let x' = pmod (x + time * dx) w + y' = pmod (y + time * dy) h + in (x', y') + +count : ∀ a. (a → Bool) → List a → Int +count {a} f xs = go xs 0 + where + go : List a → Int → Int + go Nil acc = acc + go (x :: xs) acc = if f x then go xs (acc + 1) else go xs acc + +draw' : Int → Int → SortedMap Point Int → IO Unit +draw' w h pts = go 0 + where + mkLine : Int → Int → SnocList Char → String + mkLine y x acc = if x == w then pack (acc <>> Nil) + else case lookupMap (x,y) pts of + Nothing => mkLine y (x + 1) (acc :< '.') + _ => mkLine y (x + 1) (acc :< '*') + + go : Int → IO Unit + go y = if y == h then pure MkUnit else do + putStrLn $ mkLine y 0 Lin + go (y + 1) + +draw : Int → Int → List Point → IO Unit +draw w h pts = + let m = foldMap _+_ EmptyMap $ map (flip _,_ 1) pts in draw' w h m + + +part2 : Int → Int → List Robot → List Point × Int +part2 w h robots = go 1 + where + heuristic : Point → Bool + heuristic (x,y) = if x < w / 2 then 100 < 2 * x + y else 2 * (x - 50) < y + -- heuristic (x,y) = x == w / 2 + go : Int → List Point × Int + go t = + let pts = map (move w h t) robots + cnt = count heuristic pts + in if cnt > 20 then (pts, t) + else go (t + 1) + +run : String → Int → Int → IO Unit +run fn w h = do + putStrLn fn + text <- readFile fn + let (Right (robots, Nil)) = some probot $ unpack text + | Left msg => putStrLn $ "Parse Error " ++ msg + | Right (robots, rest) => putStrLn $ "stuck at¬" ++ pack rest + let result = map (move w h 100) robots + -- debugLog 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) + 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 + dump robots stuff 1 + where + dump : List Robot → List (Int × Int) → Int → IO Unit + dump robots Nil _ = pure MkUnit + dump robots (((t,cnt) :: xs)) 0 = pure MkUnit + dump robots (((t,cnt) :: xs)) gas = do + printLn t + draw w h $ map (move w h t) robots + printLn "" + dump robots xs (gas - 1) + + quad1 : Point → Bool + quad1 (x,y) = x < w / 2 && y < h / 2 + + quad2 : Point → Bool + quad2 (x,y) = x > w / 2 && y < h / 2 + + quad3 : Point → Bool + quad3 (x,y) = x > w / 2 && y > h / 2 + + quad4 : Point → Bool + quad4 (x,y) = x < w / 2 && y > h / 2 + + heuristic : Point → Bool + heuristic (x,y) = if x < w / 2 then 100 - 2 * x < y else 2 * x - 100 < y + + dist : Point → Int + dist (x,y) = let d = if x < w / 2 then y - (h - 2 * x) else y - (h - 2 * (w - x)) in + if d < 0 then 0 - d else d + + collect : List Robot → Int → List (Int × Int) → List (Int × Int) + collect robots iter acc = + if iter > w * h then acc else + let pts = map (move w h iter) robots in + + -- This heuristic found it, attempting to find an outline of a large tree + -- but the picture looks nothing like that, so I got lucky + -- let cnt = foldl _+_ 0 $ map dist pts in + -- so I'll go with min danger (although it takes 4 * as long) + let q1 = count quad1 pts + q2 = count quad2 pts + q3 = count quad3 pts + q4 = count quad4 pts + cnt = q1 * q2 * q3 * q4 in + collect robots (iter + 1) ((iter,cnt) :: acc) + +main : IO Unit +main = do + -- run "aoc2024/day14/eg.txt" 11 7 + run "aoc2024/day14/input.txt" 101 103 diff --git a/aoc2024/Day6.newt b/aoc2024/Day6.newt index c0bbd38..797cabc 100644 --- a/aoc2024/Day6.newt +++ b/aoc2024/Day6.newt @@ -5,15 +5,6 @@ import Node import Aoc import SortedMap -Point : U -Point = Int × Int - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - Grid : U Grid = SortedMap Point Char diff --git a/aoc2024/Day8.newt b/aoc2024/Day8.newt index 6215b12..415f771 100644 --- a/aoc2024/Day8.newt +++ b/aoc2024/Day8.newt @@ -5,15 +5,6 @@ import Node import Aoc import SortedMap -Point : U -Point = Int × Int - -instance Add Point where - (a,b) + (c,d) = (a + c, b + d) - -instance Sub Point where - (a,b) - (c,d) = (a - c, b - d) - Ant : U Ant = Char × Int × Int @@ -59,12 +50,6 @@ doGroup2 : Int -> List Ant -> List Point doGroup2 m (x :: xs) = join $ doGroup2 m xs :: map (doPair2 m (snd x) ∘ snd) xs doGroup2 m Nil = Nil -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - run : String -> IO Unit run fn = do putStrLn fn diff --git a/aoc2024/Parser.newt b/aoc2024/Parser.newt index 8b73092..9ea8b51 100644 --- a/aoc2024/Parser.newt +++ b/aoc2024/Parser.newt @@ -65,5 +65,11 @@ number = stringToInt ∘ pack <$> some (satisfy isDigit) -- digs <- some (satisfy isDigit) -- pure $ stringToInt $ pack digs +optional : ∀ a. Parser a → Parser (Maybe a) +optional pa = Just <$> pa <|> pure Nothing + ws : Parser Unit ws = many (match ' ') >> pure MkUnit + +token : String → Parser Unit +token str = string str >> ws diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt index 264131d..ae7fea6 100644 --- a/aoc2024/SortedMap.newt +++ b/aoc2024/SortedMap.newt @@ -187,3 +187,9 @@ toList {k} {v} (MapOf smap) = reverse $ go smap Nil go (Node2 t1 k1 t2) acc = go t2 (go t1 acc) go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc toList _ = Nil + +foldMap : ∀ a b. {{Ord a}} {{Eq a}} → (b → b → b) → SortedMap a b → List (a × b) → SortedMap a b +foldMap f m Nil = m +foldMap f m ((a,b) :: xs) = case lookupMap a m of + Nothing => foldMap f (updateMap a b m) xs + Just (_, b') => foldMap f (updateMap a (f b' b) m) xs diff --git a/aoc2024/day14/eg.txt b/aoc2024/day14/eg.txt new file mode 100644 index 0000000..72a324a --- /dev/null +++ b/aoc2024/day14/eg.txt @@ -0,0 +1,12 @@ +p=0,4 v=3,-3 +p=6,3 v=-1,-3 +p=10,3 v=-1,2 +p=2,0 v=2,-1 +p=0,0 v=1,3 +p=3,0 v=-2,-2 +p=7,6 v=-1,-3 +p=3,0 v=-1,-2 +p=9,3 v=2,3 +p=7,3 v=-1,2 +p=2,4 v=2,-3 +p=9,5 v=-3,-3 \ No newline at end of file diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 75facd2..bc63b98 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -675,7 +675,7 @@ tail (x :: xs) = xs -- -infixl 6 _<_ _<=_ +infixl 6 _<_ _<=_ _>_ class Ord a where -- isEq : Eq a _<_ : a → a → Bool @@ -683,6 +683,8 @@ class Ord a where _<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool a <= b = a == b || a < b +_>_ : ∀ a. {{Ord a}} → a → a → Bool +a > b = b < a search : ∀ cl. {{cl}} -> cl search {{x}} = x @@ -743,3 +745,5 @@ instance Show Char where swap : ∀ a b. a × b → b × a swap (a,b) = (b,a) + + diff --git a/playground/samples/aoc2024/Aoc.newt b/playground/samples/aoc2024/Aoc.newt index 61f3831..cac5bec 120000 --- a/playground/samples/aoc2024/Aoc.newt +++ b/playground/samples/aoc2024/Aoc.newt @@ -1 +1 @@ -../../../aoc2023/Aoc.newt \ No newline at end of file +../../../aoc2024/Aoc.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day1.newt b/playground/samples/aoc2024/Day1.newt deleted file mode 100644 index fc4a364..0000000 --- a/playground/samples/aoc2024/Day1.newt +++ /dev/null @@ -1,60 +0,0 @@ -module Day1 - -import Prelude -import Node -import Aoc - -pairUp : List Int -> List (Int × Int) -pairUp (a :: b :: rest) = (a,b) :: pairUp rest -pairUp (a :: rest) = trace "fail" Nil -pairUp Nil = Nil - -dist : (Int × Int) → Int -dist (a,b) = if a < b then b - a else a - b - -part1 : String -> Int -part1 text = - let pairs = pairUp $ join $ map nums $ split text "\n" - left = qsort _<_ $ map fst pairs - right = qsort _<_ $ map snd pairs - dists = map dist $ zip left right - in foldl _+_ 0 dists - - -lookup : ∀ a b. {{Eq a}} → a → List (a × b) → Maybe b -lookup key Nil = Nothing -lookup key ((k,v) :: rest) = if k == key then Just v else lookup key rest - - -coalesce : List Int → Int -> List (Int × Int) -coalesce (a :: b :: rest) cnt = - if a == b then coalesce (b :: rest) (cnt + 1) else (a,cnt) :: coalesce (b :: rest) 1 -coalesce (a :: Nil) cnt = (a,cnt) :: Nil -coalesce Nil cnt = Nil - -cross : List (Int × Int) → List (Int × Int) → Int → Int -cross xs ys acc = - let ((a,cnt) :: xs') = xs | Nil => acc in - let ((b,cnt') :: ys') = ys | Nil => acc in - if a == b then cross xs' ys' (acc + a * cnt * cnt') - else if a < b then cross xs' ys acc - else cross xs ys' acc - -part2 : String → Int -part2 text = - let pairs = pairUp $ join $ map nums $ split text "\n" - left = coalesce (qsort _<_ $ map fst pairs) 1 - right = coalesce (qsort _<_ $ map snd pairs) 1 - in cross left right 0 - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - putStrLn $ "part1 " ++ show (part1 text) - putStrLn $ "part2 " ++ show (part2 text) - -main : IO Unit -main = do - run "aoc2024/day1/eg.txt" - run "aoc2024/day1/input.txt" diff --git a/playground/samples/aoc2024/Day1.newt b/playground/samples/aoc2024/Day1.newt new file mode 120000 index 0000000..984888a --- /dev/null +++ b/playground/samples/aoc2024/Day1.newt @@ -0,0 +1 @@ +../../../aoc2024/Day1.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day10.newt b/playground/samples/aoc2024/Day10.newt new file mode 120000 index 0000000..8b38a66 --- /dev/null +++ b/playground/samples/aoc2024/Day10.newt @@ -0,0 +1 @@ +../../../aoc2024/Day10.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day11.newt b/playground/samples/aoc2024/Day11.newt new file mode 120000 index 0000000..86589a0 --- /dev/null +++ b/playground/samples/aoc2024/Day11.newt @@ -0,0 +1 @@ +../../../aoc2024/Day11.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day11b.newt b/playground/samples/aoc2024/Day11b.newt new file mode 120000 index 0000000..f9c395f --- /dev/null +++ b/playground/samples/aoc2024/Day11b.newt @@ -0,0 +1 @@ +../../../aoc2024/Day11b.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day12.newt b/playground/samples/aoc2024/Day12.newt new file mode 120000 index 0000000..da889f7 --- /dev/null +++ b/playground/samples/aoc2024/Day12.newt @@ -0,0 +1 @@ +../../../aoc2024/Day12.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day13.newt b/playground/samples/aoc2024/Day13.newt new file mode 120000 index 0000000..3dab26b --- /dev/null +++ b/playground/samples/aoc2024/Day13.newt @@ -0,0 +1 @@ +../../../aoc2024/Day13.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day14.newt b/playground/samples/aoc2024/Day14.newt new file mode 120000 index 0000000..1bfd2d0 --- /dev/null +++ b/playground/samples/aoc2024/Day14.newt @@ -0,0 +1 @@ +../../../aoc2024/Day14.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day2.newt b/playground/samples/aoc2024/Day2.newt deleted file mode 100644 index 4c769e9..0000000 --- a/playground/samples/aoc2024/Day2.newt +++ /dev/null @@ -1,51 +0,0 @@ -module Day2 - -import Prelude -import Node -import Aoc - -decr : List Int → Bool -decr (x :: y :: _) = y < x -decr _ = False - -diff : Int → Int → Int -diff x y = if x < y then y - x else x - y - -isSafe : Bool → List Int → Bool -isSafe decr (x :: y :: rest) = - let d = diff x y - good = 0 < d && d < 4 - safe = if x < y then not decr && good else decr && good in - if safe then isSafe decr (y :: rest) else False -isSafe _ _ = True - -check : List Int → Bool -check x = isSafe (decr x) x - -any : ∀ a. (a → Bool) → List a → Bool -any f xs = foldl (_||_) False $ map f xs - -alts : List Int → List (List Int) -alts Nil = Nil -alts (x :: xs) = xs :: map (_::_ x) (alts xs) - --- I want lean's #eval here - -parse : String → List (List Int) -parse text = map nums $ split (trim text) "\n" - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let stuff = parse text - let good = filter check stuff - putStrLn $ "part1 " ++ show (length good) - let good = filter (any check ∘ alts) stuff - putStrLn $ "part2 " ++ show (length good) - -main : IO Unit -main = do - run "aoc2024/day2/eg.txt" - run "aoc2024/day2/input.txt" - diff --git a/playground/samples/aoc2024/Day2.newt b/playground/samples/aoc2024/Day2.newt new file mode 120000 index 0000000..fbe220e --- /dev/null +++ b/playground/samples/aoc2024/Day2.newt @@ -0,0 +1 @@ +../../../aoc2024/Day2.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day3.newt b/playground/samples/aoc2024/Day3.newt deleted file mode 100644 index fd5047b..0000000 --- a/playground/samples/aoc2024/Day3.newt +++ /dev/null @@ -1,121 +0,0 @@ -module Day3 - -import Prelude -import Node -import Aoc - -Parser : U → U -Parser a = List Char → Maybe (a × List Char) - -instance Monad Parser where - pure a = \ cs => Just (a, cs) - bind ma mab = \ cs => ma cs >>= uncurry mab - -instance Alternative Parser where - pa <|> pb = \ cs => case pa cs of - Nothing => pb cs - res => res - -fail : ∀ a. Parser a -fail = \ cs => Nothing - -satisfy : (Char → Bool) → Parser Char -satisfy pred = λ cs => case cs of - Nil => Nothing - (c :: cs) => if pred c then Just (c, cs) else Nothing - -match : Char → Parser Char -match d = satisfy (_==_ d) - -any : Parser Char -any = satisfy (λ _ => True) - -some many : ∀ a. Parser a → Parser (List a) -many p = some p <|> pure Nil -some p = do - v <- p - vs <- many p - pure (v :: vs) - -pnum : Parser Int -pnum = do - chars <- many (satisfy isDigit) - if S (S (S Z)) < length chars then fail - else pure $ stringToInt $ pack chars - -data Inst : U where - Mult : Int → Int → Inst - Do : Inst - Dont : Inst - -mul : Parser Inst -mul = do - match 'm' - match 'u' - match 'l' - match '(' - x <- pnum - match ',' - y <- pnum - match ')' - pure $ Mult x y - -pdo : Parser Inst -pdo = do - match 'd' - match 'o' - match '(' - match ')' - pure Do - -pdont : Parser Inst -pdont = do - match 'd' - match 'o' - match 'n' - match '\'' - match 't' - match '(' - match ')' - pure Dont - -some' many' : ∀ a. Parser a → Parser (List a) -many' p = do - pure MkUnit - some' p <|> (any >> many' p) <|> pure Nil - -some' p = do - v <- p - vs <- many' p - pure (v :: vs) - -inst : Parser Inst -inst = mul <|> pdo <|> pdont - -pfile : Parser (List Inst) -pfile = many' inst - -value : Inst → Int -value (Mult x y) = x * y -value _ = 0 - -part2 : List Inst → Bool → Int → Int -part2 Nil _ acc = acc -part2 (Do :: insts) _ acc = part2 insts True acc -part2 (Dont :: insts) _ acc = part2 insts False acc -part2 (_ :: insts) False acc = part2 insts False acc -part2 (Mult x y :: insts) True acc = part2 insts True (acc + x * y) - -run : String → IO Unit -run fn = do - putStrLn fn - text <- trim <$> readFile fn - let (Just (insts, Nil)) = pfile (unpack text) | _ => putStrLn "parse failed" - let part1 = foldl _+_ 0 $ map value insts - putStrLn $ "part1 " ++ show part1 - putStrLn $ "part2 " ++ show (part2 insts True 0) - -main : IO Unit -main = do - run "aoc2024/day3/eg.txt" - run "aoc2024/day3/input.txt" diff --git a/playground/samples/aoc2024/Day3.newt b/playground/samples/aoc2024/Day3.newt new file mode 120000 index 0000000..6aeebee --- /dev/null +++ b/playground/samples/aoc2024/Day3.newt @@ -0,0 +1 @@ +../../../aoc2024/Day3.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day4.newt b/playground/samples/aoc2024/Day4.newt deleted file mode 100644 index 273d9f9..0000000 --- a/playground/samples/aoc2024/Day4.newt +++ /dev/null @@ -1,76 +0,0 @@ -module Day4 - -import Prelude -import Node -import Aoc - -data Problem : U where - P : Int → String → Problem - -get : Problem → Int → Int → Char -get (P size text) r c = - if r < 0 || size <= r then '.' - else if c < 0 || size <= c then '.' - else sindex text (r * (size + 1) + c) - -check : Problem → Int → Int → Int × Int → Int -check prob r c (dr,dc) = - if (get prob r c) /= 'X' then 0 - else if (get prob (r + dr) (c + dc)) /= 'M' then 0 - else if (get prob (r + 2 * dr) (c + 2 * dc)) /= 'A' then 0 - else if (get prob (r + 3 * dr) (c + 3 * dc)) /= 'S' then 0 - else 1 - -dirs : List (Int × Int) -dirs = tail $ _,_ <$> 0 :: 0 - 1 :: 1 :: Nil <*> 0 :: 0 - 1 :: 1 :: Nil - -part1 : Problem → Int -part1 (P size text) = go 0 0 0 - where - go : Int → Int → Int → Int - go acc r c = - if r == size then acc else - if c == size then go acc (r + 1) 0 else - let acc = foldl _+_ acc $ map (check (P size text) r c) dirs in - go acc r (c + 1) - -pats : List (Char × Char × Char × Char) -pats = ('M', 'M', 'S', 'S') :: - ('S', 'M', 'M', 'S') :: - ('S', 'S', 'M', 'M') :: - ('M', 'S', 'S', 'M') :: - Nil - -check2 : Problem → Int → Int → (Char × Char × Char × Char) → Int -check2 prob r c (w,x,y,z) = - if (get prob r c) /= 'A' then 0 - else if (get prob (r - 1) (c - 1)) /= w then 0 - else if (get prob (r - 1) (c + 1)) /= x then 0 - else if (get prob (r + 1) (c + 1)) /= y then 0 - else if (get prob (r + 1) (c - 1)) /= z then 0 - else 1 - -part2 : Problem → Int -part2 (P size text) = go 0 0 0 - where - go : Int → Int → Int → Int - go acc r c = - if r == size then acc else - if c == size then go acc (r + 1) 0 else - let acc = foldl _+_ acc $ map (check2 (P size text) r c) pats in - go acc r (c + 1) - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let lines = split (trim text) "\n" - -- I'm going to assume it's square for convenience - let size = length lines - printLn $ "part1 " ++ show (part1 $ P (cast size) text) - printLn $ "part2 " ++ show (part2 $ P (cast size) text) - -main : IO Unit -main = do - run "aoc2024/day4/eg.txt" - run "aoc2024/day4/input.txt" diff --git a/playground/samples/aoc2024/Day4.newt b/playground/samples/aoc2024/Day4.newt new file mode 120000 index 0000000..46fd6cf --- /dev/null +++ b/playground/samples/aoc2024/Day4.newt @@ -0,0 +1 @@ +../../../aoc2024/Day4.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day5.newt b/playground/samples/aoc2024/Day5.newt deleted file mode 100644 index 690ea58..0000000 --- a/playground/samples/aoc2024/Day5.newt +++ /dev/null @@ -1,77 +0,0 @@ -module Day5 - -import Prelude -import Node -import Aoc -import SortedMap - -data Prob : U where - MkProb : List (Int × Int) -> List (List Int) → Prob - -parseRule : String → Maybe (Int × Int) -parseRule txt = - let (a :: b :: Nil) = nums' "|" txt | _ => Nothing - in Just (a,b) - -parse : String → Maybe Prob -parse text = do - let (a :: b :: Nil) = split (trim text) "\n\n" | pts => Nothing - rules <- traverse parseRule $ split a "\n" - let updates = map (nums' ",") $ split b "\n" - Just $ MkProb rules updates - -RuleMap : U -RuleMap = SortedMap Int (List Int) - -getDisallowed : Int → RuleMap → List Int -getDisallowed key rmap = fromMaybe Nil (map snd $ lookupMap key rmap) - -mkRuleMap : List (Int × Int) -> RuleMap -mkRuleMap rules = foldl go EmptyMap rules - where - go : RuleMap → Int × Int → RuleMap - go rmap (b,a) = updateMap a (b :: getDisallowed a rmap) rmap - -scan : RuleMap → List Int -> List Int -> Bool -scan rmap interdit Nil = True -scan rmap interdit (x :: xs) = - if elem x interdit then False - else scan rmap (getDisallowed x rmap ++ interdit) xs - -fix : RuleMap → List Int → List Int -fix rmap Nil = Nil -fix rmap (x :: xs) = - let interdit = getDisallowed x rmap in - let (prefix,rest) = partition (flip elem interdit) xs - in case prefix of - Nil => x :: fix rmap rest - ys => fix rmap (ys ++ x :: rest) - -middle : List Int -> Int -middle xs = go xs xs - where - go : List Int → List Int → Int - go (x :: xs) (_ :: _ :: ys) = go xs ys - go (x :: xs) (_ :: ys) = x - go _ _ = 0 - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let (Just prob) = parse text | _ => putStrLn "Parse Error" - let (MkProb rules things) = prob - let rmap = mkRuleMap rules - let good = filter (scan rmap Nil) things - let part1 = foldl _+_ 0 $ map middle good - let bad = filter (not ∘ scan rmap Nil) things - putStrLn $ "part1 " ++ show part1 - let fixed = map (fix rmap) bad - printLn $ length bad - let part2 = foldl _+_ 0 $ map middle fixed - putStrLn $ "part2 " ++ show part2 - -main : IO Unit -main = do - run "aoc2024/day5/eg.txt" - run "aoc2024/day5/input.txt" diff --git a/playground/samples/aoc2024/Day5.newt b/playground/samples/aoc2024/Day5.newt new file mode 120000 index 0000000..609fcbf --- /dev/null +++ b/playground/samples/aoc2024/Day5.newt @@ -0,0 +1 @@ +../../../aoc2024/Day5.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day6.newt b/playground/samples/aoc2024/Day6.newt deleted file mode 100644 index c0bbd38..0000000 --- a/playground/samples/aoc2024/Day6.newt +++ /dev/null @@ -1,132 +0,0 @@ -module Day6 - -import Prelude -import Node -import Aoc -import SortedMap - -Point : U -Point = Int × Int - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - -Grid : U -Grid = SortedMap Point Char - -loadData : String → Grid -loadData text = go (unpack text) 0 0 EmptyMap - where - go : List Char → Int → Int → SortedMap Point Char → SortedMap Point Char - go Nil r c map = map - go ('\n' :: cs) r c map = go cs (r + 1) 0 map - go (x :: xs) r c map = go xs r (c + 1) $ updateMap (r,c) x map - -data Dir : U where North East South West : Dir - -instance Show Dir where - show North = "N" - show East = "E" - show South = "S" - show West = "W" - -instance Ord Dir where - a < b = show a < show b - -instance Eq (Point × Dir) where - (a,b) == (c,d) = a == c && show b == show d - -instance Ord (Point × Dir) where - (a,b) < (c,d) = - if a < c then True - else if a /= c then False - else b < d - -Done : U -Done = SortedMap (Point × Dir) Unit - -turn : Dir → Dir -turn North = East -turn East = South -turn South = West -turn West = North - -instance Cast Dir Char where - cast North = '^' - cast East = '>' - cast South = 'v' - cast West = '<' - -step : Dir → Point → Point -step North (r, c) = (r - 1, c) -step East (r, c) = (r, c + 1) -step South (r, c) = (r + 1, c) -step West (r, c) = (r, c - 1) - -bad : Point → Bool -bad (x,y) = x < 0 || y < 0 - --- third is -walk : Dir → Point → Grid → Grid -walk dir pos grid = - let grid = updateMap pos 'X' grid in - let pos' = step dir pos in - case lookupMap pos' grid of - Just (_, '#') => walk (turn dir) pos grid - Nothing => grid - _ => walk dir pos' grid - -checkLoop : Grid → Done → Dir → Point → Bool -checkLoop grid done dir pos = - let (Nothing) = lookupMap (pos,dir) done | _ => True in - let done = updateMap (pos, dir) MkUnit done - pos' = step dir pos - in case lookupMap pos' grid of - Nothing => False - Just (_, '#') => checkLoop grid done (turn dir) pos - Just _ => checkLoop grid done dir pos' - -part2 : Dir → Point → Grid → Done → List Point → List Point -part2 dir pos grid done sol = - let done = updateMap (pos, dir) MkUnit done - grid = updateMap pos 'X' grid - turnDir = turn dir - turnPos = step turnDir pos - pos' = step dir pos in - case lookupMap pos' grid of - Nothing => sol - Just (_, '#') => part2 (turn dir) pos grid done sol - Just (_, 'X') => part2 dir pos' grid done sol - Just (_, '.') => if checkLoop (updateMap pos' '#' grid) done turnDir pos - then part2 dir pos' grid done (pos' :: sol) - else part2 dir pos' grid done sol - Just x => part2 (trace ("WAT " ++ debugStr x) dir) pos' grid done sol - -lookupV : ∀ a. Char → List (a × Char) → Maybe a -lookupV _ Nil = Nothing -lookupV needle ((k,v) :: rest) = - if v == needle then Just k else lookupV needle rest - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let grid = loadData text - let (Just pos) = lookupV '^' (toList grid) | _ => putStrLn "no guard" - let grid' = walk North pos grid - let xs = filter (\ x => 'X' == snd x) $ toList grid' - let part1 = length xs - putStrLn $ "part1 " ++ show part1 - - let cands = part2 North pos grid EmptyMap Nil - -- debugLog $ length cands -- turns out nub isn't needed for these cases, but we'll leave it in - putStrLn $ "part2 " ++ show (length $ ordNub cands) - printLn $ length $ toList grid - -main : IO Unit -main = do - run "aoc2024/day6/eg.txt" - run "aoc2024/day6/input.txt" diff --git a/playground/samples/aoc2024/Day6.newt b/playground/samples/aoc2024/Day6.newt new file mode 120000 index 0000000..aab08c0 --- /dev/null +++ b/playground/samples/aoc2024/Day6.newt @@ -0,0 +1 @@ +../../../aoc2024/Day6.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day7.newt b/playground/samples/aoc2024/Day7.newt deleted file mode 100644 index 95609a6..0000000 --- a/playground/samples/aoc2024/Day7.newt +++ /dev/null @@ -1,58 +0,0 @@ -module Day7 - -import Prelude -import Node -import Aoc - -Prob : U -Prob = Int × List Int - -cases : Int → Int → List Int → Bool -cases goal acc Nil = goal == acc -cases goal acc (x :: xs) = - if goal < acc then False - else if cases goal (x + acc) xs then True - else cases goal (x * acc) xs - -part1 : Prob → Bool -part1 (goal, x :: xs) = cases goal x xs -part1 _ = False - -cat : Int → Int → Int -cat x y = stringToInt $ show x ++ show y - -cases2 : Int → Int → List Int → Bool -cases2 goal acc Nil = goal == acc -cases2 goal acc (x :: xs) = - if goal < acc then False - else if cases2 goal (x + acc) xs then True - else if cases2 goal (x * acc) xs then True - else cases2 goal (cat acc x) xs - -part2 : Prob → Bool -part2 (goal, x :: xs) = cases2 goal x xs -part2 _ = False - -parse : String -> Maybe (List Prob) -parse text = do - traverse parseLine $ split (trim text) "\n" - where - parseLine : String → Maybe Prob - parseLine line = do - let (a :: b :: Nil) = split line ": " | _ => Nothing - Just (stringToInt a , nums b) - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let (Just probs) = parse text | _ => putStrLn "parse error" - let p1 = foldl _+_ 0 $ map fst $ filter part1 probs - putStrLn $ "part1 " ++ show p1 - let p2 = foldl _+_ 0 $ map fst $ filter part2 probs - putStrLn $ "part2 " ++ show p2 - -main : IO Unit -main = do - run "aoc2024/day7/eg.txt" - run "aoc2024/day7/input.txt" diff --git a/playground/samples/aoc2024/Day7.newt b/playground/samples/aoc2024/Day7.newt new file mode 120000 index 0000000..f4ec895 --- /dev/null +++ b/playground/samples/aoc2024/Day7.newt @@ -0,0 +1 @@ +../../../aoc2024/Day7.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day8.newt b/playground/samples/aoc2024/Day8.newt deleted file mode 100644 index 6215b12..0000000 --- a/playground/samples/aoc2024/Day8.newt +++ /dev/null @@ -1,95 +0,0 @@ -module Day8 - -import Prelude -import Node -import Aoc -import SortedMap - -Point : U -Point = Int × Int - -instance Add Point where - (a,b) + (c,d) = (a + c, b + d) - -instance Sub Point where - (a,b) - (c,d) = (a - c, b - d) - -Ant : U -Ant = Char × Int × Int - --- This should be a utility... -parse : String → List Ant -parse text = go 0 0 (unpack text) Nil - where - -- might as well be tail recursive - go : Int → Int → List Char → List Ant → List Ant - go row col Nil ants = ants - go row col ('\n' :: cs) ants = go (row + 1) 0 cs ants - go row col (c :: cs) ants = go row (col + 1) cs ((c,row,col) :: ants) - -doPair : Point → Point → List Point -doPair x y = let d = y - x in y + d :: x - d :: Nil - -doGroup : List Ant -> List Point -doGroup (x :: xs) = join $ doGroup xs :: map (doPair (snd x) ∘ snd) xs -doGroup Nil = Nil - -group : List Ant → (List Ant) → List (List Ant) -group (a :: as) Nil = group as (a :: Nil) -group (a :: as) (b :: bs) = - if fst a == fst b - then group as (a :: b :: bs) - else (b :: bs) :: group as (a :: Nil) -group Nil bs = bs :: Nil - -max : Int → Int → Int -max a b = if a < b then b else a - -check : Int → Point → Bool -check mr (r,c) = 0 <= r && 0 <= c && r <= mr && c <= mr - - -doPair2 : Int -> Point → Point → List Point -doPair2 m x y = go x (y - x) ++ go y (x - y) - where - go : Point -> Point -> List Point - go pt d = if check m pt then pt :: go (pt + d) d else Nil - -doGroup2 : Int -> List Ant -> List Point -doGroup2 m (x :: xs) = join $ doGroup2 m xs :: map (doPair2 m (snd x) ∘ snd) xs -doGroup2 m Nil = Nil - -instance Ord Point where - (a,b) < (c,d) = a < c || a == c && b < d - -instance Eq Point where - (a,b) == (c,d) = a == c && b == d - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let points = parse text - let maxrow = trace "maxrow" $ foldl max 0 $ map (fst ∘ snd) points - let maxcol = trace "maxcol" $ foldl max 0 $ map (snd ∘ snd) points - let ants = filter (\ pt => fst pt /= '.') points - let ants = qsort (\ x y => fst x < fst y) ants - let groups = group ants Nil - let stuff = join $ map doGroup groups - let nodes = filter (check maxrow) stuff - - let part1 = length $ ordNub nodes - putStrLn $ "part1 " ++ show part1 - - let stuff2 = join $ map (doGroup2 maxrow) groups - let part2 = length $ ordNub stuff2 - putStrLn $ "part2 " ++ show part2 - - - - - -main : IO Unit -main = do - run "aoc2024/day8/eg.txt" - run "aoc2024/day8/input.txt" diff --git a/playground/samples/aoc2024/Day8.newt b/playground/samples/aoc2024/Day8.newt new file mode 120000 index 0000000..b6520de --- /dev/null +++ b/playground/samples/aoc2024/Day8.newt @@ -0,0 +1 @@ +../../../aoc2024/Day8.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Day9.newt b/playground/samples/aoc2024/Day9.newt deleted file mode 100644 index fd05c3b..0000000 --- a/playground/samples/aoc2024/Day9.newt +++ /dev/null @@ -1,127 +0,0 @@ -module Day9 - -import Prelude -import Node -import Aoc -import SortedMap - -File : U -File = Int × Int × Int - -parse : String -> List File -parse cs = go 0 (unpack $ trim cs) Nil - where - go : Int -> List Char -> List File -> List File - go id (a :: b :: cs) acc = - go (id + 1) cs ((id, (ord a - 48), (ord b - 48)) :: acc) - go id (a :: cs) acc = go (id + 1) cs ((id, (ord a - 48), 0) :: acc) - go _ _ acc = reverse acc - -part1 : List File -> Int -part1 fs = go 0 0 fs $ reverse fs - where - go : Int -> Int -> List File -> List File -> Int - go pos csum Nil bwd = ? - go pos csum fwd Nil = csum - go pos csum ((id, 0, 0) :: fwd) bwd = go pos csum fwd bwd - go pos csum fwd ((id, 0, _) :: bwd) = go pos csum fwd bwd - go pos csum ((id, 0, k) :: fs) ((id', l, g) :: bwd) = - if id == id' then csum - else go (pos + 1) (csum + pos * id') ((id, 0, k - 1) :: fs) ((id', l - 1, g) :: bwd) - go pos csum ((id, k, gap) :: fs) ((id', l, g) :: rest) = - if id == id' - then go (pos + 1) (csum + pos * id) ((id, k, gap) :: fs) ((id', l - 1, g) :: Nil) - else go (pos + 1) (csum + pos * id) ((id, k - 1, gap) :: fs) ((id', l, g) :: rest) - -min : Int → Int → Int -min a b = if a < b then a else b - --- I really do want records... -Node : U -Node = Int × Int × File - -FileSystem : U -FileSystem = SortedMap Int Node - -mkfs : List File → FileSystem -mkfs = foldl go EmptyMap - where - go : FileSystem → File → FileSystem - go fs (id,l,g) = updateMap id (id - 1, id + 1, id, l, g) fs - -removeNode : Int → FileSystem → FileSystem -removeNode ix fs = - -- yeah, I want records.. - let (Just (_ ,p1,n1, i1, l1, g1)) = lookupMap ix fs | _ => fs in - let (Just (_, p2, _, i2, l2, g2)) = lookupMap p1 fs | _ => fs in - let fs = updateMap p1 (p2, n1, i2, l2, g2 + l1 + g1) fs in - let (Just (_, _, n2, i2, l2, g2)) = lookupMap n1 fs | _ => fs in - updateMap n1 (p1, n2, i2, l2, g2) fs - -insertNode : Int → File → FileSystem → FileSystem -insertNode ix (i,l,g) fs = - -- previous - let (Just (_, p1, n1, i1, l1, g1)) = lookupMap ix fs | _ => fs in - let fs = updateMap ix (p1,i,i1,l1,0) fs in - let fs = updateMap i (ix, n1, i,l,g1 - l) fs in - let (Just (_, p2, n2, i2, l2, g2)) = lookupMap n1 fs | _ => fs in - updateMap n1 (i, n2, i2, l2, g2) fs - -defrag : FileSystem → Int -> Int → Int → FileSystem -defrag fs start end limit = - case lookupMap end fs of - Nothing => fs - Just (k,(p,n,id,l,g)) => - -- our only optimization... - if limit <= l then defrag fs start p limit else - case search l start end of - Nothing => defrag fs start p (min l limit) - Just (id',l',g') => - defrag (insertNode id' (id,l,g) $ removeNode end fs) start p limit - where - search : Int → Int → Int -> Maybe File - search size pos end = - if pos == end then Nothing else - case lookupMap pos fs of - Nothing => Nothing - Just (_,(p,n,id,l,g)) => - if size <= g then Just (id,l,g) - else search size n end - -check : FileSystem → Int -check fs = go 0 0 $ files 0 Lin - where - files : Int → SnocList File → List File - files start acc = case lookupMap start fs of - Nothing => acc <>> Nil - Just (_, _, n, f) => files n (acc :< f) - - go : Int → Int → List File → Int - go pos csum Nil = csum - go pos csum ((id,l,g) :: rest) = - if l == 0 then go (pos + g) csum rest - else go (pos + 1) (csum + pos * id) ((id, l - 1, g) :: rest) - -part2 : List File → Int -part2 files = - let fs = mkfs files - end = cast (length files) - 1 - fs' = defrag fs 0 end end - in check fs' - -run : String -> IO Unit -run fn = do - putStrLn fn - text <- readFile fn - let files = parse $ trim text - putStrLn $ show (length files) ++ " files" - let p1 = part1 files - putStrLn $ "part1 " ++ show p1 - let p2 = part2 files - putStrLn $ "part2 " ++ show p2 - pure MkUnit - -main : IO Unit -main = do - run "aoc2024/day9/eg.txt" - run "aoc2024/day9/input.txt" diff --git a/playground/samples/aoc2024/Day9.newt b/playground/samples/aoc2024/Day9.newt new file mode 120000 index 0000000..0563fc0 --- /dev/null +++ b/playground/samples/aoc2024/Day9.newt @@ -0,0 +1 @@ +../../../aoc2024/Day9.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/DayXX.newt b/playground/samples/aoc2024/DayXX.newt new file mode 120000 index 0000000..2837f25 --- /dev/null +++ b/playground/samples/aoc2024/DayXX.newt @@ -0,0 +1 @@ +../../../aoc2024/DayXX.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Node.newt b/playground/samples/aoc2024/Node.newt index f14580c..1e033da 120000 --- a/playground/samples/aoc2024/Node.newt +++ b/playground/samples/aoc2024/Node.newt @@ -1 +1 @@ -../../../aoc2023/Node.newt \ No newline at end of file +../../../aoc2024/Node.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Parser.newt b/playground/samples/aoc2024/Parser.newt new file mode 120000 index 0000000..33e3852 --- /dev/null +++ b/playground/samples/aoc2024/Parser.newt @@ -0,0 +1 @@ +../../../aoc2024/Parser.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/Prelude.newt b/playground/samples/aoc2024/Prelude.newt index 2f6704c..2fa97af 120000 --- a/playground/samples/aoc2024/Prelude.newt +++ b/playground/samples/aoc2024/Prelude.newt @@ -1 +1 @@ -../../../newt/Prelude.newt \ No newline at end of file +../../../aoc2024/Prelude.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/SortedMap.newt b/playground/samples/aoc2024/SortedMap.newt deleted file mode 100644 index f661b08..0000000 --- a/playground/samples/aoc2024/SortedMap.newt +++ /dev/null @@ -1,67 +0,0 @@ -module SortedMap - -import Prelude - -data T23 : Nat -> U -> U -> U where - Leaf : ∀ k v. k -> v -> T23 Z k v - Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v - Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v - -lookupT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> T23 h k v -> Maybe (k × v) -lookupT23 key (Leaf k v)= if k == key then Just (k,v) else Nothing -lookupT23 key (Node2 t1 k1 t2) = - if key <= k1 then lookupT23 key t1 else lookupT23 key t2 -lookupT23 key (Node3 t1 k1 t2 k2 t3) = - if key <= k1 then lookupT23 key t1 - else if key <= k2 then lookupT23 key t2 - else lookupT23 key t3 - -insertT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v) -insertT23 key value (Leaf k v) = - if key == k then Left (Leaf key value) - else if key <= k then Right (Leaf key value, key, Leaf k v) - else Right (Leaf k v, k, Leaf key value) -insertT23 key value (Node2 t1 k1 t2) = - if key <= k1 then - case insertT23 key value t1 of - Left t1' => Left (Node2 t1' k1 t2) - Right (a,b,c) => Left (Node3 a b c k1 t2) - else case insertT23 key value t2 of - Left t2' => Left (Node2 t1 k1 t2') - Right (a,b,c) => Left (Node3 t1 k1 a b c) -insertT23 key value (Node3 t1 k1 t2 k2 t3) = - if key <= k1 then - case insertT23 key value t1 of - Left t1' => Left (Node3 t1' k1 t2 k2 t3) - Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3) - else if key <= k2 then - case insertT23 key value t2 of - Left t2' => Left (Node3 t1 k1 t2' k2 t3) - Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3) - else - case insertT23 key value t3 of - Left t3' => Left (Node3 t1 k1 t2 k2 t3') - Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c) - -data SortedMap : U -> U -> U where - EmptyMap : ∀ k v. SortedMap k v - MapOf : ∀ k v h. T23 h k v -> SortedMap k v - -lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v) -lookupMap k EmptyMap = Nothing -lookupMap k (MapOf map) = lookupT23 k map - -updateMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> v -> SortedMap k v -> SortedMap k v -updateMap k v EmptyMap = MapOf $ Leaf k v -updateMap k v (MapOf map) = case insertT23 k v map of - Left map' => MapOf map' - Right (a, b, c) => MapOf (Node2 a b c) - -toList : ∀ k v. SortedMap k v → List (k × v) -toList {k} {v} (MapOf smap) = reverse $ go smap Nil - where - go : ∀ h. T23 h k v → List (k × v) → List (k × v) - go (Leaf k v) acc = (k, v) :: acc - go (Node2 t1 k1 t2) acc = go t2 (go t1 acc) - go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc -toList _ = Nil diff --git a/playground/samples/aoc2024/SortedMap.newt b/playground/samples/aoc2024/SortedMap.newt new file mode 120000 index 0000000..9cea5d0 --- /dev/null +++ b/playground/samples/aoc2024/SortedMap.newt @@ -0,0 +1 @@ +../../../aoc2024/SortedMap.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/day1 b/playground/samples/aoc2024/day1 new file mode 120000 index 0000000..91e1bf3 --- /dev/null +++ b/playground/samples/aoc2024/day1 @@ -0,0 +1 @@ +../../../aoc2024/day1 \ No newline at end of file diff --git a/playground/samples/aoc2024/day1/eg.txt b/playground/samples/aoc2024/day1/eg.txt deleted file mode 100644 index dfca0b1..0000000 --- a/playground/samples/aoc2024/day1/eg.txt +++ /dev/null @@ -1,6 +0,0 @@ -3 4 -4 3 -2 5 -1 3 -3 9 -3 3 \ No newline at end of file diff --git a/playground/samples/aoc2024/day10 b/playground/samples/aoc2024/day10 new file mode 120000 index 0000000..26a37c8 --- /dev/null +++ b/playground/samples/aoc2024/day10 @@ -0,0 +1 @@ +../../../aoc2024/day10 \ No newline at end of file diff --git a/playground/samples/aoc2024/day11 b/playground/samples/aoc2024/day11 new file mode 120000 index 0000000..aee1604 --- /dev/null +++ b/playground/samples/aoc2024/day11 @@ -0,0 +1 @@ +../../../aoc2024/day11 \ No newline at end of file diff --git a/playground/samples/aoc2024/day12 b/playground/samples/aoc2024/day12 new file mode 120000 index 0000000..6cf3270 --- /dev/null +++ b/playground/samples/aoc2024/day12 @@ -0,0 +1 @@ +../../../aoc2024/day12 \ No newline at end of file diff --git a/playground/samples/aoc2024/day13 b/playground/samples/aoc2024/day13 new file mode 120000 index 0000000..b033837 --- /dev/null +++ b/playground/samples/aoc2024/day13 @@ -0,0 +1 @@ +../../../aoc2024/day13 \ No newline at end of file diff --git a/playground/samples/aoc2024/day14 b/playground/samples/aoc2024/day14 new file mode 120000 index 0000000..9c0aceb --- /dev/null +++ b/playground/samples/aoc2024/day14 @@ -0,0 +1 @@ +../../../aoc2024/day14 \ No newline at end of file diff --git a/playground/samples/aoc2024/day2 b/playground/samples/aoc2024/day2 new file mode 120000 index 0000000..aae6369 --- /dev/null +++ b/playground/samples/aoc2024/day2 @@ -0,0 +1 @@ +../../../aoc2024/day2 \ No newline at end of file diff --git a/playground/samples/aoc2024/day2/eg.txt b/playground/samples/aoc2024/day2/eg.txt deleted file mode 100644 index b49c10d..0000000 --- a/playground/samples/aoc2024/day2/eg.txt +++ /dev/null @@ -1,6 +0,0 @@ -7 6 4 2 1 -1 2 7 8 9 -9 7 6 2 1 -1 3 2 4 5 -8 6 4 4 1 -1 3 6 7 9 diff --git a/playground/samples/aoc2024/day3 b/playground/samples/aoc2024/day3 new file mode 120000 index 0000000..f693f06 --- /dev/null +++ b/playground/samples/aoc2024/day3 @@ -0,0 +1 @@ +../../../aoc2024/day3 \ No newline at end of file diff --git a/playground/samples/aoc2024/day3/eg.txt b/playground/samples/aoc2024/day3/eg.txt deleted file mode 100644 index f274bda..0000000 --- a/playground/samples/aoc2024/day3/eg.txt +++ /dev/null @@ -1 +0,0 @@ -xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5)) diff --git a/playground/samples/aoc2024/day4 b/playground/samples/aoc2024/day4 new file mode 120000 index 0000000..5ad8175 --- /dev/null +++ b/playground/samples/aoc2024/day4 @@ -0,0 +1 @@ +../../../aoc2024/day4 \ No newline at end of file diff --git a/playground/samples/aoc2024/day4/eg.txt b/playground/samples/aoc2024/day4/eg.txt deleted file mode 100644 index 32be4b8..0000000 --- a/playground/samples/aoc2024/day4/eg.txt +++ /dev/null @@ -1,11 +0,0 @@ -MMMSXXMASM -MSAMXMSMSA -AMXSXMAAMM -MSAMASMSMX -XMASAMXAMM -XXAMMXXAMA -SMSMSASXSS -SAXAMASAAA -MAMMMXMMMM -MXMXAXMASX - diff --git a/playground/samples/aoc2024/day5 b/playground/samples/aoc2024/day5 new file mode 120000 index 0000000..8957624 --- /dev/null +++ b/playground/samples/aoc2024/day5 @@ -0,0 +1 @@ +../../../aoc2024/day5 \ No newline at end of file diff --git a/playground/samples/aoc2024/day5/eg.txt b/playground/samples/aoc2024/day5/eg.txt deleted file mode 100644 index 9d146d6..0000000 --- a/playground/samples/aoc2024/day5/eg.txt +++ /dev/null @@ -1,28 +0,0 @@ -47|53 -97|13 -97|61 -97|47 -75|29 -61|13 -75|53 -29|13 -97|29 -53|29 -61|53 -97|53 -61|29 -47|13 -75|47 -97|75 -47|61 -75|61 -47|29 -75|13 -53|13 - -75,47,61,53,29 -97,61,53,29,13 -75,29,13 -75,97,47,61,53 -61,13,29 -97,13,75,29,47 diff --git a/playground/samples/aoc2024/day6 b/playground/samples/aoc2024/day6 new file mode 120000 index 0000000..0c90d86 --- /dev/null +++ b/playground/samples/aoc2024/day6 @@ -0,0 +1 @@ +../../../aoc2024/day6 \ No newline at end of file diff --git a/playground/samples/aoc2024/day6/eg.txt b/playground/samples/aoc2024/day6/eg.txt deleted file mode 100644 index fe5e49f..0000000 --- a/playground/samples/aoc2024/day6/eg.txt +++ /dev/null @@ -1,11 +0,0 @@ -....#..... -.........# -.......... -..#....... -.......#.. -.......... -.#..^..... -........#. -#......... -......#... - diff --git a/playground/samples/aoc2024/day7 b/playground/samples/aoc2024/day7 new file mode 120000 index 0000000..882e750 --- /dev/null +++ b/playground/samples/aoc2024/day7 @@ -0,0 +1 @@ +../../../aoc2024/day7 \ No newline at end of file diff --git a/playground/samples/aoc2024/day7/eg.txt b/playground/samples/aoc2024/day7/eg.txt deleted file mode 100644 index fc6e099..0000000 --- a/playground/samples/aoc2024/day7/eg.txt +++ /dev/null @@ -1,9 +0,0 @@ -190: 10 19 -3267: 81 40 27 -83: 17 5 -156: 15 6 -7290: 6 8 6 15 -161011: 16 10 13 -192: 17 8 14 -21037: 9 7 18 13 -292: 11 6 16 20 diff --git a/playground/samples/aoc2024/day8 b/playground/samples/aoc2024/day8 new file mode 120000 index 0000000..dce1280 --- /dev/null +++ b/playground/samples/aoc2024/day8 @@ -0,0 +1 @@ +../../../aoc2024/day8 \ No newline at end of file diff --git a/playground/samples/aoc2024/day8/day1/eg.txt b/playground/samples/aoc2024/day8/day1/eg.txt deleted file mode 100644 index dfca0b1..0000000 --- a/playground/samples/aoc2024/day8/day1/eg.txt +++ /dev/null @@ -1,6 +0,0 @@ -3 4 -4 3 -2 5 -1 3 -3 9 -3 3 \ No newline at end of file diff --git a/playground/samples/aoc2024/day8/day2/eg.txt b/playground/samples/aoc2024/day8/day2/eg.txt deleted file mode 100644 index b49c10d..0000000 --- a/playground/samples/aoc2024/day8/day2/eg.txt +++ /dev/null @@ -1,6 +0,0 @@ -7 6 4 2 1 -1 2 7 8 9 -9 7 6 2 1 -1 3 2 4 5 -8 6 4 4 1 -1 3 6 7 9 diff --git a/playground/samples/aoc2024/day8/day3/eg.txt b/playground/samples/aoc2024/day8/day3/eg.txt deleted file mode 100644 index f274bda..0000000 --- a/playground/samples/aoc2024/day8/day3/eg.txt +++ /dev/null @@ -1 +0,0 @@ -xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5)) diff --git a/playground/samples/aoc2024/day8/day4/eg.txt b/playground/samples/aoc2024/day8/day4/eg.txt deleted file mode 100644 index 32be4b8..0000000 --- a/playground/samples/aoc2024/day8/day4/eg.txt +++ /dev/null @@ -1,11 +0,0 @@ -MMMSXXMASM -MSAMXMSMSA -AMXSXMAAMM -MSAMASMSMX -XMASAMXAMM -XXAMMXXAMA -SMSMSASXSS -SAXAMASAAA -MAMMMXMMMM -MXMXAXMASX - diff --git a/playground/samples/aoc2024/day8/day5/eg.txt b/playground/samples/aoc2024/day8/day5/eg.txt deleted file mode 100644 index 9d146d6..0000000 --- a/playground/samples/aoc2024/day8/day5/eg.txt +++ /dev/null @@ -1,28 +0,0 @@ -47|53 -97|13 -97|61 -97|47 -75|29 -61|13 -75|53 -29|13 -97|29 -53|29 -61|53 -97|53 -61|29 -47|13 -75|47 -97|75 -47|61 -75|61 -47|29 -75|13 -53|13 - -75,47,61,53,29 -97,61,53,29,13 -75,29,13 -75,97,47,61,53 -61,13,29 -97,13,75,29,47 diff --git a/playground/samples/aoc2024/day8/day6/eg.txt b/playground/samples/aoc2024/day8/day6/eg.txt deleted file mode 100644 index fe5e49f..0000000 --- a/playground/samples/aoc2024/day8/day6/eg.txt +++ /dev/null @@ -1,11 +0,0 @@ -....#..... -.........# -.......... -..#....... -.......#.. -.......... -.#..^..... -........#. -#......... -......#... - diff --git a/playground/samples/aoc2024/day8/day7/eg.txt b/playground/samples/aoc2024/day8/day7/eg.txt deleted file mode 100644 index fc6e099..0000000 --- a/playground/samples/aoc2024/day8/day7/eg.txt +++ /dev/null @@ -1,9 +0,0 @@ -190: 10 19 -3267: 81 40 27 -83: 17 5 -156: 15 6 -7290: 6 8 6 15 -161011: 16 10 13 -192: 17 8 14 -21037: 9 7 18 13 -292: 11 6 16 20 diff --git a/playground/samples/aoc2024/day8/eg.txt b/playground/samples/aoc2024/day8/eg.txt deleted file mode 100644 index 78a1e91..0000000 --- a/playground/samples/aoc2024/day8/eg.txt +++ /dev/null @@ -1,12 +0,0 @@ -............ -........0... -.....0...... -.......0.... -....0....... -......A..... -............ -............ -........A... -.........A.. -............ -............ diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 27a3dd3..bc33de0 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -232,13 +232,13 @@ processDecl (Def fc nm clauses) = do -- Day1.newt is a test case -- tm' <- nf [] tm tm' <- zonk top 0 [] tm - putStrLn "NF\n\{render 80 $ pprint[] tm'}" + when top.verbose $ putStrLn "NF\n\{render 80 $ pprint[] tm'}" -- TODO we want to keep both versions, but this is checking in addition to erasing -- currently CompileExp is also doing erasure. -- TODO we need erasure info on the lambdas or to fake up an appropriate environment -- and erase inside. Currently the checking is imprecise tm'' <- erase [] tm' [] - putStrLn "ERASED\n\{render 80 $ pprint[] tm'}" + when top.verbose $ putStrLn "ERASED\n\{render 80 $ pprint[] tm'}" debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}" updateDef nm fc ty (Fn tm') -- logMetas mstart @@ -347,10 +347,10 @@ processDecl (Instance instfc ty decls) = do let ty' = foldr (\(MkBind fc nm' icit rig ty'), acc => Pi fc nm' icit rig ty' acc) ty tele let nm' = "\{instname},\{nm}" -- we're working with a Tm, so we define directly instead of processDecl - setDef nm' fc ty' Axiom let Just (Def fc name xs) = find (\case (Def y name xs) => name == nm; _ => False) decls | _ => error instfc "no definition for \{nm}" + setDef nm' fc ty' Axiom let decl = (Def fc nm' xs) putStrLn "***" putStrLn "«\{nm'}» : \{pprint [] ty'}" @@ -358,7 +358,8 @@ processDecl (Instance instfc ty decls) = do pure $ Just decl _ => pure Nothing -- This needs to be declared before processing the defs, but the defs need to be - -- declared before this + -- declared before this - side effect is that a duplicate def is noted at the first + -- member processDecl sigDecl for_ (mapMaybe id defs) $ \decl => do -- debug because already printed above, but nice to have it near processing