From 0c476e92e1807928ffb30864126076ef4c6a0821 Mon Sep 17 00:00:00 2001 From: Elizabeth Hunt Date: Tue, 13 Feb 2024 20:00:02 -0700 Subject: add all the stuff --- src/components/function_box.tsx | 151 ++-- src/components/lambda_reducer.tsx | 188 +++++ src/parser/grammar.pegjs | 27 + src/parser/parser.ts | 1282 ++++++++++++++++++++++++++++++ src/project.meta | 4 +- src/scenes/boolean_algebra_lambda.meta | 5 + src/scenes/boolean_algebra_lambda.tsx | 49 ++ src/scenes/boolean_encoding.meta | 5 + src/scenes/boolean_encoding.tsx | 42 + src/scenes/church_encoding.meta | 5 + src/scenes/church_encoding.tsx | 41 + src/scenes/currying.meta | 5 + src/scenes/currying.tsx | 114 +++ src/scenes/currying_detail.meta | 5 + src/scenes/currying_detail.tsx | 155 ++++ src/scenes/dna.meta | 5 + src/scenes/dna.tsx | 22 + src/scenes/function_dna.meta | 5 + src/scenes/function_dna.tsx | 91 +++ src/scenes/further.meta | 5 + src/scenes/further.tsx | 43 + src/scenes/generalized.tsx | 6 +- src/scenes/impostor.meta | 5 + src/scenes/impostor.tsx | 134 ++++ src/scenes/index.ts | 58 +- src/scenes/lambda_recursion.meta | 5 + src/scenes/lambda_recursion.tsx | 45 ++ src/scenes/lambda_reduction_example.meta | 5 + src/scenes/lambda_reduction_example.tsx | 47 ++ src/scenes/me.tsx | 8 +- src/scenes/parttwo.meta | 5 + src/scenes/parttwo.tsx | 16 + src/scenes/pros_cons.meta | 5 + src/scenes/pros_cons.tsx | 61 ++ src/scenes/questions.meta | 5 + src/scenes/questions.tsx | 16 + src/scenes/recursion.meta | 5 + src/scenes/recursion.tsx | 36 + src/scenes/reductions.meta | 5 + src/scenes/reductions.tsx | 40 + src/scenes/substitution.meta | 5 + src/scenes/substitution.tsx | 45 ++ src/scenes/the_lambda_calculus.meta | 5 + src/scenes/the_lambda_calculus.tsx | 40 + src/utils/lambdas.ts | 35 + src/utils/levenshtein.ts | 103 +++ 46 files changed, 2906 insertions(+), 83 deletions(-) create mode 100644 src/components/lambda_reducer.tsx create mode 100644 src/parser/grammar.pegjs create mode 100644 src/parser/parser.ts create mode 100644 src/scenes/boolean_algebra_lambda.meta create mode 100644 src/scenes/boolean_algebra_lambda.tsx create mode 100644 src/scenes/boolean_encoding.meta create mode 100644 src/scenes/boolean_encoding.tsx create mode 100644 src/scenes/church_encoding.meta create mode 100644 src/scenes/church_encoding.tsx create mode 100644 src/scenes/currying.meta create mode 100644 src/scenes/currying.tsx create mode 100644 src/scenes/currying_detail.meta create mode 100644 src/scenes/currying_detail.tsx create mode 100644 src/scenes/dna.meta create mode 100644 src/scenes/dna.tsx create mode 100644 src/scenes/function_dna.meta create mode 100644 src/scenes/function_dna.tsx create mode 100644 src/scenes/further.meta create mode 100644 src/scenes/further.tsx create mode 100644 src/scenes/impostor.meta create mode 100644 src/scenes/impostor.tsx create mode 100644 src/scenes/lambda_recursion.meta create mode 100644 src/scenes/lambda_recursion.tsx create mode 100644 src/scenes/lambda_reduction_example.meta create mode 100644 src/scenes/lambda_reduction_example.tsx create mode 100644 src/scenes/parttwo.meta create mode 100644 src/scenes/parttwo.tsx create mode 100644 src/scenes/pros_cons.meta create mode 100644 src/scenes/pros_cons.tsx create mode 100644 src/scenes/questions.meta create mode 100644 src/scenes/questions.tsx create mode 100644 src/scenes/recursion.meta create mode 100644 src/scenes/recursion.tsx create mode 100644 src/scenes/reductions.meta create mode 100644 src/scenes/reductions.tsx create mode 100644 src/scenes/substitution.meta create mode 100644 src/scenes/substitution.tsx create mode 100644 src/scenes/the_lambda_calculus.meta create mode 100644 src/scenes/the_lambda_calculus.tsx create mode 100644 src/utils/lambdas.ts create mode 100644 src/utils/levenshtein.ts (limited to 'src') diff --git a/src/components/function_box.tsx b/src/components/function_box.tsx index e1ed497..9f72979 100644 --- a/src/components/function_box.tsx +++ b/src/components/function_box.tsx @@ -72,9 +72,13 @@ export class FunctionBox extends Node { this.padding = props?.padding ?? 100; this.workingText = props?.workingText ?? "👷‍♀️⚙️"; + this.idlingText = props?.idlingText ?? "😴"; this.isChild = props?.isChild ?? false; + if (this.isChild) { + this.idlingText += " | 🧬"; + } this.outputFontSize = props?.outputFontSize ?? 30; this.inputFontSize = props?.inputFontSize ?? 30; @@ -82,80 +86,97 @@ export class FunctionBox extends Node { this.add( - - {range(this.arity).map((i) => ( - - + + {range(this.arity).map((i) => ( + + + + + + ))} + + + + + {this.idlingText} + + + + code={this.source} + > + + + + + - ))} - - - - - {this.idlingText} - - - - - - - - - - , @@ -252,11 +273,15 @@ export class FunctionBox extends Node { const output = this.function(...this.currentArgs.map((input) => input.val)); switch (typeof output) { case "function": + console.dir(output); + yield this.output().add( , ); 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; +} + +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; + } +} diff --git a/src/parser/grammar.pegjs b/src/parser/grammar.pegjs new file mode 100644 index 0000000..48a7564 --- /dev/null +++ b/src/parser/grammar.pegjs @@ -0,0 +1,27 @@ +LambdaTerm + = Abstraction + / Application + / Variable + +Application + = LPAREN _? left:LambdaTerm _? right:LambdaTerm _? RPAREN { + return { left, right }; + } + +Abstraction + = LPAREN _? LAMBDA _? param:Variable _? DOT _? body:LambdaTerm _? RPAREN { + return { param, body }; + } + +Variable + = name:([a-zA-Z][A-Z0-9a-z]*) { return { name: name[0] + name[1].join('') }; } + +LAMBDA = "λ" + +DOT = "." + +LPAREN = "(" + +RPAREN = ")" + +_ = (" " / "\n" / "\t" / "\t\n")+ \ No newline at end of file diff --git a/src/parser/parser.ts b/src/parser/parser.ts new file mode 100644 index 0000000..3dcbd6c --- /dev/null +++ b/src/parser/parser.ts @@ -0,0 +1,1282 @@ +/* eslint-disable */ + + + +const peggyParser: {parse: any, SyntaxError: any, DefaultTracer?: any} = // Generated by Peggy 3.0.2. +// +// https://peggyjs.org/ +// @ts-ignore +(function() { +// @ts-ignore + "use strict"; + +// @ts-ignore +function peg$subclass(child, parent) { +// @ts-ignore + function C() { this.constructor = child; } +// @ts-ignore + C.prototype = parent.prototype; +// @ts-ignore + child.prototype = new C(); +} + +// @ts-ignore +function peg$SyntaxError(message, expected, found, location) { +// @ts-ignore + var self = Error.call(this, message); + // istanbul ignore next Check is a necessary evil to support older environments +// @ts-ignore + if (Object.setPrototypeOf) { +// @ts-ignore + Object.setPrototypeOf(self, peg$SyntaxError.prototype); + } +// @ts-ignore + self.expected = expected; +// @ts-ignore + self.found = found; +// @ts-ignore + self.location = location; +// @ts-ignore + self.name = "SyntaxError"; +// @ts-ignore + return self; +} + +// @ts-ignore +peg$subclass(peg$SyntaxError, Error); + +// @ts-ignore +function peg$padEnd(str, targetLength, padString) { +// @ts-ignore + padString = padString || " "; +// @ts-ignore + if (str.length > targetLength) { return str; } +// @ts-ignore + targetLength -= str.length; +// @ts-ignore + padString += padString.repeat(targetLength); +// @ts-ignore + return str + padString.slice(0, targetLength); +} + +// @ts-ignore +peg$SyntaxError.prototype.format = function(sources) { +// @ts-ignore + var str = "Error: " + this.message; +// @ts-ignore + if (this.location) { +// @ts-ignore + var src = null; +// @ts-ignore + var k; +// @ts-ignore + for (k = 0; k < sources.length; k++) { +// @ts-ignore + if (sources[k].source === this.location.source) { +// @ts-ignore + src = sources[k].text.split(/\r\n|\n|\r/g); +// @ts-ignore + break; + } + } +// @ts-ignore + var s = this.location.start; +// @ts-ignore + var offset_s = (this.location.source && (typeof this.location.source.offset === "function")) +// @ts-ignore + ? this.location.source.offset(s) +// @ts-ignore + : s; +// @ts-ignore + var loc = this.location.source + ":" + offset_s.line + ":" + offset_s.column; +// @ts-ignore + if (src) { +// @ts-ignore + var e = this.location.end; +// @ts-ignore + var filler = peg$padEnd("", offset_s.line.toString().length, ' '); +// @ts-ignore + var line = src[s.line - 1]; +// @ts-ignore + var last = s.line === e.line ? e.column : line.length + 1; +// @ts-ignore + var hatLen = (last - s.column) || 1; +// @ts-ignore + str += "\n --> " + loc + "\n" +// @ts-ignore + + filler + " |\n" +// @ts-ignore + + offset_s.line + " | " + line + "\n" +// @ts-ignore + + filler + " | " + peg$padEnd("", s.column - 1, ' ') +// @ts-ignore + + peg$padEnd("", hatLen, "^"); +// @ts-ignore + } else { +// @ts-ignore + str += "\n at " + loc; + } + } +// @ts-ignore + return str; +}; + +// @ts-ignore +peg$SyntaxError.buildMessage = function(expected, found) { +// @ts-ignore + var DESCRIBE_EXPECTATION_FNS = { +// @ts-ignore + literal: function(expectation) { +// @ts-ignore + return "\"" + literalEscape(expectation.text) + "\""; + }, + +// @ts-ignore + class: function(expectation) { +// @ts-ignore + var escapedParts = expectation.parts.map(function(part) { +// @ts-ignore + return Array.isArray(part) +// @ts-ignore + ? classEscape(part[0]) + "-" + classEscape(part[1]) +// @ts-ignore + : classEscape(part); + }); + +// @ts-ignore + return "[" + (expectation.inverted ? "^" : "") + escapedParts.join("") + "]"; + }, + +// @ts-ignore + any: function() { +// @ts-ignore + return "any character"; + }, + +// @ts-ignore + end: function() { +// @ts-ignore + return "end of input"; + }, + +// @ts-ignore + other: function(expectation) { +// @ts-ignore + return expectation.description; + } + }; + +// @ts-ignore + function hex(ch) { +// @ts-ignore + return ch.charCodeAt(0).toString(16).toUpperCase(); + } + +// @ts-ignore + function literalEscape(s) { +// @ts-ignore + return s +// @ts-ignore + .replace(/\\/g, "\\\\") +// @ts-ignore + .replace(/"/g, "\\\"") +// @ts-ignore + .replace(/\0/g, "\\0") +// @ts-ignore + .replace(/\t/g, "\\t") +// @ts-ignore + .replace(/\n/g, "\\n") +// @ts-ignore + .replace(/\r/g, "\\r") +// @ts-ignore + .replace(/[\x00-\x0F]/g, function(ch) { return "\\x0" + hex(ch); }) +// @ts-ignore + .replace(/[\x10-\x1F\x7F-\x9F]/g, function(ch) { return "\\x" + hex(ch); }); + } + +// @ts-ignore + function classEscape(s) { +// @ts-ignore + return s +// @ts-ignore + .replace(/\\/g, "\\\\") +// @ts-ignore + .replace(/\]/g, "\\]") +// @ts-ignore + .replace(/\^/g, "\\^") +// @ts-ignore + .replace(/-/g, "\\-") +// @ts-ignore + .replace(/\0/g, "\\0") +// @ts-ignore + .replace(/\t/g, "\\t") +// @ts-ignore + .replace(/\n/g, "\\n") +// @ts-ignore + .replace(/\r/g, "\\r") +// @ts-ignore + .replace(/[\x00-\x0F]/g, function(ch) { return "\\x0" + hex(ch); }) +// @ts-ignore + .replace(/[\x10-\x1F\x7F-\x9F]/g, function(ch) { return "\\x" + hex(ch); }); + } + +// @ts-ignore + function describeExpectation(expectation) { +// @ts-ignore + return DESCRIBE_EXPECTATION_FNS[expectation.type](expectation); + } + +// @ts-ignore + function describeExpected(expected) { +// @ts-ignore + var descriptions = expected.map(describeExpectation); +// @ts-ignore + var i, j; + +// @ts-ignore + descriptions.sort(); + +// @ts-ignore + if (descriptions.length > 0) { +// @ts-ignore + for (i = 1, j = 1; i < descriptions.length; i++) { +// @ts-ignore + if (descriptions[i - 1] !== descriptions[i]) { +// @ts-ignore + descriptions[j] = descriptions[i]; +// @ts-ignore + j++; + } + } +// @ts-ignore + descriptions.length = j; + } + +// @ts-ignore + switch (descriptions.length) { +// @ts-ignore + case 1: +// @ts-ignore + return descriptions[0]; + +// @ts-ignore + case 2: +// @ts-ignore + return descriptions[0] + " or " + descriptions[1]; + +// @ts-ignore + default: +// @ts-ignore + return descriptions.slice(0, -1).join(", ") +// @ts-ignore + + ", or " +// @ts-ignore + + descriptions[descriptions.length - 1]; + } + } + +// @ts-ignore + function describeFound(found) { +// @ts-ignore + return found ? "\"" + literalEscape(found) + "\"" : "end of input"; + } + +// @ts-ignore + return "Expected " + describeExpected(expected) + " but " + describeFound(found) + " found."; +}; + +// @ts-ignore +function peg$parse(input, options) { +// @ts-ignore + options = options !== undefined ? options : {}; + +// @ts-ignore + var peg$FAILED = {}; +// @ts-ignore + var peg$source = options.grammarSource; + +// @ts-ignore + var peg$startRuleFunctions = { LambdaTerm: peg$parseLambdaTerm }; +// @ts-ignore + var peg$startRuleFunction = peg$parseLambdaTerm; + +// @ts-ignore + var peg$c0 = "\u03BB"; + var peg$c1 = "."; + var peg$c2 = "("; + var peg$c3 = ")"; + var peg$c4 = " "; + var peg$c5 = "\n"; + var peg$c6 = "\t"; + var peg$c7 = "\t\n"; + + var peg$r0 = /^[a-zA-Z]/; + var peg$r1 = /^[A-Z0-9a-z]/; + + var peg$e0 = peg$classExpectation([["a", "z"], ["A", "Z"]], false, false); + var peg$e1 = peg$classExpectation([["A", "Z"], ["0", "9"], ["a", "z"]], false, false); + var peg$e2 = peg$literalExpectation("\u03BB", false); + var peg$e3 = peg$literalExpectation(".", false); + var peg$e4 = peg$literalExpectation("(", false); + var peg$e5 = peg$literalExpectation(")", false); + var peg$e6 = peg$literalExpectation(" ", false); + var peg$e7 = peg$literalExpectation("\n", false); + var peg$e8 = peg$literalExpectation("\t", false); + var peg$e9 = peg$literalExpectation("\t\n", false); +// @ts-ignore + + var peg$f0 = function(left, right) { +// @ts-ignore + return { left, right }; + };// @ts-ignore + + var peg$f1 = function(param, body) { +// @ts-ignore + return { param, body }; + };// @ts-ignore + + var peg$f2 = function(name) {// @ts-ignore + return { name: name[0] + name[1].join('') }; }; +// @ts-ignore + var peg$currPos = 0; +// @ts-ignore + var peg$savedPos = 0; +// @ts-ignore + var peg$posDetailsCache = [{ line: 1, column: 1 }]; +// @ts-ignore + var peg$maxFailPos = 0; +// @ts-ignore + var peg$maxFailExpected = []; +// @ts-ignore + var peg$silentFails = 0; + +// @ts-ignore + var peg$result; + +// @ts-ignore + if ("startRule" in options) { +// @ts-ignore + if (!(options.startRule in peg$startRuleFunctions)) { +// @ts-ignore + throw new Error("Can't start parsing from rule \"" + options.startRule + "\"."); + } + +// @ts-ignore + peg$startRuleFunction = peg$startRuleFunctions[options.startRule]; + } + +// @ts-ignore + function text() { +// @ts-ignore + return input.substring(peg$savedPos, peg$currPos); + } + +// @ts-ignore + function offset() { +// @ts-ignore + return peg$savedPos; + } + +// @ts-ignore + function range() { +// @ts-ignore + return { +// @ts-ignore + source: peg$source, +// @ts-ignore + start: peg$savedPos, +// @ts-ignore + end: peg$currPos + }; + } + +// @ts-ignore + function location() { +// @ts-ignore + return peg$computeLocation(peg$savedPos, peg$currPos); + } + +// @ts-ignore + function expected(description, location) { +// @ts-ignore + location = location !== undefined +// @ts-ignore + ? location +// @ts-ignore + : peg$computeLocation(peg$savedPos, peg$currPos); + +// @ts-ignore + throw peg$buildStructuredError( +// @ts-ignore + [peg$otherExpectation(description)], +// @ts-ignore + input.substring(peg$savedPos, peg$currPos), +// @ts-ignore + location + ); + } + +// @ts-ignore + function error(message, location) { +// @ts-ignore + location = location !== undefined +// @ts-ignore + ? location +// @ts-ignore + : peg$computeLocation(peg$savedPos, peg$currPos); + +// @ts-ignore + throw peg$buildSimpleError(message, location); + } + +// @ts-ignore + function peg$literalExpectation(text, ignoreCase) { +// @ts-ignore + return { type: "literal", text: text, ignoreCase: ignoreCase }; + } + +// @ts-ignore + function peg$classExpectation(parts, inverted, ignoreCase) { +// @ts-ignore + return { type: "class", parts: parts, inverted: inverted, ignoreCase: ignoreCase }; + } + +// @ts-ignore + function peg$anyExpectation() { +// @ts-ignore + return { type: "any" }; + } + +// @ts-ignore + function peg$endExpectation() { +// @ts-ignore + return { type: "end" }; + } + +// @ts-ignore + function peg$otherExpectation(description) { +// @ts-ignore + return { type: "other", description: description }; + } + +// @ts-ignore + function peg$computePosDetails(pos) { +// @ts-ignore + var details = peg$posDetailsCache[pos]; +// @ts-ignore + var p; + +// @ts-ignore + if (details) { +// @ts-ignore + return details; +// @ts-ignore + } else { +// @ts-ignore + p = pos - 1; +// @ts-ignore + while (!peg$posDetailsCache[p]) { +// @ts-ignore + p--; + } + +// @ts-ignore + details = peg$posDetailsCache[p]; +// @ts-ignore + details = { +// @ts-ignore + line: details.line, +// @ts-ignore + column: details.column + }; + +// @ts-ignore + while (p < pos) { +// @ts-ignore + if (input.charCodeAt(p) === 10) { +// @ts-ignore + details.line++; +// @ts-ignore + details.column = 1; +// @ts-ignore + } else { +// @ts-ignore + details.column++; + } + +// @ts-ignore + p++; + } + +// @ts-ignore + peg$posDetailsCache[pos] = details; + +// @ts-ignore + return details; + } + } + +// @ts-ignore + function peg$computeLocation(startPos, endPos, offset) { +// @ts-ignore + var startPosDetails = peg$computePosDetails(startPos); +// @ts-ignore + var endPosDetails = peg$computePosDetails(endPos); + +// @ts-ignore + var res = { +// @ts-ignore + source: peg$source, +// @ts-ignore + start: { +// @ts-ignore + offset: startPos, +// @ts-ignore + line: startPosDetails.line, +// @ts-ignore + column: startPosDetails.column + }, +// @ts-ignore + end: { +// @ts-ignore + offset: endPos, +// @ts-ignore + line: endPosDetails.line, +// @ts-ignore + column: endPosDetails.column + } + }; +// @ts-ignore + if (offset && peg$source && (typeof peg$source.offset === "function")) { +// @ts-ignore + res.start = peg$source.offset(res.start); +// @ts-ignore + res.end = peg$source.offset(res.end); + } +// @ts-ignore + return res; + } + +// @ts-ignore + function peg$fail(expected) { +// @ts-ignore + if (peg$currPos < peg$maxFailPos) { return; } + +// @ts-ignore + if (peg$currPos > peg$maxFailPos) { +// @ts-ignore + peg$maxFailPos = peg$currPos; +// @ts-ignore + peg$maxFailExpected = []; + } + +// @ts-ignore + peg$maxFailExpected.push(expected); + } + +// @ts-ignore + function peg$buildSimpleError(message, location) { +// @ts-ignore + return new peg$SyntaxError(message, null, null, location); + } + +// @ts-ignore + function peg$buildStructuredError(expected, found, location) { +// @ts-ignore + return new peg$SyntaxError( +// @ts-ignore + peg$SyntaxError.buildMessage(expected, found), +// @ts-ignore + expected, +// @ts-ignore + found, +// @ts-ignore + location + ); + } + +// @ts-ignore + function // @ts-ignore +peg$parseLambdaTerm() { +// @ts-ignore + var s0; + +// @ts-ignore + s0 = peg$parseAbstraction(); +// @ts-ignore + if (s0 === peg$FAILED) { +// @ts-ignore + s0 = peg$parseApplication(); +// @ts-ignore + if (s0 === peg$FAILED) { +// @ts-ignore + s0 = peg$parseVariable(); + } + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseApplication() { +// @ts-ignore + var s0, s1, s2, s3, s4, s5, s6, s7; + +// @ts-ignore + s0 = peg$currPos; +// @ts-ignore + s1 = peg$parseLPAREN(); +// @ts-ignore + if (s1 !== peg$FAILED) { +// @ts-ignore + s2 = peg$parse_(); +// @ts-ignore + if (s2 === peg$FAILED) { +// @ts-ignore + s2 = null; + } +// @ts-ignore + s3 = peg$parseLambdaTerm(); +// @ts-ignore + if (s3 !== peg$FAILED) { +// @ts-ignore + s4 = peg$parse_(); +// @ts-ignore + if (s4 === peg$FAILED) { +// @ts-ignore + s4 = null; + } +// @ts-ignore + s5 = peg$parseLambdaTerm(); +// @ts-ignore + if (s5 !== peg$FAILED) { +// @ts-ignore + s6 = peg$parse_(); +// @ts-ignore + if (s6 === peg$FAILED) { +// @ts-ignore + s6 = null; + } +// @ts-ignore + s7 = peg$parseRPAREN(); +// @ts-ignore + if (s7 !== peg$FAILED) { +// @ts-ignore + peg$savedPos = s0; +// @ts-ignore + s0 = peg$f0(s3, s5); +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseAbstraction() { +// @ts-ignore + var s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11; + +// @ts-ignore + s0 = peg$currPos; +// @ts-ignore + s1 = peg$parseLPAREN(); +// @ts-ignore + if (s1 !== peg$FAILED) { +// @ts-ignore + s2 = peg$parse_(); +// @ts-ignore + if (s2 === peg$FAILED) { +// @ts-ignore + s2 = null; + } +// @ts-ignore + s3 = peg$parseLAMBDA(); +// @ts-ignore + if (s3 !== peg$FAILED) { +// @ts-ignore + s4 = peg$parse_(); +// @ts-ignore + if (s4 === peg$FAILED) { +// @ts-ignore + s4 = null; + } +// @ts-ignore + s5 = peg$parseVariable(); +// @ts-ignore + if (s5 !== peg$FAILED) { +// @ts-ignore + s6 = peg$parse_(); +// @ts-ignore + if (s6 === peg$FAILED) { +// @ts-ignore + s6 = null; + } +// @ts-ignore + s7 = peg$parseDOT(); +// @ts-ignore + if (s7 !== peg$FAILED) { +// @ts-ignore + s8 = peg$parse_(); +// @ts-ignore + if (s8 === peg$FAILED) { +// @ts-ignore + s8 = null; + } +// @ts-ignore + s9 = peg$parseLambdaTerm(); +// @ts-ignore + if (s9 !== peg$FAILED) { +// @ts-ignore + s10 = peg$parse_(); +// @ts-ignore + if (s10 === peg$FAILED) { +// @ts-ignore + s10 = null; + } +// @ts-ignore + s11 = peg$parseRPAREN(); +// @ts-ignore + if (s11 !== peg$FAILED) { +// @ts-ignore + peg$savedPos = s0; +// @ts-ignore + s0 = peg$f1(s5, s9); +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s0; +// @ts-ignore + s0 = peg$FAILED; + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseVariable() { +// @ts-ignore + var s0, s1, s2, s3, s4; + +// @ts-ignore + s0 = peg$currPos; +// @ts-ignore + s1 = peg$currPos; +// @ts-ignore + if (peg$r0.test(input.charAt(peg$currPos))) { +// @ts-ignore + s2 = input.charAt(peg$currPos); +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s2 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e0); } + } +// @ts-ignore + if (s2 !== peg$FAILED) { +// @ts-ignore + s3 = []; +// @ts-ignore + if (peg$r1.test(input.charAt(peg$currPos))) { +// @ts-ignore + s4 = input.charAt(peg$currPos); +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s4 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e1); } + } +// @ts-ignore + while (s4 !== peg$FAILED) { +// @ts-ignore + s3.push(s4); +// @ts-ignore + if (peg$r1.test(input.charAt(peg$currPos))) { +// @ts-ignore + s4 = input.charAt(peg$currPos); +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s4 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e1); } + } + } +// @ts-ignore + s2 = [s2, s3]; +// @ts-ignore + s1 = s2; +// @ts-ignore + } else { +// @ts-ignore + peg$currPos = s1; +// @ts-ignore + s1 = peg$FAILED; + } +// @ts-ignore + if (s1 !== peg$FAILED) { +// @ts-ignore + peg$savedPos = s0; +// @ts-ignore + s1 = peg$f2(s1); + } +// @ts-ignore + s0 = s1; + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseLAMBDA() { +// @ts-ignore + var s0; + +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 955) { +// @ts-ignore + s0 = peg$c0; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s0 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e2); } + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseDOT() { +// @ts-ignore + var s0; + +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 46) { +// @ts-ignore + s0 = peg$c1; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s0 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e3); } + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseLPAREN() { +// @ts-ignore + var s0; + +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 40) { +// @ts-ignore + s0 = peg$c2; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s0 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e4); } + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parseRPAREN() { +// @ts-ignore + var s0; + +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 41) { +// @ts-ignore + s0 = peg$c3; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s0 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e5); } + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + function // @ts-ignore +peg$parse_() { +// @ts-ignore + var s0, s1; + +// @ts-ignore + s0 = []; +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 32) { +// @ts-ignore + s1 = peg$c4; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e6); } + } +// @ts-ignore + if (s1 === peg$FAILED) { +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 10) { +// @ts-ignore + s1 = peg$c5; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e7); } + } +// @ts-ignore + if (s1 === peg$FAILED) { +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 9) { +// @ts-ignore + s1 = peg$c6; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e8); } + } +// @ts-ignore + if (s1 === peg$FAILED) { +// @ts-ignore + if (input.substr(peg$currPos, 2) === peg$c7) { +// @ts-ignore + s1 = peg$c7; +// @ts-ignore + peg$currPos += 2; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e9); } + } + } + } + } +// @ts-ignore + if (s1 !== peg$FAILED) { +// @ts-ignore + while (s1 !== peg$FAILED) { +// @ts-ignore + s0.push(s1); +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 32) { +// @ts-ignore + s1 = peg$c4; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e6); } + } +// @ts-ignore + if (s1 === peg$FAILED) { +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 10) { +// @ts-ignore + s1 = peg$c5; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e7); } + } +// @ts-ignore + if (s1 === peg$FAILED) { +// @ts-ignore + if (input.charCodeAt(peg$currPos) === 9) { +// @ts-ignore + s1 = peg$c6; +// @ts-ignore + peg$currPos++; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e8); } + } +// @ts-ignore + if (s1 === peg$FAILED) { +// @ts-ignore + if (input.substr(peg$currPos, 2) === peg$c7) { +// @ts-ignore + s1 = peg$c7; +// @ts-ignore + peg$currPos += 2; +// @ts-ignore + } else { +// @ts-ignore + s1 = peg$FAILED; +// @ts-ignore + if (peg$silentFails === 0) { peg$fail(peg$e9); } + } + } + } + } + } +// @ts-ignore + } else { +// @ts-ignore + s0 = peg$FAILED; + } + +// @ts-ignore + return s0; + } + +// @ts-ignore + peg$result = peg$startRuleFunction(); + +// @ts-ignore + if (peg$result !== peg$FAILED && peg$currPos === input.length) { +// @ts-ignore + return peg$result; +// @ts-ignore + } else { +// @ts-ignore + if (peg$result !== peg$FAILED && peg$currPos < input.length) { +// @ts-ignore + peg$fail(peg$endExpectation()); + } + +// @ts-ignore + throw peg$buildStructuredError( +// @ts-ignore + peg$maxFailExpected, +// @ts-ignore + peg$maxFailPos < input.length ? input.charAt(peg$maxFailPos) : null, +// @ts-ignore + peg$maxFailPos < input.length +// @ts-ignore + ? peg$computeLocation(peg$maxFailPos, peg$maxFailPos + 1) +// @ts-ignore + : peg$computeLocation(peg$maxFailPos, peg$maxFailPos) + ); + } +} + +// @ts-ignore + return { + SyntaxError: peg$SyntaxError, + parse: peg$parse + }; +})() + +export interface FilePosition { + offset: number; + line: number; + column: number; +} + +export interface FileRange { + start: FilePosition; + end: FilePosition; + source: string; +} + +export interface LiteralExpectation { + type: "literal"; + text: string; + ignoreCase: boolean; +} + +export interface ClassParts extends Array {} + +export interface ClassExpectation { + type: "class"; + parts: ClassParts; + inverted: boolean; + ignoreCase: boolean; +} + +export interface AnyExpectation { + type: "any"; +} + +export interface EndExpectation { + type: "end"; +} + +export interface OtherExpectation { + type: "other"; + description: string; +} + +export type Expectation = LiteralExpectation | ClassExpectation | AnyExpectation | EndExpectation | OtherExpectation; + +declare class _PeggySyntaxError extends Error { + public static buildMessage(expected: Expectation[], found: string | null): string; + public message: string; + public expected: Expectation[]; + public found: string | null; + public location: FileRange; + public name: string; + constructor(message: string, expected: Expectation[], found: string | null, location: FileRange); + format(sources: { + source?: any; + text: string; + }[]): string; +} + +export interface TraceEvent { + type: string; + rule: string; + result?: any; + location: FileRange; + } + +declare class _DefaultTracer { + private indentLevel: number; + public trace(event: TraceEvent): void; +} + +peggyParser.SyntaxError.prototype.name = "PeggySyntaxError"; + +export interface ParseOptions { + filename?: string; + startRule?: "LambdaTerm"; + tracer?: any; + [key: string]: any; +} +export type ParseFunction = ( + input: string, + options?: Options + ) => Options extends { startRule: infer StartRule } ? + StartRule extends "LambdaTerm" ? LambdaTerm : LambdaTerm + : LambdaTerm; +export const parse: ParseFunction = peggyParser.parse; + +export const PeggySyntaxError = peggyParser.SyntaxError as typeof _PeggySyntaxError; + +export type PeggySyntaxError = _PeggySyntaxError; + +// These types were autogenerated by ts-pegjs +export type LambdaTerm = Abstraction | Application | Variable; +export type Application = { left: LambdaTerm; right: LambdaTerm }; +export type Abstraction = { param: Variable; body: LambdaTerm }; +export type Variable = { name: string }; +export type LAMBDA = "\u03bb"; +export type DOT = "."; +export type LPAREN = "("; +export type RPAREN = ")"; +export type _ = (" " | "\n" | "\t" | "\t\n")[]; diff --git a/src/project.meta b/src/project.meta index 7c59eb3..4ebbd36 100644 --- a/src/project.meta +++ b/src/project.meta @@ -3,8 +3,8 @@ "shared": { "background": "rgb(30,30,46)", "range": [ - 0, - 33.18333233333333 + 3.5666656666666667, + null ], "size": { "x": 1920, diff --git a/src/scenes/boolean_algebra_lambda.meta b/src/scenes/boolean_algebra_lambda.meta new file mode 100644 index 0000000..385a68c --- /dev/null +++ b/src/scenes/boolean_algebra_lambda.meta @@ -0,0 +1,5 @@ +{ + "version": 0, + "timeEvents": [], + "seed": 2667185663 +} \ No newline at end of file diff --git a/src/scenes/boolean_algebra_lambda.tsx b/src/scenes/boolean_algebra_lambda.tsx new file mode 100644 index 0000000..2639461 --- /dev/null +++ b/src/scenes/boolean_algebra_lambda.tsx @@ -0,0 +1,49 @@ +import { Layout, makeScene2D } from "@motion-canvas/2d"; +import { + Direction, + beginSlide, + createRef, + slideTransition, +} from "@motion-canvas/core"; +import { LambdaReducer } from "../components/lambda_reducer"; +import { baseDefinitions } from "../utils/lambdas"; + +export default makeScene2D(function* (view) { + const lambdaReducer = createRef(); + const layout = createRef(); + + view.add( + + ); + yield* slideTransition(Direction.Right); + yield* beginSlide("Boolean Reductions"); + + for (const term of [ + "((false one) zero)", + "((true one) zero)", + "(((if true) one) zero)", + ]) { + yield* layout().opacity(0, 0.5); + layout().add( + + ); + yield* layout().opacity(1, 0.5); + + yield* beginSlide("Next Reduction " + term); + for (let i = 0; !lambdaReducer().isDone(); i++) { + yield* lambdaReducer().step(0.5); + yield* beginSlide(term + " Next Step " + i); + } + layout().removeChildren(); + } +}); diff --git a/src/scenes/boolean_encoding.meta b/src/scenes/boolean_encoding.meta new file mode 100644 index 0000000..8f4d744 --- /dev/null +++ b/src/scenes/boolean_encoding.meta @@ -0,0 +1,5 @@ +{ + "version": 0, + "timeEvents": [], + "seed": 2394701117 +} \ No newline at end of file diff --git a/src/scenes/boolean_encoding.tsx b/src/scenes/boolean_encoding.tsx new file mode 100644 index 0000000..60a0ea9 --- /dev/null +++ b/src/scenes/boolean_encoding.tsx @@ -0,0 +1,42 @@ +import { Layout, Txt, makeScene2D } from "@motion-canvas/2d"; +import { + Direction, + beginSlide, + createRef, + slideTransition, +} from "@motion-canvas/core"; +import { theme } from "../theme"; + +const boolE = [ + "true = λ t . λ f . t", + "false = λ t . λ f . f", + "if = λ b . λ x . λ y . b x y", + "not = λ b . b false true", + "and = λ b . λ c . b c false", +]; + +export default makeScene2D(function* (view) { + const numerals = createRef(); + + view.add( + + + Boolean Encoding + + + + ); + + yield* slideTransition(Direction.Right); + yield* beginSlide("The Lambda Calculus - Boolean Encoding"); + + for (const bool of boolE) { + yield* numerals().text(numerals().text() + "\n\n" + bool, 1); + yield* beginSlide("boolean - " + bool); + } +}); diff --git a/src/scenes/church_encoding.meta b/src/scenes/church_encoding.meta new file mode 100644 index 0000000..638e825 --- /dev/null +++ b/src/scenes/church_encoding.meta @@ -0,0 +1,5 @@ +{ + "version": 0, + "timeEvents": [], + "seed": 533121975 +} \ No newline at end of file diff --git a/src/scenes/church_encoding.tsx b/src/scenes/church_encoding.tsx new file mode 100644 index 0000000..70bafe4 --- /dev/null +++ b/src/scenes/church_encoding.tsx @@ -0,0 +1,41 @@ +import { Layout, Txt, makeScene2D } from "@motion-canvas/2d"; +import { + Direction, + beginSlide, + createRef, + slideTransition, +} from "@motion-canvas/core"; +import { theme } from "../theme"; + +const churchNumerals = [ + "0 = λ f . λ x . x (no application of f)", + "1 = λ f . λ x . f x (one application of f)", + "2 = λ f . λ x . f (f x) (two applications of f)", + "succ = λ n . λ f . λ x . f ((n f) x)", +]; + +export default makeScene2D(function* (view) { + const numerals = createRef(); + + view.add( + + + Church Encoding + + + + ); + + yield* slideTransition(Direction.Right); + yield* beginSlide("The Lambda Calculus - Church Encoding"); + + for (const numeral of churchNumerals) { + yield* numerals().text(numerals().text() + "\n\n" + numeral, 1); + yield* beginSlide("substitution - " + numeral); + } +}); diff --git a/src/scenes/currying.meta b/src/scenes/currying.meta new file mode 100644 index 0000000..1dd71f1 --- /dev/null +++ b/src/scenes/currying.meta @@ -0,0 +1,5 @@ +{ + "version": 0, + "timeEvents": [], + "seed": 2262306570 +} \ No newline at end of file diff --git a/src/scenes/currying.tsx b/src/scenes/currying.tsx new file mode 100644 index 0000000..01ce24a --- /dev/null +++ b/src/scenes/currying.tsx @@ -0,0 +1,114 @@ +import { Video, Layout, makeScene2D } from "@motion-canvas/2d"; +import { + Direction, + all, + beginSlide, + createRef, + slideTransition, +} from "@motion-canvas/core"; +import { PEOPLE, Person, PersonI } from "../components/person"; +import { birthdayCardFn, valentineCardFn } from "./generalized"; +import { CardI } from "./birthday_letters"; +import { FunctionBox } from "../components/function_box"; +import curry from "../../public/img/curry.mp4"; + +export const cardGeneratorsFor = ( + person: PersonI, +): ((type: string) => () => CardI) => { + const birthdayCardGenerator = () => birthdayCardFn(person); + const valentineCardGenerator = () => valentineCardFn(person); + + const messageType = (type: string) => { + switch (type) { + case "valentine": + return valentineCardGenerator; + case "birthday": + return birthdayCardGenerator; + } + throw new Error(type + " not implemented"); + }; + + return messageType; +}; + +export const cardGeneratorsForSource = `const cardGeneratorsFor = (person: PersonI): ((type: string) => () => CardI) => { + const birthdayCardGenerator = () => birthdayCardFn(person); + const valentineCardGenerator = () => valentineCardFn(person); + + const generatorForType = (type: string) => { + switch (type) { + case "valentine": + return valentineCardGenerator; + case "birthday": + return birthdayCardGenerator; + } + + throw new Error(type + " not implemented"); + }; + + return generatorForType; +};`; + +export default makeScene2D(function* (view) { + const box = createRef(); + const vid = createRef