Add a simple REPL and GUI

Makefile

@@ -37,6 +37,30 @@ 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,6 +19,7 @@ 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.
@@ -76,7 +77,42 @@ let rule = RuleBuilder::new()
     .build();
 ```
 
-#### Usful Commands
+#### Frontends
+
+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
-- [ ] Property-based tests (QuickCheck/proptest)
+- [x] 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
-- [ ] CLI interface
+- [x] CLI interface
-- [ ] REPL for interactive queries
+- [x] REPL for interactive queries

src/frontend/language.rs

@@ -0,0 +1,369 @@
+//! 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

@@ -0,0 +1,10 @@
+//! 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

@@ -0,0 +1,39 @@
+//! 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

@@ -0,0 +1,251 @@
+//! 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

@@ -0,0 +1,286 @@
+//! 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,4 +1,5 @@
 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,4 +1,42 @@
-fn main() {
+use std::env;
-    // TODO: Implement CLI for chase-rs
+use std::fs;
-    println!("chase-rs: An implementation of the chase algorithm");
+use std::io;
+
+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,9 +1,30 @@
 //! 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, Term, chase};
+use chase_rs::{Atom, Instance, Substitution, 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> {
@@ -57,335 +78,366 @@ fn instance_strategy() -> impl Strategy<Value = Instance> {
 // Property: Chase always terminates
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(50))]
+fn chase_always_terminates() {
+    const SEED: u64 = 12345;
+    let mut runner = seeded_runner(SEED, 50);
 
-    #[test]
+    runner
-    fn chase_always_terminates(instance in instance_strategy()) {
+        .run(&instance_strategy(), |instance| {
-        // Simple rule: P(X) -> Q(X)
+            let rule = RuleBuilder::new()
-        let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
-            .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
-            .then("Q", vec![Term::var("X")])
+                .build();
-            .build();
 
-        let result = chase(instance, &[rule]);
+            let result = chase(instance, &[rule]);
 
-        // Chase should always terminate (either fixpoint or max iterations)
+            prop_assert!(result.terminated || result.steps > 0);
-        prop_assert!(result.terminated || result.steps > 0);
+            Ok(())
-    }
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Chase is monotonic (facts are only added, never removed)
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(50))]
+fn chase_is_monotonic() {
+    const SEED: u64 = 23456;
+    let mut runner = seeded_runner(SEED, 50);
 
-    #[test]
+    runner
-    fn chase_is_monotonic(instance in instance_strategy()) {
+        .run(&instance_strategy(), |instance| {
-        let initial_facts: Vec<_> = instance.iter().cloned().collect();
+            let initial_facts: Vec<_> = instance.iter().cloned().collect();
 
-        let rule = RuleBuilder::new()
+            let rule = RuleBuilder::new()
-            .when("P", vec![Term::var("X")])
+                .when("P", vec![Term::var("X")])
-            .then("Q", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
-            .build();
+                .build();
 
-        let result = chase(instance, &[rule]);
+            let result = chase(instance, &[rule]);
 
-        // All original facts should still be present
+            for fact in &initial_facts {
-        for fact in &initial_facts {
+                prop_assert!(
-            prop_assert!(
+                    result.instance.contains(fact),
-                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());
-        prop_assert!(result.instance.len() >= initial_facts.len());
+            Ok(())
-    }
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Fixpoint is stable (running chase again produces no changes)
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(30))]
+fn fixpoint_is_stable() {
+    const SEED: u64 = 34567;
+    let mut runner = seeded_runner(SEED, 30);
 
-    #[test]
+    runner
-    fn fixpoint_is_stable(instance in instance_strategy()) {
+        .run(&instance_strategy(), |instance| {
-        let rule = RuleBuilder::new()
+            let rule = RuleBuilder::new()
-            .when("P", vec![Term::var("X")])
+                .when("P", vec![Term::var("X")])
-            .then("Q", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
-            .build();
+                .build();
 
-        // Run chase to fixpoint
+            let result1 = chase(instance, &[rule.clone()]);
-        let result1 = chase(instance, &[rule.clone()]);
+            prop_assert!(result1.terminated);
-        prop_assert!(result1.terminated);
 
-        // Run chase again on the result
+            let result2 = chase(result1.instance.clone(), &[rule]);
-        let result2 = chase(result1.instance.clone(), &[rule]);
 
-        // Should terminate immediately with no new facts
+            prop_assert!(result2.terminated);
-        prop_assert!(result2.terminated);
+            prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
-        prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
+            prop_assert_eq!(result1.instance.len(), result2.instance.len());
-        prop_assert_eq!(result1.instance.len(), result2.instance.len());
+            Ok(())
-    }
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: All derived facts are ground (no variables)
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(50))]
+fn all_facts_are_ground() {
+    const SEED: u64 = 45678;
+    let mut runner = seeded_runner(SEED, 50);
 
-    #[test]
+    runner
-    fn all_facts_are_ground(instance in instance_strategy()) {
+        .run(&instance_strategy(), |instance| {
-        let rule = RuleBuilder::new()
+            let rule = RuleBuilder::new()
-            .when("P", vec![Term::var("X"), Term::var("Y")])
+                .when("P", vec![Term::var("X"), Term::var("Y")])
-            .then("R", vec![Term::var("X"), Term::var("Y")])
+                .then("R", vec![Term::var("X"), Term::var("Y")])
-            .build();
+                .build();
 
-        let result = chase(instance, &[rule]);
+            let result = chase(instance, &[rule]);
 
-        for fact in result.instance.iter() {
+            for fact in result.instance.iter() {
-            prop_assert!(
+                prop_assert!(fact.is_ground(), "Fact {:?} contains variables", fact);
-                fact.is_ground(),
+            }
-                "Fact {:?} contains variables", fact
+            Ok(())
-            );
+        })
-        }
+        .unwrap();
-    }
 }
 
 // =============================================================================
 // Property: Rules without existentials don't create nulls
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(50))]
+fn no_existentials_means_no_nulls() {
+    const SEED: u64 = 56789;
+    let mut runner = seeded_runner(SEED, 50);
 
-    #[test]
+    runner
-    fn no_existentials_means_no_nulls(instance in instance_strategy()) {
+        .run(&instance_strategy(), |instance| {
-        // Rule with all head variables appearing in body
+            let rule = RuleBuilder::new()
-        let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
-            .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
-            .then("Q", vec![Term::var("X")])
+                .build();
-            .build();
 
-        let result = chase(instance, &[rule]);
+            let result = chase(instance, &[rule]);
 
-        for fact in result.instance.iter() {
+            for fact in result.instance.iter() {
-            for term in &fact.terms {
+                for term in &fact.terms {
-                prop_assert!(
+                    prop_assert!(
-                    !matches!(term, Term::Null(_)),
+                        !matches!(term, Term::Null(_)),
-                    "Found null in fact {:?} but rule has no existentials", fact
+                        "Found null in fact {:?} but rule has no existentials",
-                );
+                        fact
+                    );
+                }
             }
-        }
+            Ok(())
-    }
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Existential rules create exactly one null per trigger
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(30))]
+fn existentials_create_unique_nulls() {
+    const SEED: u64 = 67890;
+    let mut runner = seeded_runner(SEED, 30);
 
-    #[test]
+    runner
-    fn existentials_create_unique_nulls(
+        .run(&(1usize..5), |num_constants| {
-        num_constants in 1usize..5
+            let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
-    ) {
+            let instance: Instance = constants
-        // Create facts P(c0), P(c1), P(c2), ... with unique constants
+                .iter()
-        let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
+                .map(|c| Atom::new("P", vec![Term::constant(c)]))
-        let instance: Instance = constants
+                .collect();
-            .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()
-        let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
-            .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X"), Term::var("Y")])
-            .then("Q", vec![Term::var("X"), Term::var("Y")])
+                .build();
-            .build();
 
-        let result = chase(instance, &[rule]);
+            let result = chase(instance, &[rule]);
 
-        let q_facts: Vec<_> = result.instance.facts_for_predicate("Q");
+            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);
-        prop_assert_eq!(q_facts.len(), num_constants);
 
-        // Each Q fact should have a null in the second position
+            for fact in &q_facts {
-        for fact in &q_facts {
+                prop_assert!(
-            prop_assert!(
+                    matches!(fact.terms[1], Term::Null(_)),
-                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
-        let nulls: Vec<_> = q_facts
+                .iter()
-            .iter()
+                .filter_map(|f| match &f.terms[1] {
-            .filter_map(|f| match &f.terms[1] {
+                    Term::Null(id) => Some(*id),
-                Term::Null(id) => Some(*id),
+                    _ => None,
-                _ => None,
+                })
-            })
+                .collect();
-            .collect();
 
-        let mut unique_nulls = nulls.clone();
+            let mut unique_nulls = nulls.clone();
-        unique_nulls.sort();
+            unique_nulls.sort();
-        unique_nulls.dedup();
+            unique_nulls.dedup();
-        prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
+            prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
-    }
+            Ok(())
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Transitive closure computes correct number of facts
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(20))]
+fn transitive_closure_chain() {
+    const SEED: u64 = 78901;
+    let mut runner = seeded_runner(SEED, 20);
 
-    #[test]
+    runner
-    fn transitive_closure_chain(chain_length in 2usize..6) {
+        .run(&(2usize..6), |chain_length| {
-        // Create a chain: E(0,1), E(1,2), ..., E(n-1,n)
+            let mut facts = Vec::new();
-        let mut facts = Vec::new();
+            for i in 0..chain_length {
-        for i in 0..chain_length {
+                facts.push(Atom::new(
-            facts.push(Atom::new(
+                    "E",
-                "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();
+                ));
+            }
+            let instance: Instance = facts.into_iter().collect();
 
-        // E(X,Y) -> T(X,Y)
+            let rule1 = RuleBuilder::new()
-        let rule1 = RuleBuilder::new()
+                .when("E", vec![Term::var("X"), Term::var("Y")])
-            .when("E", vec![Term::var("X"), Term::var("Y")])
+                .then("T", vec![Term::var("X"), Term::var("Y")])
-            .then("T", vec![Term::var("X"), Term::var("Y")])
+                .build();
-            .build();
 
-        // T(X,Y), E(Y,Z) -> T(X,Z)
+            let rule2 = RuleBuilder::new()
-        let rule2 = RuleBuilder::new()
+                .when("T", vec![Term::var("X"), Term::var("Y")])
-            .when("T", vec![Term::var("X"), Term::var("Y")])
+                .when("E", vec![Term::var("Y"), Term::var("Z")])
-            .when("E", vec![Term::var("Y"), Term::var("Z")])
+                .then("T", vec![Term::var("X"), Term::var("Z")])
-            .then("T", vec![Term::var("X"), Term::var("Z")])
+                .build();
-            .build();
 
-        let result = chase(instance, &[rule1, rule2]);
+            let result = chase(instance, &[rule1, rule2]);
-        prop_assert!(result.terminated);
+            prop_assert!(result.terminated);
 
-        let t_facts = result.instance.facts_for_predicate("T");
+            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;
-        let expected = chain_length * (chain_length + 1) / 2;
+            prop_assert_eq!(
-        prop_assert_eq!(
+                t_facts.len(),
-            t_facts.len(),
+                expected,
-            expected,
+                "Chain of {} edges should have {} transitive pairs",
-            "Chain of {} edges should have {} transitive pairs",
+                chain_length,
-            chain_length,
+                expected
-            expected
+            );
-        );
+            Ok(())
-    }
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Empty instance with any rules produces empty or stays empty
 // =============================================================================
 
-proptest! {
+#[test]
-    #[test]
+fn empty_instance_stays_bounded() {
-    fn empty_instance_stays_bounded(_seed in 0u64..1000) {
+    const SEED: u64 = 89012;
-        let instance = Instance::new();
+    let mut runner = seeded_runner(SEED, 100);
 
-        let rule = RuleBuilder::new()
+    runner
-            .when("P", vec![Term::var("X")])
+        .run(&(0u64..1000), |_| {
-            .then("Q", vec![Term::var("X")])
+            let instance = Instance::new();
-            .build();
 
-        let result = chase(instance, &[rule]);
+            let rule = RuleBuilder::new()
+                .when("P", vec![Term::var("X")])
+                .then("Q", vec![Term::var("X")])
+                .build();
 
-        prop_assert!(result.terminated);
+            let result = chase(instance, &[rule]);
-        prop_assert_eq!(result.steps, 0);
+
-        prop_assert!(result.instance.is_empty());
+            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
 // =============================================================================
 
-use chase_rs::Substitution;
+#[test]
+fn substitution_ground_term_unchanged() {
+    const SEED: u64 = 90123;
+    let mut runner = seeded_runner(SEED, 100);
 
-proptest! {
+    runner
-    #![proptest_config(ProptestConfig::with_cases(100))]
+        .run(&constant_strategy(), |c| {
+            let term = Term::constant(&c);
+            let mut subst = Substitution::new();
+            subst.bind("X".to_string(), Term::constant("other"));
 
-    #[test]
+            let result = subst.apply_term(&term);
-    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!(
-
+                result,
-        prop_assert_eq!(result, term, "Ground term should be unchanged by substitution");
+                term,
-    }
+                "Ground term should be unchanged by substitution"
+            );
+            Ok(())
+        })
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Substitution correctly replaces variables
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(100))]
+fn substitution_replaces_variable() {
+    const SEED: u64 = 11111;
+    let mut runner = seeded_runner(SEED, 100);
 
-    #[test]
+    runner
-    fn substitution_replaces_variable(
+        .run(
-        var in variable_strategy(),
+            &(variable_strategy(), constant_strategy()),
-        replacement in constant_strategy()
+            |(var, replacement)| {
-    ) {
+                let term = Term::var(&var);
-        let term = Term::var(&var);
+                let mut subst = Substitution::new();
-        let mut subst = Substitution::new();
+                subst.bind(var.clone(), Term::constant(&replacement));
-        subst.bind(var.clone(), Term::constant(&replacement));
 
-        let result = subst.apply_term(&term);
+                let result = subst.apply_term(&term);
 
-        prop_assert_eq!(
+                prop_assert_eq!(
-            result,
+                    result,
-            Term::constant(&replacement),
+                    Term::constant(&replacement),
-            "Variable should be replaced"
+                    "Variable should be replaced"
-        );
+                );
-    }
+                Ok(())
+            },
+        )
+        .unwrap();
 }
 
 // =============================================================================
 // Property: Atom arity is preserved through substitution
 // =============================================================================
 
-proptest! {
+#[test]
-    #![proptest_config(ProptestConfig::with_cases(50))]
+fn substitution_preserves_arity() {
+    const SEED: u64 = 22222;
+    let mut runner = seeded_runner(SEED, 50);
 
-    #[test]
+    let strategy = (
-    fn substitution_preserves_arity(
+        predicate_strategy(),
-        pred in predicate_strategy(),
+        prop::collection::vec(variable_strategy(), 1..4),
-        vars in prop::collection::vec(variable_strategy(), 1..4),
+        constant_strategy(),
-        replacement in constant_strategy()
+    );
-    ) {
-        let atom = Atom::new(
-            &pred,
-            vars.iter().map(|v| Term::var(v)).collect(),
-        );
 
-        let mut subst = Substitution::new();
+    runner
-        for var in &vars {
+        .run(&strategy, |(pred, vars, replacement)| {
-            subst.bind(var.clone(), Term::constant(&replacement));
+            let atom = Atom::new(&pred, vars.iter().map(|v| Term::var(v)).collect());
-        }
 
-        let result = subst.apply_atom(&atom);
+            let mut subst = Substitution::new();
+            for var in &vars {
+                subst.bind(var.clone(), Term::constant(&replacement));
+            }
 
-        prop_assert_eq!(result.arity(), atom.arity());
+            let result = subst.apply_atom(&atom);
-        prop_assert_eq!(result.predicate, atom.predicate);
+
-    }
+            prop_assert_eq!(result.arity(), atom.arity());
+            prop_assert_eq!(result.predicate, atom.predicate);
+            Ok(())
+        })
+        .unwrap();
 }