WITH-block internals for Modula-2 bodies

WITH bodies are fully checked instead of skipped: the guard must
denote a record variable or field (gm2 rejects non-records,
undereferenced pointers, and even record-valued function results,
where a call guard is a syntax error); field names shadow outer scope
innermost-first; bodies see real field types, so assignments, calls
and expressions check exactly as qualified accesses would. Genuinely
unknown names are reported by the checker (the analyser skips WITH
regions), including unknown guards.

Validation: 22-case differential suite against gm2 -fiso with zero
mismatches (shadowing, nesting, two-level access, field guards,
builtin-named fields, call guards); 178-case builtin suite still
clean; 21 real files at zero errors; live LSP round-trip publishes
the new diagnostics.

extensions/modula2-language/DIAGNOSTICS.md

@@ -58,8 +58,7 @@ calibrated case-by-case against `gm2`:
 - `RETURN` without a value, value-returning `RETURN`s, `RETURN` outside
   procedures and values returned from void procedures.
 
-Still out of scope: use-before-declaration order, range checking,
-`WITH`-block internals.
+Still out of scope: use-before-declaration order, range checking.
 
 ## Real-file validation
 
@@ -150,6 +149,21 @@ existing ignored-result/void paths. A 178-case differential suite
 (`gm2` accept ⇒ zero diagnostics; `gm2` reject ⇒ at least one) passes
 with no mismatches, and the real-file corpora stay at zero issues.
 
+## WITH-block internals
+
+`WITH` bodies used to be skipped wholesale; they are now fully checked
+with the guard record's fields in scope. The guard must denote a record
+variable or field (gm2 rejects anything else, including an
+undereferenced pointer and even a record-valued function result, which
+is a syntax error there); field names shadow outer scope, nesting works
+innermost-first, and bodies see real field types, so assignments, calls
+and expressions inside are checked exactly as qualified accesses would
+be. Genuinely unknown names are reported (`WITH rec DO nope := 1` and
+`WITH nope DO` both error, matching gm2). A 22-case differential suite
+passes with no mismatches, including shadowing, nesting, two-level
+access (`inner.y`), field guards (`WITH o.inner DO`), and fields named
+like builtins (`ORD`).
+
 ## Circular dependencies (no use-before-declaration)
 gm2 is multi-pass, so declaration order never matters — there is
 deliberately no use-before-declaration check. What is checked instead is

extensions/modula2-language/src/m2/checker.ts

@@ -98,6 +98,10 @@ class Walker {
   private returnType: M2Type | null | undefined;
   /** Depth of nested builtin-procedure argument lists (type args allowed). */
   private builtinArgs = 0;
+  /** Guard records of enclosing WITH blocks (innermost last). */
+  private withStack: {
+    type: M2Type; decl: { sym: M2Symbol; unit: M2Unit; dir: string } | null;
+  }[] = [];
   /** Parsing the right-hand side of an assignment to a procedure variable. */
   private expectingProc = false;
   constructor(
@@ -166,7 +170,7 @@ class Walker {
         case 'REPEAT': this.parseRepeat(depth); return;
         case 'LOOP': this.next(); this.parseSeq(new Set(['END']), depth + 1); this.expectKw('END'); return;
         case 'FOR': this.parseFor(depth); return;
-        case 'WITH': this.parseWith(); return;
+        case 'WITH': this.parseWith(depth); return;
         case 'CASE': this.parseCase(depth); return;
         case 'EXIT': this.next(); return;
         default:
@@ -323,40 +327,80 @@ class Walker {
     this.expectKw('END');
   }
 
-  /** WITH blocks use unqualified field access: skip without checks (conservative). */
-  private parseWith(): void {
+  /** WITH opens its guard record's fields as unqualified names.
+   *
+   *  The guard is checked like any expression, then must denote a record
+   *  (gm2 rejects anything else, including an undereferenced pointer).
+   *  Field names shadow outer scope (verified against gm2); genuinely
+   *  unknown names fall through to normal resolution and are reported
+   *  by the analyser, never here. */
+  private parseWith(depth: number): void {
     this.next(); // WITH
-    let depth = 0;
-    for (;;) {
-      const t = this.peek();
-      if (!t) return;
-      if (t.kind === 'symbol') {
-        if (t.text === ';' && depth === 0) return;
-        if (t.text === '[' || t.text === '(' || t.text === '{') depth++;
-        else if (t.text === ']' || t.text === ')' || t.text === '}') depth = Math.max(0, depth - 1);
-        this.next();
-      } else if (t.kind === 'keyword' && t.text === 'DO' && depth === 0) {
-        this.next();
-        break;
-      } else if (t.kind === 'keyword') {
-        return;
-      } else {
-        this.next();
-      }
+    const guard = this.parseExpr(0);
+    this.expectKw('DO');
+    const gtype = guard.type.kind === 'subrange' ? guard.type.base : guard.type;
+    if (gtype.kind !== 'unknown' && gtype.kind !== 'record') {
+      this.issue(guard.tok, `WITH requires a record, found ${displayType(guard.type)}`);
     }
-    let nest = 1;
-    for (;;) {
-      const t = this.peek();
-      if (!t) return;
-      if (t.kind === 'keyword' && OPENERS.has(t.text)) nest++;
-      else if (t.kind === 'keyword' && t.text === 'END') {
-        nest--;
-        this.next();
-        if (nest === 0) return;
-        continue;
+    // The guard must be a variable (or field) designator: gm2 rejects
+    // even a record-valued function result (`WITH Get(0) DO` is a syntax
+    // error there). Unknown designators stay silent.
+    if (guard.info.kind === 'proc') {
+      this.issue(guard.tok, `WITH requires a variable, found procedure "${guard.tok.text}"`);
+    }
+    const decl = (guard.info.kind === 'var' || guard.info.kind === 'const')
+      ? { sym: guard.info.sym, unit: guard.info.host, dir: guard.info.dir } : null;
+    // An unresolvable guard designator (`WITH nope DO`, `WITH UNK[i] DO`)
+    // is unknown exactly as gm2 reports it; anything else (literals and
+    // the like) is covered by the record check below.
+    if (guard.info.kind === 'unknown' && guard.tok.kind === 'ident') {
+      this.issue(guard.tok, `Unknown identifier "${guard.tok.text}"`);
+    }
+    this.withStack.push({ type: guard.type, decl });
+    try {
+      this.parseSeq(new Set(['END']), depth + 1);
+    } finally {
+      this.withStack.pop();
+    }
+    this.expectKw('END');
+  }
+
+  /** A bare name visible through the WITH stack (innermost guard first).
+   *
+   *  Pointer guards dereference to their target record (gm2 rejects the
+   *  guard itself unless `^`-dereferenced, but the body still sees the
+   *  record's fields). Absent fields and unknown guards fall through to
+   *  normal resolution. */
+  private resolveWithField(head: Token): {
+    type: M2Type; decl: { sym: M2Symbol; unit: M2Unit; dir: string } | null;
+  } | null {
+    if (head.kind !== 'ident') return null;
+    for (let k = this.withStack.length - 1; k >= 0; k--) {
+      const g = this.withStack[k];
+      if (g.decl) {
+        const found = findRecordField(
+          g.decl.unit, g.decl.dir, g.decl.sym, head.text, head.line, head.ch);
+        if (found) {
+          return {
+            type: resolveDeclaredType(found.sym, found.unit, found.dir, head.line, head.ch),
+            decl: { sym: found.sym, unit: found.unit, dir: found.dir },
+          };
+        }
+      }
+      let t = g.type.kind === 'subrange' ? g.type.base : g.type;
+      for (let n = 0; n < 8 && t.kind === 'pointer'; n++) t = t.target;
+      if (t.kind !== 'unknown' && t.kind === 'record') {
+        const found = findFieldInType(
+          this.ctx.unit, this.ctx.docDir, t, head.text, head.line, head.ch);
+        if (found) {
+          return {
+            type: resolveDeclaredType(found.sym, found.unit, found.dir, head.line, head.ch),
+            decl: { sym: found.sym, unit: found.unit, dir: found.dir },
+          };
+        }
       }
-      this.next();
     }
+    return null;
   }
 
   private parseCase(depth: number): void {
@@ -440,13 +484,20 @@ class Walker {
 
   /** Parse qualifier chain, postfixes and an optional call. Emits call/operand issues. */
   private parseDesignatorRest(head: Token, mode: 'expr' | 'stmt'): Value {
-    let info = this.resolveHead(head);
+    const withField = this.resolveWithField(head);
+    let info = withField ? { kind: 'field' as const } : this.resolveHead(head);
+    // Inside WITH, a bare name resolving nowhere is unknown (the analyser
+    // skips WITH regions, so the checker reports it — once, here).
+    if (!withField && this.withStack.length > 0 && head.kind === 'ident' && info.kind === 'unknown') {
+      this.issue(head, `Unknown identifier "${head.text}"`);
+    }
     let tok = head;
     // Declaration behind the current value (for field selection).
     let cur: { sym: M2Symbol; unit: M2Unit; dir: string } | null =
-      (info.kind === 'var' || info.kind === 'const')
+      withField ? withField.decl
+      : (info.kind === 'var' || info.kind === 'const')
         ? { sym: info.sym, unit: info.host, dir: info.dir } : null;
-    let type = this.valueType(info, tok);
+    let type = withField ? withField.type : this.valueType(info, tok);
     // Qualifier chain: M.X or r.field.
     while (this.atSym('.')) {
       this.next(); // .