//! Phase 273 P3: PlanVerifier - CorePlan 不変条件検証 (fail-fast)
//!
//! # Responsibilities
//!
//! - Validate CorePlan invariants before lowering
//! - Fail fast on close-but-unsupported patterns
//! - Prevent silent miscompilation
//!
//! # Invariants (V2-V9)
//!
//! - V2: Condition validity (valid ValueId)
//! - V3: Exit validity (Return in function, Break/Continue in loop)
//! - V4: Seq non-empty
//! - V5: If completeness (then_plans non-empty)
//! - V6: ValueId validity (all ValueIds pre-generated)
//! - V7: PHI non-empty (loops require at least one carrier)
//! - V8: Frag entry matches header_bb
//! - V9: block_effects contains header_bb
//! - V10: body_bb effects go in loop_plan.body (block_effects[body_bb] must be empty)
//! - V11: Exit must be last in Seq/If branch (ExitMap alignment)
//! - V12: Loop.body must be Effect-only (Seq-of-effects allowed)
//!
//! Phase 273 P3: V1 (Carrier completeness) removed with CoreCarrierInfo

use super::{CoreEffectPlan, CoreExitPlan, CoreIfPlan, CoreLoopPlan, CorePlan};
use crate::mir::builder::control_flow::plan::normalize::CanonicalLoopFacts;
use crate::mir::ValueId;

/// Phase 273 P1: PlanVerifier - CorePlan 不変条件検証 (fail-fast)
pub(in crate::mir::builder) struct PlanVerifier;

impl PlanVerifier {
    /// Verify CorePlan invariants
    ///
    /// Returns Ok(()) if all invariants hold, Err with details otherwise.
    pub(in crate::mir::builder) fn verify(plan: &CorePlan) -> Result<(), String> {
        Self::verify_plan(plan, 0, false)
    }

    fn verify_plan(plan: &CorePlan, depth: usize, in_loop: bool) -> Result<(), String> {
        match plan {
            CorePlan::Seq(plans) => Self::verify_seq(plans, depth, in_loop),
            CorePlan::Loop(loop_plan) => Self::verify_loop(loop_plan, depth),
            CorePlan::If(if_plan) => Self::verify_if(if_plan, depth, in_loop),
            CorePlan::Effect(effect) => Self::verify_effect(effect, depth),
            CorePlan::Exit(exit) => Self::verify_exit(exit, depth, in_loop),
        }
    }

    /// V4: Seq non-empty
    fn verify_seq(plans: &[CorePlan], depth: usize, in_loop: bool) -> Result<(), String> {
        if plans.is_empty() {
            return Err(format!(
                "[V4] Empty Seq at depth {} (Seq must have at least one plan)",
                depth
            ));
        }

        Self::verify_exit_position(plans, depth, "Seq")?;

        for (i, plan) in plans.iter().enumerate() {
            Self::verify_plan(plan, depth + 1, in_loop).map_err(|e| {
                format!("[Seq[{}]] {}", i, e)
            })?;
        }

        Ok(())
    }

    /// Phase 273 P3: Verify loop with generalized fields
    ///
    /// Invariants:
    /// - V2: Condition validity (cond_loop, cond_match)
    /// - V7: PHI non-empty (at least one carrier)
    /// - V8: Frag entry matches header_bb
    /// - V9: block_effects contains header_bb
    fn verify_loop(loop_plan: &CoreLoopPlan, depth: usize) -> Result<(), String> {
        // V2: Condition validity (basic check - ValueId should be non-zero for safety)
        Self::verify_value_id_basic(loop_plan.cond_loop, depth, "cond_loop")?;
        Self::verify_value_id_basic(loop_plan.cond_match, depth, "cond_match")?;

        // V7: PHI non-empty (loops must have at least one carrier)
        if loop_plan.phis.is_empty() {
            return Err(format!(
                "[V7] Loop at depth {} has no PHI nodes (loops require at least one carrier)",
                depth
            ));
        }

        // V8: Frag entry matches header_bb (loop entry SSOT)
        if loop_plan.frag.entry != loop_plan.header_bb {
            return Err(format!(
                "[V8] Loop at depth {} has frag.entry {:?} != header_bb {:?}",
                depth, loop_plan.frag.entry, loop_plan.header_bb
            ));
        }

        // V9: block_effects contains header_bb
        let has_header = loop_plan.block_effects.iter().any(|(bb, _)| *bb == loop_plan.header_bb);
        if !has_header {
            return Err(format!(
                "[V9] Loop at depth {} block_effects missing header_bb {:?}",
                depth, loop_plan.header_bb
            ));
        }

        // V10: body_bb effects must be empty in block_effects (use loop_plan.body instead)
        // Phase 286 P2.7: lowerer emits loop_plan.body for body_bb, ignoring block_effects
        for (bb, effects) in loop_plan.block_effects.iter() {
            if *bb == loop_plan.body_bb && !effects.is_empty() {
                return Err(format!(
                    "[V10] Loop at depth {} has non-empty block_effects for body_bb {:?} ({} effects). \
                    Body effects must go in loop_plan.body instead.",
                    depth, loop_plan.body_bb, effects.len()
                ));
            }
        }

        // Verify block_effects
        for (i, (bb, effects)) in loop_plan.block_effects.iter().enumerate() {
            for (j, effect) in effects.iter().enumerate() {
                Self::verify_effect(effect, depth).map_err(|e| {
                    format!("[Loop.block_effects[{}={:?}][{}]] {}", i, bb, j, e)
                })?;
            }
        }

        // Verify body plans (now in_loop = true)
        Self::verify_loop_body_effect_only(&loop_plan.body, depth)?;
        for (i, plan) in loop_plan.body.iter().enumerate() {
            Self::verify_plan(plan, depth + 1, true).map_err(|e| {
                format!("[Loop.body[{}]] {}", i, e)
            })?;
        }

        // Verify PHIs
        for (i, phi) in loop_plan.phis.iter().enumerate() {
            Self::verify_value_id_basic(phi.dst, depth, &format!("phi[{}].dst", i))?;
            for (j, (_, val)) in phi.inputs.iter().enumerate() {
                Self::verify_value_id_basic(*val, depth, &format!("phi[{}].inputs[{}]", i, j))?;
            }
        }

        // Verify final_values
        for (i, (name, val)) in loop_plan.final_values.iter().enumerate() {
            if name.is_empty() {
                return Err(format!(
                    "[V6] final_values[{}] at depth {} has empty name",
                    i, depth
                ));
            }
            Self::verify_value_id_basic(*val, depth, &format!("final_values[{}]", i))?;
        }

        Ok(())
    }

    // Phase 273 P3: verify_carrier() removed (CoreCarrierInfo replaced by CorePhiInfo)

    /// V5: If completeness
    fn verify_if(if_plan: &CoreIfPlan, depth: usize, in_loop: bool) -> Result<(), String> {
        // V2: Condition validity
        Self::verify_value_id_basic(if_plan.condition, depth, "if.condition")?;

        // V5: then_plans non-empty
        if if_plan.then_plans.is_empty() {
            return Err(format!(
                "[V5] If at depth {} has empty then_plans",
                depth
            ));
        }

        if let Some(else_plans) = &if_plan.else_plans {
            if else_plans.is_empty() {
                return Err(format!(
                    "[V5] If at depth {} has empty else_plans",
                    depth
                ));
            }
        }

        Self::verify_exit_position(&if_plan.then_plans, depth, "If.then")?;
        if let Some(else_plans) = &if_plan.else_plans {
            Self::verify_exit_position(else_plans, depth, "If.else")?;
        }

        for (i, plan) in if_plan.then_plans.iter().enumerate() {
            Self::verify_plan(plan, depth + 1, in_loop).map_err(|e| {
                format!("[If.then[{}]] {}", i, e)
            })?;
        }

        if let Some(else_plans) = &if_plan.else_plans {
            for (i, plan) in else_plans.iter().enumerate() {
                Self::verify_plan(plan, depth + 1, in_loop).map_err(|e| {
                    format!("[If.else[{}]] {}", i, e)
                })?;
            }
        }

        Ok(())
    }

    /// V6: Effect ValueId validity
    fn verify_effect(effect: &CoreEffectPlan, depth: usize) -> Result<(), String> {
        match effect {
            CoreEffectPlan::MethodCall { dst, object, method, args, effects: _ } => {
                // P2: dst is now Option<ValueId>
                if let Some(dst_val) = dst {
                    Self::verify_value_id_basic(*dst_val, depth, "MethodCall.dst")?;
                }
                Self::verify_value_id_basic(*object, depth, "MethodCall.object")?;
                if method.is_empty() {
                    return Err(format!(
                        "[V6] MethodCall at depth {} has empty method name",
                        depth
                    ));
                }
                for (i, arg) in args.iter().enumerate() {
                    Self::verify_value_id_basic(*arg, depth, &format!("MethodCall.args[{}]", i))?;
                }
            }
            CoreEffectPlan::BinOp { dst, lhs, op: _, rhs } => {
                Self::verify_value_id_basic(*dst, depth, "BinOp.dst")?;
                Self::verify_value_id_basic(*lhs, depth, "BinOp.lhs")?;
                Self::verify_value_id_basic(*rhs, depth, "BinOp.rhs")?;
            }
            CoreEffectPlan::Compare { dst, lhs, op: _, rhs } => {
                Self::verify_value_id_basic(*dst, depth, "Compare.dst")?;
                Self::verify_value_id_basic(*lhs, depth, "Compare.lhs")?;
                Self::verify_value_id_basic(*rhs, depth, "Compare.rhs")?;
            }
            CoreEffectPlan::Const { dst, value: _ } => {
                Self::verify_value_id_basic(*dst, depth, "Const.dst")?;
            }
        }
        Ok(())
    }

    /// V3: Exit validity
    fn verify_exit(exit: &CoreExitPlan, depth: usize, in_loop: bool) -> Result<(), String> {
        match exit {
            CoreExitPlan::Return(opt_val) => {
                if let Some(val) = opt_val {
                    Self::verify_value_id_basic(*val, depth, "Return.value")?;
                }
                // Return is always valid (in function context)
            }
            CoreExitPlan::Break => {
                if !in_loop {
                    return Err(format!(
                        "[V3] Break at depth {} outside of loop",
                        depth
                    ));
                }
            }
            CoreExitPlan::Continue => {
                if !in_loop {
                    return Err(format!(
                        "[V3] Continue at depth {} outside of loop",
                        depth
                    ));
                }
            }
        }
        Ok(())
    }

    fn verify_exit_position(plans: &[CorePlan], depth: usize, scope: &str) -> Result<(), String> {
        for (i, plan) in plans.iter().enumerate() {
            if matches!(plan, CorePlan::Exit(_)) && i + 1 != plans.len() {
                return Err(format!(
                    "[V11] Exit at depth {} in {} must be last (index {}, len {})",
                    depth,
                    scope,
                    i,
                    plans.len()
                ));
            }
        }
        Ok(())
    }

    fn verify_loop_body_effect_only(plans: &[CorePlan], depth: usize) -> Result<(), String> {
        for (i, plan) in plans.iter().enumerate() {
            let path = format!("Loop.body[{}]", i);
            Self::verify_body_plan_effect_only(plan, depth, &path)?;
        }
        Ok(())
    }

    fn verify_body_plan_effect_only(
        plan: &CorePlan,
        depth: usize,
        path: &str,
    ) -> Result<(), String> {
        match plan {
            CorePlan::Effect(_) => Ok(()),
            CorePlan::Seq(plans) => {
                for (i, nested) in plans.iter().enumerate() {
                    let nested_path = format!("{}.Seq[{}]", path, i);
                    Self::verify_body_plan_effect_only(nested, depth + 1, &nested_path)?;
                }
                Ok(())
            }
            _ => Err(format!(
                "[V12] Loop body contains non-effect plan {} at depth {} ({})",
                Self::plan_kind(plan),
                depth,
                path
            )),
        }
    }

    fn plan_kind(plan: &CorePlan) -> &'static str {
        match plan {
            CorePlan::Seq(_) => "Seq",
            CorePlan::Loop(_) => "Loop",
            CorePlan::If(_) => "If",
            CorePlan::Effect(_) => "Effect",
            CorePlan::Exit(_) => "Exit",
        }
    }

    /// V6: Basic ValueId validity check
    ///
    /// Note: This is a basic check. Full validity would require builder context.
    fn verify_value_id_basic(value_id: ValueId, depth: usize, context: &str) -> Result<(), String> {
        // ValueId(0) might be valid in some contexts, so we don't check for zero
        // This is a placeholder for more sophisticated checks if needed
        let _ = (value_id, depth, context);
        Ok(())
    }
}

#[cfg(debug_assertions)]
pub(in crate::mir::builder) fn debug_assert_value_join_invariants(facts: &CanonicalLoopFacts) {
    if facts.value_join_needed {
        debug_assert!(
            !facts.exit_kinds_present.is_empty(),
            "value join requires at least one exit kind"
        );
    }
}

#[cfg(not(debug_assertions))]
pub(in crate::mir::builder) fn debug_assert_value_join_invariants(_facts: &CanonicalLoopFacts) {}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::mir::{BasicBlockId, ConstValue, ValueId};
    use crate::mir::builder::control_flow::edgecfg::api::Frag;
    use crate::mir::builder::control_flow::plan::CorePhiInfo;
    use crate::mir::builder::control_flow::plan::facts::feature_facts::{
        LoopFeatureFacts, ValueJoinFacts,
    };
    use crate::mir::builder::control_flow::plan::facts::loop_facts::LoopFacts;
    use crate::mir::builder::control_flow::plan::facts::scan_shapes::{
        ConditionShape, StepShape,
    };
    use crate::mir::builder::control_flow::plan::facts::skeleton_facts::{
        SkeletonFacts, SkeletonKind,
    };
    use crate::mir::builder::control_flow::plan::normalize::canonicalize_loop_facts;
    use std::collections::BTreeMap;

    fn make_loop_plan(body: Vec<CorePlan>) -> CoreLoopPlan {
        let preheader_bb = BasicBlockId(0);
        let header_bb = BasicBlockId(1);
        let body_bb = BasicBlockId(2);
        let step_bb = BasicBlockId(3);
        let after_bb = BasicBlockId(4);

        CoreLoopPlan {
            preheader_bb,
            header_bb,
            body_bb,
            step_bb,
            after_bb,
            found_bb: after_bb,
            body,
            cond_loop: ValueId(100),
            cond_match: ValueId(101),
            block_effects: vec![
                (preheader_bb, vec![]),
                (header_bb, vec![]),
                (body_bb, vec![]),
                (step_bb, vec![]),
            ],
            phis: vec![CorePhiInfo {
                block: header_bb,
                dst: ValueId(102),
                inputs: vec![(preheader_bb, ValueId(103)), (step_bb, ValueId(104))],
                tag: "test_phi".to_string(),
            }],
            frag: Frag::new(header_bb),
            final_values: vec![("i".to_string(), ValueId(102))],
        }
    }

    #[test]
    fn test_verify_empty_seq_fails() {
        let plan = CorePlan::Seq(vec![]);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V4]"));
    }

    #[test]
    fn test_verify_break_outside_loop_fails() {
        let plan = CorePlan::Exit(CoreExitPlan::Break);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V3]"));
    }

    #[test]
    fn test_verify_const_effect_succeeds() {
        let plan = CorePlan::Effect(CoreEffectPlan::Const {
            dst: ValueId(1),
            value: ConstValue::Integer(42),
        });
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_ok());
    }

    #[test]
    fn test_verify_loop_body_seq_effects_ok() {
        let body = vec![CorePlan::Seq(vec![
            CorePlan::Effect(CoreEffectPlan::Const {
                dst: ValueId(10),
                value: ConstValue::Integer(1),
            }),
            CorePlan::Seq(vec![CorePlan::Effect(CoreEffectPlan::Const {
                dst: ValueId(11),
                value: ConstValue::Integer(2),
            })]),
        ])];
        let plan = CorePlan::Loop(make_loop_plan(body));
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_ok());
    }

    #[test]
    fn test_verify_loop_body_if_fails() {
        let if_plan = CoreIfPlan {
            condition: ValueId(1),
            then_plans: vec![CorePlan::Effect(CoreEffectPlan::Const {
                dst: ValueId(2),
                value: ConstValue::Integer(1),
            })],
            else_plans: None,
        };
        let plan = CorePlan::Loop(make_loop_plan(vec![CorePlan::If(if_plan)]));
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V12]"));
    }

    #[test]
    fn test_verify_loop_body_exit_fails() {
        let plan = CorePlan::Loop(make_loop_plan(vec![CorePlan::Exit(
            CoreExitPlan::Return(None),
        )]));
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V12]"));
    }

    #[test]
    fn test_verify_if_empty_else_fails() {
        let if_plan = CoreIfPlan {
            condition: ValueId(1),
            then_plans: vec![CorePlan::Effect(CoreEffectPlan::Const {
                dst: ValueId(2),
                value: ConstValue::Integer(1),
            })],
            else_plans: Some(vec![]),
        };
        let plan = CorePlan::If(if_plan);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V5]"));
    }

    #[test]
    fn test_verify_exit_not_last_fails() {
        let plan = CorePlan::Seq(vec![
            CorePlan::Exit(CoreExitPlan::Return(None)),
            CorePlan::Effect(CoreEffectPlan::Const {
                dst: ValueId(1),
                value: ConstValue::Integer(0),
            }),
        ]);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V11]"));
    }

    #[test]
    fn test_verify_if_exit_not_last_fails() {
        let if_plan = CoreIfPlan {
            condition: ValueId(1),
            then_plans: vec![
                CorePlan::Exit(CoreExitPlan::Return(None)),
                CorePlan::Effect(CoreEffectPlan::Const {
                    dst: ValueId(2),
                    value: ConstValue::Integer(1),
                }),
            ],
            else_plans: Some(vec![CorePlan::Effect(CoreEffectPlan::Const {
                dst: ValueId(3),
                value: ConstValue::Integer(2),
            })]),
        };
        let plan = CorePlan::If(if_plan);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("[V11]"));
    }

    #[cfg(debug_assertions)]
    #[test]
    fn debug_value_join_invariant_allows_empty_when_not_needed() {
        let facts = LoopFacts {
            condition_shape: ConditionShape::Unknown,
            step_shape: StepShape::Unknown,
            skeleton: SkeletonFacts {
                kind: SkeletonKind::Loop,
            },
            features: LoopFeatureFacts::default(),
            scan_with_init: None,
            split_scan: None,
            pattern1_simplewhile: None,
            pattern3_ifphi: None,
            pattern4_continue: None,
            pattern5_infinite_early_exit: None,
            pattern8_bool_predicate_scan: None,
            pattern9_accum_const_loop: None,
            pattern2_break: None,
            pattern2_loopbodylocal: None,
        };
        let canonical = canonicalize_loop_facts(facts);
        debug_assert_value_join_invariants(&canonical);
    }

    #[cfg(debug_assertions)]
    #[test]
    #[should_panic]
    fn debug_value_join_invariant_panics_without_exit_kinds() {
        let facts = LoopFacts {
            condition_shape: ConditionShape::Unknown,
            step_shape: StepShape::Unknown,
            skeleton: SkeletonFacts {
                kind: SkeletonKind::Loop,
            },
            features: LoopFeatureFacts {
                exit_usage: Default::default(),
                exit_map: None,
                value_join: Some(ValueJoinFacts { needed: true }),
                cleanup: None,
            },
            scan_with_init: None,
            split_scan: None,
            pattern1_simplewhile: None,
            pattern3_ifphi: None,
            pattern4_continue: None,
            pattern5_infinite_early_exit: None,
            pattern8_bool_predicate_scan: None,
            pattern9_accum_const_loop: None,
            pattern2_break: None,
            pattern2_loopbodylocal: None,
        };
        let canonical = canonicalize_loop_facts(facts);
        debug_assert_value_join_invariants(&canonical);
    }

    #[test]
    fn test_v10_body_bb_effects_in_block_effects_fails() {
        // V10: body_bb effects must be empty in block_effects
        // This test verifies that having effects in body_bb's block_effects fails validation
        let preheader_bb = BasicBlockId(0);
        let header_bb = BasicBlockId(1);
        let body_bb = BasicBlockId(2);
        let step_bb = BasicBlockId(3);
        let after_bb = BasicBlockId(4);

        let loop_plan = CoreLoopPlan {
            preheader_bb,
            header_bb,
            body_bb,
            step_bb,
            after_bb,
            found_bb: after_bb,
            body: vec![],
            cond_loop: ValueId(100),
            cond_match: ValueId(101),
            block_effects: vec![
                (preheader_bb, vec![]),
                (header_bb, vec![]),
                // V10 violation: body_bb has effects in block_effects
                (body_bb, vec![CoreEffectPlan::Const {
                    dst: ValueId(102),
                    value: ConstValue::Integer(42),
                }]),
                (step_bb, vec![]),
            ],
            phis: vec![CorePhiInfo {
                block: header_bb,
                dst: ValueId(103),
                inputs: vec![(preheader_bb, ValueId(104)), (step_bb, ValueId(105))],
                tag: "test_phi".to_string(),
            }],
            frag: Frag {
                entry: header_bb,
                exits: BTreeMap::new(),
                wires: vec![],
                branches: vec![],
            },
            final_values: vec![("i".to_string(), ValueId(103))],
        };

        let plan = CorePlan::Loop(loop_plan);
        let result = PlanVerifier::verify(&plan);
        assert!(result.is_err());
        let err = result.unwrap_err();
        assert!(err.contains("[V10]"), "Expected V10 error, got: {}", err);
        assert!(err.contains("body_bb"), "Expected body_bb in error, got: {}", err);
    }
}
