get delete, leftMost, rightMost, pop working for SortedMap

required fixing an issue in case building.

aoc2024/Day10.newt

@@ -31,12 +31,6 @@ instance Ord Point where
 instance Eq Point where
   (a,b) == (c,d) = a == c && b == d
 
-swap : ∀ a b. a × b → b × a
-swap (a,b) = (b,a)
-
-const : ∀ a b. a → b → a
-const a b = a
-
 -- TODO add parameter a and pass Char -> a into getGrid
 Grid : U
 Grid = SortedMap Point Int

aoc2024/SortedMap.newt

@@ -2,6 +2,10 @@ module SortedMap
 
 import Prelude
 
+-- TODO We'll want to replace Ord/Eq with (a → Ordering) (and rewrite most of our aoc solutions...)
+-- data Ordering : U where
+--   LT EQ GT : Ordering
+
 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
@@ -43,9 +47,127 @@ insertT23 key value (Node3 t1 k1 t2 k2 t3) =
       Left t3' => Left (Node3 t1 k1 t2 k2 t3')
       Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
 
+-- This is cribbed from Idris. Deleting nodes takes a bit of code.
+Hole : Nat → U → U → U
+Hole Z k v = Unit
+Hole (S n) k v = T23 n k v
+
+Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
+
+Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
+
+Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
+
+Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
+
+merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
+merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
+merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
+merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
+merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
+
+-- height is erased in the data everywhere but the top, but needed for case
+-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
+deleteT23 : ∀ k v. {{Ord k}} {{Eq k}} → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
+deleteT23 Z key (Leaf k v) = if k == key then Right MkUnit else Left (Leaf k v)
+deleteT23 (S Z) key (Node2 t1 k1 t2) =
+  if key <= k1
+  then case deleteT23 Z key t1 of
+    Left t1 => Left (Node2 t1 k1 t2)
+    Right _ => Right t2
+  else case deleteT23 Z key t2 of
+    Left t2 => Left (Node2 t1 k1 t2)
+    Right MkUnit => Right t1
+deleteT23 (S Z) key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1
+  then case deleteT23 _ key t1 of
+    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+    Right MkUnit => Left (Node2 t2 k2 t3)
+  else if key <= k2 then case deleteT23 _ key t2 of
+    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+    Right _ => Left (Node2 t1 k1 t3)
+  else case deleteT23 _ key t3 of
+    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+    Right _ => Left (Node2 t1 k1 t2)
+deleteT23 (S (S h)) key (Node2 t1 k1 t2) =
+  if key <= k1
+  then case deleteT23 (S h) key t1 of
+    Left t1 => Left (Node2 t1 k1 t2)
+    Right t1 => case t2 of
+      Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
+      Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
+  else case deleteT23 _ key t2 of
+    Left t2 => Left (Node2 t1 k1 t2)
+    Right t2 => case t1 of
+      Node2 a b c => Right (Node3 a b c k1 t2)
+      Node3 a b c d e => Left (Node4 a b c d e k1 t2)
+deleteT23 (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
+  if key <= k1
+  then case deleteT23 _ key t1 of
+    Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t1 => Left (merge1 t1 k1 t2 k2 t3)
+  else if key <= k2 then case deleteT23 _ key t2 of
+    Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t2 => Left (merge2 t1 k1 t2 k2 t3)
+  else case deleteT23 _ key t3 of
+    Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+    Right t3 => Left (merge3 t1 k1 t2 k2 t3)
+
+treeLeft : ∀ h k v. T23 h k v → (k × v)
+treeLeft (Leaf k v) = (k, v)
+treeLeft (Node2 t1 _ _) = treeLeft t1
+treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
+
+treeRight : ∀ h k v. T23 h k v → (k × v)
+treeRight (Leaf k v) = (k, v)
+treeRight (Node2 _ _ t2) = treeRight t2
+treeRight (Node3 _ _ _ _ t3) = treeRight t3
+
+
 data SortedMap : U -> U -> U where
   EmptyMap : ∀ k v. SortedMap k v
-  MapOf : ∀ k v h. T23 h k v -> SortedMap k v
+  -- not erased so we know what happens in delete
+  MapOf : ∀ k v. {h : Nat} →  T23 h k v -> SortedMap k v
+
+deleteMap : ∀ k v. {{Ord k}} {{Eq k}} → k → SortedMap k v → SortedMap k v
+deleteMap key EmptyMap = EmptyMap
+-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
+deleteMap key (MapOf {k} {v} {Z} tree) = case deleteT23 Z key tree of
+  Left t => MapOf t
+  Right t => EmptyMap
+deleteMap key (MapOf {k} {v} {S n} tree) = case deleteT23 (S n) key tree of
+  Left t => MapOf t
+  Right t => MapOf t
+
+leftMost : ∀ k v. SortedMap k v → Maybe (k × v)
+leftMost EmptyMap = Nothing
+leftMost (MapOf m) = Just (treeLeft m)
+
+rightMost : ∀ k v. SortedMap k v → Maybe (k × v)
+rightMost EmptyMap = Nothing
+rightMost (MapOf m) = Just (treeRight m)
+
+-- TODO issue with metas and case if written as `do` block
+pop : ∀ k v. {{Eq k}} {{Ord k}} → SortedMap k v → Maybe ((k × v) × SortedMap k v)
+pop m = case leftMost m of
+    Just (k,v) => Just ((k,v), deleteMap k m)
+    Nothing => Nothing
 
 lookupMap : ∀ k v. {{Ord k}} {{Eq k}} -> k -> SortedMap k v -> Maybe (k × v)
 lookupMap k EmptyMap = Nothing

newt/Prelude.newt

@@ -637,8 +637,8 @@ instance Cast Int Double where
 instance Applicative IO where
   return a = \ w => MkIORes a w
   f <*> a = \ w =>
-    let (MkIORes f w) = trace "fw" $ f w in
+    let (MkIORes f w) = f w in
-    let (MkIORes a w) = trace "aw" $ a w in
+    let (MkIORes a w) = a w in
     MkIORes (f a) w
 
 class Bifunctor (f : U → U → U) where
@@ -740,3 +740,6 @@ instance Cast Int Nat where
 
 instance Show Char where
   show c = jsShow c
+
+swap : ∀ a b. a × b → b × a
+swap (a,b) = (b,a)

playground/samples/Combinatory.newt

@@ -79,9 +79,10 @@ sapp (CApp K t) I = t
 sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
 -- was out of pattern because of unexpanded lets.
 sapp (CApp K t) u = CApp (CApp B t) u
--- TODO unsolved meta, out of pattern fragment
+-- TODO unsolved meta, out of pattern fragment (now it's skolem - from changes to updateContext?)
+-- so I may need to point the var -> var in another direction (hopefully something simple)
 sapp t (CApp K u) = ? -- CApp (CApp C t) u
--- TODO unsolved meta, out of pattern fragment
+-- TODO unsolved meta, out of pattern fragment (ditto, skolem)
 sapp t u = ? -- CApp (CApp S t) u
 
 abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env))

src/Lib/Elab.idr

@@ -517,13 +517,31 @@ substVal k v tm = go tm
     -- go (VLit x y) = ?rhs_8
 
 
+-- need to turn k into a ground value
+
+-- TODO rework this to do something better.  We've got constraints, and
+-- and may need to do proper unification if it's already defined to a value
+-- below we're handling the case if it's defined to another var, but not
+-- checking for loops.
 updateContext : Context -> List (Nat, Val) -> M Context
 updateContext ctx [] = pure ctx
-updateContext ctx ((k, val) :: cs) = let ix = (length ctx.env `minus` k) `minus` 1 in
+updateContext ctx ((k, val) :: cs) =
-  updateContext ({env $= map (substVal k val), bds $= replaceV ix Defined } ctx) cs
+  let ix = (length ctx.env `minus` k) `minus` 1 in
+  case getAt ix ctx.env of
+    (Just (VVar _ k' [<])) =>
+      if k' /= k
+        then updateContext ctx ((k',val) :: cs)
+        else updateContext ({env $= map (substVal k val), bds $= replaceV ix Defined } ctx) cs
+    (Just val') => do
+      -- This is fine for Z =?= Z but for other stuff, we probably have to match
+      info (getFC val) "need to unify \{show val} and \{show val'} or something"
+      updateContext ctx cs
+    Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext"
+
+  --
   -- updateContext ({env $= replace ix val, bds $= replaceV ix Defined } ctx) cs
   where
-    replace : Nat -> a -> List a -> List a
+    replace : Nat -> Val -> List Val -> List Val
     replace k x [] = []
     replace 0 x (y :: xs) = x :: xs
     replace (S k) x (y :: xs) = y :: replace k x xs
@@ -562,16 +580,29 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
   let (VRef _ sctynm _ _) = scty | _ => error (getFC scty) "case split on non-inductive \{show scty}"
 
   case lookupDef ctx scnm of
+    -- NOW this is S var7
     Just val@(VRef fc nm y sp) =>
       if nm /= dcName
       then do
         debug "SKIP \{dcName} because \{scnm} forced to \{show val}"
         pure Nothing
       else do
-        debug "DOTTED \{dcName} \{show val}"
+        debug "case \{dcName} dotted \{show val}"
+        when (length vars /= length sp) $ error emptyFC "\{show $ length vars} vars /= \{show $ length sp}"
+
+        -- TODO - do we need this one?
+        -- Constrain the scrutinee's variable to be dcon applied to args
+        -- let Just x = findIndex ((==scnm) . fst) ctx'.types
+        --   | Nothing => error ctx.fc "\{scnm} not is scope?"
+        -- let lvl = ((length ctx'.env) `minus` (cast x)) `minus` 1
+        -- let scon : (Nat, Val) = (lvl, VRef ctx.fc dcName (DCon arity dcName) sc)
 
         -- TODO - I think we need to define the context vars to sp via updateContext
 
+        let lvl = (length ctx'.env `minus` length vars)
+        let scons = constrainSpine lvl (sp <>> []) -- REVIEW is this the right order?
+        ctx' <- updateContext ctx' scons
+
         debug "(dcon \{show dcName} ty \{show ty'} scty \{show scty}"
         debug "(dcon \{show dcName}) (vars \{show vars}) clauses were"
         for_ prob.clauses $ (\x => debug "    \{show x}")
@@ -620,6 +651,10 @@ buildCase ctx prob scnm scty (dcName, arity, ty) = do
         tm <- buildTree ctx' (MkProb clauses prob.ty)
         pure $ Just $ CaseCons dcName (map getName vars) tm
   where
+    constrainSpine : Nat -> List Val -> List (Nat, Val)
+    constrainSpine lvl [] = []
+    constrainSpine lvl (v :: vs) = (lvl, v) :: constrainSpine (S lvl) vs
+
     getName : Bind -> String
     getName (MkBind nm _ _) = nm