add TS equivalent
This commit is contained in:
parent
a9004d0a88
commit
3f90dda2e7
24
Makefile
24
Makefile
|
@ -2,11 +2,25 @@
|
|||
|
||||
default: calc
|
||||
|
||||
clean:
|
||||
rm -rfv MAlonzo/
|
||||
rm -v Calc
|
||||
clean: clean-agda clean-typescript
|
||||
|
||||
calc:
|
||||
clean-agda:
|
||||
rm -rfv agda/MAlonzo/
|
||||
rm -v agda/Calc
|
||||
|
||||
clean-typescript:
|
||||
rm -rfv typescript/node_modules
|
||||
rm -rfv typescript/out
|
||||
|
||||
build-agda:
|
||||
agda -c Calc.agda
|
||||
|
||||
Calc: calc
|
||||
build-typescript:
|
||||
( \
|
||||
cd typescript; \
|
||||
$$(npm bin)/tsc \
|
||||
)
|
||||
|
||||
Calc: build-agda
|
||||
|
||||
typescript/out/index.js: build-typescript
|
|
@ -0,0 +1,3 @@
|
|||
node_modules/
|
||||
out/
|
||||
|
|
@ -0,0 +1,14 @@
|
|||
import { getLine, putStrLn } from './IO.js';
|
||||
|
||||
import { evalBin } from './Eval.js';
|
||||
import { takeLine } from './Parse.js';
|
||||
import { show, showList, showResult } from './Show.js';
|
||||
import { map, primStringToList } from './Util.js';
|
||||
|
||||
export function main(): Promise<void> {
|
||||
return getLine().then(c => putStrLn(showList((showResult<number>).bind(null, show), map(evalBin, takeLine(primStringToList(c))))));
|
||||
}
|
||||
|
||||
main().catch(err => {
|
||||
console.error(err);
|
||||
});
|
|
@ -0,0 +1,5 @@
|
|||
import { BinExpr, emitCont, Result } from './Parse.js';
|
||||
|
||||
export function evalBin(b: Result<BinExpr>): Result<number> {
|
||||
return emitCont(0, b.rem); // TODO
|
||||
}
|
|
@ -0,0 +1,34 @@
|
|||
import { Buffer } from 'node:buffer';
|
||||
import { stdin, stdout } from 'node:process';
|
||||
|
||||
export async function getLine(): Promise<string> {
|
||||
return new Promise((res, rej) => {
|
||||
const chunks: Array<Buffer> = [];
|
||||
|
||||
const onData = (chunk: Buffer) => {
|
||||
chunks.push(chunk);
|
||||
};
|
||||
|
||||
const onEnd = () => {
|
||||
off();
|
||||
res(chunks.join(''));
|
||||
};
|
||||
|
||||
const onError = (err: Error) => {
|
||||
rej(err);
|
||||
}
|
||||
|
||||
const off = () => {
|
||||
// stdin.off('data', onData);
|
||||
// stdin.off('end', onEnd);
|
||||
};
|
||||
|
||||
stdin.on('end', onEnd);
|
||||
stdin.on('error', onError);
|
||||
stdin.on('data', onData);
|
||||
});
|
||||
}
|
||||
|
||||
export async function putStrLn(ln: string): Promise<void> {
|
||||
stdout.write(ln);
|
||||
}
|
|
@ -0,0 +1,34 @@
|
|||
export const SymbolNothing = Symbol.for('nothing');
|
||||
export const SymbolJust = Symbol.for('just');
|
||||
|
||||
export type Nothing = {
|
||||
[SymbolNothing]: null;
|
||||
}
|
||||
|
||||
export type Just<T> = {
|
||||
[SymbolJust]: T;
|
||||
}
|
||||
|
||||
export type Maybe<T> = Nothing | Just<T>;
|
||||
|
||||
export const Nothing: Nothing = {
|
||||
[SymbolNothing]: null,
|
||||
};
|
||||
|
||||
export function just<T>(val: T): Just<T> {
|
||||
return {
|
||||
[SymbolJust]: val,
|
||||
};
|
||||
}
|
||||
|
||||
export function nothing(): Nothing {
|
||||
return Nothing;
|
||||
}
|
||||
|
||||
export function isJust<T>(m: Maybe<T>): m is Just<T> {
|
||||
return Object.getOwnPropertyDescriptor(m, SymbolJust) !== undefined;
|
||||
}
|
||||
|
||||
export function isNothing<T>(m: Maybe<T>): m is Nothing {
|
||||
return Object.getOwnPropertyDescriptor(m, SymbolNothing) !== undefined;
|
||||
}
|
|
@ -0,0 +1,85 @@
|
|||
import { isJust, isNothing, Just, just, Maybe, Nothing, nothing } from './Maybe.js';
|
||||
import { map, split } from './Util.js';
|
||||
|
||||
export type Token = {
|
||||
type: 'digit';
|
||||
val: number;
|
||||
} | {
|
||||
type: 'delim';
|
||||
val: string;
|
||||
} | {
|
||||
type: 'oper';
|
||||
val: string;
|
||||
} | {
|
||||
type: 'skip';
|
||||
val: string;
|
||||
} | {
|
||||
type: 'term';
|
||||
};
|
||||
|
||||
export interface BinExpr {
|
||||
oper: Token;
|
||||
lhs: Token;
|
||||
rhs: Token;
|
||||
}
|
||||
|
||||
export interface Result<T, R = Maybe<T>> {
|
||||
res: R;
|
||||
rem: Array<string>;
|
||||
}
|
||||
|
||||
export function emitCont<T>(val: T, rem: Array<string>): Result<T> {
|
||||
return {
|
||||
res: just(val),
|
||||
rem,
|
||||
};
|
||||
}
|
||||
|
||||
export function emitBack<T>(rem: Array<string>): Result<T> {
|
||||
return {
|
||||
res: nothing(),
|
||||
rem,
|
||||
};
|
||||
}
|
||||
|
||||
export function isCont<T>(r: Result<T>): r is Result<T, Just<T>> {
|
||||
return isJust(r.res);
|
||||
}
|
||||
|
||||
export function isBack<T>(r: Result<T>): r is Result<T, Nothing> {
|
||||
return isNothing(r.res);
|
||||
}
|
||||
|
||||
export function takeCons(cs: Array<string>, xs: Array<string>): Result<Array<string>> {
|
||||
return emitBack([]); // TODO
|
||||
}
|
||||
|
||||
export function ignoreConst(cs: Array<string>, xs: Array<string>): Array<string> {
|
||||
return xs; // TODO
|
||||
}
|
||||
|
||||
export function parseChar(): Result<Token> {
|
||||
return emitBack([]); // TODO
|
||||
}
|
||||
|
||||
export function parseNat(): Result<number> {
|
||||
return emitBack([]); // TODO
|
||||
}
|
||||
|
||||
export function takeNat(): Result<number> {
|
||||
return emitBack([]); // TODO
|
||||
}
|
||||
|
||||
export function parseOper() {}
|
||||
|
||||
export function takeOper(): Result<Token> {
|
||||
return emitBack([]); // TODO
|
||||
}
|
||||
|
||||
export function takeBin(): Result<BinExpr> {
|
||||
return emitBack([]); // TODO
|
||||
}
|
||||
|
||||
export function takeLine(c: Array<string>): Array<Result<BinExpr>> {
|
||||
return map(takeBin, split([';'], c));
|
||||
}
|
|
@ -0,0 +1,18 @@
|
|||
import { SymbolJust } from './Maybe.js';
|
||||
import { isCont, Result } from './Parse.js';
|
||||
|
||||
export function show(n: number): string {
|
||||
return n.toString();
|
||||
}
|
||||
|
||||
export function showList<T>(f: (t: T) => string, arr: Array<T>): string {
|
||||
return arr.map(f).join(', ');
|
||||
}
|
||||
|
||||
export function showResult<T>(f: (t: T) => string, r: Result<T>): string {
|
||||
if (isCont(r)) {
|
||||
return f(r.res[SymbolJust]);
|
||||
} else {
|
||||
return r.rem.join('');
|
||||
}
|
||||
}
|
|
@ -0,0 +1,27 @@
|
|||
export function map<T, R>(f: (t: T) => R, arr: Array<T>): Array<R> {
|
||||
return arr.map(f);
|
||||
}
|
||||
|
||||
export function split<T>(cs: Array<T>, xs: Array<T>): Array<Array<T>> {
|
||||
const acl: Array<Array<T>> = [];
|
||||
let acc: Array<T> = [];
|
||||
|
||||
for (const x of xs) {
|
||||
if (cs.includes(x)) {
|
||||
acl.push(acc);
|
||||
acc = [];
|
||||
} else {
|
||||
acc.push(x);
|
||||
}
|
||||
}
|
||||
|
||||
if (acc.length > 0) {
|
||||
acl.push(acc);
|
||||
}
|
||||
|
||||
return acl;
|
||||
}
|
||||
|
||||
export function primStringToList(s: string): Array<string> {
|
||||
return s.split('');
|
||||
}
|
|
@ -0,0 +1,66 @@
|
|||
{
|
||||
"name": "agulator",
|
||||
"version": "1.0.0",
|
||||
"lockfileVersion": 2,
|
||||
"requires": true,
|
||||
"packages": {
|
||||
"": {
|
||||
"name": "agulator",
|
||||
"version": "1.0.0",
|
||||
"license": "ISC",
|
||||
"devDependencies": {
|
||||
"@types/node": "^18.7.23",
|
||||
"tsc": "^2.0.4",
|
||||
"typescript": "^4.8.4"
|
||||
}
|
||||
},
|
||||
"node_modules/@types/node": {
|
||||
"version": "18.7.23",
|
||||
"resolved": "https://registry.npmjs.org/@types/node/-/node-18.7.23.tgz",
|
||||
"integrity": "sha512-DWNcCHolDq0ZKGizjx2DZjR/PqsYwAcYUJmfMWqtVU2MBMG5Mo+xFZrhGId5r/O5HOuMPyQEcM6KUBp5lBZZBg==",
|
||||
"dev": true
|
||||
},
|
||||
"node_modules/tsc": {
|
||||
"version": "2.0.4",
|
||||
"resolved": "https://registry.npmjs.org/tsc/-/tsc-2.0.4.tgz",
|
||||
"integrity": "sha512-fzoSieZI5KKJVBYGvwbVZs/J5za84f2lSTLPYf6AGiIf43tZ3GNrI1QzTLcjtyDDP4aLxd46RTZq1nQxe7+k5Q==",
|
||||
"dev": true,
|
||||
"bin": {
|
||||
"tsc": "bin/tsc"
|
||||
}
|
||||
},
|
||||
"node_modules/typescript": {
|
||||
"version": "4.8.4",
|
||||
"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.8.4.tgz",
|
||||
"integrity": "sha512-QCh+85mCy+h0IGff8r5XWzOVSbBO+KfeYrMQh7NJ58QujwcE22u+NUSmUxqF+un70P9GXKxa2HCNiTTMJknyjQ==",
|
||||
"dev": true,
|
||||
"bin": {
|
||||
"tsc": "bin/tsc",
|
||||
"tsserver": "bin/tsserver"
|
||||
},
|
||||
"engines": {
|
||||
"node": ">=4.2.0"
|
||||
}
|
||||
}
|
||||
},
|
||||
"dependencies": {
|
||||
"@types/node": {
|
||||
"version": "18.7.23",
|
||||
"resolved": "https://registry.npmjs.org/@types/node/-/node-18.7.23.tgz",
|
||||
"integrity": "sha512-DWNcCHolDq0ZKGizjx2DZjR/PqsYwAcYUJmfMWqtVU2MBMG5Mo+xFZrhGId5r/O5HOuMPyQEcM6KUBp5lBZZBg==",
|
||||
"dev": true
|
||||
},
|
||||
"tsc": {
|
||||
"version": "2.0.4",
|
||||
"resolved": "https://registry.npmjs.org/tsc/-/tsc-2.0.4.tgz",
|
||||
"integrity": "sha512-fzoSieZI5KKJVBYGvwbVZs/J5za84f2lSTLPYf6AGiIf43tZ3GNrI1QzTLcjtyDDP4aLxd46RTZq1nQxe7+k5Q==",
|
||||
"dev": true
|
||||
},
|
||||
"typescript": {
|
||||
"version": "4.8.4",
|
||||
"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.8.4.tgz",
|
||||
"integrity": "sha512-QCh+85mCy+h0IGff8r5XWzOVSbBO+KfeYrMQh7NJ58QujwcE22u+NUSmUxqF+un70P9GXKxa2HCNiTTMJknyjQ==",
|
||||
"dev": true
|
||||
}
|
||||
}
|
||||
}
|
|
@ -0,0 +1,17 @@
|
|||
{
|
||||
"name": "agulator",
|
||||
"type": "module",
|
||||
"version": "1.0.0",
|
||||
"description": "calculator equivalent to agda",
|
||||
"main": "out/index.js",
|
||||
"scripts": {
|
||||
"test": "mocha"
|
||||
},
|
||||
"author": "ssube",
|
||||
"license": "ISC",
|
||||
"devDependencies": {
|
||||
"@types/node": "^18.7.23",
|
||||
"tsc": "^2.0.4",
|
||||
"typescript": "^4.8.4"
|
||||
}
|
||||
}
|
|
@ -0,0 +1,40 @@
|
|||
{
|
||||
"compileOnSave": false,
|
||||
"compilerOptions": {
|
||||
"allowJs": false,
|
||||
"allowSyntheticDefaultImports": true,
|
||||
"declaration": true,
|
||||
"declarationMap": true,
|
||||
"emitDecoratorMetadata": true,
|
||||
"experimentalDecorators": true,
|
||||
"importHelpers": true,
|
||||
"lib": [
|
||||
"es2017",
|
||||
"esnext.asynciterable"
|
||||
],
|
||||
"module": "esnext",
|
||||
"moduleResolution": "node",
|
||||
"noImplicitAny": true,
|
||||
"noImplicitReturns": true,
|
||||
"noImplicitThis": true,
|
||||
"outDir": "./out",
|
||||
"sourceMap": true,
|
||||
"strict": true,
|
||||
"strictNullChecks": true,
|
||||
"target": "es2017",
|
||||
"types": [
|
||||
"node"
|
||||
],
|
||||
"typeRoots": [
|
||||
"./node_modules/@types",
|
||||
"./node_modules",
|
||||
"./vendor"
|
||||
]
|
||||
},
|
||||
"exclude": [
|
||||
"./node_modules"
|
||||
],
|
||||
"include": [
|
||||
"./*.ts"
|
||||
]
|
||||
}
|
Loading…
Reference in New Issue