diff --git a/aoc2024/Day17.newt b/aoc2024/Day17.newt new file mode 100644 index 0000000..15a7b82 --- /dev/null +++ b/aoc2024/Day17.newt @@ -0,0 +1,141 @@ +module Day17 + +import Prelude +import Node +import Aoc +import Parser + +ptype BigInt + +pfunc itobi : Int → BigInt := `(x) => BigInt(x)` +pfunc bitoi : BigInt → Int := `(x) => Number(x)` +pfunc addbi : BigInt → BigInt → BigInt := `(a,b) => a + b` +pfunc subbi : BigInt → BigInt → BigInt := `(a,b) => a - b` +pfunc mulbi : BigInt → BigInt → BigInt := `(a,b) => a * b` +pfunc divbi : BigInt → BigInt → BigInt := `(a,b) => a / b` + +instance Mul BigInt where a * b = mulbi a b +instance Div BigInt where a / b = divbi a b +instance Add BigInt where a + b = addbi a b +instance Sub BigInt where a - b = subbi a b +instance Cast Int BigInt where cast x = itobi x +instance Eq BigInt where a == b = jsEq a b +instance Show BigInt where show = jsShow +instance Ord BigInt where a < b = jsLT a b + +data Machine : U where + M : BigInt → BigInt → BigInt → List Int → Int → SnocList Int → Machine + +preg : Parser BigInt +preg = do + token "Register" + any + token ":" + n <- number + match '\n' + pure $ itobi n + +pprog : Parser (List Int) +pprog = do + token "Program:" + n <- number + ns <- many $ match ',' >> number + many $ match '\n' + pure $ n :: ns + +pmachine : Parser Machine +pmachine = do + a <- preg + b <- preg + c <- preg + many $ match '\n' + prog <- pprog + pure $ M a b c prog 0 Lin + +infixl 7 _**_ _|_ _^_ _%_ _>>>_ +pfunc _**_ : Int → Int → Int := `(x,y) => x ** y` +pfunc _>>>_ : BigInt → BigInt → BigInt := `(x,y) => x >> y` +pfunc _%_ : BigInt → BigInt → BigInt := `(x,y) => x % y` +pfunc bxor : BigInt → BigInt → BigInt := `(x,y) => x ^ y` + +step : Machine -> Machine +step mach@(M a b c mem ip out) = + let ip' = cast ip in + let (Just ins) = getAt ip' mem | _ => mach in + let (Just op) = getAt (S ip') mem | _ => mach in + case ins of + 0 => let a = a >>> combo op in step (M a b c mem (ip + 2) out) + 1 => let b = bxor b (itobi op) in step (M a b c mem (ip + 2) out) + 2 => let b = combo op % itobi 8 in step (M a b c mem (ip + 2) out) + 3 => if a == itobi 0 then step (M a b c mem (ip + 2) out) else step (M a b c mem op out) + 4 => let b = bxor b c in step (M a b c mem (ip + 2) out) + 5 => let o = combo op % itobi 8 in step (M a b c mem (ip + 2) (out :< bitoi o)) + 6 => let b = a >>> combo op in step (M a b c mem (ip + 2) out) + 7 => let c = a >>> combo op in step (M a b c mem (ip + 2) out) + _ => ? + where + combo : Int → BigInt + combo 4 = a + combo 5 = b + combo 6 = c + combo n = itobi n + +find : ∀ a. (a → Bool) → List a → Maybe a +find f Nil = Nothing +find f (x :: xs) = if f x then Just x else find f xs + +Cand : U +Cand = BigInt × SnocList Int × List Int + +part2 : Machine -> Maybe BigInt +part2 mach@(M a b c mem ip out) = go ((itobi 0,(Lin <>< mem), Nil) :: Nil) + where + cands : List BigInt + cands = map itobi (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: Nil) + + matches : List Int → BigInt → Bool + matches want a = + let (M _ b c mem ip out) = step (M a b c mem ip Lin) in + let out = out <>> Nil in + out == want + + chain : (Int → Maybe Int) → List Int → Maybe Int + chain f Nil = Nothing + chain f (x :: xs) = case f x of + Just a => Just a + Nothing => chain f xs + + go : List Cand → Maybe BigInt + go Nil = Nothing + go ((a, Lin, acc) :: _) = Just a + go ((a, xs :< x, acc) :: todo) = + let next = filter (matches (x :: acc)) $ map (_+_ (a * itobi 8)) cands in + go (map (\a => (a, xs, x :: acc)) next ++ todo) + +render : SnocList Int → String +render out = go out Nil + where + go : SnocList Int → List Char → String + go Lin chars = pack $ tail chars + go (xs :< x) acc = go xs (',' :: chr (x + 48) :: acc) + +run : String -> IO Unit +run fn = do + putStrLn fn + text <- readFile fn + + let (Right (mach, Nil)) = pmachine (unpack text) + | (Right (_, cs)) => putStrLn $ "extra: " ++ pack cs + | _ => putStrLn "parse error" + + let (M a b c mem ip out) = (step mach) + putStrLn $ "part1 " ++ render out + let (Just p2) = part2 mach | Nothing => putStrLn "fail" + putStrLn $ "part2 " ++ show p2 + putStrLn "" + +main : IO Unit +main = do + run "aoc2024/day17/eg.txt" + run "aoc2024/day17/eg2.txt" + run "aoc2024/day17/input.txt" diff --git a/aoc2024/day17/eg.txt b/aoc2024/day17/eg.txt new file mode 100644 index 0000000..f09839b --- /dev/null +++ b/aoc2024/day17/eg.txt @@ -0,0 +1,5 @@ +Register A: 729 +Register B: 0 +Register C: 0 + +Program: 0,1,5,4,3,0 diff --git a/aoc2024/day17/eg2.txt b/aoc2024/day17/eg2.txt new file mode 100644 index 0000000..4a91c26 --- /dev/null +++ b/aoc2024/day17/eg2.txt @@ -0,0 +1,5 @@ +Register A: 2024 +Register B: 0 +Register C: 0 + +Program: 0,3,5,4,3,0 diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 201bee8..88929d6 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -74,11 +74,15 @@ data SnocList : U → U where _:<_ : ∀ A. SnocList A → A → SnocList A -- 'chips' -infixr 6 _<>>_ +infixr 6 _<>>_ _<><_ _<>>_ : ∀ a. SnocList a → List a → List a Lin <>> ys = ys (xs :< x) <>> ys = xs <>> x :: ys +_<><_ : ∀ a. SnocList a → List a → SnocList a +xs <>< Nil = xs +xs <>< (y :: ys) = (xs :< y) <>< ys + -- This is now handled by the parser, and LHS becomes `f a`. -- infixr 0 _$_ -- _$_ : ∀ a b. (a -> b) -> a -> b @@ -387,6 +391,7 @@ instance Show Int where show = showInt pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` +pfunc chr : Int → Char := `(c) => String.fromCharCode(c)` pfunc unpack uses (Nil _::_) : String -> List Char := `(s) => { @@ -752,3 +757,7 @@ instance ∀ a b. {{Eq a}} {{Eq b}} → Eq (a × b) where instance ∀ a b. {{Eq a}} {{Ord a}} {{Ord b}} → Ord (a × b) where (a,b) < (c,d) = if a == c then b < d else a < c +instance ∀ a. {{Eq a}} → Eq (List a) where + Nil == Nil = True + (x :: xs) == (y :: ys) = if x == y then xs == ys else False + _ == _ = False diff --git a/src/Main.idr b/src/Main.idr index a4f8578..1a425a0 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -123,7 +123,11 @@ processModule base stk name = do putStrLn "process Decls" traverse_ tryProcessDecl (collectDecl decls) - if (stk == []) then logMetas mstart else pure () + + -- we don't want implict errors from half-processed functions + -- but suppress them all on error for simplicity. + errors <- readIORef top.errors + if stk == [] && length errors == 0 then logMetas mstart else pure () pure src where