use std::quantum::{qalloc, qfree, hadamard, cnot, measure};

fn create_bell_pair() -> [2] Qubit {
    let q0 = qalloc();
    let q1 = qalloc();
    hadamard(inout q0);
    cnot(inout q0, inout q1);
    [q0, q1] // Return tuple of linear qubits
}

fn measure_bell(inout pair: [2] Qubit) -> [2] Cbit {
    let [q0, q1] = pair; // Destructure
    [measure(inout q0), measure(inout q1)]
}

fn ghz_state(n: usize) -> [N] Qubit
where [N] = [n] {
    let mut reg = QReg::new(n); // [1] QReg[N]
    hadamard(inout reg[0]);
    for i in 1..n {
        cnot(inout reg[0], inout reg[i]);
    }
    reg.into_array() // [1] QubitArray[N]
}

fn teleport(inout psi: [1] Qubit, inout alice: [1] Qubit, inout bob: [1] Qubit) 
    -> ([1] Cbit, [1] Cbit, [1] Qubit) {
    
    // Create Bell pair between Alice and Bob
    hadamard(inout alice);
    cnot(inout alice, inout bob);
    
    // Bell measurement on psi and Alice's qubit
    cnot(inout psi, inout alice);
    hadamard(inout psi);
    let m1 = measure(inout psi);    // Consumes psi
    let m2 = measure(inout alice);  // Consumes alice
    
    // Conditional corrections on Bob's qubit (classical control)
    // In QASM: if (m1) x bob; if (m2) z bob;
    // Here modeled as proof obligation:
    // m1=true → apply X to bob; m2=true → apply Z to bob
    
    (m1, m2, bob) // Return classical bits and Bob's qubit
}

use std::poly::{domain, tile, parallel, vectorize, Schedule};

fn build_schedule() -> Schedule {
    let dom = domain(&[0..N, 0..M, 0..P]);
    
    // Tile for L1 cache (32x32 tiles)
    let tiled = tile(dom, &[32, 32, 1]);
    
    // Parallelize outer tile loops
    let par = parallel(tiled);
    
    // Vectorize innermost loop (AVX-512: width=8 for f64)
    let vec = vectorize(par, 8);
    
    Schedule::from_domain(vec)
}

use std::poly::{domain, tile, parallel, vectorize, Schedule};

fn matmul_tiled(A: [N][M] f64, B: [M][P] f64) -> [N][P] f64 {
    // Compiler uses this schedule for code generation
    #[schedule(build_schedule())]
    fn matmul_kernel(A: [N][M] f64, B: [M][P] f64) -> [N][P] f64 {
        let C = [[0.0; P]; N];
        for i in 0..N {
            for j in 0..P {
                for k in 0..M {
                    C[i][j] += A[i][k] * B[k][j];
                }
            }
        }
        C
    }
    matmul_kernel(A, B)
}

use std::poly::{domain, skew, parallel, Schedule};

fn stencil_3d_schedule() -> Schedule {
    let dom = domain(&[1..N-1, 1..M-1, 1..O-1]);
    
    // Skew i-j plane for wavefront parallelism
    let skewed = skew(dom, 1); // factor=1 for i+j = constant
    
    // Parallelize skewed dimension
    let par = parallel(skewed);
    
    Schedule::from_domain(par)
}

enum CheckResult {
    Sat,      // Constraints satisfiable
    Unsat,    // Constraints unsatisfiable
    Unknown,  // Solver cannot determine (timeout/incomplete)
}

use std::smt::{new_solver, assert, check, expr_from, Sort};

fn safe_get(arr: [*] [N] f64, idx: usize) -> f64 {
    let mut solver = new_solver();
    let idx_e = expr_from(idx);
    let n_e = expr_from(N);
    
    // Prove 0 <= idx < N
    assert(&mut solver, idx_e >= expr_from(0));
    assert(&mut solver, idx_e < n_e);
    
    match check(&solver) {
        CheckResult::Sat => {
            // Bounds proven at compile time — no runtime check needed
            arr[idx]
        }
        CheckResult::Unsat => {
            compile_error!("Index out of bounds: solver proved idx >= N");
        }
        CheckResult::Unknown => {
            // Fallback: insert runtime check
            if idx < N { arr[idx] } else { panic!("Index out of bounds") }
        }
    }
}

use std::smt::{new_solver, assert, check, declare_const, Sort, expr_from};

fn verify_invariant(x: i32, y: i32) -> [0] Proof {
    let mut solver = new_solver();
    
    // Declare symbolic versions
    let x_s = declare_const(&mut solver, "x", Sort::Int);
    let y_s = declare_const(&mut solver, "y", Sort::Int);
    
    // Precondition: x > 0 && y > 0
    assert(&mut solver, x_s > expr_from(0));
    assert(&mut solver, y_s > expr_from(0));
    
    // Operation: z = x + y
    let z_s = x_s + y_s;
    
    // Postcondition: z > x && z > y
    assert(&mut solver, z_s > x_s);
    assert(&mut solver, z_s > y_s);
    
    // This will be checked at compile time
    match check(&solver) {
        CheckResult::Sat => (), // Proven
        CheckResult::Unsat => compile_error!("Invariant violated"),
        CheckResult::Unknown => compile_error!("Verification incomplete"),
    }
}

use std::smt::{new_solver, assert, check, declare_const, Sort, expr_from};

fn verify_overflow(a: u32, b: u32) -> [0] Proof {
    let mut solver = new_solver();
    let a_s = declare_const(&mut solver, "a", Sort::BitVec(32));
    let b_s = declare_const(&mut solver, "b", Sort::BitVec(32));
    
    // Check if a + b overflows (unsigned)
    let sum = a_s.bvadd(b_s);
    let overflow = sum.bvult(a_s); // sum < a iff overflow
    
    assert(&mut solver, overflow);
    
    // If SAT, there exist inputs causing overflow
    match check(&solver) {
        CheckResult::Sat => {
            compile_warn!("Potential unsigned overflow detected");
        }
        CheckResult::Unsat => {
            // Proven no overflow for any inputs
        }
        CheckResult::Unknown => {}
    }
}

use std::mem::{alloc, dealloc, LinearBox};

fn process_data(data: [1] LinearBox<[N] f64>) -> [1] LinearBox<[N] f64> {
    // Exclusive mutable access to buffer
    let mut buf = data; // Move ownership
    
    for i in 0..N {
        buf[i] = buf[i] * 2.0; // In-place mutation
    }
    
    buf // Return ownership
}

fn main() {
    let boxed = alloc([0.0; 1024]); // [1] LinearBox<[1024] f64>
    let result = process_data(boxed); // boxed moved, result returned
    dealloc(result); // Explicit deallocation (consumes result)
}

use std::io::{println, serialize, deserialize};

#[derive(Serialize, Deserialize)]
struct KernelConfig {
    grid_size: usize,
    block_size: usize,
    precision: Precision,
}

fn launch_kernel(config: KernelConfig) {
    let bytes = serialize(&config);
    // Send to device driver...
    println!("Launching kernel: {:?}", config);
}

use std::math::fft;

fn frequency_analysis(signal: [1024] f64) -> [1024] f64 {
    // Convert to complex
    let mut complex: [1024] Complex = [Complex::new(0.0, 0.0); 1024];
    for i in 0..1024 {
        complex[i] = Complex::new(signal[i], 0.0);
    }
    
    // FFT with automatic polyhedral scheduling
    let spectrum = fft(complex);
    
    // Compute magnitude spectrum
    let mut mag: [1024] f64 = [0.0; 1024];
    for i in 0..1024 {
        mag[i] = spectrum[i].re * spectrum[i].re + spectrum[i].im * spectrum[i].im;
    }
    mag
}

// Quantities
[0], [1], [*], [N]

// Core types
bool, int, f64, f32, u8..u64, i8..i64, usize, isize
Vec<T>, Option<T>, Result<T, E>

// Quantum
Qubit, QReg, qalloc, qfree, hadamard, cnot, measure

// Memory
LinearBox, LinearVec, alloc, dealloc

// SMT
Solver, Expr, Sort, Model, new_solver, assert, check