dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

use new record update syntax

Browse Source
This commit is contained in:
Steve Dunham
2026-03-29 10:19:29 -07:00
parent ba519bdc7f
commit ee9664838f
6 changed files with 38 additions and 38 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Commands.newt
View File

@@ -38,7 +38,7 @@ switchModule repo modns = do
top <- getTop
-- mod <- processModule emptyFC repo Nil modns
let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing
modifyTop [ currentMod := mod; ops := mod.modOps ]
modifyTop { currentMod := mod; ops := mod.modOps }
pure $ Just mod
data HoverInfo = NoHoverInfo | NeedCheck | HasHover FC String

24
src/LSP.newt
View File

@@ -68,12 +68,12 @@ lspFileSource = do
updateFile : String → String → Unit
updateFile fn src = unsafePerformIO $ do
modifyIORef state [ files $= updateMap fn src ]
modifyIORef state { files $= updateMap fn src }
st <- readIORef state
let (base,modName) = decomposeName fn
Right (ctx,_) <- (invalidateModule modName).runM st.topContext
| _ => writeIORef state st
modifyIORef state [ topContext := ctx ]
modifyIORef state { topContext := ctx }
fcToRange : FC → Json
@@ -96,17 +96,17 @@ hoverInfo uri line col = unsafePerformIO $ do
-- We're proactively running check if there is no module information, make sure we save it
Right (top, HasHover fc msg) <- (getHoverInfo repo modns line col).runM st.topContext
| Right (top, NeedCheck) => do
modifyIORef state $ [ topContext := top ]
modifyIORef state $ { topContext := top }
putStrLn $ "NeedsCheck"
pure $ js_castBool True
| Right (top, NoHoverInfo) => do
modifyIORef state $ [ topContext := top ]
modifyIORef state $ { topContext := top }
putStrLn $ "Nothing to see here"
pure $ js_castBool True
| Left err => do
putStrLn $ showError "" err
pure $ jsonToJObject JsonNull
modifyIORef state $ [ topContext := top ]
modifyIORef state $ { topContext := top }
let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil
pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil
@@ -126,7 +126,7 @@ codeActionInfo uri line col = unsafePerformIO $ do
putStrLn "ACTIONS ERROR"
putStrLn $ showError "" err
pure js_null
modifyIORef state $ [ topContext := top ]
modifyIORef state $ { topContext := top }
pure $ jsonToJObject $ JsonArray $ map actionToJson actions
where
single : String → Json → Json
@@ -238,7 +238,7 @@ checkFile fn = unsafePerformIO $ do
(Right (top, json)) <- (do
putStrLn "processModule"
mod <- processModule emptyFC repo Nil modName
modifyTop [ currentMod := mod; ops := mod.modOps ]
modifyTop { currentMod := mod; ops := mod.modOps }
-- pull out errors and infos
top <- getTop
@@ -251,7 +251,7 @@ checkFile fn = unsafePerformIO $ do
putStrLn $ showError "" err
pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
-- Cache loaded modules
modifyIORef state $ [ topContext := top ]
modifyIORef state $ { topContext := top }
pure $ jsonToJObject $ JsonArray json
docSymbols : String → JSObject
@@ -265,11 +265,11 @@ docSymbols fn = unsafePerformIO $ do
repo <- lspFileSource
(Right (top, json)) <- (do
mod <- processModule emptyFC repo Nil modName
modifyTop [ currentMod := mod; ops := mod.modOps ]
modifyTop { currentMod := mod; ops := mod.modOps }
getSymbols).runM st.topContext
| Left err => do
pure $ jsonToJObject $ JsonNull
modifyIORef state $ [ topContext := top ]
modifyIORef state $ { topContext := top }
pure $ jsonToJObject $ JsonArray json
compileJS : String → JSObject
@@ -287,7 +287,7 @@ compileJS fn = unsafePerformIO $ do
++ map (render 90 ∘ noAlt) docs
pure src).runM st.topContext
| Left err => pure $ js_castStr "// \{errorMsg err}"
modifyIORef state [ topContext := top ]
modifyIORef state { topContext := top }
pure $ js_castStr src
compileToScheme : String → JSObject
@@ -302,7 +302,7 @@ compileToScheme fn = unsafePerformIO $ do
let src = unlines docs
pure src).runM st.topContext
| Left err => pure $ js_castStr ";; \{errorMsg err}"
modifyIORef state [ topContext := top ]
modifyIORef state { topContext := top }
pure $ js_castStr src
#export updateFile checkFile hoverInfo codeActionInfo compileJS docSymbols compileToScheme

8
src/Lib/Elab.newt
View File

@@ -118,10 +118,10 @@ isCandidate _ _ = False
setMetaMode : MetaMode → M Unit
-- ideally we would support dotted paths like metaCtx.mcmode := CheckFirst
setMetaMode mcmode = modifyTop [ currentMod $= [modMetaCtx $= [mcmode := mcmode] ] ]
setMetaMode mcmode = modifyTop { currentMod $= {modMetaCtx $= {mcmode := mcmode} } }
setMetaContext : MetaContext → M Unit
setMetaContext mc = modifyTop [ currentMod $= [ modMetaCtx := mc ]]
setMetaContext mc = modifyTop { currentMod $= { modMetaCtx := mc }}
findMatches : Context -> Val -> List (QName × Tm) -> M (List QName)
findMatches ctx ty Nil = pure Nil
@@ -255,7 +255,7 @@ updateMeta ix f = do
let autos = case me of
Solved _ _ _ => filter (_/=_ ix) mc.autos
_ => mc.autos
setMetaContext $ [metas $= updateMap ix me; autos := autos] mc
setMetaContext $ {metas $= updateMap ix me; autos := autos} mc
-- Try to solve autos that reference the meta ix
checkAutos : QName -> List QName -> M Unit
@@ -618,7 +618,7 @@ freshMeta ctx fc ty kind = do
let autos = case kind of
AutoSolve => qn :: mc.autos
_ => mc.autos
setMetaContext $ [ metas $= updateMap qn newmeta; autos := autos; next $= 1 +] mc
setMetaContext $ { metas $= updateMap qn newmeta; autos := autos; next $= 1 +} mc
-- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
pure $ applyBDs 0 (Meta fc qn) ctx.bds

22
src/Lib/ProcessModule.newt
View File

@@ -17,13 +17,13 @@ import Lib.Elab
-- declare internal primitives
addPrimitives : M ModContext
addPrimitives = do
modifyTop [ currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap ]
modifyTop { currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap }
processDecl primNS (PType emptyFC "Int" Nothing)
processDecl primNS (PType emptyFC "String" Nothing)
processDecl primNS (PType emptyFC "Char" Nothing)
setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil
top <- getTop
modifyTop [ modules $= updateMap primNS top.currentMod ]
modifyTop { modules $= updateMap primNS top.currentMod }
pure top.currentMod
record FileSource where
@@ -74,12 +74,12 @@ processModule importFC repo stk modns = do
-- Dummy for initial load/parse
let mod = MkModCtx modns "" emptyMap freshMC emptyMap Nil Nil Nil
modifyTop [ currentMod := mod; hints := emptyMap; ops := emptyMap ]
modifyTop { currentMod := mod; hints := emptyMap; ops := emptyMap }
-- TODO now we can pass in the module name...
Right (fn,src) <- tryError $ repo.getFile importFC fn
| Left err => reportError err -- TODO maybe want a better FC.
modifyTop [ currentMod $= [ modSource := src ]]
modifyTop { currentMod $= { modSource := src }}
let (Right toks) = tokenise fn src
| Left err => reportError err
@@ -108,10 +108,10 @@ processModule importFC repo stk modns = do
-- currentMod has been wiped by imports..
let freshMC = MC emptyMap Nil 0 CheckAll
let mod = MkModCtx modns src emptyMap freshMC emptyMap imported Nil Nil
modifyTop [ currentMod := mod
modifyTop { currentMod := mod
; hints := emptyMap
; ops := ops
]
}
-- top hints / ops include all directly imported modules
top <- getTop
@@ -119,7 +119,7 @@ processModule importFC repo stk modns = do
(MkImport fc (nameFC, ns)) => do
let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
importHints (listValues mod.modDefs)
modifyTop [ ops $= mergeOps mod.modOps ]
modifyTop { ops $= mergeOps mod.modOps }
-- add error if an import contains an error
-- maybe move this to after reporting
@@ -135,7 +135,7 @@ processModule importFC repo stk modns = do
-- aside from reworking parsing, we could filter
-- other options are removing updates from parsing (so we must use incremental parsing)
-- or removing pratt from parsing (so it happens in elaboration)
modifyTop [ currentMod $= [ modOps := ops ] ]
modifyTop { currentMod $= { modOps := ops } }
log 1 $ \ _ => "process Decls"
traverse (tryProcessDecl src modns) (collectDecl decls)
@@ -151,7 +151,7 @@ processModule importFC repo stk modns = do
-- update modules with result, leave the rest of context in case this is top file
top <- getTop
let modules = updateMap modns top.currentMod top.modules
modifyTop [modules := modules]
modifyTop {modules := modules}
pure top.currentMod
where
@@ -159,7 +159,7 @@ processModule importFC repo stk modns = do
reportError err = do
addError err
top <- getTop
modifyTop [modules $= updateMap modns top.currentMod ]
modifyTop {modules $= updateMap modns top.currentMod }
pure top.currentMod
tryProcessDecl : String → String → Decl → M Unit
@@ -174,7 +174,7 @@ invalidateModule modname = do
let modules = join $ map getDeps $ toList top.modules
let revMap = map swap modules
let deps = foldl accumulate emptyMap revMap
modifyTop [ modules $= go deps (modname :: Nil) ]
modifyTop { modules $= go deps (modname :: Nil) }
where
accumulate : SortedMap String (List String) → String × String → SortedMap String (List String)
accumulate deps (k,v) = let prev = fromMaybe Nil $ lookupMap' k deps

14
src/Lib/TopContext.newt
View File

@@ -53,7 +53,7 @@ setFlag name fc flag = do
top <- getTop
let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.currentMod.modDefs
| Nothing => error fc "\{show name} not declared"
modifyTop [ currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))] ]
modifyTop { currentMod $= { modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))} }
setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
setDef name fc ty def flags = do
@@ -61,14 +61,14 @@ setDef name fc ty def flags = do
let (Nothing) = lookupMap' name top.currentMod.modDefs
| Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}"
modifyTop [currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def flags))] ]
modifyTop {currentMod $= { modDefs $= (updateMap name (MkEntry fc name ty def flags))} }
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.currentMod.modDefs
| Nothing => error fc "\{show name} not declared"
modifyTop [ currentMod $= [ modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs ] ]
modifyTop { currentMod $= { modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs } }
typeName : Tm → Maybe QName
typeName (Pi fc nm Explicit rig t u) = Nothing
@@ -86,18 +86,18 @@ addHint qn = do
| 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
modifyTop [ hints := hints ]
modifyTop { hints := hints }
Nothing => pure MkUnit
addError : Error -> M Unit
addError err = modifyTop [ currentMod $= [ modErrors $= (err ::) ] ]
addError err = modifyTop { currentMod $= { modErrors $= (err ::) } }
addInfo : EditorInfo → M Unit
addInfo info = modifyTop [ currentMod $= [modInfos $= (info ::) ] ]
addInfo info = modifyTop { currentMod $= {modInfos $= (info ::) } }
-- temporary? used in derive for now
freshName : String → M String
freshName nm = do
top <- getTop
modifyTop [ freshIx $= 1 + ]
modifyTop { freshIx $= 1 + }
pure $ "f$" ++ nm ++ show top.freshIx

6
src/Main.newt
View File

@@ -114,7 +114,7 @@ cmdLine : List String -> M (Maybe String × List String)
cmdLine Nil = pure (Nothing, Nil)
cmdLine ("--top" :: args) = cmdLine args -- handled later
cmdLine ("-v" :: args) = do
modifyTop [ verbose $= _+_ 1 ]
modifyTop { verbose $= _+_ 1 }
cmdLine args
cmdLine ("-o" :: fn :: args) = do
(out, files) <- cmdLine args
@@ -166,8 +166,8 @@ runCommand (Load fn) = processFile fn
runCommand (HelpCmd) = replHelp
runCommand (BrowseCmd qn) = browseTop qn
runCommand (GetDoc name) = getDoc name
runCommand (Verbose Nothing) = modifyTop [ verbose $= _+_ 1 ]
runCommand (Verbose (Just v)) = modifyTop [ verbose := v ]
runCommand (Verbose Nothing) = modifyTop { verbose $= _+_ 1 }
runCommand (Verbose (Just v)) = modifyTop { verbose := v }
runCommand (OutputJS fn) = writeSource fn
runCommand DumpTop = do
json <- jsonTopContext