In-logic evaluation is a key bottleneck in interactive theorem provers, and a recent HOL4 library aims to accelerate it. To make this library usable in practice, we need a parser that can target its translation interface — but the standard parser engine wasn't built with that interface in mind. The core implementation work restructures the parser engine into a defunctionalized form, so it can explicitly call the library translation interface instead of relying on the legacy evaluation path.

The results are mixed in an instructive way. For short, flat programs, the new parser is about 1.5x faster than the legacy solution. But for long, deeply nested programs, garbage collection overhead dominates, and the new approach actually loses to the old one. This suggests that "faster evaluation library" doesn't automatically mean "port everything to it" — the crossover point depends on program shape, and naively porting can backfire.

We present the implementation details behind the defunctionalization and translation-interface calls, walk through the benchmark methodology and results, and discuss what the GC overhead on large inputs implies for deciding when computation should be ported to the new library — and what changes to the library itself might address this case.