## Coverage Report

#### Created: 2025-09-08 21:26

next uncovered line (L), next uncovered region (R), next uncovered branch (B)

    /home/noah/src/ruchy/src/bin/handlers/handlers_modules/prove.rs

    Line
    Count
    Source
    1
    //! Refactored prove command handler
    2
    //! Complexity reduced from 390 to ≤10 per function
    3
    4
    use anyhow::Result;
    5
    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};
    6
    use ruchy::proving::{InteractiveProver, ProverSession};
    7
    use std::io::{self, Write};
    8
    9
    /// Handle interactive theorem prover - refactored with ≤10 complexity
    10
    0
    pub fn handle_prove_command(
    11
    0
        file: Option<&std::path::Path>,
    12
    0
        backend: &str,
    13
    0
        ml_suggestions: bool,
    14
    0
        timeout: u64,
    15
    0
        script: Option<&std::path::Path>,
    16
    0
        export: Option<&std::path::Path>,
    17
    0
        check: bool,
    18
    0
        counterexample: bool,
    19
    0
        verbose: bool,
    20
    0
        format: &str,
    21
    0
    ) -> Result<()> {
    22
    0
        if verbose {
    23
    0
            println!("🔍 Starting interactive prover with backend: {}", backend);
    24
    0
        }
    25
    26
        // Parse backend and create prover
    27
    0
        let smt_backend = parse_smt_backend(backend, verbose);
    28
    0
        let mut prover = InteractiveProver::new(smt_backend);
    29
    30
        // Configure prover settings
    31
    0
        configure_prover(&mut prover, timeout, ml_suggestions, verbose);
    32
    33
        // Handle file-based proof checking
    34
    0
        if let Some(file_path) = file {
    35
    0
            return handle_file_proving(file_path, format, counterexample, verbose);
    36
    0
        }
    37
    38
        // Load script if provided
    39
    0
        if let Some(script_path) = script {
    40
    0
            load_proof_script(&mut prover, script_path, verbose)?;
    41
    0
        }
    42
    43
        // Run interactive session if not in check mode
    44
    0
        if !check {
    45
    0
            run_interactive_session(&mut prover, ml_suggestions, export, format, verbose)?;
    46
    0
        }
    47
    48
    0
        Ok(())
    49
    0
    }
    50
    51
    /// Handle file-based proof checking
    52
    0
    fn handle_file_proving(
    53
    0
        file_path: &std::path::Path,
    54
    0
        format: &str,
    55
    0
        counterexample: bool,
    56
    0
        verbose: bool,
    57
    0
    ) -> Result<()> {
    58
    0
        let ast = load_proof_file(file_path, verbose)?;
    59
    60
    0
        println!("✓ Checking proofs in {}...", file_path.display());
    61
    0
        verify_proofs_from_ast(&ast, file_path, format, counterexample, verbose)
    62
    0
    }
    63
    64
    /// Run interactive prover session
    65
    0
    fn run_interactive_session(
    66
    0
        prover: &mut InteractiveProver,
    67
    0
        ml_suggestions: bool,
    68
    0
        export: Option<&std::path::Path>,
    69
    0
        format: &str,
    70
    0
        verbose: bool,
    71
    0
    ) -> Result<()> {
    72
    0
        println!("🚀 Starting Ruchy Interactive Prover");
    73
    0
        println!("Type 'help' for available commands\n");
    74
    75
    0
        let mut session = ProverSession::new();
    76
    77
        // Main interactive loop
    78
        loop {
    79
    0
            prompt_user()?;
    80
    81
    0
            let input = read_user_input()?;
    82
    0
            if input.is_empty() {
    83
    0
                continue;
    84
    0
            }
    85
    86
            // Process command
    87
    0
            let should_exit = handle_prover_command(&input, prover, &mut session, verbose)?;
    88
    0
            if should_exit {
    89
    0
                break;
    90
    0
            }
    91
    92
            // Show current state
    93
    0
            show_prover_state(&session, prover, ml_suggestions);
    94
        }
    95
    96
        // Export proof if requested
    97
    0
        if let Some(export_path) = export {
    98
    0
            export_proof(&session, export_path, format, verbose)?;
    99
    0
        }
    100
    101
    0
        Ok(())
    102
    0
    }
    103
    104
    /// Display prompt to user
    105
    0
    fn prompt_user() -> Result<()> {
    106
    0
        print!("prove> ");
    107
    0
        io::stdout().flush()?;
    108
    0
        Ok(())
    109
    0
    }
    110
    111
    /// Read input from user
    112
    0
    fn read_user_input() -> Result<String> {
    113
    0
        let mut input = String::new();
    114
    0
        io::stdin().read_line(&mut input)?;
    115
    0
        Ok(input.trim().to_string())
    116
    0
    }