use super::helpers_by_stmt::impossible_proof_error_message;
use crate::prelude::*;

impl Runtime {
    pub fn exec_by_cases_stmt(&mut self, stmt: &ByCasesStmt) -> Result<StmtResult, RuntimeError> {
        for fact in stmt.then_facts.iter() {
            self.verify_fact_well_defined(fact, &VerifyState::new(0, false))
                .map_err(|verify_error| {
                    short_exec_error(
                        stmt.clone().into(),
                        format!("by cases: failed to prove `{}`", fact),
                        Some(verify_error),
                        vec![],
                    )
                })?;
        }

        if stmt
            .then_facts
            .iter()
            .any(|f| matches!(f, Fact::ForallFactWithIff(_)))
        {
            return Err(short_exec_error(
                stmt.clone().into(),
                "by cases: `prove:` with `forall`/`iff` (forall-iff) is not supported; use a plain `forall` goal"
                    .to_string(),
                None,
                vec![],
            ));
        }
        if stmt
            .then_facts
            .iter()
            .filter(|f| matches!(f, Fact::ForallFact(_)))
            .count()
            > 1
        {
            return Err(short_exec_error(
                stmt.clone().into(),
                "by cases: `prove:` may contain at most one `forall` fact".to_string(),
                None,
                vec![],
            ));
        }
        if stmt
            .then_facts
            .get(0)
            .is_some_and(|f| !matches!(f, Fact::ForallFact(_)))
            && stmt
                .then_facts
                .iter()
                .any(|f| matches!(f, Fact::ForallFact(_)))
        {
            return Err(short_exec_error(
                stmt.clone().into(),
                "by cases: when `prove:` includes `forall`, the `forall` must be listed first"
                    .to_string(),
                None,
                vec![],
            ));
        }
        if stmt
            .then_facts
            .iter()
            .any(|f| matches!(f, Fact::ForallFact(_)))
            && stmt.impossible_facts.iter().any(|o| o.is_some())
        {
            return Err(short_exec_error(
                stmt.clone().into(),
                "by cases: `prove:` with `forall` cannot be used in the same statement as a case arm that ends with `impossible`"
                    .to_string(),
                None,
                vec![],
            ));
        }

        self.exec_by_cases_stmt_verify_cases_cover_all_situations(stmt)?;

        for case_index in 0..stmt.cases.len() {
            self.run_in_local_env(|rt| rt.exec_by_cases_stmt_for_one_case(stmt, case_index))?;
        }

        let mut infer_result = InferResult::new();
        for then_fact in stmt.then_facts.iter() {
            let one_then_fact_infer_result = self
                .verify_well_defined_and_store_and_infer_with_default_verify_state(
                    then_fact.clone(),
                )
                .map_err(|store_fact_error| {
                    short_exec_error(
                        stmt.clone().into(),
                        format!("by cases: failed to release `{}`", then_fact),
                        Some(store_fact_error),
                        vec![],
                    )
                })?;
            infer_result.new_infer_result_inside(one_then_fact_infer_result);
        }

        // Omit per-case stmt results from JSON/output; failures still attach inside_results on errors.
        Ok((NonFactualStmtSuccess::new(stmt.clone().into(), infer_result, vec![])).into())
    }

    fn exec_by_cases_stmt_verify_cases_cover_all_situations(
        &mut self,
        stmt: &ByCasesStmt,
    ) -> Result<(), RuntimeError> {
        let all_cases_or_fact: Fact =
            OrFact::new(stmt.cases.clone(), stmt.line_file.clone()).into();
        let vs = VerifyState::new(0, false);
        if let Some(Fact::ForallFact(ff)) = stmt.then_facts.first() {
            self.run_in_local_env(|rt| {
                rt.forall_assume_params_and_dom_in_current_env(ff, &vs)?;
                rt.verify_fact_return_err_if_not_true(&all_cases_or_fact, &vs)
            })
            .map_err(|verify_error| {
                short_exec_error(
                    stmt.clone().into(),
                    "by cases: cannot verify that all cases cover all situations".to_string(),
                    Some(verify_error),
                    vec![],
                )
            })?;
        } else {
            self.verify_fact_return_err_if_not_true(&all_cases_or_fact, &vs)
                .map_err(|verify_error| {
                    short_exec_error(
                        stmt.clone().into(),
                        "by cases: cannot verify that all cases cover all situations".to_string(),
                        Some(verify_error),
                        vec![],
                    )
                })?;
        }
        Ok(())
    }

    fn exec_by_cases_stmt_prove_then_facts_under_case(
        &mut self,
        stmt: &ByCasesStmt,
        case_index: usize,
        inside_results: &mut Vec<StmtResult>,
    ) -> Result<(), RuntimeError> {
        for then_fact in stmt.then_facts.iter() {
            let exec_fact_result = self.exec_fact(then_fact).map_err(|statement_error| {
                short_exec_error(
                    stmt.clone().into(),
                    format!(
                        "by cases: failed to prove `{}` under case `{}`",
                        then_fact, stmt.cases[case_index]
                    ),
                    Some(statement_error),
                    std::mem::take(inside_results),
                )
            })?;
            inside_results.push(exec_fact_result);
        }
        Ok(())
    }

    fn exec_by_cases_stmt_for_one_case(
        &mut self,
        stmt: &ByCasesStmt,
        case_index: usize,
    ) -> Result<Vec<StmtResult>, RuntimeError> {
        let case_fact = &stmt.cases[case_index];
        let case_label = case_fact.to_string();
        let mut inside_results: Vec<StmtResult> = Vec::new();
        let vs = VerifyState::new(0, false);

        if let Some(Fact::ForallFact(ff)) = stmt.then_facts.first() {
            let mut infer_acc = self
                .forall_assume_params_and_dom_in_current_env(ff, &vs)
                .map_err(|e| {
                    short_exec_error(
                        stmt.clone().into(),
                        format!(
                            "by cases: failed to open `forall` parameters and dom for goal `{}`",
                            ff
                        ),
                        Some(e),
                        vec![],
                    )
                })?;

            self.store_and_chain_atomic_fact_without_well_defined_verified_and_infer(
                case_fact.clone(),
            )
            .map_err(|store_fact_error| {
                short_exec_error(
                    stmt.clone().into(),
                    format!("by cases: failed to assume case `{}`", case_fact),
                    Some(store_fact_error),
                    vec![],
                )
            })?;

            for proof_stmt in stmt.proofs[case_index].iter() {
                let exec_stmt_result = self.exec_stmt(proof_stmt);
                match exec_stmt_result {
                    Ok(result) => inside_results.push(result),
                    Err(statement_error) => {
                        return Err(short_exec_error(
                            stmt.clone().into(),
                            format!(
                                "by cases: failed while executing proof under case `{}`",
                                case_fact
                            ),
                            Some(statement_error),
                            inside_results,
                        ));
                    }
                }
            }

            let forall_then_result = self.forall_verify_then_facts_in_current_env(
                ff,
                &vs,
                &mut infer_acc,
                Some(&case_label),
            )?;
            if !forall_then_result.is_true() {
                inside_results.push(forall_then_result);
                return Err(short_exec_error(
                    stmt.clone().into(),
                    format!(
                        "by cases: failed to prove `forall` goal under case `{}`",
                        case_fact
                    ),
                    None,
                    inside_results,
                ));
            }
            inside_results.push(forall_then_result);

            for then_fact in stmt.then_facts.iter().skip(1) {
                let exec_fact_result = self.exec_fact(then_fact).map_err(|statement_error| {
                    short_exec_error(
                        stmt.clone().into(),
                        format!(
                            "by cases: failed to prove `{}` under case `{}`",
                            then_fact, case_fact
                        ),
                        Some(statement_error),
                        std::mem::take(&mut inside_results),
                    )
                })?;
                inside_results.push(exec_fact_result);
            }

            return Ok(inside_results);
        }

        self.store_and_chain_atomic_fact_without_well_defined_verified_and_infer(case_fact.clone())
            .map_err(|store_fact_error| {
                short_exec_error(
                    stmt.clone().into(),
                    format!("by cases: failed to assume case `{}`", case_fact),
                    Some(store_fact_error),
                    vec![],
                )
            })?;

        for proof_stmt in stmt.proofs[case_index].iter() {
            let exec_stmt_result = self.exec_stmt(proof_stmt);
            match exec_stmt_result {
                Ok(result) => inside_results.push(result),
                Err(statement_error) => {
                    return Err(short_exec_error(
                        stmt.clone().into(),
                        format!(
                            "by cases: failed while executing proof under case `{}`",
                            case_fact
                        ),
                        Some(statement_error),
                        inside_results,
                    ));
                }
            }
        }

        if let Some(impossible_fact) = &stmt.impossible_facts[case_index] {
            let verify_state = VerifyState::new(0, false);
            let verify_impossible_fact_result = self
                .verify_atomic_fact(impossible_fact, &verify_state)
                .map_err(|verify_error| {
                    short_exec_error(
                        stmt.clone().into(),
                        impossible_proof_error_message(
                            impossible_fact,
                            Some(case_fact.to_string()),
                        ),
                        Some(verify_error),
                        vec![],
                    )
                })?;

            if verify_impossible_fact_result.is_unknown() {
                return Err(short_exec_error(
                    stmt.clone().into(),
                    impossible_proof_error_message(impossible_fact, Some(case_fact.to_string())),
                    None,
                    vec![],
                ));
            }

            let verify_reversed_impossible_fact_result = self
                .verify_atomic_fact(&impossible_fact.make_reversed(), &verify_state)
                .map_err(|verify_error| {
                    short_exec_error(
                        stmt.clone().into(),
                        impossible_proof_error_message(
                            impossible_fact,
                            Some(case_fact.to_string()),
                        ),
                        Some(verify_error),
                        vec![],
                    )
                })?;

            if verify_reversed_impossible_fact_result.is_unknown() {
                return Err(short_exec_error(
                    stmt.clone().into(),
                    impossible_proof_error_message(impossible_fact, Some(case_fact.to_string())),
                    None,
                    vec![],
                ));
            }

            inside_results.push(
                (NonFactualStmtSuccess::new(
                    stmt.clone().into(),
                    InferResult::new(),
                    vec![
                        verify_impossible_fact_result,
                        verify_reversed_impossible_fact_result,
                    ],
                ))
                .into(),
            );

            return Ok(inside_results);
        }

        self.exec_by_cases_stmt_prove_then_facts_under_case(stmt, case_index, &mut inside_results)?;
        Ok(inside_results)
    }
}
