diff --git a/frontend/src/app/annotate/annotation-menu/annotation-menu.component.html b/frontend/src/app/annotate/annotation-menu/annotation-menu.component.html index dbea7eb0..820687f9 100644 --- a/frontend/src/app/annotate/annotation-menu/annotation-menu.component.html +++ b/frontend/src/app/annotate/annotation-menu/annotation-menu.component.html @@ -1,35 +1,54 @@ - - -
+@let proofs = proofs$ | async; + + + +
diff --git a/frontend/src/app/annotate/annotation-menu/annotation-menu.component.ts b/frontend/src/app/annotate/annotation-menu/annotation-menu.component.ts index f0c63cc3..1fdb4855 100644 --- a/frontend/src/app/annotate/annotation-menu/annotation-menu.component.ts +++ b/frontend/src/app/annotate/annotation-menu/annotation-menu.component.ts @@ -1,32 +1,37 @@ -import { Component } from "@angular/core"; +import { Component, inject } from "@angular/core"; +import { CommonModule } from "@angular/common"; import { FontAwesomeModule } from "@fortawesome/angular-fontawesome"; import { NgbNavModule } from "@ng-bootstrap/ng-bootstrap"; import { faSquarePollHorizontal, - faTree, faPenNib, } from "@fortawesome/free-solid-svg-icons"; + +import { ParseService } from "@/services/parse.service"; import { AnnotationParseResultsComponent } from "../annotation-parse-results/annotation-parse-results.component"; -import { AnnotationTableauComponent } from "../annotation-tableau/annotation-tableau.component"; +import { TableauSVG } from '../tableau-svg/tableau-svg.component'; import { AnnotationCommentsComponent } from "../annotation-comments/annotation-comments.component"; @Component({ selector: "la-annotation-menu", standalone: true, imports: [ + CommonModule, NgbNavModule, FontAwesomeModule, AnnotationParseResultsComponent, - AnnotationTableauComponent, + TableauSVG, AnnotationCommentsComponent, ], templateUrl: "./annotation-menu.component.html", styleUrl: "./annotation-menu.component.scss", }) export class AnnotationMenuComponent { + private parseService = inject(ParseService); + public readonly proofs$ = this.parseService.proofs$; + public active = 1; public faSquarePollHorizontal = faSquarePollHorizontal; - public faTree = faTree; public faPenNib = faPenNib; } diff --git a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.html b/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.html deleted file mode 100644 index 17691c03..00000000 --- a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.html +++ /dev/null @@ -1,3 +0,0 @@ -
- -
diff --git a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.spec.ts b/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.spec.ts deleted file mode 100644 index 45773c4c..00000000 --- a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.spec.ts +++ /dev/null @@ -1,22 +0,0 @@ -import { ComponentFixture, TestBed } from "@angular/core/testing"; - -import { AnnotationTableauComponent } from "./annotation-tableau.component"; - -describe("AnnotationTableauComponent", () => { - let component: AnnotationTableauComponent; - let fixture: ComponentFixture; - - beforeEach(async () => { - await TestBed.configureTestingModule({ - imports: [AnnotationTableauComponent], - }).compileComponents(); - - fixture = TestBed.createComponent(AnnotationTableauComponent); - component = fixture.componentInstance; - fixture.detectChanges(); - }); - - it("should create", () => { - expect(component).toBeTruthy(); - }); -}); diff --git a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.ts b/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.ts deleted file mode 100644 index 453539a2..00000000 --- a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.ts +++ /dev/null @@ -1,11 +0,0 @@ -import { Component } from "@angular/core"; -import { TableauSVG } from "../tableau-svg/tableau-svg.component"; - -@Component({ - selector: "la-annotation-tableau", - standalone: true, - imports: [TableauSVG], - templateUrl: "./annotation-tableau.component.html", - styleUrl: "./annotation-tableau.component.scss", -}) -export class AnnotationTableauComponent {} diff --git a/frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.scss b/frontend/src/app/annotate/tableau-svg/tableau-node.component.scss similarity index 100% rename from frontend/src/app/annotate/annotation-tableau/annotation-tableau.component.scss rename to frontend/src/app/annotate/tableau-svg/tableau-node.component.scss diff --git a/frontend/src/app/annotate/tableau-svg/tableau-node.component.svg b/frontend/src/app/annotate/tableau-svg/tableau-node.component.svg new file mode 100644 index 00000000..c6c9e03a --- /dev/null +++ b/frontend/src/app/annotate/tableau-svg/tableau-node.component.svg @@ -0,0 +1,33 @@ + +@if(id) { + + {{ id }} +} + +@if(mod) { + + {{ mod }} +} + +@if(sign != null) { + +} + +@if(end) { + + {{rule ? '⛌' : '⭘'}} +} +@else { + {{ head }} +} + +@if(args) { + + {{ args }} +} + +@if(rule || end) { +{{ rule || 'Open branch' }} +} + + diff --git a/frontend/src/app/annotate/tableau-svg/tableau-node.component.ts b/frontend/src/app/annotate/tableau-svg/tableau-node.component.ts new file mode 100644 index 00000000..d0ef0462 --- /dev/null +++ b/frontend/src/app/annotate/tableau-svg/tableau-node.component.ts @@ -0,0 +1,84 @@ +import { Component, ElementRef, Input, Output, ViewChild, EventEmitter } from '@angular/core'; +import { Dimensions } from '@/types'; + +@Component({ + selector: "[node]", + standalone: true, + imports: [], + templateUrl: "./tableau-node.component.svg", + styleUrl: "./tableau-node.component.scss", +}) +export class TableauNode { + @Input() + public id?: number; + + @Input() + public mod?: string; + + @Input() + public args?: string; + + @Input() + public sign?: boolean; + + @Input() + public head: string = ''; + + @Input() + public end: boolean = false; + + @Input() + public rule?: string; + + @ViewChild('idText') + idText?: ElementRef; + + @ViewChild('headText') + headText?: ElementRef; + + @ViewChild('modText') + modText?: ElementRef; + + @ViewChild('argsText') + argsText?: ElementRef; + + @ViewChild('ruleText') + ruleText?: ElementRef; + + @Output() + public onSize = new EventEmitter(); + + padding = 5; + height = 20; + + idW = 0; + modX = 0; + modW = 0; + headX = 0; + headW = 0; + argsX = 0; + argsW = 0; + totalW = 0; + + ngAfterViewChecked() { + this.idW = this.idText ? this.idText.nativeElement.getComputedTextLength() + this.padding : 0; + this.modX = this.idW; + this.modW = this.modText ? this.modText.nativeElement.getComputedTextLength() + this.padding : 0; + this.argsW = this.argsText ? this.argsText.nativeElement.getComputedTextLength() + this.padding : 0; + this.headW = this.headText ? this.headText.nativeElement.getComputedTextLength() : 0; + this.headX = this.modX + this.modW; + this.argsX = this.headX + this.headW + this.padding; + + const mainW = ( + this.headText ? + this.argsW + this.idW + this.headW + this.modW : + 0 + ); + + const ruleW = this.ruleText ? this.ruleText.nativeElement.getComputedTextLength() : 0; + this.totalW = Math.max(mainW, ruleW) + + this.onSize.emit({width: this.totalW, height: this.height}); + } + +} diff --git a/frontend/src/app/annotate/tableau-svg/tableau-svg.component.svg b/frontend/src/app/annotate/tableau-svg/tableau-svg.component.svg index 5f91428d..f262c9eb 100644 --- a/frontend/src/app/annotate/tableau-svg/tableau-svg.component.svg +++ b/frontend/src/app/annotate/tableau-svg/tableau-svg.component.svg @@ -1,7 +1,8 @@ +@let proofTableau = tree(); - diff --git a/frontend/src/app/annotate/tableau-svg/tableau-svg.component.ts b/frontend/src/app/annotate/tableau-svg/tableau-svg.component.ts index 8a84fb32..e5addf95 100644 --- a/frontend/src/app/annotate/tableau-svg/tableau-svg.component.ts +++ b/frontend/src/app/annotate/tableau-svg/tableau-svg.component.ts @@ -1,7 +1,7 @@ -import { Component, ChangeDetectorRef} from '@angular/core'; +import { Component, ChangeDetectorRef, ElementRef, input } from '@angular/core'; import { CommonModule } from "@angular/common"; import { Subject } from "rxjs"; -import { Dimensions } from '@/types'; +import { Dimensions, ProofTree } from '@/types'; import { TableauTree } from './tableau-tree.component'; @Component({ @@ -13,10 +13,15 @@ import { TableauTree } from './tableau-tree.component'; }) export class TableauSVG { + public readonly tree = input.required(); + treeDimensions$ = new Subject(); treeDimensions: Dimensions = {width:0, height: 0}; - constructor(private cdref: ChangeDetectorRef) {} + constructor( + private cdref: ChangeDetectorRef, + private element: ElementRef + ) {} onTreeSize(size: Dimensions) { this.treeDimensions = size; @@ -25,59 +30,9 @@ export class TableauSVG { ngAfterViewChecked() { this.treeDimensions$.next(this.treeDimensions); this.cdref.detectChanges(); - } - - tree: any = { - nodes: [ - {idx: 1, term: 'every@man@(be@work)', bg: 'honeydew'}, - {idx: 2, term: 'every@(who@(be@work)@person)@(λ1,a@(expensive@car)@(λ2,have@2@1))', bg: 'honeydew'}, - {idx: 3, term: 'every@man@(λ3,a@car@(λ2,own@2@3))', bg: 'mistyrose'}, - {idx: 4, term: 'be@work', label: 'c1', rule: 'up_mon_fun_some[1,3]', bg: 'honeydew'}, - {idx: 5, term: '(λ3,a@car@(λ2,own@2@3))', label: 'c1', rule: 'up_mon_fun_some[1,3]', bg: 'mistyrose'}, - {idx: 6, term: 'man', label: 'c1', rule: 'up_mon_fun_some[1,3]', bg: 'honeydew'}, - {idx: 7, term: 'a@car@(λ2,own@2@c1)', rule: 'pull_arg[5]', bg: 'mistyrose'}, - {idx: 8, term: 'work', label: 'c1', rule: 'aux_verb[4]', bg: 'honeydew'}, - {idx: 9, term: 'be@work', label: 'c1', rule: 'tr_every_c[1,6], [c1]', bg: 'honeydew'}, - {idx: 8, term: 'work', label: 'c1', rule: 'aux_verb[9]', bg: 'honeydew'}, - ], - subtrees: [ - { - nodes: [ - {idx: 10, term: 'who@(be@work)@person', label: 'c1', rule: 'tr_every[2],[c1]', bg: 'mistyrose'}, - ], - subtrees: [ - { - nodes: [ - {idx: 13, term: 'be@work', label: 'c1', rule: 'fl_conj_who[10]', bg: 'mistyrose'}, - {idx: 16, term: 'work', label: 'c1', rule: 'aux_verb[13]', bg: 'mistyrose'}, - {end: true, rule: 'cl_subcat[16,8]'} - ], - }, - { - nodes: [ - {idx: 14, term: 'person', label: 'c1', rule: 'fl_conj_who[10]', bg: 'mistyrose'}, - {end: true, rule: 'cl_subsumption[14,6]'} - ] - } - ] - }, - { - nodes: [ - {idx: 11, term: 'who@(be@work)@person', label: 'c1', rule: 'tr_every[2],[c1]', bg: 'honeydew'}, - {idx: 12, term: '(λ1,a@(expensive@car)@(λ2,have@2@1))', label: 'c1', rule: 'tr_every[2],[c1]', bg: 'honeydew'}, - {idx: 15, term: 'a@(expensive@car)@(λ2,have@2@c1)', label: 'c1', rule: 'pull_arg[12]', bg: 'honeydew'}, - {idx: 17, term: 'be@work', label: 'c1', rule: 'tr_conj_who[11]', bg: 'honeydew'}, - {idx: 18, term: 'person', label: 'c1', rule: 'tr_conj_who[11]' , bg: 'honeydew'}, - {idx: 8, term: 'work', label: 'c1', rule: 'aux_verb[17]', bg: 'honeydew'}, - {idx: 19, term: 'a@(expensive@car)', label: '(λ2,have@2@c1)', rule: 'same_args[15,7]', bg: 'honeydew'}, - {idx: 20, term: 'a@car', label: '(λ2,have@2@c1)', rule: 'same_args[15,7]', bg: 'mistyrose'}, - {idx: 21, term: 'expensive@car', label: 'c2', rule: 'up_mon_fun[19,20]', bg: 'honeydew'}, - {idx: 22, term: 'car', label: 'c2', rule: 'up_mon_fun[19,20]', bg: 'mistyrose'}, - {idx: 23, term: 'car', label: 'c2', rule:'int_mod_tr[21]', bg: 'honeydew'}, - {idx: 24, term: 'expensive', label: 'c2', rule:'int_mod_tr[21]', bg: 'honeydew'}, - {end: true, rule: 'cl_subsmption[23,22]'} - ] - } - ] + const width = this.treeDimensions.width; + if (width) this.element.nativeElement.parentElement.scroll({ + left: Math.max(0, width / 2 - 500) + }); } } diff --git a/frontend/src/app/annotate/tableau-svg/tableau-term.component.scss b/frontend/src/app/annotate/tableau-svg/tableau-term.component.scss deleted file mode 100644 index e69de29b..00000000 diff --git a/frontend/src/app/annotate/tableau-svg/tableau-term.component.svg b/frontend/src/app/annotate/tableau-svg/tableau-term.component.svg deleted file mode 100644 index 0f92a960..00000000 --- a/frontend/src/app/annotate/tableau-svg/tableau-term.component.svg +++ /dev/null @@ -1,28 +0,0 @@ - -@if(idx) { - - {{ idx }} -} - -@if(bg) { - -} - -@if(end) { - - ⛌ -} -@else { - {{ term }} -} - -@if(label) { - - {{ label }} -} - -@if(rule) { -{{ rule }} -} - - diff --git a/frontend/src/app/annotate/tableau-svg/tableau-term.component.ts b/frontend/src/app/annotate/tableau-svg/tableau-term.component.ts deleted file mode 100644 index 616a0ba2..00000000 --- a/frontend/src/app/annotate/tableau-svg/tableau-term.component.ts +++ /dev/null @@ -1,64 +0,0 @@ -import { Component, ElementRef, Input, Output, ViewChild, EventEmitter } from '@angular/core'; -import { Dimensions } from '@/types'; - -@Component({ - selector: "[term]", - standalone: true, - imports: [], - templateUrl: "./tableau-term.component.svg", - styleUrl: "./tableau-term.component.scss", -}) -export class TableauTerm { - @Input() - public idx?: number; - - @Input() - public label?: string; - - /* background color, should probably be replaced by an enum type with the color lookup done elsewhere */ - @Input() - public bg?: string; - - @Input() - public term: string = ''; - - @Input() - public end: boolean = false; - - @Input() - public rule?: string; - - @ViewChild('idxText') - idxText?: ElementRef; - - @ViewChild('termText') - termText?: ElementRef; - - @ViewChild('labelText') - labelText?: ElementRef; - - @Output() - public onSize = new EventEmitter(); - - padding = 5; - height = 20; - - idxW = 0; - termX = 0; - termW = 0; - labelX = 0; - labelW = 0; - totalW = 0; - - ngAfterViewChecked() { - this.idxW = this.idxText ? this.idxText.nativeElement.getComputedTextLength() + this.padding : 0; - this.labelW = this.labelText ? this.labelText.nativeElement.getComputedTextLength() + this.padding : 0; - this.termX = this.idxW; - this.termW = this.termText ? this.termText.nativeElement.getComputedTextLength() : 0; - this.labelX = this.termX + this.termW + this.padding; - this.totalW = this.termText ? this.labelW + this.idxW + this.termText.nativeElement.getComputedTextLength() : 0; - - this.onSize.emit({width: this.totalW, height: this.height}); - } - -} diff --git a/frontend/src/app/annotate/tableau-svg/tableau-tree.component.svg b/frontend/src/app/annotate/tableau-svg/tableau-tree.component.svg index 1aea2b34..0a60239c 100644 --- a/frontend/src/app/annotate/tableau-svg/tableau-tree.component.svg +++ b/frontend/src/app/annotate/tableau-svg/tableau-tree.component.svg @@ -1,13 +1,14 @@ @for (node of visibleNodes(); track $index; let i = $index) { - @if(!expanded[$index]) { + + (click)="nodeClick($index)">+ } @else if (!$last) { diff --git a/frontend/src/app/annotate/tableau-svg/tableau-tree.component.ts b/frontend/src/app/annotate/tableau-svg/tableau-tree.component.ts index e2e7ef7b..ba8ca18c 100644 --- a/frontend/src/app/annotate/tableau-svg/tableau-tree.component.ts +++ b/frontend/src/app/annotate/tableau-svg/tableau-tree.component.ts @@ -1,32 +1,32 @@ import { Component, Input, Output, EventEmitter } from '@angular/core'; -import { TableauTerm } from './tableau-term.component'; -import { Dimensions } from '@/types'; +import { TableauNode } from './tableau-node.component'; +import { Dimensions, ProofTree, ProofNode } from '@/types'; import { sum } from "@/util"; @Component({ selector: "[tableau-tree]", standalone: true, - imports: [TableauTerm], + imports: [TableauNode], templateUrl: "./tableau-tree.component.svg", styleUrl: "./tableau-tree.component.scss", }) export class TableauTree { expanded: boolean[] = []; - _tree: any; + _tree: ProofTree = {nodes: []}; @Input() - get tree(): any { + get tree(): ProofTree { return this._tree; } - set tree(value: any) { + set tree(value: ProofTree) { this._tree = value; this.expanded = value.nodes.map(() => true); } levelHeight = 40; - /* Width of the tree node, has to be determined dynamically via onSize events from terms */ + /* Width of the tree node, has to be determined dynamically via onSize events from nodes */ width = 0; /* Height isn't stored in a member variable, because it can be computed as needed */ @@ -61,7 +61,8 @@ export class TableauTree { /* Determines the X coordinate of where subtree of index `idx` should be drawn */ subtreePosition(idx: number) { let widthWithPadding = 1.15 * this.subWidth; - return widthWithPadding * idx - (widthWithPadding / 2) * (this.tree.subtrees.length - 1); + const subtreeCount = this.tree.subtrees!.length; + return widthWithPadding * idx - (widthWithPadding / 2) * (subtreeCount - 1); } /* Generates a path definition for linking the end of the current node to subtree index `idx` */ @@ -76,7 +77,7 @@ export class TableauTree { ].join(' '); } - nodeHeight(node: any) { + nodeHeight(node: ProofNode) { // note that in this case height includes bottom padding for the node return node.rule ? 60 : 40; } @@ -90,7 +91,7 @@ export class TableauTree { return sum(this.tree.nodes.slice(0, idx).map(this.nodeHeight)); } - termClick(idx: number) { + nodeClick(idx: number) { // the last node can't be collapsed // unless there are subtrees if (idx < this.expanded.length - 1 || this.tree.subtrees) { diff --git a/frontend/src/app/services/parse.service.spec.ts b/frontend/src/app/services/parse.service.spec.ts index de5486b0..b96aa6e4 100644 --- a/frontend/src/app/services/parse.service.spec.ts +++ b/frontend/src/app/services/parse.service.spec.ts @@ -1,8 +1,12 @@ import { TestBed } from '@angular/core/testing'; -import { ParseService } from './parse.service'; import { provideHttpClient } from '@angular/common/http'; +import { NLTKTree, ProofTree } from '@/types'; +import { ParseService, nltk2tableau } from './parse.service'; +import realNltk from '@/shared/mockNltkProof'; +import realTableau from '@/shared/mockTableauTree'; + describe('ParseService', () => { let service: ParseService; @@ -17,3 +21,115 @@ describe('ParseService', () => { expect(service).toBeTruthy(); }); }); + +describe('nltk2tableau', () => { + it('handles a trivial dead end', () => { + const nltk: NLTKTree = {node: 'Model'}; + const tableau: ProofTree = {nodes: [{end: true}]}; + expect(nltk2tableau(nltk)).toEqual(tableau); + }); + + it('handles a closing end', () => { + const nltk: NLTKTree = {node: 'Closed\ncl_subsumption([1, 2])'}; + const tableau: ProofTree = {nodes: [{ + end: true, + rule: 'cl_subsumption([1, 2])', + }]}; + expect(nltk2tableau(nltk)).toEqual(tableau); + }); + + it('handles nested nodes', () => { + const nltk: NLTKTree = { + node: '1\nterm\nTrue', + children: [{ + node: '2:some_rule([1])\nanotherterm\n[c1]\nFalse', + children: [{ + node: '3:another_rule([2])\n[c1]\nterm\nTrue', + children: [{ + node: '4:rule([1])\n[c2]\nterm\n[term]\nTrue', + children: [{ + node: 'Model', + }], + }], + }], + }], + }; + const tableau: ProofTree = { + nodes: [{ + id: 1, + head: 'term', + sign: true, + }, { + id: 2, + rule: 'some_rule([1])', + head: 'anotherterm', + args: 'c1', + sign: false, + }, { + id: 3, + rule: 'another_rule([2])', + mod: 'c1', + head: 'term', + sign: true, + }, { + id: 4, + rule: 'rule([1])', + mod: 'c2', + head: 'term', + args: 'term', + sign: true, + }, { + end: true, + }], + }; + expect(nltk2tableau(nltk)).toEqual(tableau); + }); + + it('can handle branching', () => { + const nltk: NLTKTree = { + node: '1:rule([1, 2])\nterm\n[arg]\nFalse', + children: [{ + node: 'Model', + }, { + node: 'Closed\nclosing_rule([1])', + }], + }; + const tableau: ProofTree = { + nodes: [{ + id: 1, + rule: 'rule([1, 2])', + head: 'term', + args: 'arg', + sign: false, + }], + subtrees: [{ + nodes: [{end: true}], + }, { + nodes: [{end: true, rule: 'closing_rule([1])'}], + }], + }; + expect(nltk2tableau(nltk)).toEqual(tableau); + }); + + it('does not cause a stack overflow', () => { + let nltk: NLTKTree = {node: 'Model'}; + const tableau: ProofTree = {nodes: []}; + for (let i = 0; i < 100000; ++i) { + nltk = { + node: '1\nterm\nFalse', + children: [nltk], + }; + tableau.nodes.push({ + id: 1, + head: 'term', + sign: false, + }); + } + tableau.nodes.push({end: true}); + expect(nltk2tableau(nltk)).toEqual(tableau); + }); + + it('can process real-world data', () => { + expect(nltk2tableau(realNltk)).toEqual(realTableau); + }); +}); diff --git a/frontend/src/app/services/parse.service.ts b/frontend/src/app/services/parse.service.ts index bbf3a5da..6d250f31 100644 --- a/frontend/src/app/services/parse.service.ts +++ b/frontend/src/app/services/parse.service.ts @@ -1,16 +1,16 @@ import { HttpClient } from '@angular/common/http'; import { inject, Injectable } from '@angular/core'; -import { Subject, switchMap, catchError, of, merge, map } from 'rxjs'; +import { Subject, switchMap, catchError, of, merge, map, share } from 'rxjs'; import { ParseInput } from '@/annotate/annotation-input/annotation-input.component'; import { ProblemService } from './problem.service'; -import { ParseResponseData } from '@/types'; +import { + ParseResponse, + NLTKTree, + ProofNode, + ProofTree, +} from '@/types'; -export type ParseResponse = { - data: ParseResponseData; - error: string | null; -}; - @Injectable({ providedIn: 'root' }) @@ -18,11 +18,13 @@ export class ParseService { private http = inject(HttpClient); private problemService = inject(ProblemService); + // Sink for triggering parse-and-prove requests to the backend. public submit$ = new Subject(); // Clear parse results when a new problem is loaded. private clearOnNewProblem$ = this.problemService.problemResponse$.pipe(map(() => null)); + // Raw responses from the backend. private parseResults$ = this.submit$.pipe( switchMap((form) => this.http.post("/api/problem/parse", form).pipe( @@ -31,11 +33,153 @@ export class ParseService { return of({ data: null, error: error.message || "An error occurred while parsing the problem." }); }), ) - ) + ), + share() ); public parse$ = merge( this.parseResults$, this.clearOnNewProblem$ ); + + // Proofs from the response in a format that is easier to handle than the + // stringly NLTK.Tree serialization. + public proofs$ = this.parse$.pipe(map(extractProofs)); +} + +/** + * Given a `{data: {ccg_trees, proofs}}` response from the backend, tease out + * the `proofs` and apply the `nltk2tableau` transformation to each proof + * within. + */ +function extractProofs( + response: ParseResponse | {data: null, error: any} | null +) { + if (!response || !response.data) return null; + // This is basically just `_.mapObject(response.data.proofs, nltk2tableau)`, + // but we don't depend on Underscore yet. + const {entailment, contradiction} = response.data.proofs; + return { + entailment: nltk2tableau(entailment), + contradiction: nltk2tableau(contradiction), + }; +} + +// Regular expressions matching the stringified nltk.Tree node payloads. +const openLeafPattern = /^Model$/; +const closedLeafPattern = /^Closed\n(?.+)$/; +const internalNodePattern = /^(?\d+):?(?.+)?(\n\[(?.+)\])?\n(?.+)(\n\[(?.+)\])?\n(?True|False)$/; + +// Helpers for the functions below. +const emptyTableau = (): ProofTree => ({nodes: []}); +const pairNodes = (other: any[]) => + (node: any, index: number) => [node, other[index]]; +const quotes = /'/g; +const unquote = (text: string) => text.replace(quotes, ''); + +type ProofConversionThunk = [NLTKTree, ProofTree]; + +/** + * Given a single proof in serialized NLTK.Tree format, return the same proof in + * a more convenient format where each node has explicitly labeled `id`, `rule`, + * `mod`, `head`, `args` and `sign`. + * + * This function can handle proof trees of arbitrary depth without causing a + * stack overflow. + */ +export function nltk2tableau(nltk: NLTKTree): ProofTree { + const tree = emptyTableau(); + // We will be using trampolining instead of recursion. A general but + // admittedly not very helpful description can be found in the first bullet + // of + // https://en.wikipedia.org/wiki/Trampoline_(computing)#High-level_programming. + // The gist is this: instead of recursing, functions return pieces of work + // ("thunks") that should be executed next. The trampoline, which in this + // case is the current function, takes care of executing the thunks. + + // The list of thunks to execute. One will be added for each tree node, one + // will be taken off on each iteration. Since we are always calling + // `nltkNode2tableauNode`, we leave this implicit in the thunk + // representation. It consists only of the arguments that we are passing to + // the function. + const todo: ProofConversionThunk[] = [[nltk, tree]]; + // The core of the trampoline. Process one thunk at a time. We know we are + // done when the list is empty. + while (todo.length) { + // The algorithm is written such that the order in which we process + // child nodes does not matter, so we can simply pop thunks off the back + // of the todo list. tsc is apparently unable to infer that `todo` is + // guaranteed to be nonempty on the next line; hence + // the type assertion. + const task = todo.pop() as ProofConversionThunk; + // Processing a thunk might produce zero or more new thunks, depending + // on the number of children of the processed node. + const newTasks = nltkNode2tableauNode(...task); + todo.push(...newTasks); + } + return tree; +} + +/** + * Internal function that maps a single serialized NLTK.Tree node to an + * explicitly structured node inside `tree`. This function relies on an external + * trampoline (in `nltk2tableau`) and returns thunks instead of recursing into + * child nodes. + */ +function nltkNode2tableauNode(nltk: NLTKTree, tree: ProofTree): +ProofConversionThunk[] { + // `nltk` is in a strictly nested format: each node contains its children. + // Our own format does not follow this rule: chains of nodes with single + // children are stored as adjacent elements in an array. `tree` is the + // object that contains this array (`tree.nodes`). When there is a + // bifurcation, the subtrees are stored inside `tree` rather than in the + // bifurcating node. + const node = parseNltkNode(nltk.node); + tree.nodes.push(node); + // With the node itself having been decoded, now comes the part where a + // "normal" function would recurse and where we return follow-up thunks + // instead. + if (!nltk.children || !nltk.children.length) { + node.end = true; + // Leaf node. No recursion, no thunks. + return []; + } + if (nltk.children.length === 1) { + // Node with one child, the most common case. The child will be appended + // to `tree.nodes` after the current node. + return [[nltk.children[0], tree]]; + } + // Multiple children. Most likely two, but the code would transparently + // support larger numbers of children. We create empty subtrees so we can + // pass those in the thunks as containers for the child nodes. The fact that + // the subtrees have already been created, is what makes it possible to + // process the children in arbitrary order. + tree.subtrees = nltk.children.map(emptyTableau); + // We essentially do a `_.zip(nltk.children, tree.subtrees)` in order to + // create the thunks. I could have fumbled with `Iterator.zip` instead, but + // that feels like more hassle and the polyfill would be huge. + return nltk.children.map(pairNodes(tree.subtrees)) as ProofConversionThunk[]; +} + +/** + * Decode the payload of a serialized nltk.Tree node, where all information is + * combined in a single string, back to an object with explicitly labeled parts. + */ +function parseNltkNode(text: string): ProofNode { + if (openLeafPattern.test(text)) return {}; + let match; + if (match = text.match(closedLeafPattern)) { + return match.groups as unknown as ProofNode; + } + match = text.match(internalNodePattern); + if (!match || !match.groups) return {head: text}; + const result: any = { + id: +match.groups['id'], + head: match.groups['head'], + sign: match.groups['sign'] === 'True', + }; + if (match.groups['rule']) result.rule = unquote(match.groups['rule']); + if (match.groups['mod']) result.mod = match.groups['mod']; + if (match.groups['args']) result.args = match.groups['args']; + return result; } diff --git a/frontend/src/app/shared/mockNltkProof.ts b/frontend/src/app/shared/mockNltkProof.ts new file mode 100644 index 00000000..ecd66424 --- /dev/null +++ b/frontend/src/app/shared/mockNltkProof.ts @@ -0,0 +1,133 @@ +import { NLTKTree } from '@/types'; + +const tree: NLTKTree = { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "node": "Closed\ncl_subsumption([15, 8])" + } + ], + "node": "15:empty_mod([12])\nwork\n[c1]\nFalse" + } + ], + "node": "12:fl_conj_who([9])\nbe work\n[c1]\nFalse" + }, + { + "children": [ + { + "node": "Closed\ncl_subsumption([13, 6])" + } + ], + "node": "13:fl_conj_who([9])\nperson\n[c1]\nFalse" + } + ], + "node": "9:tr_every([2],['c1'])\n(who (be work)) person\n[c1]\nFalse" + }, + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "children": [ + { + "node": "Closed\ncl_subsumption([22, 21])" + } + ], + "node": "23:int_mod_tr([20])\nexpensive\n[c2]\nTrue" + } + ], + "node": "22:int_mod_tr([20])\ncar\n[c2]\nTrue" + } + ], + "node": "21:up_mon_fun(['c2'],[18,19])\ncar\n[c2]\nFalse" + } + ], + "node": "20:up_mon_fun(['c2'],[18,19])\nexpensive car\n[c2]\nTrue" + } + ], + "node": "19:same_args_tf([14,7])\na car\n[λE.((have E) c1)]\nFalse" + } + ], + "node": "18:same_args_tf([14,7])\na (expensive car)\n[λE.((have E) c1)]\nTrue" + } + ], + "node": "8:empty_mod([16])\nwork\n[c1]\nTrue" + } + ], + "node": "17:tr_conj_who([10])\nperson\n[c1]\nTrue" + } + ], + "node": "16:tr_conj_who([10])\nbe work\n[c1]\nTrue" + } + ], + "node": "14:pull_arg([11])\n(a (expensive car))(λE.((have E) c1))\nTrue" + } + ], + "node": "11:tr_every([2],['c1'])\nλF.((a (expensive car))(λE.((have E) F)))\n[c1]\nTrue" + } + ], + "node": "10:tr_every([2],['c1'])\n(who (be work)) person\n[c1]\nTrue" + } + ], + "node": "8:empty_mod([4])\nwork\n[c1]\nTrue" + } + ], + "node": "7:pull_arg([5])\n(a car)(λE.((own E) c1))\nFalse" + } + ], + "node": "6:up_mon_fun_some(['c1'],[1,3])\nman\n[c1]\nTrue" + } + ], + "node": "5:up_mon_fun_some(['c1'],[1,3])\nλM.((a car)(λE.((own E) M)))\n[c1]\nFalse" + } + ], + "node": "4:up_mon_fun_some(['c1'],[1,3])\nbe work\n[c1]\nTrue" + } + ], + "node": "3:\n(every man)(λM.((a car)(λE.((own E) M))))\nFalse" + } + ], + "node": "2:\n(every ((who (be work)) person))(λF.((a (expensive car))(λE.((have E) F))))\nTrue" + } + ], + "node": "1:\n(every man)(be work)\nTrue" +}; + +export default tree; diff --git a/frontend/src/app/shared/mockTableauTree.ts b/frontend/src/app/shared/mockTableauTree.ts new file mode 100644 index 00000000..aac896c3 --- /dev/null +++ b/frontend/src/app/shared/mockTableauTree.ts @@ -0,0 +1,55 @@ +import { ProofTree } from '@/types'; + +const tree: ProofTree = { + nodes: [ + {id: 1, head: '(every man)(be work)', sign: true}, + {id: 2, head: '(every ((who (be work)) person))(λF.((a (expensive car))(λE.((have E) F))))', sign: true}, + {id: 3, head: '(every man)(λM.((a car)(λE.((own E) M))))', sign: false}, + {id: 4, head: 'be work', args: 'c1', rule: 'up_mon_fun_some([c1],[1,3])', sign: true}, + {id: 5, head: 'λM.((a car)(λE.((own E) M)))', args: 'c1', rule: 'up_mon_fun_some([c1],[1,3])', sign: false}, + {id: 6, head: 'man', args: 'c1', rule: 'up_mon_fun_some([c1],[1,3])', sign: true}, + {id: 7, head: '(a car)(λE.((own E) c1))', rule: 'pull_arg([5])', sign: false}, + {id: 8, head: 'work', args: 'c1', rule: 'empty_mod([4])', sign: true}, + ], + subtrees: [ + { + nodes: [ + {id: 9, head: '(who (be work)) person', args: 'c1', rule: 'tr_every([2],[c1])', sign: false}, + ], + subtrees: [ + { + nodes: [ + {id: 12, head: 'be work', args: 'c1', rule: 'fl_conj_who([9])', sign: false}, + {id: 15, head: 'work', args: 'c1', rule: 'empty_mod([12])', sign: false}, + {end: true, rule: 'cl_subsumption([15, 8])'} + ], + }, + { + nodes: [ + {id: 13, head: 'person', args: 'c1', rule: 'fl_conj_who([9])', sign: false}, + {end: true, rule: 'cl_subsumption([13, 6])'} + ] + } + ] + }, + { + nodes: [ + {id: 10, head: '(who (be work)) person', args: 'c1', rule: 'tr_every([2],[c1])', sign: true}, + {id: 11, head: 'λF.((a (expensive car))(λE.((have E) F)))', args: 'c1', rule: 'tr_every([2],[c1])', sign: true}, + {id: 14, head: '(a (expensive car))(λE.((have E) c1))', rule: 'pull_arg([11])', sign: true}, + {id: 16, head: 'be work', args: 'c1', rule: 'tr_conj_who([10])', sign: true}, + {id: 17, head: 'person', args: 'c1', rule: 'tr_conj_who([10])' , sign: true}, + {id: 8, head: 'work', args: 'c1', rule: 'empty_mod([16])', sign: true}, + {id: 18, head: 'a (expensive car)', args: 'λE.((have E) c1)', rule: 'same_args_tf([14,7])', sign: true}, + {id: 19, head: 'a car', args: 'λE.((have E) c1)', rule: 'same_args_tf([14,7])', sign: false}, + {id: 20, head: 'expensive car', args: 'c2', rule: 'up_mon_fun([c2],[18,19])', sign: true}, + {id: 21, head: 'car', args: 'c2', rule: 'up_mon_fun([c2],[18,19])', sign: false}, + {id: 22, head: 'car', args: 'c2', rule: 'int_mod_tr([20])', sign: true}, + {id: 23, head: 'expensive', args: 'c2', rule: 'int_mod_tr([20])', sign: true}, + {end: true, rule: 'cl_subsumption([22, 21])'} + ] + } + ] +}; + +export default tree; diff --git a/frontend/src/app/types.ts b/frontend/src/app/types.ts index 9ffd6c00..f097e28d 100644 --- a/frontend/src/app/types.ts +++ b/frontend/src/app/types.ts @@ -133,7 +133,7 @@ export interface Dimensions { } // -// Syntactic parse tree types +// Syntactic parse and proof tree types from the backend // export type LeafNode = { @@ -160,8 +160,39 @@ export interface CCGParse { ccg_trees: Record; }; +export interface NLTKTree { + node: string; + children?: NLTKTree[]; +} + export type ParseResponseData = { ccg_parses: CCGParse[]; - proofs: unknown[]; + proofs: { + entailment: NLTKTree, + contradiction: NLTKTree, + }; +}; + +export type ParseResponse = { + data: ParseResponseData; + error: string | null; }; +// +// Our internal representation of proof trees +// + +export type ProofNode = { + id?: number; + rule?: string; + mod?: string; + head?: string; + args?: string; + sign?: boolean; + end?: true; +}; + +export interface ProofTree { + nodes: ProofNode[]; + subtrees?: ProofTree[]; +}