TDFA(1): delay the tag writes of a closure to the outgoing transitions

[hhugo]

Turns the tagged DFA of #204 into a TDFA(1), after Trofimovich, "Tagged Deterministic Finite Automata with Lookahead" (2017). Stacked on #208 (base: the pr4c-no-mark-snapshot branch), four commits.

The idea. In #204 the tag writes met in the epsilon closure of a state are performed on the transition entering it (TDFA(0)). Here each configuration keeps them as delayed writes and performs them when it takes a character transition, i.e. once the next character is known. A configuration that cannot consume that character never performs them.

• The end tag of (Plus digit as n), '.' is written once, on the '.' transition, not on every digit: the "self-loop tag delay" Goal of the codegen tests, obtained in general.
• Fewer tags have two live values at once. Over test/codegen/test_gen.ml: writes 47 → 29, copies 29 → 19, cells 48 → 40, for 127 → 130 states (states that differ only by their delayed writes cannot be identified). Realistic lexer: 17 states before and after, writes 4 → 2.
• Nothing runs before the automaton starts: init_tags is removed from compiled and compiled_ir (sedlex.compiler has not been released).

Commits

1. End of input gets its own transitions. eof | 'b' is one character set in the NFA, so a DFA transition could be taken both by end of input and by characters; reading end of input does not advance the position, unlike reading a character. split_moves now splits such sets: a transition's character set is either Cset.eof or does not contain end of input. One more match arm for those rare patterns, no existing expect output changes.
2. Runtime primitive __private__set_mem_prev_pos.
3. The switch. config gains delayed; the closure records writes there; transitions turns the delayed writes of a configuration that moves into the writes of that transition, so cell assignment and register moves are untouched; state keys include the delayed writes; final operations set those of the accepting configuration on the canonical cells. The operations of a transition execute before its character is consumed, but the generated code runs them after reading it, so Set_position compiles to set_mem_prev_pos on character transitions and stays set_mem_pos on end-of-input ones.
4. Behaviour test for sub-matches that end where end of input is read.

Verification

• Every captured value pinned in test/basic.ml is unchanged (one cell count drops). Patterns without captures generate byte-identical code.
• The Add an oracle test harness: reference matcher vs compiled tagged DFA #202 oracle, run locally with transition operations applied before the character and no cell snapshot: no disagreement on the hand-written cases nor on 300k random cases at this tip (5M on an earlier version of this branch). It does not model eof, hence commit 4.

#207 (register optimizations) is stacked on this PR.

🤖 Generated with Claude Code

[Copilot]

Copilot review overview

🟢 Approval recommended

The TDFA(1) delayed-write mechanics, runtime position primitives, PPX emission logic, and updated/added tests are consistent and coherent with the stated semantics (including eof cases).

Review effort: Lite
Findings: None

What changed in this PR

This PR upgrades Sedlex’s tagged determinization from TDFA(0) to TDFA(1) by delaying tag writes discovered in an epsilon-closure until the configuration actually takes a character transition (one-symbol lookahead). This improves capture semantics in loop/closure shapes (e.g., avoids repeatedly writing the same end tag on every loop iteration) while keeping the generated runtime operations correct around eof.

Changes:

• Implement TDFA(1) delayed-closure writes in the compiler (state keys include delayed writes; transitions materialize delayed writes; accepting final_ops materialize delayed writes onto canonical cells).
• Extend the runtime + PPX code generator to record “position before the consumed character” correctly, including transitions that may consume either a character or eof.
• Update/extend expect tests to reflect the new DOT/codegen output and add coverage for eof-involved transitions.

File	Description
test/​codegen/​test_realistic.ml	Updates the “realistic” codegen expect output to reflect delayed tag writes on loop exit transitions.
test/​codegen/​test_gen.ml	Updates many codegen expects for TDFA(1) tag placement and adds an expect for transitions that eof can take.
test/​basic.ml	Adjusts memory-cell expectation for a discriminator case and adds behavior tests for submatch end positions around eof.
src/​syntax/​ppx_sedlex.ml	Adds position modes and emits set_mem_prev_pos / set_mem_pos_before depending on whether a transition may read eof.
src/​lib/​sedlexing.mli	Exposes new runtime primitives for recording pre-consumption positions in memory cells.
src/​lib/​sedlexing.ml	Implements __private__set_mem_prev_pos and __private__set_mem_pos_before.
src/​compiler/​sedlex.mli	Updates documentation around transition op timing and clarifies init_tags as always empty under delayed-closure writes.
src/​compiler/​sedlex.ml	Implements TDFA(1) delayed writes via config.delayed, updated closure/transition logic, and accepting-state finalization of delayed writes.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[Copilot]

Copilot review overview

🔵 Needs a closer look

The core determinization and capture-position semantics require final human validation, and one public API comment remains outdated.

Review effort: Balanced
Findings: 1

Open (1)

• Update compile docs to remove nonexistent initial tag operations · New

[pmetzger]

Ah, you found the Trofimovich paper! Very cool!

[pmetzger]

(When do you think you want to commit?)

[hhugo]

(When do you think you want to commit?)

This is ready to merge, I think