monadic version of day21

TODO.md

@@ -48,7 +48,7 @@ More comments in code! This is getting big enough that I need to re-find my bear
   - [x] Support @ on the LHS
   - [x] if / then / else sugar
   - [ ] `data Foo = A | B` sugar
-  - [ ] records
+  - [x] records
   - [x] where
   - [ ] add namespaces
   - [ ] magic nat?
@@ -154,7 +154,8 @@ More comments in code! This is getting big enough that I need to re-find my bear
   - [x] check quantity
   - [x] erase in output
   - [ ] remove erased top level arguments
-- [ ] type at point in vscode NOW
+- [x] top level at point in vscode
+- [ ] in-scope type at point in vscode
 - [ ] repl
 - [ ] LSP
 - [x] don't match forced constructors at runtime

aoc2024/Day21.newt

@@ -71,11 +71,10 @@ seqCost : Point → List Point → Keypad × Int → Keypad × Int
 seqCost cur Nil (kp, cost) = (kp, cost)
 seqCost cur (pt :: pts) (kp, cost) =
   let (kp, cost') = pathCost cur pt kp in
-  let x = cost' in
   seqCost pt pts (kp, cost + cost')
 
 -- cost of best path from -> to in kp
-pathCost from to kp = do
+pathCost from to kp =
   case lookupMap (from, to) (costs kp) of
     Just (_, cost) => (kp, cost)
     Nothing =>
@@ -124,6 +123,7 @@ run fn = do
 
   -- the space is illegal spot
   let numpad = fromList $ filter (not ∘ _==_ ' ' ∘ fst) $ gridPoints "789\n456\n123\n 0A"
+  debugLog $ toList numpad
 
   let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing
   let robn = makeKeypad 2 rob1

aoc2024/Day21monad.newt

@@ -0,0 +1,178 @@
+module Day21monad
+
+import Prelude
+import Node
+import Aoc
+import SortedMap
+import Parser
+
+record State st a where
+  constructor ST
+  runState : st → (st × a)
+
+instance ∀ st. Applicative (State st) where
+  return x = ST (\st => (st, x))
+  (ST sf) <*> (ST sx) = ST $ \st =>
+    let (st', f) = sf st in
+    let (st'', x) = sx st' in
+    (st'', f x)
+
+instance ∀ st. Monad (State st) where
+  pure x = ST (\st => (st, x))
+  bind (ST run) f = ST $ \st =>
+    let (st', a) = run st in
+    let (ST run') = f a in
+    run' st'
+
+get : ∀ st. State st st
+get = ST (\st => (st, st))
+
+put : ∀ st. st → State st Unit
+put st = ST (\_ => (st, MkUnit))
+
+
+min : Int → Int → Int
+min a b = if a < b then a else b
+
+gridPoints : String → List (Char × Int × Int)
+gridPoints text = go 0 0 (unpack text) Nil
+  where
+    -- might as well be tail recursive
+    go : Int → Int → List Char → List (Char × Int × Int) → List (Char × Int × Int)
+    go row col Nil points = points
+    go row col ('\n' :: cs) points = go (row + 1) 0 cs points
+    go row col (c :: cs) points = go row (col + 1) cs ((c,row,col) :: points)
+
+data Dir : U where North East South West : Dir
+
+dirs : List Dir
+dirs = (North :: South :: East :: West :: Nil)
+
+move : Point → Dir → Point
+move (r, c) North  = (r - 1, c)
+move (r, c) East   = (r, c + 1)
+move (r, c) South  = (r + 1, c)
+move (r, c) West   = (r, c - 1)
+
+Costs : U
+Costs = SortedMap (Point × Point) Int
+
+-- linked list of keypads
+record Keypad where
+  constructor KP
+  name : String
+  start : Point
+  interdit : Point
+  costs : Costs -- cache of costs
+  next : Maybe Keypad
+
+getPaths : Point → Point → Point → List (List Dir)
+getPaths interdit pt@(a,b) to@(c,d) =
+  if pt == to then Nil :: Nil else
+  if pt == interdit then Nil else
+  join $ map check dirs
+  where
+    check : Dir → List (List Dir)
+    check North = if c < a then map (_::_ North) $ getPaths interdit (move pt North) (c,d) else Nil
+    check South = if a < c then map (_::_ South) $ getPaths interdit (move pt South) (c,d) else Nil
+    check East = if b < d then map (_::_ East) $ getPaths interdit (move pt East) (c,d) else Nil
+    check West = if d < b then map (_::_ West) $ getPaths interdit (move pt West) (c,d) else Nil
+
+updateCost : Point × Point → Int → State Keypad Unit
+updateCost path cost = do
+  kp <- get
+  put (KP (name kp) (start kp) (interdit kp) (updateMap path cost (costs kp)) (next kp))
+
+keyPos : Dir → Point
+keyPos North = (0,1)
+keyPos South = (1,1)
+keyPos East  = (1,2)
+keyPos West  = (1,0)
+
+-- cost to run a path in a keypad
+pathCost : Point → Point → State Keypad Int
+
+-- cost of sequence of points (run in parent keypad)
+-- for numpad, we pick points from the map, for the rest map keyPos ...
+seqCost : Point → List Point → Int → State Keypad Int
+seqCost cur Nil cost = pure cost
+seqCost cur (pt :: pts) cost = do
+  cost' <- pathCost cur pt
+  seqCost pt pts (cost + cost')
+
+-- cost of best path from -> to in kp
+pathCost from to = do
+  kp <- get {Keypad}
+  case lookupMap (from, to) (costs kp) of
+    Just (_, cost) => pure {State Keypad} cost
+    Nothing =>
+      let (path :: paths) = getPaths (interdit kp) from to | _ => ? in
+      case kp of
+        (KP n s i c Nothing) => pure 1
+        (KP n s i c (Just kp')) => do
+          put kp'
+          cost <- mincost path paths
+          kp' <- get
+          put $ KP n s i c (Just kp')
+          -- need to ensure cost goes into correct kp
+          updateCost (from,to) cost
+          pure cost
+  where
+    xlate : List Dir → Point -> List Point
+    xlate Nil a = a :: Nil
+    xlate (d :: ds) a = keyPos d :: xlate ds a
+
+    mincost : List Dir → List (List Dir) → State Keypad Int
+    mincost path paths = do
+      kp <- get
+      cost <- seqCost (0,2) (xlate path $ start kp) 0
+      case paths of
+        Nil => pure cost
+        (path :: paths) => do
+          cost' <- mincost path paths
+          pure $ min cost cost'
+
+fromList : ∀ k v. {{Ord k}} {{Eq k}} → List (k × v) → SortedMap k v
+fromList xs = foldMap (\ a b => b) EmptyMap xs
+
+getNum : String → Int
+getNum str = case number (unpack str) of
+  Right (n, _) => n
+  _ => 0
+
+runOne : SortedMap Char Point → String → State Keypad (Int × Int)
+runOne numpad str = do
+  let pts = map snd $ mapMaybe (flip lookupMap numpad) $ unpack str
+  res <- seqCost (3,2) pts 0
+  pure (getNum str, res)
+
+makeKeypad : Int → Keypad -> Keypad
+makeKeypad 0 kp = kp
+makeKeypad n kp = makeKeypad (n - 1) $ KP (show n) (0,2) (0,0) EmptyMap (Just kp)
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let codes = split (trim text) "\n"
+
+  -- the space is illegal spot
+  let numpad = fromList $ filter (not ∘ _==_ ' ' ∘ fst) $ gridPoints "789\n456\n123\n 0A"
+  debugLog $ toList numpad
+
+  let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing
+  let robn = makeKeypad 2 rob1
+  let kp = KP "kp" (3,2) (3,0) EmptyMap (Just robn)
+  let p1 = foldl _+_ 0 $ map (uncurry _*_) $ snd $ runState (traverse (runOne numpad) codes) kp
+  putStrLn $ "part1 " ++ show p1
+
+  let rob1 = KP "r1" (0,2) (0,0) EmptyMap Nothing
+  let robn = makeKeypad 25 rob1
+  let kp = KP "kp" (3,2) (3,0) EmptyMap (Just robn)
+  let p2 = foldl _+_ 0 $ map (uncurry _*_) $ snd $ runState (traverse (runOne numpad) codes) kp
+  putStrLn $ "part2 " ++ show p2
+
+main : IO Unit
+main = do
+  run "aoc2024/day21/eg.txt"
+  run "aoc2024/day21/input.txt"

src/Lib/Elab.idr

@@ -724,7 +724,7 @@ mkPat : TopContext -> (Raw, Icit) -> M Pattern
 mkPat top (RAs fc as tm, icit) =
   case !(mkPat top (tm, icit)) of
     (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
-    (PatCon fc icit nm args Nothing) => error fc "Double as pattern \{show tm}"
+    (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}"
     t => error fc "Can't put as on non-constructor \{show tm}"
 mkPat top (tm, icit) = do
   case splitArgs tm [] of