From e1562beacb78684751f057af73fdeab5f5e92ad4 Mon Sep 17 00:00:00 2001 From: Hassan Abedi Date: Tue, 10 Mar 2026 13:02:19 +0100 Subject: [PATCH] WIP --- README.md | 2 + src/frontend/language.rs | 15 +++ src/frontend/mod.rs | 1 + src/frontend/provenance.rs | 264 +++++++++++++++++++++++++++++++++++++ src/frontend/session.rs | 111 ++++++++++------ src/frontend/web.rs | 4 +- 6 files changed, 356 insertions(+), 41 deletions(-) create mode 100644 src/frontend/provenance.rs diff --git a/README.md b/README.md index a6106ac..03b263a 100644 --- a/README.md +++ b/README.md @@ -99,6 +99,7 @@ fact Parent(alice, bob). rule Parent(?X, ?Y) -> Ancestor(?X, ?Y). run. query Ancestor(?X, ?Y)? +explain Ancestor(alice, carol)? show facts show rules reset @@ -109,6 +110,7 @@ Rules: - facts and rules end with `.` - queries end with `?` +- `explain ... ?` shows one derivation tree per matching answer - variables are prefixed with `?` - quoted constants are supported, for example `"alice smith"` diff --git a/src/frontend/language.rs b/src/frontend/language.rs index 1d0b9df..e41cebd 100644 --- a/src/frontend/language.rs +++ b/src/frontend/language.rs @@ -9,6 +9,7 @@ pub enum Command { Rule(Rule), Run, Query(Vec), + Explain(Vec), ShowFacts, ShowRules, Reset, @@ -82,6 +83,11 @@ pub fn parse_command(input: &str) -> Result { return Ok(Command::Query(atoms)); } + if let Some(rest) = strip_keyword(trimmed, "explain") { + let atoms = parse_atom_list(trim_suffix(rest, '?')?)?; + return Ok(Command::Explain(atoms)); + } + Err("unknown command; try `help`".to_string()) } @@ -361,6 +367,15 @@ mod tests { } } + #[test] + fn parse_explain_command() { + let command = parse_command("explain Ancestor(alice, carol)?").unwrap(); + match command { + Command::Explain(atoms) => assert_eq!(atoms.len(), 1), + other => panic!("unexpected command: {:?}", other), + } + } + #[test] fn parse_script_reports_line_numbers() { let error = parse_script("help\nbogus\nrun.").unwrap_err(); diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs index 84f00b4..f989999 100644 --- a/src/frontend/mod.rs +++ b/src/frontend/mod.rs @@ -1,6 +1,7 @@ //! Frontend utilities for interacting with chase-rs through scripts, a REPL, or a GUI. pub mod language; +pub mod provenance; pub mod repl; pub mod session; pub mod web; diff --git a/src/frontend/provenance.rs b/src/frontend/provenance.rs new file mode 100644 index 0000000..9bab970 --- /dev/null +++ b/src/frontend/provenance.rs @@ -0,0 +1,264 @@ +//! Provenance tracking for frontend query explanations. + +use std::collections::{HashMap, HashSet}; + +use crate::chase::substitution::unify_atom; +use crate::{Atom, ChaseResult, Instance, Rule, Substitution, Term}; + +const DEFAULT_MAX_STEPS: usize = 10_000; + +#[derive(Debug)] +pub struct MaterializedState { + pub result: ChaseResult, + provenance: HashMap, +} + +#[derive(Debug, Clone)] +pub enum Derivation { + Input, + Derived { + rule_index: usize, + rule: Rule, + premises: Vec, + }, +} + +#[derive(Debug, Default)] +struct NullGenerator { + counter: usize, +} + +impl NullGenerator { + fn fresh(&mut self) -> Term { + let id = self.counter; + self.counter += 1; + Term::Null(id) + } +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +struct Trigger { + rule_index: usize, + frontier_bindings: Vec<(String, Term)>, +} + +impl Trigger { + fn new(rule_index: usize, rule: &Rule, subst: &Substitution) -> Self { + let frontier = rule.frontier_variables(); + let mut bindings: Vec<_> = frontier + .into_iter() + .filter_map(|var| subst.get(&var).map(|term| (var, term.clone()))) + .collect(); + bindings.sort_by(|left, right| left.0.cmp(&right.0)); + Self { + rule_index, + frontier_bindings: bindings, + } + } +} + +#[derive(Debug)] +struct PendingFact { + fact: Atom, + derivation: Derivation, +} + +pub fn materialize(base_instance: Instance, rules: &[Rule]) -> MaterializedState { + let mut instance = base_instance; + let mut provenance = instance + .iter() + .cloned() + .map(|fact| (fact, Derivation::Input)) + .collect::>(); + let mut null_gen = NullGenerator::default(); + let mut applied_triggers = HashSet::new(); + let mut steps = 0; + + loop { + if steps >= DEFAULT_MAX_STEPS { + return MaterializedState { + result: ChaseResult { + instance, + steps, + terminated: false, + }, + provenance, + }; + } + + let derived = chase_step( + &instance, + rules, + &mut null_gen, + &mut applied_triggers, + &provenance, + ); + + if derived.is_empty() { + return MaterializedState { + result: ChaseResult { + instance, + steps, + terminated: true, + }, + provenance, + }; + } + + for pending in derived { + if instance.add(pending.fact.clone()) { + provenance.entry(pending.fact).or_insert(pending.derivation); + } + } + + steps += 1; + } +} + +pub fn explain_atom(atom: &Atom, provenance: &MaterializedState) -> String { + let mut lines = vec![atom.to_string()]; + let mut seen = HashSet::new(); + render_derivation(atom, provenance, 1, &mut seen, &mut lines); + lines.join("\n") +} + +pub fn find_matches(instance: &Instance, body: &[Atom]) -> Vec { + if body.is_empty() { + return vec![Substitution::new()]; + } + + let mut results = vec![Substitution::new()]; + + for body_atom in body { + let mut new_results = Vec::new(); + + for subst in &results { + let pattern = subst.apply_atom(body_atom); + for fact in instance.facts_for_predicate(&pattern.predicate) { + if let Some(next_subst) = unify_atom(&pattern, fact) { + let mut combined = subst.clone(); + for (var, term) in next_subst.iter() { + combined.bind(var.clone(), term.clone()); + } + new_results.push(combined); + } + } + } + + results = new_results; + } + + results +} + +impl MaterializedState { + pub fn provenance_for(&self, atom: &Atom) -> Option<&Derivation> { + self.provenance.get(atom) + } +} + +fn chase_step( + instance: &Instance, + rules: &[Rule], + null_gen: &mut NullGenerator, + applied_triggers: &mut HashSet, + provenance: &HashMap, +) -> Vec { + let mut pending = Vec::new(); + + for (rule_index, rule) in rules.iter().enumerate() { + let matches = find_matches(instance, &rule.body); + + for subst in matches { + let trigger = Trigger::new(rule_index, rule, &subst); + if applied_triggers.contains(&trigger) { + continue; + } + + if rule.existential_variables().is_empty() { + let head_facts = rule + .head + .iter() + .map(|atom| subst.apply_atom(atom)) + .collect::>(); + if head_facts.iter().all(|fact| instance.contains(fact)) { + continue; + } + } + + applied_triggers.insert(trigger); + + let premises = rule + .body + .iter() + .map(|atom| subst.apply_atom(atom)) + .collect::>(); + + for fact in apply_rule_head(rule, &subst, null_gen) { + if instance.contains(&fact) || provenance.contains_key(&fact) { + continue; + } + pending.push(PendingFact { + fact, + derivation: Derivation::Derived { + rule_index: rule_index + 1, + rule: rule.clone(), + premises: premises.clone(), + }, + }); + } + } + } + + pending +} + +fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerator) -> Vec { + let mut extended_subst = subst.clone(); + + for variable in rule.existential_variables() { + extended_subst.bind(variable, null_gen.fresh()); + } + + rule.head + .iter() + .map(|atom| extended_subst.apply_atom(atom)) + .collect() +} + +fn render_derivation( + atom: &Atom, + state: &MaterializedState, + depth: usize, + seen: &mut HashSet, + lines: &mut Vec, +) { + let indent = " ".repeat(depth); + if !seen.insert(atom.clone()) { + lines.push(format!("{}already shown", indent)); + return; + } + + match state.provenance_for(atom) { + Some(Derivation::Input) => { + lines.push(format!("{}input fact", indent)); + } + Some(Derivation::Derived { + rule_index, + rule, + premises, + }) => { + lines.push(format!( + "{}derived by rule #{}: {}", + indent, rule_index, rule + )); + for premise in premises { + lines.push(format!("{}premise: {}", indent, premise)); + render_derivation(premise, state, depth + 1, seen, lines); + } + } + None => { + lines.push(format!("{}no provenance recorded", indent)); + } + } +} diff --git a/src/frontend/session.rs b/src/frontend/session.rs index 86083ac..0aa887d 100644 --- a/src/frontend/session.rs +++ b/src/frontend/session.rs @@ -2,16 +2,16 @@ use std::fmt; -use crate::chase::substitution::unify_atom; -use crate::{Atom, ChaseResult, Instance, Rule, Substitution, chase}; +use crate::{Atom, Instance, Rule, Substitution}; use super::language::{Command, parse_script}; +use super::provenance::{MaterializedState, explain_atom, find_matches, materialize}; #[derive(Debug, Default)] pub struct Session { base_instance: Instance, rules: Vec, - materialized: Option, + materialized: Option, } impl Session { @@ -56,6 +56,7 @@ impl Session { } Command::Run => Ok(self.run_chase()), Command::Query(query) => Ok(self.run_query(&query)), + Command::Explain(query) => Ok(self.explain_query(&query)), Command::ShowFacts => Ok(self.show_facts()), Command::ShowRules => Ok(self.show_rules()), Command::Reset => { @@ -71,20 +72,20 @@ impl Session { } fn run_chase(&mut self) -> String { - let result = chase(self.base_instance.clone(), &self.rules); - let message = if result.terminated { + let state = materialize(self.base_instance.clone(), &self.rules); + let message = if state.result.terminated { format!( "Chase completed in {} step(s); {} fact(s) available.", - result.steps, - result.instance.len() + state.result.steps, + state.result.instance.len() ) } else { format!( "Chase stopped after {} step(s); result may be incomplete.", - result.steps + state.result.steps ) }; - self.materialized = Some(result); + self.materialized = Some(state); message } @@ -117,6 +118,46 @@ impl Session { rendered.join("\n") } + fn explain_query(&self, query: &[Atom]) -> String { + let instance = self.active_instance(); + let matches = find_matches(instance, query); + if matches.is_empty() { + return if self.materialized.is_none() && !self.rules.is_empty() { + "0 explanations. Run `run.` first to trace derived answers.".to_string() + } else { + "0 explanations".to_string() + }; + } + + let variables = query_variables(query); + let mut sections = Vec::new(); + + for (index, subst) in matches.iter().enumerate() { + let mut lines = Vec::new(); + lines.push(format!("match {}", index + 1)); + if !variables.is_empty() { + lines.push(format!(" {}", format_substitution(subst, &variables))); + } + + for atom in query.iter().map(|atom| subst.apply_atom(atom)) { + lines.push(format!(" answer atom: {}", atom)); + if let Some(state) = &self.materialized { + for detail in explain_atom(&atom, state).lines().skip(1) { + lines.push(format!(" {}", detail)); + } + } else { + lines.push(" input fact".to_string()); + } + } + + sections.push(lines.join("\n")); + } + + let mut output = vec![format!("{} explanation(s)", sections.len())]; + output.extend(sections); + output.join("\n") + } + fn show_facts(&self) -> String { let facts = sorted_render(self.active_instance().iter()); if facts.is_empty() { @@ -141,7 +182,7 @@ impl Session { fn active_instance(&self) -> &Instance { if let Some(result) = &self.materialized { - &result.instance + &result.result.instance } else { &self.base_instance } @@ -154,6 +195,7 @@ fact Parent(alice, bob). rule Parent(?X, ?Y) -> Ancestor(?X, ?Y). run. query Ancestor(?X, ?Y)? +explain Ancestor(alice, bob)? show facts show rules reset @@ -188,35 +230,6 @@ fn format_substitution(subst: &Substitution, variables: &[String]) -> String { .join(", ") } -fn find_matches(instance: &Instance, body: &[Atom]) -> Vec { - if body.is_empty() { - return vec![Substitution::new()]; - } - - let mut results = vec![Substitution::new()]; - - for body_atom in body { - let mut new_results = Vec::new(); - - for subst in &results { - let pattern = subst.apply_atom(body_atom); - for fact in instance.facts_for_predicate(&pattern.predicate) { - if let Some(next_subst) = unify_atom(&pattern, fact) { - let mut combined = subst.clone(); - for (var, term) in next_subst.iter() { - combined.bind(var.clone(), term.clone()); - } - new_results.push(combined); - } - } - } - - results = new_results; - } - - results -} - #[cfg(test)] mod tests { use super::*; @@ -248,4 +261,24 @@ mod tests { .unwrap(); assert!(output.ends_with("true")); } + + #[test] + fn explain_query_shows_rule_trace() { + let mut session = Session::new(); + let output = session + .execute_script( + "fact Parent(alice, bob).\n\ + fact Parent(bob, carol).\n\ + rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).\n\ + rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z).\n\ + run.\n\ + explain Ancestor(alice, carol)?", + ) + .unwrap(); + + assert!(output.contains("explanation(s)")); + assert!(output.contains("derived by rule #2")); + assert!(output.contains("premise: Ancestor(alice, bob)")); + assert!(output.contains("input fact")); + } } diff --git a/src/frontend/web.rs b/src/frontend/web.rs index 4f25335..9ff49c6 100644 --- a/src/frontend/web.rs +++ b/src/frontend/web.rs @@ -248,12 +248,12 @@ fact Parent(bob, carol). rule Parent(?X, ?Y) -> Ancestor(?X, ?Y). rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z). run. -query Ancestor(?X, ?Y)? +explain Ancestor(alice, carol)?
-

Try show facts, show rules, or boolean queries like query Parent(alice, bob)?.

+

Try query Ancestor(?X, ?Y)?, explain Ancestor(alice, carol)?, or boolean queries like query Parent(alice, bob)?.