From 71cbfd43d941a2d743a48e0ec9d5631874fe721e Mon Sep 17 00:00:00 2001
From: Kevin Gibbons <bakkot@gmail.com>
Date: Mon, 17 Oct 2022 15:39:53 -0700
Subject: [PATCH] expression parser: skip contents of <del> tags

---
 src/expr-parser.ts  | 25 ++++++++++++++++-
 test/expr-parser.js | 65 ++++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 88 insertions(+), 2 deletions(-)

diff --git a/src/expr-parser.ts b/src/expr-parser.ts
index 0d42a407..a2fd5666 100644
--- a/src/expr-parser.ts
+++ b/src/expr-parser.ts
@@ -171,6 +171,20 @@ function emptyThingHasNewline(s: Seq) {
   );
 }
 
+function getTagName(tok: ProsePart): 'open-del' | 'close-del' | null {
+  if (tok.name !== 'tag') {
+    return null;
+  }
+  const lowcase = tok.contents.toLowerCase();
+  if (lowcase.startsWith('<del>') || lowcase.startsWith('<del ')) {
+    return 'open-del';
+  } else if (lowcase.startsWith('</del>') || lowcase.startsWith('</del ')) {
+    return 'close-del';
+  } else {
+    return null;
+  }
+}
+
 class ExprParser {
   declare src: FragmentNode[];
   declare opNames: Set<String>;
@@ -218,6 +232,15 @@ class ExprParser {
         }
         ++this.srcIndex;
         this.textTokOffset = null;
+        // skip anything in `<del>`
+        if (getTagName(tok) === 'open-del') {
+          while (
+            this.srcIndex < this.src.length &&
+            getTagName(this.src[this.srcIndex]) !== 'close-del'
+          ) {
+            ++this.srcIndex;
+          }
+        }
         continue;
       }
       const { groups } = match;
@@ -302,7 +325,7 @@ class ExprParser {
           return { type: 'seq', items };
         }
         case 'eof': {
-          if (items.length === 0 || !close.includes('eof')) {
+          if (!close.includes('eof')) {
             throw new ParseFailure(`unexpected eof (expected ${formatClose(close)})`, next.offset);
           }
           return { type: 'seq', items };
diff --git a/test/expr-parser.js b/test/expr-parser.js
index 48706108..fc18adc4 100644
--- a/test/expr-parser.js
+++ b/test/expr-parser.js
@@ -1,6 +1,12 @@
 'use strict';
 
-let { assertLint, positioned, lintLocationMarker: M, assertLintFree } = require('./utils.js');
+let {
+  assertLint,
+  positioned,
+  lintLocationMarker: M,
+  assertLintFree,
+  getBiblio,
+} = require('./utils.js');
 
 describe('expression parsing', () => {
   describe('valid', () => {
@@ -286,4 +292,61 @@ describe('expression parsing', () => {
       );
     });
   });
+
+  describe('handling of <del>', () => {
+    let biblio;
+    before(async () => {
+      biblio = await getBiblio(`
+        <emu-clause id="del-complex" type="abstract operation">
+          <h1>
+          Example (
+              _x_: unknown,
+              _y_: unknown,
+            ): unknown
+          </h1>
+          <dl class="header"></dl>
+        </emu-clause>
+      `);
+    });
+
+    it('ignores contents of <del> tags', async () => {
+      await assertLint(
+        positioned`
+          <emu-alg>
+            1. Perform ${M}Example(x<del>, y</del>).
+          </emu-alg>
+        `,
+        {
+          ruleId: 'typecheck',
+          nodeType: 'emu-alg',
+          message: 'Example takes 2 arguments, but this invocation passes 1',
+        },
+        {
+          extraBiblios: [biblio],
+        }
+      );
+
+      await assertLintFree(
+        `
+          <emu-alg>
+            1. Perform Example(x, y<del>, z</del>).
+          </emu-alg>
+        `,
+        {
+          extraBiblios: [biblio],
+        }
+      );
+
+      await assertLintFree(
+        `
+          <emu-alg>
+            1. <del>Perform Example(x, y, z).</del>
+          </emu-alg>
+        `,
+        {
+          extraBiblios: [biblio],
+        }
+      );
+    });
+  });
 });