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

cleanup

Browse Source
This commit is contained in:
Steve Dunham
2026-03-27 20:19:27 -07:00
parent a40956a4cc
commit aa6604038b
5 changed files with 5 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
newt-vscode-lsp/src/extension.ts
View File

@@ -23,7 +23,7 @@ export function activate(context: vscode.ExtensionContext) {
let serverOptions: ServerOptions let serverOptions: ServerOptions
if (cmd) { if (cmd) {
serverOptions = { serverOptions = {
run: { command: "node", args: [cmd], transport: TransportKind.pipe }, run: { command: "node", args: ['--heapsnapshot-signal=SIGUSR2',cmd], transport: TransportKind.pipe },
debug: { command: "node", args: [cmd], transport: TransportKind.pipe }, debug: { command: "node", args: [cmd], transport: TransportKind.pipe },
} }
} else { } else {

2
src/Lib/Erasure.newt
View File

@@ -96,7 +96,7 @@ erase env t sp = case t of
eraseSpine env (LetRec fc nm ty u' v') sp Nothing eraseSpine env (LetRec fc nm ty u' v') sp Nothing
(Bnd fc k) => do (Bnd fc k) => do
case getAt (cast k) env of case getAt (cast k) env of
Nothing => error fc "bad index \{show k}" Nothing => error fc "Erase: bad index \{show k}"
Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)" Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)"
Just (nm, Many, ty) => eraseSpine env t sp ty Just (nm, Many, ty) => eraseSpine env t sp ty
(UU fc) => eraseSpine env t sp (Just $ UU fc) (UU fc) => eraseSpine env t sp (Just $ UU fc)

4
src/Lib/Eval.newt
View File

@@ -12,7 +12,7 @@ import Data.SortedMap
eval : Env -> Tm -> M Val eval : Env -> Tm -> M Val
-- REVIEW everything is evalutated whether it's needed or not -- REVIEW everything is evaluated whether it's needed or not
-- It would be nice if the environment were lazy. -- It would be nice if the environment were lazy.
-- e.g. case is getting evaluated when passed to a function because -- e.g. case is getting evaluated when passed to a function because
-- of dependencies in pi-types, even if the dependency isn't used -- of dependencies in pi-types, even if the dependency isn't used
@@ -50,7 +50,7 @@ unlet : Env -> Val -> M Val
unlet env t@(VVar fc k sp) = case lookupVar env k of unlet env t@(VVar fc k sp) = case lookupVar env k of
Just tt@(VVar fc' k' sp') => do Just tt@(VVar fc' k' sp') => do
debug $ \ _ => "lookup \{show k} is \{show tt}" debug $ \ _ => "lookup \{show k} is \{show tt}"
if k' == k then pure t else (vappSpine (VVar fc' k' sp') sp >>= unlet env) if k' == k then pure t else (vappSpine tt sp >>= unlet env)
Just t => vappSpine t sp >>= unlet env Just t => vappSpine t sp >>= unlet env
Nothing => do Nothing => do
debug $ \ _ => "lookup \{show k} is Nothing in env \{show env}" debug $ \ _ => "lookup \{show k} is Nothing in env \{show env}"

1
src/Lib/ProcessDecl.newt
View File

@@ -310,7 +310,6 @@ processInstance ns instfc ty decls = do
vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty
| x => error (getFC x) "dcty not Pi" | x => error (getFC x) "dcty not Pi"
debug $ \ _ => "dcty \{render 90 $ pprint Nil dcty}" debug $ \ _ => "dcty \{render 90 $ pprint Nil dcty}"
let (_,args) = funArgs codomain
debug $ \ _ => "traverse \{show $ map show args}" debug $ \ _ => "traverse \{show $ map show args}"
-- This is a little painful because we're reverse engineering the -- This is a little painful because we're reverse engineering the