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

Playground highlights and shows info/errors from build

Browse Source
This commit is contained in:
Steve Dunham
2024-11-05 13:44:16 -08:00
parent f92d287909
commit 182876d16b
15 changed files with 305 additions and 145 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.gitignore vendored
View File

@@ -5,6 +5,6 @@ build/
*.log *.log
*.agda *.agda
*.agdai *.agdai
*.js /*.js
input.txt input.txt
node_modules node_modules

5
Makefile
View File

@@ -1,6 +1,6 @@
SRCS=$(shell find src -name "*.idr") SRCS=$(shell find src -name "*.idr")
all: build/exec/newt build/exec/newt.js all: build/exec/newt build/exec/newt.js build/exec/newt.min.js
build/exec/newt: ${SRCS} build/exec/newt: ${SRCS}
idris2 --build newt.ipkg idris2 --build newt.ipkg
@@ -8,6 +8,9 @@ build/exec/newt: ${SRCS}
build/exec/newt.js: ${SRCS} build/exec/newt.js: ${SRCS}
idris2 --cg node -o newt.js -p contrib -c src/Main.idr idris2 --cg node -o newt.js -p contrib -c src/Main.idr
build/exec/newt.min.js: ${SRCS}
idris2 --cg node -o newt.min.js -p contrib -c src/Main.idr --directive minimal
test: build/exec/newt test: build/exec/newt
scripts/test scripts/test

9
TODO.md
View File

@@ -1,17 +1,19 @@
## TODO ## TODO
- [ ] Check for shadowing when declaring dcon
- [ ] Require infix decl before declaring names
- [x] Allow unicode operators/names - [x] Allow unicode operators/names
- [ ] Web tool - [ ] Web tool
- edit, view output, view js, run js, monaco would be nice. - edit, view output, view js, run js, monaco would be nice.
- need to shim out Buffer - need to shim out Buffer
- [x] get rid of stray INFO from auto resolution - [x] get rid of stray INFO from auto resolution
- [ ] handle if_then_else_ style mixfix - [ ] handle `if_then_else_` style mixfix
- [ ] Check for shadowing when declaring dcon
- [ ] Search should look at context - [ ] Search should look at context
- [ ] records - [ ] records
- [ ] copattern matching - [ ] copattern matching
- [ ] Support @ on the LHS - [ ] Support @ on the LHS
- [ ] Get `Combinatory.newt` to work
- [x] Remember operators from imports - [x] Remember operators from imports
- [ ] Default cases for non-primitives (currently gets expanded to all constructors) - [ ] Default cases for non-primitives (currently gets expanded to all constructors)
- This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from the individual, unnamed cases though. - This may need a little care. But I think I could collect all constructors that only match wildcards into a single case. This would lose any information from the individual, unnamed cases though.
@@ -83,4 +85,7 @@
- [ ] Read Ulf Norell thesis - [ ] Read Ulf Norell thesis
- [ ] Finish reading dynamic pattern unification paper to see what is missing/wrong with the current implementation - [ ] Finish reading dynamic pattern unification paper to see what is missing/wrong with the current implementation
### Other issues
- [ ] Name space flattening makes it a bit more subtle when a misspelled (or shadowed) constructor turns into a variable.

10
newt/Combinatory.newt
View File

@@ -77,11 +77,11 @@ sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
Comb Γ (σ ~> τ ~> ρ) f → Comb Γ (σ ~> τ ~> ρ) f →
Comb Γ (σ ~> τ) x → Comb Γ (σ ~> τ) x →
Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y)) Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y))
-- sapp (CApp K t) I = t sapp (CApp K t) I = t
-- sapp (CApp K t) (CApp K u) = CApp K (CApp t u) sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
-- sapp (CApp K t) u = CApp (CApp B t) u sapp (CApp K t) u = CApp (CApp B t) u
-- sapp t (CApp K u) = CApp (CApp C t) u sapp t (CApp K u) = CApp (CApp C t) u
-- sapp t u = CApp (CApp S t) u sapp t u = CApp (CApp S t) u
abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env)) abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env))
abs S = CApp K S abs S = CApp K S

5
playground/README.md Normal file
View File

@@ -0,0 +1,5 @@
- Run `make` in newt directory
- Run `./build`
- Run `vite`
- Click on url

9
playground/build Executable file
View File

@@ -0,0 +1,9 @@
#!/bin/sh
echo Builds the workMain.js and copies newt.js
esbuild --bundle node_modules/monaco-editor/esm/vs/editor/editor.worker.js > public/workerMain.js
# bare javascript, it fakes node api for the idris code in newt.js
esbuild src/shim.ts > public/shim.js
cp ../build/exec/newt.js public
# uncomment to make this smaller
# esbuild --minify ../build/exec/newt.min.js > public/newt.js

7
playground/index.html
View File

@@ -2,18 +2,17 @@
<html lang="en"> <html lang="en">
<head> <head>
<meta charset="UTF-8" /> <meta charset="UTF-8" />
<link rel="icon" type="image/svg+xml" href="/vite.svg" /> <link rel="stylesheet" href="style.css">
<meta name="viewport" content="width=device-width, initial-scale=1.0" /> <meta name="viewport" content="width=device-width, initial-scale=1.0" />
<title>Vite + TS</title> <title>Newt Playground</title>
<script src="shim.js"></script> <script src="shim.js"></script>
<script src="newt.js"></script> <script src="newt.js"></script>
<script src="hack.js"></script>
</head> </head>
<body> <body>
<div id="app"> <div id="app">
<div class="wrapper"> <div class="wrapper">
<div id="editor"></div> <div id="editor"></div>
<div id="result">result</div> <div id="result"></div>
</div> </div>
</div> </div>
<script type="module" src="/src/main.ts"></script> <script type="module" src="/src/main.ts"></script>

89
playground/public/shim.js
View File

@@ -1,89 +0,0 @@
class Buffer extends ArrayBuffer {
static alloc(n) {
return new Buffer(n);
}
indexOf(n) {
let view = new Uint8Array(this);
return view.indexOf(n);
}
static concat(bufs) {
let size = bufs.reduce((a, b) => (a += b.byteLength), 0);
console.log('concat', size, bufs);
let rval = new Buffer(size);
let view = new Uint8Array(rval);
let off = 0;
for (let buf of bufs) {
view.set(new Uint8Array(buf), off);
off += buf.byteLength;
}
return rval;
}
toString() {
return dec.decode(this)
}
}
let dec = new TextDecoder();
let enc = new TextEncoder();
let files = {
};
let fds = [];
let shim = {
os: {
platform() {
return "linux";
},
},
fs: {
openSync(fn) {
console.log("openSync", fn);
let te = new TextEncoder();
let fd = fds.length;
if (!files[fn]) throw new Error(`${fn} not found`)
let buf = te.encode(files[fn]);
let pos = 0;
fds.push({ buf, pos });
// we'll mutate the pointer as stuff is read
return fd;
},
readSync(fd, buf, start, len) {
let hand = fds[fd]
let avail = hand.buf.byteLength - hand.pos
let rd = Math.min(avail, len)
let src = new Uint8Array(hand.buf)
let dest = new Uint8Array(buf)
for (let i=0;i<rd;i++)
dest[start+i] = src[hand.pos++]
console.log('read', rd)
return rd
},
closeSync(fd) {
delete fds[fd]
}
},
};
shim.fs = new Proxy(shim.fs, {
get(target, prop, receiver) {
console.log("fs get", prop);
return target[prop];
},
});
const process = {
platform: "linux",
argv: ["", ""],
stdout: {
// We'll want to replace this one
write: console.log,
},
exit(v) {
console.log("exit", v);
},
// stdin: { fd: 0 },
};
const require = (x) => shim[x];

18
playground/src/global.d.ts vendored
View File

@@ -1,13 +1,15 @@
export {} declare module "*.css";
export {};
declare global { declare global {
interface Process { interface Process {
platform: string;
stdout: { stdout: {
write(s: string): void write(s: string): void;
}, };
argv: string[] argv: string[];
exit(_: number): void;
} }
let files : Record<string,string> let files: Record<string, string>;
let process : Process let process: Process;
let __mainExpression_0 : () => unknown let newtMain: () => unknown;
} }

123
playground/src/main.ts
View File

@@ -1,45 +1,106 @@
import './style.css' // import "./style.css";
import {newtLanguage} from './monarch.ts' import { newtConfig, newtTokens } from "./monarch.ts";
import * as monaco from "monaco-editor";
import * as monaco from 'monaco-editor' monaco.languages.register({ id: "newt" });
monaco.languages.setMonarchTokensProvider("newt", newtTokens);
monaco.languages.setLanguageConfiguration("newt", newtConfig);
self.MonacoEnvironment = {
getWorkerUrl(moduleId, label) {
console.log("Get worker", moduleId);
return moduleId;
},
};
monaco.languages.setMonarchTokensProvider("newt", newtLanguage); // I keep pressing this.
document.addEventListener('keydown', (ev) => {
let container = document.getElementById('editor')! if (ev.metaKey && ev.code == 'KeyS') ev.preventDefault();
let result = document.getElementById('result')!
const editor = monaco.editor.create(container, {
value: "module Main\n\n",
language: "newt",
theme: "vs",
automaticLayout: true,
}) })
let timeout : number | undefined let value = localStorage.code || "module Main\n";
let container = document.getElementById("editor")!;
let result = document.getElementById("result")!;
const editor = monaco.editor.create(container, {
value,
language: "newt",
theme: "vs",
automaticLayout: true,
minimap: { enabled: false },
});
let timeout: number | undefined;
function run(s: string) { function run(s: string) {
console.log('run', s) console.log("run", s);
process.argv = ['','', 'src/Main.newt'] process.argv = ["", "", "src/Main.newt", "-o", "out.js"];
files['src/Main.newt'] = s console.log("args", process.argv);
result.innerHTML = '' files["src/Main.newt"] = s;
__mainExpression_0() result.innerHTML = "";
stdout = ''
newtMain();
processOutput();
} }
let stdout = ''
// We'll want to collect and put info in the monaco // We'll want to collect and put info in the monaco
process.stdout.write = (s) => { process.stdout.write = (s) => {
console.log('write', s) stdout += s
let div = document.createElement('div') };
div.className = 'log'
div.textContent = s // Adapted from the vscode extension, but types are slightly different
result.appendChild(div) // and positions are 1-based.
const processOutput = () => {
result.innerText = stdout
let model = editor.getModel()!
let markers: monaco.editor.IMarkerData[] = []
let lines = stdout.split('\n')
for (let i = 0; i < lines.length; i++) {
const line = lines[i];
const match = line.match(/(INFO|ERROR) at \((\d+), (\d+)\):\s*(.*)/);
if (match) {
let [_full, kind, line, col, message] = match;
let lineNumber = +line+1
let column = +col+1;
let start = {column, lineNumber};
// we don't have the full range, so grab the surrounding word
let endColumn = column + 1
let word = model.getWordAtPosition(start)
if (word) endColumn = word.endColumn
// heuristics to grab the entire message:
// anything indented
// Context:, or Goal: are part of PRINTME
// unexpected / expecting appear in parse errors
while (
lines[i + 1]?.match(/^( )/)
) {
message += "\n" + lines[++i];
}
const severity = kind === 'ERROR' ? monaco.MarkerSeverity.Error : monaco.MarkerSeverity.Info
markers.push({
severity,
message,
startLineNumber: lineNumber,
endLineNumber: lineNumber,
startColumn: column,
endColumn,
})
}
}
console.log('setMarkers', markers)
monaco.editor.setModelMarkers(model, 'newt', markers)
} }
editor.onDidChangeModelContent((ev) => { editor.onDidChangeModelContent((ev) => {
console.log('mc', ev) console.log("mc", ev);
let value = editor.getValue() let value = editor.getValue();
clearTimeout(timeout) clearTimeout(timeout);
timeout = setTimeout(() => run(value), 1000) timeout = setTimeout(() => run(value), 1000);
}) localStorage.code = value;
console.log('REGISTER') });
run(value);

57
playground/src/monarch.ts
View File

@@ -1,8 +1,59 @@
import * as monaco from 'monaco-editor' import * as monaco from "monaco-editor";
export let newtLanguage: monaco.languages.IMonarchLanguage = { export let newtConfig: monaco.languages.LanguageConfiguration = {
comments: {
// symbol used for single line comment. Remove this entry if your language does not support line comments
lineComment: "--",
// symbols used for start and end a block comment. Remove this entry if your language does not support block comments
blockComment: ["/-", "-/"],
},
// symbols used as brackets
brackets: [
["{", "}"],
["[", "]"],
["(", ")"],
],
// symbols that are auto closed when typing
autoClosingPairs: [
{ open: "{", close: "}" },
{ open: "[", close: "]" },
{ open: "(", close: ")" },
{ open: '"', close: '"' },
{ open: "'", close: "'" },
],
// symbols that can be used to surround a selection
surroundingPairs: [
{ open: "{", close: "}" },
{ open: "[", close: "]" },
{ open: "(", close: ")" },
{ open: '"', close: '"' },
{ open: "'", close: "'" },
],
onEnterRules: [
{
beforeText: /^\s+$/,
action: {
indentAction: monaco.languages.IndentAction.Outdent,
},
},
{
beforeText: /\bwhere$/,
action: {
indentAction: monaco.languages.IndentAction.Indent,
},
},
{
beforeText: /\bof$/,
action: {
indentAction: monaco.languages.IndentAction.Indent,
},
},
],
};
export let newtTokens: monaco.languages.IMonarchLanguage = {
// Set defaultToken to invalid to see what you do not tokenize yet // Set defaultToken to invalid to see what you do not tokenize yet
// defaultToken: 'invalid', defaultToken: "invalid",
keywords: [ keywords: [
"let", "let",

112
playground/src/shim.ts Normal file
View File

@@ -0,0 +1,112 @@
class Buffer extends ArrayBuffer {
static alloc(n: number) {
return new Buffer(n);
}
indexOf(n: number) {
let view = new Uint8Array(this);
return view.indexOf(n);
}
static concat(bufs: Buffer[]) {
let size = bufs.reduce((a, b) => (a += b.byteLength), 0);
let rval = new Buffer(size);
let view = new Uint8Array(rval);
let off = 0;
for (let buf of bufs) {
view.set(new Uint8Array(buf), off);
off += buf.byteLength;
}
return rval;
}
toString() {
return new TextDecoder().decode(this);
}
}
let files: Record<string, string> = {};
interface Handle {
name: string;
mode: string;
pos: number;
buf: Buffer;
}
let fds: Handle[] = [];
let shim: any = {
os: {
platform() {
return "linux";
},
},
fs: {
openSync(name: string, mode: string) {
console.log("open", name, arguments);
let te = new TextEncoder();
let fd = fds.findIndex((x) => !x);
if (fd < 0) fd = fds.length;
let buf;
let pos = 0;
if (mode == "w") {
buf = new Buffer(0);
} else {
if (!files[name]) throw new Error(`${name} not found`);
buf = te.encode(files[name]);
}
fds[fd] = { buf, pos, mode, name };
// we'll mutate the pointer as stuff is read
return fd;
},
writeSync(fd: number, line: string) {
if (typeof line !== "string") throw new Error("not implemented");
let handle = fds[fd];
if (!handle) throw new Error(`bad fd ${fd}`)
let buf2 = new TextEncoder().encode(line);
handle.buf = Buffer.concat([handle.buf, buf2])
},
chmodSync(fn: string, mode: number) {
console.log('chmod', fn, mode)
},
readSync(fd: number, buf: Buffer, start: number, len: number) {
let hand = fds[fd];
let avail = hand.buf.byteLength - hand.pos;
let rd = Math.min(avail, len);
let src = new Uint8Array(hand.buf);
let dest = new Uint8Array(buf);
for (let i = 0; i < rd; i++) dest[start + i] = src[hand.pos++];
return rd;
},
closeSync(fd: number) {
let handle = fds[fd];
if (handle.mode == "w") {
files[handle.name] = new TextDecoder().decode(handle.buf);
}
delete fds[fd];
},
},
};
// Spy on Idris' calls to see what we need to fill in
shim.fs = new Proxy(shim.fs, {
get(target, prop, receiver) {
if (prop in target) {
return (target as any)[prop];
}
throw new Error(`implement fs.${String(prop)}`)
},
});
const process: Process = {
platform: "linux",
argv: ["", ""],
stdout: {
// We'll want to replace this one
write: console.log,
},
exit(v: number) {
console.log("exit", v);
},
// stdin: { fd: 0 },
};
const require = (x: string) => shim[x];

0
playground/src/style.css → playground/style.css
View File

3
src/Lib/ProcessDecl.idr
View File

@@ -139,7 +139,8 @@ processDecl (TypeSig fc names tm) = do
-- ty' <- nf [] ty -- ty' <- nf [] ty
-- putStrLn "nf \{pprint [] ty'}" -- putStrLn "nf \{pprint [] ty'}"
for_ names $ \nm => modify $ setDef nm ty Axiom for_ names $ \nm => modify $ setDef nm ty Axiom
logMetas mstart -- Zoo4eg has metas in TypeSig, need to decide if I want to support that going forward.
-- logMetas mstart
processDecl (PType fc nm ty) = do processDecl (PType fc nm ty) = do
top <- get top <- get

1
src/Main.idr
View File

@@ -140,6 +140,7 @@ main' = do
Just name => writeSource name Just name => writeSource name
-- traverse_ processFile (filter (".newt" `isSuffixOf`) files) out -- traverse_ processFile (filter (".newt" `isSuffixOf`) files) out
%export "javascript:newtMain"
main : IO () main : IO ()
main = do main = do
-- we'll need to reset for each file, etc. -- we'll need to reset for each file, etc.