day4

TODO.md

@@ -1,13 +1,14 @@
 
 ## TODO
 
+- [ ] syntax for negative integers
 - [x] Put worker in iframe on safari
 - [ ] Warnings or errors for missing definitions
 - [ ] Warnings or errors for unused cases
   - Important when misspelled constructors become pattern vars
 - [ ] if we're staying with this version of auto, we might need to list candidates and why they're rejected. e.g. I had a bifunctor fail to solve because the right answer unblocked a Foo vs IO Foo mismatch
 - [ ] literals for double
-- [ ] default failing case for constructor matching
+- [ ] add default failing case for constructor matching to catch errors
 - [ ] Add icit to Lam (see `check` for details)
 - [ ] add jump to definition magic to vscode extension
 - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
@@ -19,8 +20,9 @@
   - [ ] `$` no longer works inside ≡⟨ ⟩ sort out how to support both that and `$ \ x => ...`
 - [ ] Support @ on the LHS
 - [ ] records
-- [ ] rework unify case tree
+- [ ] rework `unify` case tree
   - Idris needs help with the case tree to keep code size down, do it in stages, one dcon at a time.
+  - I'm not sure it can go a few steps deep and have a default hanging off the side, so we may need to put the default case in another function ourselves.
 - [x] Strategy to avoid three copies of `Prelude.newt` in this source tree
 - [ ] `mapM` needs inference help when scrutinee (see Day2.newt)
   - Meta hasn't been solved yet. It's Normal, but maybe our delayed solving of Auto plays into it. Idris will peek at LHS of CaseAlts to guess the type if it doesn't have one.
@@ -36,7 +38,7 @@
 - [ ] refactor playground to better share code with idris2-playground
 - [ ] accepting DCon for another type (skipping case, but should be an error)
 - [ ] don't allow (or dot) duplicate names on LHS
-- [ ] remove metas from context, M has TopContext
+- [x] remove metas from context, M has TopContext
 - [ ] improve test driver
   - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
@@ -75,14 +77,16 @@
 - [x] Case for primitives
 - [ ] aoc2023 translation
   - [x] day1
-  - [x] day2
+  - [x] day2 - day6
   - some "real world" examples
 - [ ] Translate newt to newt
   - [x] Prettier
   - [x] if / then / else sugar
   - [ ] `data Foo = A | B` sugar
   - [ ] records
-  - [ ] where
+  - [x] where
+  - [ ] namespaces
+  - [ ] magic nat?
 - [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet
 - [x] unsolved meta errors repeat (need to freeze or only report at end)
 - [x] Sanitize JS idents, e.g. `_+_`

aoc2024/Day4.newt

@@ -0,0 +1,81 @@
+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
+
+tail : ∀ a. List a → List a
+tail Nil = Nil
+tail (x :: xs) = xs
+
+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
+  -- part2 will probably wrap around.
+  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"

aoc2024/day4/eg.txt

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

newt/Prelude.newt

@@ -627,3 +627,9 @@ instance Functor IO where
 
 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