import { Rect, Node, Txt, Line, NodeProps } from "@motion-canvas/2d"; import { createRef, all, range, makeRef, DEFAULT } from "@motion-canvas/core"; import { CodeBlock, insert, edit, lines, } from "@motion-canvas/2d/lib/components/CodeBlock"; import { Abstraction, Application, LambdaTerm, parse } from "../parser/parser"; import { EditOperation, calculateLevenshteinOperations, } from "../utils/levenshtein"; export interface LambdaReducerProps extends NodeProps { lambdaTerm?: string; definitions?: Record; } export class LambdaReducer extends Node { private readonly codeBlock = createRef(); private reductions: string[]; private ast: LambdaTerm; public constructor(props?: LambdaReducerProps) { super({ ...props, }); const functionDefinitions = props.definitions ?? {}; let lambdaTerm = props.lambdaTerm ?? "((λ x . x) (λ y . y))"; while ( Object.keys(functionDefinitions).some((x) => lambdaTerm.includes(x)) ) { lambdaTerm = Object.entries(functionDefinitions).reduce( (acc, [name, definition]) => { return acc.replace(new RegExp(name, "g"), definition); }, lambdaTerm ); } console.log(lambdaTerm); this.reductions = [props.lambdaTerm, lambdaTerm]; this.ast = parse(lambdaTerm); this.add( ); } private getReductions() { return this.reductions.filter((x) => x).join("\n=> "); } private isApplication(ast: any): boolean { return ast.left && ast.right; } private isAbstraction(ast: any): boolean { return ast.param && ast.body; } private isVariable(ast: any): boolean { return !!ast.name; } private substitute( ast: LambdaTerm, param: string, replacement: LambdaTerm ): LambdaTerm { const node = ast as any; if (this.isVariable(node)) { return node.name === param ? replacement : node; } else if (this.isApplication(node)) { const left = this.substitute(node.left, param, replacement); const right = this.substitute(node.right, param, replacement); return { left, right } as Application; } return { param: node.param, body: this.substitute(node.body, param, replacement) as Abstraction, }; } public getCode() { return this.emitCode(this.ast); } private betaReduceStep(ast: LambdaTerm): LambdaTerm { const node = ast as any; if (this.isApplication(node)) { const left = node.left as any; const right = node.right as any; if (this.isAbstraction(left)) { return this.substitute(left.body, left.param.name, right); } return { left: this.betaReduceStep(left), right: this.betaReduceStep(right), } as Application; } if (this.isAbstraction(node)) { return { param: node.param, body: this.betaReduceStep(node.body), } as Abstraction; } return node; } private emitCode(ast: LambdaTerm): string { const node = ast as any; if (this.isVariable(node)) { return node.name; } else if (this.isApplication(node)) { return `(${this.emitCode(node.left)} ${this.emitCode(node.right)})`; } else if (this.isAbstraction(node)) { return `(λ ${node.param.name}.${this.emitCode(node.body)})`; } throw new Error("Invalid lambda term"); } public isDone() { return ( this.emitCode(this.betaReduceStep(this.ast)) === this.emitCode(this.ast) ); } public *step(duration: number) { yield* this.codeBlock().selection([], 0); const old = this.getReductions(); const next = this.betaReduceStep(this.ast); const nextCode = this.emitCode(next); const operations = calculateLevenshteinOperations( this.reductions.at(-1), nextCode ); yield* this.codeBlock().edit(duration)`${old}${insert( "\n=> " + this.reductions.at(-1) )}`; let code = `this.codeBlock().edit(duration)\`${old}\\n=> `; // this is SO FUCKING CURSED window.editInLambda = edit; window.insertInLambda = insert; for (const { operation, diff } of operations) { const next = `'${diff.new ?? ""}'`; const old = `'${diff.old ?? ""}'`; if (operation === EditOperation.Edit) { code += `\${editInLambda(${old}, ${next})}`; continue; } if (operation === EditOperation.Insert) { code += `\${insertInLambda(${next})}`; continue; } code += diff.new ?? ""; } code += "`;"; yield* eval(code); yield* this.codeBlock().selection(lines(this.reductions.length), 0.3); this.reductions.push(nextCode); this.ast = next; } }