Research-Stack/fix_offloat.py

#!/usr/bin/env python3
"""
Eliminate ofFloat calls from compute-path Lean code.

Strategy:
- Integer values like 100.0 → ofNat 100
- Simple rationals like 0.5 → ofRatio 1 2, 0.1 → ofRatio 1 10
- Complex values → ofRawInt with exact Q16.16 raw value
- Comments/docstrings are left alone

Usage: python3 fix_offloat.py [--dry-run] [files...]
"""

import re
import sys
import os
from pathlib import Path

SEMANTICS = Path("/home/allaun/Research Stack/0-Core-Formalism/lean/Semantics")

# Scale constants
Q16_SCALE = 65536
Q0_16_SCALE = 32767

def q16_raw(f: float) -> int:
    """Compute Q16.16 raw value matching Lean's Q16_16.ofFloat (floor semantics)."""
    if f >= 32768.0 or f <= -32768.0:
        return None
    return int(f * Q16_SCALE)

def q0_16_raw(f: float) -> int:
    """Compute Q0.16 raw value matching Lean's Q0_16.ofFloat (round semantics)."""
    return int(round(f * Q0_16_SCALE))


def replacement(line: str) -> str:
    """Replace ofFloat calls in a line of code. Returns modified line or original."""
    # Skip comment-only lines
    stripped = line.strip()
    if stripped.startswith("--") or stripped.startswith("/-"):
        return line
    # Block comment continuation
    if stripped.startswith(" *") or stripped.startswith("/*"):
        return line
    # Don't touch lines that define ofFloat itself
    if "def ofFloat" in line or "def toFloat" in line:
        return line

    # Patterns: <prefix>.ofFloat <float_literal> or bare ofFloat (in FixedPoint namespace)
    # Parenthesized numbers for negative literals like (-1.2); no partial expression matches
    ofloat_re = r'(?:(Q16_16|Q0_16|Q0_64)\.ofFloat|(?<![.\w])ofFloat)\s+(?:\(([-+]?\d+\.?\d*(?:[eE][-+]?\d+)?)\)|([-+]?\d+\.?\d*(?:[eE][-+]?\d+)?))'

    def replacer(m):
        type_prefix = m.group(1)  # "Q16_16", "Q0_16", "Q0_64", or None
        float_str = m.group(2) or m.group(3)  # number in parens, or bare number
        f = float(float_str)

        # Determine the type prefix for the replacement
        if type_prefix:
            t = type_prefix  # e.g. "Q16_16"
        else:
            t = "Q16_16"  # bare ofFloat → default to Q16_16

        if t == "Q0_16":
            if f >= 1.0:
                return "Q0_16.one"
            elif f <= -1.0:
                return "Q0_16.neg Q0_16.one"
            elif f == 0.0:
                return "Q0_16.zero"
            elif f == 0.5:
                return "Q0_16.half"
            else:
                raw = q0_16_raw(f)
                return f"Q0_16.ofRawInt {raw}"

        elif t == "Q0_64":
            if f >= 1.0:
                return "Q0_64.one"
            elif f <= -1.0:
                return "Q0_64.neg Q0_64.one"
            elif f == 0.0:
                return "Q0_64.zero"
            elif f == 0.5:
                return "Q0_64.half"
            else:
                return line  # skip for now

        else:  # Q16_16 or bare ofFloat
            # Integer values
            if f == int(f):
                n = int(f)
                if n == 0:
                    return f"{t}.zero"
                elif n == 1:
                    return f"{t}.one"
                elif n == -1:
                    return f"{t}.negOne"
                elif n == 2:
                    return f"{t}.two"
                elif n > 0:
                    return f"{t}.ofNat {n}"
                else:
                    return f"{t}.neg ({t}.ofNat {-n})"

            # Simple rationals
            frac_map = {
                0.5: (1, 2), 0.25: (1, 4), 0.75: (3, 4),
                0.125: (1, 8), 0.375: (3, 8), 0.625: (5, 8), 0.875: (7, 8),
                0.1: (1, 10), 0.2: (1, 5), 0.3: (3, 10),
                0.4: (2, 5), 0.6: (3, 5), 0.7: (7, 10),
                0.8: (4, 5), 0.9: (9, 10),
                0.05: (1, 20), 0.15: (3, 20), 0.35: (7, 20),
                0.45: (9, 20), 0.55: (11, 20), 0.65: (13, 20),
                0.85: (17, 20), 0.95: (19, 20),
                0.01: (1, 100), 0.02: (1, 50), 0.03: (3, 100),
                0.04: (1, 25), 0.06: (3, 50), 0.07: (7, 100),
                0.08: (2, 25), 0.09: (9, 100),
            }
            for val, (num, den) in frac_map.items():
                if abs(f - val) < 1e-10:
                    return f"{t}.ofRatio {num} {den}"

            # Complex value: use ofRawInt with exact Q16.16 raw = floor(f * 65536)
            raw = q16_raw(f)
            if raw is not None:
                return f"{t}.ofRawInt 0x{raw & 0xFFFFFFFF:08X}"

            return line  # fallback

    return re.sub(ofloat_re, replacer, line)


def fix_file(filepath: Path, dry_run: bool = False) -> tuple:
    if not filepath.exists():
        return (str(filepath), 0, 0, [])

    with open(filepath, 'r') as f:
        content = f.read()

    original_count = content.count("ofFloat")
    if original_count == 0:
        return (str(filepath), 0, 0, [])

    # Count only non-comment ofFloat occurrences for the "target" count
    lines = content.split('\n')
    changed_lines = []
    change_count = 0

    for i, line in enumerate(lines):
        if "ofFloat" not in line:
            continue
        new_line = replacement(line)
        if new_line != line:
            change_count += 1
            changed_lines.append((i+1, line, new_line))
        lines[i] = new_line

    if not dry_run and change_count > 0:
        new_content = '\n'.join(lines)
        with open(filepath, 'w') as f:
            f.write(new_content)

    return (str(filepath), change_count, original_count, changed_lines)


def main():
    dry_run = '--dry-run' in sys.argv

    target_files = [
        "Semantics/QFactor.lean",
        "Semantics/SubagentOrchestrator.lean",
        "Semantics/TopologyGoldenSpiral.lean",
        "Semantics/UnitConversion.lean",
        "Semantics/DynamicCanal.lean",
        "Semantics/GeneticGroundUp.lean",
        "Semantics/Geometry/ImplicitShellLattice.lean",
        "Semantics/TopologyDlessScalar.lean",
        "Semantics/TopologyFractalEncoding.lean",
        "Semantics/Hardware/LaserPathCell.lean",
        "Semantics/HumanNeuralCompression.lean",
        "Semantics/F01_Q16_16_FixedPoint.lean",
        "Semantics/MOFCO2Reduction.lean",
        "Semantics/DeltaGCLCompression.lean",
        "Semantics/TopologicalAwareness.lean",
        "Semantics/BrainBoxDescriptor.lean",
    ]

    total_changed = 0
    total_original = 0

    for relpath in target_files:
        filepath = SEMANTICS / relpath
        if not filepath.exists():
            print(f"SKIP  {relpath} (not found)")
            continue

        r = fix_file(filepath, dry_run)
        rel, changed, original, details = r
        rel_short = os.path.relpath(rel, str(SEMANTICS))
        total_changed += changed
        total_original += original

        action = "DRY-RUN" if dry_run else "FIXED"
        print(f"{action:>8} {rel_short}: {changed}/{original} ofFloat calls replaced")

        if dry_run and changed > 0:
            for lineno, old, new in details:
                def shorten(s, maxlen=80):
                    s = s.rstrip()
                    if len(s) > maxlen:
                        return s[:maxlen-3] + "..."
                    return s
                print(f"  L{lineno}: {shorten(old)}")
                print(f"      \u2192 {shorten(new)}")
                print()

    print(f"\n{'DRY-RUN' if dry_run else 'COMPLETE'}: {total_changed}/{total_original} total ofFloat calls replaced")


if __name__ == "__main__":
    main()