Compare commits
8 Commits
9ec827c607
...
fcb6bd3e1e
| Author | SHA1 | Date | |
|---|---|---|---|
|
|
fcb6bd3e1e | ||
|
|
a6a57ab53f | ||
|
|
7a57c6daef | ||
|
|
38bccbfa3f | ||
|
|
15821e53ce | ||
|
|
966cd3ad1b | ||
|
|
4d1044b0af | ||
|
|
ac2d363737 |
18
README2.md
18
README2.md
@ -97,17 +97,6 @@ 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
|
||||||
@ -135,9 +124,8 @@ 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 │ │
|
||||||
@ -148,8 +136,6 @@ 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,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
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -292,11 +288,7 @@ 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 splitter_height = 8.0;
|
let editor_height = available_height * 0.5;
|
||||||
// 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(
|
||||||
@ -307,63 +299,10 @@ impl GeologApp {
|
|||||||
},
|
},
|
||||||
);
|
);
|
||||||
|
|
||||||
// Draggable splitter
|
ui.separator();
|
||||||
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
|
||||||
ui.allocate_ui_with_layout(
|
self.inspector.show(ui, &mut self.state);
|
||||||
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,9 +56,10 @@ impl BrowserPanel {
|
|||||||
format!("Theories ({}/{})", filtered.len(), theories.len())
|
format!("Theories ({}/{})", filtered.len(), theories.len())
|
||||||
};
|
};
|
||||||
|
|
||||||
let response = egui::CollapsingHeader::new(header)
|
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 {
|
||||||
@ -95,7 +96,6 @@ 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,9 +117,10 @@ impl BrowserPanel {
|
|||||||
format!("Instances ({}/{})", filtered.len(), instances.len())
|
format!("Instances ({}/{})", filtered.len(), instances.len())
|
||||||
};
|
};
|
||||||
|
|
||||||
let response = egui::CollapsingHeader::new(header)
|
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 {
|
||||||
@ -167,7 +168,6 @@ impl BrowserPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
state.instances_expanded = response.fully_open();
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@ -1,32 +1,20 @@
|
|||||||
//! 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 and a REPL input.
|
//! Shows a scrollable log of messages with color coding.
|
||||||
|
|
||||||
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 and REPL input
|
/// Console panel for output messages
|
||||||
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 {
|
Self { auto_scroll: true }
|
||||||
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) {
|
||||||
@ -47,16 +35,14 @@ impl ConsolePanel {
|
|||||||
|
|
||||||
ui.separator();
|
ui.separator();
|
||||||
|
|
||||||
// Scrollable message area (takes most of the space)
|
// Scrollable message area
|
||||||
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("Type commands below (e.g., :help, :list, or geolog code)");
|
ui.label("(no messages)");
|
||||||
} else {
|
} else {
|
||||||
for message in &state.console_messages {
|
for message in &state.console_messages {
|
||||||
let color = match message.kind {
|
let color = match message.kind {
|
||||||
@ -88,320 +74,6 @@ 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().max(0.0)),
|
egui::vec2(line_number_width, ui.available_height()),
|
||||||
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,9 +63,10 @@ impl InspectorPanel {
|
|||||||
.auto_shrink([false, false])
|
.auto_shrink([false, false])
|
||||||
.show(ui, |ui| {
|
.show(ui, |ui| {
|
||||||
// Sorts section
|
// Sorts section
|
||||||
let sorts_response = egui::CollapsingHeader::new(format!("Sorts ({})", detail.sorts.len()))
|
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 {
|
||||||
@ -74,12 +75,12 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
state.inspector_sorts_expanded = sorts_response.fully_open();
|
|
||||||
|
|
||||||
// Functions section
|
// Functions section
|
||||||
let funcs_response = egui::CollapsingHeader::new(format!("Functions ({})", detail.functions.len()))
|
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 {
|
||||||
@ -88,12 +89,12 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
state.inspector_functions_expanded = funcs_response.fully_open();
|
|
||||||
|
|
||||||
// Relations section
|
// Relations section
|
||||||
let rels_response = egui::CollapsingHeader::new(format!("Relations ({})", detail.relations.len()))
|
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 {
|
||||||
@ -102,7 +103,6 @@ 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,9 +119,10 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
|
|
||||||
// Axioms section
|
// Axioms section
|
||||||
let axioms_response = egui::CollapsingHeader::new(format!("Axioms ({})", detail.axioms.len()))
|
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 {
|
||||||
@ -152,7 +153,6 @@ impl InspectorPanel {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
});
|
});
|
||||||
state.inspector_axioms_expanded = axioms_response.fully_open();
|
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -190,9 +190,10 @@ 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();
|
||||||
let elems_response = egui::CollapsingHeader::new(format!("Elements ({})", total_elements))
|
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 {
|
||||||
@ -217,7 +218,6 @@ 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,17 +290,16 @@ 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;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Use a fixed coordinate system centered at (0, 0)
|
// Simple circular layout
|
||||||
// The transform in draw_graph will handle screen positioning
|
let radius = (available.x.min(available.y) / 2.0 - 50.0).max(100.0);
|
||||||
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() {
|
||||||
@ -319,36 +318,34 @@ impl GraphView {
|
|||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
// Calculate bounding box of node positions (in world coordinates)
|
// Calculate bounding box
|
||||||
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 {
|
||||||
let pos = self.node_positions.get(&node.id).copied().unwrap_or(node.position);
|
min_x = min_x.min(node.position.x);
|
||||||
min_x = min_x.min(pos.x);
|
min_y = min_y.min(node.position.y);
|
||||||
min_y = min_y.min(pos.y);
|
max_x = max_x.max(node.position.x);
|
||||||
max_x = max_x.max(pos.x);
|
max_y = max_y.max(node.position.y);
|
||||||
max_y = max_y.max(pos.y);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
let width = (max_x - min_x).max(1.0);
|
let width = max_x - min_x;
|
||||||
let height = (max_y - min_y).max(1.0);
|
let height = max_y - min_y;
|
||||||
let available = ui.available_size();
|
let available = ui.available_size();
|
||||||
|
|
||||||
// Calculate zoom to fit with padding
|
// Calculate zoom to fit
|
||||||
let padding = 100.0;
|
let zoom_x = if width > 0.0 { (available.x - 100.0) / width } else { 1.0 };
|
||||||
let zoom_x = (available.x - padding) / width;
|
let zoom_y = if height > 0.0 { (available.y - 100.0) / height } else { 1.0 };
|
||||||
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);
|
||||||
|
|
||||||
// Reset pan to center the content (since our world origin is already at center)
|
// Calculate pan to center
|
||||||
let world_center_x = (min_x + max_x) / 2.0;
|
let center_x = (min_x + max_x) / 2.0;
|
||||||
let world_center_y = (min_y + max_y) / 2.0;
|
let center_y = (min_y + max_y) / 2.0;
|
||||||
self.pan = egui::Vec2::new(
|
self.pan = egui::Vec2::new(
|
||||||
-world_center_x * self.zoom,
|
available.x / 2.0 - center_x * self.zoom,
|
||||||
-world_center_y * self.zoom,
|
available.y / 2.0 - center_y * self.zoom,
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -381,12 +378,11 @@ impl GraphView {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
// Transform helper - centers (0,0) world coordinates in the view
|
// Transform helper
|
||||||
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,
|
rect.min.x + pos.x * self.zoom + self.pan.x,
|
||||||
center.y + pos.y * self.zoom + self.pan.y,
|
rect.min.y + pos.y * self.zoom + self.pan.y,
|
||||||
)
|
)
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user