Compare commits
7 Commits
fcb6bd3e1e
...
9ec827c607
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
9ec827c607 | ||
|
|
84d1f0d86a | ||
|
|
6518e99263 | ||
|
|
e6b1c64ad9 | ||
|
|
d13c756954 | ||
|
|
868891289b | ||
|
|
07fe9b2512 |
18
README2.md
18
README2.md
@ -97,6 +97,17 @@ src/gui/
|
|||||||
- Color-coded messages: info (gray), success (green), error (red), warning (orange)
|
- Color-coded messages: info (gray), success (green), error (red), warning (orange)
|
||||||
- Auto-scroll option
|
- Auto-scroll option
|
||||||
- Clear button
|
- Clear button
|
||||||
|
- **Integrated REPL input** with command history (Up/Down arrows)
|
||||||
|
- Type `:help` for commands
|
||||||
|
- Type `:list` to list theories/instances
|
||||||
|
- Type `:inspect <name>` to inspect
|
||||||
|
- Type `:chase <instance>` 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**
|
**Chase Visualization**
|
||||||
- Step/Run All/Stop controls
|
- Step/Run All/Stop controls
|
||||||
@ -124,8 +135,9 @@ src/gui/
|
|||||||
│ Graph │ │ theory Foo { │ │
|
│ Graph │ │ theory Foo { │ │
|
||||||
│ ▼ Instances│ │ X : Sort; │ │
|
│ ▼ Instances│ │ X : Sort; │ │
|
||||||
│ Chain3 │ │ } [Run] [Clear] │ │
|
│ Chain3 │ │ } [Run] [Clear] │ │
|
||||||
│ │ └─────────────────────────────────────────┘ │
|
│ │ ├─────────────────────────────────────────┤ │
|
||||||
│ │ ┌─────────────────────────────────────────┐ │
|
│ │ │ ═══════════ [drag to resize] ═══════════│ │
|
||||||
|
│ │ ├─────────────────────────────────────────┤ │
|
||||||
│ │ │ Inspector: Chain3 : Preorder │ │
|
│ │ │ Inspector: Chain3 : Preorder │ │
|
||||||
│ │ │ ▼ Elements (3) │ │
|
│ │ │ ▼ Elements (3) │ │
|
||||||
│ │ │ X: bot, mid, top │ │
|
│ │ │ X: bot, mid, top │ │
|
||||||
@ -136,6 +148,8 @@ src/gui/
|
|||||||
│ 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) │
|
||||||
|
│─────────────────────────────────────────────────────────────│
|
||||||
|
│ geolog> :list [Run] │
|
||||||
└─────────────────────────────────────────────────────────────┘
|
└─────────────────────────────────────────────────────────────┘
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|||||||
@ -21,6 +21,9 @@ 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 {
|
||||||
@ -34,6 +37,7 @@ 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
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -288,7 +292,11 @@ impl GeologApp {
|
|||||||
CentralView::EditorAndInspector => {
|
CentralView::EditorAndInspector => {
|
||||||
// Split vertically: editor on top, inspector on bottom
|
// Split vertically: editor on top, inspector on bottom
|
||||||
let available_height = ui.available_height();
|
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
|
// Editor section
|
||||||
ui.allocate_ui_with_layout(
|
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
|
// 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 => {
|
CentralView::ChaseVisualization => {
|
||||||
self.chase_viz.show(ui, &mut self.state);
|
self.chase_viz.show(ui, &mut self.state);
|
||||||
|
|||||||
@ -56,10 +56,9 @@ impl BrowserPanel {
|
|||||||
format!("Theories ({}/{})", filtered.len(), theories.len())
|
format!("Theories ({}/{})", filtered.len(), theories.len())
|
||||||
};
|
};
|
||||||
|
|
||||||
egui::CollapsingHeader::new(header)
|
let response = egui::CollapsingHeader::new(header)
|
||||||
.default_open(state.theories_expanded)
|
.default_open(state.theories_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.theories_expanded = true;
|
|
||||||
if filtered.is_empty() {
|
if filtered.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} 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) {
|
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())
|
format!("Instances ({}/{})", filtered.len(), instances.len())
|
||||||
};
|
};
|
||||||
|
|
||||||
egui::CollapsingHeader::new(header)
|
let response = egui::CollapsingHeader::new(header)
|
||||||
.default_open(state.instances_expanded)
|
.default_open(state.instances_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.instances_expanded = true;
|
|
||||||
if filtered.is_empty() {
|
if filtered.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} else {
|
||||||
@ -168,6 +167,7 @@ impl BrowserPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
state.instances_expanded = response.fully_open();
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@ -1,20 +1,32 @@
|
|||||||
//! Console panel for displaying output and error messages
|
//! 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 eframe::egui;
|
||||||
|
|
||||||
use crate::gui::state::{GuiState, MessageKind};
|
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 {
|
pub struct ConsolePanel {
|
||||||
/// Whether to auto-scroll to bottom
|
/// Whether to auto-scroll to bottom
|
||||||
auto_scroll: bool,
|
auto_scroll: bool,
|
||||||
|
/// REPL input buffer
|
||||||
|
input: String,
|
||||||
|
/// Command history
|
||||||
|
history: Vec<String>,
|
||||||
|
/// Current position in history (for up/down navigation)
|
||||||
|
history_pos: Option<usize>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl ConsolePanel {
|
impl ConsolePanel {
|
||||||
pub fn new() -> Self {
|
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) {
|
pub fn show(&mut self, ui: &mut egui::Ui, state: &mut GuiState) {
|
||||||
@ -35,14 +47,16 @@ impl ConsolePanel {
|
|||||||
|
|
||||||
ui.separator();
|
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()
|
let scroll_area = egui::ScrollArea::vertical()
|
||||||
.auto_shrink([false, false])
|
.auto_shrink([false, false])
|
||||||
|
.max_height(available_height)
|
||||||
.stick_to_bottom(self.auto_scroll);
|
.stick_to_bottom(self.auto_scroll);
|
||||||
|
|
||||||
scroll_area.show(ui, |ui| {
|
scroll_area.show(ui, |ui| {
|
||||||
if state.console_messages.is_empty() {
|
if state.console_messages.is_empty() {
|
||||||
ui.label("(no messages)");
|
ui.label("Type commands below (e.g., :help, :list, or geolog code)");
|
||||||
} else {
|
} else {
|
||||||
for message in &state.console_messages {
|
for message in &state.console_messages {
|
||||||
let color = match message.kind {
|
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 <n> Inspect a theory or instance");
|
||||||
|
state.log_info(" :chase <inst> Run chase on instance");
|
||||||
|
state.log_info(" :reset Reset all state");
|
||||||
|
state.log_info(" :clear Clear console");
|
||||||
|
state.log_info("");
|
||||||
|
state.log_info("Or type geolog code directly.");
|
||||||
|
}
|
||||||
|
Some(t) => {
|
||||||
|
state.log_info(format!("Help topic: {}", t));
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
MetaCommand::List(target) => {
|
||||||
|
match target {
|
||||||
|
ListTarget::Theories | ListTarget::All => {
|
||||||
|
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<usize>) {
|
||||||
|
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 => {}
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@ -72,7 +72,7 @@ impl EditorPanel {
|
|||||||
// Line numbers column
|
// Line numbers column
|
||||||
if self.show_line_numbers {
|
if self.show_line_numbers {
|
||||||
ui.allocate_ui_with_layout(
|
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),
|
egui::Layout::top_down(egui::Align::RIGHT),
|
||||||
|ui| {
|
|ui| {
|
||||||
ui.style_mut().visuals.override_text_color =
|
ui.style_mut().visuals.override_text_color =
|
||||||
|
|||||||
@ -63,10 +63,9 @@ impl InspectorPanel {
|
|||||||
.auto_shrink([false, false])
|
.auto_shrink([false, false])
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
// Sorts section
|
// 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)
|
.default_open(state.inspector_sorts_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.inspector_sorts_expanded = true;
|
|
||||||
if detail.sorts.is_empty() {
|
if detail.sorts.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} else {
|
||||||
@ -75,12 +74,12 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
state.inspector_sorts_expanded = sorts_response.fully_open();
|
||||||
|
|
||||||
// Functions section
|
// 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)
|
.default_open(state.inspector_functions_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.inspector_functions_expanded = true;
|
|
||||||
if detail.functions.is_empty() {
|
if detail.functions.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} else {
|
||||||
@ -89,12 +88,12 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
state.inspector_functions_expanded = funcs_response.fully_open();
|
||||||
|
|
||||||
// Relations section
|
// 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)
|
.default_open(state.inspector_relations_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.inspector_relations_expanded = true;
|
|
||||||
if detail.relations.is_empty() {
|
if detail.relations.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} else {
|
||||||
@ -103,6 +102,7 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
state.inspector_relations_expanded = rels_response.fully_open();
|
||||||
|
|
||||||
// Instance fields section
|
// Instance fields section
|
||||||
if !detail.instance_fields.is_empty() {
|
if !detail.instance_fields.is_empty() {
|
||||||
@ -119,10 +119,9 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Axioms section
|
// 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)
|
.default_open(state.inspector_axioms_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.inspector_axioms_expanded = true;
|
|
||||||
if detail.axioms.is_empty() {
|
if detail.axioms.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} else {
|
||||||
@ -153,6 +152,7 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
state.inspector_axioms_expanded = axioms_response.fully_open();
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -190,10 +190,9 @@ impl InspectorPanel {
|
|||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
// Elements section
|
// Elements section
|
||||||
let total_elements: usize = detail.elements.iter().map(|(_, v)| v.len()).sum();
|
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)
|
.default_open(state.inspector_elements_expanded)
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
state.inspector_elements_expanded = true;
|
|
||||||
if detail.elements.is_empty() {
|
if detail.elements.is_empty() {
|
||||||
ui.label("(none)");
|
ui.label("(none)");
|
||||||
} else {
|
} else {
|
||||||
@ -218,6 +217,7 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
|
state.inspector_elements_expanded = elems_response.fully_open();
|
||||||
|
|
||||||
// Functions section
|
// Functions section
|
||||||
let total_func_values: usize = detail.functions.iter().map(|(_, v)| v.len()).sum();
|
let total_func_values: usize = detail.functions.iter().map(|(_, v)| v.len()).sum();
|
||||||
|
|||||||
@ -290,16 +290,17 @@ impl GraphView {
|
|||||||
self.needs_layout = true;
|
self.needs_layout = true;
|
||||||
}
|
}
|
||||||
|
|
||||||
fn apply_layout(&mut self, ui: &egui::Ui) {
|
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);
|
|
||||||
|
|
||||||
if self.nodes.is_empty() {
|
if self.nodes.is_empty() {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Simple circular layout
|
// Use a fixed coordinate system centered at (0, 0)
|
||||||
let radius = (available.x.min(available.y) / 2.0 - 50.0).max(100.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();
|
let count = self.nodes.len();
|
||||||
|
|
||||||
for (i, node) in self.nodes.iter_mut().enumerate() {
|
for (i, node) in self.nodes.iter_mut().enumerate() {
|
||||||
@ -318,34 +319,36 @@ impl GraphView {
|
|||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Calculate bounding box
|
// Calculate bounding box of node positions (in world coordinates)
|
||||||
let mut min_x = f32::MAX;
|
let mut min_x = f32::MAX;
|
||||||
let mut min_y = f32::MAX;
|
let mut min_y = f32::MAX;
|
||||||
let mut max_x = f32::MIN;
|
let mut max_x = f32::MIN;
|
||||||
let mut max_y = f32::MIN;
|
let mut max_y = f32::MIN;
|
||||||
|
|
||||||
for node in &self.nodes {
|
for node in &self.nodes {
|
||||||
min_x = min_x.min(node.position.x);
|
let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
|
||||||
min_y = min_y.min(node.position.y);
|
min_x = min_x.min(pos.x);
|
||||||
max_x = max_x.max(node.position.x);
|
min_y = min_y.min(pos.y);
|
||||||
max_y = max_y.max(node.position.y);
|
max_x = max_x.max(pos.x);
|
||||||
|
max_y = max_y.max(pos.y);
|
||||||
}
|
}
|
||||||
|
|
||||||
let width = max_x - min_x;
|
let width = (max_x - min_x).max(1.0);
|
||||||
let height = max_y - min_y;
|
let height = (max_y - min_y).max(1.0);
|
||||||
let available = ui.available_size();
|
let available = ui.available_size();
|
||||||
|
|
||||||
// Calculate zoom to fit
|
// Calculate zoom to fit with padding
|
||||||
let zoom_x = if width > 0.0 { (available.x - 100.0) / width } else { 1.0 };
|
let padding = 100.0;
|
||||||
let zoom_y = if height > 0.0 { (available.y - 100.0) / height } else { 1.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);
|
self.zoom = zoom_x.min(zoom_y).clamp(0.1, 2.0);
|
||||||
|
|
||||||
// Calculate pan to center
|
// Reset pan to center the content (since our world origin is already at center)
|
||||||
let center_x = (min_x + max_x) / 2.0;
|
let world_center_x = (min_x + max_x) / 2.0;
|
||||||
let 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(
|
||||||
available.x / 2.0 - center_x * self.zoom,
|
-world_center_x * self.zoom,
|
||||||
available.y / 2.0 - center_y * 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 {
|
let transform = |pos: egui::Pos2| -> egui::Pos2 {
|
||||||
egui::Pos2::new(
|
egui::Pos2::new(
|
||||||
rect.min.x + pos.x * self.zoom + self.pan.x,
|
center.x + pos.x * self.zoom + self.pan.x,
|
||||||
rect.min.y + pos.y * self.zoom + self.pan.y,
|
center.y + pos.y * self.zoom + self.pan.y,
|
||||||
)
|
)
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user