From 7a57c6daef70fc98607efa54ae6e2e835d992223 Mon Sep 17 00:00:00 2001 From: Hassan Abedi Date: Thu, 19 Mar 2026 17:42:04 +0100 Subject: [PATCH] Add a simple debugger implmenation --- src/bin/geolog.rs | 100 ++++++++++++++ src/debugger.rs | 291 +++++++++++++++++++++++++++++++++++++++++ src/lib.rs | 1 + src/query/chase.rs | 185 ++++++++++++++++++++++++++ src/repl.rs | 14 ++ tests/unit_chase.rs | 142 +++++++++++++++++++- tests/unit_debugger.rs | 93 +++++++++++++ 7 files changed, 825 insertions(+), 1 deletion(-) create mode 100644 src/debugger.rs create mode 100644 tests/unit_debugger.rs diff --git a/src/bin/geolog.rs b/src/bin/geolog.rs index 6785a7e..6ba4e34 100644 --- a/src/bin/geolog.rs +++ b/src/bin/geolog.rs @@ -254,6 +254,9 @@ fn handle_command(state: &mut ReplState, cmd: MetaCommand) -> bool { MetaCommand::Chase { instance, max_iterations } => { handle_chase(state, &instance, max_iterations); } + MetaCommand::DebugChase { instance, max_iterations } => { + handle_debug_chase(state, &instance, max_iterations); + } MetaCommand::Unknown(msg) => { eprintln!("Error: {}", msg); eprintln!("Type :help for available commands"); @@ -342,6 +345,7 @@ fn print_help(topic: Option<&str>) { println!(" :explain Show query execution plan"); println!(" :compile Show RelAlgIR compilation"); println!(" :chase [max_iter] Run chase on instance axioms"); + println!(" :debug-chase [max] Run chase with interactive debugger"); println!(); println!("Solver:"); println!(" :solve [budget_ms] Find model of theory from scratch"); @@ -1078,6 +1082,102 @@ fn handle_chase(state: &mut ReplState, instance_name: &str, max_iterations: Opti } } +/// Handle :debug-chase command - run chase with interactive debugger +fn handle_debug_chase(state: &mut ReplState, instance_name: &str, max_iterations: Option) { + use geolog::core::RelationStorage; + use geolog::debugger::InteractiveDebugger; + use geolog::query::chase::chase_fixpoint_with_observer; + + // Get the instance + let entry = match state.instances.get_mut(instance_name) { + Some(e) => e, + None => { + eprintln!("Instance '{}' not found", instance_name); + return; + } + }; + + // Get the theory + let theory = match state.theories.get(&entry.theory_name) { + Some(t) => t.clone(), + None => { + eprintln!("Theory '{}' not found", entry.theory_name); + return; + } + }; + + let sig = &theory.theory.signature; + let axioms = &theory.theory.axioms; + let axiom_names = &theory.theory.axiom_names; + + if axioms.is_empty() { + println!("Theory '{}' has no axioms to chase.", entry.theory_name); + return; + } + + println!("Starting debug chase on instance '{}' (theory '{}')", instance_name, entry.theory_name); + println!("{} axiom(s) to process", axioms.len()); + println!("Type 'help' for debugger commands.\n"); + + // Snapshot relation tuple counts before chase + let tuple_counts_before: Vec = entry.structure.relations + .iter() + .map(|r| r.len()) + .collect(); + + // Create debugger with element name mapping + let mut debugger = InteractiveDebugger::new(&entry.slid_to_name, axiom_names); + + // Run the chase with observer + let max_iter = max_iterations.unwrap_or(100); + + match chase_fixpoint_with_observer( + axioms, + axiom_names, + &mut entry.structure, + &mut state.store.universe, + sig, + max_iter, + &mut debugger, + ) { + Ok(iterations) => { + println!("\nStructure after chase:"); + print_structure_summary(&entry.structure, sig); + + // Check if any new tuples were added + let tuple_counts_after: Vec = entry.structure.relations + .iter() + .map(|r| r.len()) + .collect(); + let tuples_added = tuple_counts_before.iter() + .zip(tuple_counts_after.iter()) + .any(|(before, after)| after > before); + + // Save info needed for persistence before dropping entry borrow + let theory_name_owned = entry.theory_name.clone(); + + if tuples_added { + if let Err(e) = persist_chase_results( + state, + instance_name, + &theory_name_owned, + ) { + eprintln!("Warning: Failed to persist chase results: {}", e); + } else { + println!("Chase results persisted to store."); + } + } + + if iterations == 0 { + println!("\nChase stopped by user."); + } + } + Err(e) => { + eprintln!("✗ Chase error: {}", e); + } + } +} + /// Persist chase results (relation tuples) to columnar batches as IDB data. /// /// IDB batches are persisted locally but NOT transmitted over the wire. diff --git a/src/debugger.rs b/src/debugger.rs new file mode 100644 index 0000000..2b4fc72 --- /dev/null +++ b/src/debugger.rs @@ -0,0 +1,291 @@ +//! Interactive debugger for the chase algorithm. +//! +//! Provides step-through debugging, breakpoints, and variable inspection +//! for understanding chase execution. + +use std::collections::{HashMap, HashSet}; +use std::io::{self, Write}; + +use crate::id::Slid; +use crate::query::chase::{Binding, ChaseControl, ChaseEvent, ChaseObserver}; + +/// Debug mode controlling execution flow +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum DebugMode { + /// Continue until breakpoint or completion + Continue, + /// Step to next axiom firing + Step, + /// Step to next iteration + StepIteration, +} + +/// Interactive debugger for chase execution +pub struct InteractiveDebugger<'a> { + /// Current debug mode + mode: DebugMode, + /// Breakpoints on axiom name patterns + breakpoints: HashSet, + /// Mapping from Slid to element names for display + slid_to_name: &'a HashMap, + /// Last binding seen (for inspect command) + last_binding: Option, + /// Axiom names for display + axiom_names: &'a [String], + /// Current iteration number + current_iteration: usize, + /// Whether we should stop (user quit) + should_stop: bool, +} + +impl<'a> InteractiveDebugger<'a> { + /// Create a new interactive debugger + pub fn new( + slid_to_name: &'a HashMap, + axiom_names: &'a [String], + ) -> Self { + Self { + mode: DebugMode::Step, // Start in step mode + breakpoints: HashSet::new(), + slid_to_name, + last_binding: None, + axiom_names, + current_iteration: 0, + should_stop: false, + } + } + + /// Format a binding for display using element names + pub fn format_binding(&self, binding: &Binding) -> String { + if binding.is_empty() { + return "(empty)".to_string(); + } + + let mut parts: Vec = binding + .iter() + .map(|(var, slid)| { + let elem_name = self + .slid_to_name + .get(slid) + .map(|s| s.as_str()) + .unwrap_or_else(|| "?"); + format!("{}={}", var, elem_name) + }) + .collect(); + parts.sort(); // Consistent ordering + parts.join(", ") + } + + /// Check if an axiom name matches any breakpoint pattern + fn matches_breakpoint(&self, axiom_name: Option<&str>) -> bool { + let Some(name) = axiom_name else { + return false; + }; + + self.breakpoints.iter().any(|pattern| { + // Simple substring matching for now + name.contains(pattern) + }) + } + + /// Process a debugger command + fn process_command(&mut self, cmd: &str) -> bool { + let parts: Vec<&str> = cmd.trim().split_whitespace().collect(); + let command = parts.first().map(|s| *s).unwrap_or(""); + + match command { + "s" | "step" => { + self.mode = DebugMode::Step; + true // Continue execution + } + "c" | "continue" => { + self.mode = DebugMode::Continue; + true + } + "n" | "next" => { + self.mode = DebugMode::StepIteration; + true + } + "b" | "break" => { + if let Some(pattern) = parts.get(1) { + self.breakpoints.insert(pattern.to_string()); + println!("Breakpoint set on axioms matching '{}'", pattern); + } else { + println!("Usage: break "); + } + false // Don't continue, wait for another command + } + "d" | "delete" => { + if let Some(pattern) = parts.get(1) { + if self.breakpoints.remove(*pattern) { + println!("Breakpoint '{}' removed", pattern); + } else { + println!("No breakpoint matching '{}'", pattern); + } + } else { + self.breakpoints.clear(); + println!("All breakpoints cleared"); + } + false + } + "i" | "inspect" => { + if let Some(binding) = &self.last_binding { + println!("Current binding: {}", self.format_binding(binding)); + } else { + println!("No binding available"); + } + false + } + "l" | "list" => { + if self.breakpoints.is_empty() { + println!("No breakpoints set"); + } else { + println!("Breakpoints:"); + for bp in &self.breakpoints { + println!(" - {}", bp); + } + } + println!("\nAxioms:"); + for (i, name) in self.axiom_names.iter().enumerate() { + let display_name = if name.is_empty() { "(unnamed)" } else { name.as_str() }; + println!(" #{}: {}", i, display_name); + } + false + } + "q" | "quit" => { + self.should_stop = true; + true + } + "h" | "help" | "?" => { + print_help(); + false + } + "" => false, // Empty line, just reprompt + _ => { + println!("Unknown command: '{}'. Type 'help' for available commands.", command); + false + } + } + } + + /// Wait for user input and process commands + fn prompt(&mut self) -> ChaseControl { + loop { + print!("(chase-dbg) "); + io::stdout().flush().ok(); + + let mut input = String::new(); + if io::stdin().read_line(&mut input).is_err() { + self.should_stop = true; + return ChaseControl::Stop; + } + + let should_continue = self.process_command(&input); + + if self.should_stop { + return ChaseControl::Stop; + } + + if should_continue { + return ChaseControl::Continue; + } + } + } +} + +impl<'a> ChaseObserver for InteractiveDebugger<'a> { + fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl { + if self.should_stop { + return ChaseControl::Stop; + } + + match event { + ChaseEvent::IterationStart { iteration } => { + self.current_iteration = iteration; + println!("\n--- Iteration {} ---", iteration); + ChaseControl::Continue + } + + ChaseEvent::AxiomFiring { + axiom_index, + axiom_name, + binding, + violation_count, + } => { + // Store binding for inspect command + self.last_binding = Some(binding.clone()); + + let name_display = axiom_name.unwrap_or("(unnamed)"); + println!( + "Firing axiom #{}: {} ({} violations)", + axiom_index, name_display, violation_count + ); + println!(" Binding: {}", self.format_binding(binding)); + + // Check if we should stop + let should_prompt = match self.mode { + DebugMode::Step => true, + DebugMode::Continue => self.matches_breakpoint(axiom_name), + DebugMode::StepIteration => false, + }; + + if should_prompt { + if self.matches_breakpoint(axiom_name) { + println!(" [Breakpoint hit]"); + } + self.prompt() + } else { + ChaseControl::Continue + } + } + + ChaseEvent::AxiomFired { + axiom_index: _, + axiom_name: _, + changed, + } => { + if changed { + println!(" -> Structure changed"); + } + ChaseControl::Continue + } + + ChaseEvent::IterationEnd { + iteration, + changed, + } => { + if !changed { + println!("Iteration {} complete (no changes - fixpoint reached)", iteration); + } else { + println!("Iteration {} complete (structure changed)", iteration); + } + + // In StepIteration mode, prompt at end of iteration + if self.mode == DebugMode::StepIteration { + self.prompt() + } else { + ChaseControl::Continue + } + } + + ChaseEvent::ChaseComplete { iterations } => { + println!("\nChase complete after {} iterations.", iterations); + ChaseControl::Continue + } + } + } +} + +fn print_help() { + println!("Chase Debugger Commands:"); + println!(); + println!(" step, s Step to next axiom firing"); + println!(" continue, c Continue until breakpoint or completion"); + println!(" next, n Step to next iteration"); + println!(" break , b Set breakpoint on axioms matching pattern"); + println!(" delete [pat], d Remove breakpoint (all if no pattern)"); + println!(" inspect, i Show current variable binding"); + println!(" list, l List breakpoints and axioms"); + println!(" quit, q Stop the chase"); + println!(" help, h, ? Show this help"); +} diff --git a/src/lib.rs b/src/lib.rs index e5f8c89..1f95507 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -6,6 +6,7 @@ pub mod ast; pub mod cc; pub mod core; +pub mod debugger; pub mod elaborate; pub mod error; pub mod id; diff --git a/src/query/chase.rs b/src/query/chase.rs index aa3ee5d..b471402 100644 --- a/src/query/chase.rs +++ b/src/query/chase.rs @@ -84,6 +84,46 @@ impl std::error::Error for ChaseError {} /// Variable binding: maps variable names to Slids pub type Binding = HashMap; +/// Events emitted during chase execution +#[derive(Clone, Debug)] +pub enum ChaseEvent<'a> { + IterationStart { iteration: usize }, + AxiomFiring { + axiom_index: usize, + axiom_name: Option<&'a str>, + binding: &'a Binding, + violation_count: usize, + }, + AxiomFired { + axiom_index: usize, + axiom_name: Option<&'a str>, + changed: bool, + }, + IterationEnd { iteration: usize, changed: bool }, + ChaseComplete { iterations: usize }, +} + +/// Control signal returned by observer to control chase execution +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum ChaseControl { + Continue, + Stop, +} + +/// Observer trait for monitoring chase execution +pub trait ChaseObserver { + fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl; +} + +/// Null observer that does nothing (default for regular chase) +pub struct NullObserver; + +impl ChaseObserver for NullObserver { + fn on_event(&mut self, _: ChaseEvent<'_>) -> ChaseControl { + ChaseControl::Continue + } +} + /// Execute one step of the chase algorithm. /// /// Iterates over all axioms, evaluates premises using the tensor system, @@ -707,4 +747,149 @@ pub fn chase_fixpoint( Ok(iterations) } +/// Run the chase algorithm with an observer for debugging/monitoring. +/// +/// This is the instrumented version that calls `observer.on_event()` at key points: +/// - Start of each iteration +/// - Before firing each axiom (with binding) +/// - After firing each axiom (with changed flag) +/// - End of each iteration +/// - Chase completion +/// +/// The observer can return `ChaseControl::Stop` to halt execution early. +/// +/// # Arguments +/// +/// * `axioms` - The sequents (axioms) to apply +/// * `axiom_names` - Names for axioms (for display in debugger) +/// * `structure` - The structure to modify +/// * `universe` - The universe for element creation +/// * `sig` - The signature +/// * `max_iterations` - Safety limit to prevent infinite loops +/// * `observer` - The observer to receive events +/// +/// # Returns +/// +/// The number of iterations taken, or error if chase failed or was stopped. +pub fn chase_fixpoint_with_observer( + axioms: &[Sequent], + axiom_names: &[String], + structure: &mut Structure, + universe: &mut Universe, + sig: &Signature, + max_iterations: usize, + observer: &mut O, +) -> Result { + let mut cc = CongruenceClosure::new(); + let mut iterations = 0; + + loop { + if iterations >= max_iterations { + return Err(ChaseError::MaxIterationsExceeded(max_iterations)); + } + + // Notify iteration start + if observer.on_event(ChaseEvent::IterationStart { iteration: iterations + 1 }) == ChaseControl::Stop { + return Ok(iterations); + } + + let mut iteration_changed = false; + + // Fire axiom conclusions with observer notifications + for (axiom_idx, axiom) in axioms.iter().enumerate() { + let axiom_name = axiom_names.get(axiom_idx).map(|n| n.as_str()).filter(|s| !s.is_empty()); + + // Check the axiom - if compilation fails due to unsupported patterns, skip silently + let violations = match check_sequent(axiom, structure, sig) { + Ok(CheckResult::Satisfied) => continue, + Ok(CheckResult::Violated(vs)) => vs, + Err(_) => continue, + }; + + if violations.is_empty() { + continue; + } + + // Build index→Slid lookup for each context variable + let index_to_slid: Vec> = axiom.context.vars.iter() + .map(|(_, sort)| carrier_to_slid_vec(structure, sort)) + .collect(); + + // Map from variable name to its position in the context + let var_to_ctx_idx: HashMap<&str, usize> = axiom.context.vars.iter() + .enumerate() + .map(|(i, (name, _))| (name.as_str(), i)) + .collect(); + + // Fire conclusion for each violation + for violation in &violations { + // Build binding from violation assignment + let binding: Binding = violation.variable_names.iter() + .enumerate() + .filter_map(|(tensor_idx, var_name)| { + let ctx_idx = var_to_ctx_idx.get(var_name.as_str())?; + let slid_vec = &index_to_slid[*ctx_idx]; + let tensor_val = violation.assignment.get(tensor_idx)?; + let slid = slid_vec.get(*tensor_val)?; + Some((var_name.clone(), *slid)) + }) + .collect(); + + // Notify before firing + if observer.on_event(ChaseEvent::AxiomFiring { + axiom_index: axiom_idx, + axiom_name, + binding: &binding, + violation_count: violations.len(), + }) == ChaseControl::Stop { + return Ok(iterations); + } + + // Fire conclusion with this binding + let changed = match fire_conclusion(&axiom.conclusion, &binding, structure, &mut cc, universe, sig) { + Ok(c) => c, + Err(_) => false, // Skip unsupported conclusions + }; + + iteration_changed |= changed; + + // Notify after firing + if observer.on_event(ChaseEvent::AxiomFired { + axiom_index: axiom_idx, + axiom_name, + changed, + }) == ChaseControl::Stop { + return Ok(iterations); + } + } + } + + // Propagate pending equations in CC + let eq_changed = propagate_equations(structure, &mut cc, sig); + iteration_changed |= eq_changed; + + iterations += 1; + + // Notify iteration end + if observer.on_event(ChaseEvent::IterationEnd { + iteration: iterations, + changed: iteration_changed, + }) == ChaseControl::Stop { + return Ok(iterations); + } + + if !iteration_changed { + break; + } + } + + // Canonicalize structure to reflect CC merges + canonicalize_structure(structure, &mut cc); + + // Notify chase completion + observer.on_event(ChaseEvent::ChaseComplete { iterations }); + + Ok(iterations) +} + // Tests are in tests/unit_chase.rs diff --git a/src/repl.rs b/src/repl.rs index 7482da8..b380738 100644 --- a/src/repl.rs +++ b/src/repl.rs @@ -1279,6 +1279,9 @@ pub enum MetaCommand { /// Chase: run chase algorithm on instance to compute derived relations/functions /// `:chase [max_iterations]` Chase { instance: String, max_iterations: Option }, + /// DebugChase: run chase with interactive debugger + /// `:debug-chase [max_iterations]` + DebugChase { instance: String, max_iterations: Option }, Unknown(String), } @@ -1436,6 +1439,17 @@ impl MetaCommand { MetaCommand::Unknown(":chase requires [max_iterations]".to_string()) } } + "debug-chase" => { + if let Some(instance_name) = arg { + let max_iterations = parts.next().and_then(|s| s.parse().ok()); + MetaCommand::DebugChase { + instance: instance_name.to_string(), + max_iterations, + } + } else { + MetaCommand::Unknown(":debug-chase requires [max_iterations]".to_string()) + } + } other => MetaCommand::Unknown(format!("Unknown command: :{}", other)), } } diff --git a/tests/unit_chase.rs b/tests/unit_chase.rs index 55d514a..004af53 100644 --- a/tests/unit_chase.rs +++ b/tests/unit_chase.rs @@ -3,8 +3,9 @@ use geolog::core::{ Context, DerivedSort, Formula, RelationStorage, Sequent, Signature, Structure, Term, Theory, }; -use geolog::query::chase::chase_fixpoint; +use geolog::query::chase::{chase_fixpoint, chase_fixpoint_with_observer, ChaseEvent, ChaseControl, ChaseObserver}; use geolog::universe::Universe; +use std::collections::HashMap; /// Create a simple test theory with one sort and one unary relation fn simple_theory_with_relation() -> Theory { @@ -424,3 +425,142 @@ fn test_chase_existential_premise() { println!("Chase with existential premise completed in {} iterations", iterations); } + +/// A test observer that counts events +struct CountingObserver { + iteration_starts: usize, + axiom_firings: usize, + axiom_fired: usize, + iteration_ends: usize, + complete: usize, + last_binding: Option>, +} + +impl CountingObserver { + fn new() -> Self { + Self { + iteration_starts: 0, + axiom_firings: 0, + axiom_fired: 0, + iteration_ends: 0, + complete: 0, + last_binding: None, + } + } +} + +impl ChaseObserver for CountingObserver { + fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl { + match event { + ChaseEvent::IterationStart { .. } => self.iteration_starts += 1, + ChaseEvent::AxiomFiring { binding, .. } => { + self.axiom_firings += 1; + self.last_binding = Some(binding.clone()); + } + ChaseEvent::AxiomFired { .. } => self.axiom_fired += 1, + ChaseEvent::IterationEnd { .. } => self.iteration_ends += 1, + ChaseEvent::ChaseComplete { .. } => self.complete += 1, + } + ChaseControl::Continue + } +} + +#[test] +fn test_chase_with_observer() { + // Test that the observer-based chase works and receives events + let theory = preorder_theory(); + let mut universe = Universe::new(); + let mut structure = Structure::new(1); + + // Add 2 elements + structure.add_element(&mut universe, 0); + structure.add_element(&mut universe, 0); + + // Initialize relation with arity 2 + structure.init_relations(&[2]); + + let mut observer = CountingObserver::new(); + + let iterations = chase_fixpoint_with_observer( + &theory.axioms, + &theory.axiom_names, + &mut structure, + &mut universe, + &theory.signature, + 100, + &mut observer, + ).unwrap(); + + // Should complete with events + assert_eq!(iterations, 2); + assert!(observer.iteration_starts >= 1, "Should have at least 1 iteration start"); + assert!(observer.axiom_firings >= 2, "Should have at least 2 axiom firings (reflexivity for 2 elements)"); + assert_eq!(observer.complete, 1, "Should have exactly 1 completion event"); + + // Check that reflexive pairs were added + let relation = structure.get_relation(0); + assert_eq!(relation.len(), 2, "Should have 2 reflexive tuples"); +} + +/// An observer that stops after a fixed number of firings +struct StoppingObserver { + max_firings: usize, + firing_count: usize, +} + +impl StoppingObserver { + fn new(max_firings: usize) -> Self { + Self { + max_firings, + firing_count: 0, + } + } +} + +impl ChaseObserver for StoppingObserver { + fn on_event(&mut self, event: ChaseEvent<'_>) -> ChaseControl { + if let ChaseEvent::AxiomFiring { .. } = event { + self.firing_count += 1; + if self.firing_count >= self.max_firings { + return ChaseControl::Stop; + } + } + ChaseControl::Continue + } +} + +#[test] +fn test_chase_observer_can_stop() { + // Test that returning ChaseControl::Stop halts the chase + let theory = preorder_theory(); + let mut universe = Universe::new(); + let mut structure = Structure::new(1); + + // Add 5 elements - would normally produce 5 reflexive pairs + for _ in 0..5 { + structure.add_element(&mut universe, 0); + } + + // Initialize relation with arity 2 + structure.init_relations(&[2]); + + // Stop after just 2 firings + // Note: The stop happens when the 2nd firing event is received, before the 2nd tuple is added + // So we expect only 1 tuple (from the first firing) + let mut observer = StoppingObserver::new(2); + + let _iterations = chase_fixpoint_with_observer( + &theory.axioms, + &theory.axiom_names, + &mut structure, + &mut universe, + &theory.signature, + 100, + &mut observer, + ).unwrap(); + + // Should have stopped early - only 1 tuple (the 2nd firing was interrupted before execution) + let relation = structure.get_relation(0); + assert!(relation.len() < 5, "Should have fewer than 5 tuples after early stop"); + assert_eq!(observer.firing_count, 2, "Should have stopped after exactly 2 firings"); +} diff --git a/tests/unit_debugger.rs b/tests/unit_debugger.rs new file mode 100644 index 0000000..a1f66ab --- /dev/null +++ b/tests/unit_debugger.rs @@ -0,0 +1,93 @@ +//! Unit tests for the chase debugger + +use std::collections::HashMap; +use geolog::debugger::InteractiveDebugger; +use geolog::id::{NumericId, Slid}; +use geolog::query::chase::{Binding, ChaseControl, ChaseEvent, ChaseObserver}; + +/// Test that format_binding correctly displays bindings with element names +#[test] +fn test_format_binding_with_names() { + let mut slid_to_name: HashMap = HashMap::new(); + slid_to_name.insert(Slid::from_usize(0), "alice".to_string()); + slid_to_name.insert(Slid::from_usize(1), "bob".to_string()); + slid_to_name.insert(Slid::from_usize(2), "charlie".to_string()); + + let axiom_names: Vec = vec!["ax/test".to_string()]; + let debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names); + + let mut binding: Binding = HashMap::new(); + binding.insert("x".to_string(), Slid::from_usize(0)); + binding.insert("y".to_string(), Slid::from_usize(1)); + + let formatted = debugger.format_binding(&binding); + + // Should contain both variable bindings with element names + assert!(formatted.contains("x=alice"), "Should contain x=alice, got: {}", formatted); + assert!(formatted.contains("y=bob"), "Should contain y=bob, got: {}", formatted); +} + +/// Test that format_binding handles unknown elements gracefully +#[test] +fn test_format_binding_unknown_elements() { + let slid_to_name: HashMap = HashMap::new(); // Empty - no names + let axiom_names: Vec = vec![]; + let debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names); + + let mut binding: Binding = HashMap::new(); + binding.insert("x".to_string(), Slid::from_usize(42)); + + let formatted = debugger.format_binding(&binding); + + // Should show "?" for unknown element + assert!(formatted.contains("x=?"), "Should contain x=? for unknown element, got: {}", formatted); +} + +/// Test that format_binding handles empty bindings +#[test] +fn test_format_binding_empty() { + let slid_to_name: HashMap = HashMap::new(); + let axiom_names: Vec = vec![]; + let debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names); + + let binding: Binding = HashMap::new(); + let formatted = debugger.format_binding(&binding); + + assert_eq!(formatted, "(empty)"); +} + +/// Test that observer responds to iteration events +#[test] +fn test_debugger_iteration_events() { + let slid_to_name: HashMap = HashMap::new(); + let axiom_names: Vec = vec!["ax/refl".to_string()]; + let mut debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names); + + // Iteration start should continue + let result = debugger.on_event(ChaseEvent::IterationStart { iteration: 1 }); + assert_eq!(result, ChaseControl::Continue); + + // Iteration end should continue (in default step mode, but no prompt in test) + let result = debugger.on_event(ChaseEvent::IterationEnd { iteration: 1, changed: false }); + assert_eq!(result, ChaseControl::Continue); + + // Chase complete should continue + let result = debugger.on_event(ChaseEvent::ChaseComplete { iterations: 1 }); + assert_eq!(result, ChaseControl::Continue); +} + +/// Test that axiom fired events are handled +#[test] +fn test_debugger_axiom_fired_event() { + let slid_to_name: HashMap = HashMap::new(); + let axiom_names: Vec = vec!["ax/refl".to_string()]; + let mut debugger = InteractiveDebugger::new(&slid_to_name, &axiom_names); + + // AxiomFired should always continue (it's informational) + let result = debugger.on_event(ChaseEvent::AxiomFired { + axiom_index: 0, + axiom_name: Some("ax/refl"), + changed: true, + }); + assert_eq!(result, ChaseControl::Continue); +}