reify-reflect 0.1.1

//! # Full Roundtrip: Type-Level → Value → Type-Level → Value
//!
//! This example demonstrates the complete reify-reflect ecosystem:
//!
//! 1. **Reflect** (type → value): Peano naturals and derived structs produce runtime values
//! 2. **Reify** (value → scoped context): Branded lifetime token for safe scoped access
//! 3. **Reify to const generic** (value → type): `#[reifiable]` dispatches runtime values
//!    into const-generic contexts where the compiler knows N
//! 4. **Full roundtrip**: Start at the type level, go to values, go back to type level,
//!    compute, and return a value
//!
//! Run with: `cargo run --example roundtrip --features const-reify`

use reflect_nat::{N3, N5, S, Z};
use reify_reflect_core::{reify, Reflect, RuntimeValue};

// ============================================================================
// Part 1: Type-Level → Value (Reflect)
// ============================================================================

fn part1_reflect() {
    println!("=== Part 1: Type-Level → Value (Reflect) ===\n");

    // Type-level naturals reflect to runtime values
    type Three = S<S<S<Z>>>;
    type Five = N5;

    println!("  Three::reflect() = {:?}", Three::reflect());
    println!("  Five::reflect()  = {:?}", Five::reflect());

    // Derived structs reflect their fields
    #[derive(reflect_derive::Reflect)]
    #[allow(dead_code)]
    struct Config {
        width: N3,
        height: N5,
    }

    let config = Config::reflect();
    println!("  Config::reflect() = {:?}", config);
    println!();
}

// ============================================================================
// Part 2: Value → Scoped Context (reify with branded lifetime)
// ============================================================================

fn part2_reify_branded() {
    println!("=== Part 2: Value → Scoped Context (branded reify) ===\n");

    // reify takes a runtime value and gives you a branded token
    // that can't escape the closure
    let val = 42i32;
    let result = reify(&val, |token| {
        let v: &i32 = token.reflect();
        println!("  Inside reify: token.reflect() = {}", v);
        v * 2
    });
    println!("  Result from reify: {}", result);

    // Nested reify — two branded tokens, both accessible
    let sum = reify(&10i32, |a| {
        reify(&20i32, |b| {
            let result = a.reflect() + b.reflect();
            println!(
                "  Nested reify: {} + {} = {}",
                a.reflect(),
                b.reflect(),
                result
            );
            result
        })
    });
    println!("  Nested result: {}", sum);

    // Reify a reflected value — connecting the two directions
    let reflected = N5::reflect(); // RuntimeValue::Nat(5)
    reify(&reflected, |token| {
        println!("  Reified a reflected value: {:?}", token.reflect());
    });
    println!();
}

// ============================================================================
// Part 3: Value → Const Generic (true type-level dispatch)
// ============================================================================

// The #[reifiable] macro generates dispatch functions automatically.
// This trait has const-generic methods — the macro generates reify_* functions
// that dispatch a runtime u64 into a const-generic context.
#[const_reify_derive::reifiable(range = 0..=255)]
trait ModularArith {
    /// Compute base^exp mod N, where N is a const generic
    fn pow_mod<const N: u64>(&self, base: u64, exp: u64) -> u64;

    /// Check if a value is a quadratic residue mod N
    fn is_qr<const N: u64>(&self, a: u64) -> bool;
}

struct ModArithImpl;

impl ModularArith for ModArithImpl {
    fn pow_mod<const N: u64>(&self, base: u64, exp: u64) -> u64 {
        if N == 0 {
            return 0;
        }
        let mut result = 1u64;
        let mut b = base % N;
        let mut e = exp;
        while e > 0 {
            if e % 2 == 1 {
                result = result * b % N;
            }
            b = b * b % N;
            e /= 2;
        }
        result
    }

    fn is_qr<const N: u64>(&self, a: u64) -> bool {
        if N <= 1 {
            return true;
        }
        // Euler's criterion: a is a QR mod p iff a^((p-1)/2) ≡ 1 (mod p)
        self.pow_mod::<N>(a, (N - 1) / 2) == 1
    }
}

fn part3_reify_const_generic() {
    println!("=== Part 3: Value → Const Generic (#[reifiable]) ===\n");

    let impl_ = ModArithImpl;

    // The modulus is a RUNTIME value, but inside the dispatch,
    // N is a fully known const generic
    let modulus = 7u64;

    // reify_pow_mod was auto-generated by the #[reifiable] macro
    let result = reify_pow_mod(modulus, &impl_, 3, 5);
    println!("  3^5 mod 7 = {} (expected {})", result, 243u64 % 7);

    // Fermat's little theorem: a^(p-1) ≡ 1 (mod p)
    let fermat = reify_pow_mod(modulus, &impl_, 3, 6);
    println!("  3^6 mod 7 = {} (Fermat's little theorem)", fermat);

    // Quadratic residues mod 7
    println!("  Quadratic residues mod 7:");
    for a in 1..7u64 {
        let is_qr = reify_is_qr(modulus, &impl_, a);
        println!("    {} is QR mod 7: {}", a, is_qr);
    }

    // Change modulus at runtime — different dispatch, same code
    let modulus = 13u64;
    let result = reify_pow_mod(modulus, &impl_, 2, 12);
    println!("  2^12 mod 13 = {} (Fermat)", result);
    println!();
}

// ============================================================================
// Part 4: Full Roundtrip — Type → Value → Type → Value
// ============================================================================

// Use the closure-based ergonomic API for simple cases
fn part4_full_roundtrip() {
    println!("=== Part 4: Full Roundtrip ===\n");

    // Step 1: Start at the type level
    type Base = S<S<S<Z>>>; // 3
    type Exponent = N5; // 5

    // Step 2: Reflect to runtime values
    let base_val = match Base::reflect() {
        RuntimeValue::Nat(n) => n,
        _ => unreachable!(),
    };
    let exp_val = match Exponent::reflect() {
        RuntimeValue::Nat(n) => n,
        _ => unreachable!(),
    };
    println!("  Type-level: Base=3, Exponent=5");
    println!("  Reflected:  base={}, exp={}", base_val, exp_val);

    // Step 3: Get a modulus from "user input" (runtime)
    let modulus = 7u64;
    println!("  Runtime modulus: {}", modulus);

    // Step 4: Reify the modulus into a const-generic context and compute
    let result = reify_pow_mod(modulus, &ModArithImpl, base_val, exp_val);
    println!(
        "  Reified computation: {}^{} mod {} = {}",
        base_val, exp_val, modulus, result
    );

    // Step 5: We can also use the NatCallback trait directly for full const-generic power
    use const_reify::nat_reify::{reify_nat, NatCallback};

    struct FermatTest {
        base: u64,
    }

    impl NatCallback<bool> for FermatTest {
        fn call<const P: u64>(&self) -> bool {
            if P <= 1 {
                return false;
            }
            // Inside here, P is a const generic.
            // We could construct [u8; P], Mod<P>, etc.
            // For now, test Fermat's little theorem.
            let mut result = 1u64;
            let mut b = self.base % P;
            let mut e = P - 1;
            while e > 0 {
                if e % 2 == 1 {
                    result = result * b % P;
                }
                b = b * b % P;
                e /= 2;
            }
            result == 1
        }
    }

    // Test primality hint via Fermat for several primes reflected from the type level
    println!("\n  Fermat test with type-level base:");
    for &p in &[7u64, 11, 13, 17, 23] {
        let passes = reify_nat(p, &FermatTest { base: base_val });
        println!("    {}^({}-1) ≡ 1 (mod {})? {}", base_val, p, p, passes);
    }

    // Step 6: Use the branded reify for scoped value access
    let final_result = reify(&result, |token| {
        let v = token.reflect();
        println!("\n  Branded reify of result: {}", v);
        format!("{}^{} mod {} = {}", base_val, exp_val, modulus, v)
    });

    println!("  Final: {}", final_result);
    println!();
}

// ============================================================================
// Part 5: The def_nat_callback! macro for quick one-offs
// ============================================================================

fn part5_macro_ergonomics() {
    println!("=== Part 5: Macro Ergonomics ===\n");

    use const_reify::nat_reify::{reify_nat, reify_nat2_fn, reify_nat_fn};

    // Closure-based (simplest, no const generic access)
    let squared = reify_nat_fn(12, |n| n * n);
    println!("  reify_nat_fn(12, |n| n * n) = {}", squared);

    // Two-value closure
    let sum = reify_nat2_fn(100, 55, |a, b| a + b);
    println!("  reify_nat2_fn(100, 55, |a, b| a + b) = {}", sum);

    // def_nat_callback! macro for const-generic access without manual struct
    const_reify::def_nat_callback!(Factorial -> u64 {
        let mut result = 1u64;
        let mut i = 1u64;
        while i <= N {
            result *= i;
            i += 1;
        }
        result
    });

    let fact5 = reify_nat(5, &Factorial);
    let fact10 = reify_nat(10, &Factorial);
    println!("  5!  = {}", fact5);
    println!("  10! = {}", fact10);

    println!();
}

fn main() {
    part1_reflect();
    part2_reify_branded();
    part3_reify_const_generic();
    part4_full_roundtrip();
    part5_macro_ergonomics();

    println!("=== Summary ===");
    println!("  Reflect:         type-level → runtime value");
    println!("  reify (branded): runtime value → scoped token (borrow-checker enforced)");
    println!("  reify_nat:       runtime u64 → const generic N (true type-level dispatch)");
    println!("  #[reifiable]:    auto-generate dispatch for any trait with const-generic methods");
    println!("  Full roundtrip:  S<S<S<Z>>> → 3 → reify_nat(modulus, ...) → compute → result");
}