Improve the frontend UI (REPL, TUI, and the web UI)

AGENTS.md

@@ -6,7 +6,7 @@ This file provides guidance to coding agents collaborating on this repository.
 
 Query Engine is an experimental Rust project for building query-engine
 components. The current implementation is centered on a chase-based reasoning
-core, lightweight interactive frontends, and an early relational/SQL scaffold.
+core, interactive frontends, and an early relational/SQL scaffold.
 
 Priorities, in order:
 
@@ -55,7 +55,7 @@ Quick examples:
     - `inference.rs`: shared matching, negation filtering, and provenance-aware materialization helpers.
     - `stratification.rs`: stratification analysis for rules with negation.
     - `union_find.rs`: equality merging support.
-- `src/frontend/`: lightweight interactive surface for scripts, REPL, local web UI, TUI (behind `tui` feature), and syntax highlighting.
+- `src/frontend/`: interactive surface for scripts, REPL, local web UI, TUI (behind `tui` feature), and syntax highlighting.
 - `src/relational/`: schemas, values, rows, and result sets for relational execution.
 - `src/catalog/`: predicate-to-table schema inference and catalog access.
 - `src/io/`: CSV-based fact import and export.
@@ -76,7 +76,7 @@ Quick examples:
 - The current SQL support is intentionally narrow: `SELECT-FROM-WHERE-GROUP BY-ORDER BY-LIMIT` over predicate-backed tables; equality and inequality predicates combined with `AND` and `OR`; comma-join style multi-table queries; table aliases; ordering by output-column names; integer and string literals; `COUNT`, `SUM`, `MIN`, `MAX`, and `AVG` aggregates with optional `GROUP BY`.
 - Stable SQL column names come from explicit catalog registration or the frontend `schema ...` command, including for empty tables; otherwise the default names are positional such as `c0` and `c1`.
 - Single-table SQL queries may use the table name as a qualifier when no alias is present.
-- Do not describe unsupported SQL features such as aggregates, grouping, or arbitrary expressions as implemented.
+- Do not describe unsupported SQL features (such as subqueries, window functions, or arbitrary expressions) as implemented.
 - The executor operates on the `DataSource` trait, not on `Instance` directly. `Instance` and `TableStore` are the two built-in implementations.
 - Relational and SQL modules should build on explicit schemas and logical plans, not call frontend helpers directly.
 - If you add parser, planner, or executor layers, keep their responsibilities separate.

README.md

@@ -2,7 +2,7 @@
 
 An experimental Rust project for building query-engine components.
 
-Right now the repository is centered on a chase-based reasoning core, a small
+Right now the repository is centered on a chase-based reasoning core, an
 interactive frontend, and an early relational/SQL scaffold. The broader target
 shape is a query engine with clearer front-end, planning, optimization, and
 execution boundaries.
@@ -15,8 +15,8 @@ execution boundaries.
 - Provenance-oriented explanations for derived answers
 - Script, REPL, local web UI, and optional TUI for experimentation (all with syntax highlighting)
 - Relational schema, catalog, logical-plan, and execution scaffolding
-- Physical operator scaffolding with a small rule-based rewrite layer
+- Physical operator scaffolding with a rule-based rewrite layer
-- A minimal SQL slice for `SELECT-FROM-WHERE-GROUP BY-ORDER BY-LIMIT` queries over predicate-backed tables, including `COUNT`, `SUM`, `MIN`, `MAX`, and `AVG` aggregates
+- A SQL slice for `SELECT-FROM-WHERE-GROUP BY-ORDER BY-LIMIT` queries over predicate-backed tables, including `COUNT`, `SUM`, `MIN`, `MAX`, and `AVG` aggregates
 - Filter push-down across joins in the physical rewrite pass
 
 ### Architecture
@@ -28,7 +28,7 @@ The repository is currently organized around a few clear subsystems:
 - `src/frontend/`: REPL, script, GUI, and explanation rendering
 - `src/relational/`: schemas, values, rows, and result sets
 - `src/catalog/`: predicate-backed table metadata
-- `src/sql/`: minimal SQL AST and parser
+- `src/sql/`: SQL AST and parser
 - `src/planner/`: logical plan structures and SQL-to-plan translation
 - `src/execution/`: execution for the current logical-plan subset, the `DataSource` trait, the `TableStore`, and a physical operator layer with rule-based rewrites
 
@@ -102,16 +102,22 @@ cargo run -- script examples/scripts/sql_join.ech
 cargo run --features tui -- tui
 ```
 
-#### REPL language
+#### REPL Language
 
 ```text
 fact Parent(alice, bob).
 rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
+rule Node(?X), NOT Connected(?X) -> Isolated(?X).
 schema Parent(parent, child).
 sql SELECT * FROM Parent;
 run.
 query Ancestor(?X, ?Y)?
 explain Ancestor(alice, carol)?
+set chase skolem
+set semi-naive on
+load /path/to/csv/dir
+save /path/to/csv/dir
+source examples/scripts/ancestor.ech
 show facts
 show rules
 reset
@@ -124,7 +130,7 @@ The repository now has a narrow SQL pipeline with:
 
 - predicate-backed catalog inference
 - relational schemas, rows, and values
-- SQL parsing for a small subset
+- SQL parsing for the supported subset
 - logical planning
 - execution for filtering, ordering, limiting, and basic multi-table joins
 

examples/scripts/README.md

@@ -11,8 +11,12 @@ Available examples:
 
 - `ancestor.ech`: transitive closure over `Parent/2`
 - `employee_departments.ech`: existential rule that creates labeled nulls
+- `negation.ech`: stratified negation-as-failure with `NOT` in rule bodies
 - `same_team.ech`: conjunctive query with a self-join
+- `skolem_chase.ech`: Skolem chase with deterministic labeled nulls
+- `sql_aggregate.ech`: `GROUP BY` with `COUNT`, `SUM`, `MIN`, `MAX`, and `AVG`
 - `sql_basic.ech`: named-column filtering in the SQL frontend
+- `sql_filter_ops.ech`: inequality, `OR`, `LIMIT`, and integer literals
 - `sql_join.ech`: multi-table SQL join over predicate-backed tables
 - `sql_self_join.ech`: self-join with SQL table aliases
 - `sql_order_by.ech`: ordered SQL output with `ORDER BY`

src/chase/engine.rs

@@ -205,12 +205,12 @@ pub fn chase_stratified(instance: Instance, rules: &[Rule], config: ChaseConfig)
         total_steps += result.steps;
         current_instance = result.instance;
 
-        if let Some(error) = result.error {
+        if !result.terminated || result.error.is_some() {
             return ChaseResult {
                 instance: current_instance,
                 steps: total_steps,
                 terminated: false,
-                error: Some(error),
+                error: result.error,
             };
         }
     }

src/chase/inference.rs

@@ -137,6 +137,67 @@ struct PendingFact {
 }
 
 pub fn materialize(base_instance: Instance, rules: &[Rule]) -> MaterializedState {
+    let has_negation = rules.iter().any(|r| r.has_negation());
+    if has_negation {
+        return materialize_stratified(base_instance, rules);
+    }
+    materialize_flat(base_instance, rules)
+}
+
+fn materialize_stratified(base_instance: Instance, rules: &[Rule]) -> MaterializedState {
+    use super::stratification::stratify;
+
+    let strata = match stratify(rules) {
+        Ok(s) => s,
+        Err(_) => {
+            // Unstratifiable: fall back to flat materialization.
+            return materialize_flat(base_instance, rules);
+        }
+    };
+
+    let mut instance = base_instance;
+    let mut provenance: HashMap<Atom, Derivation> = instance
+        .iter()
+        .cloned()
+        .map(|fact| (fact, Derivation::Input))
+        .collect();
+    let mut total_steps = 0;
+
+    for stratum_indexes in &strata {
+        let stratum_rules: Vec<Rule> = stratum_indexes.iter().map(|&i| rules[i].clone()).collect();
+
+        let state = materialize_flat(instance, &stratum_rules);
+        total_steps += state.result.steps;
+        instance = state.result.instance;
+        for (atom, derivation) in state.provenance {
+            provenance.entry(atom).or_insert(derivation);
+        }
+
+        if !state.result.terminated {
+            return MaterializedState {
+                result: ChaseResult {
+                    instance,
+                    steps: total_steps,
+                    terminated: false,
+                    error: state.result.error,
+                },
+                provenance,
+            };
+        }
+    }
+
+    MaterializedState {
+        result: ChaseResult {
+            instance,
+            steps: total_steps,
+            terminated: true,
+            error: None,
+        },
+        provenance,
+    }
+}
+
+fn materialize_flat(base_instance: Instance, rules: &[Rule]) -> MaterializedState {
     let mut instance = base_instance;
     let mut provenance = instance
         .iter()
@@ -289,10 +350,11 @@ impl MaterializedState {
 
 /// Filter a set of body-match substitutions against negated atoms.
 ///
-/// A substitution is removed if, after applying it to any negated atom, the
+/// A substitution is removed if, after applying it to any negated atom, any
-/// resulting ground atom exists in the instance. This implements
+/// matching ground fact exists in the instance. When the substitution
-/// negation-as-failure semantics: the negated atom must be absent for the
+/// leaves unbound variables in a negated atom, the check uses pattern
-/// rule to fire.
+/// matching against the instance (existential semantics: the negated atom
+/// blocks if any witness exists).
 pub(crate) fn filter_negated(
     instance: &Instance,
     results: Vec<Substitution>,
@@ -305,8 +367,14 @@ pub(crate) fn filter_negated(
         .into_iter()
         .filter(|subst| {
             negated_body.iter().all(|atom| {
-                let ground = subst.apply_atom(atom);
+                let applied = subst.apply_atom(atom);
-                !instance.contains(&ground)
+                if applied.is_ground() {
+                    !instance.contains(&applied)
+                } else {
+                    // Unbound variables remain: check whether any matching
+                    // fact exists via pattern matching.
+                    instance.facts_matching_pattern(&applied).is_empty()
+                }
             })
         })
         .collect()
@@ -441,3 +509,67 @@ fn term_null_id(term: &Term) -> Option<usize> {
         _ => None,
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn filter_negated_blocks_when_fact_present() {
+        let instance: Instance = vec![
+            Atom::new("A", vec![Term::constant("x")]),
+            Atom::new("B", vec![Term::constant("x")]),
+        ]
+        .into_iter()
+        .collect();
+
+        let mut subst = Substitution::new();
+        subst.bind("X".into(), Term::constant("x"));
+
+        let negated = vec![Atom::new("B", vec![Term::var("X")])];
+        let result = filter_negated(&instance, vec![subst], &negated);
+        assert!(result.is_empty());
+    }
+
+    #[test]
+    fn filter_negated_passes_when_fact_absent() {
+        let instance: Instance = vec![Atom::new("A", vec![Term::constant("x")])]
+            .into_iter()
+            .collect();
+
+        let mut subst = Substitution::new();
+        subst.bind("X".into(), Term::constant("x"));
+
+        let negated = vec![Atom::new("B", vec![Term::var("X")])];
+        let result = filter_negated(&instance, vec![subst], &negated);
+        assert_eq!(result.len(), 1);
+    }
+
+    #[test]
+    fn filter_negated_handles_unbound_variables() {
+        // NOT Q(X, Y) where Y is not bound. Should block if any Q(x, _) exists.
+        let instance: Instance = vec![
+            Atom::new("A", vec![Term::constant("x")]),
+            Atom::new("Q", vec![Term::constant("x"), Term::constant("anything")]),
+        ]
+        .into_iter()
+        .collect();
+
+        let mut subst = Substitution::new();
+        subst.bind("X".into(), Term::constant("x"));
+        // Y is NOT bound
+
+        let negated = vec![Atom::new("Q", vec![Term::var("X"), Term::var("Y")])];
+        let result = filter_negated(&instance, vec![subst], &negated);
+        // Should be blocked because Q(x, anything) exists
+        assert!(result.is_empty());
+    }
+
+    #[test]
+    fn filter_negated_passes_empty_negated_body() {
+        let instance = Instance::new();
+        let subst = Substitution::new();
+        let result = filter_negated(&instance, vec![subst], &[]);
+        assert_eq!(result.len(), 1);
+    }
+}

src/chase/stratification.rs

@@ -47,6 +47,22 @@ impl Error for StratificationError {}
 /// dependencies) upward. Rules without negation all land in stratum 0 when
 /// there are no dependency chains through negation.
 pub fn stratify(rules: &[Rule]) -> Result<Vec<Vec<usize>>, StratificationError> {
+    // Reject rules that have negated body atoms but no positive body atoms.
+    // Such rules cannot anchor to the instance and are not supported by
+    // standard stratified evaluation.
+    for rule in rules {
+        if rule.body.is_empty() && !rule.negated_body.is_empty() {
+            let preds: Vec<String> = rule
+                .negated_body
+                .iter()
+                .map(|a| a.predicate.clone())
+                .collect();
+            return Err(StratificationError {
+                cycle_predicates: preds,
+            });
+        }
+    }
+
     // Collect all predicates.
     let mut all_predicates: HashSet<String> = HashSet::new();
     for rule in rules {
@@ -219,4 +235,18 @@ mod tests {
         let result = stratify(&rules);
         assert!(result.is_err());
     }
+
+    #[test]
+    fn rejects_rule_with_only_negated_body() {
+        // NOT A(X) -> B(X) has no positive body atoms.
+        let rules = vec![
+            RuleBuilder::new()
+                .when_not("A", vec![Term::var("X")])
+                .then("B", vec![Term::var("X")])
+                .build(),
+        ];
+
+        let result = stratify(&rules);
+        assert!(result.is_err());
+    }
 }

src/execution/mod.rs

@@ -485,4 +485,53 @@ mod tests {
         let result = instance.scan("Missing", &schema).unwrap();
         assert_eq!(result.rows().len(), 0);
     }
+
+    #[test]
+    fn value_from_term_parses_integer_constants() {
+        assert_eq!(
+            value_from_term(&Term::constant("42")).unwrap(),
+            Value::Integer(42)
+        );
+        assert_eq!(
+            value_from_term(&Term::constant("alice")).unwrap(),
+            Value::text("alice")
+        );
+        assert_eq!(value_from_term(&Term::Null(0)).unwrap(), Value::Null);
+        assert!(value_from_term(&Term::var("X")).is_err());
+    }
+
+    #[test]
+    fn aggregate_execution_count_and_sum() {
+        let schema = Schema::new(vec![
+            Field::new("dept", DataType::Text, false),
+            Field::new("salary", DataType::Integer, false),
+        ]);
+        let rows = vec![
+            Row::new(vec![Value::text("eng"), Value::Integer(100)]),
+            Row::new(vec![Value::text("eng"), Value::Integer(200)]),
+            Row::new(vec![Value::text("sales"), Value::Integer(50)]),
+        ];
+
+        let aggregates = vec![
+            PlanAggregateExpr {
+                name: "__agg_0".into(),
+                func: AggregateFunc::Count,
+                arg: None,
+            },
+            PlanAggregateExpr {
+                name: "__agg_1".into(),
+                func: AggregateFunc::Sum,
+                arg: Some("salary".into()),
+            },
+        ];
+        let result = compute_aggregate(&rows, &schema, &["dept".into()], &aggregates).unwrap();
+        assert_eq!(result.len(), 2);
+        // Each row: [dept, count, sum]
+        let eng = result
+            .iter()
+            .find(|r| r.values()[0] == Value::text("eng"))
+            .unwrap();
+        assert_eq!(eng.values()[1], Value::Integer(2));
+        assert_eq!(eng.values()[2], Value::Integer(300));
+    }
 }

src/frontend/highlight.rs

@@ -118,7 +118,7 @@ pub fn highlight_line(line: &str) -> Vec<HighlightToken> {
             continue;
         }
 
-        // Variable (?X) — must be checked before the single-char operator set
+        // Variable (?X): must be checked before the single-char operator set
         // since `?` also appears there for standalone query terminators.
         if ch == '?' && i + 1 < len && (chars[i + 1].is_alphanumeric() || chars[i + 1] == '_') {
             let start = i;
@@ -171,7 +171,9 @@ fn classify_word(word: &str, is_first_word: bool) -> TokenKind {
     if is_first_word {
         match upper.as_str() {
             "FACT" | "RULE" | "RUN" | "QUERY" | "EXPLAIN" | "SHOW" | "RESET" | "HELP"
-            | "SCHEMA" | "SQL" => return TokenKind::Command,
+            | "SCHEMA" | "SQL" | "SET" | "LOAD" | "SAVE" | "SOURCE" => {
+                return TokenKind::Command;
+            }
             _ => {}
         }
     }
@@ -181,7 +183,7 @@ fn classify_word(word: &str, is_first_word: bool) -> TokenKind {
         "SELECT" | "FROM" | "WHERE" | "GROUP" | "BY" | "ORDER" | "LIMIT" | "AS" | "AND" | "OR"
         | "ASC" | "DESC" | "NULL" | "NOT" | "ON" | "JOIN" | "INNER" | "LEFT" | "RIGHT"
         | "OUTER" | "HAVING" | "DISTINCT" | "INSERT" | "UPDATE" | "DELETE" | "CREATE" | "DROP"
-        | "TABLE" | "INTO" | "VALUES" | "SET" => {
+        | "TABLE" | "INTO" | "VALUES" => {
             return TokenKind::SqlKeyword;
         }
         _ => {}

src/frontend/language.rs

@@ -16,6 +16,10 @@ pub enum Command {
     Explain(Vec<Atom>),
     ShowFacts,
     ShowRules,
+    Set { key: String, value: String },
+    Load(String),
+    Save(String),
+    Source(String),
     Reset,
     Help,
 }
@@ -150,6 +154,41 @@ pub fn parse_command(input: &str) -> Result<Command, String> {
         return Ok(Command::Explain(atoms));
     }
 
+    if let Some(rest) = strip_keyword(trimmed, "set") {
+        let rest = rest.trim_end_matches('.');
+        let (key, value) = rest
+            .split_once(char::is_whitespace)
+            .ok_or_else(|| "set requires a key and value (e.g., `set chase skolem`)".to_string())?;
+        return Ok(Command::Set {
+            key: key.trim().to_ascii_lowercase(),
+            value: value.trim().to_ascii_lowercase(),
+        });
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "load") {
+        let path = rest.trim().trim_end_matches('.');
+        if path.is_empty() {
+            return Err("load requires a directory path".to_string());
+        }
+        return Ok(Command::Load(path.to_string()));
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "save") {
+        let path = rest.trim().trim_end_matches('.');
+        if path.is_empty() {
+            return Err("save requires a directory path".to_string());
+        }
+        return Ok(Command::Save(path.to_string()));
+    }
+
+    if let Some(rest) = strip_keyword(trimmed, "source") {
+        let path = rest.trim().trim_end_matches('.');
+        if path.is_empty() {
+            return Err("source requires a file path".to_string());
+        }
+        return Ok(Command::Source(path.to_string()));
+    }
+
     Err("unknown command; try `help`".to_string())
 }
 
@@ -163,6 +202,14 @@ fn command_is_complete(input: &str) -> bool {
         || trimmed.eq_ignore_ascii_case("show rules")
         || trimmed.eq_ignore_ascii_case("reset")
         || trimmed.eq_ignore_ascii_case("help")
+        || starts_with_keyword(trimmed, "set")
+        || starts_with_keyword(trimmed, "load")
+        || starts_with_keyword(trimmed, "save")
+        || starts_with_keyword(trimmed, "source")
+}
+
+fn starts_with_keyword(input: &str, keyword: &str) -> bool {
+    strip_keyword(input, keyword).is_some()
 }
 
 fn strip_keyword<'a>(input: &'a str, keyword: &str) -> Option<&'a str> {
@@ -598,4 +645,19 @@ mod tests {
         let error = parse_script("help\nbogus\nrun.").unwrap_err();
         assert!(error.contains("line 2"));
     }
+
+    #[test]
+    fn parse_rule_with_negation() {
+        let command = parse_command("rule Node(?X), NOT Connected(?X) -> Isolated(?X).").unwrap();
+        match command {
+            Command::Rule(rule) => {
+                assert_eq!(rule.body.len(), 1);
+                assert_eq!(rule.body[0].predicate, "Node");
+                assert_eq!(rule.negated_body.len(), 1);
+                assert_eq!(rule.negated_body[0].predicate, "Connected");
+                assert_eq!(rule.head.len(), 1);
+            }
+            other => panic!("unexpected command: {:?}", other),
+        }
+    }
 }

src/frontend/session.rs

@@ -2,12 +2,14 @@
 
 use std::collections::HashMap;
 use std::fmt;
+use std::path::Path;
 
 use crate::catalog::{CatalogError, PredicateCatalog};
 use crate::chase::{
-    Atom, Instance, MaterializedState, Rule, Substitution, find_matches, materialize,
+    Atom, ChaseVariant, Instance, MaterializedState, Rule, Substitution, find_matches, materialize,
 };
 use crate::execution::execute;
+use crate::io::csv;
 use crate::planner::sql::plan_select;
 use crate::relational::{DataType, Field, ResultSet, Schema};
 
@@ -20,6 +22,8 @@ pub struct Session {
     rules: Vec<Rule>,
     column_names: HashMap<String, Vec<String>>,
     materialized: Option<MaterializedState>,
+    chase_variant: ChaseVariant,
+    semi_naive: bool,
 }
 
 impl Session {
@@ -79,6 +83,10 @@ impl Session {
             Command::Explain(query) => Ok(self.explain_query(&query)),
             Command::ShowFacts => Ok(self.show_facts()),
             Command::ShowRules => Ok(self.show_rules()),
+            Command::Set { key, value } => self.apply_setting(&key, &value),
+            Command::Load(path) => self.load_csv(&path),
+            Command::Save(path) => self.save_csv(&path),
+            Command::Source(path) => self.run_source(&path),
             Command::Reset => {
                 *self = Self::default();
                 Ok("Session reset.".to_string())
@@ -91,6 +99,76 @@ impl Session {
         *self = Self::default();
     }
 
+    fn apply_setting(&mut self, key: &str, value: &str) -> Result<String, String> {
+        match key {
+            "chase" => {
+                self.chase_variant = match value {
+                    "restricted" => ChaseVariant::Restricted,
+                    "standard" => ChaseVariant::Standard,
+                    "oblivious" => ChaseVariant::Oblivious,
+                    "skolem" => ChaseVariant::Skolem,
+                    _ => {
+                        return Err(format!(
+                            "unknown chase variant `{}`; expected restricted, standard, oblivious, or skolem",
+                            value
+                        ));
+                    }
+                };
+                self.materialized = None;
+                Ok(format!("Chase variant set to {}.", value))
+            }
+            "semi-naive" => {
+                self.semi_naive = match value {
+                    "on" | "true" | "yes" | "1" => true,
+                    "off" | "false" | "no" | "0" => false,
+                    _ => {
+                        return Err(format!(
+                            "expected on or off for semi-naive, got `{}`",
+                            value
+                        ));
+                    }
+                };
+                self.materialized = None;
+                Ok(format!(
+                    "Semi-naive evaluation {}.",
+                    if self.semi_naive {
+                        "enabled"
+                    } else {
+                        "disabled"
+                    }
+                ))
+            }
+            _ => Err(format!(
+                "unknown setting `{}`; try `set chase <variant>` or `set semi-naive on|off`",
+                key
+            )),
+        }
+    }
+
+    fn load_csv(&mut self, path: &str) -> Result<String, String> {
+        let dir = Path::new(path);
+        let loaded = csv::load_directory(dir).map_err(|e| e.to_string())?;
+        let count = loaded.len();
+        for atom in loaded.iter().cloned() {
+            self.base_instance.add(atom);
+        }
+        self.materialized = None;
+        Ok(format!("Loaded {} fact(s) from {}.", count, path))
+    }
+
+    fn save_csv(&self, path: &str) -> Result<String, String> {
+        let dir = Path::new(path);
+        let instance = self.active_instance();
+        csv::export_directory(instance, dir).map_err(|e| e.to_string())?;
+        Ok(format!("Exported {} fact(s) to {}.", instance.len(), path))
+    }
+
+    fn run_source(&mut self, path: &str) -> Result<String, String> {
+        let script =
+            std::fs::read_to_string(path).map_err(|e| format!("cannot read `{}`: {}", path, e))?;
+        self.execute_script(&script)
+    }
+
     fn run_chase(&mut self) -> String {
         let state = materialize(self.base_instance.clone(), &self.rules);
         let message = if state.result.terminated {
@@ -239,18 +317,38 @@ impl Session {
 }
 
 fn help_text() -> &'static str {
-    "Commands:
+    "\
-fact Parent(alice, bob).
+Facts and rules
-rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
+  fact Parent(alice, bob).           Add a ground fact.
-schema Parent(parent, child).
+  rule A(?X) -> B(?X).              Add a derivation rule (TGD).
+  rule A(?X), NOT B(?X) -> C(?X).   Negation-as-failure in rule body.
+  schema Parent(parent, child).     Register column names for SQL.
+  run.                              Run the chase to fixpoint.
+
+Queries
+  query Ancestor(?X, ?Y)?           Find all matching substitutions.
+  query Parent(alice, bob)?         Boolean: true or false.
+  explain Ancestor(alice, carol)?   Show derivation provenance.
+
+SQL (ends with ;)
   sql SELECT * FROM Parent;
-run.
+  sql SELECT dept, COUNT(*) FROM Emp GROUP BY dept;
-query Ancestor(?X, ?Y)?
+
-explain Ancestor(alice, bob)?
+Configuration
-show facts
+  set chase restricted              Chase variant: restricted, standard,
-show rules
+                                    oblivious, or skolem.
-reset
+  set semi-naive on                 Toggle semi-naive evaluation (on/off).
-help"
+
+Data
+  load <directory>                  Import facts from CSV files.
+  save <directory>                  Export facts to CSV files.
+  source <path>                     Run a .ech script file.
+
+Session
+  show facts                        List current facts.
+  show rules                        List current rules.
+  reset                             Clear all session state.
+  help                              Show this message."
 }
 
 fn sorted_render<'a, T>(items: impl Iterator<Item = &'a T>) -> Vec<String>
@@ -270,16 +368,15 @@ fn render_result_set(result: &ResultSet) -> String {
         return lines.join("\n");
     }
 
-    let header = result
+    let col_count = result.schema().len();
+    let headers: Vec<String> = result
         .schema()
         .fields()
         .iter()
         .map(|field| field.name().to_string())
-        .collect::<Vec<_>>()
+        .collect();
-        .join(" | ");
-    lines.push(header);
 
-    let rows = result
+    let cell_rows: Vec<Vec<String>> = result
         .rows()
         .iter()
         .map(|row| {
@@ -287,10 +384,40 @@ fn render_result_set(result: &ResultSet) -> String {
                 .iter()
                 .map(ToString::to_string)
                 .collect::<Vec<_>>()
-                .join(" | ")
         })
-        .collect::<Vec<_>>();
+        .collect();
-    lines.extend(rows);
+
+    // Compute column widths from headers and data.
+    let mut widths = vec![0usize; col_count];
+    for (i, header) in headers.iter().enumerate() {
+        widths[i] = widths[i].max(header.len());
+    }
+    for row in &cell_rows {
+        for (i, cell) in row.iter().enumerate() {
+            if i < col_count {
+                widths[i] = widths[i].max(cell.len());
+            }
+        }
+    }
+
+    let format_row = |cells: &[String]| -> String {
+        let formatted = cells
+            .iter()
+            .enumerate()
+            .map(|(i, cell)| {
+                let w = widths.get(i).copied().unwrap_or(0);
+                format!("{:<width$}", cell, width = w)
+            })
+            .collect::<Vec<_>>()
+            .join(" | ");
+        // Trim trailing whitespace from the last column.
+        formatted.trim_end().to_string()
+    };
+
+    lines.push(format_row(&headers));
+    for row in &cell_rows {
+        lines.push(format_row(row));
+    }
     lines.join("\n")
 }
 
@@ -317,6 +444,24 @@ fn format_substitution(subst: &Substitution, variables: &[String]) -> String {
 mod tests {
     use super::*;
 
+    /// Normalize a pipe-separated output by trimming whitespace around pipes
+    /// so that column-alignment padding does not break contains-checks.
+    fn normalize_pipes(s: &str) -> String {
+        s.lines()
+            .map(|line| {
+                if line.contains('|') {
+                    line.split('|')
+                        .map(str::trim)
+                        .collect::<Vec<_>>()
+                        .join(" | ")
+                } else {
+                    line.trim_end().to_string()
+                }
+            })
+            .collect::<Vec<_>>()
+            .join("\n")
+    }
+
     #[test]
     fn session_runs_chase_and_query() {
         let mut session = Session::new();
@@ -391,11 +536,12 @@ mod tests {
                  sql SELECT c0 AS parent_name, 'seed' AS label FROM Parent;",
             )
             .unwrap();
+        let normalized = normalize_pipes(&output);
 
-        assert!(output.contains("2 row(s)"));
+        assert!(normalized.contains("2 row(s)"));
-        assert!(output.contains("parent_name | label"));
+        assert!(normalized.contains("parent_name | label"));
-        assert!(output.contains("alice | seed"));
+        assert!(normalized.contains("alice | seed"));
-        assert!(output.contains("bob | seed"));
+        assert!(normalized.contains("bob | seed"));
     }
 
     #[test]
@@ -447,10 +593,11 @@ mod tests {
             )
             .unwrap();
 
-        assert!(output.contains("2 row(s)"));
+        let normalized = normalize_pipes(&output);
-        assert!(output.contains("Parent.parent | Ancestor.child"));
+        assert!(normalized.contains("2 row(s)"));
-        assert!(output.contains("alice | carol"));
+        assert!(normalized.contains("Parent.parent | Ancestor.child"));
-        assert!(output.contains("bob | dave"));
+        assert!(normalized.contains("alice | carol"));
+        assert!(normalized.contains("bob | dave"));
     }
 
     #[test]
@@ -467,10 +614,11 @@ mod tests {
             )
             .unwrap();
 
-        assert!(output.contains("2 row(s)"));
+        let normalized = normalize_pipes(&output);
-        assert!(output.contains("p.parent | q.child"));
+        assert!(normalized.contains("2 row(s)"));
-        assert!(output.contains("alice | carol"));
+        assert!(normalized.contains("p.parent | q.child"));
-        assert!(output.contains("bob | dave"));
+        assert!(normalized.contains("alice | carol"));
+        assert!(normalized.contains("bob | dave"));
     }
 
     #[test]

src/frontend/web.rs

@@ -173,17 +173,39 @@ const INDEX_HTML: &str = r##"<!DOCTYPE html>
       line-height: 1.5;
     }
 
+    .editor-container {
+      position: relative;
+    }
+
+    .highlight-backdrop {
+      position: absolute;
+      top: 0; left: 0; right: 0; bottom: 0;
+      border: 1px solid transparent;
+      border-radius: 14px;
+      padding: 1rem;
+      font: inherit;
+      line-height: 1.5;
+      white-space: pre-wrap;
+      word-break: break-word;
+      overflow: hidden;
+      pointer-events: none;
+      color: transparent;
+    }
+
     textarea {
       width: 100%;
       min-height: 22rem;
       border: 1px solid var(--border);
       border-radius: 14px;
-      background: #fffdfa;
+      background: transparent;
-      color: var(--ink);
+      color: transparent;
+      caret-color: var(--ink);
       padding: 1rem;
       resize: vertical;
       font: inherit;
       line-height: 1.5;
+      position: relative;
+      z-index: 1;
     }
 
     .actions {
@@ -245,12 +267,15 @@ const INDEX_HTML: &str = r##"<!DOCTYPE html>
           <p>Minimal local workbench for rule-driven query experiments.</p>
         </div>
       </div>
+      <div class="editor-container">
+      <pre class="highlight-backdrop" id="backdrop" aria-hidden="true"></pre>
       <textarea id="script">fact Parent(alice, bob).
 fact Parent(bob, carol).
 rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
 rule Ancestor(?X, ?Y), Parent(?Y, ?Z) -> Ancestor(?X, ?Z).
 run.
 explain Ancestor(alice, carol)?</textarea>
+      </div>
       <div class="actions">
         <button class="primary" id="execute">Execute</button>
         <button class="secondary" id="reset">Reset Session</button>
@@ -266,6 +291,15 @@ explain Ancestor(alice, carol)?</textarea>
   <script>
     const output = document.getElementById("output");
     const script = document.getElementById("script");
+    const backdrop = document.getElementById("backdrop");
+
+    function syncBackdrop() {
+      backdrop.innerHTML = highlightBlock(script.value) + "\n";
+      backdrop.scrollTop = script.scrollTop;
+    }
+    script.addEventListener("input", syncBackdrop);
+    script.addEventListener("scroll", () => { backdrop.scrollTop = script.scrollTop; });
+    syncBackdrop();
 
     const CMD_RE = /^(fact|rule|run|query|explain|show|reset|help|schema|sql)\b/i;
     const SQL_KW = /^(SELECT|FROM|WHERE|GROUP|BY|ORDER|LIMIT|AS|AND|OR|ASC|DESC|NULL|NOT|ON|JOIN|HAVING|DISTINCT)\b/i;