Fix aoc2024 build

- Holes are no longer allowed when building executables
- Stack overflow in mapMaybe (Day15)
This commit is contained in:
2025-04-10 08:50:52 -04:00
parent 0ce1a5e454
commit d6156ebc79
8 changed files with 16 additions and 17 deletions

View File

@@ -72,7 +72,7 @@ step mach@(M a b c mem ip out) =
5 => let o = combo op % itobi 8 in step (M a b c mem (ip + 2) (out :< bitoi o)) 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) 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) 7 => let c = a >>> combo op in step (M a b c mem (ip + 2) out)
_ => ? _ => mach
where where
combo : Int BigInt combo : Int BigInt
combo 4 = a combo 4 = a

View File

@@ -72,10 +72,7 @@ calcCheats start dists fuel threshold = go (toList start) 0
-- only '.' have dist -- only '.' have dist
tryCand : Int Point Point Int tryCand : Int Point Point Int
tryCand l pt cand = case lookupMap cand dists of tryCand l pt cand = case lookupMap cand dists of
Just (_, dist) => Just (_, dist) => if l + manh pt cand + dist <= threshold then 1 else 0
let d = manh pt cand in
if fuel < d then (let x = (trace "X" (pt, cand, d)) in ?) else
if l + manh pt cand + dist <= threshold then 1 else 0
Nothing => 0 Nothing => 0
go : List (Point × Int) Int Int go : List (Point × Int) Int Int

View File

@@ -78,7 +78,7 @@ pathCost from to kp =
case lookupMap (from, to) kp.costs of case lookupMap (from, to) kp.costs of
Just (_, cost) => (kp, cost) Just (_, cost) => (kp, cost)
Nothing => Nothing =>
let (path :: paths) = getPaths kp.interdit from to | _ => ? in let (path :: paths) = getPaths kp.interdit from to | _ => fatalError "empty path list" in
case kp of case kp of
(KP n s i c Nothing) => (kp, 1) (KP n s i c Nothing) => (kp, 1)
(KP n s i c (Just kp')) => (KP n s i c (Just kp')) =>

View File

@@ -106,7 +106,7 @@ pathCost from to = do
case lookupMap (from, to) (.costs kp) of case lookupMap (from, to) (.costs kp) of
Just (_, cost) => pure {State Keypad} cost Just (_, cost) => pure {State Keypad} cost
Nothing => Nothing =>
let (path :: paths) = getPaths (.interdit kp) from to | _ => ? in let (path :: paths) = getPaths (.interdit kp) from to | _ => fatalError "empty paths" in
case kp of case kp of
(KP n s i c Nothing) => pure 1 (KP n s i c Nothing) => pure 1
(KP n s i c (Just kp')) => do (KP n s i c (Just kp')) => do

View File

@@ -132,7 +132,7 @@ swapPins a g (MkG i1 i2 op out) =
else MkG i1 i2 op out else MkG i1 i2 op out
fail : a. String -> a fail : a. String -> a
fail msg = let x = trace "FAIL" msg in ? fail msg = fatalError msg
check : List Gate List Int String Either (String × String) Unit check : List Gate List Int String Either (String × String) Unit
check gates Nil carry = Right MkUnit check gates Nil carry = Right MkUnit

View File

@@ -21,7 +21,7 @@ part1 : List File -> Int
part1 fs = go 0 0 fs $ reverse fs part1 fs = go 0 0 fs $ reverse fs
where where
go : Int -> Int -> List File -> List File -> Int go : Int -> Int -> List File -> List File -> Int
go pos csum Nil bwd = ? go pos csum Nil bwd = fatalError "Shouldn't happen"
go pos csum fwd Nil = csum go pos csum fwd Nil = csum
go pos csum ((id, 0, 0) :: fwd) bwd = go pos csum fwd bwd 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 fwd ((id, 0, _) :: bwd) = go pos csum fwd bwd

View File

@@ -580,10 +580,13 @@ elem v (x :: xs) = if v == x then True else elem v xs
pfunc trace uses (debugStr) : a. String -> a -> a := `(_, msg, a) => { console.log(msg,Prelude_debugStr(_,a)); return a }` pfunc trace uses (debugStr) : a. String -> a -> a := `(_, msg, a) => { console.log(msg,Prelude_debugStr(_,a)); return a }`
mapMaybe : a b. (a Maybe b) List a List b mapMaybe : a b. (a Maybe b) List a List b
mapMaybe f Nil = Nil mapMaybe {a} {b} f xs = go Lin xs
mapMaybe f (x :: xs) = case f x of where
Just y => y :: mapMaybe f xs go : SnocList b List a List b
Nothing => mapMaybe f xs go acc Nil = acc <>> Nil
go acc (x :: xs) = case f x of
Just y => go (acc :< y) xs
Nothing => go acc xs
zip : a b. List a List b List (a × b) zip : a b. List a List b List (a × b)
zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
@@ -781,10 +784,6 @@ find : ∀ a. (a → Bool) → List a → Maybe a
find f Nil = Nothing find f Nil = Nothing
find f (x :: xs) = if f x then Just x else find f xs find f (x :: xs) = if f x then Just x else find f xs
any : a. (a Bool) List a Bool
any f Nil = False
any f (x :: xs) = if f x then True else any f xs
-- TODO this would be faster, but less pure as a primitive -- TODO this would be faster, but less pure as a primitive
-- fastConcat might be a good compromise -- fastConcat might be a good compromise
joinBy : String List String String joinBy : String List String String

View File

@@ -76,6 +76,9 @@ arityForName fc nm = do
(Just (PrimFn t arity used)) => pure arity (Just (PrimFn t arity used)) => pure arity
any : a. (a Bool) List a Bool
any f Nil = False
any f (x :: xs) = if f x then True else any f xs
-- need to eta out extra args, fill in the rest of the apps -- need to eta out extra args, fill in the rest of the apps
-- NOW - maybe eta here instead of Compile.newt, drop number on CApp -- NOW - maybe eta here instead of Compile.newt, drop number on CApp