From 2794f8fe85f26c31e897418d0721ef4dd9f10a51 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 11 Oct 2025 21:45:26 -0700
Subject: [PATCH] Cleanup some old comments, use record update a bit more

---
 src/Lib/Elab.newt       |  8 ++------
 src/Lib/TopContext.newt | 26 ++++++--------------------
 src/Lib/Types.newt      |  5 +----
 3 files changed, 9 insertions(+), 30 deletions(-)

diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt
index b3d4c81..ed586f0 100644
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -510,7 +510,7 @@ unify env mode t u = do
           vtm <- eval Nil tm
           appvtm <- vappSpine vtm sp'
           unify env mode t appvtm
-        _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]\n  env is \{show env}"
+        _ => error fc' "unify failed \{show t} =?= \{show u} [no Fn]"
 
     unifyRef t@(VRef fc k sp) u = do
       debug $ \ _ => "expand %ref \{show k} \{show sp} =?= \{show u}"
@@ -520,7 +520,7 @@ unify env mode t u = do
           vtm <- eval Nil tm
           tmsp <- vappSpine vtm sp
           unify env mode tmsp u
-        _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}\n  env is \{show env}"
+        _ => error fc "unify failed \{show t} [no Fn] =?= \{show u}"
     unifyRef t u = unifyRest t u
 
     unifyVar : Val -> Val -> M UnifyResult
@@ -783,7 +783,6 @@ updateContext ctx ((k, val) :: cs) =
       updateContext ctx cs
     Nothing => error (getFC val) "INTERNAL ERROR: bad index in updateContext"
   where
-
     replaceV : ∀ a. Nat -> a -> List a -> List a
     replaceV k x Nil = Nil
     replaceV Z x (y :: xs) = x :: xs
@@ -1037,9 +1036,6 @@ checkWhere ctx decls body ty = do
   -- But I'll attempt letrec first
   tm <- buildTree (withPos ctx' defFC) (MkProb clauses' vty)
   vtm <- eval ctx'.env tm
-  -- Should we run the rest with the definition in place?
-  -- I'm wondering if switching from bind to define will mess with metas
-  -- let ctx' = define ctx name vtm vty
   ty' <- checkWhere ctx' decls' body ty
   pure $ LetRec sigFC name funTy tm ty'
 
diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt
index 2d81a2d..babc5f7 100644
--- a/src/Lib/TopContext.newt
+++ b/src/Lib/TopContext.newt
@@ -37,7 +37,7 @@ lookupRaw raw top =
 
 
 instance Show TopContext where
-  show (MkTop _ _ _ _ defs metas _ _ _) = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList defs}]"
+  show top = "\nContext:\n [\{ joinBy "\n" $ map (show ∘ snd) $ toList top.defs}]"
 
 -- TODO need to get class dependencies working
 emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
@@ -52,32 +52,22 @@ setFlag name fc flag = do
   top <- getTop
   let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.defs
     | Nothing => error fc "\{show name} not declared"
-  modifyTop $ \case
-    MkTop mods imp hints ns defs metaCtx verbose errors ops =>
-      let defs = (updateMap name (MkEntry fc name ty def (flag :: flags)) defs) in
-      MkTop mods imp hints ns defs metaCtx verbose errors ops
+  modifyTop $ \ top => [ defs := (updateMap name (MkEntry fc name ty def (flag :: flags)) top.defs) ] top
 
 setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
 setDef name fc ty def flags = do
   top <- getTop
   let (Nothing) = lookupMap' name top.defs
     | Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}"
-  modifyTop $ \case
-    MkTop mods imp hints ns defs metaCtx verbose errors ops =>
-      let defs = (updateMap name (MkEntry fc name ty def flags) top.defs) in
-      MkTop mods imp hints ns defs metaCtx verbose errors ops
-
+  modifyTop $ \top =>
+    [ defs := (updateMap name (MkEntry fc name ty def flags) top.defs)] top
 
 updateDef : QName -> FC -> Tm -> Def -> M Unit
 updateDef name fc ty def = do
   top <- getTop
   let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.defs
     | Nothing => error fc "\{show name} not declared"
-  modifyTop $ \case
-    MkTop mods imp hints ns defs metaCtx verbose errors ops =>
-      let defs = (updateMap name (MkEntry fc' name ty def flags) defs) in
-      MkTop mods imp hints ns defs metaCtx verbose errors ops
-
+  putTop $ [ defs := updateMap name (MkEntry fc' name ty def flags) top.defs ] top
 
 typeName : Tm → Maybe QName
 typeName (Pi fc nm Explicit rig t u) = Nothing
@@ -93,15 +83,11 @@ addHint qn = do
     Just entry => do
       let (Just tyname) = typeName entry.type
         | Nothing => error entry.fc "can't find tcon name for \{show qn}"
-
       let xs = fromMaybe Nil $ lookupMap' tyname top.hints
       let hints = updateMap tyname ((qn, entry.type) :: xs) top.hints
-      putTop $ MkTop top.modules top.imported hints top.ns top.defs top.metaCtx top.verbose top.errors top.ops
-      pure MkUnit
-
+      putTop $ [ hints := hints ] top
     Nothing => pure MkUnit
 
-
 addError : Error -> M Unit
 addError err = do
   top <- getTop
diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt
index 797b2f4..c5544eb 100644
--- a/src/Lib/Types.newt
+++ b/src/Lib/Types.newt
@@ -427,7 +427,6 @@ record TopContext where
   -- Global values
   verbose : Int -- command line flag
   errors : IORef (List Error)
-  -- what do we do here? we can accumulate for now, but we'll want to respect import
   ops : Operators
 
 -- we'll use this for typechecking, but need to keep a TopContext around too.
@@ -445,13 +444,11 @@ record Context where
   ctxFC : FC
 
 -- add a binding to environment
-
 extend : Context -> String -> Val -> Context
 extend (MkCtx lvl env types bds ctxFC) name ty =
   MkCtx (1 + lvl) (VVar emptyFC lvl Lin :: env) ((name,ty) :: types) (Bound :: bds) ctxFC
 
--- I guess we define things as values?
-
+-- add a def to the environment
 define : Context -> String -> Val -> Val -> Context
 define (MkCtx lvl env types bds ctxFC) name val ty =
   MkCtx (1 + lvl) (val :: env) ((name,ty) :: types) (Defined :: bds) ctxFC