diff --git a/examples/scripts/negation.ech b/examples/scripts/negation.ech new file mode 100644 index 0000000..28fc413 --- /dev/null +++ b/examples/scripts/negation.ech @@ -0,0 +1,28 @@ +# Stratified negation: derive isolated nodes that have no outgoing edges. +# +# This example uses negation-as-failure (NOT) in a rule body. The chase +# evaluates rules in stratified order so that Connected/1 is fully +# materialized before Isolated/1 checks for its absence. +# +# NOTE: this script requires chase_stratified(), which is available via +# the Rust API. The REPL currently runs the non-stratified chase, so +# negation here works correctly only when the negated predicate is never +# derived by another rule in the same stratum. + +fact Node(a). +fact Node(b). +fact Node(c). +fact Node(d). +fact Edge(a, b). +fact Edge(b, c). + +# Copy edges to a unary Connected predicate. +rule Edge(?X, ?Y) -> Connected(?X). + +# Nodes without outgoing edges are isolated. +# (In the REPL's single-stratum chase this fires correctly because +# Connected is derived from Edge, which is a base predicate.) +rule Node(?X), NOT Connected(?X) -> Isolated(?X). + +run. +query Isolated(?X)? diff --git a/examples/scripts/skolem_chase.ech b/examples/scripts/skolem_chase.ech new file mode 100644 index 0000000..8f25886 --- /dev/null +++ b/examples/scripts/skolem_chase.ech @@ -0,0 +1,22 @@ +# Skolem chase: deterministic labeled nulls for existential variables. +# +# With the Skolem variant, re-applying a rule with the same frontier +# bindings reuses the same null value, so the chase terminates even for +# rules that introduce existentials. Compare this with the oblivious +# variant, which generates a fresh null each round and hits the step +# limit. +# +# NOTE: the REPL uses the restricted chase by default. To run with the +# Skolem variant, use the Rust API: +# +# let result = skolem_chase(instance, &rules); + +fact Person(alice). +fact Person(bob). +fact Person(carol). + +# Every person has an id (existential Y). +rule Person(?X) -> HasId(?X, ?Y). + +run. +query HasId(?X, ?Y)? diff --git a/examples/scripts/sql_aggregate.ech b/examples/scripts/sql_aggregate.ech new file mode 100644 index 0000000..3485892 --- /dev/null +++ b/examples/scripts/sql_aggregate.ech @@ -0,0 +1,21 @@ +# Demonstrate GROUP BY with aggregate functions in the SQL frontend. + +fact Employee(alice, 30, engineering). +fact Employee(bob, 25, sales). +fact Employee(carol, 35, engineering). +fact Employee(dave, 28, marketing). +fact Employee(eve, 32, sales). + +schema Employee(name, age, dept). + +# Count all employees. +sql SELECT COUNT(*) FROM Employee; + +# Count and average age per department. +sql SELECT dept, COUNT(*) AS headcount, AVG(age) AS avg_age FROM Employee GROUP BY dept; + +# Min and max age per department. +sql SELECT dept, MIN(age), MAX(age) FROM Employee GROUP BY dept; + +# Sum of ages in engineering. +sql SELECT SUM(age) FROM Employee WHERE dept = 'engineering'; diff --git a/src/chase/inference.rs b/src/chase/inference.rs index 7b39abb..bd0bf4c 100644 --- a/src/chase/inference.rs +++ b/src/chase/inference.rs @@ -395,6 +395,7 @@ fn chase_step( for (rule_index, rule) in rules.iter().enumerate() { let matches = find_matches(instance, &rule.body); + let matches = filter_negated(instance, matches, &rule.negated_body); for subst in matches { let trigger = Trigger::new(rule_index, rule, &subst); diff --git a/src/chase/rule.rs b/src/chase/rule.rs index ec30500..3149e8c 100644 --- a/src/chase/rule.rs +++ b/src/chase/rule.rs @@ -90,13 +90,20 @@ impl Rule { impl fmt::Display for Rule { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - // Body + // Positive body for (i, atom) in self.body.iter().enumerate() { if i > 0 { write!(f, ", ")?; } write!(f, "{}", atom)?; } + // Negated body + for atom in &self.negated_body { + if !self.body.is_empty() { + write!(f, ", ")?; + } + write!(f, "NOT {}", atom)?; + } write!(f, " → ")?; // Head for (i, atom) in self.head.iter().enumerate() { diff --git a/src/execution/mod.rs b/src/execution/mod.rs index 92e3d47..bf0a19a 100644 --- a/src/execution/mod.rs +++ b/src/execution/mod.rs @@ -387,7 +387,15 @@ fn eval_expr( fn value_from_term(term: &Term) -> Result { match term { - Term::Constant(value) => Ok(Value::text(value.clone())), + Term::Constant(value) => { + // Try to interpret the constant as an integer so numeric + // aggregates (SUM, AVG) work on chase-backed data. + if let Ok(n) = value.parse::() { + Ok(Value::Integer(n)) + } else { + Ok(Value::text(value.clone())) + } + } Term::Null(_) => Ok(Value::Null), Term::Variable(_) => Err(ExecutionError::NonGroundScanTerm), } diff --git a/src/frontend/language.rs b/src/frontend/language.rs index 6d3c9b8..1635664 100644 --- a/src/frontend/language.rs +++ b/src/frontend/language.rs @@ -121,11 +121,18 @@ pub fn parse_command(input: &str) -> Result { return Err("rule body and head must both be non-empty".to_string()); } - let body = parse_atom_list(body_text)?; + let body_items = parse_body_literal_list(body_text)?; let head = parse_atom_list(head_text)?; let mut builder = RuleBuilder::new(); - for atom in body { - builder = builder.when(&atom.predicate, atom.terms); + for item in body_items { + match item { + BodyLiteral::Positive(atom) => { + builder = builder.when(&atom.predicate, atom.terms); + } + BodyLiteral::Negated(atom) => { + builder = builder.when_not(&atom.predicate, atom.terms); + } + } } for atom in head { builder = builder.then(&atom.predicate, atom.terms); @@ -187,6 +194,27 @@ fn trim_suffix(input: &str, suffix: char) -> Result<&str, String> { } } +enum BodyLiteral { + Positive(Atom), + Negated(Atom), +} + +fn parse_body_literal_list(input: &str) -> Result, String> { + split_top_level(input, ',')? + .into_iter() + .map(|s| { + let trimmed = s.trim(); + if let Some(rest) = trimmed.strip_prefix("NOT ") { + Ok(BodyLiteral::Negated(parse_atom(rest.trim())?)) + } else if let Some(rest) = trimmed.strip_prefix("not ") { + Ok(BodyLiteral::Negated(parse_atom(rest.trim())?)) + } else { + Ok(BodyLiteral::Positive(parse_atom(trimmed)?)) + } + }) + .collect() +} + fn parse_atom_list(input: &str) -> Result, String> { split_top_level(input, ',')? .into_iter()