WIP

AGENTS.md

@@ -1,146 +0,0 @@
-# AGENTS.md
-
-This file provides guidance to coding agents collaborating on this repository.
-
-## Mission
-
-Geolog is a Rust codebase for geometric logic:
-
-- a parser and pretty-printer for the Geolog language,
-- an elaboration layer that turns syntax into core structures,
-- a REPL and workspace/persistence layer,
-- a chase/query/solver runtime,
-- and an optional egui GUI behind the `gui` Cargo feature.
-
-Priorities, in order:
-
-1. Semantic correctness of theories, instances, queries, and chase behavior.
-2. Clear boundaries between parsing, elaboration, core structures, REPL/workspace, and GUI code.
-3. Focused, maintainable changes with good regression coverage.
-4. Performance only after correctness and testability are preserved.
-
-## Core Rules
-
-- Use English for code, comments, docs, tests, and commit-facing text.
-- Prefer small, targeted changes over broad rewrites.
-- Fix root causes rather than layering on ad hoc workarounds.
-- Keep modules decoupled: parsing in parser/lexer, semantics in `core`/`elaborate`, runtime behavior in `repl`/`query`/`solver`, presentation in `gui`.
-- Do not introduce unnecessary global mutable state.
-- Preserve feature gating: GUI code must remain behind the `gui` feature.
-- Avoid adding dependencies unless clearly justified.
-- Add comments only when they clarify non-obvious invariants, algorithms, or semantic constraints.
-
-Quick examples:
-
-- Good: add a targeted regression test for a chase bug in an existing GUI or unit test module.
-- Good: fix a REPL/workspace bug in `src/repl.rs` or `src/store/` without refactoring unrelated parser code.
-- Bad: rewrite the AST/core boundary during a small GUI task.
-- Bad: mix GUI presentation logic into core semantic modules.
-
-## Repository Layout
-
-- `src/lib.rs`: crate entrypoint and module exports.
-- `src/ast.rs`, `src/lexer.rs`, `src/parser.rs`, `src/pretty.rs`: syntax pipeline and round-tripping.
-- `src/core.rs`: core semantic data structures such as signatures, theories, and structures.
-- `src/elaborate/`: elaboration from AST into core representations.
-- `src/repl.rs`: REPL state, command handling, and top-level execution flow.
-- `src/store/`: persistence/workspace and storage-related logic.
-- `src/query/`: chase, query compilation, optimization, backend execution.
-- `src/solver/`: solver and tactic logic.
-- `src/tensor/`: tensor-based checking/evaluation support.
-- `src/gui/`: egui GUI state, panels, and visualizations.
-- `src/bin/geolog.rs`: CLI/REPL binary.
-- `src/bin/geolog-gui.rs`: GUI binary (requires `--features gui`).
-- `examples/geolog/`: sample Geolog programs.
-- `tests/`: integration, regression, unit-style cross-module, and property tests.
-- `docs/`: architecture and syntax documentation.
-- `proofs/`: Lean proofs and formal artifacts.
-- `fuzz/`: fuzzing targets.
-
-## Architecture Constraints
-
-- Keep the syntax pipeline clean: text → lexer → parser → AST.
-- Keep elaboration separate from parsing and separate from UI code.
-- `core` types should remain usable without the GUI.
-- GUI code should orchestrate and present existing behavior, not reimplement semantic logic.
-- Workspace/persistence behavior belongs in `repl`/`store`, not inside GUI widgets.
-- Query/chase behavior changes must preserve observable semantics and existing tests.
-- If a change affects persistence or serialization, consider compatibility with existing workspace behavior.
-
-## GUI Rules
-
-- The GUI is optional and must compile cleanly only when the `gui` feature is enabled.
-- Prefer fixing GUI bugs in `src/gui/state.rs`, `src/gui/panels/`, or `src/gui/visualizations/` before touching core logic.
-- Keep GUI state transitions explicit and centralized when possible.
-- Avoid hard-coding theme assumptions; UI should remain readable in the intended visual style.
-- File dialog, editor, browser, inspector, console, and visualization behavior should stay consistent with REPL/workspace state.
-
-## Testing Layout Rules
-
-- Prefer unit tests near the code they exercise when there is already a local test module.
-- Put broader cross-module coverage in `tests/`.
-- Keep regression tests close to the bug they reproduce when that is the clearest fit.
-- Do not add a new testing framework if existing `cargo test`, property tests, or fuzz targets are sufficient.
-- If you move behavior across modules, move or rewrite the relevant tests with it.
-
-## Workflow
-
-Before coding:
-
-1. Identify whether the task is parser, elaboration, runtime, persistence, solver/query, or GUI work.
-2. Read the touched module and nearby tests first.
-3. Check whether the change should live in `core`/`repl`/`store` rather than the GUI.
-
-Implement and validate:
-
-1. Make the smallest change that solves the problem.
-2. Add or update tests when behavior changes or a bug is fixed.
-3. Run the narrowest relevant command while iterating.
-4. Run broader validation once the change is stable.
-5. Update docs if user-facing behavior or workflow changed.
-
-## Validation Commands
-
-Use the narrowest relevant command first:
-
-- General compile check: `cargo check`
-- Full test suite: `cargo test`
-- GUI compile check: `cargo check --features gui --bin geolog-gui`
-- GUI-related tests: `cargo test --features gui`
-- Single test/module during iteration: `cargo test <name>`
-
-Formatting:
-
-- Prefer formatting only touched Rust files when the repository is not already fully formatted.
-- Avoid reformatting unrelated files as part of a focused bugfix.
-
-## Testing Expectations
-
-- No semantic bugfix is complete without appropriate validation.
-- Parser/elaboration changes should preserve round-trip and error-reporting behavior where relevant.
-- Query/chase/solver changes need explicit coverage because regressions can be subtle.
-- GUI bugfixes should get a focused test when practical, especially for state transitions or regressions.
-- Keep tests deterministic and focused on observable behavior.
-
-## Documentation Expectations
-
-- Update `README.md` when user workflow, CLI behavior, or GUI usage changes.
-- Update `docs/ARCHITECTURE.md` or `docs/SYNTAX.md` when architectural or language behavior changes materially.
-- If you find stale docs directly related to your change, fix them in the same patch.
-
-## Review Guidelines
-
-Review output should be concise and focus on real defects.
-
-- `P0`: broken build, broken tests, data loss, or incorrect core semantics.
-- `P1`: likely semantic regression, unsafe state transition, missing validation on risky changes.
-
-Use this review format:
-
-1. `Severity` (`P0`/`P1`)
-2. `File:line`
-3. `Issue`
-4. `Why it matters`
-5. `Minimal fix direction`
-
-Do not include style-only feedback or broad praise.

README2.md

@@ -37,10 +37,6 @@ Usage in REPL:
 
 A full-featured graphical interface built with egui.
 
-Current design note:
-- The GUI uses a rigid docked layout rather than draggable in-window splitters.
-- This was done to reduce hover/drag-induced layout jitter and keep the workspace visually stable.
-
 #### Building the GUI
 
 ```bash

src/bin/geolog-gui.rs

@@ -114,18 +114,22 @@ fn setup_fonts(ctx: &egui::Context) {
     // Use a slightly larger default font
     let mut style = (*ctx.style()).clone();
     style.animation_time = 0.0;
-    style
-        .text_styles
-        .insert(egui::TextStyle::Body, egui::FontId::proportional(14.0));
-    style
-        .text_styles
-        .insert(egui::TextStyle::Heading, egui::FontId::proportional(18.0));
-    style
-        .text_styles
-        .insert(egui::TextStyle::Monospace, egui::FontId::monospace(13.0));
+    style.text_styles.insert(
+        egui::TextStyle::Body,
+        egui::FontId::proportional(14.0),
+    );
+    style.text_styles.insert(
+        egui::TextStyle::Heading,
+        egui::FontId::proportional(18.0),
+    );
+    style.text_styles.insert(
+        egui::TextStyle::Monospace,
+        egui::FontId::monospace(13.0),
+    );
 
-    // Force a light theme for the GUI.
-    style.visuals = egui::Visuals::light();
+    // Set up dark theme with custom colors
+    style.visuals = egui::Visuals::dark();
+    style.visuals.override_text_color = Some(egui::Color32::from_gray(220));
     style.visuals.widgets.noninteractive.expansion = 0.0;
     style.visuals.widgets.inactive.expansion = 0.0;
     style.visuals.widgets.hovered.expansion = 0.0;

src/gui/app.rs

@@ -46,21 +46,21 @@ impl GeologApp {
 
     /// Render the menu bar
     fn menu_bar(&mut self, ui: &mut egui::Ui) {
-        egui::MenuBar::new().ui(ui, |ui| {
+        egui::menu::bar(ui, |ui| {
             ui.menu_button("File", |ui| {
                 if ui.button("Open...").clicked() {
                     self.handle_open_file();
-                    ui.close();
+                    ui.close_menu();
                 }
                 if ui.button("Save").clicked() {
                     self.handle_save_file();
-                    ui.close();
+                    ui.close_menu();
                 }
                 ui.separator();
                 if ui.button("Reset State").clicked() {
-                    self.state.reset_runtime_state();
+                    self.state.repl.reset();
                     self.state.log_info("State reset");
-                    ui.close();
+                    ui.close_menu();
                 }
                 ui.separator();
                 if ui.button("Quit").clicked() {
@@ -71,11 +71,11 @@ impl GeologApp {
             ui.menu_button("Edit", |ui| {
                 if ui.button("Clear Editor").clicked() {
                     self.state.editor_content.clear();
-                    ui.close();
+                    ui.close_menu();
                 }
                 if ui.button("Clear Console").clicked() {
                     self.state.clear_console();
-                    ui.close();
+                    ui.close_menu();
                 }
             });
 
@@ -88,7 +88,7 @@ impl GeologApp {
                     .clicked()
                 {
                     self.state.central_view = CentralView::EditorAndInspector;
-                    ui.close();
+                    ui.close_menu();
                 }
                 if ui
                     .selectable_label(
@@ -98,7 +98,7 @@ impl GeologApp {
                     .clicked()
                 {
                     self.state.central_view = CentralView::ChaseVisualization;
-                    ui.close();
+                    ui.close_menu();
                 }
                 if ui
                     .selectable_label(
@@ -108,7 +108,7 @@ impl GeologApp {
                     .clicked()
                 {
                     self.state.central_view = CentralView::GraphVisualization;
-                    ui.close();
+                    ui.close_menu();
                 }
             });
 
@@ -119,11 +119,11 @@ impl GeologApp {
                     let name = name.clone();
                     if ui.button(format!("Run Chase on {}", name)).clicked() {
                         self.handle_run_chase(&name);
-                        ui.close();
+                        ui.close_menu();
                     }
                     if ui.button(format!("Debug Chase on {}", name)).clicked() {
                         self.state.start_chase(&name);
-                        ui.close();
+                        ui.close_menu();
                     }
                 } else {
                     ui.label("(Select an instance first)");
@@ -132,13 +132,15 @@ impl GeologApp {
 
             ui.menu_button("Help", |ui| {
                 if ui.button("About").clicked() {
-                    self.state
-                        .log_info(format!("Geolog GUI v{}", env!("CARGO_PKG_VERSION")));
-                    ui.close();
+                    self.state.log_info(format!(
+                        "Geolog GUI v{}",
+                        env!("CARGO_PKG_VERSION")
+                    ));
+                    ui.close_menu();
                 }
                 if ui.button("Syntax Help").clicked() {
                     self.show_syntax_help();
-                    ui.close();
+                    ui.close_menu();
                 }
             });
         });
@@ -146,7 +148,7 @@ impl GeologApp {
 
     /// Handle opening a file
     fn handle_open_file(&mut self) {
-        if let Some(path) = Self::new_file_dialog()
+        if let Some(path) = rfd::FileDialog::new()
             .add_filter("Geolog", &["geolog"])
             .add_filter("All Files", &["*"])
             .pick_file()
@@ -168,7 +170,7 @@ impl GeologApp {
             }
         } else {
             // Save As
-            if let Some(path) = Self::new_file_dialog()
+            if let Some(path) = rfd::FileDialog::new()
                 .add_filter("Geolog", &["geolog"])
                 .save_file()
             {
@@ -185,14 +187,6 @@ impl GeologApp {
         }
     }
 
-    fn new_file_dialog() -> rfd::FileDialog {
-        let dialog = rfd::FileDialog::new();
-        match std::env::current_dir() {
-            Ok(dir) => dialog.set_directory(dir),
-            Err(_) => dialog,
-        }
-    }
-
     /// Run chase on an instance
     fn handle_run_chase(&mut self, instance_name: &str) {
         use crate::core::RelationStorage;
@@ -248,7 +242,8 @@ impl GeologApp {
             Ok(iterations) => {
                 let elapsed = start.elapsed();
                 // Get structure info before releasing borrow
-                let total_tuples: usize = entry.structure.relations.iter().map(|r| r.len()).sum();
+                let total_tuples: usize =
+                    entry.structure.relations.iter().map(|r| r.len()).sum();
                 let num_elements = entry.structure.len();
 
                 self.state.log_success(format!(
@@ -260,7 +255,8 @@ impl GeologApp {
                 // Show structure summary
                 self.state.log_info(format!(
                     "Structure: {} elements, {} relation tuples",
-                    num_elements, total_tuples
+                    num_elements,
+                    total_tuples
                 ));
             }
             Err(e) => {

src/gui/panels/browser.rs

@@ -147,7 +147,7 @@ impl BrowserPanel {
                             if ui.button("Inspect").clicked() {
                                 state.selected_item =
                                     Some(SelectedItem::Instance(instance.name.clone()));
-                                ui.close();
+                                ui.close_menu();
                             }
                             if ui.button("Run Chase").clicked() {
                                 // This will be handled by the app
@@ -157,11 +157,11 @@ impl BrowserPanel {
                                     "Use Chase menu to run chase on '{}'",
                                     instance.name
                                 ));
-                                ui.close();
+                                ui.close_menu();
                             }
                             if ui.button("View Graph").clicked() {
                                 state.show_graph(&instance.name, None);
-                                ui.close();
+                                ui.close_menu();
                             }
                         });
                     }

src/gui/panels/console.rs

@@ -6,7 +6,7 @@ use eframe::egui;
 use egui_extras::{Size, StripBuilder};
 
 use crate::gui::state::{GuiState, MessageKind};
-use crate::repl::{ExecuteResult, ListTarget, MetaCommand};
+use crate::repl::{MetaCommand, ListTarget, ExecuteResult};
 
 /// Console panel for output messages and REPL input
 pub struct ConsolePanel {
@@ -73,7 +73,12 @@ impl ConsolePanel {
                                         ui.label("Type commands below (e.g., :help, :list, or geolog code)");
                                     } else {
                                         for message in &state.console_messages {
-                                            let color = message_color(ui, message.kind);
+                                            let color = match message.kind {
+                                                MessageKind::Info => egui::Color32::LIGHT_GRAY,
+                                                MessageKind::Success => egui::Color32::from_rgb(100, 200, 100),
+                                                MessageKind::Error => egui::Color32::from_rgb(255, 100, 100),
+                                                MessageKind::Warning => egui::Color32::from_rgb(255, 200, 100),
+                                            };
 
                                             let prefix = match message.kind {
                                                 MessageKind::Info => ">",
@@ -110,7 +115,7 @@ impl ConsolePanel {
                             egui::Label::new(
                                 egui::RichText::new("geolog>")
                                     .monospace()
-                                    .color(ui.visuals().hyperlink_color),
+                                    .color(egui::Color32::from_rgb(100, 150, 255)),
                             ),
                         );
 
@@ -226,22 +231,24 @@ impl ConsolePanel {
 
     fn handle_meta_command(&mut self, state: &mut GuiState, cmd: MetaCommand) {
         match cmd {
-            MetaCommand::Help(topic) => match topic.as_deref() {
-                None => {
-                    state.log_info("Commands:");
-                    state.log_info("  :help          Show this help");
-                    state.log_info("  :list          List theories and instances");
-                    state.log_info("  :inspect <n>   Inspect a theory or instance");
-                    state.log_info("  :chase <inst>  Run chase on instance");
-                    state.log_info("  :reset         Reset all state");
-                    state.log_info("  :clear         Clear console");
-                    state.log_info("");
-                    state.log_info("Or type geolog code directly.");
+            MetaCommand::Help(topic) => {
+                match topic.as_deref() {
+                    None => {
+                        state.log_info("Commands:");
+                        state.log_info("  :help          Show this help");
+                        state.log_info("  :list          List theories and instances");
+                        state.log_info("  :inspect <n>   Inspect a theory or instance");
+                        state.log_info("  :chase <inst>  Run chase on instance");
+                        state.log_info("  :reset         Reset all state");
+                        state.log_info("  :clear         Clear console");
+                        state.log_info("");
+                        state.log_info("Or type geolog code directly.");
+                    }
+                    Some(t) => {
+                        state.log_info(format!("Help topic: {}", t));
+                    }
                 }
-                Some(t) => {
-                    state.log_info(format!("Help topic: {}", t));
-                }
-            },
+            }
             MetaCommand::List(target) => {
                 match target {
                     ListTarget::Theories | ListTarget::All => {
@@ -279,7 +286,7 @@ impl ConsolePanel {
                 }
             }
             MetaCommand::Inspect(name) => {
-                use crate::repl::{format_instance_detail, format_theory_detail, InspectResult};
+                use crate::repl::{InspectResult, format_theory_detail, format_instance_detail};
                 match state.repl.inspect(&name) {
                     Some(InspectResult::Theory(detail)) => {
                         for line in format_theory_detail(&detail).lines() {
@@ -300,26 +307,26 @@ impl ConsolePanel {
                 state.clear_console();
             }
             MetaCommand::Reset => {
-                state.reset_runtime_state();
+                state.repl.reset();
+                state.selected_item = None;
                 state.log_success("State reset.");
             }
-            MetaCommand::Chase {
-                instance,
-                max_iterations,
-            } => {
+            MetaCommand::Chase { instance, max_iterations } => {
                 self.run_chase(state, &instance, max_iterations);
             }
-            MetaCommand::Source(path) => match std::fs::read_to_string(&path) {
-                Ok(content) => {
-                    state.editor_content = content;
-                    state.current_file = Some(path.clone());
-                    state.log_info(format!("Loaded: {}", path.display()));
-                    state.execute_editor();
+            MetaCommand::Source(path) => {
+                match std::fs::read_to_string(&path) {
+                    Ok(content) => {
+                        state.editor_content = content;
+                        state.current_file = Some(path.clone());
+                        state.log_info(format!("Loaded: {}", path.display()));
+                        state.execute_editor();
+                    }
+                    Err(e) => {
+                        state.log_error(format!("Failed to load: {}", e));
+                    }
                 }
-                Err(e) => {
-                    state.log_error(format!("Failed to load: {}", e));
-                }
-            },
+            }
             _ => {
                 state.log_warning("Command not yet implemented in GUI");
             }
@@ -354,11 +361,7 @@ impl ConsolePanel {
             return;
         }
 
-        state.log_info(format!(
-            "Running chase on '{}' ({} axioms)...",
-            instance_name,
-            axioms.len()
-        ));
+        state.log_info(format!("Running chase on '{}' ({} axioms)...", instance_name, axioms.len()));
 
         let entry = state.repl.instances.get_mut(instance_name).unwrap();
         let max_iter = max_iterations.unwrap_or(100);
@@ -386,7 +389,8 @@ impl ConsolePanel {
                 ));
                 state.log_info(format!(
                     "Structure: {} elements, {} relation tuples",
-                    num_elements, total_tuples
+                    num_elements,
+                    total_tuples
                 ));
             }
             Err(e) => {
@@ -428,15 +432,6 @@ impl ConsolePanel {
     }
 }
 
-fn message_color(ui: &egui::Ui, kind: MessageKind) -> egui::Color32 {
-    match kind {
-        MessageKind::Info => ui.visuals().text_color(),
-        MessageKind::Success => egui::Color32::from_rgb(25, 110, 55),
-        MessageKind::Error => egui::Color32::from_rgb(170, 30, 45),
-        MessageKind::Warning => egui::Color32::from_rgb(145, 95, 15),
-    }
-}
-
 impl Default for ConsolePanel {
     fn default() -> Self {
         Self::new()

src/gui/state.rs

@@ -179,16 +179,6 @@ impl GuiState {
         }
     }
 
-    /// Reset the loaded theories/instances and clear any stale GUI selections.
-    pub fn reset_runtime_state(&mut self) {
-        self.repl.reset();
-        self.selected_item = None;
-        self.chase_state = None;
-        self.graph_instance = None;
-        self.graph_relation = None;
-        self.central_view = CentralView::EditorAndInspector;
-    }
-
     /// Add an info message to the console
     pub fn log_info(&mut self, text: impl Into<String>) {
         self.console_messages.push(ConsoleMessage {
@@ -340,30 +330,3 @@ impl GuiState {
         self.central_view = CentralView::GraphVisualization;
     }
 }
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-
-    #[test]
-    fn reset_runtime_state_clears_gui_navigation_state() {
-        let mut state = GuiState::new();
-        state.selected_item = Some(SelectedItem::Theory("Demo".into()));
-        state.chase_state = Some(ChaseVisualizationState::new("I".into(), Structure::new(0)));
-        state.graph_instance = Some("I".into());
-        state.graph_relation = Some("R".into());
-        state.central_view = CentralView::GraphVisualization;
-        state.editor_content = "theory Demo {}".into();
-        state.current_file = Some(PathBuf::from("demo.geolog"));
-
-        state.reset_runtime_state();
-
-        assert!(state.selected_item.is_none());
-        assert!(state.chase_state.is_none());
-        assert!(state.graph_instance.is_none());
-        assert!(state.graph_relation.is_none());
-        assert_eq!(state.central_view, CentralView::EditorAndInspector);
-        assert_eq!(state.editor_content, "theory Demo {}");
-        assert_eq!(state.current_file, Some(PathBuf::from("demo.geolog")));
-    }
-}

src/gui/visualizations/chase.rs

@@ -6,9 +6,7 @@ use eframe::egui;
 use std::collections::HashSet;
 
 use crate::core::RelationStorage;
-use crate::gui::state::{
-    CentralView, ChaseEventRecord, ChaseMode, ChaseVisualizationState, GuiState, SelectedItem,
-};
+use crate::gui::state::{ChaseEventRecord, ChaseMode, ChaseVisualizationState, CentralView, GuiState, SelectedItem};
 use crate::query::chase::{ChaseControl, ChaseEvent, ChaseObserver};
 
 /// Chase visualization panel
@@ -52,10 +50,7 @@ impl ChaseVisualization {
             ui.label("No instances defined. Create an instance first.");
         } else {
             for instance in instances {
-                if ui
-                    .button(format!("{} : {}", instance.name, instance.theory_name))
-                    .clicked()
-                {
+                if ui.button(format!("{} : {}", instance.name, instance.theory_name)).clicked() {
                     state.start_chase(&instance.name);
                 }
             }
@@ -65,10 +60,7 @@ impl ChaseVisualization {
         if let Some(SelectedItem::Instance(name)) = &state.selected_item {
             ui.add_space(16.0);
             let name = name.clone();
-            if ui
-                .button(format!("Start Chase on selected: {}", name))
-                .clicked()
-            {
+            if ui.button(format!("Start Chase on selected: {}", name)).clicked() {
                 state.start_chase(&name);
             }
         }
@@ -194,11 +186,11 @@ impl ChaseVisualization {
                             );
 
                             let color = if is_current {
-                                ui.visuals().hyperlink_color
+                                egui::Color32::YELLOW
                             } else if event.changed {
-                                egui::Color32::from_rgb(25, 110, 55)
+                                egui::Color32::from_rgb(100, 200, 100)
                             } else {
-                                ui.visuals().weak_text_color()
+                                egui::Color32::LIGHT_GRAY
                             };
 
                             ui.label(egui::RichText::new(text).color(color).monospace());
@@ -620,10 +612,7 @@ impl<'a> ChaseObserver for GuiChaseObserver<'a> {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use crate::core::{
-        Context, DerivedSort, ElaboratedTheory, Formula, Sequent, Signature, Structure, Term,
-        Theory,
-    };
+    use crate::core::{Context, DerivedSort, ElaboratedTheory, Formula, Sequent, Signature, Structure, Term, Theory};
     use crate::repl::InstanceEntry;
     use std::rc::Rc;
 
@@ -650,14 +639,8 @@ mod tests {
                 conclusion: Formula::Rel(
                     0,
                     Term::Record(vec![
-                        (
-                            "x".to_string(),
-                            Term::Var("x".to_string(), DerivedSort::Base(0)),
-                        ),
-                        (
-                            "y".to_string(),
-                            Term::Var("x".to_string(), DerivedSort::Base(0)),
-                        ),
+                        ("x".to_string(), Term::Var("x".to_string(), DerivedSort::Base(0))),
+                        ("y".to_string(), Term::Var("x".to_string(), DerivedSort::Base(0))),
                     ]),
                 ),
             }],
@@ -677,8 +660,11 @@ mod tests {
         let (b, _) = structure.add_element(&mut state.repl.store.universe, 0);
         structure.init_relations(&[2]);
 
-        let mut entry =
-            InstanceEntry::new(structure, "Preorder".to_string(), "Preorder".to_string());
+        let mut entry = InstanceEntry::new(
+            structure,
+            "Preorder".to_string(),
+            "Preorder".to_string(),
+        );
         entry.register_element("a".to_string(), a);
         entry.register_element("b".to_string(), b);
         state.repl.instances.insert("Chain".to_string(), entry);
@@ -732,14 +718,7 @@ mod tests {
 
         viz.step_chase(&mut state);
         assert_eq!(
-            state
-                .repl
-                .instances
-                .get("Chain")
-                .unwrap()
-                .structure
-                .relations[0]
-                .len(),
+            state.repl.instances.get("Chain").unwrap().structure.relations[0].len(),
             1
         );
 

src/gui/visualizations/graph.rs

@@ -83,8 +83,7 @@ impl GraphView {
         ui.separator();
 
         // Check if we need to rebuild the graph
-        if state.graph_instance != self.last_instance || state.graph_relation != self.last_relation
-        {
+        if state.graph_instance != self.last_instance || state.graph_relation != self.last_relation {
             self.rebuild_graph(state);
         }
 
@@ -110,23 +109,21 @@ impl GraphView {
 
                         ui.label("Relation:");
                         egui::ComboBox::from_label("")
-                            .selected_text(self.selected_relation.as_deref().unwrap_or("(all)"))
+                            .selected_text(
+                                self.selected_relation
+                                    .as_deref()
+                                    .unwrap_or("(all)"),
+                            )
                             .show_ui(ui, |ui| {
-                                if ui
-                                    .selectable_label(self.selected_relation.is_none(), "(all)")
-                                    .clicked()
-                                {
+                                if ui.selectable_label(self.selected_relation.is_none(), "(all)").clicked() {
                                     self.selected_relation = None;
                                     self.needs_layout = true;
                                 }
                                 for rel in relations {
-                                    if ui
-                                        .selectable_label(
-                                            self.selected_relation.as_deref() == Some(rel),
-                                            rel,
-                                        )
-                                        .clicked()
-                                    {
+                                    if ui.selectable_label(
+                                        self.selected_relation.as_deref() == Some(rel),
+                                        rel,
+                                    ).clicked() {
                                         self.selected_relation = Some(rel.to_string());
                                         self.needs_layout = true;
                                     }
@@ -186,10 +183,7 @@ impl GraphView {
             ui.label("No instances defined.");
         } else {
             for instance in instances {
-                if ui
-                    .button(format!("{} : {}", instance.name, instance.theory_name))
-                    .clicked()
-                {
+                if ui.button(format!("{} : {}", instance.name, instance.theory_name)).clicked() {
                     state.graph_instance = Some(instance.name.clone());
                     self.needs_layout = true;
                 }
@@ -236,10 +230,7 @@ impl GraphView {
                 .unwrap_or_else(|| format!("#{}", slid_idx));
 
             let sort_name = sig.sorts.get(sort_id).cloned().unwrap_or_default();
-            let color = sort_colors
-                .get(sort_id)
-                .copied()
-                .unwrap_or(egui::Color32::GRAY);
+            let color = sort_colors.get(sort_id).copied().unwrap_or(egui::Color32::GRAY);
 
             self.nodes.push(GraphNode {
                 id: slid,
@@ -335,11 +326,7 @@ impl GraphView {
         let mut max_y = f32::MIN;
 
         for node in &self.nodes {
-            let pos = self
-                .node_positions
-                .get(&node.id)
-                .copied()
-                .unwrap_or(node.position);
+            let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
             min_x = min_x.min(pos.x);
             min_y = min_y.min(pos.y);
             max_x = max_x.max(pos.x);
@@ -359,15 +346,17 @@ impl GraphView {
         // Reset pan to center the content (since our world origin is already at center)
         let world_center_x = (min_x + max_x) / 2.0;
         let world_center_y = (min_y + max_y) / 2.0;
-        self.pan = egui::Vec2::new(-world_center_x * self.zoom, -world_center_y * self.zoom);
+        self.pan = egui::Vec2::new(
+            -world_center_x * self.zoom,
+            -world_center_y * self.zoom,
+        );
     }
 
     fn draw_graph(&mut self, ui: &mut egui::Ui) {
-        let (response, painter) =
-            ui.allocate_painter(ui.available_size(), egui::Sense::click_and_drag());
-        let edge_color = ui.visuals().weak_text_color();
-        let border_color = ui.visuals().text_color();
-        let hint_color = ui.visuals().weak_text_color();
+        let (response, painter) = ui.allocate_painter(
+            ui.available_size(),
+            egui::Sense::click_and_drag(),
+        );
 
         let rect = response.rect;
         let pointer_delta = ui.input(|i| i.pointer.delta());
@@ -393,10 +382,8 @@ impl GraphView {
                         .copied()
                         .unwrap_or(node.position);
                     let screen_pos = hit_test_transform(pos);
-                    let node_rect = egui::Rect::from_center_size(
-                        screen_pos,
-                        egui::Vec2::splat(node_radius * 2.0),
-                    );
+                    let node_rect =
+                        egui::Rect::from_center_size(screen_pos, egui::Vec2::splat(node_radius * 2.0));
                     node_rect.contains(pointer).then_some(node.id)
                 })
             })
@@ -452,12 +439,14 @@ impl GraphView {
                     painter.circle_stroke(
                         loop_center,
                         10.0 * self.zoom,
-                        egui::Stroke::new(1.5, edge_color),
+                        egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
                     );
                 } else {
                     // Regular edge
-                    painter
-                        .line_segment([from_screen, to_screen], egui::Stroke::new(1.5, edge_color));
+                    painter.line_segment(
+                        [from_screen, to_screen],
+                        egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
+                    );
 
                     // Draw arrowhead
                     let dir = (to_screen - from_screen).normalized();
@@ -472,7 +461,7 @@ impl GraphView {
 
                     painter.add(egui::Shape::convex_polygon(
                         vec![p1, p2, p3],
-                        edge_color,
+                        egui::Color32::LIGHT_GRAY,
                         egui::Stroke::NONE,
                     ));
                 }
@@ -481,11 +470,7 @@ impl GraphView {
 
         // Draw nodes
         for node in &self.nodes {
-            let pos = self
-                .node_positions
-                .get(&node.id)
-                .copied()
-                .unwrap_or(node.position);
+            let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
             let screen_pos = transform(pos);
             let is_hovered = hovered_node == Some(node.id);
 
@@ -512,7 +497,7 @@ impl GraphView {
             painter.circle_stroke(
                 screen_pos,
                 node_radius,
-                egui::Stroke::new(2.0, border_color),
+                egui::Stroke::new(2.0, egui::Color32::WHITE),
             );
 
             // Draw node label
@@ -522,7 +507,7 @@ impl GraphView {
                 egui::Align2::CENTER_CENTER,
                 &node.name,
                 egui::FontId::proportional(font_size),
-                text_color_for_fill(fill_color),
+                egui::Color32::WHITE,
             );
 
             // Draw sort label below
@@ -532,7 +517,7 @@ impl GraphView {
                     egui::Align2::CENTER_TOP,
                     &node.sort,
                     egui::FontId::proportional(10.0 * self.zoom),
-                    hint_color,
+                    egui::Color32::LIGHT_GRAY,
                 );
             }
         }
@@ -544,7 +529,7 @@ impl GraphView {
                 egui::Align2::CENTER_CENTER,
                 "No elements to display",
                 egui::FontId::proportional(16.0),
-                hint_color,
+                egui::Color32::GRAY,
             );
         }
     }
@@ -569,16 +554,6 @@ fn generate_sort_colors(count: usize) -> Vec<egui::Color32> {
     colors
 }
 
-fn text_color_for_fill(fill: egui::Color32) -> egui::Color32 {
-    let luminance =
-        (0.2126 * fill.r() as f32 + 0.7152 * fill.g() as f32 + 0.0722 * fill.b() as f32) / 255.0;
-    if luminance > 0.6 {
-        egui::Color32::BLACK
-    } else {
-        egui::Color32::WHITE
-    }
-}
-
 /// Convert HSV to RGB
 fn hsv_to_rgb(h: f32, s: f32, v: f32) -> (u8, u8, u8) {
     let c = v * s;