From 2f518a953d6bd39964ee574059f078b31d945ce2 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Mon, 9 Dec 2024 16:53:32 -0800 Subject: [PATCH] Day9 --- aoc2024/Day9.newt | 127 ++++++++++++++++++++++++ aoc2024/day9/eg.txt | 1 + newt/Prelude.newt | 40 +++++++- playground/samples/aoc2023/Prelude.newt | 40 +++++++- playground/samples/aoc2024/Day9.newt | 127 ++++++++++++++++++++++++ playground/samples/aoc2024/day9 | 1 + src/Lib/Compile.idr | 2 +- 7 files changed, 333 insertions(+), 5 deletions(-) create mode 100644 aoc2024/Day9.newt create mode 100644 aoc2024/day9/eg.txt create mode 100644 playground/samples/aoc2024/Day9.newt create mode 120000 playground/samples/aoc2024/day9 diff --git a/aoc2024/Day9.newt b/aoc2024/Day9.newt new file mode 100644 index 0000000..fd05c3b --- /dev/null +++ b/aoc2024/Day9.newt @@ -0,0 +1,127 @@ +module Day9 + +import Prelude +import Node +import Aoc +import SortedMap + +File : U +File = Int × Int × Int + +parse : String -> List File +parse cs = go 0 (unpack $ trim cs) Nil + where + go : Int -> List Char -> List File -> List File + go id (a :: b :: cs) acc = + go (id + 1) cs ((id, (ord a - 48), (ord b - 48)) :: acc) + go id (a :: cs) acc = go (id + 1) cs ((id, (ord a - 48), 0) :: acc) + go _ _ acc = reverse acc + +part1 : List File -> Int +part1 fs = go 0 0 fs $ reverse fs + where + go : Int -> Int -> List File -> List File -> Int + go pos csum Nil bwd = ? + go pos csum fwd Nil = csum + 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 ((id, 0, k) :: fs) ((id', l, g) :: bwd) = + if id == id' then csum + else go (pos + 1) (csum + pos * id') ((id, 0, k - 1) :: fs) ((id', l - 1, g) :: bwd) + go pos csum ((id, k, gap) :: fs) ((id', l, g) :: rest) = + if id == id' + then go (pos + 1) (csum + pos * id) ((id, k, gap) :: fs) ((id', l - 1, g) :: Nil) + else go (pos + 1) (csum + pos * id) ((id, k - 1, gap) :: fs) ((id', l, g) :: rest) + +min : Int → Int → Int +min a b = if a < b then a else b + +-- I really do want records... +Node : U +Node = Int × Int × File + +FileSystem : U +FileSystem = SortedMap Int Node + +mkfs : List File → FileSystem +mkfs = foldl go EmptyMap + where + go : FileSystem → File → FileSystem + go fs (id,l,g) = updateMap id (id - 1, id + 1, id, l, g) fs + +removeNode : Int → FileSystem → FileSystem +removeNode ix fs = + -- yeah, I want records.. + let (Just (_ ,p1,n1, i1, l1, g1)) = lookupMap ix fs | _ => fs in + let (Just (_, p2, _, i2, l2, g2)) = lookupMap p1 fs | _ => fs in + let fs = updateMap p1 (p2, n1, i2, l2, g2 + l1 + g1) fs in + let (Just (_, _, n2, i2, l2, g2)) = lookupMap n1 fs | _ => fs in + updateMap n1 (p1, n2, i2, l2, g2) fs + +insertNode : Int → File → FileSystem → FileSystem +insertNode ix (i,l,g) fs = + -- previous + let (Just (_, p1, n1, i1, l1, g1)) = lookupMap ix fs | _ => fs in + let fs = updateMap ix (p1,i,i1,l1,0) fs in + let fs = updateMap i (ix, n1, i,l,g1 - l) fs in + let (Just (_, p2, n2, i2, l2, g2)) = lookupMap n1 fs | _ => fs in + updateMap n1 (i, n2, i2, l2, g2) fs + +defrag : FileSystem → Int -> Int → Int → FileSystem +defrag fs start end limit = + case lookupMap end fs of + Nothing => fs + Just (k,(p,n,id,l,g)) => + -- our only optimization... + if limit <= l then defrag fs start p limit else + case search l start end of + Nothing => defrag fs start p (min l limit) + Just (id',l',g') => + defrag (insertNode id' (id,l,g) $ removeNode end fs) start p limit + where + search : Int → Int → Int -> Maybe File + search size pos end = + if pos == end then Nothing else + case lookupMap pos fs of + Nothing => Nothing + Just (_,(p,n,id,l,g)) => + if size <= g then Just (id,l,g) + else search size n end + +check : FileSystem → Int +check fs = go 0 0 $ files 0 Lin + where + files : Int → SnocList File → List File + files start acc = case lookupMap start fs of + Nothing => acc <>> Nil + Just (_, _, n, f) => files n (acc :< f) + + go : Int → Int → List File → Int + go pos csum Nil = csum + go pos csum ((id,l,g) :: rest) = + if l == 0 then go (pos + g) csum rest + else go (pos + 1) (csum + pos * id) ((id, l - 1, g) :: rest) + +part2 : List File → Int +part2 files = + let fs = mkfs files + end = cast (length files) - 1 + fs' = defrag fs 0 end end + in check fs' + +run : String -> IO Unit +run fn = do + putStrLn fn + text <- readFile fn + let files = parse $ trim text + putStrLn $ show (length files) ++ " files" + let p1 = part1 files + putStrLn $ "part1 " ++ show p1 + let p2 = part2 files + putStrLn $ "part2 " ++ show p2 + pure MkUnit + +main : IO Unit +main = do + run "aoc2024/day9/eg.txt" + run "aoc2024/day9/input.txt" diff --git a/aoc2024/day9/eg.txt b/aoc2024/day9/eg.txt new file mode 100644 index 0000000..f96c390 --- /dev/null +++ b/aoc2024/day9/eg.txt @@ -0,0 +1 @@ +2333133121414131402 diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 35f73f8..f7d60e4 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -3,6 +3,9 @@ module Prelude id : ∀ a. a → a id x = x +the : (a : U) → a → a +the _ a = a + data Bool : U where True False : Bool @@ -288,6 +291,14 @@ pfunc natToInt : Nat -> Int := `(n) => { return rval }` +pfunc intToNat uses (Z S) : Int -> Nat := `(n) => { + let rval = Z + for (;n>0;n--) rval = S(rval); + return rval; +}` + + + pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')` pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` @@ -360,8 +371,8 @@ pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` pfunc unpack uses (Nil _::_) : String -> List Char := `(s) => { - let acc = Nil(Char) - for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc) + let acc = Nil(undefined) + for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(undefined, s[i], acc) return acc }` @@ -378,10 +389,21 @@ pfunc pack : List Char → String := `(cs) => { pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { const go = (obj) => { if (obj === undefined) return "_" + if (obj.tag === '_,_') { + let rval = '(' + while (obj?.tag === '_,_') { + rval += go(obj.h2) + ', ' + obj = obj.h3 + } + return rval + go(obj) + ')' + } if (obj?.tag === '_::_' || obj?.tag === 'Nil') { let stuff = listToArray(undefined,obj) return '['+(stuff.map(go).join(', '))+']' } + if (obj instanceof Array) { + return 'io['+(obj.map(go).join(', '))+']' + } if (obj?.tag === 'S' || obj?.tag === 'Z') { return ''+natToInt(obj) } else if (obj?.tag) { @@ -558,6 +580,7 @@ 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)` @@ -565,6 +588,7 @@ pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_ arr[ix] = v return MkIORes(undefined, MkUnit, w) }` +pfunc arraySize uses (MkIORes) : ∀ a. IOArray a → IO Int := `(_, arr) => w => MkIORes(undefined, arr.length, w)` pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a) := `(a,arr) => w => { let rval = Nil(a) @@ -574,6 +598,15 @@ pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a return MkIORes(undefined, rval, w) }` +pfunc listToIOArray uses (MkIORes) : {0 a} → List a → IO (Array a) := `(a,list) => w => { + let rval = [] + while (list.tag === '_::_') { + rval.push(list.h1) + list = list.h2 + } + return MkIORes(undefined,rval,w) +}` + class Cast a b where cast : a → b @@ -683,3 +716,6 @@ ite c t e = if c then t else e instance Ord String where a < b = jsLT a b + +instance Cast Int Nat where + cast n = intToNat n diff --git a/playground/samples/aoc2023/Prelude.newt b/playground/samples/aoc2023/Prelude.newt index 35f73f8..f7d60e4 100644 --- a/playground/samples/aoc2023/Prelude.newt +++ b/playground/samples/aoc2023/Prelude.newt @@ -3,6 +3,9 @@ module Prelude id : ∀ a. a → a id x = x +the : (a : U) → a → a +the _ a = a + data Bool : U where True False : Bool @@ -288,6 +291,14 @@ pfunc natToInt : Nat -> Int := `(n) => { return rval }` +pfunc intToNat uses (Z S) : Int -> Nat := `(n) => { + let rval = Z + for (;n>0;n--) rval = S(rval); + return rval; +}` + + + pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')` pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` @@ -360,8 +371,8 @@ pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` pfunc unpack uses (Nil _::_) : String -> List Char := `(s) => { - let acc = Nil(Char) - for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc) + let acc = Nil(undefined) + for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(undefined, s[i], acc) return acc }` @@ -378,10 +389,21 @@ pfunc pack : List Char → String := `(cs) => { pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => { const go = (obj) => { if (obj === undefined) return "_" + if (obj.tag === '_,_') { + let rval = '(' + while (obj?.tag === '_,_') { + rval += go(obj.h2) + ', ' + obj = obj.h3 + } + return rval + go(obj) + ')' + } if (obj?.tag === '_::_' || obj?.tag === 'Nil') { let stuff = listToArray(undefined,obj) return '['+(stuff.map(go).join(', '))+']' } + if (obj instanceof Array) { + return 'io['+(obj.map(go).join(', '))+']' + } if (obj?.tag === 'S' || obj?.tag === 'Z') { return ''+natToInt(obj) } else if (obj?.tag) { @@ -558,6 +580,7 @@ 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)` @@ -565,6 +588,7 @@ pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_ arr[ix] = v return MkIORes(undefined, MkUnit, w) }` +pfunc arraySize uses (MkIORes) : ∀ a. IOArray a → IO Int := `(_, arr) => w => MkIORes(undefined, arr.length, w)` pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a) := `(a,arr) => w => { let rval = Nil(a) @@ -574,6 +598,15 @@ pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a return MkIORes(undefined, rval, w) }` +pfunc listToIOArray uses (MkIORes) : {0 a} → List a → IO (Array a) := `(a,list) => w => { + let rval = [] + while (list.tag === '_::_') { + rval.push(list.h1) + list = list.h2 + } + return MkIORes(undefined,rval,w) +}` + class Cast a b where cast : a → b @@ -683,3 +716,6 @@ ite c t e = if c then t else e instance Ord String where a < b = jsLT a b + +instance Cast Int Nat where + cast n = intToNat n diff --git a/playground/samples/aoc2024/Day9.newt b/playground/samples/aoc2024/Day9.newt new file mode 100644 index 0000000..fd05c3b --- /dev/null +++ b/playground/samples/aoc2024/Day9.newt @@ -0,0 +1,127 @@ +module Day9 + +import Prelude +import Node +import Aoc +import SortedMap + +File : U +File = Int × Int × Int + +parse : String -> List File +parse cs = go 0 (unpack $ trim cs) Nil + where + go : Int -> List Char -> List File -> List File + go id (a :: b :: cs) acc = + go (id + 1) cs ((id, (ord a - 48), (ord b - 48)) :: acc) + go id (a :: cs) acc = go (id + 1) cs ((id, (ord a - 48), 0) :: acc) + go _ _ acc = reverse acc + +part1 : List File -> Int +part1 fs = go 0 0 fs $ reverse fs + where + go : Int -> Int -> List File -> List File -> Int + go pos csum Nil bwd = ? + go pos csum fwd Nil = csum + 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 ((id, 0, k) :: fs) ((id', l, g) :: bwd) = + if id == id' then csum + else go (pos + 1) (csum + pos * id') ((id, 0, k - 1) :: fs) ((id', l - 1, g) :: bwd) + go pos csum ((id, k, gap) :: fs) ((id', l, g) :: rest) = + if id == id' + then go (pos + 1) (csum + pos * id) ((id, k, gap) :: fs) ((id', l - 1, g) :: Nil) + else go (pos + 1) (csum + pos * id) ((id, k - 1, gap) :: fs) ((id', l, g) :: rest) + +min : Int → Int → Int +min a b = if a < b then a else b + +-- I really do want records... +Node : U +Node = Int × Int × File + +FileSystem : U +FileSystem = SortedMap Int Node + +mkfs : List File → FileSystem +mkfs = foldl go EmptyMap + where + go : FileSystem → File → FileSystem + go fs (id,l,g) = updateMap id (id - 1, id + 1, id, l, g) fs + +removeNode : Int → FileSystem → FileSystem +removeNode ix fs = + -- yeah, I want records.. + let (Just (_ ,p1,n1, i1, l1, g1)) = lookupMap ix fs | _ => fs in + let (Just (_, p2, _, i2, l2, g2)) = lookupMap p1 fs | _ => fs in + let fs = updateMap p1 (p2, n1, i2, l2, g2 + l1 + g1) fs in + let (Just (_, _, n2, i2, l2, g2)) = lookupMap n1 fs | _ => fs in + updateMap n1 (p1, n2, i2, l2, g2) fs + +insertNode : Int → File → FileSystem → FileSystem +insertNode ix (i,l,g) fs = + -- previous + let (Just (_, p1, n1, i1, l1, g1)) = lookupMap ix fs | _ => fs in + let fs = updateMap ix (p1,i,i1,l1,0) fs in + let fs = updateMap i (ix, n1, i,l,g1 - l) fs in + let (Just (_, p2, n2, i2, l2, g2)) = lookupMap n1 fs | _ => fs in + updateMap n1 (i, n2, i2, l2, g2) fs + +defrag : FileSystem → Int -> Int → Int → FileSystem +defrag fs start end limit = + case lookupMap end fs of + Nothing => fs + Just (k,(p,n,id,l,g)) => + -- our only optimization... + if limit <= l then defrag fs start p limit else + case search l start end of + Nothing => defrag fs start p (min l limit) + Just (id',l',g') => + defrag (insertNode id' (id,l,g) $ removeNode end fs) start p limit + where + search : Int → Int → Int -> Maybe File + search size pos end = + if pos == end then Nothing else + case lookupMap pos fs of + Nothing => Nothing + Just (_,(p,n,id,l,g)) => + if size <= g then Just (id,l,g) + else search size n end + +check : FileSystem → Int +check fs = go 0 0 $ files 0 Lin + where + files : Int → SnocList File → List File + files start acc = case lookupMap start fs of + Nothing => acc <>> Nil + Just (_, _, n, f) => files n (acc :< f) + + go : Int → Int → List File → Int + go pos csum Nil = csum + go pos csum ((id,l,g) :: rest) = + if l == 0 then go (pos + g) csum rest + else go (pos + 1) (csum + pos * id) ((id, l - 1, g) :: rest) + +part2 : List File → Int +part2 files = + let fs = mkfs files + end = cast (length files) - 1 + fs' = defrag fs 0 end end + in check fs' + +run : String -> IO Unit +run fn = do + putStrLn fn + text <- readFile fn + let files = parse $ trim text + putStrLn $ show (length files) ++ " files" + let p1 = part1 files + putStrLn $ "part1 " ++ show p1 + let p2 = part2 files + putStrLn $ "part2 " ++ show p2 + pure MkUnit + +main : IO Unit +main = do + run "aoc2024/day9/eg.txt" + run "aoc2024/day9/input.txt" diff --git a/playground/samples/aoc2024/day9 b/playground/samples/aoc2024/day9 new file mode 120000 index 0000000..4ae6efc --- /dev/null +++ b/playground/samples/aoc2024/day9 @@ -0,0 +1 @@ +../../../aoc2024/day9 \ No newline at end of file diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index edead2d..1a6b722 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -175,7 +175,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", "for", "while", "Function" + "Number", "default", "for", "while", "Function", "Array" ] ||| escape identifiers for js