refactoring in playground, use zip file for web

playground/samples/aoc2023/Day3.newt

@@ -0,0 +1,115 @@
+module Day3
+
+import Prelude
+import Node
+
+pfunc repr : {a : U} -> a -> String := `(a,o) => ''+o`
+pfunc jrepr : {a : U} -> a -> String := `(a,o) => JSON.stringify(o, null, '  ')`
+
+
+maybe : ∀ a b. b → (a → b) → Maybe a → b
+maybe def f Nothing = def
+maybe def f (Just a) = f a
+
+-- was 'structure' I could make a `record` that destructures to this..
+data Number : U where
+  MkNumber : (start : Nat) -> (stop : Nat) → (value : Int) → Number
+
+isDigit : Char -> Bool
+isDigit '0' = True
+isDigit '1' = True
+isDigit '2' = True
+isDigit '3' = True
+isDigit '4' = True
+isDigit '5' = True
+isDigit '6' = True
+isDigit '7' = True
+isDigit '8' = True
+isDigit '9' = True
+isDigit _ = False
+
+numbers : List Char -> List Number
+numbers arr = go arr Z
+  where
+    go : List Char → Nat → List Number
+    go (c :: cs) start = if isDigit c
+      then case span isDigit (c :: cs) of
+          (front,back) => let stop = start + length front
+            in MkNumber start stop (stringToInt $ pack front) :: go back stop
+      else go cs (S start)
+    go Nil start = Nil
+
+
+range : ∀ a. Nat -> Nat -> List a -> List a
+range _ _ Nil = Nil
+range _ Z _ = Nil
+range Z (S k) (x :: xs) = x :: range Z k xs
+range (S n) (S m) (x :: xs) = range n m xs
+
+isPart : List (List Char) -> Nat -> Number -> Bool
+isPart rows row (MkNumber start end _) =
+  checkRow (pred row) || checkRow row || checkRow (S row)
+  where
+    isThing : Char -> Bool
+    isThing c = not (isDigit c || c == '.')
+
+    checkRow : Nat -> Bool
+    checkRow r = case getAt r rows of
+      Nothing => False
+      Just chars => case filter isThing (range (pred start) (S end) chars) of
+        Nil => False
+        _ => True
+
+getValue : Number -> Int
+getValue (MkNumber _ _ v) = v
+
+part1 : List (List Char) -> Int
+part1 rows =
+    foldl (\ acc num => acc + getValue num) 0 $
+      join $ map (partNums rows) $ enumerate rows
+  where
+    partNums : List (List Char) -> (Nat × List Char) -> List Number
+    partNums grid (r, cs) =
+      filter (isPart grid r) $ (numbers cs)
+
+gears : List (List Char) -> List Char -> Nat -> Int
+gears rows row y =
+    let a = numbers (getAt! (pred y) rows)
+        b = numbers (getAt! y rows)
+        c = numbers (getAt! (S y) rows)
+        all = a ++ b ++ c
+        cands = map fst $ filter (_==_ '*' ∘ snd) (enumerate row)
+    in foldl _+_ 0 $ map (check all) cands
+  where
+    ratio : List Int → Int
+    ratio (a :: b :: Nil) = a * b
+    ratio _ = 0
+
+    match : Nat → Number → Bool
+    match y (MkNumber start stop value) = pred start <= y && y < S stop
+
+    check : List Number → Nat →  Int
+    check nums y = ratio $ map getValue (filter (match y) nums)
+
+part2 : List (List Char) -> Int
+part2 rows =
+  foldl go 0 (enumerate rows)
+  where
+    go : Int → Nat × List Char → Int
+    go acc (y, row) = acc + gears rows row y
+
+-- 4361 / 467835
+-- 517021 / 81296995
+run : String -> IO Unit
+run fn = do
+  content <- readFile fn
+  let grid = (splitOn '\n' $ unpack $ trim content)
+  putStrLn fn
+  printLn (part1 grid)
+  printLn (part2 grid)
+
+main : IO Unit
+main = do
+  run "aoc2023/day3/eg.txt"
+  run "aoc2023/day3/input.txt"
+

playground/samples/aoc2023/Day4.newt

@@ -0,0 +1,67 @@
+module Day4
+
+import Prelude
+import Node
+
+Round : U
+Round = List Int × List Int
+
+parseRound : String → Maybe Round
+parseRound s =
+  case split s ": " of
+    (a :: b :: Nil) => case split b " | " of
+      (l :: r :: Nil) => Just (nums l, nums r)
+      _ => Nothing
+    _ => Nothing
+  where
+    -- Nat or Int here?
+    nums : String → List Int
+    -- catch - split returns empty strings that become zeros
+    nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
+
+parse : String -> Maybe (List Round)
+parse s = mapM parseRound (split (trim s) "\n")
+
+pfunc pow : Int → Int → Int := `(x,y) => x ** y`
+
+part1 : List Round → Int
+part1 rounds = foldl _+_ 0 $ map score rounds
+  where
+    -- TODO we'll keep the math in Int land until we have magic Nat
+    score : Round → Int
+    score (a,b) = let count = natToInt $ length $ filter (\ n => elem n b) a
+      in if count == 0 then 0 else pow 2 (count - 1)
+
+part2 : List Round → Int
+part2 rounds = go 0 $ map (_,_ 1) rounds
+  where
+    mark : Int -> Nat → List (Int × Round) → List (Int × Round)
+    mark _ _ Nil = Nil
+    mark v Z rounds = rounds
+    mark v (S k) ((cnt, round) :: rounds) = (cnt + v, round) :: mark v k rounds
+
+    go : Int → List (Int × Round) → Int
+    go acc Nil = acc
+    go acc ((cnt, a, b) :: rounds) =
+      let n = length $ filter (\ n => elem n b) a
+      in go (acc + cnt) $ mark cnt n rounds
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+
+  case parse text of
+    Nothing => putStrLn "fail"
+    Just cards => do
+      putStrLn "part1"
+      printLn (part1 cards)
+      putStrLn "part2"
+      printLn (part2 cards)
+
+-- 13/30
+-- 25004/14427616
+main : IO Unit
+main = do
+  run "aoc2023/day4/eg.txt"
+  run "aoc2023/day4/input.txt"

playground/samples/aoc2023/Prelude.newt

@@ -0,0 +1,685 @@
+module Prelude
+
+id : ∀ a. a → a
+id x = x
+
+data Bool : U where
+  True False : Bool
+
+not : Bool → Bool
+not True = False
+not False = True
+
+-- In Idris, this is lazy in the second arg, we're not doing
+-- magic laziness for now, it's messy
+infixr 4 _||_
+_||_ : Bool → Bool → Bool
+True || _ = True
+False || b = b
+
+infixr 5 _&&_
+_&&_ : Bool → Bool → Bool
+False && b = False
+True && b = b
+
+infixl 6 _==_
+class Eq a where
+  _==_ : a → a → Bool
+
+infixl 6 _/=_
+_/=_ : ∀ a. {{Eq a}} → a → a → Bool
+a /= b = not (a == b)
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+pred : Nat → Nat
+pred Z = Z
+pred (S k) = k
+
+instance Eq Nat where
+  Z == Z = True
+  S n == S m = n == m
+  x == y = False
+
+data Maybe : U -> U where
+  Just : ∀ a. a -> Maybe a
+  Nothing : ∀ a. Maybe a
+
+fromMaybe : ∀ a. a → Maybe a → a
+fromMaybe a Nothing = a
+fromMaybe _ (Just a) = a
+
+data Either : U -> U -> U where
+  Left : {0 a b : U} -> a -> Either a b
+  Right : {0 a b : U} -> b -> Either a b
+
+infixr 7 _::_
+data List : U -> U where
+  Nil : ∀ A. List A
+  _::_ : ∀ A. A → List A → List A
+
+length : ∀ a. List a → Nat
+length Nil = Z
+length (x :: xs) = S (length xs)
+
+
+infixl 7 _:<_
+data SnocList : U → U where
+  Lin : ∀ A. SnocList A
+  _:<_ : ∀ A. SnocList A → A → SnocList A
+
+-- 'chips'
+infixr 6 _<>>_
+_<>>_ : ∀ a. SnocList a → List a → List a
+Lin <>> ys = ys
+(xs :< x) <>> ys = xs <>> x :: ys
+
+-- This is now handled by the parser, and LHS becomes `f a`.
+-- infixr 0 _$_
+-- _$_ : ∀ a b. (a -> b) -> a -> b
+-- f $ a = f a
+
+infixr 8 _×_
+infixr 2 _,_
+data _×_ : U → U → U where
+  _,_ : ∀ A B. A → B → A × B
+
+fst : ∀ a b. a × b → a
+fst (a,b) = a
+
+snd : ∀ a b. a × b → b
+snd (a,b) = b
+-- Monad
+
+class Monad (m : U → U) where
+  bind : {0 a b} → m a → (a → m b) → m b
+  pure : {0 a} → a → m a
+
+infixl 1 _>>=_ _>>_
+_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
+ma >>= amb = bind ma amb
+
+_>>_ :  ∀ m a b. {{Monad m}} -> m a -> m b -> m b
+ma >> mb = ma >>= (\ _ => mb)
+
+join : ∀ m a. {{Monad m}} → m (m a) → m a
+join mma = mma >>= id
+
+-- Equality
+
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+  Refl :  {A : U} -> {a : A} -> a ≡ a
+
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
+sym Refl = Refl
+
+-- Functor
+
+class Functor (m : U → U) where
+  map : {0 a b} → (a → b) → m a → m b
+
+infixr 4 _<$>_
+_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b
+f <$> ma = map f ma
+
+instance Functor Maybe where
+  map f Nothing = Nothing
+  map f (Just a) = Just (f a)
+
+instance Functor List where
+  map f Nil = Nil
+  map f (x :: xs) = f x :: map f xs
+
+instance Functor SnocList where
+  map f Lin = Lin
+  map f (xs :< x) = map f xs :< f x
+
+-- TODO this probably should depend on / entail Functor
+infixl 3 _<*>_
+class Applicative (f : U → U) where
+  -- appIsFunctor : Functor f
+  return : {0 a} → a → f a
+  _<*>_ : {0 a b} -> f (a → b) → f a → f b
+
+class Traversable (t : U → U) where
+  traverse : ∀ f a b. {{Applicative f}} → (a → f b) → t a → f (t b)
+
+instance Traversable List where
+  traverse f Nil = return Nil
+  traverse f (x :: xs) = return _::_ <*> f x <*> 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
+  Just f <*> fa = f <$> fa
+
+infixr 2 _<|>_
+class Alternative (m : U → U) where
+  _<|>_ : {0 a} → m a → m a → m a
+
+instance Alternative Maybe where
+  Nothing <|> x = x
+  Just x <|> _ = Just x
+
+-- Semigroup
+
+infixl 8 _<+>_
+class Semigroup a where
+  _<+>_ : a → a → a
+
+infixl 7 _+_
+class Add a where
+  _+_ : a → a → a
+
+infixl 8 _*_ _/_
+class Mul a where
+  _*_ : a → a → a
+
+class Div a where
+  _/_ : a → a → a
+
+instance Add Nat where
+  Z + m = m
+  S n + m = S (n + m)
+
+instance Mul Nat where
+  Z * _ = Z
+  S n * m = m + n * m
+
+infixl 7 _-_
+class Sub a where
+  _-_ : a → a → a
+
+instance Sub Nat where
+  Z - m = Z
+  n - Z = n
+  S n - S m = n - m
+
+infixr 7 _++_
+class Concat a where
+  _++_ : a → a → a
+
+ptype String
+ptype Int
+ptype Char
+
+pfunc sconcat : String → String → String := `(x,y) => x + y`
+instance Concat String where
+  _++_ = sconcat
+
+
+pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? True : False`
+pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? True : False`
+
+instance Eq Int where
+  a == b = jsEq a b
+
+instance Eq String where
+  a == b = jsEq a b
+
+instance Eq Char where
+  a == b = jsEq a b
+
+data Unit : U where
+  MkUnit : Unit
+
+ptype Array : U → U
+pfunc listToArray : {a : U} -> List a -> Array a := `
+(a, l) => {
+  let rval = []
+  while (l.tag !== 'Nil') {
+    rval.push(l.h1)
+    l = l.h2
+  }
+  return rval
+}
+`
+
+pfunc alen : {0 a : U} -> Array a -> Int := `(a,arr) => arr.length`
+pfunc aget : {0 a : U} -> Array a -> Int -> a := `(a, arr, ix) => arr[ix]`
+pfunc aempty : {0 a : U} -> Unit -> Array a := `() => []`
+
+pfunc arrayToList uses (Nil _::_) : {0 a} → Array a → List a := `(a,arr) => {
+  let rval = Nil(a)
+  for (let i = arr.length - 1;i >= 0; i--) {
+    rval = _$3A$3A_(a, arr[i], rval)
+  }
+  return rval
+}`
+
+
+
+-- for now I'll run this in JS
+pfunc lines : String → List String := `(s) => arrayToList(s.split('\n'))`
+
+pfunc p_strHead : (s : String) -> Char := `(s) => s[0]`
+pfunc p_strTail : (s : String) -> String := `(s) => s[0]`
+
+pfunc trim : String -> String := `s => s.trim()`
+pfunc split uses (Nil _::_) : String -> String -> List String := `(s, by) => {
+  let parts = s.split(by)
+  let rval = Nil(String)
+  parts.reverse()
+  parts.forEach(p => { rval = _$3A$3A_(undefined, p, rval) })
+  return rval
+}`
+
+pfunc slen : String -> Int := `s => s.length`
+pfunc sindex : String -> Int -> Char := `(s,i) => s[i]`
+
+-- TODO represent Nat as number at runtime
+pfunc natToInt : Nat -> Int := `(n) => {
+  let rval = 0
+  while (n.tag === 'S') {
+    n = n.h0
+    rval++
+  }
+  return rval
+}`
+
+pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')`
+pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))`
+
+-- I don't want to use an empty type because it would be a proof of void
+ptype World
+
+data IORes : U -> U where
+  MkIORes : ∀ a. a -> World -> IORes a
+
+IO : U -> U
+IO a = World -> IORes a
+
+instance Monad IO where
+  bind ma mab = \ w => case ma w of
+    MkIORes a w => mab a w
+  pure x = \ w => MkIORes x w
+
+bindList : ∀ a b. List a → (a → List b) → List b
+
+instance ∀ a. Concat (List a) where
+  Nil ++ ys = ys
+  (x :: xs) ++ ys = x :: (xs ++ ys)
+
+instance Monad List where
+  pure a = a :: Nil
+  bind Nil amb = Nil
+  bind (x :: xs) amb = amb x ++ bind xs amb
+
+
+
+-- This is traverse, but we haven't defined Traversable yet
+mapA : ∀ m. {{Applicative m}} {0 a b} → (a → m b) → List a → m (List b)
+mapA f Nil = return Nil
+mapA f (x :: xs) = return _::_ <*> f x <*> mapA f xs
+
+
+mapM : ∀ m. {{Monad m}} {0 a b} → (a → m b) → List a → m (List b)
+mapM f Nil = pure Nil
+mapM f (x :: xs) = do
+  b <- f x
+  bs <- mapM f xs
+  pure (b :: bs)
+
+class HasIO (m : U -> U) where
+  liftIO : ∀ a. IO a → m a
+
+instance HasIO IO where
+  liftIO a = a
+
+pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
+  console.log(s)
+  return MkIORes(undefined,MkUnit,w)
+}`
+
+putStrLn : ∀ io. {{HasIO io}} -> String -> io Unit
+putStrLn s = liftIO (primPutStrLn s)
+
+pfunc showInt : Int -> String := `(i) => String(i)`
+
+class Show a where
+  show : a → String
+
+instance Show String where
+  show a = a
+
+instance Show Int where
+  show = showInt
+
+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)
+    return acc
+}`
+
+pfunc pack : List Char → String := `(cs) => {
+  let rval = ''
+  while (cs.tag === '_::_') {
+    rval += cs.h1
+    cs = cs.h2
+  }
+  return rval
+}
+`
+
+pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
+  const go = (obj) => {
+    if (obj === undefined) return "_"
+    if (obj?.tag === '_::_' || obj?.tag === 'Nil') {
+      let stuff = listToArray(undefined,obj)
+      return '['+(stuff.map(go).join(', '))+']'
+    }
+    if (obj?.tag === 'S' || obj?.tag === 'Z') {
+      return ''+natToInt(obj)
+    } else if (obj?.tag) {
+      let rval = '('+obj.tag
+      for(let i=0;;i++) {
+        let key = 'h'+i
+        if (!(key in obj)) break
+        rval += ' ' + go(obj[key])
+      }
+      return rval+')'
+    } else {
+      return JSON.stringify(obj)
+    }
+  }
+  return go(obj)
+}`
+
+debugLog : ∀ a. a → IO Unit
+debugLog a = putStrLn (debugStr a)
+
+pfunc stringToInt : String → Int := `(s) => {
+  let rval = Number(s)
+  if (isNaN(rval)) throw new Error(s + " is NaN")
+  return rval
+}`
+
+foldl : ∀ A B. (B -> A -> B) -> B -> List A -> B
+foldl f acc Nil = acc
+foldl f acc (x :: xs) = foldl f (f acc x) xs
+
+infixl 9 _∘_
+_∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C
+(f ∘ g) x = f (g x)
+
+
+pfunc addInt : Int → Int → Int := `(x,y) => x + y`
+pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
+pfunc subInt : Int → Int → Int := `(x,y) => x - y`
+pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False`
+
+instance Mul Int where
+  x * y = mulInt x y
+
+instance Add Int where
+  x + y = addInt x y
+
+instance Sub Int where
+  x - y = subInt x y
+
+printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
+printLn a = putStrLn (show a)
+
+-- opaque JSObject
+ptype JSObject
+
+reverse : ∀ a. List a → List a
+reverse {a} = go Nil
+  where
+    go : List a → List a → List a
+    go acc Nil = acc
+    go acc (x :: xs) = go (x :: acc) xs
+
+-- Like Idris1, but not idris2, we need {a} to put a in scope.
+span : ∀ a. (a -> Bool) -> List a -> List a × List a
+span {a} f xs = go xs Nil
+  where
+    go : List a -> List a -> List a × List a
+    go Nil left = (reverse left, Nil)
+    go (x :: xs) left = if f x
+      then go xs (x :: left)
+      else (reverse left, x :: xs)
+
+instance Show Nat where
+  show n = show (natToInt n)
+
+enumerate : ∀ a. List a → List (Nat × a)
+enumerate {a} xs = go Z xs
+  where
+    go : Nat → List a → List (Nat × a)
+    go k Nil = Nil
+    go k (x :: xs) = (k,x) :: go (S k) xs
+
+filter : ∀ a. (a → Bool) → List a → List a
+filter pred Nil = Nil
+filter pred (x :: xs) = if pred x then x :: filter pred xs else filter pred xs
+
+drop : ∀ a. Nat -> List a -> List a
+drop _ Nil = Nil
+drop Z xs = xs
+drop (S k) (x :: xs) = drop k xs
+
+take : ∀ a. Nat -> List a -> List a
+take Z xs = Nil
+take _ Nil = Nil
+take (S k) (x :: xs) = x :: take k xs
+
+getAt : ∀ a. Nat → List a → Maybe a
+getAt _ Nil = Nothing
+getAt Z (x :: xs) = Just x
+getAt (S k) (x :: xs) = getAt k xs
+
+splitOn : ∀ a. {{Eq a}} → a → List a → List (List a)
+splitOn {a} v xs = go Nil xs
+  where
+    go : List a → List a → List (List a)
+    go acc Nil = reverse acc :: Nil
+    go acc (x :: xs) = if x == v
+      then reverse acc :: go Nil xs
+      else go (x :: acc) xs
+
+
+class Inhabited a where
+  default : a
+
+instance ∀ a. Inhabited (List a) where
+  default = Nil
+
+getAt! : ∀ a. {{Inhabited a}} → Nat → List a → a
+getAt! _ Nil = default
+getAt! Z (x :: xs) = x
+getAt! (S k) (x :: xs) = getAt! k xs
+
+
+instance ∀ a. Applicative (Either a) where
+  return b = Right b
+  Right x <*> Right y = Right (x y)
+  Left x <*> _ = Left x
+  Right x <*> Left y = Left y
+
+instance ∀ a. Monad (Either a) where
+  pure x = Right x
+  bind (Right x) mab = mab x
+  bind (Left x) mab = Left x
+
+instance Monad Maybe where
+  pure x = Just x
+  bind Nothing mab = Nothing
+  bind (Just x) mab = mab x
+
+
+elem : ∀ a. {{Eq a}} → a → List a → Bool
+elem v Nil = False
+elem v (x :: xs) = if v == x then True else elem v xs
+
+-- TODO no empty value on my `Add`, I need a group..
+-- sum : ∀ a. {{Add a}} → List a → a
+-- sum xs = foldl _+_
+pfunc trace uses (debugStr) : ∀ a. String -> a -> a := `(_, msg, a) => { console.log(msg,debugStr(_,a)); return a }`
+
+mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
+mapMaybe f Nil = Nil
+mapMaybe f (x :: xs) = case f x of
+  Just y => y :: mapMaybe f xs
+  Nothing => mapMaybe f xs
+
+zip : ∀ a b. List a → List b → List (a × b)
+zip (x :: xs) (y :: ys) = (x,y) :: zip xs ys
+zip _ _ = Nil
+
+-- TODO add double literals
+ptype Double
+pfunc intToDouble : Int → Double := `(x) => x`
+pfunc doubleToInt : Double → Int := `(x) => x`
+pfunc addDouble : Double → Double → Double := `(x,y) => x + y`
+pfunc subDouble : Double → Double → Double := `(x,y) => x - y`
+pfunc mulDouble : Double → Double → Double := `(x,y) => x * y`
+pfunc divDouble : Double → Double → Double := `(x,y) => x / y`
+pfunc sqrtDouble : Double → Double := `(x) => Math.sqrt(x)`
+pfunc ceilDouble : Double → Double := `(x) => Math.ceil(x)`
+
+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)
+}`
+
+pfunc ioArrayToList uses (Nil _::_ MkIORes) : {0 a} → IOArray a → IO (List a) := `(a,arr) => w => {
+  let rval = Nil(a)
+  for (let i = arr.length - 1;i >= 0; i--) {
+    rval = _$3A$3A_(a, arr[i], rval)
+  }
+  return MkIORes(undefined, rval, 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
+
+class Bifunctor (f : U → U → U) where
+  bimap : ∀ a b c d. (a → c) → (b → d) → f a b → f c d
+
+mapFst : ∀ a b c f. {{Bifunctor f}} → (a → c) → f a b → f c b
+mapFst f ab = bimap f id ab
+
+mapSnd : ∀ a b c f. {{Bifunctor f}} → (b → c) → f a b → f a c
+mapSnd f ab = bimap id f ab
+
+isNothing : ∀ a. Maybe a → Bool
+isNothing Nothing = True
+isNothing _ = False
+
+instance Bifunctor _×_ where
+  bimap f g (a,b) = (f a, g b)
+
+instance Functor IO where
+  map f a = bind a $ \ a => pure (f a)
+
+uncurry : ∀ a b c. (a -> b -> c) -> (a × b) -> c
+uncurry f (a,b) = f a b
+
+-- TODO Idris has a tail recursive version of this
+instance Applicative List where
+  return a = a :: Nil
+  Nil <*> _ = Nil
+  fs <*> ys = join $ map (\ f => map f ys) fs
+
+tail : ∀ a. List a → List a
+tail Nil = Nil
+tail (x :: xs) = xs
+
+--
+
+infixl 6 _<_ _<=_
+class Ord a where
+  -- isEq : Eq a
+  _<_ : a → a → Bool
+
+_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
+a <= b = a == b || a < b
+
+
+search : ∀ cl. {{cl}} -> cl
+search {{x}} = x
+
+instance Ord Nat where
+  -- isEq = search
+  _ < Z = False
+  Z < S _ = True
+  S n < S m = n < m
+
+
+instance Ord Int where
+  -- isEq = ?
+  x < y = ltInt x y
+
+instance Ord Char where
+  x < y = jsLT x y
+
+-- foo : ∀ a. {{Ord a}} -> a -> Bool
+-- foo a = a == a
+
+
+flip : ∀ a b c. (a → b → c) → (b → a → c)
+flip f b a = f a b
+
+partition : ∀ a. (a → Bool) → List a → List a × List a
+partition {a} pred xs = go xs Nil Nil
+  where
+    go : List a → List a → List a → List a × List a
+    go Nil as bs = (as, bs)
+    go (x :: xs) as bs = if pred x
+      then go xs (x :: as) bs
+      else go xs as (x :: bs)
+
+-- 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)
+
+ordNub : ∀ a. {{Eq a}} {{Ord a}} -> List a -> List a
+ordNub {a} {{ordA}} xs = go $ qsort _<_ xs
+  where
+    go : List a → List a
+    go (a :: b :: xs) = if a == b then go (a :: xs) else a :: go (b :: xs)
+    go t = t
+
+ite : ∀ a. Bool → a → a → a
+ite c t e = if c then t else e
+
+instance Ord String where
+  a < b = jsLT a b

playground/samples/aoc2023/day3/eg.txt

@@ -0,0 +1,10 @@
+467..114..
+...*......
+..35..633.
+......#...
+617*......
+.....+.58.
+..592.....
+......755.
+...$.*....
+.664.598..

playground/samples/aoc2023/day4/eg.txt

@@ -0,0 +1,6 @@
+Card 1: 41 48 83 86 17 | 83 86  6 31 17  9 48 53
+Card 2: 13 32 20 16 61 | 61 30 68 82 17 32 24 19
+Card 3:  1 21 53 59 44 | 69 82 63 72 16 21 14  1
+Card 4: 41 92 73 84 69 | 59 84 76 51 58  5 54 83
+Card 5: 87 83 26 28 32 | 88 30 70 12 93 22 82 36
+Card 6: 31 18 13 56 72 | 74 77 10 23 35 67 36 11

playground/samples/aoc2024/Aoc.newt

@@ -0,0 +1 @@
+../../../aoc2023/Aoc.newt

playground/samples/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"

playground/samples/aoc2024/Day2.newt

@@ -0,0 +1,51 @@
+module Day2
+
+import Prelude
+import Node
+import Aoc
+
+decr : List Int → Bool
+decr (x :: y :: _) = y < x
+decr _ = False
+
+diff : Int → Int → Int
+diff x y = if x < y then y - x else x - y
+
+isSafe : Bool → List Int → Bool
+isSafe decr (x :: y :: rest) =
+  let d = diff x y
+      good = 0 < d && d < 4
+      safe = if x < y then not decr && good else decr && good in
+  if safe then isSafe decr (y :: rest) else False
+isSafe _ _ = True
+
+check : List Int → Bool
+check x = isSafe (decr x) x
+
+any : ∀ a. (a → Bool) → List a → Bool
+any f xs = foldl (_||_) False $ map f xs
+
+alts : List Int → List (List Int)
+alts Nil = Nil
+alts (x :: xs) = xs :: map (_::_ x) (alts xs)
+
+-- I want lean's #eval here
+
+parse : String → List (List Int)
+parse text = map nums $ split (trim text) "\n"
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let stuff = parse text
+  let good = filter check stuff
+  putStrLn $ "part1 " ++ show (length good)
+  let good = filter (any check ∘ alts) stuff
+  putStrLn $ "part2 " ++ show (length good)
+
+main : IO Unit
+main = do
+  run "aoc2024/day2/eg.txt"
+  run "aoc2024/day2/input.txt"
+

playground/samples/aoc2024/Day3.newt

@@ -0,0 +1,121 @@
+module Day3
+
+import Prelude
+import Node
+import Aoc
+
+Parser : U → U
+Parser a = List Char → Maybe (a × List Char)
+
+instance Monad Parser where
+  pure a = \ cs => Just (a, cs)
+  bind ma mab = \ cs => ma cs >>= uncurry mab
+
+instance Alternative Parser where
+  pa <|> pb = \ cs => case pa cs of
+    Nothing => pb cs
+    res => res
+
+fail : ∀ a. Parser a
+fail = \ cs => Nothing
+
+satisfy : (Char → Bool) → Parser Char
+satisfy pred = λ cs => case cs of
+  Nil => Nothing
+  (c :: cs) => if pred c then Just (c, cs) else Nothing
+
+match : Char → Parser Char
+match d = satisfy (_==_ d)
+
+any : Parser Char
+any = satisfy (λ _ => True)
+
+some many : ∀ a. Parser a → Parser (List a)
+many p = some p <|> pure Nil
+some p = do
+  v <- p
+  vs <- many p
+  pure (v :: vs)
+
+pnum : Parser Int
+pnum = do
+  chars <- many (satisfy isDigit)
+  if S (S (S Z)) < length chars then fail
+    else pure $ stringToInt $ pack chars
+
+data Inst : U where
+  Mult : Int → Int → Inst
+  Do : Inst
+  Dont : Inst
+
+mul : Parser Inst
+mul = do
+  match 'm'
+  match 'u'
+  match 'l'
+  match '('
+  x <- pnum
+  match ','
+  y <- pnum
+  match ')'
+  pure $ Mult x y
+
+pdo : Parser Inst
+pdo = do
+  match 'd'
+  match 'o'
+  match '('
+  match ')'
+  pure Do
+
+pdont : Parser Inst
+pdont = do
+  match 'd'
+  match 'o'
+  match 'n'
+  match '\''
+  match 't'
+  match '('
+  match ')'
+  pure Dont
+
+some' many' : ∀ a. Parser a → Parser (List a)
+many' p = do
+  pure MkUnit
+  some' p <|> (any >> many' p) <|> pure Nil
+
+some' p = do
+  v <- p
+  vs <- many' p
+  pure (v :: vs)
+
+inst : Parser Inst
+inst = mul <|> pdo <|> pdont
+
+pfile : Parser (List Inst)
+pfile = many' inst
+
+value : Inst → Int
+value (Mult x y) = x * y
+value _ = 0
+
+part2 : List Inst → Bool → Int → Int
+part2 Nil _ acc = acc
+part2 (Do :: insts) _ acc = part2 insts True acc
+part2 (Dont :: insts) _ acc = part2 insts False acc
+part2 (_ :: insts) False acc = part2 insts False acc
+part2 (Mult x y :: insts) True acc = part2 insts True (acc + x * y)
+
+run : String → IO Unit
+run fn = do
+  putStrLn fn
+  text <- trim <$> readFile fn
+  let (Just (insts, Nil)) = pfile (unpack text) | _ => putStrLn "parse failed"
+  let part1 = foldl _+_ 0 $ map value insts
+  putStrLn $ "part1 " ++ show part1
+  putStrLn $ "part2 " ++ show (part2 insts True 0)
+
+main : IO Unit
+main = do
+  run "aoc2024/day3/eg.txt"
+  run "aoc2024/day3/input.txt"

playground/samples/aoc2024/Day4.newt

@@ -0,0 +1,76 @@
+module Day4
+
+import Prelude
+import Node
+import Aoc
+
+data Problem : U where
+  P : Int → String → Problem
+
+get : Problem → Int → Int → Char
+get (P size text) r c =
+  if r < 0 || size <= r then '.'
+  else if c < 0 || size <= c then '.'
+  else sindex text (r * (size + 1) + c)
+
+check : Problem → Int → Int → Int × Int → Int
+check prob r c (dr,dc) =
+  if (get prob r c) /= 'X' then 0
+  else if (get prob (r + dr) (c + dc)) /= 'M' then 0
+  else if (get prob (r + 2 * dr) (c + 2 * dc)) /= 'A' then 0
+  else if (get prob (r + 3 * dr) (c + 3 * dc)) /= 'S' then 0
+  else 1
+
+dirs : List (Int × Int)
+dirs = tail $ _,_ <$> 0 :: 0 - 1 :: 1 :: Nil <*> 0 :: 0 - 1 :: 1 :: Nil
+
+part1 : Problem → Int
+part1 (P size text) = go 0 0 0
+  where
+    go : Int → Int → Int → Int
+    go acc r c =
+      if r == size then acc else
+      if c == size then go acc (r + 1) 0 else
+      let acc = foldl _+_ acc $ map (check (P size text) r c) dirs in
+      go acc r (c + 1)
+
+pats : List (Char × Char × Char × Char)
+pats = ('M', 'M', 'S', 'S') ::
+       ('S', 'M', 'M', 'S') ::
+       ('S', 'S', 'M', 'M') ::
+       ('M', 'S', 'S', 'M') ::
+       Nil
+
+check2 : Problem → Int → Int → (Char × Char × Char × Char) → Int
+check2 prob r c (w,x,y,z) =
+  if (get prob r c) /= 'A' then 0
+  else if (get prob (r - 1) (c - 1)) /= w then 0
+  else if (get prob (r - 1) (c + 1)) /= x then 0
+  else if (get prob (r + 1) (c + 1)) /= y then 0
+  else if (get prob (r + 1) (c - 1)) /= z then 0
+  else 1
+
+part2 : Problem → Int
+part2 (P size text) = go 0 0 0
+  where
+    go : Int → Int → Int → Int
+    go acc r c =
+      if r == size then acc else
+      if c == size then go acc (r + 1) 0 else
+      let acc = foldl _+_ acc $ map (check2 (P size text) r c) pats in
+      go acc r (c + 1)
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let lines = split (trim text) "\n"
+  -- I'm going to assume it's square for convenience
+  let size = length lines
+  printLn $ "part1 " ++ show (part1 $ P (cast size) text)
+  printLn $ "part2 " ++ show (part2 $ P (cast size) text)
+
+main : IO Unit
+main = do
+  run "aoc2024/day4/eg.txt"
+  run "aoc2024/day4/input.txt"

playground/samples/aoc2024/Day5.newt

@@ -0,0 +1,77 @@
+module Day5
+
+import Prelude
+import Node
+import Aoc
+import SortedMap
+
+data Prob : U where
+  MkProb : List (Int × Int) -> List (List Int) → Prob
+
+parseRule : String → Maybe (Int × Int)
+parseRule txt =
+  let (a :: b :: Nil) = nums' "|" txt  | _ => Nothing
+  in Just (a,b)
+
+parse : String → Maybe Prob
+parse text = do
+  let (a :: b :: Nil) = split (trim text) "\n\n" | pts => Nothing
+  rules <- traverse parseRule $ split a "\n"
+  let updates = map (nums' ",") $ split b "\n"
+  Just $ MkProb rules updates
+
+RuleMap : U
+RuleMap = SortedMap Int (List Int)
+
+getDisallowed : Int → RuleMap → List Int
+getDisallowed key rmap = fromMaybe Nil (map snd $ lookupMap key rmap)
+
+mkRuleMap : List (Int × Int) -> RuleMap
+mkRuleMap rules = foldl go EmptyMap rules
+  where
+    go : RuleMap → Int × Int → RuleMap
+    go rmap (b,a) = updateMap a (b :: getDisallowed a rmap) rmap
+
+scan : RuleMap → List Int -> List Int -> Bool
+scan rmap interdit Nil = True
+scan rmap interdit (x :: xs) =
+  if elem x interdit then False
+  else scan rmap (getDisallowed x rmap ++ interdit) xs
+
+fix : RuleMap → List Int → List Int
+fix rmap Nil = Nil
+fix rmap (x :: xs) =
+  let interdit = getDisallowed x rmap in
+  let (prefix,rest) = partition (flip elem interdit) xs
+  in case prefix of
+    Nil => x :: fix rmap rest
+    ys => fix rmap (ys ++ x :: rest)
+
+middle : List Int -> Int
+middle xs = go xs xs
+  where
+    go : List Int → List Int → Int
+    go (x :: xs) (_ :: _ :: ys) = go xs ys
+    go (x :: xs) (_ :: ys) = x
+    go _ _ = 0
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let (Just prob) = parse text | _ => putStrLn "Parse Error"
+  let (MkProb rules things) = prob
+  let rmap = mkRuleMap rules
+  let good = filter (scan rmap Nil) things
+  let part1 = foldl _+_ 0 $ map middle good
+  let bad = filter (not ∘ scan rmap Nil) things
+  putStrLn $ "part1 " ++ show part1
+  let fixed = map (fix rmap) bad
+  printLn $ length bad
+  let part2 = foldl _+_ 0 $ map middle fixed
+  putStrLn $ "part2 " ++ show part2
+
+main : IO Unit
+main = do
+  run "aoc2024/day5/eg.txt"
+  run "aoc2024/day5/input.txt"

playground/samples/aoc2024/Day6.newt

@@ -0,0 +1,132 @@
+module Day6
+
+import Prelude
+import Node
+import Aoc
+import SortedMap
+
+Point : U
+Point = Int × Int
+
+instance Eq Point where
+  (a,b) == (c,d) = a == c && b == d
+
+instance Ord Point where
+  (a,b) < (c,d) = a < c || a == c && b < d
+
+Grid : U
+Grid = SortedMap Point Char
+
+loadData : String → Grid
+loadData text = go (unpack text) 0 0 EmptyMap
+  where
+    go : List Char → Int → Int → SortedMap Point Char → SortedMap Point Char
+    go Nil r c map = map
+    go ('\n' :: cs) r c map = go cs (r + 1) 0 map
+    go (x :: xs) r c map = go xs r (c + 1) $ updateMap (r,c) x map
+
+data Dir : U where North East South West : Dir
+
+instance Show Dir where
+  show North = "N"
+  show East = "E"
+  show South = "S"
+  show West = "W"
+
+instance Ord Dir where
+  a < b = show a < show b
+
+instance Eq (Point × Dir) where
+  (a,b) == (c,d) = a == c && show b == show d
+
+instance Ord (Point × Dir) where
+  (a,b) < (c,d) =
+    if a < c then True
+    else if a /= c then False
+    else b < d
+
+Done : U
+Done = SortedMap (Point × Dir) Unit
+
+turn : Dir → Dir
+turn North = East
+turn East = South
+turn South = West
+turn West = North
+
+instance Cast Dir Char where
+  cast North = '^'
+  cast East = '>'
+  cast South = 'v'
+  cast West = '<'
+
+step : Dir → Point → Point
+step North (r, c) = (r - 1, c)
+step East (r, c) = (r, c + 1)
+step South (r, c) = (r + 1, c)
+step West (r, c) = (r, c - 1)
+
+bad : Point → Bool
+bad (x,y) = x < 0 || y < 0
+
+-- third is
+walk : Dir → Point → Grid → Grid
+walk dir pos grid =
+  let grid = updateMap pos 'X' grid in
+  let pos' = step dir pos in
+  case lookupMap pos' grid of
+    Just (_, '#') => walk (turn dir) pos grid
+    Nothing => grid
+    _   => walk dir pos' grid
+
+checkLoop : Grid → Done → Dir → Point → Bool
+checkLoop grid done dir pos =
+  let (Nothing) = lookupMap (pos,dir) done | _ => True in
+  let done = updateMap (pos, dir) MkUnit done
+      pos' = step dir pos
+    in case lookupMap pos' grid of
+        Nothing => False
+        Just (_, '#') => checkLoop grid done (turn dir) pos
+        Just _ => checkLoop grid done dir pos'
+
+part2 : Dir → Point → Grid → Done → List Point → List Point
+part2 dir pos grid done sol =
+  let done = updateMap (pos, dir) MkUnit done
+      grid = updateMap pos 'X' grid
+      turnDir = turn dir
+      turnPos = step turnDir pos
+      pos' = step dir pos in
+  case lookupMap pos' grid of
+    Nothing => sol
+    Just (_, '#') => part2 (turn dir) pos grid done sol
+    Just (_, 'X') => part2 dir pos' grid done sol
+    Just (_, '.') => if checkLoop (updateMap pos' '#' grid) done turnDir pos
+      then part2 dir pos' grid done (pos' :: sol)
+      else part2 dir pos' grid done sol
+    Just x => part2 (trace ("WAT " ++ debugStr x) dir) pos' grid done sol
+
+lookupV : ∀ a. Char → List (a × Char) → Maybe a
+lookupV _ Nil = Nothing
+lookupV needle ((k,v) :: rest) =
+  if v == needle then Just k else lookupV needle rest
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let grid = loadData text
+  let (Just pos) = lookupV '^' (toList grid) | _ => putStrLn "no guard"
+  let grid' = walk North pos grid
+  let xs = filter (\ x => 'X' == snd x) $ toList grid'
+  let part1 = length xs
+  putStrLn $ "part1 " ++ show part1
+
+  let cands = part2 North pos grid EmptyMap Nil
+  -- debugLog $ length cands -- turns out nub isn't needed for these cases, but we'll leave it in
+  putStrLn $ "part2 " ++ show (length $ ordNub cands)
+  printLn $ length $ toList grid
+
+main : IO Unit
+main = do
+  run "aoc2024/day6/eg.txt"
+  run "aoc2024/day6/input.txt"

playground/samples/aoc2024/Day7.newt

@@ -0,0 +1,58 @@
+module Day7
+
+import Prelude
+import Node
+import Aoc
+
+Prob : U
+Prob = Int × List Int
+
+cases : Int → Int → List Int → Bool
+cases goal acc Nil = goal == acc
+cases goal acc (x :: xs) =
+  if goal < acc then False
+  else if cases goal (x + acc) xs then True
+  else cases goal (x * acc) xs
+
+part1 : Prob → Bool
+part1 (goal, x :: xs) = cases goal x xs
+part1 _ = False
+
+cat : Int → Int → Int
+cat x y = stringToInt $ show x ++ show y
+
+cases2 : Int → Int → List Int → Bool
+cases2 goal acc Nil = goal == acc
+cases2 goal acc (x :: xs) =
+  if goal < acc then False
+  else if cases2 goal (x + acc) xs then True
+  else if cases2 goal (x * acc) xs then True
+  else cases2 goal (cat acc x) xs
+
+part2 : Prob → Bool
+part2 (goal, x :: xs) = cases2 goal x xs
+part2 _ = False
+
+parse : String -> Maybe (List Prob)
+parse text = do
+  traverse parseLine $ split (trim text) "\n"
+  where
+    parseLine : String → Maybe Prob
+    parseLine line = do
+      let (a :: b :: Nil) = split line ": " | _ => Nothing
+      Just (stringToInt a , nums b)
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let (Just probs) = parse text | _ => putStrLn "parse error"
+  let p1 = foldl _+_ 0 $ map fst $ filter part1 probs
+  putStrLn $ "part1 " ++ show p1
+  let p2 = foldl _+_ 0 $ map fst $ filter part2 probs
+  putStrLn $ "part2 " ++ show p2
+
+main : IO Unit
+main = do
+  run "aoc2024/day7/eg.txt"
+  run "aoc2024/day7/input.txt"

playground/samples/aoc2024/Day8.newt

@@ -0,0 +1,95 @@
+module Day8
+
+import Prelude
+import Node
+import Aoc
+import SortedMap
+
+Point : U
+Point = Int × Int
+
+instance Add Point where
+  (a,b) + (c,d) = (a + c, b + d)
+
+instance Sub Point where
+  (a,b) - (c,d) = (a - c, b - d)
+
+Ant : U
+Ant = Char × Int × Int
+
+-- This should be a utility...
+parse : String → List Ant
+parse text = go 0 0 (unpack text) Nil
+  where
+    -- might as well be tail recursive
+    go : Int → Int → List Char → List Ant → List Ant
+    go row col Nil ants = ants
+    go row col ('\n' :: cs) ants = go (row + 1) 0 cs ants
+    go row col (c :: cs) ants = go row (col + 1) cs ((c,row,col) :: ants)
+
+doPair : Point → Point → List Point
+doPair x y = let d = y - x in y + d :: x - d :: Nil
+
+doGroup : List Ant -> List Point
+doGroup (x :: xs) = join $ doGroup xs ::  map (doPair (snd x) ∘ snd) xs
+doGroup Nil = Nil
+
+group : List Ant → (List Ant) → List (List Ant)
+group (a :: as) Nil = group as (a :: Nil)
+group (a :: as) (b :: bs) =
+  if fst a == fst b
+    then group as (a :: b :: bs)
+    else (b :: bs) :: group as (a :: Nil)
+group Nil bs = bs :: Nil
+
+max : Int → Int → Int
+max a b = if a < b then b else a
+
+check : Int → Point → Bool
+check mr (r,c) = 0 <= r && 0 <= c && r <= mr && c <= mr
+
+
+doPair2 : Int -> Point → Point → List Point
+doPair2 m x y = go x (y - x) ++ go y (x - y)
+  where
+    go : Point -> Point -> List Point
+    go pt d = if check m pt then pt :: go (pt + d) d else Nil
+
+doGroup2 : Int -> List Ant -> List Point
+doGroup2 m (x :: xs) = join $ doGroup2 m xs ::  map (doPair2 m (snd x) ∘ snd) xs
+doGroup2 m Nil = Nil
+
+instance Ord Point where
+  (a,b) < (c,d) = a < c || a == c && b < d
+
+instance Eq Point where
+  (a,b) == (c,d) = a == c && b == d
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let points = parse text
+  let maxrow = trace "maxrow" $ foldl max 0 $ map (fst ∘ snd) points
+  let maxcol = trace "maxcol" $ foldl max 0 $ map (snd ∘ snd) points
+  let ants = filter (\ pt => fst pt /= '.') points
+  let ants = qsort (\ x y => fst x < fst y) ants
+  let groups = group ants Nil
+  let stuff = join $ map doGroup groups
+  let nodes = filter (check maxrow) stuff
+
+  let part1 = length $ ordNub nodes
+  putStrLn $ "part1 " ++ show part1
+
+  let stuff2 = join $ map (doGroup2 maxrow) groups
+  let part2 = length $ ordNub stuff2
+  putStrLn $ "part2 " ++ show part2
+
+
+
+
+
+main : IO Unit
+main = do
+  run "aoc2024/day8/eg.txt"
+  run "aoc2024/day8/input.txt"

playground/samples/aoc2024/Node.newt

@@ -0,0 +1 @@
+../../../aoc2023/Node.newt

playground/samples/aoc2024/Prelude.newt

@@ -0,0 +1 @@
+../../../newt/Prelude.newt

playground/samples/aoc2024/SortedMap.newt

@@ -0,0 +1,67 @@
+module SortedMap
+
+import Prelude
+
+data T23 : Nat -> U -> U -> U where
+  Leaf : ∀ k v. k -> v -> T23 Z k v
+  Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+  Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+
+lookupT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> T23 h k v -> Maybe (k × v)
+lookupT23 key (Leaf k v)= if k == key then Just (k,v) else Nothing
+lookupT23 key (Node2 t1 k1 t2) =
+  if key <= k1 then lookupT23 key t1 else lookupT23 key t2
+lookupT23 key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1 then lookupT23 key t1
+  else if key <= k2 then lookupT23 key t2
+  else lookupT23 key t3
+
+insertT23 : ∀ h k v. {{Ord k}} {{Eq k}} -> k -> v -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
+insertT23 key value (Leaf k v) =
+  if key == k then Left (Leaf key value)
+  else if key <= k then Right (Leaf key value, key, Leaf k v)
+  else Right (Leaf k v, k, Leaf key value)
+insertT23 key value (Node2 t1 k1 t2) =
+  if key <= k1 then
+    case insertT23 key value t1 of
+      Left t1' => Left (Node2 t1' k1 t2)
+      Right (a,b,c) => Left (Node3 a b c k1 t2)
+  else case insertT23 key value t2 of
+      Left t2' => Left (Node2 t1 k1 t2')
+      Right (a,b,c) => Left (Node3 t1 k1 a b c)
+insertT23 key value (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1 then
+    case insertT23 key value t1 of
+      Left t1' => Left (Node3 t1' k1 t2 k2 t3)
+      Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
+  else if key <= k2 then
+    case insertT23 key value t2 of
+      Left t2' => Left (Node3 t1 k1 t2' k2 t3)
+      Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
+  else
+    case insertT23 key value t3 of
+      Left t3' => Left (Node3 t1 k1 t2 k2 t3')
+      Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
+
+data SortedMap : U -> U -> U where
+  EmptyMap : ∀ k v. SortedMap k v
+  MapOf : ∀ k v h. T23 h k v -> SortedMap k v
+
+lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v)
+lookupMap k EmptyMap = Nothing
+lookupMap k (MapOf map) = lookupT23 k map
+
+updateMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> v -> SortedMap k v -> SortedMap k v
+updateMap k v EmptyMap = MapOf $ Leaf k v
+updateMap k v (MapOf map) = case insertT23 k v map of
+  Left map' => MapOf map'
+  Right (a, b, c) => MapOf (Node2 a b c)
+
+toList : ∀ k v. SortedMap k v → List (k × v)
+toList {k} {v} (MapOf smap) = reverse $ go smap Nil
+  where
+    go : ∀ h. T23 h k v → List (k × v) → List (k × v)
+    go (Leaf k v) acc = (k, v) :: acc
+    go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
+    go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
+toList _ = Nil

playground/samples/aoc2024/day1/eg.txt

@@ -0,0 +1,6 @@
+3   4
+4   3
+2   5
+1   3
+3   9
+3   3

playground/samples/aoc2024/day2/eg.txt

@@ -0,0 +1,6 @@
+7 6 4 2 1
+1 2 7 8 9
+9 7 6 2 1
+1 3 2 4 5
+8 6 4 4 1
+1 3 6 7 9

playground/samples/aoc2024/day3/eg.txt

@@ -0,0 +1 @@
+xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))

playground/samples/aoc2024/day4/eg.txt

@@ -0,0 +1,11 @@
+MMMSXXMASM
+MSAMXMSMSA
+AMXSXMAAMM
+MSAMASMSMX
+XMASAMXAMM
+XXAMMXXAMA
+SMSMSASXSS
+SAXAMASAAA
+MAMMMXMMMM
+MXMXAXMASX
+

playground/samples/aoc2024/day5/eg.txt

@@ -0,0 +1,28 @@
+47|53
+97|13
+97|61
+97|47
+75|29
+61|13
+75|53
+29|13
+97|29
+53|29
+61|53
+97|53
+61|29
+47|13
+75|47
+97|75
+47|61
+75|61
+47|29
+75|13
+53|13
+
+75,47,61,53,29
+97,61,53,29,13
+75,29,13
+75,97,47,61,53
+61,13,29
+97,13,75,29,47

playground/samples/aoc2024/day6/eg.txt

@@ -0,0 +1,11 @@
+....#.....
+.........#
+..........
+..#.......
+.......#..
+..........
+.#..^.....
+........#.
+#.........
+......#...
+

playground/samples/aoc2024/day7/eg.txt

@@ -0,0 +1,9 @@
+190: 10 19
+3267: 81 40 27
+83: 17 5
+156: 15 6
+7290: 6 8 6 15
+161011: 16 10 13
+192: 17 8 14
+21037: 9 7 18 13
+292: 11 6 16 20

playground/samples/aoc2024/day8/day1/eg.txt

@@ -0,0 +1,6 @@
+3   4
+4   3
+2   5
+1   3
+3   9
+3   3

playground/samples/aoc2024/day8/day2/eg.txt

@@ -0,0 +1,6 @@
+7 6 4 2 1
+1 2 7 8 9
+9 7 6 2 1
+1 3 2 4 5
+8 6 4 4 1
+1 3 6 7 9

playground/samples/aoc2024/day8/day3/eg.txt

@@ -0,0 +1 @@
+xmul(2,4)%&mul[3,7]!@^do_not_mul(5,5)+mul(32,64]then(mul(11,8)mul(8,5))

playground/samples/aoc2024/day8/day4/eg.txt

@@ -0,0 +1,11 @@
+MMMSXXMASM
+MSAMXMSMSA
+AMXSXMAAMM
+MSAMASMSMX
+XMASAMXAMM
+XXAMMXXAMA
+SMSMSASXSS
+SAXAMASAAA
+MAMMMXMMMM
+MXMXAXMASX
+

playground/samples/aoc2024/day8/day5/eg.txt

@@ -0,0 +1,28 @@
+47|53
+97|13
+97|61
+97|47
+75|29
+61|13
+75|53
+29|13
+97|29
+53|29
+61|53
+97|53
+61|29
+47|13
+75|47
+97|75
+47|61
+75|61
+47|29
+75|13
+53|13
+
+75,47,61,53,29
+97,61,53,29,13
+75,29,13
+75,97,47,61,53
+61,13,29
+97,13,75,29,47

playground/samples/aoc2024/day8/day6/eg.txt

@@ -0,0 +1,11 @@
+....#.....
+.........#
+..........
+..#.......
+.......#..
+..........
+.#..^.....
+........#.
+#.........
+......#...
+

playground/samples/aoc2024/day8/day7/eg.txt

@@ -0,0 +1,9 @@
+190: 10 19
+3267: 81 40 27
+83: 17 5
+156: 15 6
+7290: 6 8 6 15
+161011: 16 10 13
+192: 17 8 14
+21037: 9 7 18 13
+292: 11 6 16 20

playground/samples/aoc2024/day8/eg.txt

@@ -0,0 +1,12 @@
+............
+........0...
+.....0......
+.......0....
+....0.......
+......A.....
+............
+............
+........A...
+.........A..
+............
+............