From 52bbb5aa6509ad31a4818dc45085a51e2cab947f Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Mon, 2 Dec 2024 10:58:10 -0800
Subject: [PATCH] Day2, prelude additions/fixes, better fc on do block errors

---
 TODO.md              |  1 +
 aoc2023/Prelude.newt | 30 +++++++++++++++++++++++---
 aoc2024/Day2.newt    | 51 ++++++++++++++++++++++++++++++++++++++++++++
 aoc2024/day2/eg.txt  |  6 ++++++
 src/Lib/Elab.idr     | 27 ++++++++++++-----------
 5 files changed, 100 insertions(+), 15 deletions(-)
 create mode 100644 aoc2024/Day2.newt
 create mode 100644 aoc2024/day2/eg.txt

diff --git a/TODO.md b/TODO.md
index 2b2ed4d..2dd58f5 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,7 @@
 
 ## TODO
 
+- [ ] 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 icit to Lam (see `check` for details)
diff --git a/aoc2023/Prelude.newt b/aoc2023/Prelude.newt
index b9bbcb8..299c1d3 100644
--- a/aoc2023/Prelude.newt
+++ b/aoc2023/Prelude.newt
@@ -162,11 +162,11 @@ class Applicative (f : U → U) where
   _<*>_ : {0 a b} -> f (a → b) → f a → f b
 
 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)
+  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 a <*> traverse f xs
+  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
@@ -582,6 +582,14 @@ pfunc arraySet uses (MkUnit) : ∀ a. IOArray a → Int → a → IO Unit := `(_
   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
 
@@ -598,3 +606,19 @@ instance Applicative IO where
     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)
+
diff --git a/aoc2024/Day2.newt b/aoc2024/Day2.newt
new file mode 100644
index 0000000..4c769e9
--- /dev/null
+++ b/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"
+
diff --git a/aoc2024/day2/eg.txt b/aoc2024/day2/eg.txt
new file mode 100644
index 0000000..b49c10d
--- /dev/null
+++ b/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
diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr
index 3165924..dd20e73 100644
--- a/src/Lib/Elab.idr
+++ b/src/Lib/Elab.idr
@@ -894,23 +894,26 @@ showDef ctx names n v@(VVar _ n' [<]) =  if n == n' then pure "" else pure "= \{
 showDef ctx names n v = pure "= \{pprint names !(quote ctx.lvl v)}"
 
 
-undo : List DoStmt -> M Raw
-undo [] = error emptyFC "do block must end in expression"
-undo ((DoExpr fc tm) :: Nil) = pure tm
+undo : FC -> List DoStmt -> M Raw
+undo prev [] = error prev "do block must end in expression"
+undo prev ((DoExpr fc tm) :: Nil) = pure tm
 -- TODO decide if we want to use >> or just >>=
-undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) !(undo xs)) Explicit
+undo prev ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>=_") tm Explicit) (RLam fc (BI fc "_" Explicit Many) !(undo fc xs)) Explicit
 -- undo ((DoExpr fc tm) :: xs) = pure $ RApp fc (RApp fc (RVar fc "_>>_") tm Explicit) !(undo xs) Explicit
-undo ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo xs
-undo ((DoArrow fc (RVar fc' nm) right []) :: xs) =
+undo prev ((DoLet fc nm tm) :: xs) = RLet fc nm (RImplicit fc) tm <$> undo fc xs
+undo prev ((DoArrow fc left@(RVar fc' nm) right []) :: xs) =
   case lookup nm !get of
-    Just _ => ?todo
+    Just _ => do
+      let nm = "$sc"
+      rest <- pure $ RCase fc (RVar fc nm) [MkAlt left !(undo fc xs)]
+      pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
+        (RLam fc (BI fc nm Explicit Many) rest) Explicit
     Nothing =>
       pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
-        (RLam fc (BI fc' nm Explicit Many) !(undo xs)) Explicit
-
-undo ((DoArrow fc left right alts) :: xs) = do
+        (RLam fc (BI fc' nm Explicit Many) !(undo fc xs)) Explicit
+undo prev ((DoArrow fc left right alts) :: xs) = do
   let nm = "$sc"
-  rest <- pure $ RCase fc (RVar fc nm) (MkAlt left !(undo xs) :: alts)
+  rest <- pure $ RCase fc (RVar fc nm) (MkAlt left !(undo fc xs) :: alts)
   pure $ RApp fc (RApp fc (RVar fc "_>>=_") right Explicit)
     (RLam fc (BI fc nm Explicit Many) rest) Explicit
 
@@ -919,7 +922,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of
   (RIf fc a b c, ty) =>
     let tm' = RCase fc a [ MkAlt (RVar (getFC b) "True") b, MkAlt (RVar (getFC c) "False") c ] in
     check ctx tm' ty
-  (RDo fc stmts, ty) => check ctx !(undo stmts) ty
+  (RDo fc stmts, ty) => check ctx !(undo fc stmts) ty
   (RCase fc rsc alts, ty) => do
     (sc, scty) <- infer ctx rsc
     scty <- forceMeta scty