1 files changed, 188 insertions, 0 deletions
diff --git a/src/components/lambda_reducer.tsx b/src/components/lambda_reducer.tsx
new file mode 100644
index 0000000..bef8fde
--- /dev/null
+++ b/src/components/lambda_reducer.tsx
@@ -0,0 +1,188 @@
+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<string, string>;
+}
+
+export class LambdaReducer extends Node {
+  private readonly codeBlock = createRef<CodeBlock>();
+  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(
+      <CodeBlock
+        fontSize={25}
+        ref={this.codeBlock}
+        language="racket"
+        code={this.getReductions()}
+      ></CodeBlock>
+    );
+  }
+
+  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;
+  }
+}