add interpreter
This commit is contained in:
parent
e2e74df94f
commit
f4ad269f8b
@ -39,7 +39,7 @@ a:visited {
|
||||
display: grid;
|
||||
grid-template-rows: auto 1fr auto;
|
||||
min-width: 600px;
|
||||
width: 45%;
|
||||
width: 70%;
|
||||
margin-left: auto;
|
||||
margin-right: auto;
|
||||
padding: 0;
|
||||
|
@ -55,15 +55,10 @@ export class TheAbstractionEngine {
|
||||
const player = new Player();
|
||||
this.game.addEntity(player);
|
||||
|
||||
const box = new FunctionBox({ x: 3, y: 1 }, "λ x . (x)");
|
||||
this.game.addEntity(box);
|
||||
const box2 = new FunctionBox({ x: 4, y: 1 }, "λ x . (x)");
|
||||
this.game.addEntity(box2);
|
||||
|
||||
const wall = new Wall({ x: 5, y: 3 });
|
||||
this.game.addEntity(wall);
|
||||
|
||||
const factory = new LambdaFactory({ x: 6, y: 6 }, "λ x . (x)", 10);
|
||||
const factory = new LambdaFactory({ x: 6, y: 6 }, "(λ (x) . x)", 10);
|
||||
this.game.addEntity(factory);
|
||||
|
||||
const lockedDoor = new LockedDoor({ x: 8, y: 8 });
|
||||
|
@ -134,9 +134,7 @@ export class LambdaFactory extends Entity {
|
||||
private codeEditor(code: string) {
|
||||
return `
|
||||
<div>
|
||||
<textarea id="code" autofocus="autofocus" rows="10" cols="50">
|
||||
${code}
|
||||
</textarea>
|
||||
<textarea id="code" rows="10" cols="50">${code}</textarea>
|
||||
<button id="close-modal">Close</button>
|
||||
</div>
|
||||
`;
|
||||
|
49
src/interpreter/SymbolTable.ts
Normal file
49
src/interpreter/SymbolTable.ts
Normal file
@ -0,0 +1,49 @@
|
||||
export class UndefinedSymbolError extends Error {}
|
||||
|
||||
export class SymbolTable {
|
||||
private knownSymbols: Set<string>;
|
||||
private parent: SymbolTable | null;
|
||||
private depth: number;
|
||||
|
||||
constructor(parent: SymbolTable | null = null) {
|
||||
this.knownSymbols = new Set();
|
||||
this.parent = parent;
|
||||
this.depth = parent ? parent.getDepth() + 1 : 0;
|
||||
}
|
||||
|
||||
public getDepth() {
|
||||
return this.depth;
|
||||
}
|
||||
|
||||
public add(name: string) {
|
||||
this.knownSymbols.add(name);
|
||||
}
|
||||
|
||||
public get(name: string): number {
|
||||
if (this.knownSymbols.has(name)) {
|
||||
return 1;
|
||||
}
|
||||
|
||||
if (this.parent) {
|
||||
return 1 + this.parent.get(name);
|
||||
}
|
||||
|
||||
throw new UndefinedSymbolError(`Undefined variable: ${name}`);
|
||||
}
|
||||
|
||||
public has(name: string): boolean {
|
||||
if (this.knownSymbols.has(name)) {
|
||||
return true;
|
||||
}
|
||||
|
||||
if (this.parent) {
|
||||
return this.parent.has(name);
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
public createChild(): SymbolTable {
|
||||
return new SymbolTable(this);
|
||||
}
|
||||
}
|
@ -1,2 +1,3 @@
|
||||
export * from "./parser";
|
||||
export * from "./interpreter";
|
||||
export * from "./SymbolTable";
|
||||
|
@ -1,10 +1,255 @@
|
||||
import { parse, type LambdaTerm } from ".";
|
||||
import {
|
||||
parse,
|
||||
type LambdaTerm,
|
||||
isVariable,
|
||||
isApplication,
|
||||
isAbstraction,
|
||||
SymbolTable,
|
||||
} from ".";
|
||||
|
||||
export const evaluate = (_term: LambdaTerm): LambdaTerm => {
|
||||
return "";
|
||||
export class InvalidLambdaTermError extends Error {}
|
||||
|
||||
export type DebrujinAbstraction = {
|
||||
abstraction: {
|
||||
param: string;
|
||||
body: DebrujinifiedLambdaTerm;
|
||||
};
|
||||
};
|
||||
|
||||
export const interpret = (term: string): LambdaTerm => {
|
||||
export type DebrujinApplication = {
|
||||
application: {
|
||||
left: DebrujinifiedLambdaTerm;
|
||||
args: Array<DebrujinifiedLambdaTerm>;
|
||||
};
|
||||
};
|
||||
|
||||
export type DebrujinIndex = { name: string; index: number };
|
||||
|
||||
export type DebrujinifiedLambdaTerm =
|
||||
| DebrujinAbstraction
|
||||
| DebrujinApplication
|
||||
| DebrujinIndex;
|
||||
|
||||
export const debrujinify = (
|
||||
term: LambdaTerm,
|
||||
symbolTable: SymbolTable,
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if (isVariable(term)) {
|
||||
if (!symbolTable.has(term)) {
|
||||
throw new InvalidLambdaTermError(`Undefined variable: ${term}`);
|
||||
}
|
||||
return { index: symbolTable.get(term), name: term };
|
||||
}
|
||||
|
||||
if (isAbstraction(term)) {
|
||||
const newSymbolTable = symbolTable.createChild();
|
||||
newSymbolTable.add(term.abstraction.param);
|
||||
|
||||
const { body, param } = term.abstraction;
|
||||
return {
|
||||
abstraction: {
|
||||
param,
|
||||
body: debrujinify(body, newSymbolTable),
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
if (isApplication(term)) {
|
||||
const { left, args } = term.application;
|
||||
return {
|
||||
application: {
|
||||
left: debrujinify(left, symbolTable),
|
||||
args: args.map((arg) => debrujinify(arg, symbolTable)),
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
);
|
||||
};
|
||||
|
||||
export const substitute = (
|
||||
inTerm: DebrujinifiedLambdaTerm,
|
||||
index: number,
|
||||
withTerm: DebrujinifiedLambdaTerm,
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if ("index" in inTerm) {
|
||||
if (inTerm.index > index) {
|
||||
return adjustIndices(inTerm, -1);
|
||||
}
|
||||
if (index === inTerm.index) {
|
||||
return withTerm;
|
||||
}
|
||||
return inTerm;
|
||||
}
|
||||
|
||||
if ("application" in inTerm) {
|
||||
const { left, args } = inTerm.application;
|
||||
|
||||
return {
|
||||
application: {
|
||||
left: substitute(left, index, withTerm),
|
||||
args: args.map((arg) => substitute(arg, index, withTerm)),
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
if ("abstraction" in inTerm) {
|
||||
const { param, body } = inTerm.abstraction;
|
||||
const newBody = substitute(body, index + 1, withTerm);
|
||||
|
||||
return {
|
||||
abstraction: {
|
||||
param,
|
||||
body: newBody,
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(inTerm)}`,
|
||||
);
|
||||
};
|
||||
|
||||
export const adjustIndices = (
|
||||
term: DebrujinifiedLambdaTerm,
|
||||
delta: number,
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if ("index" in term) {
|
||||
return {
|
||||
...term,
|
||||
index: term.index + delta,
|
||||
};
|
||||
}
|
||||
|
||||
if ("application" in term) {
|
||||
const { left, args } = term.application;
|
||||
|
||||
return {
|
||||
application: {
|
||||
left: adjustIndices(left, delta),
|
||||
args: args.map((arg) => adjustIndices(arg, delta)),
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
if ("abstraction" in term) {
|
||||
const { body, param } = term.abstraction;
|
||||
|
||||
return {
|
||||
abstraction: {
|
||||
body: adjustIndices(body, delta),
|
||||
param,
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
);
|
||||
};
|
||||
|
||||
export const betaReduce = (
|
||||
term: DebrujinifiedLambdaTerm,
|
||||
): DebrujinifiedLambdaTerm => {
|
||||
if ("index" in term) {
|
||||
return term;
|
||||
}
|
||||
|
||||
if ("abstraction" in term) {
|
||||
const { body, param } = term.abstraction;
|
||||
|
||||
return {
|
||||
abstraction: {
|
||||
body: betaReduce(body),
|
||||
param,
|
||||
},
|
||||
};
|
||||
}
|
||||
|
||||
if ("application" in term) {
|
||||
const { left } = term.application;
|
||||
const args = term.application.args.map(betaReduce);
|
||||
|
||||
return args.reduce((acc: DebrujinifiedLambdaTerm, x) => {
|
||||
if ("abstraction" in acc) {
|
||||
const { body } = acc.abstraction;
|
||||
const newBody = substitute(body, 1, x);
|
||||
return newBody;
|
||||
}
|
||||
if ("application" in acc) {
|
||||
const {
|
||||
application: { left, args },
|
||||
} = acc;
|
||||
return {
|
||||
application: {
|
||||
left,
|
||||
args: [...args, x],
|
||||
},
|
||||
};
|
||||
}
|
||||
return { application: { left: acc, args: [x] } };
|
||||
}, left);
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
);
|
||||
};
|
||||
|
||||
export const interpret = (term: string): DebrujinifiedLambdaTerm => {
|
||||
const ast = parse(term);
|
||||
return evaluate(ast);
|
||||
const symbolTable = new SymbolTable();
|
||||
const debrujined = debrujinify(ast, symbolTable);
|
||||
|
||||
let prev = debrujined;
|
||||
let next = betaReduce(prev);
|
||||
|
||||
while (emitDebrujin(prev) !== emitDebrujin(next)) {
|
||||
// alpha equivalence
|
||||
prev = next;
|
||||
next = betaReduce(prev);
|
||||
}
|
||||
return next;
|
||||
};
|
||||
|
||||
export const emitDebrujin = (term: DebrujinifiedLambdaTerm): string => {
|
||||
if ("index" in term) {
|
||||
return term.index.toString();
|
||||
}
|
||||
|
||||
if ("abstraction" in term) {
|
||||
return `λ.${emitDebrujin(term.abstraction.body)}`;
|
||||
}
|
||||
|
||||
if ("application" in term) {
|
||||
return `(${emitDebrujin(term.application.left)} ${term.application.args
|
||||
.map(emitDebrujin)
|
||||
.join(" ")})`;
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(
|
||||
`Invalid lambda term: ${JSON.stringify(term)}`,
|
||||
);
|
||||
};
|
||||
|
||||
export const emitNamed = (term: DebrujinifiedLambdaTerm): string => {
|
||||
if ("name" in term) {
|
||||
return term.name;
|
||||
}
|
||||
|
||||
if ("abstraction" in term) {
|
||||
return `(λ (${term.abstraction.param}) . ${emitNamed(
|
||||
term.abstraction.body,
|
||||
)})`;
|
||||
}
|
||||
|
||||
if ("application" in term) {
|
||||
return `(${emitNamed(term.application.left)} ${term.application.args
|
||||
.map(emitNamed)
|
||||
.join(" ")})`;
|
||||
}
|
||||
|
||||
throw new InvalidLambdaTermError(`Invalid lambda term: ${term}`);
|
||||
};
|
||||
|
Loading…
Reference in New Issue
Block a user