Visualize the actual proofs of the current problem with the TableauSVG component by jgonggrijp · Pull Request #79 · CentreForDigitalHumanities/langpro-annotator

jgonggrijp · 2026-03-17T03:10:44Z

Together with #78 and #77, I think this finally completes the work that started with #51.

The pre-existing "Tableau / Proof" tab is split into a "Proof / Entailment" and a "Proof / Contradiction" tab, which visualize the respective proofs for the current problem. Please read the commit messages for a quick summary of my approach.

The tests pass and it generally seems to work well. That being said, at the time of writing, there are still a few known problems with the code on this branch. More on this below.

For now, I suggest trying the branch as follows.

Enter and save two or more small problems. If you don't already have a few, I suggest the following.

The default example from the old demo

Every man is working
Everybody who is working has an expensive car
---
Every man owns a car

A similar example that I just came up with

Every child likes to play
Everyone who likes to play is creative
---
Every child is creative

Navigate to one of these problems and make sure the "CCG / LLF" tab is selected.
Press the "parse and prove" button. Wait for the contents of the "CCG / LLF" tab to disappear.
Open the "Proof / Entailment" tab and observe a proof tableau.
Open the "Proof / Contradiction" tab and observe a different proof tableau.
Repeat from 2 with another small problem and observe two yet different proof tableaux.

It works for large problems, too, but in most cases, the overflow on the tab content element is preventing the proof from being visible. For example, if you try the first SICK problem, the Entailment tab will look empty, but if you inspect the DOM, you will find that the tableau is actually there. There is still a visible visualization in the Contradiction tab, but it is truncated on the right. I have held off from fixing this because I already took a quick peek at #78 and noticed that @XanderVertegaal fixed an overflow problem on that brach, which is probably the same issue.

Other known issues that I think are also best solved in coordination with #78:

As mentioned above, the "CCG / LLF" tab must be selected when the "Parse and prove" button is pressed, in order for the tableaux to be rendered. This is because AnnotationMenuComponent, which passes the proof trees to TableauSVG, is not (yet) subscribed to the AnnotationService#proofs$ observable. The AnnotationsParseResultsComponent is subscribed to the underlying #parse$ observable, however, and is therefore used (for now) to trigger the request to the backend. We could subscribe in two places, but it's probably more elegant (and perhaps also more efficient?) to coordinate a single place where this is done.
The types are just any all over the place. Without having seen the code, I suspect @XanderVertegaal already (partially) addressed this in Feature/langpro parse results #78.

Other other known issues:

The nltk2tableau conversion function deserves some solid documentation. I still want to add this before merging.
The TableauNodeComponent does not take the rule into account when calculating the width of leaf nodes (or of non-leaf nodes with very slim terms, for that matter). Also something I still want to fix before merging.

Without the still to be added comments, I expect the conversion logic to be difficult to follow if not outright mysterious. That being said, you are welcome to review it anyway and let me know what you find most opaque/offensive. 😉

XanderVertegaal · 2026-03-17T09:04:20Z

The types are just any all over the place. Without having seen the code, I suspect @XanderVertegaal already (partially) addressed this in #78.

I hate to disappoint, but I merely replaced any with unknown when it comes to the proofs. 😂

export type ParseResponseData = {
    ccg_parses: CCGParse[];
    proofs: unknown[];
};

If you need "any" help (see what I did there?) getting rid of the anys, let me know. I actually enjoy type wrangling.

XanderVertegaal

Good work so far! I'm glad you added the comment about the proof being there (but hidden out of screen) for some of the longer problems. I was very confused. 😅 My solution for wide output was simply to add overflow: scroll to a couple of containers, so there is space to scroll horizontally. Still, I wonder if this is the neatest and most 'overzichtelijke' solution. Perhaps adding an external library with a zoom and drag interface would be a good addition at some point for both the tableaus and the (often very wide) syntactic parse result tables.

One note: I could not get this branch to work without commenting out this.parseResults = response.data.ccg_trees; in the AnnotationParseResults component. (This should be fixed once both of our branches are merged.)

As indicated in one of the comments. Let me know if you would like to delegate the type wrangling to me. I will continue my review after you have had time to add documentation to the tree2Tableau magic! 🧙‍♂️

XanderVertegaal · 2026-03-17T08:32:24Z

        <button ngbNavLink>
            <fa-icon [icon]="faTree" class="me-2" aria-hidden="true" />
-            <span i18n>Tableau / Proof</span>
+            <span i18n>Proof / Entailment</span>


Much better! 'Tableau' is a representation but does not give information as to the actual content. (I don't call the syntactic parses "Table" either :P)

XanderVertegaal · 2026-03-17T08:33:30Z

        <ng-template ngbNavContent>
-            <la-annotation-tableau />
+            <section>
+                @if (proofs) {


Perhaps for later, but maybe you could add an @else block with something like "No entailment data available yet."

Maybe we should factor that out from the AnnotationParseResults component in #78 and reuse it across tabs to make them look consistent.

XanderVertegaal · 2026-03-17T08:48:55Z

    </li>
    <li [ngbNavItem]="3">
+        <button ngbNavLink>
+            <fa-icon [icon]="faTree" class="me-2" aria-hidden="true" />


I tried looking for another icon we could use to differentiate the entailment tree from the contradiction tree, but no obvious candidates present themselves. Maybe link and linkSlash for entailment and contradiction, respectively?

(This is obviously not a high-priority item. 😅)

There are symbols in Unicode that exactly convey the intended meaning: ⊤ and ⊥. I went with those.

XanderVertegaal · 2026-03-17T08:56:29Z

+    it('does not cause a stack overflow', () => {
+        let nltk: any = {node: 'Model'};
+        const tableau: any = {nodes: []};
+        for (let i = 0; i < 100000; ++i) {


TIL about post-increments and pre-increments! Neat!

XanderVertegaal · 2026-03-17T09:10:14Z

    selector: "[tableau-tree]",
    standalone: true,
-    imports: [TableauTerm],
+    imports: [TableauNode],


My IDE says that this import is unused. Is that true?

The template of the tree component inserts instances of the node component. Maybe your IDE is failing to recognize that because the template is SVG instead of HTML?

XanderVertegaal · 2026-03-17T09:21:26Z

+    };
+}
+
+const emptyTableau = (): any => ({nodes: []});


Out of curiosity: any reason why you opt for an arrow function instead of a traditional one here? Brevity?

Yes, if a function is just a single expression that fits on one line, I like to write it as an arrow.

XanderVertegaal · 2026-03-17T09:25:13Z

+    public proofs$ = this.parse$.pipe(map(extractProofs));
+}
+
+function extractProofs(response: ParseResponse) {


Just a word of caution: catchError on line 21 returns null, so destructuring on line 32 will fail if that is the case. (This will undoubtedly be caught once we add proper typing.)

Thanks for pointing that out to me! I just assumed that it would somehow magically prevent errors from being problematic in any way.

XanderVertegaal · 2026-03-17T09:25:51Z

+    return tree;
+}
+
+function nltkNode2tableauNode(nltk: any, tree: any) {


I await the documentation for this with bated breath! It feels very magical but at the same time there is not a lot of code, which is good.

@XanderVertegaal

Per review comment by @XanderVertegaal in #79.

jgonggrijp · 2026-03-17T23:37:49Z

@XanderVertegaal I responded to most of your comments so far and added comments for the nltk2tableau jugglefest. Please feel welcome to review that part of the code while I finalize the remaining work.

Here is my full plan. Please let me know if you think I'm missing something or if you'd prefer me to proceed differently.

Handle null response in extractProofs.
Use open/closed lock symbols for leaf nodes.
Make the tableau scroll on overflow.
Horizontally center proof tab on root node.
Take rule into account when calculating node widths. I intend to get at least this far tomorrow.
Wait for you to merge Feature/langpro parse results #78 (it's OK if you do this later than tomorrow).
Rebase on develop.
Add "real" types for the proof representations to the types that you wrote for Feature/langpro parse results #78.
Invite you for another review.
Address the "no trigger unless viewing parse tab" problem, if that still persists after the rebase.
Merge.

@XanderVertegaal

Per review comment by @XanderVertegaal in #79.

…dth (#79)

XanderVertegaal · 2026-03-19T08:33:06Z

Your plan corresponds well to what we agreed, so please go ahead with the implementation. The only item on the list I would like you to clarify is 10: what do you mean with the 'no trigger unless viewing parse tab'?

XanderVertegaal

Very neat, thank you for the documentation! Have a look at the alignment of the circles+symbols at the end of the trees. Otherwise, please carry on!

XanderVertegaal · 2026-03-19T09:13:36Z

 @if(end) {
-    <svg:circle [attr.cx]="headX + 5" [attr.cy]="12" r="10" fill="salmon"/>
-    <svg:text #headText [attr.x]="headX" y="12" dominant-baseline="middle" font-weight="bold" fill="white">⛌</svg:text>
+    <svg:circle [attr.cx]="headX + 8" [attr.cy]="11" r="10" fill="salmon"/>


I like the new symbols, but they are sadly still not aligned on my screen:

Increasing the value of [attr.cx] seems to help, with totalW/2 getting it close to perfect.

Argh! Which browser is this?

By the way, I investigated using faLock and faLockOpen instead, but the icons would display with zero width and become invisible. I wasn't able to make it work and I suspect it is because the SVG icon is nested in an HTML element which is then again nested inside the larger SVG tableau.

Argh! Which browser is this?

Never mind, it happens in my browser, too. Apparently I had to rebuild the container to see it.

I see. For what it is worth: I am using Firefox.

XanderVertegaal · 2026-03-19T09:14:17Z

        this.cdref.detectChanges();
+        const width = this.treeDimensions.width;
+        if (width) this.element.nativeElement.parentElement.scroll({
+            left: Math.max(0, width / 2 - 500)


Is 500 here chosen as an arbitrary (but sensible) minimal width?

It's deliberately slightly more than half of the constrained body width. Without it, the center of the root would be on the left edge. I went with a slight bias towards the right because the description of the node starts on the left.

You seem to have been right that the root is always at the middle of the top edge, by the way.

XanderVertegaal · 2026-03-19T09:38:39Z

+        // of the todo list. tsc is apparently unable to infer that `todo` is
+        // guaranteed to be nonempty on the next line, hence the silencing
+        // comment.
+        // @ts-ignore


I understand why the @ts-ignore is here, but instead of silencing it completely, maybe a type assertion todo.pop() as [any, any] or a non-null assertion todo.pop()! would be neater.

This is not something I insist on, but rather something you might want to keep in mind when you add the types.

XanderVertegaal · 2026-03-19T09:39:09Z

+        // guaranteed to be nonempty on the next line, hence the silencing
+        // comment.
+        // @ts-ignore
+        let task: [any, any] = todo.pop();


Why are these lets rather than consts?

Because I'm still used to var semantics and mentally hoisting them to the top of the function scope. 😅 (To be honest, I don't believe that let and const were an improvement to the language and I'm only using them in order to respect the local code convention.) I'll change it to const.

XanderVertegaal · 2026-03-19T09:39:33Z

GHSA-qpx9-hpmf-5gmw

+    // 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


Interesting. Would you say trampolining is generally superior to recursion when building nested datastructures like this? Are there any trade-offs, or areas in which recursion is preferable?

When the datastructure might be arbitrarily deeply nested, you kind of "have" to use trampolining in order to avoid stack overflows. I became aware of this because of GHSA-qpx9-hpmf-5gmw and now cannot un-see that potential problem anymore, hence my vigilance. I'm actually planning to add a generalized _.trampoline to Underscore in order to provide a foundation for solutions like this one.

Suprisingly, there is no significant cost to trampolining versus recursion performancewise. The number of function calls is the same and the memory consumption is similar.

Conceptually, trampolining is one possible way to implement continuation passing style. Which has some theoretical elegance, but is more taxing on the brain than the conventional "direct" style. I would say that recursion is still preferable when you can get away with it, but in this case I went straight for trampolining because I think there might actually be a real risk that these trees get (slightly) too large.

XanderVertegaal · 2026-03-19T10:02:26Z

+    tree.nodes.push(node);
+    // Tease out the different parts of the stringified node payload. The
+    // following lines will be rewritten using regular expressions.
+    const lines = nltk.node.split('\n');


Perhaps this string decoding could live in its own function (so we can test it in isolation), but you might want to wait for that until you have introduced the regexes.

Review suggestion in #79 Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

jgonggrijp · 2026-03-19T14:52:34Z

Your plan corresponds well to what we agreed, so please go ahead with the implementation. The only item on the list I would like you to clarify is 10: what do you mean with the 'no trigger unless viewing parse tab'?

The effect that I described to you previously, where the tableau would not render unless the "CCG / LLF" tab was selected while I pressed the "Parse and prove" button. However, this seems to have been solved already, possibly because I accepted your suggestion to add the share operator. It does not matter anymore which tab is shown when I press the button.

I'll double-check after rebasing just to make sure, though.

- Adopt same names for tree node parts as in LangPro API. - Distinguish node ID vs. numerical index of appearance. - Distinguish node vs. term vs. head. Mods and args contain terms, too.

…u model

Based on actual output from the LangPro container.

@XanderVertegaal

Per review comment by @XanderVertegaal in #79.

@XanderVertegaal

Per review comment by @XanderVertegaal in #79.

Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

@XanderVertegaal

Per review comment by @XanderVertegaal in #79.

…dth (#79)

Review suggestion in #79 Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

I initially distinguished between terminal and internal trees as well, but applying this typing in the logic and convincing tsc that everything was fine became too unwildly.

jgonggrijp · 2026-03-19T22:52:46Z

@XanderVertegaal I force-pushed again because I needed to insert some of the new types early in history. Otherwise, all of the intermediate commits would be uncompilable.

I did docker compose down in order to rebase and then did docker compose --build up afterwards to check that all the tests would still pass. They did, but when trying to visit the frontend, I discovered that my templates don't typecheck yet. I will fix that later but I need to leave the library now. You are welcome to review the types in the meanwhile.

The only changes I still expect to make is type fixes in the templates and/or a simplification in the @/types, where I simply collapse all ProofNode subtypes into a single object type with all fields optional. That is a bit less correct but easier to work with. In the latter case I might rebase the last two commits one more time.

I initially distinguished between terminal and internal trees as well as between terminal nodes, internal nodes and unsupported nodes, but applying this typing in the logic and convincing tsc that everything was fine became too unwildly.

jgonggrijp · 2026-03-23T21:52:41Z

Done.

XanderVertegaal

Great work! 👍

XanderVertegaal · 2026-03-24T20:33:56Z

-            }
-        ]
-    }
+    public readonly tree = input.required<ProofTree>();


(Utterly minor: I think inputs are conventionally put at the top of the component. At least, that is where most people will expect to find them.)

XanderVertegaal · 2026-03-24T20:34:52Z

    }

-    set tree(value: any) {
+    set tree(value: ProofTree) {


It feels so good to see these anys replaced with actual types <3

XanderVertegaal · 2026-03-24T20:50:29Z

Glorious! 😍

Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

jgonggrijp requested a review from XanderVertegaal March 17, 2026 03:10

jgonggrijp added the enhancement New feature or request label Mar 17, 2026

XanderVertegaal reviewed Mar 17, 2026

View reviewed changes

jgonggrijp added a commit that referenced this pull request Mar 17, 2026

Give proof tabs different symbols

af7d88e

Per review comment by @XanderVertegaal in #79.

jgonggrijp added a commit that referenced this pull request Mar 17, 2026

Document the frontend's NLTK -> tableau conversion (#79)

83aa8da

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Take into account that extractProofs might map over null

8270a96

Per review comment by @XanderVertegaal in #79.

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Fix centering of red discs in proof tableau leaf nodes (#79)

20aaa24

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Distinguish between open and closed branches in proof tableaux (#79)

7b8f98b

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Make wide proof tableaux visible and scrollable (#79)

1605045

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Scroll proof tableau to root node initially (#79)

495f3f1

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Take rule into account when calculating tableau visualization node wi…

82cccbd

…dth (#79)

XanderVertegaal reviewed Mar 19, 2026

View reviewed changes

Comment thread frontend/src/app/annotate/annotation-menu/annotation-menu.component.html Outdated

XanderVertegaal reviewed Mar 19, 2026

View reviewed changes

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Use bootstrap overflow classes

cf484da

Review suggestion in #79 Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

jgonggrijp added 6 commits March 19, 2026 17:56

Clear up terminology in frontend tableau-svg components

a17e983

- Adopt same names for tree node parts as in LangPro API. - Distinguish node ID vs. numerical index of appearance. - Distinguish node vs. term vs. head. Mods and args contain terms, too.

Encode semantic sign instead of presentation color in frontend tablea…

98450d4

…u model

Add support for tableau tree node mods

2071161

Outfactor mock tableau tree from frontend tableau-svg component

0b083e2

Add mock NLTK proof to frontend

8e09bc8

Based on actual output from the LangPro container.

Update frontend mock NLTK proof to reflect latest data

7d47a3a

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Give proof tabs different symbols

de91ce3

Per review comment by @XanderVertegaal in #79.

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Document the frontend's NLTK -> tableau conversion (#79)

7517ffe

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Take into account that extractProofs might map over null

141f9a6

Per review comment by @XanderVertegaal in #79.

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Fix centering of red discs in proof tableau leaf nodes (#79)

c517c49

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Distinguish between open and closed branches in proof tableaux (#79)

f1e5d01

jgonggrijp force-pushed the feature/actual-proof-svg branch from cf484da to 23b81c3 Compare March 19, 2026 17:50

jgonggrijp and others added 14 commits March 19, 2026 23:34

Share the ParseService#parse$ observable

49b4656

Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

Give proof tabs different symbols

4fd0c06

Per review comment by @XanderVertegaal in #79.

Document the frontend's NLTK -> tableau conversion (#79)

f923861

Fix centering of red discs in proof tableau leaf nodes (#79)

31a48df

Distinguish between open and closed branches in proof tableaux (#79)

857b2e1

Make wide proof tableaux visible and scrollable (#79)

35e972f

Scroll proof tableau to root node initially (#79)

01fddf5

Take rule into account when calculating tableau visualization node wi…

c1a2f9a

…dth (#79)

Replace let by const after review comment by @XanderVertegaal in #79

5c90b63

Outfactor parseNltkNode from nltknode2tableaunode (#79)

03fbf8a

Strip quotes from tableau node rules (#79)

36b3536

Give the leaf node icons pixel-perfect positioning (#79)

626693a

Use bootstrap overflow classes

1b72b01

Review suggestion in #79 Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

Move frontend ParseResponse type from service to @/types (#79)

fccb884

jgonggrijp force-pushed the feature/actual-proof-svg branch from 23b81c3 to 5899df2 Compare March 19, 2026 22:46

jgonggrijp added a commit that referenced this pull request Mar 19, 2026

Apply proof types in frontend logic (#79)

5899df2

jgonggrijp added 2 commits March 23, 2026 22:44

Apply proof types in frontend logic (#79)

a5d3aca

jgonggrijp force-pushed the feature/actual-proof-svg branch from 5899df2 to a5d3aca Compare March 23, 2026 21:52

jgonggrijp requested a review from XanderVertegaal March 23, 2026 21:52

jgonggrijp mentioned this pull request Mar 23, 2026

Reduce horizontal space in rendered proof tableaux #83

Open

XanderVertegaal approved these changes Mar 24, 2026

View reviewed changes

jgonggrijp and others added 2 commits March 25, 2026 14:49

Apply suggestions from code review in #79

1a5d7a8

Co-authored-by: Xander Vertegaal <73882506+XanderVertegaal@users.noreply.github.com>

Move tableau SVG @input to top of component (#79 review comment)

35c84db

jgonggrijp merged commit 0ad5ca8 into develop Mar 25, 2026
1 check passed

jgonggrijp deleted the feature/actual-proof-svg branch March 25, 2026 13:59

Conversation

jgonggrijp commented Mar 17, 2026

Uh oh!

XanderVertegaal commented Mar 17, 2026

Uh oh!

XanderVertegaal left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jgonggrijp commented Mar 17, 2026

Uh oh!

XanderVertegaal commented Mar 19, 2026

Uh oh!

Uh oh!

XanderVertegaal left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

XanderVertegaal Mar 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jgonggrijp Mar 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jgonggrijp commented Mar 19, 2026

Uh oh!

jgonggrijp commented Mar 19, 2026

XanderVertegaal Mar 20, 2026 •

edited

Loading

jgonggrijp Mar 19, 2026 •

edited

Loading