diff --git a/.gitignore b/.gitignore
index bf086df..dc3cb4d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,6 +5,6 @@ build/
*.log
*.agda
*.agdai
-*.js
+/*.js
input.txt
node_modules
diff --git a/Makefile b/Makefile
index 66ccf03..19cddbd 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
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}
idris2 --build newt.ipkg
@@ -8,6 +8,9 @@ build/exec/newt: ${SRCS}
build/exec/newt.js: ${SRCS}
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
scripts/test
diff --git a/TODO.md b/TODO.md
index 7c54d3b..ba01984 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,17 +1,19 @@
## TODO
+- [ ] Check for shadowing when declaring dcon
+- [ ] Require infix decl before declaring names
- [x] Allow unicode operators/names
- [ ] Web tool
- edit, view output, view js, run js, monaco would be nice.
- need to shim out Buffer
- [x] get rid of stray INFO from auto resolution
-- [ ] handle if_then_else_ style mixfix
-- [ ] Check for shadowing when declaring dcon
+- [ ] handle `if_then_else_` style mixfix
- [ ] Search should look at context
- [ ] records
- [ ] copattern matching
- [ ] Support @ on the LHS
+- [ ] Get `Combinatory.newt` to work
- [x] Remember operators from imports
- [ ] 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.
@@ -83,4 +85,7 @@
- [ ] Read Ulf Norell thesis
- [ ] 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.
diff --git a/newt/Combinatory.newt b/newt/Combinatory.newt
index def1065..2b33020 100644
--- a/newt/Combinatory.newt
+++ b/newt/Combinatory.newt
@@ -77,11 +77,11 @@ sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
Comb Γ (σ ~> τ ~> ρ) f →
Comb Γ (σ ~> τ) x →
Comb Γ (σ ~> ρ) (\ env y => (f env y) (x env y))
--- sapp (CApp K t) I = t
--- sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
--- sapp (CApp K t) u = CApp (CApp B t) u
--- sapp t (CApp K u) = CApp (CApp C t) u
--- sapp t u = CApp (CApp S t) u
+sapp (CApp K t) I = t
+sapp (CApp K t) (CApp K u) = CApp K (CApp t u)
+sapp (CApp K t) u = CApp (CApp B t) u
+sapp t (CApp K u) = CApp (CApp C t) u
+sapp t u = CApp (CApp S t) u
abs : {Γ : Ctx} {σ τ : Type} {f : _} → Comb (σ :: Γ) τ f → Comb Γ (σ ~> τ) (\ env x => f (x ::: env))
abs S = CApp K S
diff --git a/playground/README.md b/playground/README.md
new file mode 100644
index 0000000..a2b4024
--- /dev/null
+++ b/playground/README.md
@@ -0,0 +1,5 @@
+- Run `make` in newt directory
+- Run `./build`
+- Run `vite`
+- Click on url
+
diff --git a/playground/build b/playground/build
new file mode 100755
index 0000000..40f0c39
--- /dev/null
+++ b/playground/build
@@ -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
+
diff --git a/playground/index.html b/playground/index.html
index 4fc171d..50a1941 100644
--- a/playground/index.html
+++ b/playground/index.html
@@ -2,18 +2,17 @@
-
+
- Vite + TS
+ Newt Playground
-
-
result
+
diff --git a/playground/public/shim.js b/playground/public/shim.js
deleted file mode 100644
index 9e592c1..0000000
--- a/playground/public/shim.js
+++ /dev/null
@@ -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 shim[x];
diff --git a/playground/src/global.d.ts b/playground/src/global.d.ts
index d8b1765..63db482 100644
--- a/playground/src/global.d.ts
+++ b/playground/src/global.d.ts
@@ -1,13 +1,15 @@
-export {}
+declare module "*.css";
+export {};
declare global {
interface Process {
+ platform: string;
stdout: {
- write(s: string): void
- },
- argv: string[]
-
+ write(s: string): void;
+ };
+ argv: string[];
+ exit(_: number): void;
}
- let files : Record
- let process : Process
- let __mainExpression_0 : () => unknown
+ let files: Record;
+ let process: Process;
+ let newtMain: () => unknown;
}
diff --git a/playground/src/main.ts b/playground/src/main.ts
index 05b33d1..5908909 100644
--- a/playground/src/main.ts
+++ b/playground/src/main.ts
@@ -1,45 +1,106 @@
-import './style.css'
-import {newtLanguage} from './monarch.ts'
+// import "./style.css";
+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);
-
-let container = document.getElementById('editor')!
-let result = document.getElementById('result')!
-const editor = monaco.editor.create(container, {
- value: "module Main\n\n",
- language: "newt",
- theme: "vs",
-
- automaticLayout: true,
+// I keep pressing this.
+document.addEventListener('keydown', (ev) => {
+ if (ev.metaKey && ev.code == 'KeyS') ev.preventDefault();
})
-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) {
- console.log('run', s)
- process.argv = ['','', 'src/Main.newt']
- files['src/Main.newt'] = s
- result.innerHTML = ''
- __mainExpression_0()
+ console.log("run", s);
+ process.argv = ["", "", "src/Main.newt", "-o", "out.js"];
+ console.log("args", process.argv);
+ files["src/Main.newt"] = s;
+ result.innerHTML = "";
+ stdout = ''
+ newtMain();
+ processOutput();
}
-
+let stdout = ''
// We'll want to collect and put info in the monaco
process.stdout.write = (s) => {
- console.log('write', s)
- let div = document.createElement('div')
- div.className = 'log'
- div.textContent = s
- result.appendChild(div)
+ stdout += s
+};
+
+// Adapted from the vscode extension, but types are slightly different
+// 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) => {
- console.log('mc', ev)
- let value = editor.getValue()
- clearTimeout(timeout)
- timeout = setTimeout(() => run(value), 1000)
-})
-console.log('REGISTER')
+ console.log("mc", ev);
+ let value = editor.getValue();
+ clearTimeout(timeout);
+ timeout = setTimeout(() => run(value), 1000);
+ localStorage.code = value;
+});
+
+run(value);
diff --git a/playground/src/monarch.ts b/playground/src/monarch.ts
index aeb6b56..cebb5c3 100644
--- a/playground/src/monarch.ts
+++ b/playground/src/monarch.ts
@@ -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
- // defaultToken: 'invalid',
+ defaultToken: "invalid",
keywords: [
"let",
diff --git a/playground/src/shim.ts b/playground/src/shim.ts
new file mode 100644
index 0000000..35dfae4
--- /dev/null
+++ b/playground/src/shim.ts
@@ -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 = {};
+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];
diff --git a/playground/src/style.css b/playground/style.css
similarity index 100%
rename from playground/src/style.css
rename to playground/style.css
diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr
index e089467..a066023 100644
--- a/src/Lib/ProcessDecl.idr
+++ b/src/Lib/ProcessDecl.idr
@@ -139,7 +139,8 @@ processDecl (TypeSig fc names tm) = do
-- ty' <- nf [] ty
-- putStrLn "nf \{pprint [] ty'}"
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
top <- get
diff --git a/src/Main.idr b/src/Main.idr
index 024a3c8..4e70838 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -140,6 +140,7 @@ main' = do
Just name => writeSource name
-- traverse_ processFile (filter (".newt" `isSuffixOf`) files) out
+%export "javascript:newtMain"
main : IO ()
main = do
-- we'll need to reset for each file, etc.