use record update for top

This commit is contained in:
2026-02-11 13:32:09 -08:00
parent 340457cab7
commit eb9921212c

View File

@@ -154,7 +154,13 @@ processModule importFC base stk qn@(QN ns nm) = do
top <- getTop top <- getTop
let freshMC = MC emptyMap Nil 0 CheckAll let freshMC = MC emptyMap Nil 0 CheckAll
-- set imported, mod, freshMC, ops before processing -- set imported, mod, freshMC, ops before processing
modifyTop (\ top => MkTop top.modules imported emptyMap modns emptyMap freshMC top.verbose top.errors ops) modifyTop [ imported := imported
; hints := emptyMap
; ns := modns
; defs := emptyMap
; metaCtx := freshMC
; ops := ops
]
for imported $ \ ns => do for imported $ \ ns => do
let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing" let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
importHints (listValues mod.modDefs) importHints (listValues mod.modDefs)
@@ -234,7 +240,12 @@ processFile fn = do
top <- getTop top <- getTop
let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules
modifyTop (\ top => MkTop modules (primNS :: Nil) emptyMap Nil emptyMap top.metaCtx top.verbose top.errors top.ops) modifyTop [ modules := modules
; imported := primNS :: Nil
; hints := emptyMap
; ns := Nil
; defs := emptyMap
]
invalidateModule qn invalidateModule qn