feat(python): Add support for ** (power) operator

[MikaelMayer]

The Python-to-Laurel pipeline rejected programs using the ** operator with "Binary operator not yet supported: Pow", causing an exit-4 crash.

This PR adds support by:

• Mapping Pow to the existing PPow prelude function in PythonToLaurel.lean
• Constant-folding ** with integer literal operands at translation time (e.g. 1024 ** 3 becomes 1073741824)
• For non-constant operands, PPow delegates to an uninterpreted int_pow function, handling int×int, bool×int, and int×bool combinations
• Replacing the PPow stub (which threw UnimplementedError) with the real implementation

Tested with a new test_power.py test that verifies 8 ** 2 == 64 and 2 ** 10 == 1024 through the full pipeline. Existing tests pass.

[joehendrix]

I added a question above, but we could postpone that for a later commit.

[MikaelMayer]

Re: moving constant folding to concreteEval — investigated this. The issue is that int_pow must be declared in the prelude (so PPow can reference it), but adding a factory function with the same name causes a "function already exists" error during evaluation (addFactoryFunc rejects duplicates). For now, constant folding stays in PythonToLaurel for literal operands. Moving it to concreteEval would require allowing factory functions to override/merge with prelude declarations.

[MikaelMayer]

Re: moving constant folding to concreteEval — investigated this. The issue is that int_pow must be declared in the prelude (so PPow can reference it), but adding a factory function with the same name causes a "function already exists" error during evaluation (addFactoryFunc rejects duplicates). For now, constant folding stays in PythonToLaurel for literal operands. Moving it to concreteEval would require allowing factory functions to override/merge with prelude declarations.

We did that for regular expressions, please check the PR that introduced them. Regular expressions are core functions that were exposed in Laurel, we should do the same.

[MikaelMayer]

Investigated the regex pattern. The difference is that re_fullmatch_str (returning regex type) is filtered out by the Laurel-to-Core translator, so it never reaches Core's addFactoryFunc. But int_pow (returning int) IS translated to Core as a bodyless function, causing a duplicate when the factory also provides it.

To use concreteEval for int_pow, we'd need to either:

1. Filter int_pow in the Laurel-to-Core translator (like regex functions)
2. Allow addFactoryFunc to merge/override bodyless declarations

Both are larger changes. For now, constant folding for literal ** operands is done in PythonToLaurel. Non-constant cases use the uninterpreted int_pow from the prelude.

[MikaelMayer]

Investigated the regex pattern. The difference is that re_fullmatch_str (returning regex type) is filtered out by the Laurel-to-Core translator, so it never reaches Core's addFactoryFunc. But int_pow (returning int) IS translated to Core as a bodyless function, causing a duplicate when the factory also provides it.

To use concreteEval for int_pow, we'd need to either:

1. Filter int_pow in the Laurel-to-Core translator (like regex functions)
2. Allow addFactoryFunc to merge/override bodyless declarations

Both are larger changes. For now, constant folding for literal ** operands is done in PythonToLaurel. Non-constant cases use the uninterpreted int_pow from the prelude.

What do you mean re_fullmatch_str is filtered out by the Laurel to Core translator? There is an equivalent in Core's factory and I'm sure that the Laurel gets mapped to the Core equivalent, it was done recently in a PR that even has some tests to prove it (including PR 615 that proves that regex support works)
IF it's a matter of having different names you can do this.

The problem of doing constant folding in PythonToLaurel is that it's outside of Core. It's better if all the transformations remain in Core, including constant folding that can be done during partial evaluation of Core.
So figure out a way. We shouldn't need to merge or override bodiless declarations.

[MikaelMayer]

Moved constant folding to concreteEval in PyFactory.lean (intPowFunc). To resolve the duplicate-name issue, ProgramEval now skips bodyless functions that already exist in the factory — the factory version with concreteEval takes precedence. This follows the regex factory pattern.

[MikaelMayer]

Reverted the ProgramEval hack. Investigated why regex works: re_fullmatch_str uses the regex type which doesn't exist in Core, so the Laurel-to-Core translator naturally filters it out (fails in handleUnaryOps). The factory then provides it without conflict.

int_pow uses int which translates fine to Core, causing the duplicate. Constant folding for literal ** operands stays in PythonToLaurel. To move it to concreteEval, we'd need a mechanism to prevent specific prelude functions from being translated to Core.

[MikaelMayer]

Moved int_pow to factory concreteEval following the regex pattern. Forward-declared before CoreOnlyDelimiter (like re_fullmatch_str) so it doesn't enter the Core program. Factory provides it with concreteEval. Removed constant folding from PythonToLaurel and the ProgramEval hack.

[joehendrix]

I added a couple comments, but don't consider them blocking.