Visualize the actual proofs of the current problem with the TableauSVG component

frontend/src/app/annotate/annotation-menu/annotation-menu.component.html

@@ -1,35 +1,54 @@
-<ul ngbNav #nav="ngbNav" [(activeId)]="active" class="nav-tabs flex-nowrap">
-    <li [ngbNavItem]="1">
-        <button ngbNavLink>
-            <fa-icon
-                [icon]="faSquarePollHorizontal"
-                class="me-2"
-                aria-hidden="true"
-            />
-            <span i18n>Syntactic parses</span>
-        </button>
-        <ng-template ngbNavContent>
-            <la-annotation-parse-results />
-        </ng-template>
-    </li>
-    <li [ngbNavItem]="2">
-        <button ngbNavLink>
-            <fa-icon [icon]="faTree" class="me-2" aria-hidden="true" />
-            <span i18n>Tableau / Proof</span>
-        </button>
-        <ng-template ngbNavContent>
-            <la-annotation-tableau />
-        </ng-template>
-    </li>
-    <li [ngbNavItem]="3">
-        <button ngbNavLink>
-            <fa-icon [icon]="faPenNib" class="me-2" aria-hidden="true" />
-            <span i18n>Comments / History</span>
-        </button>
-        <ng-template ngbNavContent>
-            <la-annotation-comments />
-        </ng-template>
-    </li>
-</ul>
-
-<div [ngbNavOutlet]="nav" class="mt-2"></div>
+@let proofs = proofs$ | async;
+
+<ul ngbNav #nav="ngbNav" [(activeId)]="active" class="nav-tabs flex-nowrap">
+    <li [ngbNavItem]="1">
+        <button ngbNavLink>
+            <fa-icon
+                [icon]="faSquarePollHorizontal"
+                class="me-2"
+                aria-hidden="true"
+            />
+            <span i18n>Syntactic parses</span>
+        </button>
+        <ng-template ngbNavContent>
+            <la-annotation-parse-results />
+        </ng-template>
+    </li>
+    <li [ngbNavItem]="2">
+        <button ngbNavLink>
+            <b class="me-2" aria-hidden>⊤</b>
+            <span i18n>Proof / Entailment</span>
+        </button>
+        <ng-template ngbNavContent>
+            <section class="overflow-x-scroll">
+                @if (proofs) {
+                <la-tableau-svg [tree]="proofs.entailment"></la-tableau-svg>
+                }
+            </section>
+        </ng-template>
+    </li>
+    <li [ngbNavItem]="3">
+        <button ngbNavLink>
+            <b class="me-2" aria-hidden>⊥</b>
+            <span i18n>Proof / Contradiction</span>
+        </button>
+        <ng-template ngbNavContent>
+            <section class="overflow-x-scroll">
+                @if (proofs) {
+                <la-tableau-svg [tree]="proofs.contradiction"></la-tableau-svg>
+                }
+            </section>
+        </ng-template>
+    </li>
+    <li [ngbNavItem]="4">
+        <button ngbNavLink>
+            <fa-icon [icon]="faPenNib" class="me-2" aria-hidden="true" />
+            <span i18n>Comments / History</span>
+        </button>
+        <ng-template ngbNavContent>
+            <la-annotation-comments />
+        </ng-template>
+    </li>
+</ul>
+
+<div [ngbNavOutlet]="nav" class="mt-2"></div>

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;
 }

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<SVGTextElement>;
+
+    @ViewChild('headText')
+    headText?: ElementRef<SVGTextElement>;
+
+    @ViewChild('modText')
+    modText?: ElementRef<SVGTextElement>;
+
+    @ViewChild('argsText')
+    argsText?: ElementRef<SVGTextElement>;
+
+    @ViewChild('ruleText')
+    ruleText?: ElementRef<SVGTextElement>;
+
+    @Output()
+    public onSize = new EventEmitter<Dimensions>();
+
+    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});
+    }
+
+}

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<ProofTree>();
+
     treeDimensions$ = new Subject<Dimensions>();
     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)
+        });
     }
 }