diff --git a/README2.md b/README2.md index 2712125..70d54a4 100644 --- a/README2.md +++ b/README2.md @@ -97,6 +97,17 @@ src/gui/ - Color-coded messages: info (gray), success (green), error (red), warning (orange) - Auto-scroll option - Clear button +- **Integrated REPL input** with command history (Up/Down arrows) + - Type `:help` for commands + - Type `:list` to list theories/instances + - Type `:inspect ` to inspect + - Type `:chase ` to run chase + - Or type geolog code directly + +**Adjustable Panels** +- Browser panel (left): drag right edge to resize +- Console panel (bottom): drag top edge to resize +- Editor/Inspector split: drag the separator bar between them **Chase Visualization** - Step/Run All/Stop controls @@ -124,8 +135,9 @@ src/gui/ │ Graph │ │ theory Foo { │ │ │ ▼ Instances│ │ X : Sort; │ │ │ Chain3 │ │ } [Run] [Clear] │ │ -│ │ └─────────────────────────────────────────┘ │ -│ │ ┌─────────────────────────────────────────┐ │ +│ │ ├─────────────────────────────────────────┤ │ +│ │ │ ═══════════ [drag to resize] ═══════════│ │ +│ │ ├─────────────────────────────────────────┤ │ │ │ │ Inspector: Chain3 : Preorder │ │ │ │ │ ▼ Elements (3) │ │ │ │ │ X: bot, mid, top │ │ @@ -136,6 +148,8 @@ src/gui/ │ Console [Clear]│ │ > Defined theory Preorder (1 sorts, 1 relations, 2 axioms) │ │ + Defined instance Chain3 : Preorder (3 elements) │ +│─────────────────────────────────────────────────────────────│ +│ geolog> :list [Run] │ └─────────────────────────────────────────────────────────────┘ ``` @@ -210,27 +224,38 @@ cargo run -- --help // Define a preorder theory theory Preorder { X : Sort; - leq : [a: X, b: X] -> Prop; - // Reflexivity - forall x : X. |- [a: x, b: x] leq; + // The ordering relation: x <= y + leq : [x: X, y: X] -> Prop; - // Transitivity - forall x : X, y : X, z : X. - [a: x, b: y] leq, [a: y, b: z] leq |- [a: x, b: z] leq; + // Reflexivity: x <= x + ax/refl : forall x : X. + |- [x: x, y: x] leq; + + // Transitivity: x <= y and y <= z implies x <= z + ax/trans : forall x : X, y : X, z : X. + [x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq; } -// Define an instance -instance Chain3 : Preorder = { +// Define an instance with automatic chase +// The 'chase' keyword applies axioms to compute the closure +instance Chain3 : Preorder = chase { bot : X; mid : X; top : X; - [a: bot, b: mid] leq; - [a: mid, b: top] leq; + + // Assert the basic ordering; chase derives reflexive pairs + // and transitive closure (bot <= top) + [x: bot, y: mid] leq; + [x: mid, y: top] leq; } ``` -Then run `:chase Chain3` to compute the transitive closure. +After loading this file, the chase algorithm automatically computes: +- Reflexive pairs: `bot <= bot`, `mid <= mid`, `top <= top` +- Transitive closure: `bot <= top` + +You can also define an instance without `chase` and run `:chase Chain3` manually. ## Development diff --git a/src/gui/app.rs b/src/gui/app.rs index ee62911..dc9e1e1 100644 --- a/src/gui/app.rs +++ b/src/gui/app.rs @@ -21,6 +21,9 @@ 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 { @@ -34,6 +37,7 @@ impl GeologApp { console: ConsolePanel::new(), chase_viz: ChaseVisualization::new(), graph_view: GraphView::new(), + editor_split: 0.5, // 50% editor, 50% inspector } } @@ -288,7 +292,11 @@ impl GeologApp { CentralView::EditorAndInspector => { // Split vertically: editor on top, inspector on bottom let available_height = ui.available_height(); - let editor_height = available_height * 0.5; + 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( @@ -299,10 +307,63 @@ impl GeologApp { }, ); - ui.separator(); + // 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 - self.inspector.show(ui, &mut self.state); + 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 => { self.chase_viz.show(ui, &mut self.state); diff --git a/src/gui/panels/browser.rs b/src/gui/panels/browser.rs index 40f4d04..7180e19 100644 --- a/src/gui/panels/browser.rs +++ b/src/gui/panels/browser.rs @@ -56,10 +56,9 @@ impl BrowserPanel { format!("Theories ({}/{})", filtered.len(), theories.len()) }; - egui::CollapsingHeader::new(header) + let response = egui::CollapsingHeader::new(header) .default_open(state.theories_expanded) .show(ui, |ui| { - state.theories_expanded = true; if filtered.is_empty() { ui.label("(none)"); } else { @@ -96,6 +95,7 @@ impl BrowserPanel { } } }); + state.theories_expanded = response.fully_open(); } fn show_instances_section(&mut self, ui: &mut egui::Ui, state: &mut GuiState) { @@ -117,10 +117,9 @@ impl BrowserPanel { format!("Instances ({}/{})", filtered.len(), instances.len()) }; - egui::CollapsingHeader::new(header) + let response = egui::CollapsingHeader::new(header) .default_open(state.instances_expanded) .show(ui, |ui| { - state.instances_expanded = true; if filtered.is_empty() { ui.label("(none)"); } else { @@ -168,6 +167,7 @@ impl BrowserPanel { } } }); + state.instances_expanded = response.fully_open(); } } diff --git a/src/gui/panels/console.rs b/src/gui/panels/console.rs index 5a410bf..d16b69d 100644 --- a/src/gui/panels/console.rs +++ b/src/gui/panels/console.rs @@ -1,20 +1,32 @@ //! Console panel for displaying output and error messages //! -//! Shows a scrollable log of messages with color coding. +//! Shows a scrollable log of messages with color coding and a REPL input. use eframe::egui; use crate::gui::state::{GuiState, MessageKind}; +use crate::repl::{MetaCommand, ListTarget, ExecuteResult}; -/// Console panel for output messages +/// Console panel for output messages and REPL input pub struct ConsolePanel { /// Whether to auto-scroll to bottom auto_scroll: bool, + /// REPL input buffer + input: String, + /// Command history + history: Vec, + /// Current position in history (for up/down navigation) + history_pos: Option, } impl ConsolePanel { pub fn new() -> Self { - Self { auto_scroll: true } + Self { + auto_scroll: true, + input: String::new(), + history: Vec::new(), + history_pos: None, + } } pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) { @@ -35,14 +47,16 @@ impl ConsolePanel { ui.separator(); - // Scrollable message area + // 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("(no messages)"); + ui.label("Type commands below (e.g., :help, :list, or geolog code)"); } else { for message in &state.console_messages { let color = match message.kind { @@ -74,6 +88,320 @@ impl ConsolePanel { } } }); + + // 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)), + ); + + 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"), + ); + + // Handle Enter key + if response.lost_focus() && ui.input(|i| i.key_pressed(egui::Key::Enter)) { + self.execute_input(state); + response.request_focus(); + } + + // 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(); + } + } + + if ui.button("Run").clicked() { + self.execute_input(state); + } + }); + } + + fn execute_input(&mut self, state: &mut GuiState) { + let input = self.input.trim().to_string(); + if input.is_empty() { + return; + } + + // Add to history + self.history.push(input.clone()); + self.history_pos = None; + + // Echo the input + state.log_info(format!("geolog> {}", input)); + + // Process the input + if input.starts_with(':') { + // Meta command + let cmd = MetaCommand::parse(&input); + self.handle_meta_command(state, cmd); + } else { + // Geolog code + match state.repl.execute_geolog(&input) { + Ok(results) => { + for result in results { + match result { + ExecuteResult::Namespace(name) => { + state.log_info(format!("Namespace: {}", name)); + } + ExecuteResult::Theory { + name, + num_sorts, + num_functions, + num_relations, + num_axioms, + } => { + let mut parts = vec![format!("{} sorts", num_sorts)]; + if num_functions > 0 { + parts.push(format!("{} functions", num_functions)); + } + if num_relations > 0 { + parts.push(format!("{} relations", num_relations)); + } + if num_axioms > 0 { + parts.push(format!("{} axioms", num_axioms)); + } + state.log_success(format!( + "Defined theory {} ({})", + name, + parts.join(", ") + )); + } + ExecuteResult::Instance { + name, + theory_name, + num_elements, + } => { + state.log_success(format!( + "Defined instance {} : {} ({} elements)", + name, theory_name, num_elements + )); + } + ExecuteResult::Query(_) => { + state.log_info("Query executed"); + } + } + } + } + Err(e) => { + state.log_error(e); + } + } + } + + self.input.clear(); + } + + fn handle_meta_command(&mut self, state: &mut GuiState, cmd: MetaCommand) { + match cmd { + MetaCommand::Help(topic) => { + match topic.as_deref() { + None => { + state.log_info("Commands:"); + state.log_info(" :help Show this help"); + state.log_info(" :list List theories and instances"); + state.log_info(" :inspect Inspect a theory or instance"); + state.log_info(" :chase Run chase on instance"); + state.log_info(" :reset Reset all state"); + state.log_info(" :clear Clear console"); + state.log_info(""); + state.log_info("Or type geolog code directly."); + } + Some(t) => { + state.log_info(format!("Help topic: {}", t)); + } + } + } + MetaCommand::List(target) => { + match target { + ListTarget::Theories | ListTarget::All => { + let theories = state.repl.list_theories(); + if theories.is_empty() { + state.log_info("No theories defined."); + } else { + state.log_info("Theories:"); + for t in theories { + state.log_info(format!( + " {} ({} sorts, {} rels, {} axioms)", + t.name, t.num_sorts, t.num_relations, t.num_axioms + )); + } + } + } + ListTarget::Instances => {} + } + match target { + ListTarget::Instances | ListTarget::All => { + let instances = state.repl.list_instances(); + if instances.is_empty() { + state.log_info("No instances defined."); + } else { + state.log_info("Instances:"); + for i in instances { + state.log_info(format!( + " {} : {} ({} elements)", + i.name, i.theory_name, i.num_elements + )); + } + } + } + ListTarget::Theories => {} + } + } + MetaCommand::Inspect(name) => { + use crate::repl::{InspectResult, format_theory_detail, format_instance_detail}; + match state.repl.inspect(&name) { + Some(InspectResult::Theory(detail)) => { + for line in format_theory_detail(&detail).lines() { + state.log_info(line.to_string()); + } + } + Some(InspectResult::Instance(detail)) => { + for line in format_instance_detail(&detail).lines() { + state.log_info(line.to_string()); + } + } + None => { + state.log_error(format!("Not found: {}", name)); + } + } + } + MetaCommand::Clear => { + state.clear_console(); + } + MetaCommand::Reset => { + state.repl.reset(); + state.selected_item = None; + state.log_success("State reset."); + } + MetaCommand::Chase { instance, max_iterations } => { + self.run_chase(state, &instance, max_iterations); + } + MetaCommand::Source(path) => { + match std::fs::read_to_string(&path) { + Ok(content) => { + state.editor_content = content; + state.current_file = Some(path.clone()); + state.log_info(format!("Loaded: {}", path.display())); + state.execute_editor(); + } + Err(e) => { + state.log_error(format!("Failed to load: {}", e)); + } + } + } + _ => { + state.log_warning("Command not yet implemented in GUI"); + } + } + } + + fn run_chase(&self, state: &mut GuiState, instance_name: &str, max_iterations: Option) { + use crate::core::RelationStorage; + use crate::query::chase::chase_fixpoint; + + let theory_name = match state.repl.instances.get(instance_name) { + Some(e) => e.theory_name.clone(), + None => { + state.log_error(format!("Instance '{}' not found", instance_name)); + return; + } + }; + + let theory = match state.repl.theories.get(&theory_name) { + Some(t) => t.clone(), + None => { + state.log_error(format!("Theory '{}' not found", theory_name)); + return; + } + }; + + let sig = &theory.theory.signature; + let axioms = &theory.theory.axioms; + + if axioms.is_empty() { + state.log_warning(format!("Theory '{}' has no axioms", theory_name)); + return; + } + + state.log_info(format!("Running chase on '{}' ({} axioms)...", instance_name, axioms.len())); + + let entry = state.repl.instances.get_mut(instance_name).unwrap(); + let max_iter = max_iterations.unwrap_or(100); + + let start = std::time::Instant::now(); + let result = chase_fixpoint( + axioms, + &mut entry.structure, + &mut state.repl.store.universe, + sig, + max_iter, + ); + + match result { + Ok(iterations) => { + let elapsed = start.elapsed(); + // Capture structure info before releasing the borrow + let total_tuples: usize = entry.structure.relations.iter().map(|r| r.len()).sum(); + let num_elements = entry.structure.len(); + + state.log_success(format!( + "Chase completed in {} iterations ({:.2}ms)", + iterations, + elapsed.as_secs_f64() * 1000.0 + )); + state.log_info(format!( + "Structure: {} elements, {} relation tuples", + num_elements, + total_tuples + )); + } + Err(e) => { + state.log_error(format!("Chase error: {}", e)); + } + } + } + + fn history_up(&mut self) { + if self.history.is_empty() { + return; + } + match self.history_pos { + None => { + self.history_pos = Some(self.history.len() - 1); + } + Some(pos) if pos > 0 => { + self.history_pos = Some(pos - 1); + } + _ => {} + } + if let Some(pos) = self.history_pos { + self.input = self.history[pos].clone(); + } + } + + fn history_down(&mut self) { + match self.history_pos { + Some(pos) if pos + 1 < self.history.len() => { + self.history_pos = Some(pos + 1); + self.input = self.history[pos + 1].clone(); + } + Some(_) => { + self.history_pos = None; + self.input.clear(); + } + None => {} + } } } diff --git a/src/gui/panels/editor.rs b/src/gui/panels/editor.rs index 97ebaa5..73c9455 100644 --- a/src/gui/panels/editor.rs +++ b/src/gui/panels/editor.rs @@ -72,7 +72,7 @@ impl EditorPanel { // Line numbers column if self.show_line_numbers { ui.allocate_ui_with_layout( - egui::vec2(line_number_width, ui.available_height()), + 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 = diff --git a/src/gui/panels/inspector.rs b/src/gui/panels/inspector.rs index 300cb3a..80f1f55 100644 --- a/src/gui/panels/inspector.rs +++ b/src/gui/panels/inspector.rs @@ -63,10 +63,9 @@ impl InspectorPanel { .auto_shrink([false, false]) .show(ui, |ui| { // Sorts section - egui::CollapsingHeader::new(format!("Sorts ({})", detail.sorts.len())) + let sorts_response = egui::CollapsingHeader::new(format!("Sorts ({})", detail.sorts.len())) .default_open(state.inspector_sorts_expanded) .show(ui, |ui| { - state.inspector_sorts_expanded = true; if detail.sorts.is_empty() { ui.label("(none)"); } else { @@ -75,12 +74,12 @@ impl InspectorPanel { } } }); + state.inspector_sorts_expanded = sorts_response.fully_open(); // Functions section - egui::CollapsingHeader::new(format!("Functions ({})", detail.functions.len())) + let funcs_response = egui::CollapsingHeader::new(format!("Functions ({})", detail.functions.len())) .default_open(state.inspector_functions_expanded) .show(ui, |ui| { - state.inspector_functions_expanded = true; if detail.functions.is_empty() { ui.label("(none)"); } else { @@ -89,12 +88,12 @@ impl InspectorPanel { } } }); + state.inspector_functions_expanded = funcs_response.fully_open(); // Relations section - egui::CollapsingHeader::new(format!("Relations ({})", detail.relations.len())) + let rels_response = egui::CollapsingHeader::new(format!("Relations ({})", detail.relations.len())) .default_open(state.inspector_relations_expanded) .show(ui, |ui| { - state.inspector_relations_expanded = true; if detail.relations.is_empty() { ui.label("(none)"); } else { @@ -103,6 +102,7 @@ impl InspectorPanel { } } }); + state.inspector_relations_expanded = rels_response.fully_open(); // Instance fields section if !detail.instance_fields.is_empty() { @@ -119,10 +119,9 @@ impl InspectorPanel { } // Axioms section - egui::CollapsingHeader::new(format!("Axioms ({})", detail.axioms.len())) + let axioms_response = egui::CollapsingHeader::new(format!("Axioms ({})", detail.axioms.len())) .default_open(state.inspector_axioms_expanded) .show(ui, |ui| { - state.inspector_axioms_expanded = true; if detail.axioms.is_empty() { ui.label("(none)"); } else { @@ -153,6 +152,7 @@ impl InspectorPanel { } } }); + state.inspector_axioms_expanded = axioms_response.fully_open(); }); } @@ -190,10 +190,9 @@ impl InspectorPanel { .show(ui, |ui| { // Elements section let total_elements: usize = detail.elements.iter().map(|(_, v)| v.len()).sum(); - egui::CollapsingHeader::new(format!("Elements ({})", total_elements)) + let elems_response = egui::CollapsingHeader::new(format!("Elements ({})", total_elements)) .default_open(state.inspector_elements_expanded) .show(ui, |ui| { - state.inspector_elements_expanded = true; if detail.elements.is_empty() { ui.label("(none)"); } else { @@ -218,6 +217,7 @@ impl InspectorPanel { } } }); + state.inspector_elements_expanded = elems_response.fully_open(); // Functions section let total_func_values: usize = detail.functions.iter().map(|(_, v)| v.len()).sum(); diff --git a/src/gui/visualizations/graph.rs b/src/gui/visualizations/graph.rs index 62192af..86c106b 100644 --- a/src/gui/visualizations/graph.rs +++ b/src/gui/visualizations/graph.rs @@ -290,16 +290,17 @@ impl GraphView { self.needs_layout = true; } - fn apply_layout(&mut self, ui: &egui::Ui) { - let available = ui.available_size(); - let center = egui::Pos2::new(available.x / 2.0, available.y / 2.0); - + fn apply_layout(&mut self, _ui: &egui::Ui) { if self.nodes.is_empty() { return; } - // Simple circular layout - let radius = (available.x.min(available.y) / 2.0 - 50.0).max(100.0); + // Use a fixed coordinate system centered at (0, 0) + // The transform in draw_graph will handle screen positioning + let center = egui::Pos2::new(0.0, 0.0); + + // Simple circular layout with fixed radius + let radius = 150.0; let count = self.nodes.len(); for (i, node) in self.nodes.iter_mut().enumerate() { @@ -318,34 +319,36 @@ impl GraphView { return; } - // Calculate bounding box + // Calculate bounding box of node positions (in world coordinates) let mut min_x = f32::MAX; let mut min_y = f32::MAX; let mut max_x = f32::MIN; let mut max_y = f32::MIN; for node in &self.nodes { - min_x = min_x.min(node.position.x); - min_y = min_y.min(node.position.y); - max_x = max_x.max(node.position.x); - max_y = max_y.max(node.position.y); + let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position); + min_x = min_x.min(pos.x); + min_y = min_y.min(pos.y); + max_x = max_x.max(pos.x); + max_y = max_y.max(pos.y); } - let width = max_x - min_x; - let height = max_y - min_y; + let width = (max_x - min_x).max(1.0); + let height = (max_y - min_y).max(1.0); let available = ui.available_size(); - // Calculate zoom to fit - let zoom_x = if width > 0.0 { (available.x - 100.0) / width } else { 1.0 }; - let zoom_y = if height > 0.0 { (available.y - 100.0) / height } else { 1.0 }; + // Calculate zoom to fit with padding + let padding = 100.0; + let zoom_x = (available.x - padding) / width; + let zoom_y = (available.y - padding) / height; self.zoom = zoom_x.min(zoom_y).clamp(0.1, 2.0); - // Calculate pan to center - let center_x = (min_x + max_x) / 2.0; - let center_y = (min_y + max_y) / 2.0; + // Reset pan to center the content (since our world origin is already at center) + let world_center_x = (min_x + max_x) / 2.0; + let world_center_y = (min_y + max_y) / 2.0; self.pan = egui::Vec2::new( - available.x / 2.0 - center_x * self.zoom, - available.y / 2.0 - center_y * self.zoom, + -world_center_x * self.zoom, + -world_center_y * self.zoom, ); } @@ -378,11 +381,12 @@ impl GraphView { } } - // Transform helper + // Transform helper - centers (0,0) world coordinates in the view + let center = rect.center(); let transform = |pos: egui::Pos2| -> egui::Pos2 { egui::Pos2::new( - rect.min.x + pos.x * self.zoom + self.pan.x, - rect.min.y + pos.y * self.zoom + self.pan.y, + center.x + pos.x * self.zoom + self.pan.x, + center.y + pos.y * self.zoom + self.pan.y, ) };