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

WIP

Browse Source
This commit is contained in:
Hassan Abedi 2026-03-20 12:07:53 +01:00
parent 9ec827c607
commit bd9b1cc11d
9 changed files with 956 additions and 855 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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]]

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

@ -113,6 +113,7 @@ 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.animation_time = 0.0;
style.text_styles.insert(
egui::TextStyle::Body,
egui::FontId::proportional(14.0),
@ -129,6 +130,11 @@ fn setup_fonts(ctx: &egui::Context) {
// Set up dark theme with custom colors
style.visuals = egui::Visuals::dark();
style.visuals.override_text_color = Some(egui::Color32::from_gray(220));
style.visuals.widgets.noninteractive.expansion = 0.0;
style.visuals.widgets.inactive.expansion = 0.0;
style.visuals.widgets.hovered.expansion = 0.0;
style.visuals.widgets.active.expansion = 0.0;
style.visuals.widgets.open.expansion = 0.0;
ctx.set_style(style);
}

101
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
}
}
@ -290,80 +286,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 +307,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);
});

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

@ -3,6 +3,7 @@
//! 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};
@ -30,101 +31,127 @@ 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 = 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 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(egui::Color32::from_rgb(100, 150, 255)),
),
);
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) {

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();
}
}
});
}
}
}

15
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,
@ -308,7 +311,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;
}

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

@ -3,6 +3,7 @@
//! 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};
@ -67,9 +68,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 +131,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;
@ -283,14 +284,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 +340,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 +353,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 +418,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 +501,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 +560,176 @@ 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);
}
}

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

@ -359,10 +359,45 @@ impl GraphView {
);
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 +416,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,
@ -436,31 +469,14 @@ 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 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;
}