toki/advent-of-code-2024
1
0
Fork 0
Code Issues Pull requests Activity

refactor: remove totality assertion

Browse source
This commit is contained in:
Kiana Sheibani 2024-12-09 00:44:40 -05:00
parent 2196df1811
commit b4391bec86
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 6 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Day7/Part1.idr
View file

@ -1,9 +1,7 @@
module Day7.Part1
import Data.List
import Data.List1
import Data.String
import Data.Vect
import Utils
@ -28,14 +26,15 @@ parseInput = traverse parseLine . lines
--- DATA
search : List Op -> Nat -> List1 Nat -> Bool
search _ n (x ::: []) = x == n
search ops n (x ::: y :: xs) =
search : List Op -> (tg, tot : Nat) -> List Nat -> Bool
search _ tg tot [] = tg == tot
search ops tg tot (x :: xs) =
-- heuristic: abandon if running total is larger than target
x <= n && any (\op => assert_total $ search ops n (op x y ::: xs)) ops
tot <= tg && any (\op => search ops tg (op tot x) xs) ops
--- SOLUTION
export
solution : String -> Maybe Nat
solution = map (sum . map fst . filter (uncurry $ search [(+),(*)])) . parseInput
solution = map (sum . map fst . filter (\(tg,x:::xs) => search [(+),(*)] tg x xs))
. parseInput