Makefile

@@ -37,30 +37,6 @@ run: build ## Build and run the binary
 	@echo "Running the $(BINARY) binary..."
 	@DEBUG_PROJ=$(DEBUG_PROJ) ./$(BINARY)
 
-.PHONY: repl
-repl: format ## Start the interactive REPL
-	@echo "Starting chase-rs REPL..."
-	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- repl
-
-.PHONY: gui
-gui: format ## Start the local GUI at 127.0.0.1:7878
-	@echo "Starting chase-rs GUI on http://127.0.0.1:7878..."
-	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- gui
-
-.PHONY: gui-addr
-gui-addr: format ## Start the local GUI at GUI_ADDR=<host:port>
-	@echo "Starting chase-rs GUI on http://$(or $(GUI_ADDR),127.0.0.1:7878)..."
-	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- gui $(or $(GUI_ADDR),127.0.0.1:7878)
-
-.PHONY: script
-script: format ## Run a frontend script with SCRIPT=<path>
-	@if [ -z "$(SCRIPT)" ]; then \
-	   echo "Usage: make script SCRIPT=<path>"; \
-	   exit 1; \
-	fi
-	@echo "Running script $(SCRIPT)..."
-	@DEBUG_PROJ=$(DEBUG_PROJ) cargo run -- script $(SCRIPT)
-
 .PHONY: clean
 clean: ## Remove generated and temporary files
 	@echo "Cleaning up..."

README.md

@@ -19,7 +19,6 @@ This implementation provides a **restricted chase** that guarantees termination
 - **Existential Quantification**: Automatic generation of labeled nulls
 - **Restricted Chase**: Termination guarantees via trigger tracking
 - **Fluent API**: `RuleBuilder` for readable rule construction
-- **Interactive Frontends**: REPL, script runner, and a local GUI
 - **Zero Dependencies**: Pure Rust with no external runtime dependencies
 
 See [ROADMAP.md](ROADMAP.md) for the list of implemented and planned features.
@@ -77,42 +76,7 @@ let rule = RuleBuilder::new()
     .build();
 ```
 
-#### Frontends
+#### Usful Commands
-
-The binary now supports three entrypoints:
-
-```bash
-# Start the interactive REPL
-cargo run -- repl
-
-# Start the local GUI at http://127.0.0.1:7878
-cargo run -- gui
-
-# Run a script file
-cargo run -- script examples/session.chase
-```
-
-The REPL and GUI share a minimal command language:
-
-```text
-fact Parent(alice, bob).
-rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
-run.
-query Ancestor(?X, ?Y)?
-show facts
-show rules
-reset
-help
-```
-
-Rules:
-
-- facts and rules end with `.`
-- queries end with `?`
-- variables are prefixed with `?`
-- quoted constants are supported, for example `"alice smith"`
-
-#### Useful Commands
 
 ```bash
 # Install dependencies

ROADMAP.md

@@ -68,7 +68,7 @@ This document outlines the implemented features and the future goals for the pro
 
 - [x] Unit tests (in-module)
 - [x] Integration tests
-- [x] Property-based tests (QuickCheck/proptest)
+- [ ] Property-based tests (QuickCheck/proptest)
 - [ ] Regression tests
 - [ ] Benchmarks
 - [ ] Fuzzing
@@ -78,5 +78,5 @@ This document outlines the implemented features and the future goals for the pro
 - [ ] API documentation (rustdoc)
 - [ ] User guide
 - [ ] Example programs
-- [x] CLI interface
+- [ ] CLI interface
-- [x] REPL for interactive queries
+- [ ] REPL for interactive queries

src/frontend/language.rs

@@ -1,369 +0,0 @@
-//! Minimal command language for the chase-rs REPL and GUI.
-
-use crate::chase::rule::RuleBuilder;
-use crate::{Atom, Rule, Term};
-
-#[derive(Debug, Clone)]
-pub enum Command {
-    Fact(Atom),
-    Rule(Rule),
-    Run,
-    Query(Vec<Atom>),
-    ShowFacts,
-    ShowRules,
-    Reset,
-    Help,
-}
-
-pub fn parse_script(input: &str) -> Result<Vec<Command>, String> {
-    let mut commands = Vec::new();
-
-    for (index, raw_line) in input.lines().enumerate() {
-        let line = raw_line.trim();
-        if line.is_empty() || line.starts_with('#') {
-            continue;
-        }
-
-        let command = parse_command(line).map_err(|err| format!("line {}: {}", index + 1, err))?;
-        commands.push(command);
-    }
-
-    Ok(commands)
-}
-
-pub fn parse_command(input: &str) -> Result<Command, String> {
-    let trimmed = input.trim();
-
-    if trimmed.eq_ignore_ascii_case("run") || trimmed.eq_ignore_ascii_case("run.") {
-        return Ok(Command::Run);
-    }
-    if trimmed.eq_ignore_ascii_case("show facts") || trimmed.eq_ignore_ascii_case("show facts.") {
-        return Ok(Command::ShowFacts);
-    }
-    if trimmed.eq_ignore_ascii_case("show rules") || trimmed.eq_ignore_ascii_case("show rules.") {
-        return Ok(Command::ShowRules);
-    }
-    if trimmed.eq_ignore_ascii_case("reset") || trimmed.eq_ignore_ascii_case("reset.") {
-        return Ok(Command::Reset);
-    }
-    if trimmed.eq_ignore_ascii_case("help") || trimmed.eq_ignore_ascii_case("help.") {
-        return Ok(Command::Help);
-    }
-
-    if let Some(rest) = strip_keyword(trimmed, "fact") {
-        let atom = parse_atom(trim_suffix(rest, '.')?)?;
-        return Ok(Command::Fact(atom));
-    }
-
-    if let Some(rest) = strip_keyword(trimmed, "rule") {
-        let rule_text = trim_suffix(rest, '.')?;
-        let arrow = find_top_level_arrow(rule_text)
-            .ok_or_else(|| "rule must contain a top-level `->`".to_string())?;
-        let body_text = rule_text[..arrow].trim();
-        let head_text = rule_text[arrow + 2..].trim();
-        if body_text.is_empty() || head_text.is_empty() {
-            return Err("rule body and head must both be non-empty".to_string());
-        }
-
-        let body = parse_atom_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 atom in head {
-            builder = builder.then(&atom.predicate, atom.terms);
-        }
-        return Ok(Command::Rule(builder.build()));
-    }
-
-    if let Some(rest) = strip_keyword(trimmed, "query") {
-        let atoms = parse_atom_list(trim_suffix(rest, '?')?)?;
-        return Ok(Command::Query(atoms));
-    }
-
-    Err("unknown command; try `help`".to_string())
-}
-
-fn strip_keyword<'a>(input: &'a str, keyword: &str) -> Option<&'a str> {
-    let prefix = input.get(..keyword.len())?;
-    if !prefix.eq_ignore_ascii_case(keyword) {
-        return None;
-    }
-
-    let rest = input.get(keyword.len()..)?;
-    if rest.is_empty() {
-        return Some(rest);
-    }
-
-    let mut chars = rest.chars();
-    let first = chars.next()?;
-    if first.is_whitespace() {
-        Some(rest.trim_start())
-    } else {
-        None
-    }
-}
-
-fn trim_suffix(input: &str, suffix: char) -> Result<&str, String> {
-    let trimmed = input.trim();
-    if let Some(stripped) = trimmed.strip_suffix(suffix) {
-        Ok(stripped.trim_end())
-    } else {
-        Err(format!("command must end with `{}`", suffix))
-    }
-}
-
-fn parse_atom_list(input: &str) -> Result<Vec<Atom>, String> {
-    split_top_level(input, ',')?
-        .into_iter()
-        .map(parse_atom)
-        .collect()
-}
-
-fn parse_atom(input: &str) -> Result<Atom, String> {
-    let trimmed = input.trim();
-    let open = trimmed
-        .find('(')
-        .ok_or_else(|| format!("expected `(` in atom `{}`", trimmed))?;
-    let close = trimmed
-        .rfind(')')
-        .ok_or_else(|| format!("expected `)` in atom `{}`", trimmed))?;
-    if close <= open {
-        return Err(format!("malformed atom `{}`", trimmed));
-    }
-    if close != trimmed.len() - 1 {
-        return Err(format!("unexpected content after atom `{}`", trimmed));
-    }
-
-    let predicate = trimmed[..open].trim();
-    validate_identifier(predicate, "predicate")?;
-
-    let args = trimmed[open + 1..close].trim();
-    let terms = if args.is_empty() {
-        Vec::new()
-    } else {
-        split_top_level(args, ',')?
-            .into_iter()
-            .map(parse_term)
-            .collect::<Result<Vec<_>, _>>()?
-    };
-
-    Ok(Atom::new(predicate, terms))
-}
-
-fn parse_term(input: &str) -> Result<Term, String> {
-    let trimmed = input.trim();
-    if trimmed.is_empty() {
-        return Err("empty term".to_string());
-    }
-
-    if let Some(var) = trimmed.strip_prefix('?') {
-        validate_identifier(var, "variable")?;
-        return Ok(Term::var(var));
-    }
-
-    if trimmed.starts_with('"') {
-        return parse_string_literal(trimmed).map(Term::constant);
-    }
-
-    if trimmed.chars().any(char::is_whitespace) {
-        return Err(format!(
-            "constants with spaces must be quoted: `{}`",
-            trimmed
-        ));
-    }
-
-    validate_identifier(trimmed, "constant")?;
-    Ok(Term::constant(trimmed))
-}
-
-fn parse_string_literal(input: &str) -> Result<String, String> {
-    if !input.ends_with('"') || input.len() < 2 {
-        return Err(format!("unterminated string literal `{}`", input));
-    }
-
-    let inner = &input[1..input.len() - 1];
-    let mut value = String::new();
-    let mut escaped = false;
-
-    for ch in inner.chars() {
-        if escaped {
-            let translated = match ch {
-                '\\' => '\\',
-                '"' => '"',
-                'n' => '\n',
-                't' => '\t',
-                other => {
-                    return Err(format!("unsupported escape sequence `\\{}`", other));
-                }
-            };
-            value.push(translated);
-            escaped = false;
-            continue;
-        }
-
-        if ch == '\\' {
-            escaped = true;
-        } else {
-            value.push(ch);
-        }
-    }
-
-    if escaped {
-        return Err("string literal ends with a trailing escape".to_string());
-    }
-
-    Ok(value)
-}
-
-fn validate_identifier(value: &str, label: &str) -> Result<(), String> {
-    if value.is_empty() {
-        return Err(format!("{} cannot be empty", label));
-    }
-
-    if value.chars().all(is_identifier_char) {
-        Ok(())
-    } else {
-        Err(format!("invalid {} `{}`", label, value))
-    }
-}
-
-fn is_identifier_char(ch: char) -> bool {
-    ch.is_ascii_alphanumeric() || matches!(ch, '_' | '-' | ':')
-}
-
-fn find_top_level_arrow(input: &str) -> Option<usize> {
-    let bytes = input.as_bytes();
-    let mut depth = 0usize;
-    let mut in_string = false;
-    let mut escaped = false;
-    let mut index = 0usize;
-
-    while index < bytes.len() {
-        let ch = bytes[index] as char;
-        if in_string {
-            if escaped {
-                escaped = false;
-            } else if ch == '\\' {
-                escaped = true;
-            } else if ch == '"' {
-                in_string = false;
-            }
-            index += 1;
-            continue;
-        }
-
-        match ch {
-            '"' => in_string = true,
-            '(' => depth += 1,
-            ')' => depth = depth.saturating_sub(1),
-            '-' if depth == 0 && bytes.get(index + 1).copied() == Some(b'>') => {
-                return Some(index);
-            }
-            _ => {}
-        }
-        index += 1;
-    }
-
-    None
-}
-
-fn split_top_level(input: &str, separator: char) -> Result<Vec<&str>, String> {
-    let mut parts = Vec::new();
-    let mut depth = 0usize;
-    let mut in_string = false;
-    let mut escaped = false;
-    let mut start = 0usize;
-
-    for (index, ch) in input.char_indices() {
-        if in_string {
-            if escaped {
-                escaped = false;
-            } else if ch == '\\' {
-                escaped = true;
-            } else if ch == '"' {
-                in_string = false;
-            }
-            continue;
-        }
-
-        match ch {
-            '"' => in_string = true,
-            '(' => depth += 1,
-            ')' => {
-                if depth == 0 {
-                    return Err(format!("unexpected `)` in `{}`", input));
-                }
-                depth -= 1;
-            }
-            ch if ch == separator && depth == 0 => {
-                let part = input[start..index].trim();
-                if part.is_empty() {
-                    return Err(format!("empty element in `{}`", input));
-                }
-                parts.push(part);
-                start = index + ch.len_utf8();
-            }
-            _ => {}
-        }
-    }
-
-    if in_string {
-        return Err(format!("unterminated string literal in `{}`", input));
-    }
-    if depth != 0 {
-        return Err(format!("unbalanced parentheses in `{}`", input));
-    }
-
-    let tail = input[start..].trim();
-    if tail.is_empty() {
-        return Err(format!("empty element in `{}`", input));
-    }
-    parts.push(tail);
-    Ok(parts)
-}
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    #[test]
-    fn parse_fact_command() {
-        let command = parse_command(r#"fact Parent(alice, "bob smith")."#).unwrap();
-        match command {
-            Command::Fact(atom) => {
-                assert_eq!(atom.predicate, "Parent");
-                assert_eq!(atom.terms.len(), 2);
-            }
-            other => panic!("unexpected command: {:?}", other),
-        }
-    }
-
-    #[test]
-    fn parse_rule_command() {
-        let command = parse_command("rule P(?X), Q(?X, a) -> R(?X).").unwrap();
-        match command {
-            Command::Rule(rule) => {
-                assert_eq!(rule.body.len(), 2);
-                assert_eq!(rule.head.len(), 1);
-            }
-            other => panic!("unexpected command: {:?}", other),
-        }
-    }
-
-    #[test]
-    fn parse_query_command() {
-        let command = parse_command("query Ancestor(?X, ?Y), Parent(?Y, ?Z)?").unwrap();
-        match command {
-            Command::Query(atoms) => assert_eq!(atoms.len(), 2),
-            other => panic!("unexpected command: {:?}", other),
-        }
-    }
-
-    #[test]
-    fn parse_script_reports_line_numbers() {
-        let error = parse_script("help\nbogus\nrun.").unwrap_err();
-        assert!(error.contains("line 2"));
-    }
-}

src/frontend/mod.rs

@@ -1,10 +0,0 @@
-//! Frontend utilities for interacting with chase-rs through scripts, a REPL, or a GUI.
-
-pub mod language;
-pub mod repl;
-pub mod session;
-pub mod web;
-
-pub use repl::run_repl;
-pub use session::Session;
-pub use web::serve_gui;

src/frontend/repl.rs

@@ -1,39 +0,0 @@
-//! Interactive REPL for the minimal chase-rs frontend language.
-
-use std::io::{self, BufRead, Write};
-
-use super::Session;
-
-pub fn run_repl() -> io::Result<()> {
-    let stdin = io::stdin();
-    let mut stdout = io::stdout();
-    let mut session = Session::new();
-
-    writeln!(stdout, "chase-rs REPL")?;
-    writeln!(stdout, "Type `help` for commands and `quit` to exit.")?;
-
-    let mut lines = stdin.lock().lines();
-    loop {
-        write!(stdout, "chase> ")?;
-        stdout.flush()?;
-
-        let Some(line) = lines.next() else {
-            writeln!(stdout)?;
-            return Ok(());
-        };
-        let line = line?;
-        let trimmed = line.trim();
-        if trimmed.eq_ignore_ascii_case("quit") || trimmed.eq_ignore_ascii_case("exit") {
-            writeln!(stdout, "bye")?;
-            return Ok(());
-        }
-        if trimmed.is_empty() {
-            continue;
-        }
-
-        match session.execute_script(trimmed) {
-            Ok(output) => writeln!(stdout, "{}", output)?,
-            Err(err) => writeln!(stdout, "error: {}", err)?,
-        }
-    }
-}

src/frontend/session.rs

@@ -1,251 +0,0 @@
-//! Session state and command execution shared by the REPL and GUI.
-
-use std::fmt;
-
-use crate::chase::substitution::unify_atom;
-use crate::{Atom, ChaseResult, Instance, Rule, Substitution, chase};
-
-use super::language::{Command, parse_script};
-
-#[derive(Debug, Default)]
-pub struct Session {
-    base_instance: Instance,
-    rules: Vec<Rule>,
-    materialized: Option<ChaseResult>,
-}
-
-impl Session {
-    pub fn new() -> Self {
-        Self::default()
-    }
-
-    pub fn execute_script(&mut self, script: &str) -> Result<String, String> {
-        let commands = parse_script(script)?;
-        let mut output = Vec::new();
-
-        for command in commands {
-            let message = self.execute(command)?;
-            if !message.is_empty() {
-                output.push(message);
-            }
-        }
-
-        if output.is_empty() {
-            Ok("No commands executed.".to_string())
-        } else {
-            Ok(output.join("\n"))
-        }
-    }
-
-    pub fn execute(&mut self, command: Command) -> Result<String, String> {
-        match command {
-            Command::Fact(atom) => {
-                self.materialized = None;
-                let inserted = self.base_instance.add(atom.clone());
-                let action = if inserted {
-                    "Added"
-                } else {
-                    "Skipped duplicate"
-                };
-                Ok(format!("{} fact: {}", action, atom))
-            }
-            Command::Rule(rule) => {
-                self.materialized = None;
-                self.rules.push(rule.clone());
-                Ok(format!("Added rule #{}: {}", self.rules.len(), rule))
-            }
-            Command::Run => Ok(self.run_chase()),
-            Command::Query(query) => Ok(self.run_query(&query)),
-            Command::ShowFacts => Ok(self.show_facts()),
-            Command::ShowRules => Ok(self.show_rules()),
-            Command::Reset => {
-                *self = Self::default();
-                Ok("Session reset.".to_string())
-            }
-            Command::Help => Ok(help_text().to_string()),
-        }
-    }
-
-    pub fn reset(&mut self) {
-        *self = Self::default();
-    }
-
-    fn run_chase(&mut self) -> String {
-        let result = chase(self.base_instance.clone(), &self.rules);
-        let message = if result.terminated {
-            format!(
-                "Chase completed in {} step(s); {} fact(s) available.",
-                result.steps,
-                result.instance.len()
-            )
-        } else {
-            format!(
-                "Chase stopped after {} step(s); result may be incomplete.",
-                result.steps
-            )
-        };
-        self.materialized = Some(result);
-        message
-    }
-
-    fn run_query(&self, query: &[Atom]) -> String {
-        let instance = self.active_instance();
-        let matches = find_matches(instance, query);
-        let variables = query_variables(query);
-
-        if variables.is_empty() {
-            return if matches.is_empty() {
-                "false".to_string()
-            } else {
-                "true".to_string()
-            };
-        }
-
-        if matches.is_empty() {
-            return "0 rows".to_string();
-        }
-
-        let mut rows = matches
-            .iter()
-            .map(|subst| format_substitution(subst, &variables))
-            .collect::<Vec<_>>();
-        rows.sort();
-
-        let mut rendered = Vec::with_capacity(rows.len() + 1);
-        rendered.push(format!("{} row(s)", rows.len()));
-        rendered.extend(rows);
-        rendered.join("\n")
-    }
-
-    fn show_facts(&self) -> String {
-        let facts = sorted_render(self.active_instance().iter());
-        if facts.is_empty() {
-            return "No facts loaded.".to_string();
-        }
-
-        facts.join("\n")
-    }
-
-    fn show_rules(&self) -> String {
-        if self.rules.is_empty() {
-            return "No rules loaded.".to_string();
-        }
-
-        self.rules
-            .iter()
-            .enumerate()
-            .map(|(index, rule)| format!("{}: {}", index + 1, rule))
-            .collect::<Vec<_>>()
-            .join("\n")
-    }
-
-    fn active_instance(&self) -> &Instance {
-        if let Some(result) = &self.materialized {
-            &result.instance
-        } else {
-            &self.base_instance
-        }
-    }
-}
-
-fn help_text() -> &'static str {
-    "Commands:
-fact Parent(alice, bob).
-rule Parent(?X, ?Y) -> Ancestor(?X, ?Y).
-run.
-query Ancestor(?X, ?Y)?
-show facts
-show rules
-reset
-help"
-}
-
-fn sorted_render<'a, T>(items: impl Iterator<Item = &'a T>) -> Vec<String>
-where
-    T: fmt::Display + 'a,
-{
-    let mut rendered = items.map(ToString::to_string).collect::<Vec<_>>();
-    rendered.sort();
-    rendered
-}
-
-fn query_variables(query: &[Atom]) -> Vec<String> {
-    let mut variables = query
-        .iter()
-        .flat_map(|atom| atom.variables())
-        .cloned()
-        .collect::<Vec<_>>();
-    variables.sort();
-    variables.dedup();
-    variables
-}
-
-fn format_substitution(subst: &Substitution, variables: &[String]) -> String {
-    variables
-        .iter()
-        .filter_map(|var| subst.get(var).map(|term| format!("?{} = {}", var, term)))
-        .collect::<Vec<_>>()
-        .join(", ")
-}
-
-fn find_matches(instance: &Instance, body: &[Atom]) -> Vec<Substitution> {
-    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::*;
-
-    #[test]
-    fn session_runs_chase_and_query() {
-        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\
-                 query Ancestor(?X, ?Y)?",
-            )
-            .unwrap();
-
-        assert!(output.contains("Chase completed"));
-        assert!(output.contains("?X = alice, ?Y = bob"));
-        assert!(output.contains("?X = alice, ?Y = carol"));
-    }
-
-    #[test]
-    fn boolean_query_returns_truth_value() {
-        let mut session = Session::new();
-        let output = session
-            .execute_script("fact Parent(alice, bob).\nquery Parent(alice, bob)?")
-            .unwrap();
-        assert!(output.ends_with("true"));
-    }
-}

src/frontend/web.rs

@@ -1,286 +0,0 @@
-//! Minimal local web UI for the chase-rs frontend language.
-
-use std::io::{self, BufRead, BufReader, Read, Write};
-use std::net::{TcpListener, TcpStream};
-use std::sync::{Arc, Mutex};
-
-use super::Session;
-
-pub fn serve_gui(address: &str) -> io::Result<()> {
-    let listener = TcpListener::bind(address)?;
-    let session = Arc::new(Mutex::new(Session::new()));
-
-    println!("GUI available at http://{}", address);
-
-    for stream in listener.incoming() {
-        match stream {
-            Ok(stream) => {
-                let shared = Arc::clone(&session);
-                if let Err(err) = handle_connection(stream, &shared) {
-                    eprintln!("gui error: {}", err);
-                }
-            }
-            Err(err) => eprintln!("gui accept error: {}", err),
-        }
-    }
-
-    Ok(())
-}
-
-fn handle_connection(mut stream: TcpStream, session: &Arc<Mutex<Session>>) -> io::Result<()> {
-    let mut reader = BufReader::new(stream.try_clone()?);
-    let mut request_line = String::new();
-    reader.read_line(&mut request_line)?;
-    if request_line.trim().is_empty() {
-        return Ok(());
-    }
-
-    let mut parts = request_line.split_whitespace();
-    let method = parts.next().unwrap_or_default();
-    let path = parts.next().unwrap_or("/");
-
-    let mut content_length = 0usize;
-    loop {
-        let mut header = String::new();
-        reader.read_line(&mut header)?;
-        if header == "\r\n" || header.is_empty() {
-            break;
-        }
-        if let Some((name, value)) = header.split_once(':')
-            && name.eq_ignore_ascii_case("content-length")
-        {
-            let parsed = value.trim().parse::<usize>().ok();
-            if let Some(length) = parsed {
-                content_length = length;
-            }
-        }
-    }
-
-    let mut body = vec![0u8; content_length];
-    if content_length > 0 {
-        reader.read_exact(&mut body)?;
-    }
-
-    let response = match (method, path) {
-        ("GET", "/") => http_response("200 OK", "text/html; charset=utf-8", INDEX_HTML),
-        ("POST", "/execute") => {
-            let script = String::from_utf8_lossy(&body);
-            let output = {
-                let mut locked = session
-                    .lock()
-                    .map_err(|_| io::Error::other("session lock poisoned"))?;
-                match locked.execute_script(script.as_ref()) {
-                    Ok(output) => output,
-                    Err(err) => format!("error: {}", err),
-                }
-            };
-            http_response("200 OK", "text/plain; charset=utf-8", &output)
-        }
-        ("POST", "/reset") => {
-            let mut locked = session
-                .lock()
-                .map_err(|_| io::Error::other("session lock poisoned"))?;
-            locked.reset();
-            http_response("200 OK", "text/plain; charset=utf-8", "Session reset.")
-        }
-        _ => http_response("404 Not Found", "text/plain; charset=utf-8", "Not found"),
-    };
-
-    stream.write_all(response.as_bytes())?;
-    stream.flush()?;
-    Ok(())
-}
-
-fn http_response(status: &str, content_type: &str, body: &str) -> String {
-    format!(
-        "HTTP/1.1 {}\r\nContent-Type: {}\r\nContent-Length: {}\r\nConnection: close\r\n\r\n{}",
-        status,
-        content_type,
-        body.len(),
-        body
-    )
-}
-
-const INDEX_HTML: &str = r#"<!DOCTYPE html>
-<html lang="en">
-<head>
-  <meta charset="utf-8">
-  <meta name="viewport" content="width=device-width, initial-scale=1">
-  <title>chase-rs GUI</title>
-  <style>
-    :root {
-      --bg: #f4efe6;
-      --panel: rgba(255, 251, 245, 0.9);
-      --ink: #1f1d1a;
-      --accent: #b5542f;
-      --accent-soft: #e7c7b8;
-      --border: #d7c7b8;
-      --shadow: rgba(78, 52, 38, 0.14);
-    }
-
-    * { box-sizing: border-box; }
-
-    body {
-      margin: 0;
-      min-height: 100vh;
-      font-family: "Iosevka", "SFMono-Regular", "Menlo", monospace;
-      color: var(--ink);
-      background:
-        radial-gradient(circle at top left, rgba(181, 84, 47, 0.18), transparent 28rem),
-        linear-gradient(135deg, #efe4d4, var(--bg));
-    }
-
-    main {
-      width: min(1100px, calc(100% - 2rem));
-      margin: 2rem auto;
-      display: grid;
-      gap: 1rem;
-      grid-template-columns: repeat(auto-fit, minmax(320px, 1fr));
-    }
-
-    section {
-      background: var(--panel);
-      border: 1px solid var(--border);
-      border-radius: 18px;
-      box-shadow: 0 18px 50px var(--shadow);
-      backdrop-filter: blur(10px);
-    }
-
-    .editor {
-      padding: 1.25rem;
-    }
-
-    .header {
-      display: flex;
-      justify-content: space-between;
-      align-items: center;
-      gap: 1rem;
-      margin-bottom: 1rem;
-    }
-
-    h1, h2, p {
-      margin: 0;
-    }
-
-    h1 {
-      font-size: clamp(1.5rem, 2vw, 2rem);
-      letter-spacing: 0.04em;
-      text-transform: uppercase;
-    }
-
-    p {
-      color: rgba(31, 29, 26, 0.74);
-      line-height: 1.5;
-    }
-
-    textarea {
-      width: 100%;
-      min-height: 22rem;
-      border: 1px solid var(--border);
-      border-radius: 14px;
-      background: #fffdfa;
-      color: var(--ink);
-      padding: 1rem;
-      resize: vertical;
-      font: inherit;
-      line-height: 1.5;
-    }
-
-    .actions {
-      display: flex;
-      gap: 0.75rem;
-      margin-top: 1rem;
-      flex-wrap: wrap;
-    }
-
-    button {
-      border: 0;
-      border-radius: 999px;
-      padding: 0.8rem 1.2rem;
-      font: inherit;
-      cursor: pointer;
-      transition: transform 140ms ease, opacity 140ms ease;
-    }
-
-    button:hover { transform: translateY(-1px); }
-    button:active { transform: translateY(0); }
-
-    .primary {
-      background: var(--accent);
-      color: #fff8f3;
-    }
-
-    .secondary {
-      background: var(--accent-soft);
-      color: var(--ink);
-    }
-
-    pre {
-      margin: 0;
-      padding: 1.25rem;
-      min-height: 100%;
-      white-space: pre-wrap;
-      word-break: break-word;
-      line-height: 1.5;
-    }
-
-    .output {
-      overflow: hidden;
-    }
-
-    .sample {
-      font-size: 0.92rem;
-      padding: 0 1.25rem 1.25rem;
-    }
-  </style>
-</head>
-<body>
-  <main>
-    <section class="editor">
-      <div class="header">
-        <div>
-          <h1>chase-rs</h1>
-          <p>Minimal REPL language exposed through a local browser session.</p>
-        </div>
-      </div>
-      <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.
-query Ancestor(?X, ?Y)?</textarea>
-      <div class="actions">
-        <button class="primary" id="execute">Execute</button>
-        <button class="secondary" id="reset">Reset Session</button>
-      </div>
-      <p class="sample">Try <code>show facts</code>, <code>show rules</code>, or boolean queries like <code>query Parent(alice, bob)?</code>.</p>
-    </section>
-
-    <section class="output">
-      <pre id="output">Session ready.</pre>
-    </section>
-  </main>
-
-  <script>
-    const output = document.getElementById("output");
-    const script = document.getElementById("script");
-
-    async function send(path, body) {
-      const response = await fetch(path, { method: "POST", body });
-      const text = await response.text();
-      return text;
-    }
-
-    document.getElementById("execute").addEventListener("click", async () => {
-      const text = await send("/execute", script.value);
-      output.textContent += `\n\n> ${new Date().toLocaleTimeString()}\n${text}`;
-    });
-
-    document.getElementById("reset").addEventListener("click", async () => {
-      const text = await send("/reset", "");
-      output.textContent = text;
-    });
-  </script>
-</body>
-</html>
-"#;

src/lib.rs

@@ -1,5 +1,4 @@
 pub mod chase;
-pub mod frontend;
 
 // Re-export main types for convenience
 pub use chase::{Atom, ChaseResult, Instance, Rule, Substitution, Term, chase};

src/main.rs

@@ -1,42 +1,4 @@
-use std::env;
+fn main() {
-use std::fs;
+    // TODO: Implement CLI for chase-rs
-use std::io;
+    println!("chase-rs: An implementation of the chase algorithm");
-
-use chase_rs::frontend::{Session, run_repl, serve_gui};
-
-fn main() -> io::Result<()> {
-    let args = env::args().skip(1).collect::<Vec<_>>();
-    if args.is_empty() {
-        return run_repl();
-    }
-
-    match args.as_slice() {
-        [cmd] if cmd.eq_ignore_ascii_case("repl") => run_repl(),
-        [cmd] if cmd.eq_ignore_ascii_case("gui") => serve_gui("127.0.0.1:7878"),
-        [cmd, address] if cmd.eq_ignore_ascii_case("gui") => serve_gui(address),
-        [cmd, path] if cmd.eq_ignore_ascii_case("script") => run_script(path),
-        _ => {
-            print_usage();
-            Ok(())
-        }
-    }
-}
-
-fn run_script(path: &str) -> io::Result<()> {
-    let script = fs::read_to_string(path)?;
-    let mut session = Session::new();
-    match session.execute_script(&script) {
-        Ok(output) => {
-            println!("{}", output);
-            Ok(())
-        }
-        Err(err) => Err(io::Error::new(io::ErrorKind::InvalidInput, err)),
-    }
-}
-
-fn print_usage() {
-    println!("Usage:");
-    println!("  chase-rs repl");
-    println!("  chase-rs gui [host:port]");
-    println!("  chase-rs script <path>");
 }

tests/property_tests.rs

@@ -1,30 +1,9 @@
 //! Property-based tests for the chase algorithm using proptest.
-//!
-//! All tests use explicit seeds for reproducibility.
 
 use proptest::prelude::*;
-use proptest::test_runner::{Config, TestRng, TestRunner};
 
 use chase_rs::chase::rule::RuleBuilder;
-use chase_rs::{Atom, Instance, Substitution, Term, chase};
+use chase_rs::{Atom, Instance, Term, chase};
-
-// =============================================================================
-// Test Configuration
-// =============================================================================
-
-/// Create a test runner with an explicit seed for reproducibility.
-fn seeded_runner(seed: u64, cases: u32) -> TestRunner {
-    let config = Config::with_cases(cases);
-    // Create a deterministic seed from u64
-    let mut seed_bytes = [0u8; 32];
-    seed_bytes[..8].copy_from_slice(&seed.to_le_bytes());
-    let rng = TestRng::from_seed(proptest::test_runner::RngAlgorithm::ChaCha, &seed_bytes);
-    TestRunner::new_with_rng(config, rng)
-}
-
-// =============================================================================
-// Strategies
-// =============================================================================
 
 /// Strategy for generating constant names
 fn constant_strategy() -> impl Strategy<Value = String> {
@@ -78,13 +57,12 @@ fn instance_strategy() -> impl Strategy<Value = Instance> {
 // Property: Chase always terminates
 // =============================================================================
 
-#[test]
+proptest! {
-fn chase_always_terminates() {
+    #![proptest_config(ProptestConfig::with_cases(50))]
-    const SEED: u64 = 12345;
-    let mut runner = seeded_runner(SEED, 50);
 
-    runner
+    #[test]
-        .run(&instance_strategy(), |instance| {
+    fn chase_always_terminates(instance in instance_strategy()) {
+        // Simple rule: P(X) -> Q(X)
         let rule = RuleBuilder::new()
             .when("P", vec![Term::var("X")])
             .then("Q", vec![Term::var("X")])
@@ -92,23 +70,20 @@ fn chase_always_terminates() {
 
         let result = chase(instance, &[rule]);
 
+        // Chase should always terminate (either fixpoint or max iterations)
         prop_assert!(result.terminated || result.steps > 0);
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Chase is monotonic (facts are only added, never removed)
 // =============================================================================
 
-#[test]
+proptest! {
-fn chase_is_monotonic() {
+    #![proptest_config(ProptestConfig::with_cases(50))]
-    const SEED: u64 = 23456;
-    let mut runner = seeded_runner(SEED, 50);
 
-    runner
+    #[test]
-        .run(&instance_strategy(), |instance| {
+    fn chase_is_monotonic(instance in instance_strategy()) {
         let initial_facts: Vec<_> = instance.iter().cloned().collect();
 
         let rule = RuleBuilder::new()
@@ -118,60 +93,56 @@ fn chase_is_monotonic() {
 
         let result = chase(instance, &[rule]);
 
+        // All original facts should still be present
         for fact in &initial_facts {
             prop_assert!(
                 result.instance.contains(fact),
-                    "Original fact {:?} was removed",
+                "Original fact {:?} was removed", fact
-                    fact
             );
         }
 
+        // Result should have at least as many facts as the input
         prop_assert!(result.instance.len() >= initial_facts.len());
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Fixpoint is stable (running chase again produces no changes)
 // =============================================================================
 
-#[test]
+proptest! {
-fn fixpoint_is_stable() {
+    #![proptest_config(ProptestConfig::with_cases(30))]
-    const SEED: u64 = 34567;
-    let mut runner = seeded_runner(SEED, 30);
 
-    runner
+    #[test]
-        .run(&instance_strategy(), |instance| {
+    fn fixpoint_is_stable(instance in instance_strategy()) {
         let rule = RuleBuilder::new()
             .when("P", vec![Term::var("X")])
             .then("Q", vec![Term::var("X")])
             .build();
 
+        // Run chase to fixpoint
         let result1 = chase(instance, &[rule.clone()]);
         prop_assert!(result1.terminated);
 
+        // Run chase again on the result
         let result2 = chase(result1.instance.clone(), &[rule]);
 
+        // Should terminate immediately with no new facts
         prop_assert!(result2.terminated);
         prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
         prop_assert_eq!(result1.instance.len(), result2.instance.len());
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: All derived facts are ground (no variables)
 // =============================================================================
 
-#[test]
+proptest! {
-fn all_facts_are_ground() {
+    #![proptest_config(ProptestConfig::with_cases(50))]
-    const SEED: u64 = 45678;
-    let mut runner = seeded_runner(SEED, 50);
 
-    runner
+    #[test]
-        .run(&instance_strategy(), |instance| {
+    fn all_facts_are_ground(instance in instance_strategy()) {
         let rule = RuleBuilder::new()
             .when("P", vec![Term::var("X"), Term::var("Y")])
             .then("R", vec![Term::var("X"), Term::var("Y")])
@@ -180,24 +151,24 @@ fn all_facts_are_ground() {
         let result = chase(instance, &[rule]);
 
         for fact in result.instance.iter() {
-                prop_assert!(fact.is_ground(), "Fact {:?} contains variables", fact);
+            prop_assert!(
+                fact.is_ground(),
+                "Fact {:?} contains variables", fact
+            );
+        }
     }
-            Ok(())
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Rules without existentials don't create nulls
 // =============================================================================
 
-#[test]
+proptest! {
-fn no_existentials_means_no_nulls() {
+    #![proptest_config(ProptestConfig::with_cases(50))]
-    const SEED: u64 = 56789;
-    let mut runner = seeded_runner(SEED, 50);
 
-    runner
+    #[test]
-        .run(&instance_strategy(), |instance| {
+    fn no_existentials_means_no_nulls(instance in instance_strategy()) {
+        // Rule with all head variables appearing in body
         let rule = RuleBuilder::new()
             .when("P", vec![Term::var("X")])
             .then("Q", vec![Term::var("X")])
@@ -209,33 +180,32 @@ fn no_existentials_means_no_nulls() {
             for term in &fact.terms {
                 prop_assert!(
                     !matches!(term, Term::Null(_)),
-                        "Found null in fact {:?} but rule has no existentials",
+                    "Found null in fact {:?} but rule has no existentials", fact
-                        fact
                 );
             }
         }
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Existential rules create exactly one null per trigger
 // =============================================================================
 
-#[test]
+proptest! {
-fn existentials_create_unique_nulls() {
+    #![proptest_config(ProptestConfig::with_cases(30))]
-    const SEED: u64 = 67890;
-    let mut runner = seeded_runner(SEED, 30);
 
-    runner
+    #[test]
-        .run(&(1usize..5), |num_constants| {
+    fn existentials_create_unique_nulls(
+        num_constants in 1usize..5
+    ) {
+        // Create facts P(c0), P(c1), P(c2), ... with unique constants
         let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
         let instance: Instance = constants
             .iter()
             .map(|c| Atom::new("P", vec![Term::constant(c)]))
             .collect();
 
+        // Rule: P(X) -> Q(X, Y) where Y is existential
         let rule = RuleBuilder::new()
             .when("P", vec![Term::var("X")])
             .then("Q", vec![Term::var("X"), Term::var("Y")])
@@ -245,16 +215,18 @@ fn existentials_create_unique_nulls() {
 
         let q_facts: Vec<_> = result.instance.facts_for_predicate("Q");
 
+        // Should have exactly as many Q facts as P facts
         prop_assert_eq!(q_facts.len(), num_constants);
 
+        // Each Q fact should have a null in the second position
         for fact in &q_facts {
             prop_assert!(
                 matches!(fact.terms[1], Term::Null(_)),
-                    "Expected null in second position of {:?}",
+                "Expected null in second position of {:?}", fact
-                    fact
             );
         }
 
+        // All nulls should be unique
         let nulls: Vec<_> = q_facts
             .iter()
             .filter_map(|f| match &f.terms[1] {
@@ -267,39 +239,35 @@ fn existentials_create_unique_nulls() {
         unique_nulls.sort();
         unique_nulls.dedup();
         prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Transitive closure computes correct number of facts
 // =============================================================================
 
-#[test]
+proptest! {
-fn transitive_closure_chain() {
+    #![proptest_config(ProptestConfig::with_cases(20))]
-    const SEED: u64 = 78901;
-    let mut runner = seeded_runner(SEED, 20);
 
-    runner
+    #[test]
-        .run(&(2usize..6), |chain_length| {
+    fn transitive_closure_chain(chain_length in 2usize..6) {
+        // Create a chain: E(0,1), E(1,2), ..., E(n-1,n)
         let mut facts = Vec::new();
         for i in 0..chain_length {
             facts.push(Atom::new(
                 "E",
-                    vec![
+                vec![Term::constant(format!("{}", i)), Term::constant(format!("{}", i + 1))],
-                        Term::constant(format!("{}", i)),
-                        Term::constant(format!("{}", i + 1)),
-                    ],
             ));
         }
         let instance: Instance = facts.into_iter().collect();
 
+        // E(X,Y) -> T(X,Y)
         let rule1 = RuleBuilder::new()
             .when("E", vec![Term::var("X"), Term::var("Y")])
             .then("T", vec![Term::var("X"), Term::var("Y")])
             .build();
 
+        // T(X,Y), E(Y,Z) -> T(X,Z)
         let rule2 = RuleBuilder::new()
             .when("T", vec![Term::var("X"), Term::var("Y")])
             .when("E", vec![Term::var("Y"), Term::var("Z")])
@@ -311,6 +279,7 @@ fn transitive_closure_chain() {
 
         let t_facts = result.instance.facts_for_predicate("T");
 
+        // For a chain of n edges, transitive closure has n*(n+1)/2 pairs
         let expected = chain_length * (chain_length + 1) / 2;
         prop_assert_eq!(
             t_facts.len(),
@@ -319,22 +288,16 @@ fn transitive_closure_chain() {
             chain_length,
             expected
         );
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Empty instance with any rules produces empty or stays empty
 // =============================================================================
 
+proptest! {
     #[test]
-fn empty_instance_stays_bounded() {
+    fn empty_instance_stays_bounded(_seed in 0u64..1000) {
-    const SEED: u64 = 89012;
-    let mut runner = seeded_runner(SEED, 100);
-
-    runner
-        .run(&(0u64..1000), |_| {
         let instance = Instance::new();
 
         let rule = RuleBuilder::new()
@@ -347,51 +310,42 @@ fn empty_instance_stays_bounded() {
         prop_assert!(result.terminated);
         prop_assert_eq!(result.steps, 0);
         prop_assert!(result.instance.is_empty());
-            Ok(())
+    }
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Substitution application is idempotent for ground terms
 // =============================================================================
 
-#[test]
+use chase_rs::Substitution;
-fn substitution_ground_term_unchanged() {
-    const SEED: u64 = 90123;
-    let mut runner = seeded_runner(SEED, 100);
 
-    runner
+proptest! {
-        .run(&constant_strategy(), |c| {
+    #![proptest_config(ProptestConfig::with_cases(100))]
+
+    #[test]
+    fn substitution_ground_term_unchanged(c in constant_strategy()) {
         let term = Term::constant(&c);
         let mut subst = Substitution::new();
         subst.bind("X".to_string(), Term::constant("other"));
 
         let result = subst.apply_term(&term);
 
-            prop_assert_eq!(
+        prop_assert_eq!(result, term, "Ground term should be unchanged by substitution");
-                result,
+    }
-                term,
-                "Ground term should be unchanged by substitution"
-            );
-            Ok(())
-        })
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Substitution correctly replaces variables
 // =============================================================================
 
-#[test]
+proptest! {
-fn substitution_replaces_variable() {
+    #![proptest_config(ProptestConfig::with_cases(100))]
-    const SEED: u64 = 11111;
-    let mut runner = seeded_runner(SEED, 100);
 
-    runner
+    #[test]
-        .run(
+    fn substitution_replaces_variable(
-            &(variable_strategy(), constant_strategy()),
+        var in variable_strategy(),
-            |(var, replacement)| {
+        replacement in constant_strategy()
+    ) {
         let term = Term::var(&var);
         let mut subst = Substitution::new();
         subst.bind(var.clone(), Term::constant(&replacement));
@@ -403,31 +357,27 @@ fn substitution_replaces_variable() {
             Term::constant(&replacement),
             "Variable should be replaced"
         );
-                Ok(())
+    }
-            },
-        )
-        .unwrap();
 }
 
 // =============================================================================
 // Property: Atom arity is preserved through substitution
 // =============================================================================
 
+proptest! {
+    #![proptest_config(ProptestConfig::with_cases(50))]
+
     #[test]
-fn substitution_preserves_arity() {
+    fn substitution_preserves_arity(
-    const SEED: u64 = 22222;
+        pred in predicate_strategy(),
-    let mut runner = seeded_runner(SEED, 50);
+        vars in prop::collection::vec(variable_strategy(), 1..4),
-
+        replacement in constant_strategy()
-    let strategy = (
+    ) {
-        predicate_strategy(),
+        let atom = Atom::new(
-        prop::collection::vec(variable_strategy(), 1..4),
+            &pred,
-        constant_strategy(),
+            vars.iter().map(|v| Term::var(v)).collect(),
         );
 
-    runner
-        .run(&strategy, |(pred, vars, replacement)| {
-            let atom = Atom::new(&pred, vars.iter().map(|v| Term::var(v)).collect());
-
         let mut subst = Substitution::new();
         for var in &vars {
             subst.bind(var.clone(), Term::constant(&replacement));
@@ -437,7 +387,5 @@ fn substitution_preserves_arity() {
 
         prop_assert_eq!(result.arity(), atom.arity());
         prop_assert_eq!(result.predicate, atom.predicate);
-            Ok(())
+    }
-        })
-        .unwrap();
 }