//! Refactored prove command handler
//! Complexity reduced from 390 to ≤10 per function

use anyhow::Result;
use super::prove_helpers::{parse_smt_backend, configure_prover, load_proof_script, load_proof_file, verify_proofs_from_ast, handle_prover_command, show_prover_state, export_proof};
use ruchy::proving::{InteractiveProver, ProverSession};
use std::io::{self, Write};

/// Handle interactive theorem prover - refactored with ≤10 complexity
pub fn handle_prove_command(
    file: Option<&std::path::Path>,
    backend: &str,
    ml_suggestions: bool,
    timeout: u64,
    script: Option<&std::path::Path>,
    export: Option<&std::path::Path>,
    check: bool,
    counterexample: bool,
    verbose: bool,
    format: &str,
) -> Result<()> {
    if verbose {
        println!("🔍 Starting interactive prover with backend: {}", backend);
    }
    
    // Parse backend and create prover
    let smt_backend = parse_smt_backend(backend, verbose);
    let mut prover = InteractiveProver::new(smt_backend);
    
    // Configure prover settings
    configure_prover(&mut prover, timeout, ml_suggestions, verbose);
    
    // Handle file-based proof checking
    if let Some(file_path) = file {
        return handle_file_proving(file_path, format, counterexample, verbose);
    }
    
    // Load script if provided
    if let Some(script_path) = script {
        load_proof_script(&mut prover, script_path, verbose)?;
    }
    
    // Run interactive session if not in check mode
    if !check {
        run_interactive_session(&mut prover, ml_suggestions, export, format, verbose)?;
    }
    
    Ok(())
}

/// Handle file-based proof checking
fn handle_file_proving(
    file_path: &std::path::Path,
    format: &str,
    counterexample: bool,
    verbose: bool,
) -> Result<()> {
    let ast = load_proof_file(file_path, verbose)?;
    
    println!("✓ Checking proofs in {}...", file_path.display());
    verify_proofs_from_ast(&ast, file_path, format, counterexample, verbose)
}

/// Run interactive prover session
fn run_interactive_session(
    prover: &mut InteractiveProver,
    ml_suggestions: bool,
    export: Option<&std::path::Path>,
    format: &str,
    verbose: bool,
) -> Result<()> {
    println!("🚀 Starting Ruchy Interactive Prover");
    println!("Type 'help' for available commands\n");
    
    let mut session = ProverSession::new();
    
    // Main interactive loop
    loop {
        prompt_user()?;
        
        let input = read_user_input()?;
        if input.is_empty() {
            continue;
        }
        
        // Process command
        let should_exit = handle_prover_command(&input, prover, &mut session, verbose)?;
        if should_exit {
            break;
        }
        
        // Show current state
        show_prover_state(&session, prover, ml_suggestions);
    }
    
    // Export proof if requested
    if let Some(export_path) = export {
        export_proof(&session, export_path, format, verbose)?;
    }
    
    Ok(())
}

/// Display prompt to user
fn prompt_user() -> Result<()> {
    print!("prove> ");
    io::stdout().flush()?;
    Ok(())
}

/// Read input from user
fn read_user_input() -> Result<String> {
    let mut input = String::new();
    io::stdin().read_line(&mut input)?;
    Ok(input.trim().to_string())
}