Day9

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"

aoc2024/day9/eg.txt

@@ -0,0 +1 @@
+2333133121414131402

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)
+    let acc = Nil(undefined)
-    for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
+    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

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)
+    let acc = Nil(undefined)
-    for (let i = s.length - 1; 0 <= i; i--) acc = _$3A$3A_(Char, s[i], acc)
+    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

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"

playground/samples/aoc2024/day9

@@ -0,0 +1 @@
+../../../aoc2024/day9

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