use crate::mir::join_ir::lowering::inline_boundary::JoinInlineBoundary;
use crate::mir::ValueId;
use std::collections::BTreeMap;

#[cfg(debug_assertions)]
use super::LoopHeaderPhiInfo;
#[cfg(debug_assertions)]
use crate::mir::join_ir::lowering::join_value_space::{LOCAL_MAX, PARAM_MAX, PARAM_MIN};
#[cfg(debug_assertions)]
use crate::mir::{BasicBlockId, MirFunction, MirInstruction};
#[cfg(debug_assertions)]
use std::collections::HashMap;

/// Phase 118 P2: Contract check (Fail-Fast) - exit_bindings carriers must have exit PHI dsts.
///
/// This prevents latent "Carrier '<name>' not found in carrier_phis" failures later in
/// ExprResultResolver and ExitLine reconnection.
pub(super) fn verify_exit_bindings_have_exit_phis(
    boundary: &JoinInlineBoundary,
    exit_carrier_phis: &BTreeMap<String, ValueId>,
) -> Result<(), String> {
    use crate::mir::join_ir::lowering::carrier_info::CarrierRole;
    use crate::mir::join_ir::lowering::error_tags;

    for binding in &boundary.exit_bindings {
        if binding.role == CarrierRole::ConditionOnly {
            continue;
        }
        if exit_carrier_phis.contains_key(&binding.carrier_name) {
            continue;
        }

        return Err(error_tags::freeze_with_hint(
            "phase118/exit_phi/missing_carrier_phi",
            &format!(
                "exit_bindings carrier '{}' is missing from exit_carrier_phis",
                binding.carrier_name
            ),
            "exit_bindings carriers must be included in exit_phi_builder inputs; check carrier_inputs derivation from jump_args",
        ));
    }

    Ok(())
}

#[cfg(debug_assertions)]
pub(super) fn verify_loop_header_phis(
    func: &MirFunction,
    header_block: BasicBlockId,
    loop_info: &LoopHeaderPhiInfo,
    boundary: &JoinInlineBoundary,
) {
    if let Some(ref loop_var_name) = boundary.loop_var_name {
        let header_block_data = func.blocks.get(&header_block).unwrap_or_else(|| {
            panic!(
                "[JoinIRVerifier] Header block {} not found ({} blocks in func)",
                header_block,
                func.blocks.len()
            )
        });
        let has_loop_var_phi = header_block_data
            .instructions
            .iter()
            .any(|instr| matches!(instr, MirInstruction::Phi { .. }));

        if !has_loop_var_phi && !loop_info.carrier_phis.is_empty() {
            panic!(
                "[JoinIRVerifier] Loop variable '{}' in boundary but no PHI in header block {} (has {} carrier PHIs)",
                loop_var_name, header_block.0, loop_info.carrier_phis.len()
            );
        }
    }

    if !loop_info.carrier_phis.is_empty() {
        let header_block_data = func.blocks.get(&header_block).unwrap_or_else(|| {
            panic!(
                "[JoinIRVerifier] Header block {} not found ({} blocks in func)",
                header_block,
                func.blocks.len()
            )
        });
        let phi_count = header_block_data
            .instructions
            .iter()
            .filter(|instr| matches!(instr, MirInstruction::Phi { .. }))
            .count();

        if phi_count == 0 {
            panic!(
                "[JoinIRVerifier] LoopHeaderPhiInfo has {} PHIs but header block {} has none",
                loop_info.carrier_phis.len(),
                header_block.0
            );
        }

        for (carrier_name, entry) in &loop_info.carrier_phis {
            let phi_exists = header_block_data.instructions.iter().any(|instr| {
                if let MirInstruction::Phi { dst, .. } = instr {
                    *dst == entry.phi_dst
                } else {
                    false
                }
            });

            if !phi_exists {
                panic!(
                    "[JoinIRVerifier] Carrier '{}' has PHI dst {:?} but PHI not found in header block {}",
                    carrier_name, entry.phi_dst, header_block.0
                );
            }
        }
    }
}

#[cfg(debug_assertions)]
pub(super) fn verify_exit_line(
    func: &MirFunction,
    exit_block: BasicBlockId,
    boundary: &JoinInlineBoundary,
) {
    if !func.blocks.contains_key(&exit_block) {
        panic!(
            "[JoinIRVerifier] Exit block {} out of range (func has {} blocks)",
            exit_block.0,
            func.blocks.len()
        );
    }

    if !boundary.exit_bindings.is_empty() {
        for binding in &boundary.exit_bindings {
            if binding.host_slot.0 >= 1_000_000 {
                panic!(
                    "[JoinIRVerifier] Exit binding '{}' has suspiciously large host_slot {:?}",
                    binding.carrier_name, binding.host_slot
                );
            }
        }
    }

    // Phase 132-P2: Verify exit PHI ValueIds don't collide with other instructions
    verify_exit_phi_no_collision(func, exit_block);
}

/// Phase 132-P2: Verify exit PHI dst ValueIds don't collide with other instructions
///
/// # Problem
///
/// If exit_phi_builder uses builder.value_gen.next() (module-level) instead of
/// func.next_value_id() (function-level), it can allocate ValueIds that collide
/// with existing instructions in the function.
///
/// Example collision:
/// - bb0: %1 = const 0   (counter init)
/// - bb3: %1 = phi ...   (exit PHI - collision!)
///
/// This causes LLVM backend errors:
/// "Cannot overwrite PHI dst=1. ValueId namespace collision detected."
///
/// # Contract
///
/// All exit PHI dst ValueIds must be unique within the function and not
/// overwrite any existing instruction dst.
///
/// # Panics
///
/// Panics if any exit PHI dst collides with an existing instruction dst.
#[cfg(debug_assertions)]
fn verify_exit_phi_no_collision(func: &MirFunction, exit_block: BasicBlockId) {
    let exit_block_data = match func.blocks.get(&exit_block) {
        Some(block) => block,
        None => return, // Block not found, other verification will catch this
    };

    // Collect all exit PHI dsts
    let mut exit_phi_dsts = std::collections::HashSet::new();
    for instr in &exit_block_data.instructions {
        if let MirInstruction::Phi { dst, .. } = instr {
            exit_phi_dsts.insert(*dst);
        }
    }

    if exit_phi_dsts.is_empty() {
        return; // No exit PHIs, nothing to verify
    }

    // Collect all instruction dsts in the entire function (excluding PHIs)
    let mut all_non_phi_dsts = std::collections::HashSet::new();
    for (block_id, block) in &func.blocks {
        if *block_id == exit_block {
            // For exit block, only check non-PHI instructions
            for instr in &block.instructions {
                if !matches!(instr, MirInstruction::Phi { .. }) {
                    if let Some(dst) = get_instruction_dst(instr) {
                        all_non_phi_dsts.insert(dst);
                    }
                }
            }
        } else {
            // For other blocks, check all instructions
            for instr in &block.instructions {
                if let Some(dst) = get_instruction_dst(instr) {
                    all_non_phi_dsts.insert(dst);
                }
            }
        }
    }

    // Check for collisions
    for phi_dst in &exit_phi_dsts {
        if all_non_phi_dsts.contains(phi_dst) {
            // Find which instruction collides
            for (block_id, block) in &func.blocks {
                for instr in &block.instructions {
                    if matches!(instr, MirInstruction::Phi { .. }) && *block_id == exit_block {
                        continue; // Skip exit PHIs themselves
                    }
                    if let Some(dst) = get_instruction_dst(instr) {
                        if dst == *phi_dst {
                            panic!(
                                "[JoinIRVerifier/Phase132-P2] Exit PHI dst {:?} collides with instruction in block {}: {:?}\n\
                                 This indicates exit_phi_builder used module-level value_gen.next() instead of function-level next_value_id().\n\
                                 Fix: Use func.next_value_id() in exit_phi_builder.rs",
                                phi_dst, block_id.0, instr
                            );
                        }
                    }
                }
            }
        }
    }
}

/// Helper: Extract dst ValueId from MirInstruction
#[cfg(debug_assertions)]
fn get_instruction_dst(instr: &MirInstruction) -> Option<ValueId> {
    use MirInstruction;
    match instr {
        MirInstruction::Const { dst, .. }
        | MirInstruction::Load { dst, .. }
        | MirInstruction::UnaryOp { dst, .. }
        | MirInstruction::BinOp { dst, .. }
        | MirInstruction::Compare { dst, .. }
        | MirInstruction::TypeOp { dst, .. }
        | MirInstruction::NewBox { dst, .. }
        | MirInstruction::NewClosure { dst, .. }
        | MirInstruction::Copy { dst, .. }
        | MirInstruction::Cast { dst, .. }
        | MirInstruction::TypeCheck { dst, .. }
        | MirInstruction::Phi { dst, .. }
        | MirInstruction::ArrayGet { dst, .. }
        | MirInstruction::RefNew { dst, .. }
        | MirInstruction::RefGet { dst, .. }
        | MirInstruction::WeakNew { dst, .. }
        | MirInstruction::WeakLoad { dst, .. }
        | MirInstruction::WeakRef { dst, .. }
        | MirInstruction::FutureNew { dst, .. }
        | MirInstruction::Await { dst, .. } => Some(*dst),
        MirInstruction::BoxCall { dst, .. }
        | MirInstruction::ExternCall { dst, .. }
        | MirInstruction::Call { dst, .. }
        | MirInstruction::PluginInvoke { dst, .. } => *dst,
        _ => None,
    }
}

#[cfg(debug_assertions)]
pub(super) fn verify_valueid_regions(loop_info: &LoopHeaderPhiInfo, boundary: &JoinInlineBoundary) {
    fn region_name(id: ValueId) -> &'static str {
        if id.0 < PARAM_MIN {
            "PHI Reserved"
        } else if id.0 <= PARAM_MAX {
            "Param"
        } else if id.0 <= LOCAL_MAX {
            "Local"
        } else {
            "Invalid (> LOCAL_MAX)"
        }
    }

    for join_id in &boundary.join_inputs {
        if !(PARAM_MIN..=PARAM_MAX).contains(&join_id.0) {
            panic!(
                "[JoinIRVerifier] join_input {:?} not in Param region ({})",
                join_id,
                region_name(*join_id)
            );
        }
    }

    for (_, entry) in &loop_info.carrier_phis {
        if entry.phi_dst.0 > LOCAL_MAX {
            panic!(
                "[JoinIRVerifier] Carrier PHI dst {:?} outside Local region ({})",
                entry.phi_dst,
                region_name(entry.phi_dst)
            );
        }
    }

    for binding in &boundary.condition_bindings {
        if !(PARAM_MIN..=PARAM_MAX).contains(&binding.join_value.0) {
            panic!(
                "[JoinIRVerifier] Condition binding '{}' join_value {:?} not in Param region ({})",
                binding.name,
                binding.join_value,
                region_name(binding.join_value)
            );
        }
    }

    for binding in &boundary.exit_bindings {
        if !(PARAM_MIN..=PARAM_MAX).contains(&binding.join_exit_value.0) {
            panic!(
                "[JoinIRVerifier] Exit binding '{}' join_exit_value {:?} not in Param region ({})",
                binding.carrier_name,
                binding.join_exit_value,
                region_name(binding.join_exit_value)
            );
        }
    }
}

/// Phase 135 P1 Step 1: Verify condition_bindings consistency (alias allowed, conflict fails)
///
/// # Contract
///
/// condition_bindings can have multiple names (aliases) pointing to the same join_value,
/// but if the same join_value appears with different host_value, it's a contract violation.
///
/// This catches merge-time inconsistencies before BoundaryInjector tries to inject Copy
/// instructions, preventing MIR SSA breakage.
///
/// # Example Valid (alias):
/// ```text
/// condition_bindings: [
///   { name: "is_char_match", join_value: ValueId(104), host_value: ValueId(12) },
///   { name: "char", join_value: ValueId(104), host_value: ValueId(12) }  // Same host_value - OK
/// ]
/// ```
///
/// # Example Invalid (conflict):
/// ```text
/// condition_bindings: [
///   { name: "is_char_match", join_value: ValueId(104), host_value: ValueId(12) },
///   { name: "char", join_value: ValueId(104), host_value: ValueId(18) }  // Different host_value - FAIL
/// ]
/// ```
///
/// # Panics
///
/// Panics if the same join_value has conflicting host_value mappings.
#[cfg(debug_assertions)]
pub(super) fn verify_condition_bindings_consistent(boundary: &JoinInlineBoundary) {
    let mut join_to_host: HashMap<ValueId, ValueId> = HashMap::new();

    for binding in &boundary.condition_bindings {
        if let Some(&existing_host) = join_to_host.get(&binding.join_value) {
            if existing_host != binding.host_value {
                panic!(
                    "[JoinIRVerifier/Phase135-P1] condition_bindings conflict: join_value {:?} mapped to both {:?} and {:?}\n\
                     Binding names with conflict: check all bindings with join_value={:?}\n\
                     Contract: Same join_value can have multiple names (alias) but must have same host_value.\n\
                     Fix: Ensure ConditionLoweringBox uses SSOT allocator (ConditionContext.alloc_value).",
                    binding.join_value, existing_host, binding.host_value, binding.join_value
                );
            }
        } else {
            join_to_host.insert(binding.join_value, binding.host_value);
        }
    }
}

/// Phase 135 P1 Step 2: Verify header PHI dsts are not redefined by non-PHI instructions
///
/// # Contract
///
/// Loop header PHI dst ValueIds must not be reused as dst in non-PHI instructions.
/// This prevents "PHI dst overwrite" where a Copy/BinOp/etc. instruction redefines
/// the PHI result, breaking MIR SSA.
///
/// # Example Invalid:
/// ```text
/// bb3 (header):
///   %14 = phi [%2, bb1], [%28, bb8]  // Header PHI
///   %16 = copy %0
///   %14 = call %16.length()          // INVALID: Redefines PHI dst %14
/// ```
///
/// This typically happens when:
/// - ConditionLoweringBox bypasses SSOT allocator and reuses PHI dst ValueIds
/// - JoinIR merge incorrectly remaps values to PHI dst range
///
/// # Panics
///
/// Panics if any header PHI dst is redefined by a non-PHI instruction in the function.
#[cfg(debug_assertions)]
pub(super) fn verify_header_phi_dsts_not_redefined(
    func: &MirFunction,
    header_block: BasicBlockId,
    phi_dsts: &std::collections::HashSet<ValueId>,
) {
    if phi_dsts.is_empty() {
        return; // No PHI dsts to protect
    }

    // Check all blocks for non-PHI instructions that redefine PHI dsts
    for (block_id, block) in &func.blocks {
        for instr in &block.instructions {
            // Skip PHIs in header block (they're the definitions we're protecting)
            if *block_id == header_block && matches!(instr, MirInstruction::Phi { .. }) {
                continue;
            }

            // Check if this instruction redefines a PHI dst
            if let Some(dst) = get_instruction_dst(instr) {
                if phi_dsts.contains(&dst) {
                    panic!(
                        "[JoinIRVerifier/Phase135-P1] Header PHI dst {:?} redefined by non-PHI instruction in block {}:\n\
                         Instruction: {:?}\n\
                         Contract: Header PHI dsts must not be reused as dst in other instructions.\n\
                         Fix: Ensure ConditionLoweringBox uses SSOT allocator (ConditionContext.alloc_value) to avoid ValueId collisions.",
                        dst, block_id.0, instr
                    );
                }
            }
        }
    }
}
