diff --git a/aoc2023/Aoc.newt b/aoc2023/Aoc.newt index 65fc575..d36c1fa 100644 --- a/aoc2023/Aoc.newt +++ b/aoc2023/Aoc.newt @@ -17,3 +17,21 @@ isDigit '7' = True isDigit '8' = True isDigit '9' = True isDigit _ = False + +indexOf? : ∀ a. {{Eq a}} → a → List a → Maybe Nat +indexOf? {a} z xs = go Z z xs + where + go : Nat → a → List a → Maybe Nat + go ix z Nil = Nothing + go ix z (x :: xs) = + if z == x then Just ix else go (S ix) z xs + +-- if_then_else shorthand +-- Lean version uses a decidable instead of Bool +ite : ∀ a. Bool → a → a → a +ite c t e = if c then t else e + +-- probably not super efficient, but it works +qsort : ∀ a. (a → a → Bool) → List a → List a +qsort lt Nil = Nil +qsort lt (x :: xs) = qsort lt (filter (λ y => not $ lt x y) xs) ++ x :: qsort lt (filter (lt x) xs) diff --git a/aoc2023/Day5.newt b/aoc2023/Day5.newt index 3df60a7..e69e99f 100644 --- a/aoc2023/Day5.newt +++ b/aoc2023/Day5.newt @@ -2,10 +2,11 @@ module Day5 import Prelude import Node +import Aoc -- AoC lib? -nums : String → List Int -nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " " +-- nums : String → List Int +-- nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " " data MapEntry : U where -- dest / src / len @@ -78,10 +79,6 @@ apply' (r1, r2) x = case x of else (r1 + d - s, r2) :: Nil --- probably not super efficient, but it works -qsort : ∀ a. (a → a → Bool) → List a → List a -qsort lt Nil = Nil -qsort lt (x :: xs) = qsort lt (filter (λ y => not $ lt x y) xs) ++ x :: qsort lt (filter (lt x) xs) apply : List Range → List MapEntry → List Range apply ranges entries = diff --git a/aoc2023/Prelude.newt b/aoc2023/Prelude.newt index 631c202..b9bbcb8 100644 --- a/aoc2023/Prelude.newt +++ b/aoc2023/Prelude.newt @@ -164,6 +164,13 @@ class Applicative (f : U → U) where class Traversable (t : U → U) where traverse : {f : U → U} → {{appf : Applicative f}} → {a : U} → {b : U} → (a → f b) → t a → f (t b) +instance Traversable List where + traverse f nil = return Nil + traverse f (x :: xs) = return _::_ <*> f a <*> traverse f xs + +for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b) +for stuff fun = traverse fun stuff + instance Applicative Maybe where return a = Just a Nothing <*> _ = Nothing @@ -308,6 +315,7 @@ instance Monad IO where MkIORes a w => mab a w pure a = \ w => MkIORes a w + bindList : ∀ a b. List a → (a → List b) → List b instance ∀ a. Concat (List a) where @@ -386,11 +394,11 @@ pfunc pack : List Char → String := `(cs) => { pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { const go = (obj) => { - if (obj?.tag === '_::_') { + if (obj?.tag === '_::_' || obj?.tag === 'Nil') { let stuff = listToArray(undefined,obj) return '['+(stuff.map(go).join(', '))+']' } - if (obj?.tag === 'S') { + if (obj?.tag === 'S' || obj?.tag === 'Z') { return ''+natToInt(obj) } else if (obj?.tag) { let rval = '('+obj.tag @@ -564,3 +572,29 @@ instance Add Double where x + y = addDouble x y instance Sub Double where x - y = subDouble x y instance Mul Double where x * y = mulDouble x y instance Div Double where x / y = divDouble x y + +ptype IOArray : U → U +pfunc newArray uses (MkIORes) : ∀ a. Int → a → IO (IOArray a) := + `(_, n, v) => (w) => MkIORes(undefined,Array(n).fill(v),w)` +pfunc arrayGet : ∀ a. IOArray a → Int → IO a := `(_, arr, ix) => w => MkIORes(undefined, arr[ix], w)` +pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_, arr, ix, v) => w => { + arr[ix] = v + return MkIORes(undefined, MkUnit, w) +}` + +class Cast a b where + cast : a → b + +instance Cast Nat Int where + cast = natToInt + +instance Cast Int Double where + cast = intToDouble + +instance Applicative IO where + return a = \ w => MkIORes a w + f <*> a = \ w => + let (MkIORes f w) = trace "fw" $ f w in + let (MkIORes a w) = trace "aw" $ a w in + MkIORes (f a) w + diff --git a/aoc2024/Day1.newt b/aoc2024/Day1.newt new file mode 100644 index 0000000..fc4a364 --- /dev/null +++ b/aoc2024/Day1.newt @@ -0,0 +1,60 @@ +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/aoc2024/day1/eg.txt b/aoc2024/day1/eg.txt new file mode 100644 index 0000000..dfca0b1 --- /dev/null +++ b/aoc2024/day1/eg.txt @@ -0,0 +1,6 @@ +3 4 +4 3 +2 5 +1 3 +3 9 +3 3 \ No newline at end of file diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 518d0f3..2b57220 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -202,7 +202,7 @@ keywords : List String keywords = [ "var", "true", "false", "let", "case", "switch", "if", "then", "else", "String", "function", "void", "undefined", "null", "await", "async", "return", "const", - "Number", "default" + "Number", "default", "for", "while", "Function" ] ||| escape identifiers for js