## 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/proving/prover.rs

    Line
    Count
    Source
    1
    //! Simplified interactive theorem prover
    2
    3
    use anyhow::Result;
    4
    use serde::{Deserialize, Serialize};
    5
    use std::collections::HashMap;
    6
    7
    use super::smt::SmtBackend;
    8
    use super::tactics::TacticLibrary;
    9
    10
    /// Interactive prover
    11
    pub struct InteractiveProver {
    12
        _backend: SmtBackend,
    13
        tactics: TacticLibrary,
    14
        timeout: u64,
    15
        ml_suggestions: bool,
    16
    }
    17
    18
    impl InteractiveProver {
    19
        /// Create new prover
    20
    0
        pub fn new(backend: SmtBackend) -> Self {
    21
    0
            Self {
    22
    0
                _backend: backend,
    23
    0
                tactics: TacticLibrary::default(),
    24
    0
                timeout: 5000,
    25
    0
                ml_suggestions: false,
    26
    0
            }
    27
    0
        }
    28
    29
        /// Set timeout
    30
    0
        pub fn set_timeout(&mut self, timeout: u64) {
    31
    0
            self.timeout = timeout;
    32
    0
        }
    33
    34
        /// Enable ML suggestions
    35
    0
        pub fn set_ml_suggestions(&mut self, enabled: bool) {
    36
    0
            self.ml_suggestions = enabled;
    37
    0
        }
    38
    39
        /// Load proof script
    40
    0
        pub fn load_script(&mut self, _script: &str) -> Result<()> {
    41
            // Simplified: just return ok
    42
    0
            Ok(())
    43
    0
        }
    44
    45
        /// Get available tactics
    46
    0
        pub fn get_available_tactics(&self) -> Vec<&dyn super::tactics::Tactic> {
    47
    0
            self.tactics.all_tactics()
    48
    0
        }
    49
    50
        /// Apply tactic
    51
    0
        pub fn apply_tactic(&mut self, session: &mut ProverSession, tactic_name: &str, args: &[&str]) -> Result<ProofResult> {
    52
    0
            let tactic = self.tactics.get_tactic(tactic_name)?;
    53
    54
    0
            if let Some(goal) = session.current_goal() {
    55
    0
                let result = tactic.apply(goal, args, &session.context)?;
    56
    0
                match result {
    57
                    StepResult::Solved => {
    58
    0
                        session.complete_goal();
    59
    0
                        Ok(ProofResult::Solved)
    60
                    }
    61
    0
                    StepResult::Simplified(new_goal) => {
    62
    0
                        session.update_goal(new_goal);
    63
    0
                        Ok(ProofResult::Progress)
    64
                    }
    65
    0
                    StepResult::Subgoals(subgoals) => {
    66
    0
                        session.replace_with_subgoals(subgoals);
    67
    0
                        Ok(ProofResult::Progress)
    68
                    }
    69
    0
                    StepResult::Failed(msg) => {
    70
    0
                        Ok(ProofResult::Failed(msg))
    71
                    }
    72
                }
    73
            } else {
    74
    0
                Ok(ProofResult::Failed("No active goal".to_string()))
    75
            }
    76
    0
        }
    77
    78
        /// Process input
    79
    0
        pub fn process_input(&mut self, session: &mut ProverSession, input: &str) -> Result<ProofResult> {
    80
            // Try to parse as goal
    81
    0
            if let Some(goal) = input.strip_prefix("prove ") {
    82
    0
                session.add_goal(goal.to_string());
    83
    0
                return Ok(ProofResult::Progress);
    84
    0
            }
    85
    86
            // Try as tactic
    87
    0
            let parts: Vec<&str> = input.split_whitespace().collect();
    88
    0
            if !parts.is_empty() {
    89
    0
                let tactic_name = parts[0];
    90
    0
                let args = &parts[1..];
    91
    0
                return self.apply_tactic(session, tactic_name, args);
    92
    0
            }
    93
    94
    0
            Ok(ProofResult::Failed("Unknown command".to_string()))
    95
    0
        }
    96
    97
        /// Suggest tactics
    98
    0
        pub fn suggest_tactics(&self, goal: &ProofGoal) -> Result<Vec<super::tactics::TacticSuggestion>> {
    99
    0
            self.tactics.suggest_tactics(goal, &ProofContext::new())
    100
    0
        }
    101
    }
    102
    103
    /// Prover session
    104
    #[derive(Debug, Clone, Serialize, Deserialize)]
    105
    pub struct ProverSession {
    106
        goals: Vec<ProofGoal>,
    107
        context: ProofContext,
    108
        history: Vec<String>,
    109
    }
    110
    111
    impl ProverSession {
    112
        /// Create new session
    113
    0
        pub fn new() -> Self {
    114
    0
            Self {
    115
    0
                goals: Vec::new(),
    116
    0
                context: ProofContext::new(),
    117
    0
                history: Vec::new(),
    118
    0
            }
    119
    0
        }
    120
    121
        /// Add goal
    122
    0
        pub fn add_goal(&mut self, statement: String) {
    123
    0
            self.goals.push(ProofGoal { statement });
    124
    0
        }
    125
    126
        /// Get current goal
    127
    0
        pub fn current_goal(&self) -> Option<&ProofGoal> {
    128
    0
            self.goals.first()
    129
    0
        }
    130
    131
        /// Update current goal
    132
    0
        pub fn update_goal(&mut self, statement: String) {
    133
    0
            if !self.goals.is_empty() {
    134
    0
                self.goals[0].statement = statement;
    135
    0
            }
    136
    0
        }
    137
    138
        /// Complete current goal
    139
    0
        pub fn complete_goal(&mut self) {
    140
    0
            if !self.goals.is_empty() {
    141
    0
                self.goals.remove(0);
    142
    0
            }
    143
    0
        }
    144
    145
        /// Replace with subgoals
    146
    0
        pub fn replace_with_subgoals(&mut self, subgoals: Vec<String>) {
    147
    0
            if !self.goals.is_empty() {
    148
    0
                self.goals.remove(0);
    149
    0
                for subgoal in subgoals.into_iter().rev() {
    150
    0
                    self.goals.insert(0, ProofGoal { statement: subgoal });
    151
    0
                }
    152
    0
            }
    153
    0
        }
    154
    155
        /// Get all goals
    156
    0
        pub fn get_goals(&self) -> &[ProofGoal] {
    157
    0
            &self.goals
    158
    0
        }
    159
    160
        /// Check if complete
    161
    0
        pub fn is_complete(&self) -> bool {
    162
    0
            self.goals.is_empty()
    163
    0
        }
    164
    165
        /// Export to text
    166
    0
        pub fn to_text_proof(&self) -> String {
    167
    0
            let mut proof = String::new();
    168
    0
            proof.push_str("Proof:\n");
    169
    0
            for line in &self.history {
    170
                use std::fmt::Write;
    171
    0
                let _ = writeln!(proof, "  {line}");
    172
            }
    173
    0
            if self.is_complete() {
    174
    0
                proof.push_str("Qed.\n");
    175
    0
            }
    176
    0
            proof
    177
    0
        }
    178
    179
        /// Export to Coq
    180
    0
        pub fn to_coq_proof(&self) -> String {
    181
    0
            self.to_text_proof() // Simplified
    182
    0
        }
    183
    184
        /// Export to Lean
    185
    0
        pub fn to_lean_proof(&self) -> String {
    186
    0
            self.to_text_proof() // Simplified
    187
    0
        }
    188
    }
    189
    190
    impl Default for ProverSession {
    191
    0
        fn default() -> Self {
    192
    0
            Self::new()
    193
    0
        }
    194
    }
    195
    196
    /// Proof goal
    197
    #[derive(Debug, Clone, Serialize, Deserialize)]
    198
    pub struct ProofGoal {
    199
        pub statement: String,
    200
    }
    201
    202
    /// Proof context
    203
    #[derive(Debug, Clone, Serialize, Deserialize)]
    204
    pub struct ProofContext {
    205
        pub assumptions: Vec<String>,
    206
        pub definitions: HashMap<String, String>,
    207
    }
    208
    209
    impl ProofContext {
    210
        /// Create new context
    211
    0
        pub fn new() -> Self {
    212
    0
            Self {
    213
    0
                assumptions: Vec::new(),
    214
    0
                definitions: HashMap::new(),
    215
    0
            }
    216
    0
        }
    217
    }
    218
    219
    impl Default for ProofContext {
    220
    0
        fn default() -> Self {
    221
    0
            Self::new()
    222
    0
        }
    223
    }
    224
    225
    /// Proof result
    226
    #[derive(Debug)]
    227
    pub enum ProofResult {
    228
        Solved,
    229
        Progress,
    230
        Failed(String),
    231
    }
    232
    233
    /// Step result from tactic application
    234
    #[derive(Debug, Clone)]
    235
    pub enum StepResult {
    236
        /// Goal was solved
    237
        Solved,
    238
    239
        /// Goal was simplified to new goal
    240
        Simplified(String),
    241
    242
        /// Goal was split into subgoals
    243
        Subgoals(Vec<String>),
    244
    245
        /// Tactic failed
    246
        Failed(String),
    247
    }
    248
    249
    #[cfg(test)]
    250
    mod tests {
    251
        use super::*;
    252
        use crate::proving::smt::SmtBackend;
    253
    254
        fn create_test_prover() -> InteractiveProver {
    255
            let backend = SmtBackend::Z3;
    256
            InteractiveProver::new(backend)
    257
        }
    258
    259
        fn create_test_session() -> ProverSession {
    260
            ProverSession::new()
    261
        }
    262
    263
        // Test 1: Prover Creation and Basic Configuration
    264
        #[test]
    265
        fn test_prover_creation() {
    266
            let prover = create_test_prover();
    267
            assert_eq!(prover.timeout, 5000);
    268
            assert!(!prover.ml_suggestions);
    269
        }
    270
    271
        #[test]
    272
        fn test_prover_timeout_setting() {
    273
            let mut prover = create_test_prover();
    274
            prover.set_timeout(10000);
    275
            assert_eq!(prover.timeout, 10000);
    276
        }
    277
    278
        #[test]
    279
        fn test_prover_ml_suggestions_setting() {
    280
            let mut prover = create_test_prover();
    281
            prover.set_ml_suggestions(true);
    282
            assert!(prover.ml_suggestions);
    283
    284
            prover.set_ml_suggestions(false);
    285
            assert!(!prover.ml_suggestions);
    286
        }
    287
    288
        #[test]
    289
        fn test_prover_load_script() {
    290
            let mut prover = create_test_prover();
    291
            let result = prover.load_script("example script");
    292
            assert!(result.is_ok());
    293
        }
    294
    295
        // Test 2: Session Management
    296
        #[test]
    297
        fn test_session_creation() {
    298
            let session = create_test_session();
    299
            assert!(session.goals.is_empty());
    300
            assert!(session.history.is_empty());
    301
            assert!(session.is_complete());
    302
        }
    303
    304
        #[test]
    305
        fn test_session_default() {
    306
            let session = ProverSession::default();
    307
            assert!(session.goals.is_empty());
    308
            assert!(session.is_complete());
    309
        }
    310
    311
        #[test]
    312
        fn test_session_add_goal() {
    313
            let mut session = create_test_session();
    314
            session.add_goal("forall x, x = x".to_string());
    315
    316
            assert_eq!(session.goals.len(), 1);
    317
            assert!(!session.is_complete());
    318
    319
            let current_goal = session.current_goal().unwrap();
    320
            assert_eq!(current_goal.statement, "forall x, x = x");
    321
        }
    322
    323
        #[test]
    324
        fn test_session_multiple_goals() {
    325
            let mut session = create_test_session();
    326
            session.add_goal("goal1".to_string());
    327
            session.add_goal("goal2".to_string());
    328
    329
            assert_eq!(session.goals.len(), 2);
    330
            let current = session.current_goal().unwrap();
    331
            assert_eq!(current.statement, "goal1");
    332
        }
    333
    334
        #[test]
    335
        fn test_session_complete_goal() {
    336
            let mut session = create_test_session();
    337
            session.add_goal("test goal".to_string());
    338
    339
            assert!(!session.is_complete());
    340
            session.complete_goal();
    341
            assert!(session.is_complete());
    342
        }
    343
    344
        #[test]
    345
        fn test_session_update_goal() {
    346
            let mut session = create_test_session();
    347
            session.add_goal("original goal".to_string());
    348
    349
            session.update_goal("updated goal".to_string());
    350
            let current = session.current_goal().unwrap();
    351
            assert_eq!(current.statement, "updated goal");
    352
        }
    353
    354
        #[test]
    355
        fn test_session_replace_with_subgoals() {
    356
            let mut session = create_test_session();
    357
            session.add_goal("main goal".to_string());
    358
    359
            let subgoals = vec!["subgoal1".to_string(), "subgoal2".to_string()];
    360
            session.replace_with_subgoals(subgoals);
    361
    362
            assert_eq!(session.goals.len(), 2);
    363
            // Due to .rev() then inserting at position 0, order is preserved
    364
            assert_eq!(session.goals[0].statement, "subgoal1");
    365
            assert_eq!(session.goals[1].statement, "subgoal2");
    366
        }
    367
    368
        // Test 3: Goal Operations
    369
        #[test]
    370
        fn test_get_goals() {
    371
            let mut session = create_test_session();
    372
            session.add_goal("goal1".to_string());
    373
            session.add_goal("goal2".to_string());
    374
    375
            let goals = session.get_goals();
    376
            assert_eq!(goals.len(), 2);
    377
            assert_eq!(goals[0].statement, "goal1");
    378
            assert_eq!(goals[1].statement, "goal2");
    379
        }
    380
    381
        #[test]
    382
        fn test_session_completion_status() {
    383
            let mut session = create_test_session();
    384
            assert!(session.is_complete());
    385
    386
            session.add_goal("test".to_string());
    387
            assert!(!session.is_complete());
    388
    389
            session.complete_goal();
    390
            assert!(session.is_complete());
    391
        }
    392
    393
        // Test 4: Text Export Features
    394
        #[test]
    395
        fn test_text_proof_export_empty() {
    396
            let session = create_test_session();
    397
            let text_proof = session.to_text_proof();
    398
    399
            assert!(text_proof.contains("Proof:"));
    400
            assert!(text_proof.contains("Qed."));
    401
        }
    402
    403
        #[test]
    404
        fn test_text_proof_export_with_history() {
    405
            let mut session = create_test_session();
    406
            session.history.push("apply reflexivity".to_string());
    407
            session.history.push("exact H".to_string());
    408
    409
            let text_proof = session.to_text_proof();
    410
            assert!(text_proof.contains("apply reflexivity"));
    411
            assert!(text_proof.contains("exact H"));
    412
            assert!(text_proof.contains("Qed."));
    413
        }
    414
    415
        #[test]
    416
        fn test_text_proof_export_incomplete() {
    417
            let mut session = create_test_session();
    418
            session.add_goal("incomplete goal".to_string());
    419
            session.history.push("started proof".to_string());
    420
    421
            let text_proof = session.to_text_proof();
    422
            assert!(text_proof.contains("started proof"));
    423
            assert!(!text_proof.contains("Qed.")); // Should not have Qed for incomplete proof
    424
        }
    425
    426
        #[test]
    427
        fn test_coq_proof_export() {
    428
            let session = create_test_session();
    429
            let coq_proof = session.to_coq_proof();
    430
    431
            // Currently simplified to text proof
    432
            assert!(coq_proof.contains("Proof:"));
    433
            assert!(coq_proof.contains("Qed."));
    434
        }
    435
    436
        #[test]
    437
        fn test_lean_proof_export() {
    438
            let session = create_test_session();
    439
            let lean_proof = session.to_lean_proof();
    440
    441
            // Currently simplified to text proof
    442
            assert!(lean_proof.contains("Proof:"));
    443
            assert!(lean_proof.contains("Qed."));
    444
        }
    445
    446
        // Test 5: Input Processing
    447
        #[test]
    448
        fn test_process_prove_command() {
    449
            let mut prover = create_test_prover();
    450
            let mut session = create_test_session();
    451
    452
            let result = prover.process_input(&mut session, "prove forall x, x = x").unwrap();
    453
    454
            match result {
    455
                ProofResult::Progress => {
    456
                    assert_eq!(session.goals.len(), 1);
    457
                    assert_eq!(session.current_goal().unwrap().statement, "forall x, x = x");
    458
                }
    459
                _ => panic!("Expected Progress result"),
    460
            }
    461
        }
    462
    463
        #[test]
    464
        fn test_process_empty_input() {
    465
            let mut prover = create_test_prover();
    466
            let mut session = create_test_session();
    467
    468
            let result = prover.process_input(&mut session, "").unwrap();
    469
    470
            match result {
    471
                ProofResult::Failed(msg) => {
    472
                    assert!(msg.contains("Unknown command"));
    473
                }
    474
                _ => panic!("Expected Failed result"),
    475
            }
    476
        }
    477
    478
        #[test]
    479
        fn test_process_unknown_command() {
    480
            let mut prover = create_test_prover();
    481
            let mut session = create_test_session();
    482
    483
            let result = prover.process_input(&mut session, "unknown_command arg1 arg2");
    484
    485
            // Should try to apply as tactic and fail with error
    486
            match result {
    487
                Err(e) => {
    488
                    assert!(e.to_string().contains("Unknown tactic"));
    489
                }
    490
                Ok(ProofResult::Failed(_)) => {
    491
                    // This is also acceptable
    492
                }
    493
                _ => panic!("Expected error or Failed result"),
    494
            }
    495
        }
    496
    497
        // Test 6: Proof Context
    498
        #[test]
    499
        fn test_proof_context_creation() {
    500
            let context = ProofContext::new();
    501
            assert!(context.assumptions.is_empty());
    502
            assert!(context.definitions.is_empty());
    503
        }
    504
    505
        #[test]
    506
        fn test_proof_context_default() {
    507
            let context = ProofContext::default();
    508
            assert!(context.assumptions.is_empty());
    509
            assert!(context.definitions.is_empty());
    510
        }
    511
    512
        // Test 7: Proof Goal Structure
    513
        #[test]
    514
        fn test_proof_goal_creation() {
    515
            let goal = ProofGoal {
    516
                statement: "test statement".to_string(),
    517
            };
    518
            assert_eq!(goal.statement, "test statement");
    519
        }
    520
    521
        // Test 8: Edge Cases
    522
        #[test]
    523
        fn test_complete_goal_empty_session() {
    524
            let mut session = create_test_session();
    525
            session.complete_goal(); // Should not panic
    526
            assert!(session.is_complete());
    527
        }
    528
    529
        #[test]
    530
        fn test_update_goal_empty_session() {
    531
            let mut session = create_test_session();
    532
            session.update_goal("new goal".to_string()); // Should not panic
    533
            assert!(session.is_complete());
    534
        }
    535
    536
        #[test]
    537
        fn test_replace_subgoals_empty_session() {
    538
            let mut session = create_test_session();
    539
            session.replace_with_subgoals(vec!["goal1".to_string()]); // Should not panic
    540
            assert!(session.is_complete());
    541
        }
    542
    543
        #[test]
    544
        fn test_current_goal_empty_session() {
    545
            let session = create_test_session();
    546
            assert!(session.current_goal().is_none());
    547
        }
    548
    549
        // Test 9: Serialization (Basic Structure Test)
    550
        #[test]
    551
        fn test_session_serialization_structure() {
    552
            let mut session = create_test_session();
    553
            session.add_goal("test goal".to_string());
    554
            session.context.assumptions.push("assumption1".to_string());
    555
            session.history.push("step1".to_string());
    556
    557
            // Test that all fields are accessible for serialization
    558
            assert_eq!(session.goals.len(), 1);
    559
            assert_eq!(session.context.assumptions.len(), 1);
    560
            assert_eq!(session.history.len(), 1);
    561
        }
    562
    563
        // Test 10: Multiple Session Operations
    564
        #[test]
    565
        fn test_complex_session_workflow() {
    566
            let mut session = create_test_session();
    567
    568
            // Add initial goal
    569
            session.add_goal("main theorem".to_string());
    570
            assert_eq!(session.goals.len(), 1);
    571
    572
            // Replace with subgoals
    573
            session.replace_with_subgoals(vec![
    574
                "subgoal 1".to_string(),
    575
                "subgoal 2".to_string(),
    576
                "subgoal 3".to_string(),
    577
            ]);
    578
            assert_eq!(session.goals.len(), 3);
    579
    580
            // Complete first subgoal
    581
            session.complete_goal();
    582
            assert_eq!(session.goals.len(), 2);
    583
    584
            // Update current goal
    585
            session.update_goal("modified subgoal".to_string());
    586
            assert_eq!(session.current_goal().unwrap().statement, "modified subgoal");
    587
    588
            // Complete remaining goals
    589
            session.complete_goal();
    590
            session.complete_goal();
    591
            assert!(session.is_complete());
    592
        }
    593
    }