From 0269412033728667acef789d01972ceeedcd7d4c Mon Sep 17 00:00:00 2001 From: Ryan Reilly Date: Sun, 14 Apr 2024 14:37:16 -0400 Subject: [PATCH 1/2] Slightly better format. Initial commit --- src/AEG/AEGTree.ts | 12 ++++++++++++ src/AEG/CutNode.ts | 26 ++++++++++++++++++++++++++ src/index.ts | 12 ++++++------ 3 files changed, 44 insertions(+), 6 deletions(-) diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index 3f2b6a31..48b8b755 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -258,8 +258,20 @@ export class AEGTree { return this.sheet.isEqualTo(otherTree.sheet); } + /** + * Returns a formatted string for downloaded proof files. + * This format was introduced for proof files having their auto-generated names displayed on + * applications like Discord. + * + * @returns Formatted string for downloaded proof files. + */ + public toDownloadString(): string { + return this.internalSheet.toDownloadString(); + } + /** * Returns a string representation of this AEGTree. + * * @returns Structured ordering of all children in this AEGTree in string form. */ public toString(): string { diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index 81fd9aaa..6b23d848 100644 --- a/src/AEG/CutNode.ts +++ b/src/AEG/CutNode.ts @@ -412,6 +412,32 @@ export class CutNode { return formulaString; } + /** + * Creates and returns a formatted string for this CutNode and its children. + * As opposed to the above format, this auto-generated format + * can be displayed on applications like Discord. + * + * @returns Friendlier auto-generated string format. + */ + public toDownloadString(): string { + let downloadString = ""; + + for (const child of this.internalChildren) { + if (child instanceof AtomNode) { + downloadString += child.identifier; + } else if (child instanceof CutNode) { + downloadString += child.toDownloadString(); + } + downloadString += " "; + } + downloadString = downloadString.slice(0, -1); + + if (downloadString === "") { + downloadString += "NO_ASSUMPTIONS"; + } + return downloadString; + } + /** * Creates and returns a string representation of this CutNode. * @returns Children and boundary of this CutNode in string form. diff --git a/src/index.ts b/src/index.ts index e10ac301..71aba2cc 100644 --- a/src/index.ts +++ b/src/index.ts @@ -208,7 +208,7 @@ export function aegStringify(treeData: AEGTree | ProofModeNode[]): string { /** * Calls appropriate methods to save the current AEGTree as a file. */ -async function saveMode() { +async function saveMode(): Promise { let name: string; let data: AEGTree | ProofModeNode[]; @@ -216,13 +216,13 @@ async function saveMode() { name = "AEG Tree"; data = TreeContext.tree; } else { - if (TreeContext.proof.length === 0) { - name = "[] \u2192 []"; + if (TreeContext.proof.length === 1) { + name = "Empty Proof"; } else { name = - TreeContext.proof[0].tree.toString() + - "\u2192" + - TreeContext.getLastProofStep().tree.toString(); + TreeContext.proof[0].tree.toDownloadString() + + "___YIELDS___" + + TreeContext.getLastProofStep().tree.toDownloadString(); } data = TreeContext.proof; } From a894438e429132c2c44212cf6c776a981b0be25d Mon Sep 17 00:00:00 2001 From: Ryan Reilly Date: Sun, 14 Apr 2024 21:59:09 -0400 Subject: [PATCH 2/2] Kids these days and their gosh darn unicodes... --- src/AEG/AEGTree.ts | 11 ----------- src/AEG/CutNode.ts | 26 -------------------------- src/index.ts | 8 ++++---- 3 files changed, 4 insertions(+), 41 deletions(-) diff --git a/src/AEG/AEGTree.ts b/src/AEG/AEGTree.ts index 48b8b755..c2898f6c 100644 --- a/src/AEG/AEGTree.ts +++ b/src/AEG/AEGTree.ts @@ -258,17 +258,6 @@ export class AEGTree { return this.sheet.isEqualTo(otherTree.sheet); } - /** - * Returns a formatted string for downloaded proof files. - * This format was introduced for proof files having their auto-generated names displayed on - * applications like Discord. - * - * @returns Formatted string for downloaded proof files. - */ - public toDownloadString(): string { - return this.internalSheet.toDownloadString(); - } - /** * Returns a string representation of this AEGTree. * diff --git a/src/AEG/CutNode.ts b/src/AEG/CutNode.ts index 6b23d848..81fd9aaa 100644 --- a/src/AEG/CutNode.ts +++ b/src/AEG/CutNode.ts @@ -412,32 +412,6 @@ export class CutNode { return formulaString; } - /** - * Creates and returns a formatted string for this CutNode and its children. - * As opposed to the above format, this auto-generated format - * can be displayed on applications like Discord. - * - * @returns Friendlier auto-generated string format. - */ - public toDownloadString(): string { - let downloadString = ""; - - for (const child of this.internalChildren) { - if (child instanceof AtomNode) { - downloadString += child.identifier; - } else if (child instanceof CutNode) { - downloadString += child.toDownloadString(); - } - downloadString += " "; - } - downloadString = downloadString.slice(0, -1); - - if (downloadString === "") { - downloadString += "NO_ASSUMPTIONS"; - } - return downloadString; - } - /** * Creates and returns a string representation of this CutNode. * @returns Children and boundary of this CutNode in string form. diff --git a/src/index.ts b/src/index.ts index 71aba2cc..106e6169 100644 --- a/src/index.ts +++ b/src/index.ts @@ -217,12 +217,12 @@ async function saveMode(): Promise { data = TreeContext.tree; } else { if (TreeContext.proof.length === 1) { - name = "Empty Proof"; + name = "One-Step Proof"; } else { name = - TreeContext.proof[0].tree.toDownloadString() + - "___YIELDS___" + - TreeContext.getLastProofStep().tree.toDownloadString(); + TreeContext.proof[0].tree.toString() + + " PROVES " + + TreeContext.getLastProofStep().tree.toString(); } data = TreeContext.proof; }