From b4391bec8697b29a65271145483b5ed9eef35c1c Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 9 Dec 2024 00:44:40 -0500 Subject: [PATCH] refactor: remove totality assertion --- src/Day7/Part1.idr | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/Day7/Part1.idr b/src/Day7/Part1.idr index 211a540..ad9a0c1 100644 --- a/src/Day7/Part1.idr +++ b/src/Day7/Part1.idr @@ -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