habedi-work/geolog-zeta-fork
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Compare commits

base: habedi-work:af0e3560d5026c35d2d80537ebfbf2241c8954b9
Branches Tags
habedi-work:master
...
compare: habedi-work:638bb6db8ed33c4922acc4e4a3439bed6c1e9976
Branches Tags
habedi-work:master

2 Commits
af0e3560d5 ... 638bb6db8e

Author SHA1 Message Date
Hassan Abedi
638bb6db8e Add an AGENTS.md file to project 2026-03-23 09:55:15 +01:00
Hassan Abedi
e97b87060a Fix a few bugs in the GUI 2026-03-23 09:55:11 +01:00
12 changed files with 1330 additions and 996 deletions
Show Stats Expand all files Collapse all files

146
AGENTS.md Normal file
View File

@ -0,0 +1,146 @@
# 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.

1001
Cargo.lock generated
View File

File diff suppressed because it is too large Load Diff

6
Cargo.toml
View File

@ -31,15 +31,15 @@ default = []
gui = ["eframe", "egui_extras", "rfd"]
[dependencies.eframe]
version = "0.29"
version = "0.33.3"
optional = true
[dependencies.egui_extras]
version = "0.29"
version = "0.33.3"
optional = true
[dependencies.rfd]
version = "0.15"
version = "0.17.2"
optional = true
[[bin]]

45
README2.md
View File

@ -37,6 +37,10 @@ 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
@ -79,18 +83,19 @@ src/gui/
- Filter/search functionality
- Click to select, right-click for context menu
- Shows counts (sorts, functions, relations, axioms, elements)
- Fixed-width docked sidebar
**Editor Panel (Center Top)**
**Editor Panel (Center)**
- Multi-line code editor
- Line numbers
- Run button (or Ctrl+Enter) to execute code
- Clear button
**Inspector Panel (Center Bottom)**
**Inspector Panel (Right)**
- Theory details: parameters, sorts, functions, relations, instance fields, axioms
- Instance details: elements by sort, function values, relation tuples, nested instances
- Collapsible sections
- "View Graph" button for instances
- Fixed-width docked sidebar in the main workspace view
**Console Panel (Bottom)**
- Scrollable message log
@ -103,11 +108,13 @@ src/gui/
- Type `:inspect <name>` to inspect
- Type `:chase <instance>` to run chase
- Or type geolog code directly
- Fixed-height docked footer
**Adjustable Panels**
- Browser panel (left): drag right edge to resize
- Console panel (bottom): drag top edge to resize
- Editor/Inspector split: drag the separator bar between them
**Layout**
- Docked workspace layout for stability
- Browser on the left, editor in the center, inspector on the right
- Console fixed at the bottom
- Chase and graph visualizations replace the central workspace when active
**Chase Visualization**
- Step/Run All/Stop controls
@ -129,22 +136,14 @@ src/gui/
```
┌─────────────────────────────────────────────────────────────┐
│ File Edit View Chase Help │
├────────────┬────────────────────────────────────────────────┤
│ ▼ Theories │ ┌─────────────────────────────────────────┐ │
│ Preorder │ │ Editor │ │
│ Graph │ │ theory Foo { │ │
│ ▼ Instances│ │ X : Sort; │ │
│ Chain3 │ │ } [Run] [Clear] │ │
│ │ ├─────────────────────────────────────────┤ │
│ │ │ ═══════════ [drag to resize] ═══════════│ │
│ │ ├─────────────────────────────────────────┤ │
│ │ │ Inspector: Chain3 : Preorder │ │
│ │ │ ▼ Elements (3) │ │
│ │ │ X: bot, mid, top │ │
│ │ │ ▼ Relations │ │
│ │ │ leq: 6 tuples [View Graph] │ │
│ │ └─────────────────────────────────────────┘ │
├────────────┴────────────────────────────────────────────────┤
├──────────────┬──────────────────────────────┬───────────────┤
│ Browser │ Editor │ Inspector │
│ ▼ Theories │ theory Foo { │ Chain3 │
│ Preorder │ X : Sort; │ : Preorder │
│ ▼ Instances │ } [Run] [Clear] │ ▼ Elements │
│ Chain3 │ │ ▼ Relations │
│ │ │ [View Graph] │
├──────────────┴──────────────────────────────┴───────────────┤
│ Console [Clear]│
│ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms) │
│ + Defined instance Chain3 : Preorder (3 elements) │

32
src/bin/geolog-gui.rs
View File

@ -113,22 +113,24 @@ fn parse_args(args: &[String]) -> (Option<PathBuf>, Vec<PathBuf>) {
fn setup_fonts(ctx: &egui::Context) {
// Use a slightly larger default font
let mut style = (*ctx.style()).clone();
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.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));
// Set up dark theme with custom colors
style.visuals = egui::Visuals::dark();
style.visuals.override_text_color = Some(egui::Color32::from_gray(220));
// Force a light theme for the GUI.
style.visuals = egui::Visuals::light();
style.visuals.widgets.noninteractive.expansion = 0.0;
style.visuals.widgets.inactive.expansion = 0.0;
style.visuals.widgets.hovered.expansion = 0.0;
style.visuals.widgets.active.expansion = 0.0;
style.visuals.widgets.open.expansion = 0.0;
ctx.set_style(style);
}

153
src/gui/app.rs
View File

@ -21,9 +21,6 @@ pub struct GeologApp {
console: ConsolePanel,
chase_viz: ChaseVisualization,
graph_view: GraphView,
/// Editor/Inspector split ratio (0.0 to 1.0, where 0.5 = equal)
editor_split: f32,
}
impl GeologApp {
@ -37,7 +34,6 @@ impl GeologApp {
console: ConsolePanel::new(),
chase_viz: ChaseVisualization::new(),
graph_view: GraphView::new(),
editor_split: 0.5, // 50% editor, 50% inspector
}
}
@ -50,21 +46,21 @@ impl GeologApp {
/// Render the menu bar
fn menu_bar(&mut self, ui: &mut egui::Ui) {
egui::menu::bar(ui, |ui| {
egui::MenuBar::new().ui(ui, |ui| {
ui.menu_button("File", |ui| {
if ui.button("Open...").clicked() {
self.handle_open_file();
ui.close_menu();
ui.close();
}
if ui.button("Save").clicked() {
self.handle_save_file();
ui.close_menu();
ui.close();
}
ui.separator();
if ui.button("Reset State").clicked() {
self.state.repl.reset();
self.state.reset_runtime_state();
self.state.log_info("State reset");
ui.close_menu();
ui.close();
}
ui.separator();
if ui.button("Quit").clicked() {
@ -75,11 +71,11 @@ impl GeologApp {
ui.menu_button("Edit", |ui| {
if ui.button("Clear Editor").clicked() {
self.state.editor_content.clear();
ui.close_menu();
ui.close();
}
if ui.button("Clear Console").clicked() {
self.state.clear_console();
ui.close_menu();
ui.close();
}
});
@ -92,7 +88,7 @@ impl GeologApp {
.clicked()
{
self.state.central_view = CentralView::EditorAndInspector;
ui.close_menu();
ui.close();
}
if ui
.selectable_label(
@ -102,7 +98,7 @@ impl GeologApp {
.clicked()
{
self.state.central_view = CentralView::ChaseVisualization;
ui.close_menu();
ui.close();
}
if ui
.selectable_label(
@ -112,7 +108,7 @@ impl GeologApp {
.clicked()
{
self.state.central_view = CentralView::GraphVisualization;
ui.close_menu();
ui.close();
}
});
@ -123,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_menu();
ui.close();
}
if ui.button(format!("Debug Chase on {}", name)).clicked() {
self.state.start_chase(&name);
ui.close_menu();
ui.close();
}
} else {
ui.label("(Select an instance first)");
@ -136,15 +132,13 @@ 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_menu();
self.state
.log_info(format!("Geolog GUI v{}", env!("CARGO_PKG_VERSION")));
ui.close();
}
if ui.button("Syntax Help").clicked() {
self.show_syntax_help();
ui.close_menu();
ui.close();
}
});
});
@ -152,7 +146,7 @@ impl GeologApp {
/// Handle opening a file
fn handle_open_file(&mut self) {
if let Some(path) = rfd::FileDialog::new()
if let Some(path) = Self::new_file_dialog()
.add_filter("Geolog", &["geolog"])
.add_filter("All Files", &["*"])
.pick_file()
@ -174,7 +168,7 @@ impl GeologApp {
}
} else {
// Save As
if let Some(path) = rfd::FileDialog::new()
if let Some(path) = Self::new_file_dialog()
.add_filter("Geolog", &["geolog"])
.save_file()
{
@ -191,6 +185,14 @@ 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;
@ -246,8 +248,7 @@ 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!(
@ -259,8 +260,7 @@ impl GeologApp {
// Show structure summary
self.state.log_info(format!(
"Structure: {} elements, {} relation tuples",
num_elements,
total_tuples
num_elements, total_tuples
));
}
Err(e) => {
@ -290,80 +290,7 @@ impl GeologApp {
fn central_panel(&mut self, ui: &mut egui::Ui) {
match self.state.central_view {
CentralView::EditorAndInspector => {
// Split vertically: editor on top, inspector on bottom
let available_height = ui.available_height();
let splitter_height = 8.0;
// Ensure heights are never negative
let usable_height = (available_height - splitter_height).max(0.0);
let editor_height = (usable_height * self.editor_split).max(0.0);
let inspector_height = (usable_height * (1.0 - self.editor_split)).max(0.0);
// Editor section
ui.allocate_ui_with_layout(
egui::vec2(ui.available_width(), editor_height),
egui::Layout::top_down(egui::Align::LEFT),
|ui| {
self.editor.show(ui, &mut self.state);
},
);
// Draggable splitter
let splitter_response = ui.allocate_response(
egui::vec2(ui.available_width(), splitter_height),
egui::Sense::drag(),
);
// Draw splitter bar
let splitter_rect = splitter_response.rect;
let is_dragging = splitter_response.dragged();
let is_hovered = splitter_response.hovered();
let splitter_color = if is_dragging {
egui::Color32::from_rgb(100, 150, 255)
} else if is_hovered {
egui::Color32::from_rgb(80, 80, 100)
} else {
egui::Color32::from_rgb(60, 60, 70)
};
ui.painter().rect_filled(splitter_rect, 0.0, splitter_color);
// Draw grip lines
let center_y = splitter_rect.center().y;
let grip_width = 30.0;
let grip_x = splitter_rect.center().x;
for i in -1..=1 {
let y = center_y + (i as f32) * 2.0;
ui.painter().line_segment(
[
egui::pos2(grip_x - grip_width / 2.0, y),
egui::pos2(grip_x + grip_width / 2.0, y),
],
egui::Stroke::new(1.0, egui::Color32::GRAY),
);
}
// Handle dragging
if is_dragging {
let delta = splitter_response.drag_delta().y;
let divisor = (available_height - splitter_height).max(1.0);
let new_split = self.editor_split + delta / divisor;
self.editor_split = new_split.clamp(0.1, 0.9);
}
// Change cursor when hovering
if is_hovered || is_dragging {
ui.ctx().set_cursor_icon(egui::CursorIcon::ResizeVertical);
}
// Inspector section
ui.allocate_ui_with_layout(
egui::vec2(ui.available_width(), inspector_height),
egui::Layout::top_down(egui::Align::LEFT),
|ui| {
self.inspector.show(ui, &mut self.state);
},
);
self.editor.show(ui, &mut self.state);
}
CentralView::ChaseVisualization => {
self.chase_viz.show(ui, &mut self.state);
@ -384,18 +311,28 @@ impl eframe::App for GeologApp {
// Left panel: Browser
egui::SidePanel::left("browser_panel")
.default_width(200.0)
.min_width(150.0)
.resizable(true)
.default_width(240.0)
.min_width(240.0)
.resizable(false)
.show(ctx, |ui| {
self.browser.show(ui, &mut self.state);
});
if self.state.central_view == CentralView::EditorAndInspector {
egui::SidePanel::right("inspector_panel")
.default_width(340.0)
.min_width(340.0)
.resizable(false)
.show(ctx, |ui| {
self.inspector.show(ui, &mut self.state);
});
}
// Bottom panel: Console
egui::TopBottomPanel::bottom("console_panel")
.default_height(150.0)
.min_height(100.0)
.resizable(true)
.default_height(200.0)
.min_height(200.0)
.resizable(false)
.show(ctx, |ui| {
self.console.show(ui, &mut self.state);
});

6
src/gui/panels/browser.rs
View File

@ -147,7 +147,7 @@ impl BrowserPanel {
if ui.button("Inspect").clicked() {
state.selected_item =
Some(SelectedItem::Instance(instance.name.clone()));
ui.close_menu();
ui.close();
}
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_menu();
ui.close();
}
if ui.button("View Graph").clicked() {
state.show_graph(&instance.name, None);
ui.close_menu();
ui.close();
}
});
}

282
src/gui/panels/console.rs
View File

@ -3,9 +3,10 @@
//! Shows a scrollable log of messages with color coding and a REPL input.
use eframe::egui;
use egui_extras::{Size, StripBuilder};
use crate::gui::state::{GuiState, MessageKind};
use crate::repl::{MetaCommand, ListTarget, ExecuteResult};
use crate::repl::{ExecuteResult, ListTarget, MetaCommand};
/// Console panel for output messages and REPL input
pub struct ConsolePanel {
@ -30,101 +31,122 @@ impl ConsolePanel {
}
pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
// Header with title and buttons
ui.horizontal(|ui| {
ui.heading("Console");
ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
if ui.button("Clear").clicked() {
state.clear_console();
}
ui.checkbox(&mut self.auto_scroll, "Auto-scroll");
ui.label(format!("{} messages", state.console_messages.len()));
});
});
ui.separator();
// Scrollable message area (takes most of the space)
let available_height = (ui.available_height() - 30.0).max(50.0); // Reserve space for input
let scroll_area = egui::ScrollArea::vertical()
.auto_shrink([false, false])
.max_height(available_height)
.stick_to_bottom(self.auto_scroll);
scroll_area.show(ui, |ui| {
if state.console_messages.is_empty() {
ui.label("Type commands below (e.g., :help, :list, or geolog code)");
} else {
for message in &state.console_messages {
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 => ">",
MessageKind::Success => "+",
MessageKind::Error => "!",
MessageKind::Warning => "?",
};
StripBuilder::new(ui)
.size(Size::exact(28.0))
.size(Size::remainder().at_least(80.0))
.size(Size::exact(28.0))
.vertical(|mut strip| {
strip.cell(|ui| {
ui.horizontal(|ui| {
ui.label(
egui::RichText::new(prefix)
.color(color)
.monospace(),
);
ui.label(
egui::RichText::new(&message.text)
.color(color)
.monospace(),
);
ui.heading("Console");
ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
if ui
.add_sized([64.0, 22.0], egui::Button::new("Clear"))
.clicked()
{
state.clear_console();
}
ui.add_sized(
[112.0, 22.0],
egui::Checkbox::new(&mut self.auto_scroll, "Auto-scroll"),
);
ui.add_sized(
[96.0, 22.0],
egui::Label::new(format!("{} messages", state.console_messages.len())),
);
});
});
}
}
});
});
// REPL input at the bottom
ui.separator();
ui.horizontal(|ui| {
ui.label(
egui::RichText::new("geolog>")
.monospace()
.color(egui::Color32::from_rgb(100, 150, 255)),
);
strip.cell(|ui| {
egui::Frame::default()
.inner_margin(egui::Margin::same(4))
.show(ui, |ui| {
egui::ScrollArea::vertical()
.auto_shrink([false, false])
.stick_to_bottom(self.auto_scroll)
.show(ui, |ui| {
if state.console_messages.is_empty() {
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 response = ui.add(
egui::TextEdit::singleline(&mut self.input)
.font(egui::FontId::monospace(13.0))
.desired_width((ui.available_width() - 60.0).max(50.0))
.hint_text(":help for commands"),
);
let prefix = match message.kind {
MessageKind::Info => ">",
MessageKind::Success => "+",
MessageKind::Error => "!",
MessageKind::Warning => "?",
};
// Handle Enter key
if response.lost_focus() && ui.input(|i| i.key_pressed(egui::Key::Enter)) {
self.execute_input(state);
response.request_focus();
}
ui.horizontal(|ui| {
ui.add_sized(
[12.0, 18.0],
egui::Label::new(
egui::RichText::new(prefix)
.color(color)
.monospace(),
),
);
ui.label(
egui::RichText::new(&message.text)
.color(color)
.monospace(),
);
});
}
}
});
});
});
// Handle Up/Down for history
if response.has_focus() {
if ui.input(|i| i.key_pressed(egui::Key::ArrowUp)) {
self.history_up();
}
if ui.input(|i| i.key_pressed(egui::Key::ArrowDown)) {
self.history_down();
}
}
strip.cell(|ui| {
ui.horizontal(|ui| {
ui.add_sized(
[68.0, 22.0],
egui::Label::new(
egui::RichText::new("geolog>")
.monospace()
.color(ui.visuals().hyperlink_color),
),
);
if ui.button("Run").clicked() {
self.execute_input(state);
}
});
let run_width = 56.0;
let spacing = ui.spacing().item_spacing.x;
let input_width = (ui.available_width() - run_width - spacing).max(120.0);
let response = ui.add_sized(
[input_width, 22.0],
egui::TextEdit::singleline(&mut self.input)
.font(egui::FontId::monospace(13.0))
.hint_text(":help for commands"),
);
if response.lost_focus() && ui.input(|i| i.key_pressed(egui::Key::Enter)) {
self.execute_input(state);
response.request_focus();
}
if response.has_focus() {
if ui.input(|i| i.key_pressed(egui::Key::ArrowUp)) {
self.history_up();
}
if ui.input(|i| i.key_pressed(egui::Key::ArrowDown)) {
self.history_down();
}
}
if ui
.add_sized([run_width, 22.0], egui::Button::new("Run"))
.clicked()
{
self.execute_input(state);
}
});
});
});
}
fn execute_input(&mut self, state: &mut GuiState) {
@ -204,24 +226,22 @@ 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.");
}
Some(t) => {
state.log_info(format!("Help topic: {}", t));
}
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));
}
},
MetaCommand::List(target) => {
match target {
ListTarget::Theories | ListTarget::All => {
@ -259,7 +279,7 @@ impl ConsolePanel {
}
}
MetaCommand::Inspect(name) => {
use crate::repl::{InspectResult, format_theory_detail, format_instance_detail};
use crate::repl::{format_instance_detail, format_theory_detail, InspectResult};
match state.repl.inspect(&name) {
Some(InspectResult::Theory(detail)) => {
for line in format_theory_detail(&detail).lines() {
@ -280,26 +300,26 @@ impl ConsolePanel {
state.clear_console();
}
MetaCommand::Reset => {
state.repl.reset();
state.selected_item = None;
state.reset_runtime_state();
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();
}
Err(e) => {
state.log_error(format!("Failed to load: {}", e));
}
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));
}
},
_ => {
state.log_warning("Command not yet implemented in GUI");
}
@ -334,7 +354,11 @@ 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);
@ -362,8 +386,7 @@ impl ConsolePanel {
));
state.log_info(format!(
"Structure: {} elements, {} relation tuples",
num_elements,
total_tuples
num_elements, total_tuples
));
}
Err(e) => {
@ -405,6 +428,15 @@ 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()

73
src/gui/panels/editor.rs
View File

@ -7,16 +7,11 @@ use eframe::egui;
use crate::gui::state::GuiState;
/// Code editor panel
pub struct EditorPanel {
/// Whether to show line numbers
show_line_numbers: bool,
}
pub struct EditorPanel {}
impl EditorPanel {
pub fn new() -> Self {
Self {
show_line_numbers: true,
}
Self {}
}
pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
@ -59,58 +54,26 @@ impl EditorPanel {
// Use a monospace font for code
let font_id = egui::FontId::monospace(14.0);
// Calculate line numbers if needed
let line_count = state.editor_content.lines().count().max(1);
let line_number_width = if self.show_line_numbers {
let digits = (line_count as f32).log10().floor() as usize + 1;
digits.max(2) as f32 * 10.0 + 8.0
} else {
0.0
};
// Main editor area - simplified layout without line numbers column
// to avoid layout instability from horizontal split calculations
let text_edit = egui::TextEdit::multiline(&mut state.editor_content)
.font(font_id)
.code_editor()
.desired_width(f32::INFINITY)
.desired_rows(20)
.lock_focus(true);
ui.horizontal(|ui| {
// Line numbers column
if self.show_line_numbers {
ui.allocate_ui_with_layout(
egui::vec2(line_number_width, ui.available_height().max(0.0)),
egui::Layout::top_down(egui::Align::RIGHT),
|ui| {
ui.style_mut().visuals.override_text_color =
Some(egui::Color32::GRAY);
let response = ui.add(text_edit);
for i in 1..=line_count {
ui.label(
egui::RichText::new(format!("{}", i))
.font(font_id.clone())
.color(egui::Color32::GRAY),
);
}
},
);
ui.separator();
}
// Main editor area
let text_edit = egui::TextEdit::multiline(&mut state.editor_content)
.font(font_id)
.code_editor()
.desired_width(f32::INFINITY)
.desired_rows(20)
.lock_focus(true);
let response = ui.add(text_edit);
// Handle keyboard shortcuts
if response.has_focus() {
let modifiers = ui.input(|i| i.modifiers);
if modifiers.ctrl || modifiers.command {
if ui.input(|i| i.key_pressed(egui::Key::Enter)) {
state.execute_editor();
}
// Handle keyboard shortcuts
if response.has_focus() {
let modifiers = ui.input(|i| i.modifiers);
if modifiers.ctrl || modifiers.command {
if ui.input(|i| i.key_pressed(egui::Key::Enter)) {
state.execute_editor();
}
}
});
}
}
}

52
src/gui/state.rs
View File

@ -5,6 +5,7 @@
use std::collections::HashSet;
use std::path::PathBuf;
use crate::core::Structure;
use crate::repl::{InstanceDetail, ReplState, TheoryDetail};
/// What item is currently selected in the browser
@ -57,6 +58,7 @@ pub enum ChaseMode {
pub struct ChaseVisualizationState {
pub mode: ChaseMode,
pub instance_name: String,
pub initial_structure: Structure,
pub events: Vec<ChaseEventRecord>,
pub current_event: usize,
pub current_iteration: usize,
@ -65,10 +67,11 @@ pub struct ChaseVisualizationState {
}
impl ChaseVisualizationState {
pub fn new(instance_name: String) -> Self {
pub fn new(instance_name: String, initial_structure: Structure) -> Self {
Self {
mode: ChaseMode::Idle,
instance_name,
initial_structure,
events: Vec::new(),
current_event: 0,
current_iteration: 0,
@ -176,6 +179,16 @@ 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 {
@ -308,7 +321,15 @@ impl GuiState {
/// Start a chase visualization for an instance
pub fn start_chase(&mut self, instance_name: &str) {
self.chase_state = Some(ChaseVisualizationState::new(instance_name.to_string()));
let Some(entry) = self.repl.instances.get(instance_name) else {
self.log_error(format!("Instance '{}' not found", instance_name));
return;
};
self.chase_state = Some(ChaseVisualizationState::new(
instance_name.to_string(),
entry.structure.clone(),
));
self.central_view = CentralView::ChaseVisualization;
}
@ -319,3 +340,30 @@ 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")));
}
}

379
src/gui/visualizations/chase.rs
View File

@ -3,9 +3,12 @@
//! Provides step-through debugging and visualization of the chase algorithm.
use eframe::egui;
use std::collections::HashSet;
use crate::core::RelationStorage;
use crate::gui::state::{ChaseEventRecord, ChaseMode, ChaseVisualizationState, CentralView, GuiState, SelectedItem};
use crate::gui::state::{
CentralView, ChaseEventRecord, ChaseMode, ChaseVisualizationState, GuiState, SelectedItem,
};
use crate::query::chase::{ChaseControl, ChaseEvent, ChaseObserver};
/// Chase visualization panel
@ -49,7 +52,10 @@ 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);
}
}
@ -59,7 +65,10 @@ 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);
}
}
@ -67,9 +76,9 @@ impl ChaseVisualization {
fn show_chase_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
// Read mode and instance_name before mutable operations
let (mode, instance_name) = {
let mode = {
let chase_state = state.chase_state.as_ref().unwrap();
(chase_state.mode, chase_state.instance_name.clone())
chase_state.mode
};
// Control buttons
@ -130,7 +139,7 @@ impl ChaseVisualization {
}
}
if reset_clicked {
state.chase_state = Some(ChaseVisualizationState::new(instance_name));
self.reset_chase(state);
}
if close_clicked {
state.chase_state = None;
@ -185,11 +194,11 @@ impl ChaseVisualization {
);
let color = if is_current {
egui::Color32::YELLOW
ui.visuals().hyperlink_color
} else if event.changed {
egui::Color32::from_rgb(100, 200, 100)
egui::Color32::from_rgb(25, 110, 55)
} else {
egui::Color32::LIGHT_GRAY
ui.visuals().weak_text_color()
};
ui.label(egui::RichText::new(text).color(color).monospace());
@ -283,14 +292,40 @@ impl ChaseVisualization {
}
}
fn reset_chase(&mut self, state: &mut GuiState) {
let Some(chase_state) = &state.chase_state else {
return;
};
let instance_name = chase_state.instance_name.clone();
let initial_structure = chase_state.initial_structure.clone();
let breakpoints = chase_state.breakpoints.clone();
let Some(entry) = state.repl.instances.get_mut(&instance_name) else {
state.log_error(format!("Instance '{}' not found", instance_name));
return;
};
entry.structure = initial_structure.clone();
let mut new_state = ChaseVisualizationState::new(instance_name, initial_structure);
new_state.breakpoints = breakpoints;
state.chase_state = Some(new_state);
self.new_breakpoint.clear();
state.log_info("Chase visualization reset");
}
/// Execute a single step of the chase
fn step_chase(&mut self, state: &mut GuiState) {
let instance_name = match &state.chase_state {
Some(s) => s.instance_name.clone(),
None => return,
};
let current_iteration = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0);
let breakpoints = state
.chase_state
.as_ref()
.map(|s| s.breakpoints.clone())
.unwrap_or_default();
// Get theory name first (immutable borrow)
let theory_name = match state.repl.instances.get(&instance_name) {
@ -313,13 +348,7 @@ impl ChaseVisualization {
let entry = state.repl.instances.get_mut(&instance_name).unwrap();
// Create a GUI observer that records events
let mut observer = GuiChaseObserver {
events: Vec::new(),
slid_to_name: &entry.slid_to_name,
iteration: current_iteration,
step_mode: true,
steps_remaining: 1,
};
let mut observer = GuiChaseObserver::new(&entry.slid_to_name, Some(1), breakpoints);
// Run chase with observer (just one step)
let sig = &theory.theory.signature;
@ -332,33 +361,43 @@ impl ChaseVisualization {
&mut entry.structure,
&mut state.repl.store.universe,
sig,
1, // Just one iteration
100,
&mut observer,
);
// Record events
let events = observer.events;
let GuiChaseObserver {
events,
iteration: current_iteration,
breakpoint_hit: paused_on_breakpoint,
completed_iterations,
..
} = observer;
if let Some(chase_state) = &mut state.chase_state {
chase_state.mode = ChaseMode::Stepping;
for event in events {
chase_state.events.push(event);
chase_state.events.extend(events);
if !chase_state.events.is_empty() {
chase_state.current_event = chase_state.events.len() - 1;
}
chase_state.current_event = chase_state.events.len().saturating_sub(1);
chase_state.current_iteration += 1;
chase_state.current_iteration = chase_state.current_iteration.max(current_iteration);
if let Ok(iterations) = result {
if iterations == 0 {
chase_state.mode = ChaseMode::Completed;
chase_state.total_iterations = Some(chase_state.current_iteration);
}
if let Some(iterations) = completed_iterations {
chase_state.mode = ChaseMode::Completed;
chase_state.current_iteration = iterations;
chase_state.total_iterations = Some(iterations);
}
}
// Log completion separately
if let Ok(iterations) = result {
if iterations == 0 {
let total = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0);
state.log_success(format!("Chase completed after {} iterations", total));
match result {
Ok(_) => {
if let Some(bp) = paused_on_breakpoint {
state.log_info(format!("Paused at breakpoint '{}'", bp));
}
if let Some(iterations) = completed_iterations {
state.log_success(format!("Chase completed after {} iterations", iterations));
}
}
Err(e) => {
state.log_error(format!("Chase error: {}", e));
}
}
}
@ -387,34 +426,70 @@ impl ChaseVisualization {
}
};
let breakpoints = state
.chase_state
.as_ref()
.map(|s| s.breakpoints.clone())
.unwrap_or_default();
// Now get mutable access to entry
let entry = state.repl.instances.get_mut(&instance_name).unwrap();
// Run chase to fixpoint
let sig = &theory.theory.signature;
let axioms = &theory.theory.axioms;
let axiom_names = &theory.theory.axiom_names;
let start = std::time::Instant::now();
let result = crate::query::chase::chase_fixpoint(
let mut observer = GuiChaseObserver::new(&entry.slid_to_name, None, breakpoints);
let result = crate::query::chase::chase_fixpoint_with_observer(
axioms,
axiom_names,
&mut entry.structure,
&mut state.repl.store.universe,
sig,
100,
&mut observer,
);
let GuiChaseObserver {
events,
iteration: current_iteration,
breakpoint_hit,
completed_iterations,
..
} = observer;
match result {
Ok(iterations) => {
Ok(_) => {
let elapsed = start.elapsed();
if let Some(chase_state) = &mut state.chase_state {
chase_state.mode = ChaseMode::Completed;
chase_state.total_iterations = Some(iterations);
chase_state.events.extend(events);
if !chase_state.events.is_empty() {
chase_state.current_event = chase_state.events.len() - 1;
}
chase_state.current_iteration =
chase_state.current_iteration.max(current_iteration);
if let Some(iterations) = completed_iterations {
chase_state.mode = ChaseMode::Completed;
chase_state.current_iteration = iterations;
chase_state.total_iterations = Some(iterations);
} else {
chase_state.mode = ChaseMode::Stepping;
chase_state.total_iterations = None;
}
}
if let Some(bp) = breakpoint_hit {
state.log_info(format!("Paused at breakpoint '{}'", bp));
} else if let Some(iterations) = completed_iterations {
state.log_success(format!(
"Chase completed in {} iterations ({:.2}ms)",
iterations,
elapsed.as_secs_f64() * 1000.0
));
}
state.log_success(format!(
"Chase completed in {} iterations ({:.2}ms)",
iterations,
elapsed.as_secs_f64() * 1000.0
));
}
Err(e) => {
state.log_error(format!("Chase error: {}", e));
@ -434,8 +509,30 @@ struct GuiChaseObserver<'a> {
events: Vec<ChaseEventRecord>,
slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>,
iteration: usize,
step_mode: bool,
steps_remaining: usize,
step_budget: Option<usize>,
breakpoints: HashSet<String>,
pending_breakpoint_hit: Option<String>,
breakpoint_hit: Option<String>,
completed_iterations: Option<usize>,
}
impl<'a> GuiChaseObserver<'a> {
fn new(
slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>,
step_budget: Option<usize>,
breakpoints: HashSet<String>,
) -> Self {
Self {
events: Vec::new(),
slid_to_name,
iteration: 0,
step_budget,
breakpoints,
pending_breakpoint_hit: None,
breakpoint_hit: None,
completed_iterations: None,
}
}
}
impl<'a> ChaseObserver for GuiChaseObserver<'a> {
@ -471,27 +568,189 @@ impl<'a> ChaseObserver for GuiChaseObserver<'a> {
binding: binding_vec,
changed: false, // Will be updated in AxiomFired
});
if self.step_mode {
self.steps_remaining = self.steps_remaining.saturating_sub(1);
if self.steps_remaining == 0 {
ChaseControl::Stop
} else {
ChaseControl::Continue
}
} else {
ChaseControl::Continue
}
self.pending_breakpoint_hit = axiom_name
.filter(|name| self.breakpoints.iter().any(|bp| name.contains(bp)))
.map(str::to_string);
ChaseControl::Continue
}
ChaseEvent::AxiomFired { changed, .. } => {
ChaseEvent::AxiomFired {
axiom_name,
changed,
..
} => {
// Update the last event with the changed status
if let Some(last) = self.events.last_mut() {
last.changed = changed;
}
ChaseControl::Continue
let mut should_stop = false;
if let Some(remaining) = &mut self.step_budget {
*remaining = remaining.saturating_sub(1);
if *remaining == 0 {
should_stop = true;
}
}
if let Some(bp) = self.pending_breakpoint_hit.take() {
self.breakpoint_hit = Some(bp);
should_stop = true;
} else if self.breakpoint_hit.is_none() {
self.breakpoint_hit = axiom_name
.filter(|name| self.breakpoints.iter().any(|bp| name.contains(bp)))
.map(str::to_string);
should_stop |= self.breakpoint_hit.is_some();
}
if should_stop {
ChaseControl::Stop
} else {
ChaseControl::Continue
}
}
ChaseEvent::IterationEnd { .. } => ChaseControl::Continue,
ChaseEvent::ChaseComplete { .. } => ChaseControl::Continue,
ChaseEvent::ChaseComplete { iterations } => {
self.completed_iterations = Some(iterations);
ChaseControl::Continue
}
}
}
}
#[cfg(test)]
mod tests {
use super::*;
use crate::core::{
Context, DerivedSort, ElaboratedTheory, Formula, Sequent, Signature, Structure, Term,
Theory,
};
use crate::repl::InstanceEntry;
use std::rc::Rc;
fn build_test_state() -> GuiState {
let mut state = GuiState::new();
let mut sig = Signature::default();
sig.add_sort("X".to_string());
sig.add_relation(
"leq".to_string(),
DerivedSort::Product(vec![
("x".to_string(), DerivedSort::Base(0)),
("y".to_string(), DerivedSort::Base(0)),
]),
);
let theory = Theory {
name: "Preorder".to_string(),
signature: sig,
axioms: vec![Sequent {
context: Context {
vars: vec![("x".to_string(), DerivedSort::Base(0))],
},
premise: Formula::True,
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)),
),
]),
),
}],
axiom_names: vec!["ax/refl".to_string()],
};
state.repl.theories.insert(
"Preorder".to_string(),
Rc::new(ElaboratedTheory {
params: vec![],
theory,
}),
);
let mut structure = Structure::new(1);
let (a, _) = structure.add_element(&mut state.repl.store.universe, 0);
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());
entry.register_element("a".to_string(), a);
entry.register_element("b".to_string(), b);
state.repl.instances.insert("Chain".to_string(), entry);
state.start_chase("Chain");
state
}
#[test]
fn gui_step_executes_exactly_one_firing() {
let mut state = build_test_state();
let mut viz = ChaseVisualization::new();
viz.step_chase(&mut state);
let entry = state.repl.instances.get("Chain").unwrap();
assert_eq!(entry.structure.relations[0].len(), 1);
let chase_state = state.chase_state.as_ref().unwrap();
assert_eq!(chase_state.events.len(), 1);
assert_eq!(chase_state.current_iteration, 1);
assert_eq!(chase_state.mode, ChaseMode::Stepping);
assert!(chase_state.events[0].changed);
}
#[test]
fn gui_run_all_pauses_after_breakpoint_and_records_event() {
let mut state = build_test_state();
let mut viz = ChaseVisualization::new();
state
.chase_state
.as_mut()
.unwrap()
.breakpoints
.insert("refl".to_string());
viz.run_chase_to_completion(&mut state);
let entry = state.repl.instances.get("Chain").unwrap();
assert_eq!(entry.structure.relations[0].len(), 1);
let chase_state = state.chase_state.as_ref().unwrap();
assert_eq!(chase_state.events.len(), 1);
assert_eq!(chase_state.current_iteration, 1);
assert_eq!(chase_state.mode, ChaseMode::Stepping);
}
#[test]
fn gui_reset_restores_initial_structure() {
let mut state = build_test_state();
let mut viz = ChaseVisualization::new();
viz.step_chase(&mut state);
assert_eq!(
state
.repl
.instances
.get("Chain")
.unwrap()
.structure
.relations[0]
.len(),
1
);
viz.reset_chase(&mut state);
let entry = state.repl.instances.get("Chain").unwrap();
assert_eq!(entry.structure.relations[0].len(), 0);
let chase_state = state.chase_state.as_ref().unwrap();
assert!(chase_state.events.is_empty());
assert_eq!(chase_state.current_iteration, 0);
assert_eq!(chase_state.mode, ChaseMode::Idle);
}
}

151
src/gui/visualizations/graph.rs
View File

@ -83,7 +83,8 @@ 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);
}
@ -109,21 +110,23 @@ 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;
}
@ -183,7 +186,10 @@ 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;
}
@ -230,7 +236,10 @@ 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,
@ -326,7 +335,11 @@ 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);
@ -346,23 +359,58 @@ 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 (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 rect = response.rect;
let pointer_delta = ui.input(|i| i.pointer.delta());
let pointer_pos = ui.input(|i| i.pointer.hover_pos());
let initial_zoom = self.zoom;
let initial_pan = self.pan;
let center = rect.center();
let hit_test_transform = |pos: egui::Pos2| -> egui::Pos2 {
egui::Pos2::new(
center.x + pos.x * initial_zoom + initial_pan.x,
center.y + pos.y * initial_zoom + initial_pan.y,
)
};
let node_radius = 20.0 * initial_zoom;
let hovered_node = if response.hovered() {
pointer_pos.and_then(|pointer| {
self.nodes.iter().find_map(|node| {
let pos = self
.node_positions
.get(&node.id)
.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),
);
node_rect.contains(pointer).then_some(node.id)
})
})
} else {
None
};
if response.drag_started() && hovered_node.is_some() {
self.dragged_node = hovered_node;
}
// Handle panning
if response.dragged() && self.dragged_node.is_none() {
self.pan += response.drag_delta();
self.pan += pointer_delta;
}
// Handle zooming with scroll
@ -381,8 +429,6 @@ impl GraphView {
}
}
// Transform helper - centers (0,0) world coordinates in the view
let center = rect.center();
let transform = |pos: egui::Pos2| -> egui::Pos2 {
egui::Pos2::new(
center.x + pos.x * self.zoom + self.pan.x,
@ -406,14 +452,12 @@ impl GraphView {
painter.circle_stroke(
loop_center,
10.0 * self.zoom,
egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
egui::Stroke::new(1.5, edge_color),
);
} else {
// Regular edge
painter.line_segment(
[from_screen, to_screen],
egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
);
painter
.line_segment([from_screen, to_screen], egui::Stroke::new(1.5, edge_color));
// Draw arrowhead
let dir = (to_screen - from_screen).normalized();
@ -428,7 +472,7 @@ impl GraphView {
painter.add(egui::Shape::convex_polygon(
vec![p1, p2, p3],
egui::Color32::LIGHT_GRAY,
edge_color,
egui::Stroke::NONE,
));
}
@ -436,31 +480,18 @@ impl GraphView {
}
// Draw nodes
let node_radius = 20.0 * self.zoom;
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);
// Check if node is being hovered or dragged
let node_rect = egui::Rect::from_center_size(
screen_pos,
egui::Vec2::splat(node_radius * 2.0),
);
let is_hovered = response.hovered()
&& ui.input(|i| i.pointer.hover_pos())
.map(|p| node_rect.contains(p))
.unwrap_or(false);
// Handle node dragging
if is_hovered && response.drag_started() {
self.dragged_node = Some(node.id);
}
let is_hovered = hovered_node == Some(node.id);
if self.dragged_node == Some(node.id) {
if response.dragged() {
let delta = response.drag_delta() / self.zoom;
let delta = pointer_delta / self.zoom;
if let Some(pos) = self.node_positions.get_mut(&node.id) {
*pos += delta;
}
@ -481,7 +512,7 @@ impl GraphView {
painter.circle_stroke(
screen_pos,
node_radius,
egui::Stroke::new(2.0, egui::Color32::WHITE),
egui::Stroke::new(2.0, border_color),
);
// Draw node label
@ -491,7 +522,7 @@ impl GraphView {
egui::Align2::CENTER_CENTER,
&node.name,
egui::FontId::proportional(font_size),
egui::Color32::WHITE,
text_color_for_fill(fill_color),
);
// Draw sort label below
@ -501,7 +532,7 @@ impl GraphView {
egui::Align2::CENTER_TOP,
&node.sort,
egui::FontId::proportional(10.0 * self.zoom),
egui::Color32::LIGHT_GRAY,
hint_color,
);
}
}
@ -513,7 +544,7 @@ impl GraphView {
egui::Align2::CENTER_CENTER,
"No elements to display",
egui::FontId::proportional(16.0),
egui::Color32::GRAY,
hint_color,
);
}
}
@ -538,6 +569,16 @@ 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;