Switch to esm, add #export statement to newt, tweaks to LSP

This commit is contained in:
2026-02-21 15:08:15 -08:00
parent c54b856f0b
commit 0a5ad3cc9b
22 changed files with 251 additions and 165 deletions

View File

@@ -25,17 +25,22 @@ decomposeName fn =
then go (x :: acc) xs
else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc)
switchModule : FileSource String M ModContext
switchModule repo modns = do
addPrimitives
modifyTop [ metaCtx := MC emptyMap Nil 0 CheckAll ]
mod <- processModule emptyFC repo Nil modns
-- FIXME keep these in ModContext, drop from TopContext
modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps; infos := mod.modInfos; ns := modns; errors := mod.modErrors ]
top <- getTop
pure mod
-- The cheap version of type at point, find the token, lookup in global context
-- Later we will either get good FC for entries or scan them all and build a cache.
getHoverInfo : FileSource String Int Int M (Maybe (String × FC))
getHoverInfo repo modns row col = do
-- REVIEW consider not running processModule and returning empty if it hasn't been processed yet
-- For Elab.newt, there would be a 1.5s delay...
mod <- processModule emptyFC repo Nil modns
-- not necessarily loaded into top... (Maybe push this down into that branch of processModule)
-- FIXME - fragile - this is why we don't want this stuff directly in TopContext
modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps; infos := mod.modInfos]
mod <- switchModule repo modns
top <- getTop
-- Find the token at the point
@@ -154,6 +159,7 @@ getCaseSplit row col fc@(MkFC uri (MkBounds sr sc er ec)) ctx nm scty = do
ty <- quote (length' ctx.env) scty
cons <- filterM (checkCase ctx nm scty) cons
let names = map fst cons
putStrLn "Make splits for \{show names}"
edits <- makeEdits fc names True
pure $ Just $ CaseSplitAction edits
@@ -163,9 +169,7 @@ posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (s
getActions : FileSource String Int Int M (List CodeAction)
getActions repo modns row col = do
mod <- processModule emptyFC repo Nil modns
-- not necessarily loaded into top... (Maybe push this down into that branch of processModule)
modifyTop [ defs := mod.modDefs; metaCtx := mod.modMetaCtx; ops := mod.ctxOps; imported := mod.modDeps; infos := mod.modInfos]
mod <- switchModule repo modns
top <- getTop
let xx = filter (posInFC row col getFC) top.infos
putStrLn "Filter got \{show $ length' xx}"

View File

@@ -122,6 +122,7 @@ codeActionInfo uri line col = unsafePerformIO $ do
putStrLn "\{show $ length' actions} actions"
pure actions).runM st.topContext
| Left err => do
putStrLn "ACTIONS ERROR"
putStrLn $ showError "" err
pure js_null
modifyIORef state $ [ topContext := top ]
@@ -195,8 +196,8 @@ checkFile fn = unsafePerformIO $ do
(Right (top, json)) <- (do
modifyTop [ errors := Nil ]
putStrLn "processModule"
_ <- processModule emptyFC lspFileSource Nil modName
pure MkUnit
_ <- switchModule lspFileSource modName
-- pull out errors and infos
top <- getTop
let errors = map (errorToDiag) top.errors
@@ -215,4 +216,7 @@ checkFile fn = unsafePerformIO $ do
-- Dummy main function with references to force functions into ouput file.
-- but we don't get `export` on it..
-- #export updateFile checkFile hoverInfo
pfunc main uses (updateFile checkFile hoverInfo codeActionInfo) : IO Unit := `() => {}`
#export updateFile checkFile hoverInfo codeActionInfo
-- pfunc main uses (updateFile checkFile hoverInfo codeActionInfo) : IO Unit := `() => {}`

View File

@@ -414,10 +414,13 @@ we're visiting shallow or deep. We're trying to avoid hitting issues with indire
- Shallow represents the declaration, so we filter to those at the end
TODO this could be made faster by keeping a map of the done information
REVIEW could I avoid most of this by using `function` instead of arrow functions?
-/
sortedNames : SortedMap QName CExp QName List QName
sortedNames defs qn = map snd $ filter (not fst) $ go Nil Nil (True, qn)
sortedNames : SortedMap QName CExp List QName List QName
sortedNames defs names =
map snd $ filter (not fst) $ foldl (go Nil) Nil $ map (True,) names
where
getBody : CAlt CExp
getBody (CConAlt _ _ _ _ t) = t
@@ -483,10 +486,10 @@ eraseEntries = do
go _ = pure MkUnit
-- given a initial function, return a dependency-ordered list of javascript source
process : QName M (List Doc)
process name = do
process : List QName M (List Doc)
process names = do
top <- getTop
entries <- getEntries emptyMap name
entries <- foldlM getEntries emptyMap names
-- Maybe move this dance into liftWhere
ref <- newIORef entries
@@ -500,18 +503,35 @@ process name = do
cexpMap <- tailCallOpt cexpMap
-- Not needed for JS, uncomment to test
-- cexpMap <- liftLambda cexpMap
let names = sortedNames cexpMap name
pure $ map cexpToDoc $ mapMaybe (\x => lookupMap x cexpMap) names
let names = sortedNames cexpMap names
pure $ mapMaybe (go cexpMap) names
where
go : ExpMap QName Maybe Doc
go cexpMap name = do
cexp <- lookupMap name cexpMap
if elem name names
then Just $ text "export" <+> cexpToDoc cexp
else Just $ cexpToDoc cexp
compile : M (List Doc)
compile = do
top <- getTop
case lookupRaw "main" top of
Just (MkEntry fc name type def _) => do
tmp <- process name
-- tack on call to main function
let exec = stmtToDoc $ JPlain $ Apply (Var $ show name) Nil
pure $ reverse (exec :: tmp)
Nothing =>
-- TODO maybe emit everything if there is no main
error emptyFC "No main function found"
let exports = getExports Nil $ listValues top.defs
let mainName = (QN top.ns "main")
let main = lookup mainName top
let todo = case main of
Nothing => exports
Just _ => mainName :: exports
defs <- process todo
case lookup mainName top of
Just _ => -- tack on call to main function
let exec = stmtToDoc $ JPlain $ Apply (Var $ show mainName) Nil
in pure $ reverse (exec :: defs)
Nothing => pure $ reverse defs
where
getExports : List QName List TopEntry List QName
getExports acc Nil = acc
getExports acc ((MkEntry fc name@(QN ns nm) type def eflags) :: rest) =
let acc = if elem Export eflags then name :: acc else acc
in getExports acc rest

View File

@@ -493,22 +493,18 @@ unify env mode t u = do
unifyRest t' u' = error (getFC t') "unify failed \{show t'} =?= \{show u'} \n env is \{show env}"
unifyRef : Val -> Val -> M UnifyResult
unifyRef t'@(VRef fc k sp) u'@(VRef fc' k' sp') =
unifyRef t'@(VRef fc k sp) u'@(VRef fc' k' sp') = do
-- unifySpine is a problem for cmp (S x) (S y) =?= cmp x y
do
-- catchError(unifySpine env mode (k == k') sp sp') $ \ err => do
Nothing <- tryEval env t'
| Just v => do
debug $ \ _ => "tryEval \{show t'} to \{show v}"
unify env mode v u'
Nothing <- tryEval env u'
| Just v => unify env mode t' v
if k == k'
then unifySpine env mode (k == k') sp sp'
else error fc "vref mismatch \{show t'} =?= \{show u'}"
Nothing <- tryEval env t'
| Just v => do
debug $ \ _ => "tryEval \{show t'} to \{show v}"
unify env mode v u'
Nothing <- tryEval env u'
| Just v => unify env mode t' v
if k == k'
then unifySpine env mode (k == k') sp sp'
else error fc "vref mismatch \{show t'} =?= \{show u'}"
-- Lennart.newt cursed type references itself
-- We _could_ look up the ref, eval against Nil and vappSpine...
unifyRef t u@(VRef fc' k' sp') = do
debug $ \ _ => "expand \{show t} =?= %ref \{show k'}"
top <- getTop
@@ -1488,7 +1484,7 @@ check ctx tm ty = do
error fc "Icity issue checking \{show t} at \{show ty}"
(t@(RLam _ (BI fc nm icit quant) tm), ty) => do
pty <- prvalCtx ty
error fc "Expected pi type, got \{pty}"
error fc "Expected \{pty}, got pi type"
(RLet fc nm ty v sc, rty) => do
ty' <- check ctx ty (VU emptyFC)

View File

@@ -669,11 +669,18 @@ parseInstance = do
parseNorm : Parser Decl
parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*> typeExpr
parseExport : Parser Decl
parseExport = do
loc <- getPos
keyword "#export"
names <- many $ withFC ident
pure $ Exports loc names
parseDecl : Parser Decl
parseDecl = parseMixfix <|> parsePType <|> parsePFunc
<|> parseNorm <|> parseData <|> parseShortData
<|> parseClass <|> parseInstance <|> parseRecord
<|> parseExport
-- We'll put the backtracing stuff last, but there is a commit issue in parseDef
<|> parseSig <|> parseDef

View File

@@ -206,7 +206,7 @@ token' : Kind -> Parser String
token' k = satisfy (\t => t.val.kind == k) "Expected a \{show k} token"
keyword' : String -> Parser Unit
keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number)) "Expected '\{kw}'"
keyword' kw = ignore $ satisfy (\t => t.val.text == kw && (t.val.kind == Keyword || t.val.kind == Symbol || t.val.kind == Number || t.val.kind == Pragma)) "Expected '\{kw}'"
-- expect indented token of given kind

View File

@@ -529,6 +529,16 @@ processRecord ns recordFC (nameFC, nm) tele cname decls = do
let deps = ((name, RApp fc (RVar fc pname) (RVar fc "$self") Explicit) :: deps)
processFields autoPat tail deps rest
processExports : String FC List (FC × String) M Unit
processExports ns fc names = do
top <- getTop
traverse_ (setExport top) names
where
setExport : TopContext FC × String M Unit
setExport top (fc, name) = do
let (Just entry) = lookupRaw name top | _ => error fc "\{name} not in scope"
setFlag entry.name fc Export
-- currently mixfix registration is handled in the parser
-- since we now run a decl at a time we could do it here.
processDecl ns (PMixFix _ _ _ _) = pure MkUnit
@@ -544,3 +554,4 @@ processDecl ns (Data fc nm ty (Just cons)) = processData ns fc nm ty cons
-- TODO distinguish from function signatures
processDecl ns (Data fc (_, nm) ty Nothing) = processTypeSig ns fc (nm :: Nil) ty
processDecl ns (Record recordFC nm tele cname decls) = processRecord ns recordFC nm tele cname decls
processDecl ns (Exports fc names) = processExports ns fc names

View File

@@ -97,10 +97,12 @@ data Decl
| Class FC (FC × Name) Telescope (List Decl)
| Instance FC Raw (Maybe (List Decl))
| Record FC (FC × Name) Telescope (Maybe $ FC × Name) (List Decl)
| Exports FC (List $ FC × Name)
instance HasFC Decl where
getFC (TypeSig x strs tm) = x
getFC (Exports x _) = x
getFC (FunDef x str xs) = x
getFC (DCheck x tm tm1) = x
getFC (Data x str tm xs) = x
@@ -148,6 +150,7 @@ instance Show Decl where
show (Class _ (_,nm) tele decls) = foo ("Class" :: nm :: "..." :: (show $ map show decls) :: Nil)
show (Instance _ nm decls) = foo ("Instance" :: show nm :: (show $ map show decls) :: Nil)
show (Record _ nm tele nm1 decls) = foo ("Record" :: show nm :: show tele :: show nm1 :: show decls :: Nil)
show (Exports _ nms) = foo ("Exports" :: show nms :: Nil)
instance Show Module where
@@ -263,6 +266,7 @@ instance Pretty Decl where
<+> (nest 2 $ text "where" </> stack (map pretty decls))
pretty (Instance _ _ _) = text "TODO pretty Instance"
pretty (ShortData _ lhs sigs) = text "data" <+> pretty lhs <+> text "=" <+> pipeSep (map pretty sigs)
pretty (Exports _ nms) = text "#export" <+> spread (map (text show snd) nms)
lhsNames : Raw List String
lhsNames tm = case tm of

View File

@@ -221,18 +221,11 @@ data VCaseAlt : U where
VCaseCons : (name : QName) -> (args : List String) -> Env -> Tm -> VCaseAlt
VCaseLit : Literal -> Val -> VCaseAlt
VCaseDefault : Val -> VCaseAlt
-- VCaseCons : (name : QName) -> (args : List String) -> Tm -> VCaseAlt
-- VCaseLit : Literal -> Tm -> VCaseAlt
-- VCaseDefault : Tm -> VCaseAlt
data Val : U where
-- This will be local / flex with spine.
VVar : FC -> (k : Int) -> (sp : SnocList Val) -> Val
VRef : FC -> (nm : QName) -> (sp : SnocList Val) -> Val
-- neutral case
VCase : FC -> (sc : Val) -> List VCaseAlt -> Val
-- we'll need to look this up in ctx with IO
VMeta : FC -> QName -> (sp : SnocList Val) -> Val
VLam : FC -> Name -> Icit -> Quant -> Closure -> Val
VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val
@@ -374,15 +367,17 @@ instance Show Def where
-- entry in the top level context
data EFlag = Hint | Inline
data EFlag = Hint | Inline | Export
instance Show EFlag where
show Hint = "hint"
show Inline = "inline"
show Export = "export"
instance Eq EFlag where
Hint == Hint = True
Inline == Inline = True
Export == Export = True
_ == _ = False
record TopEntry where
@@ -601,7 +596,7 @@ lookupMeta ix@(QN ns nm) = do
Just meta => pure meta
Nothing => case lookupMap' ns top.modules of
Nothing =>
error emptyFC "missing module: \{show ns}"
error emptyFC "missing module: \{show ns} looking up meta \{show ix}"
Just mod => case lookupMap' ix mod.modMetaCtx.metas of
Nothing =>
error emptyFC "missing meta: \{show ix}"
@@ -641,3 +636,13 @@ instance Show Pattern where
data Constraint = PC String Pattern Val
instance Show Constraint where
show (PC nm pat ty) = show (nm,pat,ty)
-- Lazy because `let` would do work at the top of a `M a`
prof : a. String Lazy (M a) M a
prof desc work = do
start <- getTime
res <- force work
end <- getTime
putStrLn "PROF \{desc} \{show $ end - start} ms"
pure res

View File

@@ -46,7 +46,7 @@ writeSource : String -> M Unit
writeSource fn = do
docs <- compile
let src = unlines $
( "\"use strict\";"
( "import fs from 'fs'"
:: "const bouncer = (f,ini) => { let obj = ini; while (obj.tag) obj = f(obj); return obj.h0 };"
:: Nil)
++ map (render 90 noAlt) docs

View File

@@ -4,7 +4,6 @@ import Prelude
pfunc getArgs uses (arrayToList MkIORes) : IO (List String) := `(w) => Prelude_MkIORes( Prelude_arrayToList(null, process.argv.slice(1)), w)`
pfunc readFile uses (MkIORes Left Right) : (fn : String) -> IO (Either String String) := `(fn) => (w) => {
let fs = require('fs')
let result
try {
let content = fs.readFileSync(fn, 'utf8')
@@ -17,7 +16,6 @@ pfunc readFile uses (MkIORes Left Right) : (fn : String) -> IO (Either String St
-- I wonder if I should automatically `uses` the constructors in the types
pfunc writeFile uses (MkIORes MkUnit) : String String IO (Either String Unit) := `(fn, content) => (w) => {
let fs = require('fs')
let result
try {
fs.writeFileSync(fn, content, 'utf8')
@@ -35,20 +33,20 @@ pfunc exitFailure : ∀ a. String → a := `(_, msg) => {
}`
pfunc putStr uses (MkIORes MkUnit): String IO Unit := `(s) => (w) => {
let {writeSync} = require('fs');
let {writeSync} = fs;
let buf = new TextEncoder().encode(s);
writeSync(1, buf);
return Prelude_MkIORes(Prelude_MkUnit, w);
}`
pfunc readLine uses (MkIORes Left Right) : IO (Either String String) := `(w) => {
let {readSync} = require('fs');
let buf = Buffer.alloc(1024);
let {readSync} = fs;
let buf = new Uint8Array(1024);
let p = 0
while (readSync(0, buf, p, 1, null)) {
if (buf[p++] == 10) return Prelude_MkIORes(Prelude_Right(new TextDecoder().decode(buf.slice(0,p))),w);
if (p + 10 > buf.length) {
let tmp = Buffer.alloc(buf.length * 1.5);
let tmp = new Uint8Array(buf.length * 1.5);
tmp.set(buf);
buf = tmp;
}

View File

@@ -389,7 +389,9 @@ instance HasIO IO where
liftIO a = a
pfunc primPutStrLn uses (MkIORes MkUnit) : String IO Unit := `(s) => (w) => {
require('fs').writeSync(1, s + '\n')
// https://nodejs.org/api/process.html#a-note-on-process-io
// Previously console.log, but that is _not_ always synchronous
fs.writeSync(1, s + '\n')
return Prelude_MkIORes(Prelude_MkUnit,w)
}`
@@ -956,3 +958,7 @@ foldlM f a xs = foldl (\ ma b => ma >>= flip f b) (pure a) xs
pfunc unsafePerformIO : a. IO a a := `(a, f) => f().h1 `
pfunc prim_getTime uses (MkIORes): IO Int := `w => Prelude_MkIORes(+new Date(),w)`
getTime : io. {{HasIO io}} io Int
getTime = liftIO prim_getTime