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"] gui = ["eframe", "egui_extras", "rfd"]
[dependencies.eframe] [dependencies.eframe]
version = "0.29" version = "0.33.3"
optional = true optional = true
[dependencies.egui_extras] [dependencies.egui_extras]
version = "0.29" version = "0.33.3"
optional = true optional = true
[dependencies.rfd] [dependencies.rfd]
version = "0.15" version = "0.17.2"
optional = true optional = true
[[bin]] [[bin]]

45
README2.md
View File

@ -37,6 +37,10 @@ Usage in REPL:
A full-featured graphical interface built with egui. 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 #### Building the GUI
```bash ```bash
@ -79,18 +83,19 @@ src/gui/
- Filter/search functionality - Filter/search functionality
- Click to select, right-click for context menu - Click to select, right-click for context menu
- Shows counts (sorts, functions, relations, axioms, elements) - Shows counts (sorts, functions, relations, axioms, elements)
- Fixed-width docked sidebar
**Editor Panel (Center Top)** **Editor Panel (Center)**
- Multi-line code editor - Multi-line code editor
- Line numbers
- Run button (or Ctrl+Enter) to execute code - Run button (or Ctrl+Enter) to execute code
- Clear button - Clear button
**Inspector Panel (Center Bottom)** **Inspector Panel (Right)**
- Theory details: parameters, sorts, functions, relations, instance fields, axioms - Theory details: parameters, sorts, functions, relations, instance fields, axioms
- Instance details: elements by sort, function values, relation tuples, nested instances - Instance details: elements by sort, function values, relation tuples, nested instances
- Collapsible sections - Collapsible sections
- "View Graph" button for instances - "View Graph" button for instances
- Fixed-width docked sidebar in the main workspace view
**Console Panel (Bottom)** **Console Panel (Bottom)**
- Scrollable message log - Scrollable message log
@ -103,11 +108,13 @@ src/gui/
- Type `:inspect <name>` to inspect - Type `:inspect <name>` to inspect
- Type `:chase <instance>` to run chase - Type `:chase <instance>` to run chase
- Or type geolog code directly - Or type geolog code directly
- Fixed-height docked footer
**Adjustable Panels** **Layout**
- Browser panel (left): drag right edge to resize - Docked workspace layout for stability
- Console panel (bottom): drag top edge to resize - Browser on the left, editor in the center, inspector on the right
- Editor/Inspector split: drag the separator bar between them - Console fixed at the bottom
- Chase and graph visualizations replace the central workspace when active
**Chase Visualization** **Chase Visualization**
- Step/Run All/Stop controls - Step/Run All/Stop controls
@ -129,22 +136,14 @@ src/gui/
``` ```
┌─────────────────────────────────────────────────────────────┐ ┌─────────────────────────────────────────────────────────────┐
│ File Edit View Chase Help │ │ File Edit View Chase Help │
├────────────┬────────────────────────────────────────────────┤ ├──────────────┬──────────────────────────────┬───────────────┤
│ ▼ Theories │ ┌─────────────────────────────────────────┐ │ │ Browser │ Editor │ Inspector │
│ Preorder │ │ Editor │ │ │ ▼ Theories │ theory Foo { │ Chain3 │
│ Graph │ │ theory Foo { │ │ │ Preorder │ X : Sort; │ : Preorder │
│ ▼ Instances│ │ X : Sort; │ │ │ ▼ Instances │ } [Run] [Clear] │ ▼ Elements │
│ Chain3 │ │ } [Run] [Clear] │ │ │ Chain3 │ │ ▼ Relations │
│ │ ├─────────────────────────────────────────┤ │ │ │ │ [View Graph] │
│ │ │ ═══════════ [drag to resize] ═══════════│ │ ├──────────────┴──────────────────────────────┴───────────────┤
│ │ ├─────────────────────────────────────────┤ │
│ │ │ Inspector: Chain3 : Preorder │ │
│ │ │ ▼ Elements (3) │ │
│ │ │ X: bot, mid, top │ │
│ │ │ ▼ Relations │ │
│ │ │ leq: 6 tuples [View Graph] │ │
│ │ └─────────────────────────────────────────┘ │
├────────────┴────────────────────────────────────────────────┤
│ Console [Clear]│ │ Console [Clear]│
│ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms) │ │ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms) │
│ + Defined instance Chain3 : Preorder (3 elements) │ │ + 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) { fn setup_fonts(ctx: &egui::Context) {
// Use a slightly larger default font // Use a slightly larger default font
let mut style = (*ctx.style()).clone(); let mut style = (*ctx.style()).clone();
style.text_styles.insert( style.animation_time = 0.0;
egui::TextStyle::Body, style
egui::FontId::proportional(14.0), .text_styles
); .insert(egui::TextStyle::Body, egui::FontId::proportional(14.0));
style.text_styles.insert( style
egui::TextStyle::Heading, .text_styles
egui::FontId::proportional(18.0), .insert(egui::TextStyle::Heading, egui::FontId::proportional(18.0));
); style
style.text_styles.insert( .text_styles
egui::TextStyle::Monospace, .insert(egui::TextStyle::Monospace, egui::FontId::monospace(13.0));
egui::FontId::monospace(13.0),
);
// Set up dark theme with custom colors // Force a light theme for the GUI.
style.visuals = egui::Visuals::dark(); style.visuals = egui::Visuals::light();
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;
style.visuals.widgets.active.expansion = 0.0;
style.visuals.widgets.open.expansion = 0.0;
ctx.set_style(style); ctx.set_style(style);
} }

153
src/gui/app.rs
View File

@ -21,9 +21,6 @@ pub struct GeologApp {
console: ConsolePanel, console: ConsolePanel,
chase_viz: ChaseVisualization, chase_viz: ChaseVisualization,
graph_view: GraphView, graph_view: GraphView,
/// Editor/Inspector split ratio (0.0 to 1.0, where 0.5 = equal)
editor_split: f32,
} }
impl GeologApp { impl GeologApp {
@ -37,7 +34,6 @@ impl GeologApp {
console: ConsolePanel::new(), console: ConsolePanel::new(),
chase_viz: ChaseVisualization::new(), chase_viz: ChaseVisualization::new(),
graph_view: GraphView::new(), graph_view: GraphView::new(),
editor_split: 0.5, // 50% editor, 50% inspector
} }
} }
@ -50,21 +46,21 @@ impl GeologApp {
/// Render the menu bar /// Render the menu bar
fn menu_bar(&mut self, ui: &mut egui::Ui) { 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| { ui.menu_button("File", |ui| {
if ui.button("Open...").clicked() { if ui.button("Open...").clicked() {
self.handle_open_file(); self.handle_open_file();
ui.close_menu(); ui.close();
} }
if ui.button("Save").clicked() { if ui.button("Save").clicked() {
self.handle_save_file(); self.handle_save_file();
ui.close_menu(); ui.close();
} }
ui.separator(); ui.separator();
if ui.button("Reset State").clicked() { if ui.button("Reset State").clicked() {
self.state.repl.reset(); self.state.reset_runtime_state();
self.state.log_info("State reset"); self.state.log_info("State reset");
ui.close_menu(); ui.close();
} }
ui.separator(); ui.separator();
if ui.button("Quit").clicked() { if ui.button("Quit").clicked() {
@ -75,11 +71,11 @@ impl GeologApp {
ui.menu_button("Edit", |ui| { ui.menu_button("Edit", |ui| {
if ui.button("Clear Editor").clicked() { if ui.button("Clear Editor").clicked() {
self.state.editor_content.clear(); self.state.editor_content.clear();
ui.close_menu(); ui.close();
} }
if ui.button("Clear Console").clicked() { if ui.button("Clear Console").clicked() {
self.state.clear_console(); self.state.clear_console();
ui.close_menu(); ui.close();
} }
}); });
@ -92,7 +88,7 @@ impl GeologApp {
.clicked() .clicked()
{ {
self.state.central_view = CentralView::EditorAndInspector; self.state.central_view = CentralView::EditorAndInspector;
ui.close_menu(); ui.close();
} }
if ui if ui
.selectable_label( .selectable_label(
@ -102,7 +98,7 @@ impl GeologApp {
.clicked() .clicked()
{ {
self.state.central_view = CentralView::ChaseVisualization; self.state.central_view = CentralView::ChaseVisualization;
ui.close_menu(); ui.close();
} }
if ui if ui
.selectable_label( .selectable_label(
@ -112,7 +108,7 @@ impl GeologApp {
.clicked() .clicked()
{ {
self.state.central_view = CentralView::GraphVisualization; self.state.central_view = CentralView::GraphVisualization;
ui.close_menu(); ui.close();
} }
}); });
@ -123,11 +119,11 @@ impl GeologApp {
let name = name.clone(); let name = name.clone();
if ui.button(format!("Run Chase on {}", name)).clicked() { if ui.button(format!("Run Chase on {}", name)).clicked() {
self.handle_run_chase(&name); self.handle_run_chase(&name);
ui.close_menu(); ui.close();
} }
if ui.button(format!("Debug Chase on {}", name)).clicked() { if ui.button(format!("Debug Chase on {}", name)).clicked() {
self.state.start_chase(&name); self.state.start_chase(&name);
ui.close_menu(); ui.close();
} }
} else { } else {
ui.label("(Select an instance first)"); ui.label("(Select an instance first)");
@ -136,15 +132,13 @@ impl GeologApp {
ui.menu_button("Help", |ui| { ui.menu_button("Help", |ui| {
if ui.button("About").clicked() { if ui.button("About").clicked() {
self.state.log_info(format!( self.state
"Geolog GUI v{}", .log_info(format!("Geolog GUI v{}", env!("CARGO_PKG_VERSION")));
env!("CARGO_PKG_VERSION") ui.close();
));
ui.close_menu();
} }
if ui.button("Syntax Help").clicked() { if ui.button("Syntax Help").clicked() {
self.show_syntax_help(); self.show_syntax_help();
ui.close_menu(); ui.close();
} }
}); });
}); });
@ -152,7 +146,7 @@ impl GeologApp {
/// Handle opening a file /// Handle opening a file
fn handle_open_file(&mut self) { 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("Geolog", &["geolog"])
.add_filter("All Files", &["*"]) .add_filter("All Files", &["*"])
.pick_file() .pick_file()
@ -174,7 +168,7 @@ impl GeologApp {
} }
} else { } else {
// Save As // Save As
if let Some(path) = rfd::FileDialog::new() if let Some(path) = Self::new_file_dialog()
.add_filter("Geolog", &["geolog"]) .add_filter("Geolog", &["geolog"])
.save_file() .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 /// Run chase on an instance
fn handle_run_chase(&mut self, instance_name: &str) { fn handle_run_chase(&mut self, instance_name: &str) {
use crate::core::RelationStorage; use crate::core::RelationStorage;
@ -246,8 +248,7 @@ impl GeologApp {
Ok(iterations) => { Ok(iterations) => {
let elapsed = start.elapsed(); let elapsed = start.elapsed();
// Get structure info before releasing borrow // Get structure info before releasing borrow
let total_tuples: usize = let total_tuples: usize = entry.structure.relations.iter().map(|r| r.len()).sum();
entry.structure.relations.iter().map(|r| r.len()).sum();
let num_elements = entry.structure.len(); let num_elements = entry.structure.len();
self.state.log_success(format!( self.state.log_success(format!(
@ -259,8 +260,7 @@ impl GeologApp {
// Show structure summary // Show structure summary
self.state.log_info(format!( self.state.log_info(format!(
"Structure: {} elements, {} relation tuples", "Structure: {} elements, {} relation tuples",
num_elements, num_elements, total_tuples
total_tuples
)); ));
} }
Err(e) => { Err(e) => {
@ -290,80 +290,7 @@ impl GeologApp {
fn central_panel(&mut self, ui: &mut egui::Ui) { fn central_panel(&mut self, ui: &mut egui::Ui) {
match self.state.central_view { match self.state.central_view {
CentralView::EditorAndInspector => { CentralView::EditorAndInspector => {
// Split vertically: editor on top, inspector on bottom self.editor.show(ui, &mut self.state);
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);
},
);
} }
CentralView::ChaseVisualization => { CentralView::ChaseVisualization => {
self.chase_viz.show(ui, &mut self.state); self.chase_viz.show(ui, &mut self.state);
@ -384,18 +311,28 @@ impl eframe::App for GeologApp {
// Left panel: Browser // Left panel: Browser
egui::SidePanel::left("browser_panel") egui::SidePanel::left("browser_panel")
.default_width(200.0) .default_width(240.0)
.min_width(150.0) .min_width(240.0)
.resizable(true) .resizable(false)
.show(ctx, |ui| { .show(ctx, |ui| {
self.browser.show(ui, &mut self.state); 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 // Bottom panel: Console
egui::TopBottomPanel::bottom("console_panel") egui::TopBottomPanel::bottom("console_panel")
.default_height(150.0) .default_height(200.0)
.min_height(100.0) .min_height(200.0)
.resizable(true) .resizable(false)
.show(ctx, |ui| { .show(ctx, |ui| {
self.console.show(ui, &mut self.state); 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() { if ui.button("Inspect").clicked() {
state.selected_item = state.selected_item =
Some(SelectedItem::Instance(instance.name.clone())); Some(SelectedItem::Instance(instance.name.clone()));
ui.close_menu(); ui.close();
} }
if ui.button("Run Chase").clicked() { if ui.button("Run Chase").clicked() {
// This will be handled by the app // This will be handled by the app
@ -157,11 +157,11 @@ impl BrowserPanel {
"Use Chase menu to run chase on '{}'", "Use Chase menu to run chase on '{}'",
instance.name instance.name
)); ));
ui.close_menu(); ui.close();
} }
if ui.button("View Graph").clicked() { if ui.button("View Graph").clicked() {
state.show_graph(&instance.name, None); 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. //! Shows a scrollable log of messages with color coding and a REPL input.
use eframe::egui; use eframe::egui;
use egui_extras::{Size, StripBuilder};
use crate::gui::state::{GuiState, MessageKind}; 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 /// Console panel for output messages and REPL input
pub struct ConsolePanel { pub struct ConsolePanel {
@ -30,101 +31,122 @@ impl ConsolePanel {
} }
pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) { pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
// Header with title and buttons StripBuilder::new(ui)
ui.horizontal(|ui| { .size(Size::exact(28.0))
ui.heading("Console"); .size(Size::remainder().at_least(80.0))
.size(Size::exact(28.0))
ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| { .vertical(|mut strip| {
if ui.button("Clear").clicked() { strip.cell(|ui| {
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 => "?",
};
ui.horizontal(|ui| { ui.horizontal(|ui| {
ui.label( ui.heading("Console");
egui::RichText::new(prefix)
.color(color) ui.with_layout(egui::Layout::right_to_left(egui::Align::Center), |ui| {
.monospace(), if ui
); .add_sized([64.0, 22.0], egui::Button::new("Clear"))
ui.label( .clicked()
egui::RichText::new(&message.text) {
.color(color) state.clear_console();
.monospace(), }
);
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 strip.cell(|ui| {
ui.separator(); egui::Frame::default()
ui.horizontal(|ui| { .inner_margin(egui::Margin::same(4))
ui.label( .show(ui, |ui| {
egui::RichText::new("geolog>") egui::ScrollArea::vertical()
.monospace() .auto_shrink([false, false])
.color(egui::Color32::from_rgb(100, 150, 255)), .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( let prefix = match message.kind {
egui::TextEdit::singleline(&mut self.input) MessageKind::Info => ">",
.font(egui::FontId::monospace(13.0)) MessageKind::Success => "+",
.desired_width((ui.available_width() - 60.0).max(50.0)) MessageKind::Error => "!",
.hint_text(":help for commands"), MessageKind::Warning => "?",
); };
// Handle Enter key ui.horizontal(|ui| {
if response.lost_focus() && ui.input(|i| i.key_pressed(egui::Key::Enter)) { ui.add_sized(
self.execute_input(state); [12.0, 18.0],
response.request_focus(); 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 strip.cell(|ui| {
if response.has_focus() { ui.horizontal(|ui| {
if ui.input(|i| i.key_pressed(egui::Key::ArrowUp)) { ui.add_sized(
self.history_up(); [68.0, 22.0],
} egui::Label::new(
if ui.input(|i| i.key_pressed(egui::Key::ArrowDown)) { egui::RichText::new("geolog>")
self.history_down(); .monospace()
} .color(ui.visuals().hyperlink_color),
} ),
);
if ui.button("Run").clicked() { let run_width = 56.0;
self.execute_input(state); 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) { 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) { fn handle_meta_command(&mut self, state: &mut GuiState, cmd: MetaCommand) {
match cmd { match cmd {
MetaCommand::Help(topic) => { MetaCommand::Help(topic) => match topic.as_deref() {
match topic.as_deref() { None => {
None => { state.log_info("Commands:");
state.log_info("Commands:"); state.log_info(" :help Show this help");
state.log_info(" :help Show this help"); state.log_info(" :list List theories and instances");
state.log_info(" :list List theories and instances"); state.log_info(" :inspect <n> Inspect a theory or instance");
state.log_info(" :inspect <n> Inspect a theory or instance"); state.log_info(" :chase <inst> Run chase on instance");
state.log_info(" :chase <inst> Run chase on instance"); state.log_info(" :reset Reset all state");
state.log_info(" :reset Reset all state"); state.log_info(" :clear Clear console");
state.log_info(" :clear Clear console"); state.log_info("");
state.log_info(""); state.log_info("Or type geolog code directly.");
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) => { MetaCommand::List(target) => {
match target { match target {
ListTarget::Theories | ListTarget::All => { ListTarget::Theories | ListTarget::All => {
@ -259,7 +279,7 @@ impl ConsolePanel {
} }
} }
MetaCommand::Inspect(name) => { 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) { match state.repl.inspect(&name) {
Some(InspectResult::Theory(detail)) => { Some(InspectResult::Theory(detail)) => {
for line in format_theory_detail(&detail).lines() { for line in format_theory_detail(&detail).lines() {
@ -280,26 +300,26 @@ impl ConsolePanel {
state.clear_console(); state.clear_console();
} }
MetaCommand::Reset => { MetaCommand::Reset => {
state.repl.reset(); state.reset_runtime_state();
state.selected_item = None;
state.log_success("State reset."); state.log_success("State reset.");
} }
MetaCommand::Chase { instance, max_iterations } => { MetaCommand::Chase {
instance,
max_iterations,
} => {
self.run_chase(state, &instance, max_iterations); self.run_chase(state, &instance, max_iterations);
} }
MetaCommand::Source(path) => { MetaCommand::Source(path) => match std::fs::read_to_string(&path) {
match std::fs::read_to_string(&path) { Ok(content) => {
Ok(content) => { state.editor_content = content;
state.editor_content = content; state.current_file = Some(path.clone());
state.current_file = Some(path.clone()); state.log_info(format!("Loaded: {}", path.display()));
state.log_info(format!("Loaded: {}", path.display())); state.execute_editor();
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"); state.log_warning("Command not yet implemented in GUI");
} }
@ -334,7 +354,11 @@ impl ConsolePanel {
return; 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 entry = state.repl.instances.get_mut(instance_name).unwrap();
let max_iter = max_iterations.unwrap_or(100); let max_iter = max_iterations.unwrap_or(100);
@ -362,8 +386,7 @@ impl ConsolePanel {
)); ));
state.log_info(format!( state.log_info(format!(
"Structure: {} elements, {} relation tuples", "Structure: {} elements, {} relation tuples",
num_elements, num_elements, total_tuples
total_tuples
)); ));
} }
Err(e) => { 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 { impl Default for ConsolePanel {
fn default() -> Self { fn default() -> Self {
Self::new() Self::new()

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

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

52
src/gui/state.rs
View File

@ -5,6 +5,7 @@
use std::collections::HashSet; use std::collections::HashSet;
use std::path::PathBuf; use std::path::PathBuf;
use crate::core::Structure;
use crate::repl::{InstanceDetail, ReplState, TheoryDetail}; use crate::repl::{InstanceDetail, ReplState, TheoryDetail};
/// What item is currently selected in the browser /// What item is currently selected in the browser
@ -57,6 +58,7 @@ pub enum ChaseMode {
pub struct ChaseVisualizationState { pub struct ChaseVisualizationState {
pub mode: ChaseMode, pub mode: ChaseMode,
pub instance_name: String, pub instance_name: String,
pub initial_structure: Structure,
pub events: Vec<ChaseEventRecord>, pub events: Vec<ChaseEventRecord>,
pub current_event: usize, pub current_event: usize,
pub current_iteration: usize, pub current_iteration: usize,
@ -65,10 +67,11 @@ pub struct ChaseVisualizationState {
} }
impl ChaseVisualizationState { impl ChaseVisualizationState {
pub fn new(instance_name: String) -> Self { pub fn new(instance_name: String, initial_structure: Structure) -> Self {
Self { Self {
mode: ChaseMode::Idle, mode: ChaseMode::Idle,
instance_name, instance_name,
initial_structure,
events: Vec::new(), events: Vec::new(),
current_event: 0, current_event: 0,
current_iteration: 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 /// Add an info message to the console
pub fn log_info(&mut self, text: impl Into<String>) { pub fn log_info(&mut self, text: impl Into<String>) {
self.console_messages.push(ConsoleMessage { self.console_messages.push(ConsoleMessage {
@ -308,7 +321,15 @@ impl GuiState {
/// Start a chase visualization for an instance /// Start a chase visualization for an instance
pub fn start_chase(&mut self, instance_name: &str) { 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; self.central_view = CentralView::ChaseVisualization;
} }
@ -319,3 +340,30 @@ impl GuiState {
self.central_view = CentralView::GraphVisualization; 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. //! Provides step-through debugging and visualization of the chase algorithm.
use eframe::egui; use eframe::egui;
use std::collections::HashSet;
use crate::core::RelationStorage; 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}; use crate::query::chase::{ChaseControl, ChaseEvent, ChaseObserver};
/// Chase visualization panel /// Chase visualization panel
@ -49,7 +52,10 @@ impl ChaseVisualization {
ui.label("No instances defined. Create an instance first."); ui.label("No instances defined. Create an instance first.");
} else { } else {
for instance in instances { 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); state.start_chase(&instance.name);
} }
} }
@ -59,7 +65,10 @@ impl ChaseVisualization {
if let Some(SelectedItem::Instance(name)) = &state.selected_item { if let Some(SelectedItem::Instance(name)) = &state.selected_item {
ui.add_space(16.0); ui.add_space(16.0);
let name = name.clone(); 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); state.start_chase(&name);
} }
} }
@ -67,9 +76,9 @@ impl ChaseVisualization {
fn show_chase_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) { fn show_chase_panel(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
// Read mode and instance_name before mutable operations // Read mode and instance_name before mutable operations
let (mode, instance_name) = { let mode = {
let chase_state = state.chase_state.as_ref().unwrap(); let chase_state = state.chase_state.as_ref().unwrap();
(chase_state.mode, chase_state.instance_name.clone()) chase_state.mode
}; };
// Control buttons // Control buttons
@ -130,7 +139,7 @@ impl ChaseVisualization {
} }
} }
if reset_clicked { if reset_clicked {
state.chase_state = Some(ChaseVisualizationState::new(instance_name)); self.reset_chase(state);
} }
if close_clicked { if close_clicked {
state.chase_state = None; state.chase_state = None;
@ -185,11 +194,11 @@ impl ChaseVisualization {
); );
let color = if is_current { let color = if is_current {
egui::Color32::YELLOW ui.visuals().hyperlink_color
} else if event.changed { } else if event.changed {
egui::Color32::from_rgb(100, 200, 100) egui::Color32::from_rgb(25, 110, 55)
} else { } else {
egui::Color32::LIGHT_GRAY ui.visuals().weak_text_color()
}; };
ui.label(egui::RichText::new(text).color(color).monospace()); 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 /// Execute a single step of the chase
fn step_chase(&mut self, state: &mut GuiState) { fn step_chase(&mut self, state: &mut GuiState) {
let instance_name = match &state.chase_state { let instance_name = match &state.chase_state {
Some(s) => s.instance_name.clone(), Some(s) => s.instance_name.clone(),
None => return, None => return,
}; };
let breakpoints = state
let current_iteration = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0); .chase_state
.as_ref()
.map(|s| s.breakpoints.clone())
.unwrap_or_default();
// Get theory name first (immutable borrow) // Get theory name first (immutable borrow)
let theory_name = match state.repl.instances.get(&instance_name) { 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(); let entry = state.repl.instances.get_mut(&instance_name).unwrap();
// Create a GUI observer that records events // Create a GUI observer that records events
let mut observer = GuiChaseObserver { let mut observer = GuiChaseObserver::new(&entry.slid_to_name, Some(1), breakpoints);
events: Vec::new(),
slid_to_name: &entry.slid_to_name,
iteration: current_iteration,
step_mode: true,
steps_remaining: 1,
};
// Run chase with observer (just one step) // Run chase with observer (just one step)
let sig = &theory.theory.signature; let sig = &theory.theory.signature;
@ -332,33 +361,43 @@ impl ChaseVisualization {
&mut entry.structure, &mut entry.structure,
&mut state.repl.store.universe, &mut state.repl.store.universe,
sig, sig,
1, // Just one iteration 100,
&mut observer, &mut observer,
); );
// Record events let GuiChaseObserver {
let events = observer.events; events,
iteration: current_iteration,
breakpoint_hit: paused_on_breakpoint,
completed_iterations,
..
} = observer;
if let Some(chase_state) = &mut state.chase_state { if let Some(chase_state) = &mut state.chase_state {
chase_state.mode = ChaseMode::Stepping; chase_state.mode = ChaseMode::Stepping;
for event in events { chase_state.events.extend(events);
chase_state.events.push(event); 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 = chase_state.current_iteration.max(current_iteration);
chase_state.current_iteration += 1;
if let Ok(iterations) = result { if let Some(iterations) = completed_iterations {
if iterations == 0 { chase_state.mode = ChaseMode::Completed;
chase_state.mode = ChaseMode::Completed; chase_state.current_iteration = iterations;
chase_state.total_iterations = Some(chase_state.current_iteration); chase_state.total_iterations = Some(iterations);
}
} }
} }
// Log completion separately match result {
if let Ok(iterations) = result { Ok(_) => {
if iterations == 0 { if let Some(bp) = paused_on_breakpoint {
let total = state.chase_state.as_ref().map(|s| s.current_iteration).unwrap_or(0); state.log_info(format!("Paused at breakpoint '{}'", bp));
state.log_success(format!("Chase completed after {} iterations", total)); }
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 // Now get mutable access to entry
let entry = state.repl.instances.get_mut(&instance_name).unwrap(); let entry = state.repl.instances.get_mut(&instance_name).unwrap();
// Run chase to fixpoint // Run chase to fixpoint
let sig = &theory.theory.signature; let sig = &theory.theory.signature;
let axioms = &theory.theory.axioms; let axioms = &theory.theory.axioms;
let axiom_names = &theory.theory.axiom_names;
let start = std::time::Instant::now(); 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, axioms,
axiom_names,
&mut entry.structure, &mut entry.structure,
&mut state.repl.store.universe, &mut state.repl.store.universe,
sig, sig,
100, 100,
&mut observer,
); );
let GuiChaseObserver {
events,
iteration: current_iteration,
breakpoint_hit,
completed_iterations,
..
} = observer;
match result { match result {
Ok(iterations) => { Ok(_) => {
let elapsed = start.elapsed(); let elapsed = start.elapsed();
if let Some(chase_state) = &mut state.chase_state { if let Some(chase_state) = &mut state.chase_state {
chase_state.mode = ChaseMode::Completed; chase_state.events.extend(events);
chase_state.total_iterations = Some(iterations); 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) => { Err(e) => {
state.log_error(format!("Chase error: {}", e)); state.log_error(format!("Chase error: {}", e));
@ -434,8 +509,30 @@ struct GuiChaseObserver<'a> {
events: Vec<ChaseEventRecord>, events: Vec<ChaseEventRecord>,
slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>, slid_to_name: &'a std::collections::HashMap<crate::id::Slid, String>,
iteration: usize, iteration: usize,
step_mode: bool, step_budget: Option<usize>,
steps_remaining: 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> { impl<'a> ChaseObserver for GuiChaseObserver<'a> {
@ -471,27 +568,189 @@ impl<'a> ChaseObserver for GuiChaseObserver<'a> {
binding: binding_vec, binding: binding_vec,
changed: false, // Will be updated in AxiomFired changed: false, // Will be updated in AxiomFired
}); });
self.pending_breakpoint_hit = axiom_name
if self.step_mode { .filter(|name| self.breakpoints.iter().any(|bp| name.contains(bp)))
self.steps_remaining = self.steps_remaining.saturating_sub(1); .map(str::to_string);
if self.steps_remaining == 0 { ChaseControl::Continue
ChaseControl::Stop
} else {
ChaseControl::Continue
}
} else {
ChaseControl::Continue
}
} }
ChaseEvent::AxiomFired { changed, .. } => { ChaseEvent::AxiomFired {
axiom_name,
changed,
..
} => {
// Update the last event with the changed status // Update the last event with the changed status
if let Some(last) = self.events.last_mut() { if let Some(last) = self.events.last_mut() {
last.changed = changed; 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::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(); ui.separator();
// Check if we need to rebuild the graph // 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); self.rebuild_graph(state);
} }
@ -109,21 +110,23 @@ impl GraphView {
ui.label("Relation:"); ui.label("Relation:");
egui::ComboBox::from_label("") egui::ComboBox::from_label("")
.selected_text( .selected_text(self.selected_relation.as_deref().unwrap_or("(all)"))
self.selected_relation
.as_deref()
.unwrap_or("(all)"),
)
.show_ui(ui, |ui| { .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.selected_relation = None;
self.needs_layout = true; self.needs_layout = true;
} }
for rel in relations { for rel in relations {
if ui.selectable_label( if ui
self.selected_relation.as_deref() == Some(rel), .selectable_label(
rel, self.selected_relation.as_deref() == Some(rel),
).clicked() { rel,
)
.clicked()
{
self.selected_relation = Some(rel.to_string()); self.selected_relation = Some(rel.to_string());
self.needs_layout = true; self.needs_layout = true;
} }
@ -183,7 +186,10 @@ impl GraphView {
ui.label("No instances defined."); ui.label("No instances defined.");
} else { } else {
for instance in instances { 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()); state.graph_instance = Some(instance.name.clone());
self.needs_layout = true; self.needs_layout = true;
} }
@ -230,7 +236,10 @@ impl GraphView {
.unwrap_or_else(|| format!("#{}", slid_idx)); .unwrap_or_else(|| format!("#{}", slid_idx));
let sort_name = sig.sorts.get(sort_id).cloned().unwrap_or_default(); 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 { self.nodes.push(GraphNode {
id: slid, id: slid,
@ -326,7 +335,11 @@ impl GraphView {
let mut max_y = f32::MIN; let mut max_y = f32::MIN;
for node in &self.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);
min_x = min_x.min(pos.x); min_x = min_x.min(pos.x);
min_y = min_y.min(pos.y); min_y = min_y.min(pos.y);
max_x = max_x.max(pos.x); 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) // 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_x = (min_x + max_x) / 2.0;
let world_center_y = (min_y + max_y) / 2.0; let world_center_y = (min_y + max_y) / 2.0;
self.pan = egui::Vec2::new( self.pan = egui::Vec2::new(-world_center_x * self.zoom, -world_center_y * self.zoom);
-world_center_x * self.zoom,
-world_center_y * self.zoom,
);
} }
fn draw_graph(&mut self, ui: &mut egui::Ui) { fn draw_graph(&mut self, ui: &mut egui::Ui) {
let (response, painter) = ui.allocate_painter( let (response, painter) =
ui.available_size(), ui.allocate_painter(ui.available_size(), egui::Sense::click_and_drag());
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 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 // Handle panning
if response.dragged() && self.dragged_node.is_none() { if response.dragged() && self.dragged_node.is_none() {
self.pan += response.drag_delta(); self.pan += pointer_delta;
} }
// Handle zooming with scroll // 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 { let transform = |pos: egui::Pos2| -> egui::Pos2 {
egui::Pos2::new( egui::Pos2::new(
center.x + pos.x * self.zoom + self.pan.x, center.x + pos.x * self.zoom + self.pan.x,
@ -406,14 +452,12 @@ impl GraphView {
painter.circle_stroke( painter.circle_stroke(
loop_center, loop_center,
10.0 * self.zoom, 10.0 * self.zoom,
egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY), egui::Stroke::new(1.5, edge_color),
); );
} else { } else {
// Regular edge // Regular edge
painter.line_segment( painter
[from_screen, to_screen], .line_segment([from_screen, to_screen], egui::Stroke::new(1.5, edge_color));
egui::Stroke::new(1.5, egui::Color32::LIGHT_GRAY),
);
// Draw arrowhead // Draw arrowhead
let dir = (to_screen - from_screen).normalized(); let dir = (to_screen - from_screen).normalized();
@ -428,7 +472,7 @@ impl GraphView {
painter.add(egui::Shape::convex_polygon( painter.add(egui::Shape::convex_polygon(
vec![p1, p2, p3], vec![p1, p2, p3],
egui::Color32::LIGHT_GRAY, edge_color,
egui::Stroke::NONE, egui::Stroke::NONE,
)); ));
} }
@ -436,31 +480,18 @@ impl GraphView {
} }
// Draw nodes // Draw nodes
let node_radius = 20.0 * self.zoom;
for node in &self.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 screen_pos = transform(pos);
let is_hovered = hovered_node == Some(node.id);
// 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);
}
if self.dragged_node == Some(node.id) { if self.dragged_node == Some(node.id) {
if response.dragged() { 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) { if let Some(pos) = self.node_positions.get_mut(&node.id) {
*pos += delta; *pos += delta;
} }
@ -481,7 +512,7 @@ impl GraphView {
painter.circle_stroke( painter.circle_stroke(
screen_pos, screen_pos,
node_radius, node_radius,
egui::Stroke::new(2.0, egui::Color32::WHITE), egui::Stroke::new(2.0, border_color),
); );
// Draw node label // Draw node label
@ -491,7 +522,7 @@ impl GraphView {
egui::Align2::CENTER_CENTER, egui::Align2::CENTER_CENTER,
&node.name, &node.name,
egui::FontId::proportional(font_size), egui::FontId::proportional(font_size),
egui::Color32::WHITE, text_color_for_fill(fill_color),
); );
// Draw sort label below // Draw sort label below
@ -501,7 +532,7 @@ impl GraphView {
egui::Align2::CENTER_TOP, egui::Align2::CENTER_TOP,
&node.sort, &node.sort,
egui::FontId::proportional(10.0 * self.zoom), egui::FontId::proportional(10.0 * self.zoom),
egui::Color32::LIGHT_GRAY, hint_color,
); );
} }
} }
@ -513,7 +544,7 @@ impl GraphView {
egui::Align2::CENTER_CENTER, egui::Align2::CENTER_CENTER,
"No elements to display", "No elements to display",
egui::FontId::proportional(16.0), egui::FontId::proportional(16.0),
egui::Color32::GRAY, hint_color,
); );
} }
} }
@ -538,6 +569,16 @@ fn generate_sort_colors(count: usize) -> Vec<egui::Color32> {
colors 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 /// Convert HSV to RGB
fn hsv_to_rgb(h: f32, s: f32, v: f32) -> (u8, u8, u8) { fn hsv_to_rgb(h: f32, s: f32, v: f32) -> (u8, u8, u8) {
let c = v * s; let c = v * s;