Apply proof types in frontend logic (#79)

Author: jgonggrijp

frontend/src/app/annotate/tableau-svg/tableau-svg.component.ts

@@ -1,7 +1,7 @@
 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({
@@ -34,5 +34,5 @@ export class TableauSVG {
         });
     }
 
-    public readonly tree = input.required<any>();
+    public readonly tree = input.required<ProofTree>();
 }

frontend/src/app/annotate/tableau-svg/tableau-tree.component.ts

@@ -1,6 +1,6 @@
 import { Component, Input, Output, EventEmitter } from '@angular/core';
 import { TableauNode } from './tableau-node.component';
-import { Dimensions } from '@/types';
+import { Dimensions, ProofTree, ProofNode } from '@/types';
 import { sum } from "@/util";
 
 @Component({
@@ -13,13 +13,13 @@ import { sum } from "@/util";
 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);
     }
@@ -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,9 +77,9 @@ 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;
+        return 'rule' in node && node.rule ? 60 : 40;
     }
 
     totalNodeHeight() {

frontend/src/app/services/parse.service.spec.ts

@@ -2,6 +2,7 @@ import { TestBed } from '@angular/core/testing';
 
 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';
@@ -23,22 +24,22 @@ describe('ParseService', () => {
 
 describe('nltk2tableau', () => {
     it('handles a trivial dead end', () => {
-        const nltk = {node: 'Model'};
-        const tableau = {nodes: [{end: true}]};
+        const nltk: NLTKTree = {node: 'Model'};
+        const tableau: ProofTree = {nodes: [{end: true}]};
         expect(nltk2tableau(nltk)).toEqual(tableau);
     });
 
     it('handles a closing end', () => {
-        const nltk = {node: 'Closed\ncl_subsumption([1, 2])'};
-        const tableau = {nodes: [{
+        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 = {
+        const nltk: NLTKTree = {
             node: '1\nterm\nTrue',
             children: [{
                 node: '2:some_rule([1])\nanotherterm\n[c1]\nFalse',
@@ -53,7 +54,7 @@ describe('nltk2tableau', () => {
                 }],
             }],
         };
-        const tableau = {
+        const tableau: ProofTree = {
             nodes: [{
                 id: 1,
                 head: 'term',
@@ -85,15 +86,15 @@ describe('nltk2tableau', () => {
     });
 
     it('can handle branching', () => {
-        const nltk = {
+        const nltk: NLTKTree = {
             node: '1:rule([1, 2])\nterm\n[arg]\nFalse',
             children: [{
                 node: 'Model',
             }, {
                 node: 'Closed\nclosing_rule([1])',
             }],
         };
-        const tableau = {
+        const tableau: ProofTree = {
             nodes: [{
                 id: 1,
                 rule: 'rule([1, 2])',
@@ -111,8 +112,8 @@ describe('nltk2tableau', () => {
     });
 
     it('does not cause a stack overflow', () => {
-        let nltk: any = {node: 'Model'};
-        const tableau: any = {nodes: []};
+        let nltk: NLTKTree = {node: 'Model'};
+        const tableau: ProofTree = {nodes: []};
         for (let i = 0; i < 100000; ++i) {
             nltk = {
                 node: '1\nterm\nFalse',

frontend/src/app/services/parse.service.ts

@@ -3,7 +3,12 @@ import { inject, Injectable } from '@angular/core';
 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 { ParseResponse } from '@/types';
+import {
+    ParseResponse,
+    NLTKTree,
+    ProofNode, InternalProofNode, TerminalProofNode,
+    ProofTree,
+} from '@/types';
 
 
 @Injectable({
@@ -66,12 +71,14 @@ const closedLeafPattern = /^Closed\n(?<rule>.+)$/;
 const internalNodePattern = /^(?<id>\d+):?(?<rule>.+)?(\n\[(?<mod>.+)\])?\n(?<head>.+)(\n\[(?<args>.+)\])?\n(?<sign>True|False)$/;
 
 // Helpers for the functions below.
-const emptyTableau = (): any => ({nodes: []});
+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`,
@@ -80,7 +87,7 @@ const unquote = (text: string) => text.replace(quotes, '');
  * This function can handle proof trees of arbitrary depth without causing a
  * stack overflow.
  */
-export function nltk2tableau(nltk: any) {
+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
@@ -95,7 +102,7 @@ export function nltk2tableau(nltk: any) {
     // `nltkNode2tableauNode`, we leave this implicit in the thunk
     // representation. It consists only of the arguments that we are passing to
     // the function.
-    const todo = [[nltk, tree]];
+    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) {
@@ -105,7 +112,7 @@ export function nltk2tableau(nltk: any) {
         // guaranteed to be nonempty on the next line, hence the silencing
         // comment.
         // @ts-ignore
-        const task: [any, any] = todo.pop();
+        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);
@@ -120,20 +127,21 @@ export function nltk2tableau(nltk: any) {
  * trampoline (in `nltk2tableau`) and returns thunks instead of recursing into
  * child nodes.
  */
-function nltkNode2tableauNode(nltk: any, tree: any) {
+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: any = parseNltkNode(nltk.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;
+        (node as TerminalProofNode).end = true;
         // Leaf node. No recursion, no thunks.
         return [];
     }
@@ -151,17 +159,19 @@ function nltkNode2tableauNode(nltk: any, tree: any) {
     // 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));
+    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) {
+function parseNltkNode(text: string): ProofNode {
     if (openLeafPattern.test(text)) return {};
     let match;
-    if (match = text.match(closedLeafPattern)) return match.groups;
+    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 = {

frontend/src/app/shared/mockNltkProof.ts

@@ -1,4 +1,6 @@
-export default {
+import { NLTKTree } from '@/types';
+
+const tree: NLTKTree = {
     "children": [
         {
             "children": [
@@ -127,3 +129,5 @@ export default {
     ],
     "node": "1:\n(every man)(be work)\nTrue"
 };
+
+export default tree;

frontend/src/app/shared/mockTableauTree.ts

@@ -1,4 +1,6 @@
-export default {
+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},
@@ -49,3 +51,5 @@ export default {
         }
     ]
 };
+
+export default tree;