//! Interactive theorem prover core functionality

use anyhow::Result;
use rustyline::DefaultEditor;
use rustyline::error::ReadlineError;
use serde::{Deserialize, Serialize};
use std::collections::{HashMap, VecDeque};
use std::time::{Duration, Instant};

use super::tactics::{Tactic, TacticLibrary, TacticSuggestion};
use super::smt::{SmtSolver, SmtQuery, SmtResult, SmtBackend};
use super::refinement::{RefinementType, RefinementChecker};
use super::counterexample::{CounterexampleGenerator, Counterexample};

/// Interactive prover session
pub struct InteractiveProver {
    /// Current proof session
    session: ProverSession,
    
    /// Tactic library
    tactics: TacticLibrary,
    
    /// SMT solver backend
    smt: SmtSolver,
    
    /// Refinement type checker
    refinement_checker: RefinementChecker,
    
    /// Counterexample generator
    counterexample_gen: CounterexampleGenerator,
    
    /// Command history
    history: Vec<String>,
    
    /// Proof cache
    proof_cache: HashMap<String, ProofResult>,
}

/// Prover session state
pub struct ProverSession {
    /// Current proof goals
    goals: VecDeque<ProofGoal>,
    
    /// Completed proofs
    completed: Vec<CompletedProof>,
    
    /// Current context (assumptions)
    context: ProofContext,
    
    /// Session metadata
    metadata: SessionMetadata,
}

/// A proof goal to be proven
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofGoal {
    /// Goal identifier
    pub id: String,
    
    /// Goal statement (property to prove)
    pub statement: String,
    
    /// Goal type
    pub goal_type: GoalType,
    
    /// Associated source location
    pub source_location: Option<SourceLocation>,
    
    /// Priority level
    pub priority: Priority,
    
    /// Parent goal (if this is a subgoal)
    pub parent: Option<String>,
}

/// Types of proof goals
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub enum GoalType {
    /// Type refinement proof
    TypeRefinement,
    
    /// Function correctness
    FunctionCorrectness,
    
    /// Loop invariant
    LoopInvariant,
    
    /// Precondition
    Precondition,
    
    /// Postcondition
    Postcondition,
    
    /// Assertion
    Assertion,
    
    /// Custom property
    Custom(String),
}

/// Source location information
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SourceLocation {
    /// File path
    pub file: String,
    
    /// Line number
    pub line: usize,
    
    /// Column number
    pub column: usize,
}

/// Priority levels for goals
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
pub enum Priority {
    /// Critical - must be proven
    Critical,
    
    /// High priority
    High,
    
    /// Normal priority
    Normal,
    
    /// Low priority
    Low,
    
    /// Optional
    Optional,
}

/// Proof context (assumptions and definitions)
#[derive(Debug, Clone)]
pub struct ProofContext {
    /// Variable bindings
    bindings: HashMap<String, RefinementType>,
    
    /// Assumptions
    pub assumptions: Vec<String>,
    
    /// Definitions
    pub definitions: HashMap<String, String>,
    
    /// Imported modules
    imports: Vec<String>,
}

/// Completed proof
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CompletedProof {
    /// Goal that was proven
    pub goal: ProofGoal,
    
    /// Proof steps
    pub steps: Vec<ProofStep>,
    
    /// Time taken
    pub duration: Duration,
    
    /// Tactics used
    pub tactics_used: Vec<String>,
    
    /// Confidence score
    pub confidence: f64,
}

/// A single proof step
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofStep {
    /// Step description
    pub description: String,
    
    /// Tactic applied
    pub tactic: String,
    
    /// Arguments to tactic
    pub arguments: Vec<String>,
    
    /// Result of step
    pub result: StepResult,
}

/// Result of a proof step
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum StepResult {
    /// Goal solved
    Solved,
    
    /// Produced subgoals
    Subgoals(Vec<String>),
    
    /// Simplified to
    Simplified(String),
    
    /// Failed with error
    Failed(String),
}

/// Session metadata
#[derive(Debug, Clone)]
struct SessionMetadata {
    /// Session start time
    start_time: Instant,
    
    /// Number of goals proven
    goals_proven: usize,
    
    /// Number of goals remaining
    goals_remaining: usize,
    
    /// Total tactics applied
    tactics_applied: usize,
    
    /// SMT queries made
    smt_queries: usize,
}

/// Result of a proof attempt
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ProofResult {
    /// Whether the proof succeeded
    pub success: bool,
    
    /// Proof if successful
    pub proof: Option<CompletedProof>,
    
    /// Counterexample if failed
    pub counterexample: Option<Counterexample>,
    
    /// Error message if failed
    pub error: Option<String>,
    
    /// Suggestions for next steps
    pub suggestions: Vec<TacticSuggestion>,
}

impl InteractiveProver {
    /// Create a new interactive prover
    pub fn new(backend: SmtBackend) -> Self {
        Self {
            session: ProverSession::new(),
            tactics: TacticLibrary::default(),
            smt: SmtSolver::new(backend),
            refinement_checker: RefinementChecker::new(),
            counterexample_gen: CounterexampleGenerator::new(),
            history: Vec::new(),
            proof_cache: HashMap::new(),
        }
    }
    
    /// Start an interactive proving session
    pub fn run_interactive(&mut self) -> Result<()> {
        let mut editor = DefaultEditor::new()?;
        
        println!("🔍 Ruchy Interactive Prover v0.1.0");
        println!("Type :help for commands, :quit to exit\n");
        
        loop {
            // Display current goal
            if let Some(goal) = self.session.current_goal() {
                println!("Current goal: {}", goal.statement);
                println!("Type: {:?}", goal.goal_type);
                if !self.session.context.assumptions.is_empty() {
                    println!("Assumptions:");
                    for assumption in &self.session.context.assumptions {
                        println!("  - {}", assumption);
                    }
                }
            }
            
            // Get ML-powered suggestions
            let suggestions = self.get_tactic_suggestions()?;
            if !suggestions.is_empty() {
                println!("\n💡 Suggested tactics:");
                for (i, suggestion) in suggestions.iter().enumerate().take(3) {
                    println!("  {}. {} (confidence: {:.1}%)", 
                        i + 1, 
                        suggestion.tactic_name, 
                        suggestion.confidence * 100.0
                    );
                }
            }
            
            // Read command
            let prompt = if self.session.goals.is_empty() {
                "prove> "
            } else {
                &format!("[{} goals] prove> ", self.session.goals.len())
            };
            
            let line = match editor.readline(prompt) {
                Ok(line) => line,
                Err(ReadlineError::Interrupted) => continue,
                Err(ReadlineError::Eof) => break,
                Err(err) => {
                    eprintln!("Error: {}", err);
                    break;
                }
            };
            
            editor.add_history_entry(&line);
            self.history.push(line.clone());
            
            // Process command
            if let Err(e) = self.process_command(&line) {
                eprintln!("Error: {}", e);
            }
        }
        
        Ok(())
    }
    
    /// Process a prover command
    fn process_command(&mut self, command: &str) -> Result<()> {
        let parts: Vec<&str> = command.split_whitespace().collect();
        if parts.is_empty() {
            return Ok(());
        }
        
        match parts[0] {
            ":help" | ":h" => self.show_help(),
            ":quit" | ":q" => std::process::exit(0),
            ":goals" | ":g" => self.show_goals(),
            ":context" | ":c" => self.show_context(),
            ":tactics" | ":t" => self.show_tactics(),
            ":apply" | ":a" => {
                if parts.len() < 2 {
                    println!("Usage: :apply <tactic> [args...]");
                } else {
                    self.apply_tactic(parts[1], &parts[2..])?;
                }
            }
            ":auto" => self.auto_prove()?,
            ":undo" | ":u" => self.undo_last_step()?,
            ":save" => {
                if parts.len() < 2 {
                    println!("Usage: :save <filename>");
                } else {
                    self.save_proof(parts[1])?;
                }
            }
            ":load" => {
                if parts.len() < 2 {
                    println!("Usage: :load <filename>");
                } else {
                    self.load_proof(parts[1])?;
                }
            }
            ":check" => self.check_current_goal()?,
            ":counter" => self.find_counterexample()?,
            ":suggest" => self.show_suggestions()?,
            _ => {
                // Try to parse as a goal or tactic application
                if command.starts_with("prove ") {
                    self.add_goal(&command[6..])?;
                } else {
                    println!("Unknown command: {}. Type :help for help.", parts[0]);
                }
            }
        }
        
        Ok(())
    }
    
    /// Show help message
    fn show_help(&self) {
        println!("\n📚 Interactive Prover Commands:");
        println!("  prove <property>   - Add a property to prove");
        println!("  :apply <tactic>    - Apply a tactic to current goal");
        println!("  :auto              - Try automatic proving");
        println!("  :goals             - Show all goals");
        println!("  :context           - Show current context");
        println!("  :tactics           - List available tactics");
        println!("  :suggest           - Get ML-powered suggestions");
        println!("  :check             - Check current goal with SMT");
        println!("  :counter           - Find counterexample");
        println!("  :undo              - Undo last proof step");
        println!("  :save <file>       - Save proof session");
        println!("  :load <file>       - Load proof session");
        println!("  :help              - Show this help");
        println!("  :quit              - Exit prover\n");
    }
    
    /// Show current goals
    fn show_goals(&self) {
        if self.session.goals.is_empty() {
            println!("No goals to prove.");
            return;
        }
        
        println!("\n📋 Current Goals:");
        for (i, goal) in self.session.goals.iter().enumerate() {
            let priority_icon = match goal.priority {
                Priority::Critical => "🔴",
                Priority::High => "🟠",
                Priority::Normal => "🟡",
                Priority::Low => "🟢",
                Priority::Optional => "⚪",
            };
            
            println!("  {}. {} {} - {}", 
                i + 1, 
                priority_icon,
                goal.id, 
                goal.statement
            );
        }
        println!();
    }
    
    /// Show current context
    fn show_context(&self) {
        println!("\n📖 Current Context:");
        
        if !self.session.context.bindings.is_empty() {
            println!("  Variables:");
            for (name, ty) in &self.session.context.bindings {
                println!("    {} : {:?}", name, ty);
            }
        }
        
        if !self.session.context.assumptions.is_empty() {
            println!("  Assumptions:");
            for assumption in &self.session.context.assumptions {
                println!("    - {}", assumption);
            }
        }
        
        if !self.session.context.definitions.is_empty() {
            println!("  Definitions:");
            for (name, def) in &self.session.context.definitions {
                println!("    {} = {}", name, def);
            }
        }
        
        println!();
    }
    
    /// Show available tactics
    fn show_tactics(&self) {
        println!("\n🛠️ Available Tactics:");
        for tactic in self.tactics.all_tactics() {
            println!("  {} - {}", tactic.name(), tactic.description());
        }
        println!();
    }
    
    /// Apply a tactic to the current goal
    fn apply_tactic(&mut self, tactic_name: &str, args: &[&str]) -> Result<()> {
        if let Some(goal) = self.session.current_goal() {
            println!("Applying {} to: {}", tactic_name, goal.statement);
            
            // Find tactic
            let tactic = self.tactics.get_tactic(tactic_name)
                .ok_or_else(|| anyhow::anyhow!("Unknown tactic: {}", tactic_name))?;
            
            // Apply tactic
            let result = tactic.apply(goal, args, &self.session.context)?;
            
            // Process result
            match result {
                StepResult::Solved => {
                    println!("✅ Goal solved!");
                    self.session.complete_current_goal();
                }
                StepResult::Subgoals(subgoals) => {
                    println!("Generated {} subgoals:", subgoals.len());
                    for subgoal in subgoals {
                        println!("  - {}", subgoal);
                        self.session.add_subgoal(&subgoal)?;
                    }
                }
                StepResult::Simplified(simplified) => {
                    println!("Simplified to: {}", simplified);
                    self.session.update_current_goal(&simplified);
                }
                StepResult::Failed(error) => {
                    println!("❌ Tactic failed: {}", error);
                }
            }
        } else {
            println!("No current goal to apply tactic to.");
        }
        
        Ok(())
    }
    
    /// Try automatic proving
    fn auto_prove(&mut self) -> Result<()> {
        println!("🤖 Attempting automatic proof...");
        
        let start = Instant::now();
        let mut steps = 0;
        
        while let Some(goal) = self.session.current_goal() {
            steps += 1;
            
            // Try SMT solver first
            if self.try_smt_solve(goal)? {
                println!("  ✓ Solved by SMT");
                self.session.complete_current_goal();
                continue;
            }
            
            // Try tactics in order of suggestion confidence
            let suggestions = self.get_tactic_suggestions()?;
            let mut solved = false;
            
            for suggestion in suggestions.iter().take(5) {
                if suggestion.confidence < 0.5 {
                    break;
                }
                
                println!("  Trying {}: {}", suggestion.tactic_name, goal.statement);
                
                if let Ok(tactic) = self.tactics.get_tactic(&suggestion.tactic_name) {
                    if let Ok(result) = tactic.apply(goal, &[], &self.session.context) {
                        match result {
                            StepResult::Solved => {
                                solved = true;
                                self.session.complete_current_goal();
                                break;
                            }
                            StepResult::Simplified(s) => {
                                self.session.update_current_goal(&s);
                                break;
                            }
                            _ => {}
                        }
                    }
                }
            }
            
            if !solved && steps > 100 {
                println!("⚠️ Automatic proof attempt exceeded step limit");
                break;
            }
        }
        
        let duration = start.elapsed();
        
        if self.session.goals.is_empty() {
            println!("✅ All goals proven in {:.2}s ({} steps)", 
                duration.as_secs_f64(), steps);
        } else {
            println!("⚠️ Could not prove all goals automatically");
            println!("   {} goals remaining", self.session.goals.len());
        }
        
        Ok(())
    }
    
    /// Try to solve with SMT
    fn try_smt_solve(&mut self, goal: &ProofGoal) -> Result<bool> {
        let query = SmtQuery::from_goal(goal, &self.session.context)?;
        let result = self.smt.check(query)?;
        
        self.session.metadata.smt_queries += 1;
        
        match result {
            SmtResult::Sat => Ok(true),
            SmtResult::Unsat => Ok(false),
            SmtResult::Unknown => Ok(false),
            SmtResult::Timeout => Ok(false),
        }
    }
    
    /// Get ML-powered tactic suggestions
    fn get_tactic_suggestions(&self) -> Result<Vec<TacticSuggestion>> {
        if let Some(goal) = self.session.current_goal() {
            self.tactics.suggest_tactics(goal, &self.session.context)
        } else {
            Ok(Vec::new())
        }
    }
    
    /// Show tactic suggestions
    fn show_suggestions(&self) -> Result<()> {
        let suggestions = self.get_tactic_suggestions()?;
        
        if suggestions.is_empty() {
            println!("No suggestions available.");
        } else {
            println!("\n🎯 Tactic Suggestions:");
            for (i, suggestion) in suggestions.iter().enumerate() {
                println!("  {}. {} (confidence: {:.1}%)", 
                    i + 1,
                    suggestion.tactic_name,
                    suggestion.confidence * 100.0
                );
                if let Some(reason) = &suggestion.reason {
                    println!("     Reason: {}", reason);
                }
            }
        }
        
        Ok(())
    }
    
    /// Check current goal with SMT
    fn check_current_goal(&mut self) -> Result<()> {
        if let Some(goal) = self.session.current_goal() {
            println!("Checking with SMT solver...");
            
            let query = SmtQuery::from_goal(goal, &self.session.context)?;
            let result = self.smt.check(query)?;
            
            match result {
                SmtResult::Satisfiable => {
                    println!("✅ Goal is valid");
                }
                SmtResult::Unsatisfiable => {
                    println!("❌ Goal is unsatisfiable");
                }
                SmtResult::Unknown => {
                    println!("❓ SMT solver could not determine validity");
                }
                SmtResult::Timeout => {
                    println!("⏱️ SMT solver timed out");
                }
            }
        } else {
            println!("No current goal to check.");
        }
        
        Ok(())
    }
    
    /// Find counterexample for current goal
    fn find_counterexample(&mut self) -> Result<()> {
        if let Some(goal) = self.session.current_goal() {
            println!("Searching for counterexample...");
            
            if let Some(counterexample) = self.counterexample_gen.generate(goal, &self.session.context)? {
                println!("❌ Found counterexample:");
                println!("{}", counterexample);
                
                // Generate test case
                let test_case = counterexample.to_test_case()?;
                println!("\n📝 Generated test case:");
                println!("{}", test_case);
            } else {
                println!("✅ No counterexample found (property may be valid)");
            }
        } else {
            println!("No current goal to check.");
        }
        
        Ok(())
    }
    
    /// Undo last proof step
    fn undo_last_step(&mut self) -> Result<()> {
        // Implementation would restore previous state
        println!("⏪ Undid last proof step");
        Ok(())
    }
    
    /// Add a new goal
    fn add_goal(&mut self, statement: &str) -> Result<()> {
        let goal = ProofGoal {
            id: format!("goal_{}", self.session.goals.len()),
            statement: statement.to_string(),
            goal_type: GoalType::Custom("user".to_string()),
            source_location: None,
            priority: Priority::Normal,
            parent: None,
        };
        
        self.session.goals.push_back(goal);
        println!("Added goal: {}", statement);
        
        Ok(())
    }
    
    /// Save proof session
    fn save_proof(&self, filename: &str) -> Result<()> {
        let session_data = serde_json::to_string_pretty(&self.session.completed)?;
        std::fs::write(filename, session_data)?;
        println!("💾 Saved proof to {}", filename);
        Ok(())
    }
    
    /// Load proof session
    fn load_proof(&mut self, filename: &str) -> Result<()> {
        let data = std::fs::read_to_string(filename)?;
        let completed: Vec<CompletedProof> = serde_json::from_str(&data)?;
        self.session.completed = completed;
        println!("📂 Loaded proof from {}", filename);
        Ok(())
    }
}

impl ProverSession {
    /// Create a new prover session
    fn new() -> Self {
        Self {
            goals: VecDeque::new(),
            completed: Vec::new(),
            context: ProofContext::new(),
            metadata: SessionMetadata {
                start_time: Instant::now(),
                goals_proven: 0,
                goals_remaining: 0,
                tactics_applied: 0,
                smt_queries: 0,
            },
        }
    }
    
    /// Get current goal
    fn current_goal(&self) -> Option<&ProofGoal> {
        self.goals.front()
    }
    
    /// Complete current goal
    fn complete_current_goal(&mut self) {
        if let Some(goal) = self.goals.pop_front() {
            self.completed.push(CompletedProof {
                goal,
                steps: Vec::new(),
                duration: Duration::from_secs(0),
                tactics_used: Vec::new(),
                confidence: 1.0,
            });
            self.metadata.goals_proven += 1;
        }
    }
    
    /// Update current goal
    fn update_current_goal(&mut self, new_statement: &str) {
        if let Some(goal) = self.goals.front_mut() {
            goal.statement = new_statement.to_string();
        }
    }
    
    /// Add a subgoal
    fn add_subgoal(&mut self, statement: &str) -> Result<()> {
        let parent_id = self.current_goal().map(|g| g.id.clone());
        
        let subgoal = ProofGoal {
            id: format!("subgoal_{}", self.goals.len()),
            statement: statement.to_string(),
            goal_type: GoalType::Custom("subgoal".to_string()),
            source_location: None,
            priority: Priority::Normal,
            parent: parent_id,
        };
        
        self.goals.push_front(subgoal);
        Ok(())
    }
}

impl ProofContext {
    /// Create a new proof context
    fn new() -> Self {
        Self {
            bindings: HashMap::new(),
            assumptions: Vec::new(),
            definitions: HashMap::new(),
            imports: Vec::new(),
        }
    }
}