Add a simple debugger implmenation

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 <inst> <sort>      Show query execution plan");
             println!("  :compile <inst> <sort>      Show RelAlgIR compilation");
             println!("  :chase <inst> [max_iter]    Run chase on instance axioms");
+            println!("  :debug-chase <inst> [max]   Run chase with interactive debugger");
             println!();
             println!("Solver:");
             println!("  :solve <theory> [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<usize>) {
+    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<usize> = 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<usize> = 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.

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<String>,
+    /// Mapping from Slid to element names for display
+    slid_to_name: &'a HashMap<Slid, String>,
+    /// Last binding seen (for inspect command)
+    last_binding: Option<Binding>,
+    /// 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<Slid, String>,
+        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<String> = 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 <pattern>");
+                }
+                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 <pat>, 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");
+}

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;

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<String, Slid>;
 
+/// 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<O: ChaseObserver>(
+    axioms: &[Sequent],
+    axiom_names: &[String],
+    structure: &mut Structure,
+    universe: &mut Universe,
+    sig: &Signature,
+    max_iterations: usize,
+    observer: &mut O,
+) -> Result<usize, ChaseError> {
+    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<Vec<Slid>> = 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

src/repl.rs

@@ -1279,6 +1279,9 @@ pub enum MetaCommand {
     /// Chase: run chase algorithm on instance to compute derived relations/functions
     /// `:chase <instance> [max_iterations]`
     Chase { instance: String, max_iterations: Option<usize> },
+    /// DebugChase: run chase with interactive debugger
+    /// `:debug-chase <instance> [max_iterations]`
+    DebugChase { instance: String, max_iterations: Option<usize> },
     Unknown(String),
 }
 
@@ -1436,6 +1439,17 @@ impl MetaCommand {
                     MetaCommand::Unknown(":chase requires <instance> [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 <instance> [max_iterations]".to_string())
+                }
+            }
             other => MetaCommand::Unknown(format!("Unknown command: :{}", other)),
         }
     }

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<HashMap<String, geolog::id::Slid>>,
+}
+
+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");
+}

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<Slid, String> = 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<String> = 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<Slid, String> = HashMap::new(); // Empty - no names
+    let axiom_names: Vec<String> = 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<Slid, String> = HashMap::new();
+    let axiom_names: Vec<String> = 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<Slid, String> = HashMap::new();
+    let axiom_names: Vec<String> = 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<Slid, String> = HashMap::new();
+    let axiom_names: Vec<String> = 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);
+}