Fix free variable issue in Boole

[kondylidou]

Problem

When a Boole program had 4+ datatype declarations and the first datatype's
testers or selectors (e.g. color..iscolor_Red, color..color_Red_0) were
referenced in a later function, the verifier reported them as free variables
during type-checking. Moving the referenced datatype to any position other than
first worked around the bug.

Closes #1142

Root cause

initFVarIsOp built a symbol-class table by scanning program commands — one
entry per command (one false per datatype command). But the GlobalContext
registers many entries per datatype: the type itself plus every constructor,
tester, and selector generated by templates. This made fvarIsOp too short and
misaligned with the actual fvar indices.

When the referenced datatype was declared first, its testers/selectors landed at
low fvar indices that fell inside the misaligned table. Those indices returned
false (treat as type symbol), so the testers were emitted as .fvar (variable
references) instead of .op (function applications). The type-checker then
rejected them as undeclared free variables.

When the datatype was not first, the tester indices fell past the end of the
table and hit the fallback path in getFVarIsOp, which correctly reads
GlobalContext.vars[i] — the same source of truth the DDM elaborator uses for
all symbols.

Fix

Removed fvarIsOp, initFVarIsOp, and registerCommandSymbols entirely.
getFVarIsOp now reads directly from GlobalContext.vars[i]:

• GlobalKind.type → emit as .fvar (type symbol, not a callable)
• GlobalKind.expr → emit as .op, except for command_var global
  variables, which become procedure parameters in Core and must remain .fvar

The command_var carve-out uses the existing globalVarTypes map (already
collected in the pre-pass), so no new state is needed.

Test

Added StrataTest/Languages/Boole/datatype_tester_freevar.lean — a direct
regression for the issue's failing case: color declared first among four
datatypes, with get_val referencing color..iscolor_Red and
color..color_Red_0.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[kondylidou]

@ChengZ3 here is the fix to the issue you submitted. Thank you

[tautschnig]

Nice root-cause writeup. The parallel fvarIsOp array was a classic "shadow data structure drifts out of sync with source of truth" bug — registerCommandSymbols emitted one slot per command while GlobalContext.vars grows by 1 + #constructors + #testers + #selectors for a datatype command (and by #funcs for a command_recfndefs). Reading directly from gctx.vars in getFVarIsOp removes the class of bug entirely. lake build passes on the branch; the added regression test also passes.

Four concerns below — (1) and (2) are the two I'd most like addressed; (3) and (4) are a proof suggestion and maintenance note.

1. globalVarTypes is now overloaded as both a type map and a command_var-name set. The new getFVarIsOp uses !globalVarTypes.contains name as the carve-out predicate. This works today, but it couples the semantics of the map (values used for parameter-type lookup elsewhere) to the semantics of the key set (membership used for op-vs-var classification). A future refactor that populates the map from another source (say, a procedure's local-var pre-pass) will silently change getFVarIsOp's behaviour. Two clean options:

• Add a dedicated globalVarNames : Std.HashSet String to TranslateState, populated in the same pre-pass, and use it for the predicate. Cheap and explicit.
• Keep one map but introduce a named predicate private def TranslateState.isGlobalVar (st) (name : String) : Bool := st.globalVarTypes.contains name with a docstring pinning the invariant. No state change; just encapsulation.

Either way, the inline comment on line 115 should spell out the invariant the predicate is relying on: "a name is in globalVarTypes iff it was introduced by a command_var". That's not a priori obvious from the field's name.

2. Test coverage is narrow for a fix that changes a hot path in translation. The regression reproduces exactly the ticket's failing case, which is the right baseline. But the fix claims to cover a broader scenario ("any datatype or command_recfndefs whose expansion exceeds 1 entry in gctx.vars"), and the test only exercises one position of one kind. Missing:

• A variant where the referenced datatype is not first (e.g. color declared 2nd or 3rd). The pre-fix bug was position-dependent; the post-fix code should be position-independent. Pinning both halves guards against regressions in either direction.
• A program with a command_var global and a datatype referenced the same way. This exercises the globalVarTypes.contains carve-out directly.
• A command_recfndefs block with several recursive functions whose names are referenced in a later function. command_recfndefs is the other "one command → many gctx.vars entries" case per the removed registerCommandSymbols. Without this test, a regression here would not be caught.

All three are small #strata seeds. I'd add them in this same test file or a datatype_tester_freevar_variants.lean.

3. Proof coverage suggestion. The new getFVarIsOp is a short, pure function with a crisp specification that reduces to reading gctx.vars[i]. Worth a theorem pinning the contract:

/-- `getFVarIsOp` agrees with `gctx.vars` classification, with the
    `command_var` names carved out as terms. -/
theorem getFVarIsOp_spec (st : TranslateState) (m : SourceRange) (i : Nat) :
    match (getFVarIsOp m i).run st with
    | .ok (b, st') =>
        st' = st ∧
        match st.gctx.vars[i]? with
        | some (name, .expr _) => b = !st.globalVarTypes.contains name
        | some (_,    .type _ _) => b = false
        | none => False
    | .error _ => st.gctx.vars[i]?.isNone

This is a pure unfolding + case-split on gctx.vars[i]?; should go through without any lemmas. Its value is not in the proof effort but in documenting the contract — anyone reading getFVarIsOp in the future can see exactly what invariant it maintains, and a regression that breaks the carve-out will fail the proof.

Stronger theorem (optional, harder): getFVarIsOp i agrees with the classification DDM's elaborator uses to decide .fvar vs .op for the same index. That would require a spec from DDM's GlobalKind handling, which I don't see a clean statement of. Worth thinking about for a follow-up, not this PR.

4. Commit history. The branch has commits fix the datatype issue, regression, more, plus a merge commit. For merge, I'd squash to one or two commits with descriptive messages — the existing PR body is already a good commit message. Nit, doesn't block.

Minor refactor callouts:

• The comment block at the top of TranslateState (lines 28-45) could briefly mention that op-vs-var classification for free variable references is derived from gctx.vars (single source of truth), and globalVarTypes supplies the only exception. That reframes future readers toward "consult gctx, not a per-command table" and prevents the next person from re-introducing a shadow table.
• registerCommandSymbols is gone, but the command-tag cases it enumerated are still useful reference documentation (which commands introduce which gctx.vars entries). Could move that list to a comment above getFVarIsOp as a table — "datatype: 1 + #ctors + #testers + #selectors; recfndefs: #funcs; typedecl: 1; constdecl/fndecl/fndef: 1; var: 1 (but carved out via globalVarTypes); procedure/block/axiom/distinct: 0". Explicit documentation of the gctx side helps anyone who has to touch this code after the fact.

[joscoh]

Never mind

[MikaelMayer]

🤖🔍 Clean fix that correctly addresses the root cause: the misaligned fvarIsOp array is replaced by reading directly from gctx.vars, which is the single source of truth. The command_var carve-out is sound — the invariant that globalVarTypes keys exactly correspond to command_var names is maintained by the pre-pass. Test coverage exercises the original bug scenario plus three meaningful variants.

The getFVarIsOp_spec theorem is a nice machine-checked contract, though it's currently unreferenced (private and unused). If it's intended as living documentation, that's fine; if it's meant to be used by downstream proofs, it should be made accessible.

One minor documentation gap noted inline.

The base branch was changed.

[joscoh]

This one can be targeting either main or main2, since unlike the other one, it doesn't depend (AFAIK) on anything currently in main2 only (i.e. the int-valued recursion PR). I will approve either way

[MikaelMayer]

🤖🔍 The new commit since my last review is just a merge from main2 — no code changes addressing my inline nit about typesynonym missing from the getFVarIsOp docstring list. That said, it's a trivial documentation nit and the PR is already approved. Reviewer sign-off still needed for the nit, but it's non-blocking.

[MikaelMayer]

🤖🔍 All previous comments appear addressed — reviewer sign-off still needed.

[joscoh]

Will merge once #1181 shows the internal benchmarks succeed