From 182876d16b291867a340b426fe19b85b0a0cb28a Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Tue, 5 Nov 2024 13:44:16 -0800 Subject: [PATCH] Playground highlights and shows info/errors from build --- .gitignore | 2 +- Makefile | 5 +- TODO.md | 9 ++- newt/Combinatory.newt | 10 +-- playground/README.md | 5 ++ playground/build | 9 +++ playground/index.html | 7 +- playground/public/shim.js | 89 ------------------------ playground/src/global.d.ts | 18 ++--- playground/src/main.ts | 123 ++++++++++++++++++++++++--------- playground/src/monarch.ts | 57 ++++++++++++++- playground/src/shim.ts | 112 ++++++++++++++++++++++++++++++ playground/{src => }/style.css | 0 src/Lib/ProcessDecl.idr | 3 +- src/Main.idr | 1 + 15 files changed, 305 insertions(+), 145 deletions(-) create mode 100644 playground/README.md create mode 100755 playground/build delete mode 100644 playground/public/shim.js create mode 100644 playground/src/shim.ts rename playground/{src => }/style.css (100%) 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.