From ccbd617671608752220cbdd79aa18dc0b2260bbe Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Thu, 5 Dec 2024 16:13:12 -0800
Subject: [PATCH] Day5, add SortedMap

---
 TODO.md                      |  4 ++
 aoc2023/Aoc.newt             | 14 ++----
 aoc2024/Day4.newt            |  7 +--
 aoc2024/Day5.newt            | 77 +++++++++++++++++++++++++++++++++
 aoc2024/DayXX.newt           | 17 ++++++++
 aoc2024/SortedMap.newt       | 58 +++++++++++++++++++++++++
 aoc2024/day5/eg.txt          | 28 ++++++++++++
 aoc2024/mkday                |  7 +++
 newt/Prelude.newt            | 84 +++++++++++++++++++++++++++---------
 playground/samples/Day1.newt |  4 --
 src/Lib/ProcessDecl.idr      | 10 ++++-
 11 files changed, 268 insertions(+), 42 deletions(-)
 create mode 100644 aoc2024/Day5.newt
 create mode 100644 aoc2024/DayXX.newt
 create mode 100644 aoc2024/SortedMap.newt
 create mode 100644 aoc2024/day5/eg.txt
 create mode 100755 aoc2024/mkday

diff --git a/TODO.md b/TODO.md
index a13d643..2ec111d 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,10 @@
 
 ## TODO
 
+- [ ] fix "insufficient patterns", wire in M or Either String
+- [ ] typeclass dependencies
+  - need to flag internal functions to not search (or flag functions for search)
+  - don't search instances that are currently being defined
 - [ ] syntax for negative integers
 - [x] Put worker in iframe on safari
 - [ ] Warnings or errors for missing definitions
diff --git a/aoc2023/Aoc.newt b/aoc2023/Aoc.newt
index d36c1fa..8ab948b 100644
--- a/aoc2023/Aoc.newt
+++ b/aoc2023/Aoc.newt
@@ -2,6 +2,10 @@ module Aoc
 
 import Prelude
 
+-- `by` is the first argument for use in `map`
+nums' : String → String → List Int
+nums' by s = map stringToInt $ filter (_/=_ "") $ split (trim s) by
+
 nums : String → List Int
 nums s = map stringToInt $ filter (_/=_ "") $ split (trim s) " "
 
@@ -25,13 +29,3 @@ indexOf? {a} z xs = go Z z xs
     go ix z Nil = Nothing
     go ix z (x :: xs) =
       if z == x then Just ix else go (S ix) z xs
-
--- if_then_else shorthand
--- Lean version uses a decidable instead of Bool
-ite : ∀ a. Bool → a → a → a
-ite c t e = if c then t else e
-
--- 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)
diff --git a/aoc2024/Day4.newt b/aoc2024/Day4.newt
index ffa489c..273d9f9 100644
--- a/aoc2024/Day4.newt
+++ b/aoc2024/Day4.newt
@@ -21,12 +21,8 @@ check prob r c (dr,dc) =
   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)
+dirs = tail $ _,_ <$> 0 :: 0 - 1 :: 1 :: Nil <*> 0 :: 0 - 1 :: 1 :: Nil
 
 part1 : Problem → Int
 part1 (P size text) = go 0 0 0
@@ -70,7 +66,6 @@ run fn = do
   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)
diff --git a/aoc2024/Day5.newt b/aoc2024/Day5.newt
new file mode 100644
index 0000000..690ea58
--- /dev/null
+++ b/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"
diff --git a/aoc2024/DayXX.newt b/aoc2024/DayXX.newt
new file mode 100644
index 0000000..4368646
--- /dev/null
+++ b/aoc2024/DayXX.newt
@@ -0,0 +1,17 @@
+module DayXX
+
+import Prelude
+import Node
+import Aoc
+
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  putStrLn text
+
+main : IO Unit
+main = do
+  run "aoc2024/dayXX/eg.txt"
+  run "aoc2024/dayXX/input.txt"
diff --git a/aoc2024/SortedMap.newt b/aoc2024/SortedMap.newt
new file mode 100644
index 0000000..bf9968f
--- /dev/null
+++ b/aoc2024/SortedMap.newt
@@ -0,0 +1,58 @@
+module SortedMap
+
+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)
+
+-- There is no empty tree23?
+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)
+
diff --git a/aoc2024/day5/eg.txt b/aoc2024/day5/eg.txt
new file mode 100644
index 0000000..9d146d6
--- /dev/null
+++ b/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
diff --git a/aoc2024/mkday b/aoc2024/mkday
new file mode 100755
index 0000000..66bdc73
--- /dev/null
+++ b/aoc2024/mkday
@@ -0,0 +1,7 @@
+#!/bin/zsh -e
+day=$1
+if [ ! -d day${day} -a ! -z "$1" ]; then
+  echo Make Day ${day}
+  mkdir day${day}
+  sed "s/XX/$day/g" DayXX.newt > Day$day.newt
+fi
diff --git a/newt/Prelude.newt b/newt/Prelude.newt
index d32ed26..95ec484 100644
--- a/newt/Prelude.newt
+++ b/newt/Prelude.newt
@@ -91,18 +91,6 @@ fst (a,b) = a
 
 snd : ∀ a b. a × b → b
 snd (a,b) = b
-
-infixl 6 _<_ _<=_
-class Ord a where
-  _<_ : a → a → Bool
-
-instance Ord Nat where
-  _ < Z = False
-  Z < S _ = True
-  S n < S m = n < m
-
-_<=_ : ∀ a. {{Eq a}} {{Ord a}} → a → a → Bool
-a <= b = a == b || a < b
 -- Monad
 
 class Monad (m : U → U) where
@@ -348,11 +336,6 @@ class HasIO (m : U -> U) where
 instance HasIO IO where
   liftIO a = a
 
-pfunc debugLog uses (MkIORes MkUnit) : ∀ a. a -> IO Unit := `(_,s) => (w) => {
-  console.log(s)
-  return MkIORes(undefined,MkUnit,w)
-}`
-
 pfunc primPutStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
   console.log(s)
   return MkIORes(undefined,MkUnit,w)
@@ -387,7 +370,6 @@ pfunc pack : List Char → String := `(cs) => {
     rval += cs.h1
     cs = cs.h2
   }
-
   return rval
 }
 `
@@ -415,6 +397,9 @@ pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, 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")
@@ -444,9 +429,6 @@ instance Add Int where
 instance Sub Int where
   x - y = subInt x y
 
-instance Ord Int where
-  x < y = ltInt x y
-
 printLn : {m} {{HasIO m}} {a} {{Show a}} → a → m Unit
 printLn a = putStrLn (show a)
 
@@ -633,3 +615,63 @@ 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
+
+-- 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
diff --git a/playground/samples/Day1.newt b/playground/samples/Day1.newt
index 8420e7f..becd768 100644
--- a/playground/samples/Day1.newt
+++ b/playground/samples/Day1.newt
@@ -17,10 +17,6 @@ digits1 (c :: cs) = let x = ord c in
       False => digits1 cs
     False => digits1 cs
 
-tail : {a : U} -> List a -> List a
-tail Nil = Nil
-tail (x :: xs) = xs
-
 -- TODO I used @ patterns in Lean
 digits2 : List Char -> List Int
 digits2 xs = case xs of
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index 6f85f38..f8b70ab 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -96,6 +96,10 @@ solveAutos : Nat -> List MetaEntry -> M ()
 solveAutos mstart [] = pure ()
 solveAutos mstart ((Unsolved fc k ctx ty AutoSolve _) :: es) = do
       debug "AUTO solving \{show k} : \{show ty}"
+      -- fill in solved metas in type
+      x <- quote ctx.lvl ty
+      ty <- eval ctx.env CBN x
+      debug "AUTO ---> \{show ty}"
       -- we want the context here too.
       top <- get
       [(tm, mc)] <- case !(contextMatches ctx ty) of
@@ -138,7 +142,11 @@ logMetas mstart = do
   mc <- readIORef top.metas
   let mlen = length mc.metas `minus` mstart
   for_ (reverse $ take mlen mc.metas) $ \case
-    (Solved fc k soln) => info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
+    (Solved fc k soln) => do
+      -- TODO put a flag on this, vscode is getting overwhelmed and
+      -- dropping errors
+      --info fc "solve \{show k} as \{pprint [] !(quote 0 soln)}"
+      pure ()
     (Unsolved fc k ctx ty User cons) => do
       ty' <- quote ctx.lvl ty
       let names = (toList $ map fst ctx.types)